diff -r c820ac0f3088 -r c89013dca1aa Test.thy
--- a/Test.thy	Sat May 24 12:39:12 2014 +0100
+++ b/Test.thy	Fri May 30 07:56:39 2014 +0100
@@ -4,7 +4,7 @@
 
 type_synonym thread = nat -- {* Type for thread identifiers. *}
 type_synonym priority = nat  -- {* Type for priorities. *}
-type_synonym cs = nat -- {* Type for critical sections (or critical resources). *}
+type_synonym cs = nat -- {* Type for critical sections (or resources). *}
 
 datatype event = 
   Create thread priority 
@@ -98,8 +98,11 @@
 definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" 
   where "wq s = wq_fun (schs s)"
 
-definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
-  where "cp s \<equiv> cprec_fun (schs s)"
+definition cpreced2 :: "state \<Rightarrow> thread \<Rightarrow> precedence"
+  where "cpreced2 s \<equiv> cprec_fun (schs s)"
+
+abbreviation
+  "cpreceds2 s ths \<equiv> {cpreced2 s th | th. th \<in> ths}"
 
 definition
   "holds2 s \<equiv> holds (wq_fun (schs s))"
@@ -113,24 +116,33 @@
 definition
   "dependants2 s \<equiv> dependants (wq_fun (schs s))"
 
+(* ready -> is a thread that is not waiting for any resource *) 
 definition readys :: "state \<Rightarrow> thread set"
   where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waits2 s th cs)}"
 
 definition runing :: "state \<Rightarrow> thread set"
-  where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
+  where "runing s \<equiv> {th . th \<in> readys s \<and> cpreced2 s th = Max (cpreceds2 s (readys s))}"
 
+(* all resources a thread hols in a state *)
 definition holding :: "state \<Rightarrow> thread \<Rightarrow> cs set"
   where "holding s th \<equiv> {cs . holds2 s th cs}"
 
 abbreviation
   "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)"
 
+lemma exists_distinct:
+  obtains ys where "distinct ys" "set ys = set xs"
+by (metis List.finite_set finite_distinct_list)
+
+lemma next_to_run_set [simp]:
+  "wts \<noteq> [] \<Longrightarrow> next_to_run wts \<in> set wts"
+apply(rule exists_distinct[of wts])
+by (metis (mono_tags, lifting) hd_in_set set_empty some_eq_ex)
+
 lemma holding_RAG: 
   "holding s th = {cs . (Cs cs, Th th) \<in> RAG2 s}"
-unfolding holding_def
-unfolding holds2_def
-unfolding RAG2_def RAG_def
-unfolding holds_def waits_def
+unfolding holding_def RAG2_def RAG_def
+unfolding holds2_def holds_def waits_def
 by auto
 
 inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"
@@ -141,6 +153,7 @@
 | step_V: "\<lbrakk>th \<in> runing s;  holds2 s th cs\<rbrakk> \<Longrightarrow> step s (V th cs)" 
 | step_Set: "\<lbrakk>th \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set th prio)"
 
+(* valid states *)
 inductive vt :: "state \<Rightarrow> bool"
   where
   vt_nil[intro]: "vt []" 
@@ -160,9 +173,10 @@
   assumes "step s e" "distinct (wq s cs)" 
   shows "distinct (wq (e # s) cs)"
 using assms
+unfolding wq_def
 apply(induct)
-apply(auto simp add: wq_def Let_def)
-apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def)[1]
+apply(auto simp add: RAG2_def RAG_def Let_def)[1]
+apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def)
 apply(auto split: list.split)
 apply(rule someI2)
 apply(auto)
@@ -225,7 +239,7 @@
 lemma RAG_v2:
 assumes vt:"vt s" "wq s cs = th # wts \<and> wts \<noteq> []"
 shows "RAG2 (V th cs # s) \<subseteq>
-  RAG2 s - {(Cs cs, Th th)} - {(Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}"
+  RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}"
 unfolding RAG2_def RAG_def waits_def holds_def
 using assms wq_distinct[OF vt(1), of"cs"]
 by (auto simp add: Let_def wq_def)
@@ -235,7 +249,22 @@
   and "waits2 s th cs1"
   and "waits2 s th cs2"
   shows "cs1 = cs2"
-sorry
+using assms
+apply(induct)
+apply(simp add: waits2_def waits_def)
+apply(erule step.cases)
+apply(auto simp add: Let_def waits2_def waits_def holds_def RAG2_def RAG_def 
+ readys_def runing_def split: if_splits)
+apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list)
+apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list)
+apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct)
+by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct)
+
+
+lemma rtrancl_eq_trancl [simp]:
+  assumes "x \<noteq> y"
+  shows "(x, y) \<in> r\<^sup>* \<longleftrightarrow> (x, y) \<in> r\<^sup>+"
+using assms by (metis rtrancl_eq_or_trancl) 
 
 lemma acyclic_RAG_step: 
   assumes vt: "vt s"
@@ -247,39 +276,35 @@
   case (step_P th s cs)
   have ac: "acyclic (RAG2 s)" by fact
   have ds: "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" by fact
-  { assume a: "wq s cs = []" -- "case waiting queue is empty"
-    have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>*"  
-    proof
-      assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>*"
-      then have "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
+  { assume wq_empty: "wq s cs = []" -- "case waiting queue is empty"
+    then have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>+"
+    proof (rule_tac notI)
+      assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+"
       then obtain x where "(x, Cs cs) \<in> RAG2 s" using tranclD2 by metis 
-      with a show False by (auto simp: RAG2_def RAG_def wq_def waits_def)
+      with wq_empty show False by (auto simp: RAG2_def RAG_def wq_def waits_def)
     qed
-    with acyclic_insert ac
-    have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp
-    then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a] 
+    with ac have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp
+    then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF wq_empty] 
       by (rule acyclic_subset)
   }
   moreover
-  { assume a: "wq s cs \<noteq> []" -- "case waiting queue is not empty"
-    from ds have "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>*" by (metis node.distinct(1) rtranclD)
-    with acyclic_insert ac 
-    have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by auto
-    then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds a] 
+  { assume wq_not_empty: "wq s cs \<noteq> []" -- "case waiting queue is not empty"
+    from ac ds
+    have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by simp
+    then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds wq_not_empty] 
       by (rule acyclic_subset)
   }
   ultimately show "acyclic (RAG2 (P th cs # s))" by metis
 next    
-  case (step_V th s cs) 
+  case (step_V th s cs) -- "case for release of a lock" 
   have vt: "vt s" by fact
   have ac: "acyclic (RAG2 s)" by fact
-  have rn: "th \<in> runing s" by fact
   have hd: "holds2 s th cs" by fact
-  from hd have th_in: "th \<in> set (wq s cs)" and
-               eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto
-  then obtain wts where
-    eq_wq: "wq s cs = th # wts" by (cases "wq s cs") (auto)
-  { assume "wts = []" -- "case no thread present to take over"
+  from vt have wq_distinct:"distinct (wq s cs)" by (rule wq_distinct)
+  from hd have "th \<in> set (wq s cs)" "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto
+  then obtain wts where eq_wq: "wq s cs = th # wts"  by (cases "wq s cs") (auto)
+  -- "case no thread present in the waiting queue to take over"
+  { assume "wts = []" 
     with eq_wq have "wq s cs = [th]" by simp
     then have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" by (rule RAG_v1)
     moreover have "acyclic (RAG2 s - {(Cs cs, Th th)})" using ac by (auto intro: acyclic_subset)
@@ -287,39 +312,39 @@
     have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
   }
   moreover
+  -- "at least one thread present to take over"
   { def nth \<equiv> "next_to_run wts"
-    assume aa: "wts \<noteq> []" -- "at least one thread present to take over"
-    with vt eq_wq 
-    have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)} \<union> {(Cs cs, Th nth)}" 
-      unfolding nth_def by (rule_tac RAG_v2) (auto)
+    assume wq_not_empty: "wts \<noteq> []" 
+    have waits2_cs: "waits2 s nth cs" 
+      using eq_wq wq_not_empty wq_distinct
+      unfolding nth_def waits2_def waits_def wq_def[symmetric] by auto
+    have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)}" 
+      unfolding nth_def using  vt wq_not_empty eq_wq by (rule_tac RAG_v2) (auto)
     moreover 
-    have "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))" 
+    have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)})" 
     proof -
-      have "acyclic (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})" using ac by (auto intro: acyclic_subset)
+      have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})" using ac by (auto intro: acyclic_subset)
       moreover 
-      have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>+" 
-        proof 
-          assume "(Th nth, Cs cs) \<in> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>+"
-          then obtain z where a: "(Th nth, z) \<in> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})"
-            by (metis converse_tranclE)
-          then have "(Th nth, z) \<in> RAG2 s" by simp
-          then obtain cs' where b: "z = Cs cs'" "(Th nth, Cs cs') \<in> RAG2 s"
-            unfolding RAG2_def RAG_def by auto
-          then have "cs = cs'" 
-            apply(rule_tac waiting_unique[OF vt])
-            using eq_wq aa
-            apply(auto simp add: nth_def RAG2_def RAG_def waits2_def waits_def wq_def)
-            apply (metis (mono_tags, lifting) `\<And>thesis. (\<And>wts. wq s cs = th # wts \<Longrightarrow> thesis) \<Longrightarrow> thesis` distinct.simps(2) hd_in_set list.inject set_empty2 tfl_some vt wq_def wq_distinct)
-            by (metis (mono_tags, lifting) `\<And>thesis. (\<And>wts. wq s cs = th # wts \<Longrightarrow> thesis) \<Longrightarrow> thesis` distinct.simps(2) hd_in_set list.sel(1) set_empty2 tfl_some vt wq_def wq_distinct)            
-         then show "False" using a b by simp
-        qed
-      then have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>*"
-        by (metis node.distinct(1) rtranclD)
+      have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+" 
+      proof (rule notI)
+        assume "(Th nth, Cs cs) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+"
+        then obtain z where a: "(Th nth, z) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})"
+          by (metis converse_tranclE)
+        then have "(Th nth, z) \<in> RAG2 s" by simp
+        then obtain cs' where b: "z = Cs cs'" "(Th nth, Cs cs') \<in> RAG2 s"
+          unfolding RAG2_def RAG_def by auto
+        moreover 
+        have "waits2 s nth cs'" 
+          using b(2) unfolding RAG2_def RAG_def waits2_def by simp
+        ultimately have "cs = cs'" 
+          by (rule_tac waiting_unique[OF vt waits2_cs])
+        then show "False" using a b(1) by simp
+      qed
       ultimately 
-      show "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))" 
-        by (simp add: acyclic_insert)
+      show "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth) })" by simp
     qed
-    ultimately have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
+    ultimately have "acyclic (RAG2 (V th cs # s))" 
+      by (rule_tac acyclic_subset)
   }
   ultimately show "acyclic (RAG2 (V th cs # s))" by metis
 qed (simp_all)