diff -r c7db2ccba18a -r 3a801bbd2687 PIPBasics.thy
--- a/PIPBasics.thy	Wed Feb 03 12:04:03 2016 +0800
+++ b/PIPBasics.thy	Wed Feb 03 21:05:15 2016 +0800
@@ -2590,6 +2590,64 @@
                   {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
    by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)
 
+context valid_trace
+begin
+
+lemma RAG_tRAG_transfer:
+  assumes  "RAG s' = RAG s \<union> {(Th th, Cs cs)}"
+  and "(Cs cs, Th th'') \<in> RAG s"
+  shows "tRAG s' = tRAG s \<union> {(Th th, Th th'')}" (is "?L = ?R")
+proof -
+  { fix n1 n2
+    assume "(n1, n2) \<in> ?L"
+    from this[unfolded tRAG_alt_def]
+    obtain th1 th2 cs' where 
+      h: "n1 = Th th1" "n2 = Th th2" 
+         "(Th th1, Cs cs') \<in> RAG s'"
+         "(Cs cs', Th th2) \<in> RAG s'" by auto
+    from h(4) and assms(1) have cs_in: "(Cs cs', Th th2) \<in> RAG s" by auto
+    from h(3) and assms(1) 
+    have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> 
+          (Th th1, Cs cs') \<in> RAG s" by auto
+    hence "(n1, n2) \<in> ?R"
+    proof
+      assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)"
+      hence eq_th1: "th1 = th" by simp
+      moreover have "th2 = th''"
+      proof -
+        from h1 have "cs' = cs" by simp
+        from assms(2) cs_in[unfolded this]
+        show ?thesis using unique_RAG by auto 
+      qed
+      ultimately show ?thesis using h(1,2) by auto
+    next
+      assume "(Th th1, Cs cs') \<in> RAG s"
+      with cs_in have "(Th th1, Th th2) \<in> tRAG s"
+        by (unfold tRAG_alt_def, auto)
+      from this[folded h(1, 2)] show ?thesis by auto
+    qed
+  } moreover {
+    fix n1 n2
+    assume "(n1, n2) \<in> ?R"
+    hence "(n1, n2) \<in>tRAG s \<or> (n1, n2) = (Th th, Th th'')" by auto
+    hence "(n1, n2) \<in> ?L" 
+    proof
+      assume "(n1, n2) \<in> tRAG s"
+      moreover have "... \<subseteq> ?L"
+      proof(rule tRAG_mono)
+        show "RAG s \<subseteq> RAG s'" by (unfold assms(1), auto)
+      qed
+      ultimately show ?thesis by auto
+    next
+      assume eq_n: "(n1, n2) = (Th th, Th th'')"
+      from assms(1, 2) have "(Cs cs, Th th'') \<in> RAG s'" by auto
+      moreover have "(Th th, Cs cs) \<in> RAG s'" using assms(1) by auto
+      ultimately show ?thesis 
+        by (unfold eq_n tRAG_alt_def, auto)
+    qed
+  } ultimately show ?thesis by auto
+qed
+
 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)
@@ -2598,6 +2656,8 @@
   "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}"
   using dependants_alt_def tRAG_trancl_eq by auto
 
+end
+
 section {* Chain to readys *}
 
 context valid_trace
@@ -4206,173 +4266,9 @@
 
 end
 
-section {* hhh *}
-
-lemma RAG_tRAG_transfer:
-  assumes "vt s'"
-  assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
-  and "(Cs cs, Th th'') \<in> RAG s'"
-  shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R")
-proof -
-  interpret vt_s': valid_trace "s'" using assms(1)
-    by (unfold_locales, simp)
-  { fix n1 n2
-    assume "(n1, n2) \<in> ?L"
-    from this[unfolded tRAG_alt_def]
-    obtain th1 th2 cs' where 
-      h: "n1 = Th th1" "n2 = Th th2" 
-         "(Th th1, Cs cs') \<in> RAG s"
-         "(Cs cs', Th th2) \<in> RAG s" by auto
-    from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \<in> RAG s'" by auto
-    from h(3) and assms(2) 
-    have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> 
-          (Th th1, Cs cs') \<in> RAG s'" by auto
-    hence "(n1, n2) \<in> ?R"
-    proof
-      assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)"
-      hence eq_th1: "th1 = th" by simp
-      moreover have "th2 = th''"
-      proof -
-        from h1 have "cs' = cs" by simp
-        from assms(3) cs_in[unfolded this]
-        show ?thesis using vt_s'.unique_RAG by auto 
-      qed
-      ultimately show ?thesis using h(1,2) by auto
-    next
-      assume "(Th th1, Cs cs') \<in> RAG s'"
-      with cs_in have "(Th th1, Th th2) \<in> tRAG s'"
-        by (unfold tRAG_alt_def, auto)
-      from this[folded h(1, 2)] show ?thesis by auto
-    qed
-  } moreover {
-    fix n1 n2
-    assume "(n1, n2) \<in> ?R"
-    hence "(n1, n2) \<in>tRAG s' \<or> (n1, n2) = (Th th, Th th'')" by auto
-    hence "(n1, n2) \<in> ?L" 
-    proof
-      assume "(n1, n2) \<in> tRAG s'"
-      moreover have "... \<subseteq> ?L"
-      proof(rule tRAG_mono)
-        show "RAG s' \<subseteq> RAG s" by (unfold assms(2), auto)
-      qed
-      ultimately show ?thesis by auto
-    next
-      assume eq_n: "(n1, n2) = (Th th, Th th'')"
-      from assms(2, 3) have "(Cs cs, Th th'') \<in> RAG s" by auto
-      moreover have "(Th th, Cs cs) \<in> RAG s" using assms(2) by auto
-      ultimately show ?thesis 
-        by (unfold eq_n tRAG_alt_def, auto)
-    qed
-  } ultimately show ?thesis by auto
-qed
-
-context valid_trace
-begin
-
-lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]
-
-end
-
-lemma cp_alt_def1: 
-  "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
-proof -
-  have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
-       ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
-       by auto
-  thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
-qed
-
-lemma cp_gen_def_cond: 
-  assumes "x = Th th"
-  shows "cp s th = cp_gen s (Th th)"
-by (unfold cp_alt_def1 cp_gen_def, simp)
-
-lemma cp_gen_over_set:
-  assumes "\<forall> x \<in> A. \<exists> th. x = Th th"
-  shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"
-proof(rule f_image_eq)
-  fix a
-  assume "a \<in> A"
-  from assms[rule_format, OF this]
-  obtain th where eq_a: "a = Th th" by auto
-  show "cp_gen s a = (cp s \<circ> the_thread) a"
-    by  (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
-qed
-
-context valid_trace
-begin
-
-lemma subtree_tRAG_thread:
-  assumes "th \<in> threads s"
-  shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")
-proof -
-  have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
-    by (unfold tRAG_subtree_eq, simp)
-  also have "... \<subseteq> ?R"
-  proof
-    fix x
-    assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
-    then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto
-    from this(2)
-    show "x \<in> ?R"
-    proof(cases rule:subtreeE)
-      case 1
-      thus ?thesis by (simp add: assms h(1)) 
-    next
-      case 2
-      thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 
-    qed
-  qed
-  finally show ?thesis .
-qed
-
-lemma readys_root:
-  assumes "th \<in> readys s"
-  shows "root (RAG s) (Th th)"
-proof -
-  { fix x
-    assume "x \<in> ancestors (RAG s) (Th th)"
-    hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
-    from tranclD[OF this]
-    obtain z where "(Th th, z) \<in> RAG s" by auto
-    with assms(1) have False
-         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
-         by (fold wq_def, blast)
-  } thus ?thesis by (unfold root_def, auto)
-qed
-
-lemma readys_in_no_subtree:
-  assumes "th \<in> readys s"
-  and "th' \<noteq> th"
-  shows "Th th \<notin> subtree (RAG s) (Th th')" 
-proof
-   assume "Th th \<in> subtree (RAG s) (Th th')"
-   thus False
-   proof(cases rule:subtreeE)
-      case 1
-      with assms show ?thesis by auto
-   next
-      case 2
-      with readys_root[OF assms(1)]
-      show ?thesis by (auto simp:root_def)
-   qed
-qed
-
-lemma not_in_thread_isolated:
-  assumes "th \<notin> threads s"
-  shows "(Th th) \<notin> Field (RAG s)"
-proof
-  assume "(Th th) \<in> Field (RAG s)"
-  with dm_RAG_threads and rg_RAG_threads assms
-  show False by (unfold Field_def, blast)
-qed
-
-end
-
 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
   where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"
 
-
 lemma detached_test:
   shows "detached s th = (Th th \<notin> Field (RAG s))"
 apply(simp add: detached_def Field_def)
@@ -4445,6 +4341,35 @@
 
 end
 
+section {* hhh *}
+
+lemma cp_alt_def1: 
+  "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
+proof -
+  have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
+       ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
+       by auto
+  thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
+qed
+
+lemma cp_gen_def_cond: 
+  assumes "x = Th th"
+  shows "cp s th = cp_gen s (Th th)"
+by (unfold cp_alt_def1 cp_gen_def, simp)
+
+lemma cp_gen_over_set:
+  assumes "\<forall> x \<in> A. \<exists> th. x = Th th"
+  shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"
+proof(rule f_image_eq)
+  fix a
+  assume "a \<in> A"
+  from assms[rule_format, OF this]
+  obtain th where eq_a: "a = Th th" by auto
+  show "cp_gen s a = (cp s \<circ> the_thread) a"
+    by  (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
+qed
+
+
 context valid_trace
 begin
 (* ddd *)
@@ -4523,58 +4448,7 @@
   qed
 qed
 
-lemma next_th_holding:
-  assumes nxt: "next_th s th cs th'"
-  shows "holding (wq s) th cs"
-proof -
-  from nxt[unfolded next_th_def]
-  obtain rest where h: "wq s cs = th # rest"
-                       "rest \<noteq> []" 
-                       "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
-  thus ?thesis
-    by (unfold cs_holding_def, auto)
-qed
-
-lemma next_th_waiting:
-  assumes nxt: "next_th s th cs th'"
-  shows "waiting (wq s) th' cs"
-proof -
-  from nxt[unfolded next_th_def]
-  obtain rest where h: "wq s cs = th # rest"
-                       "rest \<noteq> []" 
-                       "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
-  from wq_distinct[of cs, unfolded h]
-  have dst: "distinct (th # rest)" .
-  have in_rest: "th' \<in> set rest"
-  proof(unfold h, rule someI2)
-    show "distinct rest \<and> set rest = set rest" using dst by auto
-  next
-    fix x assume "distinct x \<and> set x = set rest"
-    with h(2)
-    show "hd x \<in> set (rest)" by (cases x, auto)
-  qed
-  hence "th' \<in> set (wq s cs)" by (unfold h(1), auto)
-  moreover have "th' \<noteq> hd (wq s cs)"
-    by (unfold h(1), insert in_rest dst, auto)
-  ultimately show ?thesis by (auto simp:cs_waiting_def)
-qed
-
-lemma next_th_RAG:
-  assumes nxt: "next_th (s::event list) th cs th'"
-  shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"
-  using vt assms next_th_holding next_th_waiting
-  by (unfold s_RAG_def, simp)
-
-end
-
-lemma next_th_unique: 
-  assumes nt1: "next_th s th cs th1"
-  and nt2: "next_th s th cs th2"
-  shows "th1 = th2"
-using assms by (unfold next_th_def, auto)
-
-context valid_trace
-begin
+section {* Relating @{term cp}-values of @{term threads} and @{term readys }*}
 
 lemma threads_alt_def:
   "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
@@ -4645,37 +4519,16 @@
   finally show ?thesis by simp
 qed (auto simp:threads_alt_def)
 
-lemma create_pre:
-  assumes stp: "step s e"
-  and not_in: "th \<notin> threads s"
-  and is_in: "th \<in> threads (e#s)"
-  obtains prio where "e = Create th prio"
-proof -
-  from assms  
-  show ?thesis
-  proof(cases)
-    case (thread_create thread prio)
-    with is_in not_in have "e = Create th prio" by simp
-    from that[OF this] show ?thesis .
-  next
-    case (thread_exit thread)
-    with assms show ?thesis by (auto intro!:that)
-  next
-    case (thread_P thread)
-    with assms show ?thesis by (auto intro!:that)
-  next
-    case (thread_V thread)
-    with assms show ?thesis by (auto intro!:that)
-  next 
-    case (thread_set thread)
-    with assms show ?thesis by (auto intro!:that)
-  qed
-qed
-
 end
 
 section {* Pending properties *}
 
+lemma next_th_unique: 
+  assumes nt1: "next_th s th cs th1"
+  and nt2: "next_th s th cs th2"
+  shows "th1 = th2"
+using assms by (unfold next_th_def, auto)
+
 lemma holding_next_thI:
   assumes "holding s th cs"
   and "length (wq s cs) > 1"
@@ -4704,5 +4557,143 @@
 
 end
 
+context valid_trace
+begin
+
+lemma create_pre:
+  assumes stp: "step s e"
+  and not_in: "th \<notin> threads s"
+  and is_in: "th \<in> threads (e#s)"
+  obtains prio where "e = Create th prio"
+proof -
+  from assms  
+  show ?thesis
+  proof(cases)
+    case (thread_create thread prio)
+    with is_in not_in have "e = Create th prio" by simp
+    from that[OF this] show ?thesis .
+  next
+    case (thread_exit thread)
+    with assms show ?thesis by (auto intro!:that)
+  next
+    case (thread_P thread)
+    with assms show ?thesis by (auto intro!:that)
+  next
+    case (thread_V thread)
+    with assms show ?thesis by (auto intro!:that)
+  next 
+    case (thread_set thread)
+    with assms show ?thesis by (auto intro!:that)
+  qed
+qed
+
+lemma subtree_tRAG_thread:
+  assumes "th \<in> threads s"
+  shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")
+proof -
+  have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
+    by (unfold tRAG_subtree_eq, simp)
+  also have "... \<subseteq> ?R"
+  proof
+    fix x
+    assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
+    then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto
+    from this(2)
+    show "x \<in> ?R"
+    proof(cases rule:subtreeE)
+      case 1
+      thus ?thesis by (simp add: assms h(1)) 
+    next
+      case 2
+      thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 
+    qed
+  qed
+  finally show ?thesis .
+qed
+
+lemma readys_root:
+  assumes "th \<in> readys s"
+  shows "root (RAG s) (Th th)"
+proof -
+  { fix x
+    assume "x \<in> ancestors (RAG s) (Th th)"
+    hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
+    from tranclD[OF this]
+    obtain z where "(Th th, z) \<in> RAG s" by auto
+    with assms(1) have False
+         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
+         by (fold wq_def, blast)
+  } thus ?thesis by (unfold root_def, auto)
+qed
+
+lemma readys_in_no_subtree:
+  assumes "th \<in> readys s"
+  and "th' \<noteq> th"
+  shows "Th th \<notin> subtree (RAG s) (Th th')" 
+proof
+   assume "Th th \<in> subtree (RAG s) (Th th')"
+   thus False
+   proof(cases rule:subtreeE)
+      case 1
+      with assms show ?thesis by auto
+   next
+      case 2
+      with readys_root[OF assms(1)]
+      show ?thesis by (auto simp:root_def)
+   qed
+qed
+
+lemma not_in_thread_isolated:
+  assumes "th \<notin> threads s"
+  shows "(Th th) \<notin> Field (RAG s)"
+proof
+  assume "(Th th) \<in> Field (RAG s)"
+  with dm_RAG_threads and rg_RAG_threads assms
+  show False by (unfold Field_def, blast)
+qed
+
+lemma next_th_holding:
+  assumes nxt: "next_th s th cs th'"
+  shows "holding (wq s) th cs"
+proof -
+  from nxt[unfolded next_th_def]
+  obtain rest where h: "wq s cs = th # rest"
+                       "rest \<noteq> []" 
+                       "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
+  thus ?thesis
+    by (unfold cs_holding_def, auto)
+qed
+
+lemma next_th_waiting:
+  assumes nxt: "next_th s th cs th'"
+  shows "waiting (wq s) th' cs"
+proof -
+  from nxt[unfolded next_th_def]
+  obtain rest where h: "wq s cs = th # rest"
+                       "rest \<noteq> []" 
+                       "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
+  from wq_distinct[of cs, unfolded h]
+  have dst: "distinct (th # rest)" .
+  have in_rest: "th' \<in> set rest"
+  proof(unfold h, rule someI2)
+    show "distinct rest \<and> set rest = set rest" using dst by auto
+  next
+    fix x assume "distinct x \<and> set x = set rest"
+    with h(2)
+    show "hd x \<in> set (rest)" by (cases x, auto)
+  qed
+  hence "th' \<in> set (wq s cs)" by (unfold h(1), auto)
+  moreover have "th' \<noteq> hd (wq s cs)"
+    by (unfold h(1), insert in_rest dst, auto)
+  ultimately show ?thesis by (auto simp:cs_waiting_def)
+qed
+
+lemma next_th_RAG:
+  assumes nxt: "next_th (s::event list) th cs th'"
+  shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"
+  using vt assms next_th_holding next_th_waiting
+  by (unfold s_RAG_def, simp)
+
 end
 
+end
\ No newline at end of file