diff -r 0a069a667301 -r f98a95f3deae CpsG.thy --- a/CpsG.thy Tue Dec 15 15:10:40 2015 +0000 +++ b/CpsG.thy Fri Dec 18 19:13:19 2015 +0800 @@ -21,6 +21,22 @@ \ cs. (Th th1, Cs cs) \ RAG s \ (Cs cs, Th th2) \ RAG s}" by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) +lemma tRAG_Field: + "Field (tRAG s) \ Field (RAG s)" + by (unfold tRAG_alt_def Field_def, auto) + +lemma tRAG_ancestorsE: + assumes "x \ ancestors (tRAG s) u" + obtains th where "x = Th th" +proof - + from assms have "(u, x) \ (tRAG s)^+" + by (unfold ancestors_def, auto) + from tranclE[OF this] obtain c where "(c, x) \ tRAG s" by auto + then obtain th where "x = Th th" + by (unfold tRAG_alt_def, auto) + from that[OF this] show ?thesis . +qed + lemma tRAG_mono: assumes "RAG s' \ RAG s" shows "tRAG s' \ tRAG s" @@ -205,45 +221,43 @@ qed qed -lemma threads_set_eq: - "the_thread ` (subtree (tRAG s) (Th th)) = - {th'. Th th' \ (subtree (RAG s) (Th th))}" (is "?L = ?R") +lemma tRAG_star_RAG: "(tRAG s)^* \ (RAG s)^*" +proof - + have "(wRAG s O hRAG s)^* \ (RAG s O RAG s)^*" + by (rule rtrancl_mono, auto simp:RAG_split) + also have "... \ ((RAG s)^*)^*" + by (rule rtrancl_mono, auto) + also have "... = (RAG s)^*" by simp + finally show ?thesis by (unfold tRAG_def, simp) +qed + +lemma tRAG_subtree_RAG: "subtree (tRAG s) x \ subtree (RAG s) x" proof - - { fix th' - assume "th' \ ?L" - then obtain n where h: "th' = the_thread n" "n \ subtree (tRAG s) (Th th)" by auto - from subtree_nodeE[OF this(2)] - obtain th1 where "n = Th th1" by auto - with h have "Th th' \ subtree (tRAG s) (Th th)" by auto - hence "Th th' \ subtree (RAG s) (Th th)" - proof(cases rule:subtreeE[consumes 1]) - case 1 - thus ?thesis by (auto simp:subtree_def) - next - case 2 - hence "(Th th', Th th) \ (tRAG s)^+" by (auto simp:ancestors_def) - thus ?thesis - proof(induct) - case (step y z) - from this(2)[unfolded tRAG_alt_def] - obtain u where - h: "(y, u) \ RAG s" "(u, z) \ RAG s" - by auto - hence "y \ subtree (RAG s) z" by (auto simp:subtree_def) - with step(3) - show ?case by (auto simp:subtree_def) - next - case (base y) - from this[unfolded tRAG_alt_def] - show ?case by (auto simp:subtree_def) - qed - qed - hence "th' \ ?R" by auto + { fix a + assume "a \ subtree (tRAG s) x" + hence "(a, x) \ (tRAG s)^*" by (auto simp:subtree_def) + with tRAG_star_RAG[of s] + have "(a, x) \ (RAG s)^*" by auto + hence "a \ subtree (RAG s) x" by (auto simp:subtree_def) + } thus ?thesis by auto +qed + +lemma tRAG_subtree_eq: + "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \ (subtree (RAG s) (Th th))}" + (is "?L = ?R") +proof - + { fix n + assume "n \ ?L" + with subtree_nodeE[OF this] + obtain th' where "n = Th th'" "Th th' \ subtree (tRAG s) (Th th)" by auto + with tRAG_subtree_RAG[of s "Th th"] + have "n \ ?R" by auto } moreover { - fix th' - assume "th' \ ?R" - hence "(Th th', Th th) \ (RAG s)^*" by (auto simp:subtree_def) - from star_rpath[OF this] + fix n + assume "n \ ?R" + then obtain th' where h: "n = Th th'" "(Th th', Th th) \ (RAG s)^*" + by (auto simp:subtree_def) + from star_rpath[OF this(2)] obtain xs where "rpath (RAG s) (Th th') xs (Th th)" by auto hence "Th th' \ subtree (tRAG s) (Th th)" proof(induct xs arbitrary:th' th rule:length_induct) @@ -264,7 +278,6 @@ hence "(Th th', x1) \ (RAG s)" by (cases, simp) then obtain cs where "x1 = Cs cs" by (unfold s_RAG_def, auto) - find_theorems rpath "_ = _@[_]" from rpath_nnl_lastE[OF rp[unfolded this]] show ?thesis by auto next @@ -297,11 +310,16 @@ qed qed qed - from imageI[OF this, of the_thread] - have "th' \ ?L" by simp + from this[folded h(1)] + have "n \ ?L" . } ultimately show ?thesis by auto qed - + +lemma threads_set_eq: + "the_thread ` (subtree (tRAG s) (Th th)) = + {th'. Th th' \ (subtree (RAG s) (Th th))}" (is "?L = ?R") + by (auto intro:rev_image_eqI simp:tRAG_subtree_eq) + lemma cp_alt_def1: "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))" proof - @@ -337,6 +355,15 @@ context valid_trace begin +lemma not_in_thread_isolated: + assumes "th \ threads s" + shows "(Th th) \ Field (RAG s)" +proof + assume "(Th th) \ Field (RAG s)" + with dm_RAG_threads[OF vt] and range_in[OF vt] assms + show False by (unfold Field_def, blast) +qed + lemma wf_RAG: "wf (RAG s)" proof(rule finite_acyclic_wf) from finite_RAG[OF vt] show "finite (RAG s)" . @@ -1572,25 +1599,30 @@ context step_P_cps begin -lemma rtree_RAGs: "rtree (RAG s)" -proof - show "single_valued (RAG s)" - apply (intro_locales) - by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s]) - - show "acyclic (RAG s)" - by (rule acyclic_RAG[OF vt_s]) +lemma readys_th: "th \ readys s'" +proof - + from step_back_step [OF vt_s[unfolded s_def]] + have "PIP s' (P th cs)" . + hence "th \ runing s'" by (cases, simp) + thus ?thesis by (simp add:readys_def runing_def) qed -lemma rtree_RAGs': "rtree (RAG s')" +lemma root_th: "root (RAG s') (Th th)" + using readys_root[OF vat_s'.vt readys_th] . + +lemma in_no_others_subtree: + assumes "th' \ th" + shows "Th th \ subtree (RAG s') (Th th')" proof - show "single_valued (RAG s')" - apply (intro_locales) - by (unfold single_valued_def, - auto intro:unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]]) - - show "acyclic (RAG s')" - by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]]) + assume "Th th \ subtree (RAG s') (Th th')" + thus False + proof(cases rule:subtreeE) + case 1 + with assms show ?thesis by auto + next + case 2 + with root_th show ?thesis by (auto simp:root_def) + qed qed lemma preced_kept: "the_preced s = the_preced s'" @@ -1615,143 +1647,26 @@ show ?thesis by auto qed -lemma child_kept_left: - assumes - "(n1, n2) \ (child s')^+" - shows "(n1, n2) \ (child s)^+" -proof - - from assms show ?thesis - proof(induct rule: converse_trancl_induct) - case (base y) - from base obtain th1 cs1 th2 - where h1: "(Th th1, Cs cs1) \ RAG s'" - and h2: "(Cs cs1, Th th2) \ RAG s'" - and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2" by (auto simp:child_def) - have "cs1 \ cs" - proof - assume eq_cs: "cs1 = cs" - with h1 have "(Th th1, Cs cs) \ RAG s'" by simp - with ee show False - by (auto simp:s_RAG_def cs_waiting_def) - qed - with h1 h2 RAG_s have - h1': "(Th th1, Cs cs1) \ RAG s" and - h2': "(Cs cs1, Th th2) \ RAG s" by auto - hence "(Th th1, Th th2) \ child s" by (auto simp:child_def) - with eq_y eq_n2 have "(y, n2) \ child s" by simp - thus ?case by auto - next - case (step y z) - have "(y, z) \ child s'" by fact - then obtain th1 cs1 th2 - where h1: "(Th th1, Cs cs1) \ RAG s'" - and h2: "(Cs cs1, Th th2) \ RAG s'" - and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def) - have "cs1 \ cs" - proof - assume eq_cs: "cs1 = cs" - with h1 have "(Th th1, Cs cs) \ RAG s'" by simp - with ee show False - by (auto simp:s_RAG_def cs_waiting_def) - qed - with h1 h2 RAG_s have - h1': "(Th th1, Cs cs1) \ RAG s" and - h2': "(Cs cs1, Th th2) \ RAG s" by auto - hence "(Th th1, Th th2) \ child s" by (auto simp:child_def) - with eq_y eq_z have "(y, z) \ child s" by simp - moreover have "(z, n2) \ (child s)^+" by fact - ultimately show ?case by auto - qed +lemma subtree_kept: + assumes "th' \ th" + shows "subtree (RAG s) (Th th') = subtree (RAG s') (Th th')" +proof(unfold RAG_s, rule subtree_insert_next) + from in_no_others_subtree[OF assms] + show "Th th \ subtree (RAG s') (Th th')" . qed -lemma child_kept_right: - assumes - "(n1, n2) \ (child s)^+" - shows "(n1, n2) \ (child s')^+" +lemma cp_kept: + assumes "th' \ th" + shows "cp s th' = cp s' th'" proof - - from assms show ?thesis - proof(induct) - case (base y) - from base and RAG_s - have "(n1, y) \ child s'" - apply (auto simp:child_def) - proof - - fix th' - assume "(Th th', Cs cs) \ RAG s'" - with ee have "False" - by (auto simp:s_RAG_def cs_waiting_def) - thus "\cs. (Th th', Cs cs) \ RAG s' \ (Cs cs, Th th) \ RAG s'" by auto - qed - thus ?case by auto - next - case (step y z) - have "(y, z) \ child s" by fact - with RAG_s have "(y, z) \ child s'" - apply (auto simp:child_def) - proof - - fix th' - assume "(Th th', Cs cs) \ RAG s'" - with ee have "False" - by (auto simp:s_RAG_def cs_waiting_def) - thus "\cs. (Th th', Cs cs) \ RAG s' \ (Cs cs, Th th) \ RAG s'" by auto - qed - moreover have "(n1, y) \ (child s')\<^sup>+" by fact - ultimately show ?case by auto - qed -qed - -lemma eq_child: "(child s)^+ = (child s')^+" - by (insert child_kept_left child_kept_right, auto) - -lemma eq_cp: - fixes th' - shows "cp s th' = cp s' th'" - apply (unfold cp_eq_cpreced cpreced_def) -proof - - have eq_dp: "\ th. dependants (wq s) th = dependants (wq s') th" - apply (unfold cs_dependants_def, unfold eq_RAG) - proof - - from eq_child - have "\th. {th'. (Th th', Th th) \ (child s)\<^sup>+} = {th'. (Th th', Th th) \ (child s')\<^sup>+}" - by auto - with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] - show "\th. {th'. (Th th', Th th) \ (RAG s)\<^sup>+} = {th'. (Th th', Th th) \ (RAG s')\<^sup>+}" - by simp - qed - moreover { - fix th1 - assume "th1 \ {th'} \ dependants (wq s') th'" - hence "th1 = th' \ th1 \ dependants (wq s') th'" by auto - hence "preced th1 s = preced th1 s'" - proof - assume "th1 = th'" - show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) - next - assume "th1 \ dependants (wq s') th'" - show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) - qed - } ultimately have "((\th. preced th s) ` ({th'} \ dependants (wq s) th')) = - ((\th. preced th s') ` ({th'} \ dependants (wq s') th'))" - by (auto simp:image_def) - thus "Max ((\th. preced th s) ` ({th'} \ dependants (wq s) th')) = - Max ((\th. preced th s') ` ({th'} \ dependants (wq s') th'))" by simp + have "(the_preced s ` {th'a. Th th'a \ subtree (RAG s) (Th th')}) = + (the_preced s' ` {th'a. Th th'a \ subtree (RAG s') (Th th')})" + by (unfold preced_kept subtree_kept[OF assms], simp) + thus ?thesis by (unfold cp_alt_def, simp) qed end -lemma tRAG_ancestorsE: - assumes "x \ ancestors (tRAG s) u" - obtains th where "x = Th th" -proof - - from assms have "(u, x) \ (tRAG s)^+" - by (unfold ancestors_def, auto) - from tranclE[OF this] obtain c where "(c, x) \ tRAG s" by auto - then obtain th where "x = Th th" - by (unfold tRAG_alt_def, auto) - from that[OF this] show ?thesis . -qed - - context step_P_cps_ne begin @@ -1813,19 +1728,7 @@ show ?thesis by (unfold cp_alt_def1 h preced_kept, simp) qed -lemma set_prop_split: - "A = {x. x \ A \ PP x} \ {x. x \ A \ \ PP x}" - by auto - -lemma f_image_union_eq: - assumes "f ` A = g ` A" - and "f ` B = g ` B" - shows "f ` (A \ B) = g ` (A \ B)" - using assms by auto - -(* ccc *) - -lemma cp_gen_update_stop: +lemma cp_gen_update_stop: (* ddd *) assumes "u \ ancestors (tRAG s) (Th th)" and "cp_gen s u = cp_gen s' u" and "y \ ancestors (tRAG s) u" @@ -1919,7 +1822,22 @@ case False from a_in obtain th_a where eq_a: "a = Th th_a" by (auto simp:RTree.children_def tRAG_alt_def) - have "a \ ancestors (tRAG s) (Th th)" sorry + have "a \ ancestors (tRAG s) (Th th)" + proof + assume a_in': "a \ ancestors (tRAG s) (Th th)" + have "a = z" + proof(rule vat_s.rtree_s.ancestors_children_unique) + from assms(1) h(1) have "z \ ancestors (tRAG s) (Th th)" + by (auto simp:ancestors_def) + with h(2) show " z \ ancestors (tRAG s) (Th th) \ + RTree.children (tRAG s) x" by auto + next + from a_in a_in' + show "a \ ancestors (tRAG s) (Th th) \ RTree.children (tRAG s) x" + by auto + qed + with False show False by auto + qed from cp_kept[OF this[unfolded eq_a]] have "cp s th_a = cp s' th_a" . from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a] @@ -1937,314 +1855,19 @@ qed qed - - -(* ccc *) - -lemma eq_child_left: - assumes nd: "(Th th, Th th') \ (child s)^+" - shows "(n1, Th th') \ (child s)^+ \ (n1, Th th') \ (child s')^+" -proof(induct rule:converse_trancl_induct) - case (base y) - from base obtain th1 cs1 - where h1: "(Th th1, Cs cs1) \ RAG s" - and h2: "(Cs cs1, Th th') \ RAG s" - and eq_y: "y = Th th1" by (auto simp:child_def) - have "th1 \ th" - proof - assume "th1 = th" - with base eq_y have "(Th th, Th th') \ child s" by simp - with nd show False by auto - qed - with h1 h2 RAG_s - have h1': "(Th th1, Cs cs1) \ RAG s'" and - h2': "(Cs cs1, Th th') \ RAG s'" by auto - with eq_y show ?case by (auto simp:child_def) -next - case (step y z) - have yz: "(y, z) \ child s" by fact - then obtain th1 cs1 th2 - where h1: "(Th th1, Cs cs1) \ RAG s" - and h2: "(Cs cs1, Th th2) \ RAG s" - and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def) - have "th1 \ th" - proof - assume "th1 = th" - with yz eq_y have "(Th th, z) \ child s" by simp - moreover have "(z, Th th') \ (child s)^+" by fact - ultimately have "(Th th, Th th') \ (child s)^+" by auto - with nd show False by auto - qed - with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \ RAG s'" - and h2': "(Cs cs1, Th th2) \ RAG s'" by auto - with eq_y eq_z have "(y, z) \ child s'" by (auto simp:child_def) - moreover have "(z, Th th') \ (child s')^+" by fact - ultimately show ?case by auto -qed - -lemma eq_child_right: - shows "(n1, Th th') \ (child s')^+ \ (n1, Th th') \ (child s)^+" -proof(induct rule:converse_trancl_induct) - case (base y) - with RAG_s show ?case by (auto simp:child_def) -next - case (step y z) - have "(y, z) \ child s'" by fact - with RAG_s have "(y, z) \ child s" by (auto simp:child_def) - moreover have "(z, Th th') \ (child s)^+" by fact - ultimately show ?case by auto -qed - -lemma eq_child: - assumes nd: "(Th th, Th th') \ (child s)^+" - shows "((n1, Th th') \ (child s)^+) = ((n1, Th th') \ (child s')^+)" - by (insert eq_child_left[OF nd] eq_child_right, auto) - -lemma eq_cp: - assumes nd: "th \ dependants s th'" - shows "cp s th' = cp s' th'" - apply (unfold cp_eq_cpreced cpreced_def) -proof - - have nd': "(Th th, Th th') \ (child s)^+" - proof - assume "(Th th, Th th') \ (child s)\<^sup>+" - with child_RAG_eq[OF vt_s] - have "(Th th, Th th') \ (RAG s)\<^sup>+" by simp - with nd show False - by (simp add:s_dependants_def eq_RAG) - qed - have eq_dp: "dependants (wq s) th' = dependants (wq s') th'" - proof(auto) - fix x assume " x \ dependants (wq s) th'" - thus "x \ dependants (wq s') th'" - apply (auto simp:cs_dependants_def eq_RAG) - proof - - assume "(Th x, Th th') \ (RAG s)\<^sup>+" - with child_RAG_eq[OF vt_s] have "(Th x, Th th') \ (child s)\<^sup>+" by simp - with eq_child[OF nd'] have "(Th x, Th th') \ (child s')^+" by simp - with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] - show "(Th x, Th th') \ (RAG s')\<^sup>+" by simp - qed - next - fix x assume "x \ dependants (wq s') th'" - thus "x \ dependants (wq s) th'" - apply (auto simp:cs_dependants_def eq_RAG) - proof - - assume "(Th x, Th th') \ (RAG s')\<^sup>+" - with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] - have "(Th x, Th th') \ (child s')\<^sup>+" by simp - with eq_child[OF nd'] have "(Th x, Th th') \ (child s)^+" by simp - with child_RAG_eq[OF vt_s] - show "(Th x, Th th') \ (RAG s)\<^sup>+" by simp - qed - qed - moreover { - fix th1 have "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) - } ultimately have "((\th. preced th s) ` ({th'} \ dependants (wq s) th')) = - ((\th. preced th s') ` ({th'} \ dependants (wq s') th'))" - by (auto simp:image_def) - thus "Max ((\th. preced th s) ` ({th'} \ dependants (wq s) th')) = - Max ((\th. preced th s') ` ({th'} \ dependants (wq s') th'))" by simp -qed - -lemma eq_up: - assumes dp1: "th \ dependants s th'" - and dp2: "th' \ dependants s th''" - and eq_cps: "cp s th' = cp s' th'" +lemma cp_up: + assumes "(Th th') \ ancestors (tRAG s) (Th th)" + and "cp s th' = cp s' th'" + and "(Th th'') \ ancestors (tRAG s) (Th th')" shows "cp s th'' = cp s' th''" proof - - from dp2 - have "(Th th', Th th'') \ (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def) - from RAG_child[OF vt_s this[unfolded eq_RAG]] - have ch_th': "(Th th', Th th'') \ (child s)\<^sup>+" . - moreover { - fix n th'' - have "\(Th th', n) \ (child s)^+\ \ - (\ th'' . n = Th th'' \ cp s th'' = cp s' th'')" - proof(erule trancl_induct, auto) - fix y th'' - assume y_ch: "(y, Th th'') \ child s" - and ih: "\th''. y = Th th'' \ cp s th'' = cp s' th''" - and ch': "(Th th', y) \ (child s)\<^sup>+" - from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def) - with ih have eq_cpy:"cp s thy = cp s' thy" by blast - from dp1 have "(Th th, Th th') \ (RAG s)^+" by (auto simp:s_dependants_def eq_RAG) - moreover from child_RAG_p[OF ch'] and eq_y - have "(Th th', Th thy) \ (RAG s)^+" by simp - ultimately have dp_thy: "(Th th, Th thy) \ (RAG s)^+" by auto - show "cp s th'' = cp s' th''" - apply (subst cp_rec[OF vt_s]) - proof - - have "preced th'' s = preced th'' s'" - by (simp add:s_def preced_def) - moreover { - fix th1 - assume th1_in: "th1 \ children s th''" - have "cp s th1 = cp s' th1" - proof(cases "th1 = thy") - case True - with eq_cpy show ?thesis by simp - next - case False - have neq_th1: "th1 \ th" - proof - assume eq_th1: "th1 = th" - with dp_thy have "(Th th1, Th thy) \ (RAG s)^+" by simp - from children_no_dep[OF vt_s _ _ this] and - th1_in y_ch eq_y show False by (auto simp:children_def) - qed - have "th \ dependants s th1" - proof - assume h:"th \ dependants s th1" - from eq_y dp_thy have "th \ dependants s thy" by (auto simp:s_dependants_def eq_RAG) - from dependants_child_unique[OF vt_s _ _ h this] - th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def) - with False show False by auto - qed - from eq_cp[OF this] - show ?thesis . - qed - } - ultimately have "{preced th'' s} \ (cp s ` children s th'') = - {preced th'' s'} \ (cp s' ` children s th'')" by (auto simp:image_def) - moreover have "children s th'' = children s' th''" - apply (unfold children_def child_def s_def RAG_set_unchanged, simp) - apply (fold s_def, auto simp:RAG_s) - proof - - assume "(Cs cs, Th th'') \ RAG s'" - with RAG_s have cs_th': "(Cs cs, Th th'') \ RAG s" by auto - from dp1 have "(Th th, Th th') \ (RAG s)^+" - by (auto simp:s_dependants_def eq_RAG) - from converse_tranclE[OF this] - obtain cs1 where h1: "(Th th, Cs cs1) \ RAG s" - and h2: "(Cs cs1 , Th th') \ (RAG s)\<^sup>+" - by (auto simp:s_RAG_def) - have eq_cs: "cs1 = cs" - proof - - from RAG_s have "(Th th, Cs cs) \ RAG s" by simp - from unique_RAG[OF vt_s this h1] - show ?thesis by simp - qed - have False - proof(rule converse_tranclE[OF h2]) - assume "(Cs cs1, Th th') \ RAG s" - with eq_cs have "(Cs cs, Th th') \ RAG s" by simp - from unique_RAG[OF vt_s this cs_th'] - have "th' = th''" by simp - with ch' y_ch have "(Th th'', Th th'') \ (child s)^+" by auto - with wf_trancl[OF wf_child[OF vt_s]] - show False by auto - next - fix y - assume "(Cs cs1, y) \ RAG s" - and ytd: " (y, Th th') \ (RAG s)\<^sup>+" - with eq_cs have csy: "(Cs cs, y) \ RAG s" by simp - from unique_RAG[OF vt_s this cs_th'] - have "y = Th th''" . - with ytd have "(Th th'', Th th') \ (RAG s)^+" by simp - from RAG_child[OF vt_s this] - have "(Th th'', Th th') \ (child s)\<^sup>+" . - moreover from ch' y_ch have ch'': "(Th th', Th th'') \ (child s)^+" by auto - ultimately have "(Th th'', Th th'') \ (child s)^+" by auto - with wf_trancl[OF wf_child[OF vt_s]] - show False by auto - qed - thus "\cs. (Th th, Cs cs) \ RAG s' \ (Cs cs, Th th'') \ RAG s'" by auto - qed - ultimately show "Max ({preced th'' s} \ cp s ` children s th'') = cp s' th''" - by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) - qed - next - fix th'' - assume dp': "(Th th', Th th'') \ child s" - show "cp s th'' = cp s' th''" - apply (subst cp_rec[OF vt_s]) - proof - - have "preced th'' s = preced th'' s'" - by (simp add:s_def preced_def) - moreover { - fix th1 - assume th1_in: "th1 \ children s th''" - have "cp s th1 = cp s' th1" - proof(cases "th1 = th'") - case True - with eq_cps show ?thesis by simp - next - case False - have neq_th1: "th1 \ th" - proof - assume eq_th1: "th1 = th" - with dp1 have "(Th th1, Th th') \ (RAG s)^+" - by (auto simp:s_dependants_def eq_RAG) - from children_no_dep[OF vt_s _ _ this] - th1_in dp' - show False by (auto simp:children_def) - qed - show ?thesis - proof(rule eq_cp) - show "th \ dependants s th1" - proof - assume "th \ dependants s th1" - from dependants_child_unique[OF vt_s _ _ this dp1] - th1_in dp' have "th1 = th'" - by (auto simp:children_def) - with False show False by auto - qed - qed - qed - } - ultimately have "{preced th'' s} \ (cp s ` children s th'') = - {preced th'' s'} \ (cp s' ` children s th'')" by (auto simp:image_def) - moreover have "children s th'' = children s' th''" - apply (unfold children_def child_def s_def RAG_set_unchanged, simp) - apply (fold s_def, auto simp:RAG_s) - proof - - assume "(Cs cs, Th th'') \ RAG s'" - with RAG_s have cs_th': "(Cs cs, Th th'') \ RAG s" by auto - from dp1 have "(Th th, Th th') \ (RAG s)^+" - by (auto simp:s_dependants_def eq_RAG) - from converse_tranclE[OF this] - obtain cs1 where h1: "(Th th, Cs cs1) \ RAG s" - and h2: "(Cs cs1 , Th th') \ (RAG s)\<^sup>+" - by (auto simp:s_RAG_def) - have eq_cs: "cs1 = cs" - proof - - from RAG_s have "(Th th, Cs cs) \ RAG s" by simp - from unique_RAG[OF vt_s this h1] - show ?thesis by simp - qed - have False - proof(rule converse_tranclE[OF h2]) - assume "(Cs cs1, Th th') \ RAG s" - with eq_cs have "(Cs cs, Th th') \ RAG s" by simp - from unique_RAG[OF vt_s this cs_th'] - have "th' = th''" by simp - with dp' have "(Th th'', Th th'') \ (child s)^+" by auto - with wf_trancl[OF wf_child[OF vt_s]] - show False by auto - next - fix y - assume "(Cs cs1, y) \ RAG s" - and ytd: " (y, Th th') \ (RAG s)\<^sup>+" - with eq_cs have csy: "(Cs cs, y) \ RAG s" by simp - from unique_RAG[OF vt_s this cs_th'] - have "y = Th th''" . - with ytd have "(Th th'', Th th') \ (RAG s)^+" by simp - from RAG_child[OF vt_s this] - have "(Th th'', Th th') \ (child s)\<^sup>+" . - moreover from dp' have ch'': "(Th th', Th th'') \ (child s)^+" by auto - ultimately have "(Th th'', Th th'') \ (child s)^+" by auto - with wf_trancl[OF wf_child[OF vt_s]] - show False by auto - qed - thus "\cs. (Th th, Cs cs) \ RAG s' \ (Cs cs, Th th'') \ RAG s'" by auto - qed - ultimately show "Max ({preced th'' s} \ cp s ` children s th'') = cp s' th''" - by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) - qed - qed - } - ultimately show ?thesis by auto + have "cp_gen s (Th th'') = cp_gen s' (Th th'')" + proof(rule cp_gen_update_stop[OF assms(1) _ assms(3)]) + from assms(2) cp_gen_def_cond[OF refl[of "Th th'"]] + show "cp_gen s (Th th') = cp_gen s' (Th th')" by metis + qed + with cp_gen_def_cond[OF refl[of "Th th''"]] + show ?thesis by metis qed end @@ -2254,147 +1877,182 @@ defines s_def : "s \ (Create th prio#s')" assumes vt_s: "vt s" +sublocale step_create_cps < vat_s: valid_trace "s" + by (unfold_locales, insert vt_s, simp) + +sublocale step_create_cps < vat_s': valid_trace "s'" + by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp) + context step_create_cps begin -lemma eq_dep: "RAG s = RAG s'" +lemma RAG_kept: "RAG s = RAG s'" by (unfold s_def RAG_create_unchanged, auto) +lemma tRAG_kept: "tRAG s = tRAG s'" + by (unfold tRAG_alt_def RAG_kept, auto) + +lemma preced_kept: + assumes "th' \ th" + shows "the_preced s th' = the_preced s' th'" + by (unfold s_def the_preced_def preced_def, insert assms, auto) + +lemma th_not_in: "Th th \ Field (tRAG s')" +proof - + from vt_s[unfolded s_def] + have "PIP s' (Create th prio)" by (cases, simp) + hence "th \ threads s'" by(cases, simp) + from vat_s'.not_in_thread_isolated[OF this] + have "Th th \ Field (RAG s')" . + with tRAG_Field show ?thesis by auto +qed + lemma eq_cp: - fixes th' assumes neq_th: "th' \ th" shows "cp s th' = cp s' th'" - apply (unfold cp_eq_cpreced cpreced_def) proof - - have nd: "th \ dependants s th'" - proof - assume "th \ dependants s th'" - hence "(Th th, Th th') \ (RAG s)^+" by (simp add:s_dependants_def eq_RAG) - with eq_dep have "(Th th, Th th') \ (RAG s')^+" by simp - from converse_tranclE[OF this] - obtain y where "(Th th, y) \ RAG s'" by auto - with dm_RAG_threads[OF step_back_vt[OF vt_s[unfolded s_def]]] - have in_th: "th \ threads s'" by auto - from step_back_step[OF vt_s[unfolded s_def]] - show False - proof(cases) - assume "th \ threads s'" - with in_th show ?thesis by simp + have "(the_preced s \ the_thread) ` subtree (tRAG s) (Th th') = + (the_preced s' \ the_thread) ` subtree (tRAG s') (Th th')" + proof(unfold tRAG_kept, rule f_image_eq) + fix a + assume a_in: "a \ subtree (tRAG s') (Th th')" + then obtain th_a where eq_a: "a = Th th_a" + proof(cases rule:subtreeE) + case 2 + from ancestors_Field[OF 2(2)] + and that show ?thesis by (unfold tRAG_alt_def, auto) + qed auto + have neq_th_a: "th_a \ th" + proof - + have "(Th th) \ subtree (tRAG s') (Th th')" + proof + assume "Th th \ subtree (tRAG s') (Th th')" + thus False + proof(cases rule:subtreeE) + case 2 + from ancestors_Field[OF this(2)] + and th_not_in[unfolded Field_def] + show ?thesis by auto + qed (insert assms, auto) + qed + with a_in[unfolded eq_a] show ?thesis by auto qed + from preced_kept[OF this] + show "(the_preced s \ the_thread) a = (the_preced s' \ the_thread) a" + by (unfold eq_a, simp) qed - have eq_dp: "\ th. dependants (wq s) th = dependants (wq s') th" - by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG) - moreover { - fix th1 - assume "th1 \ {th'} \ dependants (wq s') th'" - hence "th1 = th' \ th1 \ dependants (wq s') th'" by auto - hence "preced th1 s = preced th1 s'" - proof - assume "th1 = th'" - with neq_th - show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def) - next - assume "th1 \ dependants (wq s') th'" - with nd and eq_dp have "th1 \ th" - by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep) - thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def) - qed - } ultimately have "((\th. preced th s) ` ({th'} \ dependants (wq s) th')) = - ((\th. preced th s') ` ({th'} \ dependants (wq s') th'))" - by (auto simp:image_def) - thus "Max ((\th. preced th s) ` ({th'} \ dependants (wq s) th')) = - Max ((\th. preced th s') ` ({th'} \ dependants (wq s') th'))" by simp + thus ?thesis by (unfold cp_alt_def1, simp) qed -lemma nil_dependants: "dependants s th = {}" +lemma children_of_th: "RTree.children (tRAG s) (Th th) = {}" proof - - from step_back_step[OF vt_s[unfolded s_def]] - show ?thesis - proof(cases) - assume "th \ threads s'" - from not_thread_holdents[OF step_back_vt[OF vt_s[unfolded s_def]] this] - have hdn: " holdents s' th = {}" . - have "dependants s' th = {}" - proof - - { assume "dependants s' th \ {}" - then obtain th' where dp: "(Th th', Th th) \ (RAG s')^+" - by (auto simp:s_dependants_def eq_RAG) - from tranclE[OF this] obtain cs' where - "(Cs cs', Th th) \ RAG s'" by (auto simp:s_RAG_def) - with hdn - have False by (auto simp:holdents_test) - } thus ?thesis by auto - qed - thus ?thesis - by (unfold s_def s_dependants_def eq_RAG RAG_create_unchanged, simp) - qed + { fix a + assume "a \ RTree.children (tRAG s) (Th th)" + hence "(a, Th th) \ tRAG s" by (auto simp:RTree.children_def) + with th_not_in have False + by (unfold Field_def tRAG_kept, auto) + } thus ?thesis by auto qed lemma eq_cp_th: "cp s th = preced th s" - apply (unfold cp_eq_cpreced cpreced_def) - by (insert nil_dependants, unfold s_dependants_def cs_dependants_def, auto) + by (unfold vat_s.cp_rec children_of_th, simp add:the_preced_def) end - locale step_exit_cps = fixes s' th prio s defines s_def : "s \ Exit th # s'" assumes vt_s: "vt s" +sublocale step_exit_cps < vat_s: valid_trace "s" + by (unfold_locales, insert vt_s, simp) + +sublocale step_exit_cps < vat_s': valid_trace "s'" + by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp) + context step_exit_cps begin -lemma eq_dep: "RAG s = RAG s'" +lemma preced_kept: + assumes "th' \ th" + shows "the_preced s th' = the_preced s' th'" + by (unfold s_def the_preced_def preced_def, insert assms, auto) + +lemma RAG_kept: "RAG s = RAG s'" by (unfold s_def RAG_exit_unchanged, auto) +lemma tRAG_kept: "tRAG s = tRAG s'" + by (unfold tRAG_alt_def RAG_kept, auto) + +lemma th_ready: "th \ readys s'" +proof - + from vt_s[unfolded s_def] + have "PIP s' (Exit th)" by (cases, simp) + hence h: "th \ runing s' \ holdents s' th = {}" by (cases, metis) + thus ?thesis by (unfold runing_def, auto) +qed + +lemma th_holdents: "holdents s' th = {}" +proof - + from vt_s[unfolded s_def] + have "PIP s' (Exit th)" by (cases, simp) + thus ?thesis by (cases, metis) +qed + +lemma th_RAG: "Th th \ Field (RAG s')" +proof - + have "Th th \ Range (RAG s')" + proof + assume "Th th \ Range (RAG s')" + then obtain cs where "holding (wq s') th cs" + by (unfold Range_iff s_RAG_def, auto) + with th_holdents[unfolded holdents_def] + show False by (unfold eq_holding, auto) + qed + moreover have "Th th \ Domain (RAG s')" + proof + assume "Th th \ Domain (RAG s')" + then obtain cs where "waiting (wq s') th cs" + by (unfold Domain_iff s_RAG_def, auto) + with th_ready show False by (unfold readys_def eq_waiting, auto) + qed + ultimately show ?thesis by (auto simp:Field_def) +qed + +lemma th_tRAG: "(Th th) \ Field (tRAG s')" + using th_RAG tRAG_Field[of s'] by auto + lemma eq_cp: - fixes th' assumes neq_th: "th' \ th" shows "cp s th' = cp s' th'" - apply (unfold cp_eq_cpreced cpreced_def) proof - - have nd: "th \ dependants s th'" - proof - assume "th \ dependants s th'" - hence "(Th th, Th th') \ (RAG s)^+" by (simp add:s_dependants_def eq_RAG) - with eq_dep have "(Th th, Th th') \ (RAG s')^+" by simp - from converse_tranclE[OF this] - obtain cs' where bk: "(Th th, Cs cs') \ RAG s'" - by (auto simp:s_RAG_def) - from step_back_step[OF vt_s[unfolded s_def]] - show False - proof(cases) - assume "th \ runing s'" - with bk show ?thesis - apply (unfold runing_def readys_def s_waiting_def s_RAG_def) - by (auto simp:cs_waiting_def wq_def) + have "(the_preced s \ the_thread) ` subtree (tRAG s) (Th th') = + (the_preced s' \ the_thread) ` subtree (tRAG s') (Th th')" + proof(unfold tRAG_kept, rule f_image_eq) + fix a + assume a_in: "a \ subtree (tRAG s') (Th th')" + then obtain th_a where eq_a: "a = Th th_a" + proof(cases rule:subtreeE) + case 2 + from ancestors_Field[OF 2(2)] + and that show ?thesis by (unfold tRAG_alt_def, auto) + qed auto + have neq_th_a: "th_a \ th" + proof - + from readys_in_no_subtree[OF vat_s'.vt th_ready assms] + have "(Th th) \ subtree (RAG s') (Th th')" . + with tRAG_subtree_RAG[of s' "Th th'"] + have "(Th th) \ subtree (tRAG s') (Th th')" by auto + with a_in[unfolded eq_a] show ?thesis by auto qed + from preced_kept[OF this] + show "(the_preced s \ the_thread) a = (the_preced s' \ the_thread) a" + by (unfold eq_a, simp) qed - have eq_dp: "\ th. dependants (wq s) th = dependants (wq s') th" - by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG) - moreover { - fix th1 - assume "th1 \ {th'} \ dependants (wq s') th'" - hence "th1 = th' \ th1 \ dependants (wq s') th'" by auto - hence "preced th1 s = preced th1 s'" - proof - assume "th1 = th'" - with neq_th - show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def) - next - assume "th1 \ dependants (wq s') th'" - with nd and eq_dp have "th1 \ th" - by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep) - thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def) - qed - } ultimately have "((\th. preced th s) ` ({th'} \ dependants (wq s) th')) = - ((\th. preced th s') ` ({th'} \ dependants (wq s') th'))" - by (auto simp:image_def) - thus "Max ((\th. preced th s) ` ({th'} \ dependants (wq s) th')) = - Max ((\th. preced th s') ` ({th'} \ dependants (wq s') th'))" by simp + thus ?thesis by (unfold cp_alt_def1, simp) qed end + end