
diff -r af38526275f8 -r c820ac0f3088 Test.thy
--- a/Test.thy	Fri May 23 15:19:32 2014 +0100
+++ b/Test.thy	Sat May 24 12:39:12 2014 +0100
@@ -72,7 +72,7 @@
 abbreviation
   "release qs \<equiv> case qs of
              [] => [] 
-          |  (_#qs) => (SOME q. distinct q \<and> set q = set qs)"
+          |  (_ # qs) => SOME q. distinct q \<and> set q = set qs"
 
 fun schs :: "state \<Rightarrow> schedule_state"
   where 
@@ -122,6 +122,9 @@
 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 holding_RAG: 
   "holding s th = {cs . (Cs cs, Th th) \<in> RAG2 s}"
 unfolding holding_def
@@ -191,41 +194,41 @@
 
 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
+  shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Cs cs, Th th)}"
+using assms
+unfolding  RAG2_def RAG_def wq_def Let_def waits_def holds_def
+by (auto simp add: Let_def)
+
 
 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
+  assumes "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" "wq s cs \<noteq> []"
+  shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Th th, Cs cs)}"
+using assms
+unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def
+by (auto simp add: Let_def)
+
+lemma [simp]: "(SOME q. distinct q \<and> q = []) = []"
+by auto
+
+lemma [simp]: "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)"
+apply auto
+apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
+by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
 
-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_v1:
+assumes vt: "wq s cs = [th]"
+shows "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}"
+using assms
+unfolding RAG2_def RAG_def waits_def holds_def wq_def
+by (auto simp add: Let_def)
 
-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 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))}"
+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)
 
 lemma waiting_unique:
   assumes "vt s"
@@ -234,11 +237,6 @@
   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"
@@ -247,11 +245,8 @@
 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
@@ -262,14 +257,16 @@
     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
+    then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a] 
+      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 vtt a] by simp
+    then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds a] 
+      by (rule acyclic_subset)
   }
   ultimately show "acyclic (RAG2 (P th cs # s))" by metis
 next    
@@ -278,89 +275,53 @@
   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
+  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"
+    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)
+    ultimately 
+    have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
+  }
+  moreover
+  { 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)
+    moreover 
+    have "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))" 
+    proof -
+      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)
+      ultimately 
+      show "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))" 
+        by (simp add: acyclic_insert)
+    qed
+    ultimately have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
+  }
+  ultimately show "acyclic (RAG2 (V th cs # s))" by metis
 qed (simp_all)
 
 




