
diff -r da27bece9575 -r f9e6c4166476 PIPBasics.thy
--- a/PIPBasics.thy	Fri Jun 23 00:27:16 2017 +0100
+++ b/PIPBasics.thy	Tue Jun 27 14:49:42 2017 +0100
@@ -396,25 +396,17 @@
   show ?thesis using that by auto
 qed
 
+
 lemma trancl_tG_tRAG:
   assumes "(th1, th2) \<in> (tG s)^+"
   shows "(Th th1, Th th2) \<in> (tRAG s)^+"
-proof -
-  have "inj_on the_thread (Field (tRAG s))"
-    by (unfold inj_on_def Field_def tRAG_alt_def, auto)
-  from map_prod_tranclE[OF assms[unfolded tG_def] this]
-  obtain u' v' where h: "th1 = the_thread u'" "th2 = the_thread v'" "(u', v') \<in> (tRAG s)\<^sup>+"
-    by auto
-  hence "u' \<in> Domain ((tRAG s)\<^sup>+)" "v' \<in> Range ((tRAG s)\<^sup>+)" by (auto simp:Domain_def Range_def)
-  from this[unfolded trancl_domain trancl_range]
-  have "u' \<in> Field (tRAG s)" "v' \<in> Field (tRAG s)" 
-    by (unfold Field_def, auto)
-  then obtain th1' th2' where h': "u' = Th th1'" "v' = Th th2'"
-    by (auto elim!:Field_tRAGE)
-  with h have "th1' = th1" "th2' = th2" by (auto)
-  from h(3)[unfolded h' this]
-  show ?thesis by (auto simp:ancestors_def)
-qed
+  using assms unfolding tRAG_def_tG
+proof(induct rule:trancl_induct)
+  case (step y z)
+  from step(2) have "(Th y, Th z) \<in> map_prod Th Th ` (tG s)" by auto
+  with step(3)
+  show ?case by auto
+qed auto
 
 lemma rtrancl_tG_tRAG:
   assumes "(th1, th2) \<in> (tG s)^*"
@@ -706,24 +698,14 @@
   (and specifically {\em relational tree} and {\em relational forest})
   are in place.
 *}
+
+lemma cp_s_def: "cp s th = Max (preceds (subtree (tG s) th) s)"
+  by (unfold cp_eq cpreced_def s_tG_abv, simp)
+
 lemma cp_alt_def:
   "cp s th =  Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
-proof -
-  have "Max (the_preced s ` ({th} \<union> dependants s th)) =
-        Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" 
-          (is "Max (_ ` ?L) = Max (_ ` ?R)")
-  proof -
-    have "?L = ?R" 
-    unfolding subtree_def
-    apply(auto)
-    apply (simp add: s_RAG_abv s_dependants_def wq_def)
-    by (simp add: rtrancl_eq_or_trancl s_RAG_abv s_dependants_def wq_def)
-    thus ?thesis by simp
-  qed
-  thus ?thesis
-  by (metis (no_types, lifting) cp_eq cpreced_def2 f_image_eq 
-      s_dependants_abv the_preced_def)
-qed
+  apply (unfold cp_s_def subtree_tG_tRAG threads_set_eq)
+  by (smt Collect_cong Setcompr_eq_image the_preced_def)
 
 text {*
   The following is another definition of @{term cp}.
@@ -803,56 +785,6 @@
   } ultimately show ?thesis by auto
 qed
 
-text {* 
-  The following lemmas gives an alternative definition @{term dependants}
-  in terms of @{term tRAG}.
-*}
-
-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)
-
-text {* 
-  The following lemmas gives another alternative definition @{term dependants}
-  in terms of @{term RAG}.
-*}
-
-lemma dependants_alt_def1:
-  "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}"
-  using dependants_alt_def tRAG_trancl_eq by auto
-
-text {*
-  Another definition of dependants based on @{term tG}:
-*}
-lemma dependants_alt_tG:
-  "dependants s th = {th'. (th', th) \<in> (tG s)^+}" (is "?L = ?R")
-proof -
-  have "?L = {th'. (Th th', Th th) \<in> (tRAG s)\<^sup>+}"
-    by (unfold dependants_alt_def, simp)
-  also have "... = ?R" (is "?LL = ?RR")
-  proof -
-    { fix th'
-      assume "th' \<in> ?LL"
-      hence "(Th th', Th th) \<in> (tRAG s)\<^sup>+" by simp
-      from trancl_tRAG_tG[OF this]
-      have "th' \<in> ?RR" by auto
-    } moreover {
-      fix th'
-      assume "th' \<in> ?RR"
-      hence "(th', th) \<in> (tG s)\<^sup>+" by simp
-      from trancl_tG_tRAG[OF this]
-      have "th' \<in> ?LL" by auto
-    } ultimately show ?thesis by auto
-  qed
-  finally show ?thesis .
-qed
-
-lemma dependants_alt_def_tG_ancestors:
-  "dependants s th =  {th'. th \<in> ancestors (tG s) th'}"
-  by (unfold dependants_alt_tG ancestors_def, simp)
-
-
-
 section {* Locales used to investigate the execution of PIP *}
 
 text {* 
@@ -2543,8 +2475,22 @@
   show ?thesis by simp
 qed
 
+find_theorems inj finite "_ ` _"
+
+find_theorems tG tRAG
+
+thm tRAG_def_tG
+
+find_theorems "finite (?f ` ?A)" "finite ?A"
+
 lemma finite_tG: "finite (tG s)"
-  by (unfold tG_def, insert finite_tRAG, auto)
+proof(rule finite_imageD)
+  from finite_tRAG[unfolded tRAG_def_tG]
+  show "finite (map_prod Th Th ` tG s)" .
+next
+  show "inj_on (map_prod Th Th) (tG s)"
+    using inj_on_def by fastforce
+qed
 
 end
 
@@ -3108,7 +3054,7 @@
       by (unfold tRAG_alt_def Domain_def Range_def inj_on_def, auto)
   qed
   thus ?thesis
-  by (unfold tG_def, fold rel_map_alt_def, simp)
+  by (unfold tG_def_tRAG, fold rel_map_alt_def, simp) 
 qed
 
 lemma sgv_wRAG: "single_valued (wRAG s)"
@@ -3344,9 +3290,20 @@
 proof -
   from th_chain_to_ready[OF assms]
   show ?thesis
-  using dependants_alt_def1 dependants_alt_tG 
-  unfolding nancestors_def ancestors_def
-  by blast 
+  proof
+    assume "th \<in> readys s"
+    thus ?thesis by (unfold nancestors_def, auto)
+  next
+    assume "\<exists>th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)\<^sup>+"
+    then obtain th' where h: "th' \<in> readys s" "(Th th, Th th') \<in> (RAG s)\<^sup>+" by auto
+    from h(2) tRAG_trancl_eq
+    have "(Th th, Th th') \<in> (tRAG s)^+" by auto
+    hence "(th, th') \<in> (tG s)^+"
+      by (metis the_thread.simps trancl_tRAG_tG)
+    with h(1)
+    show ?thesis
+      using ancestors_def mem_Collect_eq nancestors2 by fastforce
+  qed
 qed
 
 
@@ -3754,7 +3711,6 @@
   over the union of subtrees, the following equation can be derived:
 *}
 
-
 lemma cp_alt_def3:
   shows "cp s th = Max (preceds (subtree (tG s) th) s)"
 unfolding cp_alt_def2
@@ -5173,19 +5129,13 @@
   shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
   using count_eq_RAG_plus[OF assms] by auto
 
-lemma eq_pv_dependants:
-  assumes eq_pv: "cntP s th = cntV s th"
-  shows "dependants s th = {}"
-proof -
-  from count_eq_RAG_plus[OF assms, folded dependants_alt_def1]
-  show ?thesis .
-qed
 
 lemma count_eq_tRAG_plus:
   assumes "cntP s th = cntV s th"
   shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
-  using assms count_eq_RAG_plus dependants_alt_def s_dependants_def by blast
-
+  using count_eq_RAG_plus_Th[OF assms]
+  using tRAG_trancl_eq by auto
+  
 lemma count_eq_tRAG_plus_Th:
   assumes "cntP s th = cntV s th"
   shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"




