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) \ (tG s)^+" shows "(Th th1, Th th2) \ (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') \ (tRAG s)\<^sup>+" - by auto - hence "u' \ Domain ((tRAG s)\<^sup>+)" "v' \ Range ((tRAG s)\<^sup>+)" by (auto simp:Domain_def Range_def) - from this[unfolded trancl_domain trancl_range] - have "u' \ Field (tRAG s)" "v' \ 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) \ map_prod Th Th ` (tG s)" by auto + with step(3) + show ?case by auto +qed auto lemma rtrancl_tG_tRAG: assumes "(th1, th2) \ (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' \ (subtree (RAG s) (Th th))})" -proof - - have "Max (the_preced s ` ({th} \ dependants s th)) = - Max (the_preced s ` {th'. Th th' \ 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) \ (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) \ (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) \ (tG s)^+}" (is "?L = ?R") -proof - - have "?L = {th'. (Th th', Th th) \ (tRAG s)\<^sup>+}" - by (unfold dependants_alt_def, simp) - also have "... = ?R" (is "?LL = ?RR") - proof - - { fix th' - assume "th' \ ?LL" - hence "(Th th', Th th) \ (tRAG s)\<^sup>+" by simp - from trancl_tRAG_tG[OF this] - have "th' \ ?RR" by auto - } moreover { - fix th' - assume "th' \ ?RR" - hence "(th', th) \ (tG s)\<^sup>+" by simp - from trancl_tG_tRAG[OF this] - have "th' \ ?LL" by auto - } ultimately show ?thesis by auto - qed - finally show ?thesis . -qed - -lemma dependants_alt_def_tG_ancestors: - "dependants s th = {th'. th \ 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 \ readys s" + thus ?thesis by (unfold nancestors_def, auto) + next + assume "\th'. th' \ readys s \ (Th th, Th th') \ (RAG s)\<^sup>+" + then obtain th' where h: "th' \ readys s" "(Th th, Th th') \ (RAG s)\<^sup>+" by auto + from h(2) tRAG_trancl_eq + have "(Th th, Th th') \ (tRAG s)^+" by auto + hence "(th, th') \ (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) \ (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) \ (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) \ (tRAG s)^+} = {}"