--- 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)^+} = {}"