diff -r 25fd656667a7 -r db196b066b97 PIPBasics.thy
--- a/PIPBasics.thy	Sat Jan 09 22:19:27 2016 +0800
+++ b/PIPBasics.thy	Tue Jan 12 08:35:36 2016 +0800
@@ -30,6 +30,13 @@
    "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)
+
 context valid_trace
 begin
 
@@ -60,39 +67,70 @@
 qed
 
 lemma wq_distinct: "distinct (wq s cs)"
-proof(rule ind, simp add:wq_def)
-  fix s e
-  assume h1: "step s e"
-  and h2: "distinct (wq s cs)"
-  thus "distinct (wq (e # s) cs)"
-  proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits)
-    fix thread s
-    assume h1: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+"
-      and h2: "thread \<in> set (wq_fun (schs s) cs)"
-      and h3: "thread \<in> runing s"
-    show "False" 
-    proof -
-      from h3 have "\<And> cs. thread \<in>  set (wq_fun (schs s) cs) \<Longrightarrow> 
-                             thread = hd ((wq_fun (schs s) cs))" 
-        by (simp add:runing_def readys_def s_waiting_def wq_def)
-      from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" .
-      with h2
-      have "(Cs cs, Th thread) \<in> (RAG s)"
-        by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def)
-      with h1 show False by auto
+proof(induct rule:ind)
+  case (Cons s e)
+  from Cons(4,3)
+  show ?case 
+  proof(induct)
+    case (thread_P th s cs1)
+    show ?case 
+    proof(cases "cs = cs1")
+      case True
+      thus ?thesis (is "distinct ?L")
+      proof - 
+        have "?L = wq_fun (schs s) cs1 @ [th]" using True
+          by (simp add:wq_def wf_def Let_def split:list.splits)
+        moreover have "distinct ..."
+        proof -
+          have "th \<notin> set (wq_fun (schs s) cs1)"
+          proof
+            assume otherwise: "th \<in> set (wq_fun (schs s) cs1)"
+            from runing_head[OF thread_P(1) this]
+            have "th = hd (wq_fun (schs s) cs1)" .
+            hence "(Cs cs1, Th th) \<in> (RAG s)" using otherwise
+              by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def)
+            with thread_P(2) show False by auto
+          qed
+          moreover have "distinct (wq_fun (schs s) cs1)"
+              using True thread_P wq_def by auto 
+          ultimately show ?thesis by auto
+        qed
+        ultimately show ?thesis by simp
+      qed
+    next
+      case False
+      with thread_P(3)
+      show ?thesis
+        by (auto simp:wq_def wf_def Let_def split:list.splits)
     qed
   next
-    fix thread s a list
-    assume dst: "distinct list"
-    show "distinct (SOME q. distinct q \<and> set q = set list)"
-    proof(rule someI2)
-      from dst show  "distinct list \<and> set list = set list" by auto
+    case (thread_V th s cs1)
+    thus ?case
+    proof(cases "cs = cs1")
+      case True
+      show ?thesis (is "distinct ?L")
+      proof(cases "(wq s cs)")
+        case Nil
+        thus ?thesis
+          by (auto simp:wq_def wf_def Let_def split:list.splits)
+      next
+        case (Cons w_hd w_tl)
+        moreover have "distinct (SOME q. distinct q \<and> set q = set w_tl)"
+        proof(rule someI2)
+          from thread_V(3)[unfolded Cons]
+          show  "distinct w_tl \<and> set w_tl = set w_tl" by auto
+        qed auto
+        ultimately show ?thesis
+          by (auto simp:wq_def wf_def Let_def True split:list.splits)
+      qed 
     next
-      fix q assume "distinct q \<and> set q = set list"
-      thus "distinct q" by auto
+      case False
+      with thread_V(3)
+      show ?thesis
+        by (auto simp:wq_def wf_def Let_def split:list.splits)
     qed
-  qed
-qed
+  qed (insert Cons, auto simp: wq_def Let_def split:list.splits)
+qed (unfold wq_def Let_def, simp)
 
 end
 
@@ -108,56 +146,34 @@
 *}
 
 lemma block_pre: 
-  assumes s_ni: "thread \<notin>  set (wq s cs)"
+  assumes s_ni: "thread \<notin> set (wq s cs)"
   and s_i: "thread \<in> set (wq (e#s) cs)"
   shows "e = P thread cs"
-proof -
-  show ?thesis
-  proof(cases e)
-    case (P th cs)
-    with assms
+proof(cases e)
+  -- {* This is the only non-trivial case: *}
+  case (V th cs1)
+  have False
+  proof(cases "cs1 = cs")
+    case True
     show ?thesis
-      by (auto simp:wq_def Let_def split:if_splits)
-  next
-    case (Create th prio)
-    with assms show ?thesis
-      by (auto simp:wq_def Let_def split:if_splits)
-  next
-    case (Exit th)
-    with assms show ?thesis
-      by (auto simp:wq_def Let_def split:if_splits)
-  next
-    case (Set th prio)
-    with assms show ?thesis
-      by (auto simp:wq_def Let_def split:if_splits)
-  next
-    case (V th cs)
-    with vt_e assms show ?thesis
-      apply (auto simp:wq_def Let_def split:if_splits)
-    proof -
-      fix q qs
-      assume h1: "thread \<notin> set (wq_fun (schs s) cs)"
-        and h2: "q # qs = wq_fun (schs s) cs"
-        and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
-        and vt: "vt (V th cs # s)"
-      from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp
-      moreover have "thread \<in> set qs"
+    proof(cases "(wq s cs1)")
+      case (Cons w_hd w_tl)
+      have "set (wq (e#s) cs) \<subseteq> set (wq s cs)"
       proof -
-        have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
+        have "(wq (e#s) cs) = (SOME q. distinct q \<and> set q = set w_tl)"
+          using  Cons V by (auto simp:wq_def Let_def True split:if_splits)
+        moreover have "set ... \<subseteq> set (wq s cs)"
         proof(rule someI2)
-          from wq_distinct [of cs]
-          and h2[symmetric, folded wq_def]
-          show "distinct qs \<and> set qs = set qs" by auto
-        next
-          fix x assume "distinct x \<and> set x = set qs"
-          thus "set x = set qs" by auto
-        qed
-        with h3 show ?thesis by simp
+          show "distinct w_tl \<and> set w_tl = set w_tl"
+            by (metis distinct.simps(2) local.Cons wq_distinct)
+        qed (insert Cons True, auto)
+        ultimately show ?thesis by simp
       qed
-      ultimately show "False" by auto
-      qed
-  qed
-qed
+      with assms show ?thesis by auto
+    qed (insert assms V True, auto simp:wq_def Let_def split:if_splits)
+  qed (insert assms V, auto simp:wq_def Let_def split:if_splits)
+  thus ?thesis by auto
+qed (insert assms, auto simp:wq_def Let_def split:if_splits)
 
 end
 
@@ -233,10 +249,10 @@
 
 end
 
+
 context valid_trace
 begin
-
-lemma vt_moment: "\<And> t. vt (moment t s)"
+lemma  vt_moment: "\<And> t. vt (moment t s)"
 proof(induct rule:ind)
   case Nil
   thus ?case by (simp add:vt_nil)
@@ -260,10 +276,17 @@
     ultimately show ?thesis by simp
   qed
 qed
+end
 
-(* Wrong:
-    lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
-*)
+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
+begin
+
 
 text {* (* ddd *)
   The nature of the work is like this: since it starts from a very simple and basic 
@@ -292,13 +315,13 @@
   @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} 
   and kept on blocked on them respectively ever since.
  
-  Without lose of generality, we assume @{text "t1"} is earlier than @{text "t2"}.
+  Without lost of generality, we assume @{text "t1"} is earlier than @{text "t2"}.
   However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still
   in blocked state at moment @{text "t2"} and could not
   make any request and get blocked the second time: Contradiction.
 *}
 
-lemma waiting_unique_pre:
+lemma waiting_unique_pre: (* ccc *)
   assumes h11: "thread \<in> set (wq s cs1)"
   and h12: "thread \<noteq> hd (wq s cs1)"
   assumes h21: "thread \<in> set (wq s cs2)"
@@ -519,7 +542,6 @@
 
 (* An aux lemma used later *)
 lemma unique_minus:
-  fixes x y z r
   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
   and xy: "(x, y) \<in> r"
   and xz: "(x, z) \<in> r^+"
@@ -547,7 +569,6 @@
 qed
 
 lemma unique_base:
-  fixes r x y z
   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
   and xy: "(x, y) \<in> r"
   and xz: "(x, z) \<in> r^+"
@@ -574,7 +595,6 @@
 qed
 
 lemma unique_chain:
-  fixes r x y z
   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
   and xy: "(x, y) \<in> r^+"
   and xz: "(x, z) \<in> r^+"
@@ -914,7 +934,6 @@
   with the happening of @{text "V"}-events:
 *}
 lemma step_RAG_v:
-fixes th::thread
 assumes vt:
   "vt (V th cs#s)"
 shows "
@@ -1342,7 +1361,6 @@
   by (auto intro:wq_threads)
 
 lemma readys_v_eq:
-  fixes th thread cs rest
   assumes neq_th: "th \<noteq> thread"
   and eq_wq: "wq s cs = thread#rest"
   and not_in: "th \<notin>  set rest"
@@ -1511,7 +1529,6 @@
              
 
 lemma step_holdents_p_add:
-  fixes th cs s
   assumes vt: "vt (P th cs#s)"
   and "wq s cs = []"
   shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"
@@ -1521,7 +1538,6 @@
 qed
 
 lemma step_holdents_p_eq:
-  fixes th cs s
   assumes vt: "vt (P th cs#s)"
   and "wq s cs \<noteq> []"
   shows "holdents (P th cs#s) th = holdents s th"
@@ -1551,7 +1567,6 @@
 qed
 
 lemma cntCS_v_dec: 
-  fixes s thread cs
   assumes vtv: "vt (V thread cs#s)"
   shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
 proof -