# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1400854772 -3600
# Node ID af38526275f8daf81911b7a94aa3273ad09df5bb
# Parent  92f61f6a0fe795596c04d1b24243b83c36323951
added a test theory for polishing teh proofs

diff -r 92f61f6a0fe7 -r af38526275f8 PrioG.thy
--- a/PrioG.thy	Thu May 22 17:40:39 2014 +0100
+++ b/PrioG.thy	Fri May 23 15:19:32 2014 +0100
@@ -800,9 +800,11 @@
   apply(fold wq_def)
   apply(drule_tac step_back_step)
   apply(ind_cases " step s (P (hd (wq s cs)) cs)")
-  apply(auto simp:s_RAG_def wq_def cs_holding_def)
+  apply(simp add:s_RAG_def wq_def cs_holding_def)
+  apply(auto)
   done
 
+(* FIXME: Unused
 lemma simple_A:
   fixes A
   assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"
@@ -814,6 +816,7 @@
   with h have "A = {a}" by auto
   thus ?thesis by 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)
@@ -822,126 +825,125 @@
   fixes s
   assumes vt: "vt s"
   shows "acyclic (RAG s)"
-proof -
-  from vt show ?thesis
-  proof(induct)
-    case (vt_cons s e)
-    assume ih: "acyclic (RAG s)"
-      and stp: "step s e"
-      and vt: "vt s"
-    show ?case
-    proof(cases e)
-      case (Create th prio)
-      with ih
-      show ?thesis by (simp add:RAG_create_unchanged)
-    next
-      case (Exit th)
-      with ih show ?thesis by (simp add:RAG_exit_unchanged)
-    next
-      case (V th cs)
-      from V vt stp have vtt: "vt (V th cs#s)" by auto
-      from step_RAG_v [OF this]
-      have eq_de: 
-        "RAG (e # s) = 
-            RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
-            {(Cs cs, Th th') |th'. next_th s th cs th'}"
-        (is "?L = (?A - ?B - ?C) \<union> ?D") by (simp add:V)
-      from ih have ac: "acyclic (?A - ?B - ?C)" by (auto elim:acyclic_subset)
-      from step_back_step [OF vtt]
-      have "step s (V th cs)" .
-      thus ?thesis
-      proof(cases)
-        assume "holding s th cs"
-        hence th_in: "th \<in> set (wq s cs)" and
-          eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto
-        then obtain rest where
-          eq_wq: "wq s cs = th#rest"
-          by (cases "wq s cs", auto)
-        show ?thesis
-        proof(cases "rest = []")
-          case False
-          let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
-          from eq_wq False have eq_D: "?D = {(Cs cs, Th ?th')}"
-            by (unfold next_th_def, auto)
-          let ?E = "(?A - ?B - ?C)"
-          have "(Th ?th', Cs cs) \<notin> ?E\<^sup>*"
-          proof
-            assume "(Th ?th', Cs cs) \<in> ?E\<^sup>*"
-            hence " (Th ?th', Cs cs) \<in> ?E\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
-            from tranclD [OF this]
-            obtain x where th'_e: "(Th ?th', x) \<in> ?E" by blast
-            hence th_d: "(Th ?th', x) \<in> ?A" by simp
-            from RAG_target_th [OF this]
-            obtain cs' where eq_x: "x = Cs cs'" by auto
-            with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp
-            hence wt_th': "waiting s ?th' cs'"
-              unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp
-            hence "cs' = cs"
-            proof(rule waiting_unique [OF vt])
-              from eq_wq wq_distinct[OF vt, of cs]
-              show "waiting s ?th' cs" 
-                apply (unfold s_waiting_def wq_def, auto)
-              proof -
-                assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
+using assms
+proof(induct)
+  case (vt_cons s e)
+  assume ih: "acyclic (RAG s)"
+    and stp: "step s e"
+    and vt: "vt s"
+  show ?case
+  proof(cases e)
+    case (Create th prio)
+    with ih
+    show ?thesis by (simp add:RAG_create_unchanged)
+  next
+    case (Exit th)
+    with ih show ?thesis by (simp add:RAG_exit_unchanged)
+  next
+    case (V th cs)
+    from V vt stp have vtt: "vt (V th cs#s)" by auto
+    from step_RAG_v [OF this]
+    have eq_de: 
+      "RAG (e # s) = 
+      RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
+      {(Cs cs, Th th') |th'. next_th s th cs th'}"
+      (is "?L = (?A - ?B - ?C) \<union> ?D") by (simp add:V)
+    from ih have ac: "acyclic (?A - ?B - ?C)" by (auto elim:acyclic_subset)
+    from step_back_step [OF vtt]
+    have "step s (V th cs)" .
+    thus ?thesis
+    proof(cases)
+      assume "holding s th cs"
+      hence th_in: "th \<in> set (wq s cs)" and
+        eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto
+      then obtain rest where
+        eq_wq: "wq s cs = th#rest"
+        by (cases "wq s cs", auto)
+      show ?thesis
+      proof(cases "rest = []")
+        case False
+        let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
+        from eq_wq False have eq_D: "?D = {(Cs cs, Th ?th')}"
+          by (unfold next_th_def, auto)
+        let ?E = "(?A - ?B - ?C)"
+        have "(Th ?th', Cs cs) \<notin> ?E\<^sup>*"
+        proof
+          assume "(Th ?th', Cs cs) \<in> ?E\<^sup>*"
+          hence " (Th ?th', Cs cs) \<in> ?E\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
+          from tranclD [OF this]
+          obtain x where th'_e: "(Th ?th', x) \<in> ?E" by blast
+          hence th_d: "(Th ?th', x) \<in> ?A" by simp
+          from RAG_target_th [OF this]
+          obtain cs' where eq_x: "x = Cs cs'" by auto
+          with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp
+          hence wt_th': "waiting s ?th' cs'"
+            unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp
+          hence "cs' = cs"
+          proof(rule waiting_unique [OF vt])
+            from eq_wq wq_distinct[OF vt, of cs]
+            show "waiting s ?th' cs" 
+              apply (unfold s_waiting_def wq_def, auto)
+            proof -
+              assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
                 and eq_wq: "wq_fun (schs s) cs = th # rest"
-                have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
-                proof(rule someI2)
-                  from wq_distinct[OF vt, of cs] and eq_wq
-                  show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
-                next
-                  fix x assume "distinct x \<and> set x = set rest"
-                  with False show "x \<noteq> []" by auto
-                qed
-                hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
-                                  set (SOME q. distinct q \<and> set q = set rest)" by auto
-                moreover have "\<dots> = set rest" 
-                proof(rule someI2)
-                  from wq_distinct[OF vt, of cs] and eq_wq
-                  show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
-                next
-                  show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
-                qed
-                moreover note hd_in
-                ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
+              have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+              proof(rule someI2)
+                from wq_distinct[OF vt, of cs] and eq_wq
+                show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
               next
-                assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
+                fix x assume "distinct x \<and> set x = set rest"
+                with False show "x \<noteq> []" by auto
+              qed
+              hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
+                set (SOME q. distinct q \<and> set q = set rest)" by auto
+              moreover have "\<dots> = set rest" 
+              proof(rule someI2)
+                from wq_distinct[OF vt, of cs] and eq_wq
+                show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
+              next
+                show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
+              qed
+              moreover note hd_in
+              ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
+            next
+              assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
                 and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
-                have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
-                proof(rule someI2)
-                  from wq_distinct[OF vt, of cs] and eq_wq
-                  show "distinct rest \<and> set rest = set rest" by auto
-                next
-                  fix x assume "distinct x \<and> set x = set rest"
-                  with False show "x \<noteq> []" by auto
-                qed
-                hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
-                                  set (SOME q. distinct q \<and> set q = set rest)" by auto
-                moreover have "\<dots> = set rest" 
-                proof(rule someI2)
-                  from wq_distinct[OF vt, of cs] and eq_wq
-                  show "distinct rest \<and> set rest = set rest" by auto
-                next
-                  show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
-                qed
-                moreover note hd_in
-                ultimately show False by auto
+              have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+              proof(rule someI2)
+                from wq_distinct[OF vt, of cs] and eq_wq
+                show "distinct rest \<and> set rest = set rest" by auto
+              next
+                fix x assume "distinct x \<and> set x = set rest"
+                with False show "x \<noteq> []" by auto
+              qed
+              hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
+                set (SOME q. distinct q \<and> set q = set rest)" by auto
+              moreover have "\<dots> = set rest" 
+              proof(rule someI2)
+                from wq_distinct[OF vt, of cs] and eq_wq
+                show "distinct rest \<and> set rest = set rest" by auto
+              next
+                show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
               qed
+              moreover note hd_in
+              ultimately show False by auto
             qed
-            with th'_e eq_x have "(Th ?th', Cs cs) \<in> ?E" by simp
-            with False
-            show "False" by (auto simp: next_th_def eq_wq)
           qed
-          with acyclic_insert[symmetric] and ac
-            and eq_de eq_D show ?thesis by auto
-        next
-          case True
-          with eq_wq
-          have eq_D: "?D = {}"
-            by (unfold next_th_def, auto)
-          with eq_de ac
-          show ?thesis by auto
-        qed 
-      qed
+          with th'_e eq_x have "(Th ?th', Cs cs) \<in> ?E" by simp
+          with False
+          show "False" by (auto simp: next_th_def eq_wq)
+        qed
+        with acyclic_insert[symmetric] and ac
+          and eq_de eq_D show ?thesis by auto
+      next
+        case True
+        with eq_wq
+        have eq_D: "?D = {}"
+          by (unfold next_th_def, auto)
+        with eq_de ac
+        show ?thesis by auto
+      qed 
+    qed
   next
     case (P th cs)
     from P vt stp have vtt: "vt (P th cs#s)" by auto
@@ -970,14 +972,14 @@
       proof
         assume "(Cs cs, Th th) \<in> (RAG s)\<^sup>*"
         hence "(Cs cs, Th th) \<in> (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
-          moreover from step_back_step [OF vtt] have "step s (P th cs)" .
-          ultimately show False
-          proof -
-            show " \<lbrakk>(Cs cs, Th th) \<in> (RAG s)\<^sup>+; step s (P th cs)\<rbrakk> \<Longrightarrow> False"
-              by (ind_cases "step s (P th cs)", simp)
-          qed
+        moreover from step_back_step [OF vtt] have "step s (P th cs)" .
+        ultimately show False
+        proof -
+          show " \<lbrakk>(Cs cs, Th th) \<in> (RAG s)\<^sup>+; step s (P th cs)\<rbrakk> \<Longrightarrow> False"
+            by (ind_cases "step s (P th cs)", simp)
         qed
-        with acyclic_insert ih eq_r show ?thesis by auto
+      qed
+      with acyclic_insert ih eq_r show ?thesis by auto
       qed
       ultimately show ?thesis by simp
     next
@@ -990,8 +992,8 @@
     case vt_nil
     show "acyclic (RAG ([]::state))"
       by (auto simp: s_RAG_def cs_waiting_def 
-                      cs_holding_def wq_def acyclic_def)
-  qed
+        cs_holding_def wq_def acyclic_def)
+qed
 qed
 
 lemma finite_RAG: 
diff -r 92f61f6a0fe7 -r af38526275f8 Test.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Test.thy	Fri May 23 15:19:32 2014 +0100
@@ -0,0 +1,370 @@
+theory Test 
+imports Precedence_ord
+begin
+
+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). *}
+
+datatype event = 
+  Create thread priority 
+| Exit thread 
+| P thread cs 
+| V thread cs 
+| Set thread priority 
+
+type_synonym state = "event list"
+
+fun threads :: "state \<Rightarrow> thread set"
+  where 
+  "threads [] = {}" 
+| "threads (Create th prio#s) = {th} \<union> threads s" 
+| "threads (Exit th # s) = (threads s) - {th}" 
+| "threads (_#s) = threads s" 
+
+fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
+  where
+  "priority th [] = 0" 
+| "priority th (Create th' prio#s) = (if th' = th then prio else priority th s)" 
+| "priority th (Set th' prio#s) = (if th' = th then prio else priority th s)" 
+| "priority th (_#s) = priority th s"
+
+fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"
+  where
+  "last_set th [] = 0" 
+| "last_set th ((Create th' prio)#s) = (if (th = th') then length s else last_set th s)" 
+| "last_set th ((Set th' prio)#s) = (if (th = th') then length s else last_set th s)" 
+| "last_set th (_#s) = last_set th s"
+
+definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
+  where "preced th s \<equiv> Prc (priority th s) (last_set th s)"
+
+definition
+  "holds wq th cs \<equiv> th \<in> set (wq cs) \<and> th = hd (wq cs)"
+
+definition
+  "waits wq th cs \<equiv> th \<in> set (wq cs) \<and> th \<noteq> hd (wq cs)"
+
+datatype node = 
+  Th "thread" 
+| Cs "cs" 
+
+definition
+  "RAG wq \<equiv> {(Th th, Cs cs) | th cs. waits wq th cs} \<union> {(Cs cs, Th th) | cs th. holds wq th cs}"
+
+definition
+  "dependants wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
+
+record schedule_state = 
+  wq_fun :: "cs \<Rightarrow> thread list" 
+  cprec_fun :: "thread \<Rightarrow> precedence" 
+
+definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
+  where 
+  "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"
+
+abbreviation
+  "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
+
+abbreviation 
+  "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"
+ 
+abbreviation
+  "release qs \<equiv> case qs of
+             [] => [] 
+          |  (_#qs) => (SOME q. distinct q \<and> set q = set qs)"
+
+fun schs :: "state \<Rightarrow> schedule_state"
+  where 
+  "schs [] = (| wq_fun = \<lambda> cs. [],  cprec_fun = (\<lambda>_. Prc 0 0) |)" 
+| "schs (Create th prio # s) = 
+       (let wq = wq_fun (schs s) in
+          (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"
+|  "schs (Exit th # s) = 
+       (let wq = wq_fun (schs s) in
+          (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"
+|  "schs (Set th prio # s) = 
+       (let wq = wq_fun (schs s) in
+          (|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))"
+|  "schs (P th cs # s) = 
+       (let wq = wq_fun (schs s) in
+        let new_wq = wq(cs := (wq cs @ [th])) in
+          (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))"
+|  "schs (V th cs # s) = 
+       (let wq = wq_fun (schs s) in
+        let new_wq = wq(cs := release (wq cs)) in
+          (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"
+
+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
+  "holds2 s \<equiv> holds (wq_fun (schs s))"
+
+definition
+  "waits2 s \<equiv> waits (wq_fun (schs s))"
+
+definition
+  "RAG2 s \<equiv> RAG (wq_fun (schs s))"
+  
+definition
+  "dependants2 s \<equiv> dependants (wq_fun (schs s))"
+
+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))}"
+
+definition holding :: "state \<Rightarrow> thread \<Rightarrow> cs set"
+  where "holding s th \<equiv> {cs . holds2 s th cs}"
+
+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
+by auto
+
+inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"
+  where
+  step_Create: "\<lbrakk>th \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create th prio)" 
+| step_Exit: "\<lbrakk>th \<in> runing s; holding s th = {}\<rbrakk> \<Longrightarrow> step s (Exit th)" 
+| step_P: "\<lbrakk>th \<in> runing s;  (Cs cs, Th th)  \<notin> (RAG2 s)^+\<rbrakk> \<Longrightarrow> step s (P th cs)" 
+| 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)"
+
+inductive vt :: "state \<Rightarrow> bool"
+  where
+  vt_nil[intro]: "vt []" 
+| vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"
+
+lemma runing_ready: 
+  shows "runing s \<subseteq> readys s"
+  unfolding runing_def readys_def
+  by auto 
+
+lemma readys_threads:
+  shows "readys s \<subseteq> threads s"
+  unfolding readys_def
+  by auto
+
+lemma wq_distinct_step: 
+  assumes "step s e" "distinct (wq s cs)" 
+  shows "distinct (wq (e # s) cs)"
+using assms
+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 split: list.split)
+apply(rule someI2)
+apply(auto)
+done
+
+lemma wq_distinct: 
+  assumes "vt s" 
+  shows "distinct (wq s cs)"
+using assms
+apply(induct)
+apply(simp add: wq_def)
+apply(simp add: wq_distinct_step)
+done
+
+lemma RAG_set_unchanged[simp]: 
+  shows "RAG2 (Set th prio # s) = RAG2 s"
+unfolding RAG2_def
+by (simp add: Let_def)
+
+lemma RAG_create_unchanged[simp]: 
+  "RAG2 (Create th prio # s) = RAG2 s"
+unfolding RAG2_def
+by (simp add: Let_def)
+
+lemma RAG_exit_unchanged[simp]: 
+  shows "RAG2 (Exit th # s) = RAG2 s"
+unfolding RAG2_def
+by (simp add: Let_def)
+
+lemma RAG_p1:
+  assumes "wq s cs = []"
+  shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Cs cs, Th th)}"
+  using assms
+  apply(auto simp add: RAG2_def RAG_def wq_def Let_def waits_def holds_def)
+  apply (metis in_set_insert insert_Nil list.distinct(1))
+  done
+
+lemma RAG_p2:
+  assumes "vt (P th cs#s)" "wq s cs \<noteq> []"
+  shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Th th, Cs cs)}"
+  using assms
+  apply(simp add: RAG2_def Let_def)
+  apply(erule_tac vt.cases)
+  apply(simp)
+  apply(clarify)
+  apply(simp)
+  apply(erule_tac step.cases)
+  apply(simp_all)
+  apply(simp add: wq_def RAG_def RAG2_def)
+  apply(simp add: waits_def holds_def)
+  apply(auto)
+  done
+
+definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"
+  where "next_th s th cs t = 
+    (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> t = hd (SOME q. distinct q \<and> set q = set rest))"
+
+lemma RAG_v:
+assumes vt:"vt (V th cs#s)"
+shows "
+  RAG2 (V th cs # s) =
+  RAG2 s - {(Cs cs, Th th)} -
+  {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
+  {(Cs cs, Th th') |th'.  next_th s th cs th'}"
+  apply (insert vt, unfold RAG2_def RAG_def)
+  sorry
+
+lemma waiting_unique:
+  assumes "vt s"
+  and "waits2 s th cs1"
+  and "waits2 s th cs2"
+  shows "cs1 = cs2"
+sorry
+
+lemma singleton_Un:
+  shows "A \<union> {x} = insert x A"
+by simp
+
+
+lemma acyclic_RAG_step: 
+  assumes vt: "vt s"
+  and     stp: "step s e"
+  and     ac: "acyclic (RAG2 s)"
+  shows "acyclic (RAG2 (e # s))"
+using stp vt ac
+proof (induct)
+  case (step_P th s cs)
+  have vt: "vt s" by fact
+  have ac: "acyclic (RAG2 s)" by fact
+  have rn: "th \<in> runing s" by fact
+  have ds: "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" by fact
+  have vtt: "vt (P th cs#s)" using vt rn ds by (metis step.step_P vt_cons)
+  { 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)
+      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)
+    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] by simp
+  }
+  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 vtt a] by simp
+  }
+  ultimately show "acyclic (RAG2 (P th cs # s))" by metis
+next    
+  case (step_V th s cs) 
+  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 rest where
+    eq_wq: "wq s cs = th # rest" by (cases "wq s cs") (auto)
+  show ?case
+    apply(subst RAG_v)
+    apply(rule vt_cons)
+    apply(rule vt)
+    apply(rule step.step_V)
+    apply(rule rn)
+    apply(rule hd)
+    using eq_wq
+    apply(cases "rest = []")
+    apply(subgoal_tac "{(Cs cs, Th th') |th'. next_th s th cs th'} = {}")
+    apply(simp)
+    apply(rule acyclic_subset)
+    apply(rule ac)
+    apply(auto)[1]
+    apply(auto simp add: next_th_def)[1]
+    -- "case wq more than a singleton"
+    apply(subgoal_tac "{(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest)))} = 
+      {(Cs cs, Th th') |th'. next_th s th cs th'}")
+    apply(rotate_tac 2)
+    apply(drule sym)
+    apply(simp only: singleton_Un)
+    apply(simp only: acyclic_insert)
+    apply(rule conjI)
+    apply(rule acyclic_subset)
+    apply(rule ac)
+    apply(auto)[1]
+    apply(rotate_tac 2)
+    apply(thin_tac "?X")
+    defer 
+    apply(simp add: next_th_def)
+    apply(clarify)
+    apply(simp add: rtrancl_eq_or_trancl)
+    apply(drule tranclD)
+    apply(erule exE)
+    apply(drule conjunct1)
+    apply(subgoal_tac "(Th (hd (SOME q. distinct q \<and> set q = set rest)), z) \<in> RAG2 s")
+    prefer 2
+    apply(simp)
+    apply(case_tac z)
+    apply(simp add: RAG2_def RAG_def)
+    apply(clarify)
+    apply(simp)
+    apply(simp add: next_th_def)
+    apply(rule waiting_unique)
+    apply(rule vt)
+    apply(simp add: RAG2_def RAG_def waits2_def waits_def wq_def)
+    apply(rotate_tac 2)
+    apply(thin_tac "?X")
+    apply(subgoal_tac "distinct (wq s cs)")
+    prefer 2
+    apply(rule wq_distinct)
+    apply(rule vt)
+    apply (unfold waits2_def waits_def wq_def, auto)
+    apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []")
+    prefer 2
+    apply (metis (mono_tags) set_empty tfl_some)
+    apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
+                set (SOME q. distinct q \<and> set q = set rest)") 
+    prefer 2
+    apply(auto)[1]
+    apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest") 
+    prefer 2
+    apply(rule someI2)
+    apply(auto)[2]
+    apply(auto)[1]
+    apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []")
+    prefer 2
+    apply (metis (mono_tags) set_empty tfl_some)
+    apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
+                set (SOME q. distinct q \<and> set q = set rest)") 
+    prefer 2
+    apply(auto)[1]
+    apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest") 
+    prefer 2
+    apply(rule someI2)
+    apply(auto)[2]
+    apply(auto)[1]
+    done
+qed (simp_all)
+
+
+
+
+
+