# HG changeset patch
# User zhangx
# Date 1454235313 -28800
# Node ID f7b33c633b96ede415a7059c99555cba75a8caad
# Parent  524bd3caa6b6de37e6a12591b05f9b0a911daa42
Small improvemnts in PIPBasis.thy

diff -r 524bd3caa6b6 -r f7b33c633b96 PIPBasics.thy
--- a/PIPBasics.thy	Fri Jan 29 11:01:13 2016 +0800
+++ b/PIPBasics.thy	Sun Jan 31 18:15:13 2016 +0800
@@ -2,6 +2,8 @@
 imports PIPDefs
 begin
 
+section {* Generic aulxiliary lemmas *}
+
 lemma f_image_eq:
   assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"
   shows "f ` A = g ` A"
@@ -84,6 +86,8 @@
   finally show ?thesis by simp
 qed
 
+section {* Lemmas do not depend on trace validity *}
+
 lemma birth_time_lt:  
   assumes "s \<noteq> []"
   shows "last_set th s < length s"
@@ -152,116 +156,9 @@
   thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
 qed
 
-(* ccc *)
-
-
-locale valid_trace = 
-  fixes s
-  assumes vt : "vt s"
-
-locale valid_trace_e = valid_trace +
-  fixes e
-  assumes vt_e: "vt (e#s)"
-begin
-
-lemma pip_e: "PIP s e"
-  using vt_e by (cases, simp)  
-
-end
-
-locale valid_trace_create = valid_trace_e + 
-  fixes th prio
-  assumes is_create: "e = Create th prio"
-
-locale valid_trace_exit = valid_trace_e + 
-  fixes th
-  assumes is_exit: "e = Exit th"
-
-locale valid_trace_p = valid_trace_e + 
-  fixes th cs
-  assumes is_p: "e = P th cs"
-
-locale valid_trace_v = valid_trace_e + 
-  fixes th cs
-  assumes is_v: "e = V th cs"
-begin
-  definition "rest = tl (wq s cs)"
-  definition "wq' = (SOME q. distinct q \<and> set q = set rest)"
-end
-
-locale valid_trace_v_n = valid_trace_v +
-  assumes rest_nnl: "rest \<noteq> []"
-
-locale valid_trace_v_e = valid_trace_v +
-  assumes rest_nil: "rest = []"
-
-locale valid_trace_set= valid_trace_e + 
-  fixes th prio
-  assumes is_set: "e = Set th prio"
-
-context valid_trace
-begin
-
-lemma ind [consumes 0, case_names Nil Cons, induct type]:
-  assumes "PP []"
-     and "(\<And>s e. valid_trace_e s e \<Longrightarrow>
-                   PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"
-     shows "PP s"
-proof(induct rule:vt.induct[OF vt, case_names Init Step])
-  case Init
-  from assms(1) show ?case .
-next
-  case (Step s e)
-  show ?case
-  proof(rule assms(2))
-    show "valid_trace_e s e" using Step by (unfold_locales, auto)
-  next
-    show "PP s" using Step by simp
-  next
-    show "PIP s e" using Step by simp
-  qed
-qed
-
-lemma  vt_moment: "\<And> t. vt (moment t s)"
-proof(induct rule:ind)
-  case Nil
-  thus ?case by (simp add:vt_nil)
-next
-  case (Cons s e t)
-  show ?case
-  proof(cases "t \<ge> length (e#s)")
-    case True
-    from True have "moment t (e#s) = e#s" by simp
-    thus ?thesis using Cons
-      by (simp add:valid_trace_def valid_trace_e_def, auto)
-  next
-    case False
-    from Cons have "vt (moment t s)" by simp
-    moreover have "moment t (e#s) = moment t s"
-    proof -
-      from False have "t \<le> length s" by simp
-      from moment_app [OF this, of "[e]"] 
-      show ?thesis by simp
-    qed
-    ultimately show ?thesis by simp
-  qed
-qed
-
-lemma finite_threads:
-  shows "finite (threads s)"
-using vt by (induct) (auto elim: step.cases)
-
-end
-
 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
   by (unfold s_RAG_def, auto)
 
-locale valid_moment = valid_trace + 
-  fixes i :: nat
-
-sublocale valid_moment < vat_moment: valid_trace "(moment i s)"
-  by (unfold_locales, insert vt_moment, auto)
-
 lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
   by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
 
@@ -289,9 +186,6 @@
   using assms
   by (simp add:runing_def readys_def s_waiting_def wq_def)
 
-context valid_trace
-begin
-
 lemma runing_wqE:
   assumes "th \<in> runing s"
   and "th \<in> set (wq s cs)"
@@ -312,12 +206,287 @@
   with eq_wq that show ?thesis by metis
 qed
 
+(* ccc *)
+
+section {* Locales used to investigate the execution of PIP *}
+
+text {* 
+  The following locale @{text valid_trace} is used to constrain the 
+  trace to be valid. All properties hold for valid traces are 
+  derived under this locale. 
+*}
+locale valid_trace = 
+  fixes s
+  assumes vt : "vt s"
+
+text {* 
+  The following locale @{text valid_trace_e} describes 
+  the valid extension of a valid trace. The event @{text "e"}
+  represents an event in the system, which corresponds 
+  to a one step operation of the PIP protocol. 
+  It is required that @{text "e"} is an event eligible to happen
+  under state @{text "s"}, which is already required to be valid
+  by the parent locale @{text "valid_trace"}.
+
+  This locale is used to investigate one step execution of PIP, 
+  properties concerning the effects of @{text "e"}'s execution, 
+  for example, how the values of observation functions are changed, 
+  or how desirable properties are kept invariant, are derived
+  under this locale. The state before execution is @{text "s"}, while
+  the state after execution is @{text "e#s"}. Therefore, the lemmas 
+  derived usually relate observations on @{text "e#s"} to those 
+  on @{text "s"}.
+*}
+
+locale valid_trace_e = valid_trace +
+  fixes e
+  assumes vt_e: "vt (e#s)"
+begin
+
+text {*
+  The following lemma shows that @{text "e"} must be a 
+  eligible event (or a valid step) to be taken under
+  the state represented by @{text "s"}.
+*}
+lemma pip_e: "PIP s e"
+  using vt_e by (cases, simp)  
+
 end
 
+text {*
+  Because @{term "e#s"} is also a valid trace, properties 
+  derived for valid trace @{term s} also hold on @{term "e#s"}.
+*}
+sublocale valid_trace_e < vat_es!: valid_trace "e#s" 
+  using vt_e
+  by (unfold_locales, simp)
+
+text {*
+  For each specific event (or operation), there is a sublocale
+  further constraining that the event @{text e} to be that 
+  particular event. 
+
+  For example, the following 
+  locale @{text "valid_trace_create"} is the sublocale for 
+  event @{term "Create"}:
+*}
+locale valid_trace_create = valid_trace_e + 
+  fixes th prio
+  assumes is_create: "e = Create th prio"
+
+locale valid_trace_exit = valid_trace_e + 
+  fixes th
+  assumes is_exit: "e = Exit th"
+
+locale valid_trace_p = valid_trace_e + 
+  fixes th cs
+  assumes is_p: "e = P th cs"
+
+text {*
+  locale @{text "valid_trace_p"} is divided further into two 
+  sublocales, namely, @{text "valid_trace_p_h"} 
+  and @{text "valid_trace_p_w"}.
+*}
+
+text {*
+  The following two sublocales @{text "valid_trace_p_h"}
+  and @{text "valid_trace_p_w"} represent two complementary 
+  cases under @{text "valid_trace_p"}, where
+  @{text "valid_trace_p_h"} further constraints that
+  @{text "wq s cs = []"}, which means the waiting queue of 
+  the requested resource @{text "cs"} is empty, in which
+  case,  the requesting thread @{text "th"} 
+  will take hold of @{text "cs"}. 
+
+  Opposite to @{text "valid_trace_p_h"},
+  @{text "valid_trace_p_w"} constraints that
+  @{text "wq s cs \<noteq> []"}, which means the waiting queue of 
+  the requested resource @{text "cs"} is nonempty, in which
+  case,  the requesting thread @{text "th"} will be blocked
+  on @{text "cs"}: 
+
+  Peculiar properties will be derived under respective 
+  locales.
+*}
+
+locale valid_trace_p_h = valid_trace_p +
+  assumes we: "wq s cs = []"
+
+locale valid_trace_p_w = valid_trace_p +
+  assumes wne: "wq s cs \<noteq> []"
+begin
+
+text {*
+  The following @{text "holder"} designates
+  the holder of @{text "cs"} before the @{text "P"}-operation.
+*}
+definition "holder = hd (wq s cs)"
+
+text {*
+  The following @{text "waiters"} designates
+  the list of threads waiting for @{text "cs"} 
+  before the @{text "P"}-operation.
+*}
+definition "waiters = tl (wq s cs)"
+end
+
+text {* 
+  @{text "valid_trace_v"} is set for the @{term V}-operation.
+*}
+locale valid_trace_v = valid_trace_e + 
+  fixes th cs
+  assumes is_v: "e = V th cs"
+begin
+  -- {* The following @{text "rest"} is the tail of 
+        waiting queue of the resource @{text "cs"}
+        to be released by this @{text "V"}-operation.
+     *}
+  definition "rest = tl (wq s cs)"
+
+  text {*
+    The following @{text "wq'"} is the waiting
+    queue of @{term "cs"}
+    after the @{text "V"}-operation, which
+    is simply a reordering of @{term "rest"}. 
+
+    The effect of this reordering needs to be 
+    understood by two cases:
+    \begin{enumerate}
+    \item When @{text "rest = []"},
+    the reordering gives rise to an empty list as well, 
+    which means there is no thread holding or waiting 
+    for resource @{term "cs"}, therefore, it is free.
+
+    \item When @{text "rest \<noteq> []"}, the effect of 
+    this reordering is to arbitrarily 
+    switch one thread in @{term "rest"} to the 
+    head, which, by definition take over the hold
+    of @{term "cs"} and is designated by @{text "taker"}
+    in the following sublocale @{text "valid_trace_v_n"}.
+  *}
+  definition "wq' = (SOME q. distinct q \<and> set q = set rest)"
+
+  text {* 
+  The following @{text "rest'"} is the tail of the 
+  waiting queue after the @{text "V"}-operation. 
+  It plays only auxiliary role to ease reasoning. 
+  *}
+  definition "rest' = tl wq'"
+
+end
+
+text {* 
+  In the following, @{text "valid_trace_v"} is also 
+  divided into two 
+  sublocales: when @{text "rest"} is empty (represented
+  by @{text "valid_trace_v_e"}), which means, there is no thread waiting 
+  for @{text "cs"}, therefore, after the @{text "V"}-operation, 
+  it will become free; otherwise (represented 
+  by @{text "valid_trace_v_n"}), one thread 
+  will be picked from those in @{text "rest"} to take 
+  over @{text "cs"}.
+*}
+
+locale valid_trace_v_e = valid_trace_v +
+  assumes rest_nil: "rest = []"
+
+locale valid_trace_v_n = valid_trace_v +
+  assumes rest_nnl: "rest \<noteq> []"
+begin
+
+text {* 
+  The following @{text "taker"} is the thread to 
+  take over @{text "cs"}. 
+*}
+  definition "taker = hd wq'"
+
+end
+
+
+locale valid_trace_set = valid_trace_e + 
+  fixes th prio
+  assumes is_set: "e = Set th prio"
+
+context valid_trace
+begin
+
+text {*
+  Induction rule introduced to easy the 
+  derivation of properties for valid trace @{term "s"}.
+  One more premises, namely @{term "valid_trace_e s e"}
+  is added, so that an interpretation of 
+  @{text "valid_trace_e"} can be instantiated 
+  so that all properties derived so far becomes 
+  available in the proof of induction step.
+
+  You will see its use in the proofs that follows.
+*}
+lemma ind [consumes 0, case_names Nil Cons, induct type]:
+  assumes "PP []"
+     and "(\<And>s e. valid_trace_e s e \<Longrightarrow>
+                   PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"
+     shows "PP s"
+proof(induct rule:vt.induct[OF vt, case_names Init Step])
+  case Init
+  from assms(1) show ?case .
+next
+  case (Step s e)
+  show ?case
+  proof(rule assms(2))
+    show "valid_trace_e s e" using Step by (unfold_locales, auto)
+  next
+    show "PP s" using Step by simp
+  next
+    show "PIP s e" using Step by simp
+  qed
+qed
+
+text {*
+  The following lemma says that if @{text "s"} is a valid state, so 
+  is its any postfix. Where @{term "monent t s"} is the postfix of 
+  @{term "s"} with length @{term "t"}.
+*}
+lemma  vt_moment: "\<And> t. vt (moment t s)"
+proof(induct rule:ind)
+  case Nil
+  thus ?case by (simp add:vt_nil)
+next
+  case (Cons s e t)
+  show ?case
+  proof(cases "t \<ge> length (e#s)")
+    case True
+    from True have "moment t (e#s) = e#s" by simp
+    thus ?thesis using Cons
+      by (simp add:valid_trace_def valid_trace_e_def, auto)
+  next
+    case False
+    from Cons have "vt (moment t s)" by simp
+    moreover have "moment t (e#s) = moment t s"
+    proof -
+      from False have "t \<le> length s" by simp
+      from moment_app [OF this, of "[e]"] 
+      show ?thesis by simp
+    qed
+    ultimately show ?thesis by simp
+  qed
+qed
+end
+
+text {*
+  The following locale @{text "valid_moment"} is to inherit the properties 
+  derived on any valid state to the prefix of it, with length @{text "i"}.
+*}
+locale valid_moment = valid_trace + 
+  fixes i :: nat
+
+sublocale valid_moment < vat_moment: valid_trace "(moment i s)"
+  by (unfold_locales, insert vt_moment, auto)
+
+
 context valid_trace_create
 begin
 
-lemma wq_neq_simp [simp]:
+lemma wq_kept [simp]:
   shows "wq (e#s) cs' = wq s cs'"
     using assms unfolding is_create wq_def
   by (auto simp:Let_def)
@@ -331,7 +500,7 @@
 context valid_trace_exit
 begin
 
-lemma wq_neq_simp [simp]:
+lemma wq_kept [simp]:
   shows "wq (e#s) cs' = wq s cs'"
     using assms unfolding is_exit wq_def
   by (auto simp:Let_def)
@@ -342,7 +511,7 @@
   using assms by simp
 end
 
-context valid_trace_p
+context valid_trace_p (* ccc *)
 begin
 
 lemma wq_neq_simp [simp]:
@@ -482,7 +651,7 @@
 context valid_trace_set
 begin
 
-lemma wq_neq_simp [simp]:
+lemma wq_kept [simp]:
   shows "wq (e#s) cs' = wq s cs'"
     using assms unfolding is_set wq_def
   by (auto simp:Let_def)
@@ -496,7 +665,7 @@
 context valid_trace
 begin
 
-lemma actor_inv: 
+lemma actor_inv: (* ccc *)
   assumes "PIP s e"
   and "\<not> isCreate e"
   shows "actor e \<in> runing s"
@@ -586,7 +755,7 @@
   thus ?thesis by auto
 qed (insert assms, auto simp:wq_def Let_def split:if_splits)
 
-lemma wq_out_inv: 
+lemma wq_out_inv: (* ccc *)
   assumes s_in: "thread \<in> set (wq s cs)"
   and s_hd: "thread = hd (wq s cs)"
   and s_i: "thread \<noteq> hd (wq (e#s) cs)"
@@ -996,10 +1165,6 @@
   thus "x \<noteq> []" using rest_nnl by auto
 qed 
 
-definition "taker = hd wq'"
-
-definition "rest' = tl wq'"
-
 lemma eq_wq': "wq' = taker # rest'"
   by (simp add: neq_wq' rest'_def taker_def)
 
@@ -1605,17 +1770,10 @@
 
 end
 
-locale valid_trace_p_h = valid_trace_p +
-  assumes we: "wq s cs = []"
-
-locale valid_trace_p_w = valid_trace_p +
-  assumes wne: "wq s cs \<noteq> []"
+
+context valid_trace_p_w
 begin
 
-definition "holder = hd (wq s cs)"
-definition "waiters = tl (wq s cs)"
-definition "waiters' = waiters @ [th]"
-
 lemma wq_s_cs: "wq s cs = holder#waiters"
     by (simp add: holder_def waiters_def wne)
     
@@ -2235,6 +2393,11 @@
       by (simp add: subtree_def the_preced_def)   
   qed
 
+
+lemma (in valid_trace) finite_threads:
+  shows "finite (threads s)"
+using vt by (induct) (auto elim: step.cases)
+
 lemma cp_le:
   assumes th_in: "th \<in> threads s"
   shows "cp s th \<le> Max (the_preced s ` threads s)"
@@ -3212,7 +3375,7 @@
 lemma not_waiting_th_s [simp]: "\<not> waiting s th cs'"
 proof
   assume "waiting s th cs'"
-  from this[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+  from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
   have "th \<in> set (wq s cs')" by auto
   from wq_threads[OF this] have "th \<in> threads s" .
   with th_not_live_s show False by simp
@@ -3221,7 +3384,7 @@
 lemma not_holding_th_s [simp]: "\<not> holding s th cs'"
 proof
   assume "holding s th cs'"
-  from this[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp]
+  from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
   have "th \<in> set (wq s cs')" by auto
   from wq_threads[OF this] have "th \<in> threads s" .
   with th_not_live_s show False by simp
@@ -3230,7 +3393,7 @@
 lemma not_waiting_th_es [simp]: "\<not> waiting (e#s) th cs'"
 proof
   assume "waiting (e # s) th cs'"
-  from this[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+  from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
   have "th \<in> set (wq s cs')" by auto
   from wq_threads[OF this] have "th \<in> threads s" .
   with th_not_live_s show False by simp
@@ -3239,7 +3402,7 @@
 lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'"
 proof
   assume "holding (e # s) th cs'"
-  from this[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp]
+  from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
   have "th \<in> set (wq s cs')" by auto
   from wq_threads[OF this] have "th \<in> threads s" .
   with th_not_live_s show False by simp
@@ -3274,13 +3437,13 @@
     assume h: "cs' \<in> ?L"
     hence "cs' \<in> ?R"
       by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_neq_simp, auto)
+             unfold wq_kept, auto)
   } moreover {
     fix cs'
     assume h: "cs' \<in> ?R"
     hence "cs' \<in> ?L"
       by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_neq_simp, auto)
+             unfold wq_kept, auto)
   } ultimately show ?thesis by auto
 qed
 
@@ -3300,7 +3463,7 @@
     have n_wait: "\<not> waiting (e#s) th' cs'" 
       using assms by (auto simp:readys_def)
     from wait[unfolded s_waiting_def, folded wq_def]
-         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
     have False by auto
   } thus ?thesis using assms
     by (unfold readys_def, auto)
@@ -3315,7 +3478,7 @@
     assume wait: "waiting (e#s) th' cs'"
     have n_wait: "\<not> waiting s th' cs'"
       using assms(2) by (auto simp:readys_def)
-    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
          n_wait[unfolded s_waiting_def, folded wq_def]
     have False by auto
   } with assms show ?thesis  
@@ -3388,7 +3551,7 @@
 lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'"
 proof
   assume "holding (e # s) th cs'"
-  from this[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp]
+  from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
   have "holding s th cs'" 
     by (unfold s_holding_def, fold wq_def, auto)
   with not_holding_th_s 
@@ -3421,13 +3584,13 @@
     assume h: "cs' \<in> ?L"
     hence "cs' \<in> ?R"
       by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_neq_simp, auto)
+             unfold wq_kept, auto)
   } moreover {
     fix cs'
     assume h: "cs' \<in> ?R"
     hence "cs' \<in> ?L"
       by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_neq_simp, auto)
+             unfold wq_kept, auto)
   } ultimately show ?thesis by auto
 qed
 
@@ -3447,7 +3610,7 @@
     have n_wait: "\<not> waiting (e#s) th' cs'" 
       using assms by (auto simp:readys_def)
     from wait[unfolded s_waiting_def, folded wq_def]
-         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
     have False by auto
   } thus ?thesis using assms
     by (unfold readys_def, auto)
@@ -3462,7 +3625,7 @@
     assume wait: "waiting (e#s) th' cs'"
     have n_wait: "\<not> waiting s th' cs'"
       using assms(2) by (auto simp:readys_def)
-    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
          n_wait[unfolded s_waiting_def, folded wq_def]
     have False by auto
   } with assms show ?thesis  
@@ -3526,13 +3689,13 @@
     assume h: "cs' \<in> ?L"
     hence "cs' \<in> ?R"
       by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_neq_simp, auto)
+             unfold wq_kept, auto)
   } moreover {
     fix cs'
     assume h: "cs' \<in> ?R"
     hence "cs' \<in> ?L"
       by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_neq_simp, auto)
+             unfold wq_kept, auto)
   } ultimately show ?thesis by auto
 qed
 
@@ -3554,7 +3717,7 @@
     have n_wait: "\<not> waiting (e#s) th' cs'" 
       using assms by (auto simp:readys_def)
     from wait[unfolded s_waiting_def, folded wq_def]
-         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
     have False by auto
   } moreover have "th' \<in> threads s" 
     using assms[unfolded readys_def] by auto
@@ -3570,7 +3733,7 @@
     assume wait: "waiting (e#s) th' cs'"
     have n_wait: "\<not> waiting s th' cs'"
       using assms by (auto simp:readys_def)
-    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
          n_wait[unfolded s_waiting_def, folded wq_def]
     have False by auto
   } with assms show ?thesis