diff -r 30ed212f268a -r b769f43deb30 PIPBasics.thy
--- a/PIPBasics.thy	Thu Feb 04 00:43:05 2016 +0000
+++ b/PIPBasics.thy	Thu Feb 04 14:45:30 2016 +0800
@@ -4,6 +4,12 @@
 
 section {* Generic aulxiliary lemmas *}
 
+lemma rel_eqI:
+  assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"
+  and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"
+  shows "A = B"
+  using assms by auto
+
 lemma f_image_eq:
   assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"
   shows "f ` A = g ` A"
@@ -86,14 +92,10 @@
   finally show ?thesis by simp
 qed
 
-lemma rel_eqI:
-  assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"
-  and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"
-  shows "A = B"
-  using assms by auto
-
 section {* Lemmas do not depend on trace validity *}
 
+text {* The following lemma serves to proof @{text "preced_tm_lt"} *}
+
 lemma birth_time_lt:  
   assumes "s \<noteq> []"
   shows "last_set th s < length s"
@@ -112,16 +114,18 @@
   qed
 qed simp
 
+text {* The following lemma also serves to proof @{text "preced_tm_lt"} *}
 lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
   by (induct s, auto)
 
+text {* The following lemma is used in Correctness.thy *}
 lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
   by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt)
 
-lemma eq_RAG: 
-  "RAG (wq s) = RAG s"
-  by (unfold cs_RAG_def s_RAG_def, auto)
-
+text {*
+  The follow lemma says if a resource is waited for, it must be held
+  by someone else.
+*}
 lemma waiting_holding:
   assumes "waiting (s::state) th cs"
   obtains th' where "holding s th' cs"
@@ -134,7 +138,22 @@
   from that[OF this] show ?thesis .
 qed
 
-lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
+text {* 
+  The following four lemmas relate the @{term wq}
+  and non-@{term wq} versions of @{term waiting}, @{term holding},
+  @{term dependants} and @{term cp}.
+*}
+
+lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
+  by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
+
+lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
+  by (unfold s_holding_def wq_def cs_holding_def, simp)
+
+lemma eq_dependants: "dependants (wq s) = dependants s"
+  by (simp add: s_dependants_abv wq_def)
+
+lemma cp_eq: "cp s th = cpreced (wq s) s th"
 unfolding cp_def wq_def
 apply(induct s rule: schs.induct)
 apply(simp add: Let_def cpreced_initial)
@@ -147,6 +166,13 @@
 apply(simp add: Let_def)
 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))})"
@@ -159,22 +185,25 @@
     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 cpreced_def, fold the_preced_def, simp)
+  thus ?thesis by (unfold cp_eq cpreced_def, fold the_preced_def, simp)
 qed
 
-lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
-  by (unfold s_RAG_def, auto)
-
-lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
-  by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
-
-lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
-  by (unfold s_holding_def wq_def cs_holding_def, simp)
-
+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.
+*}
 lemma children_RAG_alt_def:
   "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"
   by (unfold s_RAG_def, auto simp:children_def holding_eq)
 
+text {*
+  The following two lemmas relate @{term holdents} and @{term cntCS}
+  to @{term children} in @{term RAG}, so that proofs about
+  @{term holdents} and @{term cntCS} can be carried out under 
+  the support of the abstract theory of {\em relational graph}
+  (and specifically {\em relational tree} and {\em relational forest}).
+*}
 lemma holdents_alt_def:
   "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))"
   by (unfold children_RAG_alt_def holdents_def, simp add: image_image)
@@ -184,6 +213,11 @@
   apply (unfold children_RAG_alt_def cntCS_def holdents_def)
   by (rule card_image[symmetric], auto simp:inj_on_def)
 
+text {*
+  The following two lemmas show the inclusion relations
+  among three key sets, namely @{term runing}, @{term readys}
+  and @{term threads}.
+*}
 lemma runing_ready: 
   shows "runing s \<subseteq> readys s"
   unfolding runing_def readys_def
@@ -194,17 +228,12 @@
   unfolding readys_def
   by auto
 
-lemma wq_v_neq [simp]:
-   "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
-  by (auto simp:wq_def Let_def cp_def split:list.splits)
-
-lemma runing_head:
-  assumes "th \<in> runing s"
-  and "th \<in> set (wq_fun (schs s) cs)"
-  shows "th = hd (wq_fun (schs s) cs)"
-  using assms
-  by (simp add:runing_def readys_def s_waiting_def wq_def)
-
+text {*
+  The following lemma says that if a thread is running, 
+  it must be the head of every waiting queue it is in. 
+  In other words, a running thread must have got every 
+  resource it has requested.
+*}
 lemma runing_wqE:
   assumes "th \<in> runing s"
   and "th \<in> set (wq s cs)"
@@ -225,17 +254,6 @@
   with eq_wq that show ?thesis by metis
 qed
 
-lemma isP_E:
-  assumes "isP e"
-  obtains cs where "e = P (actor e) cs"
-  using assms by (cases e, auto)
-
-lemma isV_E:
-  assumes "isV e"
-  obtains cs where "e = V (actor e) cs"
-  using assms by (cases e, auto) 
-
-
 text {*
   Every thread can only be blocked on one critical resource, 
   symmetrically, every critical resource can only be held by one thread. 
@@ -247,6 +265,12 @@
   shows "th1 = th2"
  by (insert assms, unfold s_holding_def, auto)
 
+text {*
+  The following three lemmas establishes the uniqueness of
+  precedence, a key property about precedence.
+  The first two are just technical lemmas to assist the proof
+  of the third.
+*}
 lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
   apply (induct s, auto)
   by (case_tac a, auto split:if_splits)
@@ -267,7 +291,12 @@
   from last_set_unique [OF this th_in1 th_in2]
   show ?thesis .
 qed
-                      
+
+text {*
+  The following lemma shows that there exits a linear order
+  on precedences, which is crucial for the notion of 
+  @{term Max} to be applicable.
+*}
 lemma preced_linorder: 
   assumes neq_12: "th1 \<noteq> th2"
   and th_in1: "th1 \<in> threads s"
@@ -279,6 +308,10 @@
   thus ?thesis by auto
 qed
 
+text {*
+  The following lemma case analysis the situations when
+  two nodes are in @{term RAG}.
+*}
 lemma in_RAG_E:
   assumes "(n1, n2) \<in> RAG (s::state)"
   obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
@@ -286,6 +319,13 @@
   using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
   by auto
 
+text {*
+  The following lemmas are the simplification rules 
+  for @{term count}, @{term cntP}, @{term cntV}.
+  It is a major technical in this development to use 
+  the counter of @{term "P"} and @{term "V"} (* ccc *)
+*}
+
 lemma count_rec1 [simp]: 
   assumes "Q e"
   shows "count Q (e#es) = Suc (count Q es)"
@@ -354,30 +394,6 @@
         insert assms V, auto simp:cntV_def)
 qed (insert assms, auto simp:cntV_def)
 
-lemma eq_dependants: "dependants (wq s) = dependants s"
-  by (simp add: s_dependants_abv wq_def)
-
-lemma inj_the_preced: 
-  "inj_on (the_preced s) (threads s)"
-  by (metis inj_onI preced_unique the_preced_def)
-
-lemma holding_next_thI:
-  assumes "holding s th cs"
-  and "length (wq s cs) > 1"
-  obtains th' where "next_th s th cs th'"
-proof -
-  from assms(1)[folded holding_eq, unfolded cs_holding_def]
-  have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" 
-    by (unfold s_holding_def, fold wq_def, auto)
-  then obtain rest where h1: "wq s cs = th#rest" 
-    by (cases "wq s cs", auto)
-  with assms(2) have h2: "rest \<noteq> []" by auto
-  let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
-  have "next_th s th cs ?th'" using  h1(1) h2 
-    by (unfold next_th_def, auto)
-  from that[OF this] show ?thesis .
-qed
-
 (* ccc *)
 
 section {* Locales used to investigate the execution of PIP *}
@@ -675,6 +691,13 @@
 
 section {* Distinctiveness of waiting queues *}
 
+lemma (in valid_trace) finite_threads:
+  shows "finite (threads s)"
+  using vt by (induct) (auto elim: step.cases)
+
+lemma (in valid_trace) finite_readys [simp]: "finite (readys s)"
+  using finite_threads readys_threads rev_finite_subset by blast
+
 context valid_trace_create
 begin
 
@@ -811,13 +834,6 @@
 context valid_trace
 begin
 
-lemma  finite_threads:
-  shows "finite (threads s)"
-  using vt by (induct) (auto elim: step.cases)
-
-lemma finite_readys [simp]: "finite (readys s)"
-  using finite_threads readys_threads rev_finite_subset by blast
-
 lemma wq_distinct: "distinct (wq s cs)"
 proof(induct rule:ind)
   case (Cons s e)
@@ -1033,7 +1049,7 @@
   shows "th \<in> threads s"
 proof -
   from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
-  moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto
+  moreover then obtain cs where "n = Cs cs" by (unfold s_RAG_def, auto)
   ultimately have "(Th th, Cs cs) \<in> RAG s" by simp
   hence "th \<in> set (wq s cs)"
     by (unfold s_RAG_def, auto simp:cs_waiting_def)
@@ -1123,7 +1139,7 @@
   next
     case False
     have "wq (e#s) c = wq s c" using False
-        by (unfold is_v, simp)
+        by simp
     hence "waiting s t c" using assms 
         by (simp add: cs_waiting_def waiting_eq)
     hence "t \<notin> readys s" by (unfold readys_def, auto)
@@ -1138,7 +1154,7 @@
   shows "waiting (e#s) t c" 
 proof -
   have "wq (e#s) c = wq s c" 
-    using assms(2) is_v by auto
+    using assms(2) by auto
   with assms(1) show ?thesis 
     using cs_waiting_def waiting_eq by auto 
 qed
@@ -1148,7 +1164,7 @@
   and "holding s t c"
   shows "holding (e#s) t c"
 proof -
-  from assms(1) have "wq (e#s) c = wq s c" using is_v by auto
+  from assms(1) have "wq (e#s) c = wq s c"  by auto
   from assms(2)[unfolded s_holding_def, folded wq_def, 
                 folded this, unfolded wq_def, folded s_holding_def]
   show ?thesis .
@@ -1243,7 +1259,7 @@
      |    "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'"
 proof(cases "c = cs")
   case False
-  hence "wq (e#s) c = wq s c" using is_v by auto
+  hence "wq (e#s) c = wq s c" by auto
   with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto 
   from that(1)[OF False this] show ?thesis .
 next
@@ -1277,7 +1293,7 @@
   from that(1)[OF True this] show ?thesis .
 next
   case False
-  hence "wq (e#s) c = wq s c" using is_v by auto
+  hence "wq (e#s) c = wq s c" by auto
   from assms[unfolded s_holding_def, folded wq_def, 
              unfolded this, unfolded wq_def, folded s_holding_def]
   have "holding s t c"  .
@@ -1328,7 +1344,15 @@
   show ?thesis by auto
 qed
 
-lemma no_waiting:
+lemma no_waiter_before: "\<not> waiting s t cs"
+proof
+  assume otherwise: "waiting s t cs"
+  from this[unfolded s_waiting_def, folded wq_def, 
+            unfolded wq_s_cs rest_nil]
+  show False by simp
+qed
+
+lemma no_waiter_after:
   assumes "waiting (e#s) t cs"
   shows False
 proof -
@@ -1353,12 +1377,12 @@
   obtains "c \<noteq> cs" "waiting s t c"
 proof(cases "c = cs")
   case False
-  hence "wq (e#s) c = wq s c" using is_v by auto
+  hence "wq (e#s) c = wq s c"  by auto
   with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto 
   from that(1)[OF False this] show ?thesis .
 next
   case True
-  from no_waiting[OF assms[unfolded True]]
+  from no_waiter_after[OF assms[unfolded True]]
   show ?thesis by auto
 qed
 
@@ -1371,7 +1395,7 @@
   show ?thesis by auto
 next
   case False
-  hence "wq (e#s) c = wq s c" using is_v by auto
+  hence "wq (e#s) c = wq s c" by auto
   from assms[unfolded s_holding_def, folded wq_def, 
              unfolded this, unfolded wq_def, folded s_holding_def]
   have "holding s t c"  .
@@ -2689,6 +2713,10 @@
   finally show ?thesis .
 qed
 
+lemma eq_RAG: 
+  "RAG (wq s) = RAG s"
+  by (unfold cs_RAG_def s_RAG_def, auto)
+
 lemma dependants_alt_def:
   "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"
   by (metis eq_RAG s_dependants_def tRAG_trancl_eq)
@@ -4659,4 +4687,4 @@
 
 end
 
-end
\ No newline at end of file
+end