
diff -r 81c6ede5cd11 -r 74fc1eae4605 PIPBasics.thy
--- a/PIPBasics.thy	Tue Feb 09 22:30:43 2016 +0800
+++ b/PIPBasics.thy	Fri Feb 12 12:32:57 2016 +0800
@@ -167,28 +167,6 @@
 done
 
 text {*
-  The following lemmas is an alternative definition of @{term cp},
-  which is based on the notion of subtrees in @{term RAG} and 
-  is handy to use once the abstract theory of {\em relational graph}
-  (and specifically {\em relational tree} and {\em relational forest})
-  are in place.
-*}
-lemma cp_alt_def:
-  "cp s th =  
-           Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
-proof -
-  have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
-        Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" 
-          (is "Max (_ ` ?L) = Max (_ ` ?R)")
-  proof -
-    have "?L = ?R" 
-    by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
-    thus ?thesis by simp
-  qed
-  thus ?thesis by (unfold cp_eq cpreced_def, fold the_preced_def, simp)
-qed
-
-text {*
   The following @{text "children_RAG_alt_def"} relates
   @{term children} in @{term RAG} to the notion of @{term holding}.
   It is a technical lemmas used to prove the two following lemmas.
@@ -593,6 +571,40 @@
                   {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
    by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)
 
+text {*
+  The following lemmas is an alternative definition of @{term cp},
+  which is based on the notion of subtrees in @{term RAG} and 
+  is handy to use once the abstract theory of {\em relational graph}
+  (and specifically {\em relational tree} and {\em relational forest})
+  are in place.
+*}
+lemma cp_alt_def:
+  "cp s th =  
+           Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
+proof -
+  have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
+        Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" 
+          (is "Max (_ ` ?L) = Max (_ ` ?R)")
+  proof -
+    have "?L = ?R" 
+    by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
+    thus ?thesis by simp
+  qed
+  thus ?thesis by (unfold cp_eq cpreced_def, fold the_preced_def, simp)
+qed
+
+text {*
+  The following is another definition of @{term cp}.
+*}
+lemma cp_alt_def1: 
+  "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
+proof -
+  have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
+       ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
+       by auto
+  thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
+qed
+
 lemma RAG_tRAG_transfer:
   assumes  "RAG s' = RAG s \<union> {(Th th, Cs cs)}"
   and "(Cs cs, Th th'') \<in> RAG s"
@@ -931,6 +943,19 @@
     ultimately show ?thesis by simp
   qed
 qed
+
+text {*
+  The following two lemmas are fundamental, because they assure
+  that the numbers of both living and ready threads are finite.
+*}
+
+lemma finite_threads:
+  shows "finite (threads s)"
+  using vt by (induct) (auto elim: step.cases)
+
+lemma  finite_readys: "finite (readys s)"
+  using finite_threads readys_threads rev_finite_subset by blast
+
 end
 
 text {*
@@ -965,7 +990,7 @@
 section {* Waiting queues are distinct *}
 
 text {*
-  This section proofs that every waiting queue in the system
+  This section proves that every waiting queue in the system
   is distinct, given in lemma @{text wq_distinct}.
 
   The proof is split into the locales for events (or operations),
@@ -1478,19 +1503,29 @@
 
 end
 
-section {* The change of @{term RAG} *}
+section {* The formation of @{term RAG} *}
 
 text {*
   The whole of PIP resides on the understanding of the formation
-  of @{term RAG}. In this section, we are going to investigate how
-  @{term RAG} is changed with the execution of every event (or operation).
-  The effect of every event on @{text RAG} is derived in its respective
+  of @{term RAG}. We are going to show that @{term RAG}
+  forms a finite branching forest. The formalization is divided 
+  into a series of subsections.
+*}
+
+subsection {* The change of @{term RAG} with each step of execution *}
+
+text {*
+  The very essence to prove that @{term RAG} has a certain property is to 
+  show that this property is preserved as an invariant by the execution 
+  of the system, and the basis for such kind of invariant proofs is to 
+  show how @{term RAG} is changed with the execution of every execution step
+  (or event, or system operation). In this subsection,
+  the effect of every event on @{text RAG} is derived in its respective
   locale named @{text "RAG_es"} with all lemmas before auxiliary. 
 
-  The derivation of these @{text "RAG_es"}s forms the very basis 
-  to show the well-formedness of @{term RAG}, 
+  These derived @{text "RAG_es"}s constitute the foundation 
+  to show the various well-formed properties of @{term RAG},  
   for example, @{term RAG} is finite, acyclic, and single-valued, etc.
-
 *}
 
 text {*
@@ -2270,7 +2305,7 @@
 
 end
 
-section {* RAG is finite *}
+subsection {* RAG is finite *}
 
 context valid_trace_v
 begin
@@ -2338,8 +2373,6 @@
 qed
 end
 
-section {* RAG is acyclic *}
-
 subsection {* Uniqueness of waiting *}
 
 text {*
@@ -2721,6 +2754,9 @@
 
 end
 
+
+subsection {* RAG is acyclic *}
+
 context valid_trace
 begin
 
@@ -2793,7 +2829,7 @@
 
 end
 
-section {* RAG is single-valued *}
+subsection {* RAG is single-valued *}
 
 text {*
   The proof that @{term RAG} is single-valued makes use of 
@@ -2813,7 +2849,7 @@
 
 end
 
-section {* RAG is well-founded *}
+subsection {* RAG is well-founded *}
 
 text {*
   In this section, it is proved that both @{term RAG} and 
@@ -2844,7 +2880,7 @@
 
 end
 
-section {* RAG forms a finite-branching forest (or tree) *}
+subsection {* RAG forms a finite-branching forest (or tree) *}
 
 text {*
   With all the well-formedness proofs about @{term RAG} in place, 
@@ -2876,8 +2912,7 @@
   qed
 qed
 
-
-section {* Derived properties for sub-graphs of RAG *}
+subsection {* Derived properties for sub-graphs of RAG *}
 
 context valid_trace
 begin
@@ -2952,16 +2987,20 @@
 section {* Chain to readys *}
 
 text {*
-  In this section, a more complete view of @{term RAG} and @{term threads}
-  are given. 
+  In this section, based on the just derived
+  properties about the shape of @{term RAG}, 
+  a more complete view of the relationship 
+  between threads is established.
 *}
 
 context valid_trace
 begin
 
 text {*
-  The first lemma is technical, which says out of any node in the domain 
-  of @{term RAG}, there is a path leading to a ready thread.
+  The first lemma is technical, which says out of any node 
+  in the domain of @{term RAG},
+  (no matter whether it is thread node or resource node)  
+  there is a path leading to a ready thread.
 *}
 
 lemma chain_building:
@@ -3276,18 +3315,26 @@
 
 end
 
-(* ccc *)
 section {* Relating @{term cp} and @{term the_preced} and @{term preced} *}
 
+text {*
+ @{term cp} of a thread is defined to be the maximum of 
+ the @{term preced}-values (precedences) of all threads in 
+ its subtree given by @{term RAG}. Therefore, there exits 
+ a relationship between @{term cp} and @{term preced} (and 
+ also its variation @{term "the_preced"}) to be explored, 
+ and this is the target of this section.
+*}
+
 context valid_trace
 begin
 
-lemma finite_threads:
-  shows "finite (threads s)"
-  using vt by (induct) (auto elim: step.cases)
-
-lemma  finite_readys: "finite (readys s)"
-  using finite_threads readys_threads rev_finite_subset by blast
+text {*
+  Since @{term cp} is the maximum of all @{term preced}s in its subtree, 
+  which includes itself, it is not difficult to show
+  that the one thread's precedence is less or equal to its
+  @{text cp}-value:
+*}
 
 lemma le_cp:
   shows "preced th s \<le> cp s th"
@@ -3299,6 +3346,13 @@
       by (simp add: subtree_def the_preced_def)   
   qed
 
+text {*
+  Since @{term cp} is the maximum precedence of its subtree,
+  and the subtree is only a subset of the set of all threads,
+  it can be shown that @{text cp} is less or equal to the maximum of
+  all threads:
+*}
+
 lemma cp_le:
   assumes th_in: "th \<in> threads s"
   shows "cp s th \<le> Max (the_preced s ` threads s)"
@@ -3314,6 +3368,21 @@
         node.inject(1) rtranclD subsetI subtree_def trancl_domain) 
 qed
 
+text {*
+  Since the @{term cp}-value of each individual thread is less or equal to the 
+  maximum precedence value of all threads (shown in lemma @{thm cp_le}),
+  it is easy to derive further that maximum @{term "cp"}-value of
+  all threads is also less or equal to the latter.
+
+  On the other hand, since the precedence value of each individual 
+  thread is less of equal to its own @{term cp}-value (shown in lemma @{thm le_cp}),
+  it is easy to show that the maximum of the former is less or equal to the 
+  maximum of the latter. 
+
+  By combining these two perspectives, we get the following equality 
+  between the two maximums:
+*}
+
 lemma max_cp_eq: 
   shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"
   (is "?L = ?R")
@@ -3334,17 +3403,21 @@
 qed
 
 text {* (* ddd *) \noindent
-  Since the current precedence of the threads in ready queue will always be boosted,
-  there must be one inside it has the maximum precedence of the whole system. 
+  According to @{thm threads_alt_def} and @{thm readys_subtree_disjoint} , 
+  the set of @{term threads} can be partitioned into subtrees of the 
+  threads in @{term readys}, and also because  @{term cp}-value of a thread is 
+  the maximum precedence of its own subtree, by applying 
+  the absorbing property of @{term Max} (lemma @{thm Max_UNION}) 
+  over the union of subtrees, the following equation can be derived:
 *}
-lemma max_cp_readys_threads:
-  shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R")
+
+lemma max_cp_readys_max_preced:
+  shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R")
 proof(cases "readys s = {}")
   case False
-  have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp)
-  also have "... = 
-    Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))" 
-         by (unfold threads_alt_def, simp)
+  have "?R = 
+    Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
+    by (simp add: threads_alt_def)  
   also have "... = 
     Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
           by (unfold image_UN, simp)
@@ -3355,9 +3428,10 @@
                     {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M"
                         using finite_subtree_threads by auto
   qed (auto simp:False subtree_def finite_readys)
-  also have "... =  
-    Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` readys s)" 
-      by (unfold image_comp, simp)
+  also have "... = 
+     Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` 
+                        readys s)" 
+      by (simp add: image_comp)
   also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
   proof -
     have "(?f ` ?A) = (?g ` ?A)"
@@ -3372,10 +3446,36 @@
   finally show ?thesis by simp
 qed (auto simp:threads_alt_def)
 
+text {*
+  The following lemma is simply a corollary of @{thm max_cp_readys_max_preced}
+  and @{thm max_cp_eq}:
+*}
+lemma max_cp_readys_threads:
+  shows "Max (cp s ` readys s) = Max (cp s ` threads s)" 
+    using max_cp_readys_max_preced max_cp_eq by auto
+
 end
 
+
 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *}
 
+text {*
+  As explained in the section where @{term "cntP"},
+  @{term "cntV"} and @{term "cntCS"} are defined, 
+  we need to establish a equation (in lemma @{text "cnp_cnv_cncs"}) 
+  so that the last can be calculated out of the first two. 
+
+  While the calculation of @{term "cntV"} and @{term "cntCS"}
+  are relatively simple, the calculation of @{term "cntCS"} and 
+  @{term "pvD"} are complicated, because their definitions
+  involve a number of other functions such as @{term holdents}, @{term readys}, 
+  and @{term threads}. To prove  @{text "cnp_cnv_cncs"}, 
+  we need to investigate how the values of these functions
+  are changed with the execution of each kind of system operation.
+  Following conventions, such investigation are divided into 
+  locales corresponding to system operations.
+*}
+
 context valid_trace_p_w
 begin
 
@@ -4633,6 +4733,10 @@
 context valid_trace
 begin
 
+text {*
+  The following two lemmas are purely technical, which says
+  a non-living thread can not hold any resource.
+*}
 lemma not_thread_holdents:
   assumes not_in: "th \<notin> threads s" 
   shows "holdents s th = {}"
@@ -4654,6 +4758,14 @@
   using not_thread_holdents[OF assms]
   by (simp add:cntCS_def)
 
+text {*
+  Starting from the following @{text cnp_cnv_eq}, all 
+  lemmas in this section concern the meaning of 
+  condition @{prop "cntP s th = cntV s th"}, i.e.
+  when the numbers of resource requesting and resource releasing
+  are equal.
+*}
+
 lemma cnp_cnv_eq:
   assumes "th \<notin> threads s"
   shows "cntP s th = cntV s th"
@@ -4699,6 +4811,11 @@
     show False by simp
 qed
 
+lemma count_eq_RAG_plus_Th:
+  assumes "cntP s th = cntV s th"
+  shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
+  using count_eq_RAG_plus[OF assms] by auto
+
 lemma eq_pv_dependants:
   assumes eq_pv: "cntP s th = cntV s th"
   shows "dependants s th = {}"
@@ -4712,11 +4829,6 @@
   shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
   using assms eq_pv_dependants dependants_alt_def eq_dependants by auto 
 
-lemma count_eq_RAG_plus_Th:
-  assumes "cntP s th = cntV s th"
-  shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
-  using count_eq_RAG_plus[OF assms] by auto
-
 lemma count_eq_tRAG_plus_Th:
   assumes "cntP s th = cntV s th"
   shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
@@ -4724,9 +4836,17 @@
 
 end
 
+subsection {* A notion @{text detached} and its relation with @{term cntP} 
+  and @{term cntV} *}
+
 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
   where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"
 
+text {*
+  The following lemma shows that a thread is detached means 
+  it is isolated from @{term RAG}:
+*}
+
 lemma detached_test:
   shows "detached s th = (Th th \<notin> Field (RAG s))"
 apply(simp add: detached_def Field_def)
@@ -4799,114 +4919,6 @@
 
 end
 
-section {* Recursive definition of @{term "cp"} *}
-
-lemma cp_alt_def1: 
-  "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
-proof -
-  have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
-       ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
-       by auto
-  thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
-qed
-
-lemma cp_gen_def_cond: 
-  assumes "x = Th th"
-  shows "cp s th = cp_gen s (Th th)"
-by (unfold cp_alt_def1 cp_gen_def, simp)
-
-lemma cp_gen_over_set:
-  assumes "\<forall> x \<in> A. \<exists> th. x = Th th"
-  shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"
-proof(rule f_image_eq)
-  fix a
-  assume "a \<in> A"
-  from assms[rule_format, OF this]
-  obtain th where eq_a: "a = Th th" by auto
-  show "cp_gen s a = (cp s \<circ> the_thread) a"
-    by  (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
-qed
-
-
-context valid_trace
-begin
-(* ddd *)
-lemma cp_gen_rec:
-  assumes "x = Th th"
-  shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)"
-proof(cases "children (tRAG s) x = {}")
-  case True
-  show ?thesis
-    by (unfold True cp_gen_def subtree_children, simp add:assms)
-next
-  case False
-  hence [simp]: "children (tRAG s) x \<noteq> {}" by auto
-  note fsbttRAGs.finite_subtree[simp]
-  have [simp]: "finite (children (tRAG s) x)"
-     by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], 
-            rule children_subtree)
-  { fix r x
-    have "subtree r x \<noteq> {}" by (auto simp:subtree_def)
-  } note this[simp]
-  have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}"
-  proof -
-    from False obtain q where "q \<in> children (tRAG s) x" by blast
-    moreover have "subtree (tRAG s) q \<noteq> {}" by simp
-    ultimately show ?thesis by blast
-  qed
-  have h: "Max ((the_preced s \<circ> the_thread) `
-                ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) =
-        Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)"
-                     (is "?L = ?R")
-  proof -
-    let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L
-    let "Max (_ \<union> (?h ` ?B))" = ?R
-    let ?L1 = "?f ` \<Union>(?g ` ?B)"
-    have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)"
-    proof -
-      have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp
-      also have "... =  (\<Union> x \<in> ?B. ?f ` (?g x))" by auto
-      finally have "Max ?L1 = Max ..." by simp
-      also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)"
-        by (subst Max_UNION, simp+)
-      also have "... = Max (cp_gen s ` children (tRAG s) x)"
-          by (unfold image_comp cp_gen_alt_def, simp)
-      finally show ?thesis .
-    qed
-    show ?thesis
-    proof -
-      have "?L = Max (?f ` ?A \<union> ?L1)" by simp
-      also have "... = max (the_preced s (the_thread x)) (Max ?L1)"
-            by (subst Max_Un, simp+)
-      also have "... = max (?f x) (Max (?h ` ?B))"
-        by (unfold eq_Max_L1, simp)
-      also have "... =?R"
-        by (rule max_Max_eq, (simp)+, unfold assms, simp)
-      finally show ?thesis .
-    qed
-  qed  thus ?thesis 
-          by (fold h subtree_children, unfold cp_gen_def, simp) 
-qed
-
-lemma cp_rec:
-  "cp s th = Max ({the_preced s th} \<union> 
-                     (cp s o the_thread) ` children (tRAG s) (Th th))"
-proof -
-  have "Th th = Th th" by simp
-  note h =  cp_gen_def_cond[OF this] cp_gen_rec[OF this]
-  show ?thesis 
-  proof -
-    have "cp_gen s ` children (tRAG s) (Th th) = 
-                (cp s \<circ> the_thread) ` children (tRAG s) (Th th)"
-    proof(rule cp_gen_over_set)
-      show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th"
-        by (unfold tRAG_alt_def, auto simp:children_def)
-    qed
-    thus ?thesis by (subst (1) h(1), unfold h(2), simp)
-  qed
-qed
-end
-
 section {* Other properties useful in Implementation.thy or Correctness.thy *}
 
 context valid_trace_e 




