# HG changeset patch # User zhangx # Date 1452084374 -28800 # Node ID b620a2a0806ac7e80551db57df2da6a2e7933089 # Parent 031d2ae9c9b8c1ff68da0b0074fa314bc0688732 ExtGG.thy finished, but more comments are needed. diff -r 031d2ae9c9b8 -r b620a2a0806a CpsG.thy --- a/CpsG.thy Tue Dec 22 23:13:31 2015 +0800 +++ b/CpsG.thy Wed Jan 06 20:46:14 2016 +0800 @@ -91,15 +91,17 @@ and "(Cs cs, Th th'') \ RAG s'" shows "tRAG s = tRAG s' \ {(Th th, Th th'')}" (is "?L = ?R") proof - + interpret vt_s': valid_trace "s'" using assms(1) + by (unfold_locales, simp) interpret rtree: rtree "RAG s'" proof show "single_valued (RAG s')" apply (intro_locales) by (unfold single_valued_def, - auto intro:unique_RAG[OF assms(1)]) + auto intro:vt_s'.unique_RAG) show "acyclic (RAG s')" - by (rule acyclic_RAG[OF assms(1)]) + by (rule vt_s'.acyclic_RAG) qed { fix n1 n2 assume "(n1, n2) \ ?L" @@ -152,6 +154,13 @@ } ultimately show ?thesis by auto qed +context valid_trace +begin + +lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt] + +end + lemma cp_alt_def: "cp s th = Max ((the_preced s) ` {th'. Th th' \ (subtree (RAG s) (Th th))})" @@ -221,76 +230,133 @@ } thus ?thesis by auto qed +lemma tRAG_trancl_eq: + "{th'. (Th th', Th th) \ (tRAG s)^+} = + {th'. (Th th', Th th) \ (RAG s)^+}" + (is "?L = ?R") +proof - + { fix th' + assume "th' \ ?L" + hence "(Th th', Th th) \ (tRAG s)^+" by auto + from tranclD[OF this] + obtain z where h: "(Th th', z) \ tRAG s" "(z, Th th) \ (tRAG s)\<^sup>*" by auto + from tRAG_subtree_RAG[of s] and this(2) + have "(z, Th th) \ (RAG s)^*" by (meson subsetCE tRAG_star_RAG) + moreover from h(1) have "(Th th', z) \ (RAG s)^+" using tRAG_alt_def by auto + ultimately have "th' \ ?R" by auto + } moreover + { fix th' + assume "th' \ ?R" + hence "(Th th', Th th) \ (RAG s)^+" by (auto) + from plus_rpath[OF this] + obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \ []" by auto + hence "(Th th', Th th) \ (tRAG s)^+" + proof(induct xs arbitrary:th' th rule:length_induct) + case (1 xs th' th) + then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto) + show ?case + proof(cases "xs1") + case Nil + from 1(2)[unfolded Cons1 Nil] + have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . + hence "(Th th', x1) \ (RAG s)" by (cases, simp) + then obtain cs where "x1 = Cs cs" + by (unfold s_RAG_def, auto) + from rpath_nnl_lastE[OF rp[unfolded this]] + show ?thesis by auto + next + case (Cons x2 xs2) + from 1(2)[unfolded Cons1[unfolded this]] + have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . + from rpath_edges_on[OF this] + have eds: "edges_on (Th th' # x1 # x2 # xs2) \ RAG s" . + have "(Th th', x1) \ edges_on (Th th' # x1 # x2 # xs2)" + by (simp add: edges_on_unfold) + with eds have rg1: "(Th th', x1) \ RAG s" by auto + then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) + have "(x1, x2) \ edges_on (Th th' # x1 # x2 # xs2)" + by (simp add: edges_on_unfold) + from this eds + have rg2: "(x1, x2) \ RAG s" by auto + from this[unfolded eq_x1] + obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) + from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] + have rt1: "(Th th', Th th1) \ tRAG s" by (unfold tRAG_alt_def, auto) + from rp have "rpath (RAG s) x2 xs2 (Th th)" + by (elim rpath_ConsE, simp) + from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . + show ?thesis + proof(cases "xs2 = []") + case True + from rpath_nilE[OF rp'[unfolded this]] + have "th1 = th" by auto + from rt1[unfolded this] show ?thesis by auto + next + case False + from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons] + have "(Th th1, Th th) \ (tRAG s)\<^sup>+" by simp + with rt1 show ?thesis by auto + qed + qed + qed + hence "th' \ ?L" by auto + } ultimately show ?thesis by blast +qed + +lemma tRAG_trancl_eq_Th: + "{Th th' | th'. (Th th', Th th) \ (tRAG s)^+} = + {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" + using tRAG_trancl_eq by auto + +lemma dependants_alt_def: + "dependants s th = {th'. (Th th', Th th) \ (tRAG s)^+}" + by (metis eq_RAG s_dependants_def tRAG_trancl_eq) + +context valid_trace +begin + +lemma count_eq_tRAG_plus: + assumes "cntP s th = cntV s th" + shows "{th'. (Th th', Th th) \ (tRAG s)^+} = {}" + using assms count_eq_dependants dependants_alt_def eq_dependants by auto + +lemma count_eq_RAG_plus: + assumes "cntP s th = cntV s th" + shows "{th'. (Th th', Th th) \ (RAG s)^+} = {}" + using assms count_eq_dependants cs_dependants_def eq_RAG by auto + +lemma count_eq_RAG_plus_Th: + assumes "cntP s th = cntV s th" + shows "{Th th' | th'. (Th th', Th th) \ (RAG s)^+} = {}" + using count_eq_RAG_plus[OF assms] 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)^+} = {}" + using count_eq_tRAG_plus[OF assms] by auto + +end + 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 + { fix n + assume h: "n \ ?L" + hence "n \ ?R" + by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) } moreover { fix n assume "n \ ?R" - then obtain th' where h: "n = Th th'" "(Th th', Th th) \ (RAG s)^*" + 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) - case (1 xs th' th) - show ?case - proof(cases xs) - case Nil - from rpath_nilE[OF 1(2)[unfolded this]] - have "th' = th" by auto - thus ?thesis by (auto simp:subtree_def) - next - case (Cons x1 xs1) note Cons1 = Cons - show ?thesis - proof(cases "xs1") - case Nil - from 1(2)[unfolded Cons[unfolded this]] - have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . - hence "(Th th', x1) \ (RAG s)" by (cases, simp) - then obtain cs where "x1 = Cs cs" - by (unfold s_RAG_def, auto) - from rpath_nnl_lastE[OF rp[unfolded this]] - show ?thesis by auto - next - case (Cons x2 xs2) - from 1(2)[unfolded Cons1[unfolded this]] - have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . - from rpath_edges_on[OF this] - have eds: "edges_on (Th th' # x1 # x2 # xs2) \ RAG s" . - have "(Th th', x1) \ edges_on (Th th' # x1 # x2 # xs2)" - by (simp add: edges_on_unfold) - with eds have rg1: "(Th th', x1) \ RAG s" by auto - then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) - have "(x1, x2) \ edges_on (Th th' # x1 # x2 # xs2)" - by (simp add: edges_on_unfold) - from this eds - have rg2: "(x1, x2) \ RAG s" by auto - from this[unfolded eq_x1] - obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) - from rp have "rpath (RAG s) x2 xs2 (Th th)" - by (elim rpath_ConsE, simp) - from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . - from 1(1)[rule_format, OF _ this, unfolded Cons1 Cons] - have "Th th1 \ subtree (tRAG s) (Th th)" by simp - moreover have "(Th th', Th th1) \ (tRAG s)^*" - proof - - from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] - show ?thesis by (unfold RAG_split tRAG_def wRAG_def hRAG_def, auto) - qed - ultimately show ?thesis by (auto simp:subtree_def) - qed - qed - qed - from this[folded h(1)] - have "n \ ?L" . + from rtranclD[OF this(2)] + have "n \ ?L" + proof + assume "Th th' \ Th th \ (Th th', Th th) \ (RAG s)\<^sup>+" + with h have "n \ {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" by auto + thus ?thesis using subtree_def tRAG_trancl_eq by fastforce + qed (insert h, auto simp:subtree_def) } ultimately show ?thesis by auto qed @@ -325,13 +391,40 @@ by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) qed -locale valid_trace = - fixes s - assumes vt : "vt s" context valid_trace begin +lemma RAG_threads: + assumes "(Th th) \ Field (RAG s)" + shows "th \ threads s" + using assms + by (metis Field_def UnE dm_RAG_threads range_in vt) + +lemma subtree_tRAG_thread: + assumes "th \ threads s" + shows "subtree (tRAG s) (Th th) \ Th ` threads s" (is "?L \ ?R") +proof - + have "?L = {Th th' |th'. Th th' \ subtree (RAG s) (Th th)}" + by (unfold tRAG_subtree_eq, simp) + also have "... \ ?R" + proof + fix x + assume "x \ {Th th' |th'. Th th' \ subtree (RAG s) (Th th)}" + then obtain th' where h: "x = Th th'" "Th th' \ subtree (RAG s) (Th th)" by auto + from this(2) + show "x \ ?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 \ readys s" shows "root (RAG s) (Th th)" @@ -369,19 +462,19 @@ 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 + with dm_RAG_threads and range_in 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)" . + from finite_RAG show "finite (RAG s)" . next - from acyclic_RAG[OF vt] show "acyclic (RAG s)" . + from acyclic_RAG show "acyclic (RAG s)" . qed lemma sgv_wRAG: "single_valued (wRAG s)" - using waiting_unique[OF vt] + using waiting_unique by (unfold single_valued_def wRAG_def, auto) lemma sgv_hRAG: "single_valued (hRAG s)" @@ -394,7 +487,7 @@ lemma acyclic_tRAG: "acyclic (tRAG s)" proof(unfold tRAG_def, rule acyclic_compose) - show "acyclic (RAG s)" using acyclic_RAG[OF vt] . + show "acyclic (RAG s)" using acyclic_RAG . next show "wRAG s \ RAG s" unfolding RAG_split by auto next @@ -402,11 +495,12 @@ qed lemma sgv_RAG: "single_valued (RAG s)" - using unique_RAG[OF vt] by (auto simp:single_valued_def) + using unique_RAG by (auto simp:single_valued_def) lemma rtree_RAG: "rtree (RAG s)" - using sgv_RAG acyclic_RAG[OF vt] + using sgv_RAG acyclic_RAG by (unfold rtree_def rtree_axioms_def sgv_def, auto) + end @@ -415,10 +509,10 @@ show "single_valued (RAG s)" apply (intro_locales) by (unfold single_valued_def, - auto intro:unique_RAG[OF vt]) + auto intro:unique_RAG) show "acyclic (RAG s)" - by (rule acyclic_RAG[OF vt]) + by (rule acyclic_RAG) qed sublocale valid_trace < rtree_s: rtree "tRAG s" @@ -432,7 +526,7 @@ proof - show "fsubtree (RAG s)" proof(intro_locales) - show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG[OF vt]] . + show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] . next show "fsubtree_axioms (RAG s)" proof(unfold fsubtree_axioms_def) @@ -450,13 +544,13 @@ proof(unfold tRAG_def, rule fbranch_compose) show "fbranch (wRAG s)" proof(rule finite_fbranchI) - from finite_RAG[OF vt] show "finite (wRAG s)" + from finite_RAG show "finite (wRAG s)" by (unfold RAG_split, auto) qed next show "fbranch (hRAG s)" proof(rule finite_fbranchI) - from finite_RAG[OF vt] + from finite_RAG show "finite (hRAG s)" by (unfold RAG_split, auto) qed qed @@ -596,16 +690,18 @@ by (unfold cs_holding_def, auto) qed +context valid_trace +begin + lemma next_th_waiting: - assumes vt: "vt s" - and nxt: "next_th s th cs th'" + 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 \ []" "th' = hd (SOME q. distinct q \ set q = set rest)" by auto - from wq_distinct[OF vt, of cs, unfolded h] + from wq_distinct[of cs, unfolded h] have dst: "distinct (th # rest)" . have in_rest: "th' \ set rest" proof(unfold h, rule someI2) @@ -622,11 +718,12 @@ qed lemma next_th_RAG: - assumes vt: "vt s" - and nxt: "next_th s th cs th'" + assumes nxt: "next_th (s::event list) th cs th'" shows "{(Cs cs, Th th), (Th th', Cs cs)} \ RAG s" - using assms next_th_holding next_th_waiting -by (unfold s_RAG_def, simp) + using vt assms next_th_holding next_th_waiting + by (unfold s_RAG_def, simp) + +end -- {* A useless definition *} definition cps:: "state \ (thread \ precedence) set" @@ -909,7 +1006,7 @@ *) lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \ RAG s'" - using next_th_RAG[OF vat_s'.vt nt] . + using next_th_RAG[OF nt] . lemma ancestors_th': "ancestors (RAG s') (Th th') = {Th th, Cs cs}" @@ -1175,7 +1272,7 @@ lemma tRAG_s: "tRAG s = tRAG s' \ {(Th th, Th th')}" - using RAG_tRAG_transfer[OF step_back_vt[OF vt_s[unfolded s_def]] RAG_s cs_held] . + using RAG_tRAG_transfer[OF RAG_s cs_held] . lemma cp_kept: assumes "Th th'' \ ancestors (tRAG s) (Th th)" diff -r 031d2ae9c9b8 -r b620a2a0806a CpsG.thy~ --- a/CpsG.thy~ Tue Dec 22 23:13:31 2015 +0800 +++ b/CpsG.thy~ Wed Jan 06 20:46:14 2016 +0800 @@ -10,6 +10,10 @@ difference is the order of arguemts. *} definition "the_preced s th = preced th s" +lemma inj_the_preced: + "inj_on (the_preced s) (threads s)" + by (metis inj_onI preced_unique the_preced_def) + text {* @{term "the_thread"} extracts thread out of RAG node. *} fun the_thread :: "node \ thread" where "the_thread (Th th) = th" @@ -87,15 +91,17 @@ and "(Cs cs, Th th'') \ RAG s'" shows "tRAG s = tRAG s' \ {(Th th, Th th'')}" (is "?L = ?R") proof - + interpret vt_s': valid_trace "s'" using assms(1) + by (unfold_locales, simp) interpret rtree: rtree "RAG s'" proof show "single_valued (RAG s')" apply (intro_locales) by (unfold single_valued_def, - auto intro:unique_RAG[OF assms(1)]) + auto intro:vt_s'.unique_RAG) show "acyclic (RAG s')" - by (rule acyclic_RAG[OF assms(1)]) + by (rule vt_s'.acyclic_RAG) qed { fix n1 n2 assume "(n1, n2) \ ?L" @@ -148,6 +154,13 @@ } ultimately show ?thesis by auto qed +context valid_trace +begin + +lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt] + +end + lemma cp_alt_def: "cp s th = Max ((the_preced s) ` {th'. Th th' \ (subtree (RAG s) (Th th))})" @@ -217,76 +230,133 @@ } thus ?thesis by auto qed +lemma tRAG_trancl_eq: + "{th'. (Th th', Th th) \ (tRAG s)^+} = + {th'. (Th th', Th th) \ (RAG s)^+}" + (is "?L = ?R") +proof - + { fix th' + assume "th' \ ?L" + hence "(Th th', Th th) \ (tRAG s)^+" by auto + from tranclD[OF this] + obtain z where h: "(Th th', z) \ tRAG s" "(z, Th th) \ (tRAG s)\<^sup>*" by auto + from tRAG_subtree_RAG[of s] and this(2) + have "(z, Th th) \ (RAG s)^*" by (meson subsetCE tRAG_star_RAG) + moreover from h(1) have "(Th th', z) \ (RAG s)^+" using tRAG_alt_def by auto + ultimately have "th' \ ?R" by auto + } moreover + { fix th' + assume "th' \ ?R" + hence "(Th th', Th th) \ (RAG s)^+" by (auto) + from plus_rpath[OF this] + obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \ []" by auto + hence "(Th th', Th th) \ (tRAG s)^+" + proof(induct xs arbitrary:th' th rule:length_induct) + case (1 xs th' th) + then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto) + show ?case + proof(cases "xs1") + case Nil + from 1(2)[unfolded Cons1 Nil] + have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . + hence "(Th th', x1) \ (RAG s)" by (cases, simp) + then obtain cs where "x1 = Cs cs" + by (unfold s_RAG_def, auto) + from rpath_nnl_lastE[OF rp[unfolded this]] + show ?thesis by auto + next + case (Cons x2 xs2) + from 1(2)[unfolded Cons1[unfolded this]] + have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . + from rpath_edges_on[OF this] + have eds: "edges_on (Th th' # x1 # x2 # xs2) \ RAG s" . + have "(Th th', x1) \ edges_on (Th th' # x1 # x2 # xs2)" + by (simp add: edges_on_unfold) + with eds have rg1: "(Th th', x1) \ RAG s" by auto + then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) + have "(x1, x2) \ edges_on (Th th' # x1 # x2 # xs2)" + by (simp add: edges_on_unfold) + from this eds + have rg2: "(x1, x2) \ RAG s" by auto + from this[unfolded eq_x1] + obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) + from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] + have rt1: "(Th th', Th th1) \ tRAG s" by (unfold tRAG_alt_def, auto) + from rp have "rpath (RAG s) x2 xs2 (Th th)" + by (elim rpath_ConsE, simp) + from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . + show ?thesis + proof(cases "xs2 = []") + case True + from rpath_nilE[OF rp'[unfolded this]] + have "th1 = th" by auto + from rt1[unfolded this] show ?thesis by auto + next + case False + from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons] + have "(Th th1, Th th) \ (tRAG s)\<^sup>+" by simp + with rt1 show ?thesis by auto + qed + qed + qed + hence "th' \ ?L" by auto + } ultimately show ?thesis by blast +qed + +lemma tRAG_trancl_eq_Th: + "{Th th' | th'. (Th th', Th th) \ (tRAG s)^+} = + {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" + using tRAG_trancl_eq by auto + +lemma dependants_alt_def: + "dependants s th = {th'. (Th th', Th th) \ (tRAG s)^+}" + by (metis eq_RAG s_dependants_def tRAG_trancl_eq) + +context valid_trace +begin + +lemma count_eq_tRAG_plus: + assumes "cntP s th = cntV s th" + shows "{th'. (Th th', Th th) \ (tRAG s)^+} = {}" + using assms count_eq_dependants dependants_alt_def eq_dependants by auto + +lemma count_eq_RAG_plus: + assumes "cntP s th = cntV s th" + shows "{th'. (Th th', Th th) \ (RAG s)^+} = {}" + using assms count_eq_dependants cs_dependants_def eq_RAG by auto + +lemma count_eq_RAG_plus_Th: + assumes "cntP s th = cntV s th" + shows "{Th th' | th'. (Th th', Th th) \ (RAG s)^+} = {}" + using count_eq_RAG_plus[OF assms] 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)^+} = {}" + using count_eq_tRAG_plus[OF assms] by auto + +end + 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 + { fix n + assume h: "n \ ?L" + hence "n \ ?R" + by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) } moreover { fix n assume "n \ ?R" - then obtain th' where h: "n = Th th'" "(Th th', Th th) \ (RAG s)^*" + 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) - case (1 xs th' th) - show ?case - proof(cases xs) - case Nil - from rpath_nilE[OF 1(2)[unfolded this]] - have "th' = th" by auto - thus ?thesis by (auto simp:subtree_def) - next - case (Cons x1 xs1) note Cons1 = Cons - show ?thesis - proof(cases "xs1") - case Nil - from 1(2)[unfolded Cons[unfolded this]] - have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . - hence "(Th th', x1) \ (RAG s)" by (cases, simp) - then obtain cs where "x1 = Cs cs" - by (unfold s_RAG_def, auto) - from rpath_nnl_lastE[OF rp[unfolded this]] - show ?thesis by auto - next - case (Cons x2 xs2) - from 1(2)[unfolded Cons1[unfolded this]] - have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . - from rpath_edges_on[OF this] - have eds: "edges_on (Th th' # x1 # x2 # xs2) \ RAG s" . - have "(Th th', x1) \ edges_on (Th th' # x1 # x2 # xs2)" - by (simp add: edges_on_unfold) - with eds have rg1: "(Th th', x1) \ RAG s" by auto - then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) - have "(x1, x2) \ edges_on (Th th' # x1 # x2 # xs2)" - by (simp add: edges_on_unfold) - from this eds - have rg2: "(x1, x2) \ RAG s" by auto - from this[unfolded eq_x1] - obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) - from rp have "rpath (RAG s) x2 xs2 (Th th)" - by (elim rpath_ConsE, simp) - from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . - from 1(1)[rule_format, OF _ this, unfolded Cons1 Cons] - have "Th th1 \ subtree (tRAG s) (Th th)" by simp - moreover have "(Th th', Th th1) \ (tRAG s)^*" - proof - - from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] - show ?thesis by (unfold RAG_split tRAG_def wRAG_def hRAG_def, auto) - qed - ultimately show ?thesis by (auto simp:subtree_def) - qed - qed - qed - from this[folded h(1)] - have "n \ ?L" . + from rtranclD[OF this(2)] + have "n \ ?L" + proof + assume "Th th' \ Th th \ (Th th', Th th) \ (RAG s)\<^sup>+" + with h have "n \ {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" by auto + thus ?thesis using subtree_def tRAG_trancl_eq by fastforce + qed (insert h, auto simp:subtree_def) } ultimately show ?thesis by auto qed @@ -321,13 +391,17 @@ by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) qed -locale valid_trace = - fixes s - assumes vt : "vt s" context valid_trace begin +lemma RAG_threads: + assumes "(Th th) \ Field (RAG s)" + shows "th \ threads s" + using assms + by (metis Field_def UnE dm_RAG_threads range_in vt) + + lemma readys_root: assumes "th \ readys s" shows "root (RAG s) (Th th)" @@ -365,19 +439,19 @@ 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 + with dm_RAG_threads and range_in 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)" . + from finite_RAG show "finite (RAG s)" . next - from acyclic_RAG[OF vt] show "acyclic (RAG s)" . + from acyclic_RAG show "acyclic (RAG s)" . qed lemma sgv_wRAG: "single_valued (wRAG s)" - using waiting_unique[OF vt] + using waiting_unique by (unfold single_valued_def wRAG_def, auto) lemma sgv_hRAG: "single_valued (hRAG s)" @@ -390,7 +464,7 @@ lemma acyclic_tRAG: "acyclic (tRAG s)" proof(unfold tRAG_def, rule acyclic_compose) - show "acyclic (RAG s)" using acyclic_RAG[OF vt] . + show "acyclic (RAG s)" using acyclic_RAG . next show "wRAG s \ RAG s" unfolding RAG_split by auto next @@ -398,11 +472,12 @@ qed lemma sgv_RAG: "single_valued (RAG s)" - using unique_RAG[OF vt] by (auto simp:single_valued_def) + using unique_RAG by (auto simp:single_valued_def) lemma rtree_RAG: "rtree (RAG s)" - using sgv_RAG acyclic_RAG[OF vt] + using sgv_RAG acyclic_RAG by (unfold rtree_def rtree_axioms_def sgv_def, auto) + end @@ -411,10 +486,10 @@ show "single_valued (RAG s)" apply (intro_locales) by (unfold single_valued_def, - auto intro:unique_RAG[OF vt]) + auto intro:unique_RAG) show "acyclic (RAG s)" - by (rule acyclic_RAG[OF vt]) + by (rule acyclic_RAG) qed sublocale valid_trace < rtree_s: rtree "tRAG s" @@ -428,7 +503,7 @@ proof - show "fsubtree (RAG s)" proof(intro_locales) - show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG[OF vt]] . + show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] . next show "fsubtree_axioms (RAG s)" proof(unfold fsubtree_axioms_def) @@ -446,13 +521,13 @@ proof(unfold tRAG_def, rule fbranch_compose) show "fbranch (wRAG s)" proof(rule finite_fbranchI) - from finite_RAG[OF vt] show "finite (wRAG s)" + from finite_RAG show "finite (wRAG s)" by (unfold RAG_split, auto) qed next show "fbranch (hRAG s)" proof(rule finite_fbranchI) - from finite_RAG[OF vt] + from finite_RAG show "finite (hRAG s)" by (unfold RAG_split, auto) qed qed @@ -592,16 +667,18 @@ by (unfold cs_holding_def, auto) qed +context valid_trace +begin + lemma next_th_waiting: - assumes vt: "vt s" - and nxt: "next_th s th cs th'" + 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 \ []" "th' = hd (SOME q. distinct q \ set q = set rest)" by auto - from wq_distinct[OF vt, of cs, unfolded h] + from wq_distinct[of cs, unfolded h] have dst: "distinct (th # rest)" . have in_rest: "th' \ set rest" proof(unfold h, rule someI2) @@ -618,11 +695,12 @@ qed lemma next_th_RAG: - assumes vt: "vt s" - and nxt: "next_th s th cs th'" + assumes nxt: "next_th (s::event list) th cs th'" shows "{(Cs cs, Th th), (Th th', Cs cs)} \ RAG s" - using assms next_th_holding next_th_waiting -by (unfold s_RAG_def, simp) + using vt assms next_th_holding next_th_waiting + by (unfold s_RAG_def, simp) + +end -- {* A useless definition *} definition cps:: "state \ (thread \ precedence) set" @@ -905,7 +983,7 @@ *) lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \ RAG s'" - using next_th_RAG[OF vat_s'.vt nt] . + using next_th_RAG[OF nt] . lemma ancestors_th': "ancestors (RAG s') (Th th') = {Th th, Cs cs}" @@ -1171,7 +1249,7 @@ lemma tRAG_s: "tRAG s = tRAG s' \ {(Th th, Th th')}" - using RAG_tRAG_transfer[OF step_back_vt[OF vt_s[unfolded s_def]] RAG_s cs_held] . + using RAG_tRAG_transfer[OF RAG_s cs_held] . lemma cp_kept: assumes "Th th'' \ ancestors (tRAG s) (Th th)" diff -r 031d2ae9c9b8 -r b620a2a0806a ExtGG.thy --- a/ExtGG.thy Tue Dec 22 23:13:31 2015 +0800 +++ b/ExtGG.thy Wed Jan 06 20:46:14 2016 +0800 @@ -2,67 +2,93 @@ imports PrioG CpsG begin -lemma birth_time_lt: "s \ [] \ last_set th s < length s" - apply (induct s, simp) -proof - - fix a s - assume ih: "s \ [] \ last_set th s < length s" - and eq_as: "a # s \ []" - show "last_set th (a # s) < length (a # s)" - proof(cases "s \ []") - case False - from False show ?thesis - by (cases a, auto simp:last_set.simps) - next - case True - from ih [OF True] show ?thesis - by (cases a, auto simp:last_set.simps) - qed +text {* + The following two auxiliary lemmas are used to reason about @{term Max}. +*} +lemma image_Max_eqI: + assumes "finite B" + and "b \ B" + and "\ x \ B. f x \ f b" + shows "Max (f ` B) = f b" + using assms + using Max_eqI by blast + +lemma image_Max_subset: + assumes "finite A" + and "B \ A" + and "a \ B" + and "Max (f ` A) = f a" + shows "Max (f ` B) = f a" +proof(rule image_Max_eqI) + show "finite B" + using assms(1) assms(2) finite_subset by auto +next + show "a \ B" using assms by simp +next + show "\x\B. f x \ f a" + by (metis Max_ge assms(1) assms(2) assms(4) + finite_imageI image_eqI subsetCE) qed -lemma th_in_ne: "th \ threads s \ s \ []" - by (induct s, auto simp:threads.simps) - -lemma preced_tm_lt: "th \ threads s \ preced th s = Prc x y \ y < length s" - apply (drule_tac th_in_ne) - by (unfold preced_def, auto intro: birth_time_lt) - +text {* + The following locale @{text "highest_gen"} sets the basic context for our + investigation: supposing thread @{text th} holds the highest @{term cp}-value + in state @{text s}, which means the task for @{text th} is the + most urgent. We want to show that + @{text th} is treated correctly by PIP, which means + @{text th} will not be blocked unreasonably by other less urgent + threads. +*} locale highest_gen = fixes s th prio tm assumes vt_s: "vt s" and threads_s: "th \ threads s" and highest: "preced th s = Max ((cp s)`threads s)" - and preced_th: "preced th s = Prc prio tm" + -- {* The internal structure of @{term th}'s precedence is exposed:*} + and preced_th: "preced th s = Prc prio tm" +-- {* @{term s} is a valid trace, so it will inherit all results derived for + a valid trace: *} sublocale highest_gen < vat_s: valid_trace "s" by (unfold_locales, insert vt_s, simp) context highest_gen begin +text {* + @{term tm} is the time when the precedence of @{term th} is set, so + @{term tm} must be a valid moment index into @{term s}. +*} lemma lt_tm: "tm < length s" by (insert preced_tm_lt[OF threads_s preced_th], simp) +text {* + Since @{term th} holds the highest precedence and @{text "cp"} + is the highest precedence of all threads in the sub-tree of + @{text "th"} and @{text th} is among these threads, + its @{term cp} must equal to its precedence: +*} lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R") proof - have "?L \ ?R" by (unfold highest, rule Max_ge, - auto simp:threads_s finite_threads[OF vt_s]) + auto simp:threads_s finite_threads) moreover have "?R \ ?L" by (unfold vat_s.cp_rec, rule Max_ge, auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) ultimately show ?thesis by auto qed +(* ccc *) lemma highest_cp_preced: "cp s th = Max ((\ th'. preced th' s) ` threads s)" - by (fold max_cp_eq[OF vt_s], unfold eq_cp_s_th, insert highest, simp) + by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp) lemma highest_preced_thread: "preced th s = Max ((\ th'. preced th' s) ` threads s)" by (fold eq_cp_s_th, unfold highest_cp_preced, simp) lemma highest': "cp s th = Max (cp s ` threads s)" proof - - from highest_cp_preced max_cp_eq[OF vt_s, symmetric] + from highest_cp_preced max_cp_eq[symmetric] show ?thesis by simp qed @@ -75,6 +101,9 @@ and set_diff_low: "Set th' prio' \ set t \ th' \ th \ prio' \ prio" and exit_diff: "Exit th' \ set t \ th' \ th" +sublocale extend_highest_gen < vat_t: valid_trace "t@s" + by (unfold_locales, insert vt_t, simp) + lemma step_back_vt_app: assumes vt_ts: "vt (t@s)" shows "vt s" @@ -110,14 +139,6 @@ context extend_highest_gen begin -(* - lemma red_moment: - "extend_highest_gen s th prio tm (moment i t)" - apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) - apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) - by (unfold highest_gen_def, auto dest:step_back_vt_app) -*) - lemma ind [consumes 0, case_names Nil Cons, induct type]: assumes h0: "R []" @@ -218,48 +239,21 @@ qed qed -lemma Max_remove_less: - assumes "finite A" - and "a \ A" - and "b \ A" - and "a \ b" - and "inj_on f A" - and "f a = Max (f ` A)" - shows "Max (f ` (A - {b})) = (Max (f ` A))" -proof - - have "Max (f ` (A - {b})) = Max (f`A - {f b})" - proof - - have "f ` (A - {b}) = f ` A - f ` {b}" - by (rule inj_on_image_set_diff[OF assms(5)], insert assms(3), auto) - thus ?thesis by simp - qed - also have "... = - (if f ` A - {f b} - {f a} = {} then f a else max (f a) (Max (f ` A - {f b} - {f a})))" - proof(subst Max.remove) - from assms show "f a \ f ` A - {f b}" - by (meson DiffI empty_iff imageI inj_on_eq_iff insert_iff) - next - from assms(1) show "finite (f ` A - {f b})" by auto - qed auto - also have "... = Max (f ` A)" (is "?L = ?R") - proof(cases "f ` A - {f b} - {f a} = {}") - case True - with assms show ?thesis by auto - next - case False - hence "?L = max (f a) (Max (f ` A - {f b} - {f a}))" - by simp - also have "... = ?R" - proof - - from assms False - have "(Max (f ` A - {f b} - {f a})) \ f a" by auto - thus ?thesis by (simp add: assms(6) max_def) - qed - finally show ?thesis . - qed - finally show ?thesis . -qed +text {* + According to @{thm th_kept}, thread @{text "th"} has its living status + and precedence kept along the way of @{text "t"}. The following lemma + shows that this preserved precedence of @{text "th"} remains as the highest + along the way of @{text "t"}. + The proof goes by induction over @{text "t"} using the specialized + induction rule @{thm ind}, followed by case analysis of each possible + operations of PIP. All cases follow the same pattern rendered by the + generalized introduction rule @{thm "image_Max_eqI"}. + + The very essence is to show that precedences, no matter whether they are newly introduced + or modified, are always lower than the one held by @{term "th"}, + which by @{thm th_kept} is preserved along the way. +*} lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" proof(induct rule:ind) case Nil @@ -273,62 +267,74 @@ show ?case proof(cases e) case (Create thread prio') - from Cons(2)[unfolded this] - have thread_not_in: "thread \ threads (t@s)" by (cases, simp) show ?thesis (is "Max (?f ` ?A) = ?t") proof - - have "Max (?f ` ?A) = Max (insert (?f thread) (?f ` (threads (t@s))))" - by (unfold Create, simp) - moreover have "\ = max (?f thread) (Max (?f ` (threads (t@s))))" - proof(rule Max.insert) - from finite_threads[OF Cons(1)] - show "finite (?f ` (threads (t@s)))" by simp - qed (insert h_t.th_kept, auto) - moreover have "(Max (?f ` (threads (t@s)))) = ?t" - proof - - have "(\th'. preced th' ((e # t) @ s)) ` threads (t @ s) = - (\th'. preced th' (t @ s)) ` threads (t @ s)" - by (intro f_image_eq, insert thread_not_in, auto simp:Create preced_def) - with Cons show ?thesis by (auto simp:the_preced_def) + -- {* The following is the common pattern of each branch of the case analysis. *} + -- {* The major part is to show that @{text "th"} holds the highest precedence: *} + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto + next + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume "x \ ?A" + hence "x = thread \ x \ threads (t@s)" by (auto simp:Create) + thus "?f x \ ?f th" + proof + assume "x = thread" + thus ?thesis + apply (simp add:Create the_preced_def preced_def, fold preced_def) + using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force + next + assume h: "x \ threads (t @ s)" + from Cons(2)[unfolded Create] + have "x \ thread" using h by (cases, auto) + hence "?f x = the_preced (t@s) x" + by (simp add:Create the_preced_def preced_def) + hence "?f x \ Max (the_preced (t@s) ` threads (t@s))" + by (simp add: h_t.finite_threads h) + also have "... = ?f th" + by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + finally show ?thesis . + qed + qed qed - moreover have "?f thread < ?t" - proof - - from h_e.create_low and Create - have "prio' \ prio" by auto - thus ?thesis - by (unfold preced_th, unfold Create, insert lt_tm, - auto simp:preced_def precedence_less_def preced_th the_preced_def) - qed - ultimately show ?thesis by (auto simp:max_def) - qed + -- {* The minor part is to show that the precedence of @{text "th"} + equals to preserved one, given by the foregoing lemma @{thm th_kept} *} + also have "... = ?t" using h_e.th_kept the_preced_def by auto + -- {* Then it follows trivially that the precedence preserved + for @{term "th"} remains the maximum of all living threads along the way. *} + finally show ?thesis . + qed next case (Exit thread) - show ?thesis + show ?thesis (is "Max (?f ` ?A) = ?t") proof - - have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = - Max (the_preced (t @ s) ` (threads (t @ s)))" - proof(rule Max_remove_less) - show "th \ thread" using Exit h_e.exit_diff by auto + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto next - from Cons(2)[unfolded Exit] - show "thread \ threads (t @ s)" - by (cases, simp add: readys_def runing_def) - next - show "finite (threads (t @ s))" by (simp add: finite_threads h_t.vt_t) + show "th \ ?A" using h_e.th_kept by auto next - show "th \ threads (t @ s)" by (simp add: h_t.th_kept) - next - show "inj_on (the_preced (t @ s)) (threads (t @ s))" by (simp add: inj_the_preced) - next - show "the_preced (t @ s) th = Max (the_preced (t @ s) ` threads (t @ s))" - by (simp add: Cons.hyps(5) h_t.th_kept the_preced_def) + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume "x \ ?A" + hence "x \ threads (t@s)" by (simp add: Exit) + hence "?f x \ Max (?f ` threads (t@s))" + by (simp add: h_t.finite_threads) + also have "... \ ?f th" + apply (simp add:Exit the_preced_def preced_def, fold preced_def) + using Cons.hyps(5) h_t.th_kept the_preced_def by auto + finally show "?f x \ ?f th" . + qed qed - from this[unfolded Cons(5)] - have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = preced th s" . - moreover have "the_preced ((e # t) @ s) = the_preced (t@s)" - by (auto simp:Exit the_preced_def preced_def) - ultimately show ?thesis by (simp add:Exit) - qed + also have "... = ?t" using h_e.th_kept the_preced_def by auto + finally show ?thesis . + qed next case (P thread cs) with Cons @@ -337,202 +343,158 @@ case (V thread cs) with Cons show ?thesis by (auto simp:preced_def the_preced_def) - next (* ccc *) + next case (Set thread prio') - show ?thesis - apply (unfold Set, simp, insert Cons(5)) (* ccc *) - find_theorems priority Set - find_theorems preced Set + show ?thesis (is "Max (?f ` ?A) = ?t") proof - - let ?B = "threads (t@s)" - from Cons have "extend_highest_gen s th prio tm (e # t)" by auto - from extend_highest_gen.set_diff_low[OF this] and Set - have neq_thread: "thread \ th" and le_p: "prio' \ prio" by auto - from Set have "Max (?f ` ?A) = Max (?f ` ?B)" by simp - also have "\ = ?t" - proof(rule Max_eqI) - fix y - assume y_in: "y \ ?f ` ?B" - then obtain th1 where - th1_in: "th1 \ ?B" and eq_y: "y = ?f th1" by auto - show "y \ ?t" - proof(cases "th1 = thread") - case True - with neq_thread le_p eq_y Set - show ?thesis - apply (subst preced_th, insert lt_tm) - by (auto simp:preced_def precedence_le_def) - next - case False - with Set eq_y - have "y = preced th1 (t@s)" - by (simp add:preced_def) - moreover have "\ \ ?t" - proof - - from Cons - have "?t = Max ((\ th'. preced th' (t@s)) ` (threads (t@s)))" - by auto - moreover have "preced th1 (t@s) \ \" - proof(rule Max_ge) - from th1_in - show "preced th1 (t @ s) \ (\th'. preced th' (t @ s)) ` threads (t @ s)" - by simp - next - show "finite ((\th'. preced th' (t @ s)) ` threads (t @ s))" - proof - - from Cons have "vt (t @ s)" by auto - from finite_threads[OF this] show ?thesis by auto - qed + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto + next + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume h: "x \ ?A" + show "?f x \ ?f th" + proof(cases "x = thread") + case True + moreover have "the_preced (Set thread prio' # t @ s) thread \ the_preced (t @ s) th" + proof - + have "the_preced (t @ s) th = Prc prio tm" + using h_t.th_kept preced_th by (simp add:the_preced_def) + moreover have "prio' \ prio" using Set h_e.set_diff_low by auto + ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def) qed - ultimately show ?thesis by auto + ultimately show ?thesis + by (unfold Set, simp add:the_preced_def preced_def) + next + case False + then have "?f x = the_preced (t@s) x" + by (simp add:the_preced_def preced_def Set) + also have "... \ Max (the_preced (t@s) ` threads (t@s))" + using Set h h_t.finite_threads by auto + also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + finally show ?thesis . qed - ultimately show ?thesis by auto - qed - next - from Cons and finite_threads - show "finite (?f ` ?B)" by auto - next - from Cons have "extend_highest_gen s th prio tm t" by auto - from extend_highest_gen.th_kept [OF this] - have h: "th \ threads (t @ s) \ preced th (t @ s) = preced th s" . - show "?t \ (?f ` ?B)" - proof - - from neq_thread Set h - have "?t = ?f th" by (auto simp:preced_def) - with h show ?thesis by auto qed qed + also have "... = ?t" using h_e.th_kept the_preced_def by auto finally show ?thesis . - qed + qed qed qed -lemma max_preced: "preced th (t@s) = Max ((\ th'. preced th' (t @ s)) ` (threads (t@s)))" +lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))" by (insert th_kept max_kept, auto) -lemma th_cp_max_preced: "cp (t@s) th = Max ((\ th'. preced th' (t @ s)) ` (threads (t@s)))" - (is "?L = ?R") +text {* + The reason behind the following lemma is that: + Since @{term "cp"} is defined as the maximum precedence + of those threads contained in the sub-tree of node @{term "Th th"} + in @{term "RAG (t@s)"}, and all these threads are living threads, and + @{term "th"} is also among them, the maximum precedence of + them all must be the one for @{text "th"}. +*} +lemma th_cp_max_preced: + "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R") proof - - have "?L = cpreced (wq (t@s)) (t@s) th" - by (unfold cp_eq_cpreced, simp) - also have "\ = ?R" - proof(unfold cpreced_def) - show "Max ((\th. preced th (t @ s)) ` ({th} \ dependants (wq (t @ s)) th)) = - Max ((\th'. preced th' (t @ s)) ` threads (t @ s))" - (is "Max (?f ` ({th} \ ?A)) = Max (?f ` ?B)") - proof(cases "?A = {}") - case False - have "Max (?f ` ({th} \ ?A)) = Max (insert (?f th) (?f ` ?A))" by simp - moreover have "\ = max (?f th) (Max (?f ` ?A))" - proof(rule Max_insert) - show "finite (?f ` ?A)" - proof - - from dependants_threads[OF vt_t] - have "?A \ threads (t@s)" . - moreover from finite_threads[OF vt_t] have "finite \" . - ultimately show ?thesis - by (auto simp:finite_subset) - qed + let ?f = "the_preced (t@s)" + have "?L = ?f th" + proof(unfold cp_alt_def, rule image_Max_eqI) + show "finite {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + proof - + have "{th'. Th th' \ subtree (RAG (t @ s)) (Th th)} = + the_thread ` {n . n \ subtree (RAG (t @ s)) (Th th) \ + (\ th'. n = Th th')}" + by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps) + moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) + ultimately show ?thesis by simp + qed + next + show "th \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + by (auto simp:subtree_def) + next + show "\x\{th'. Th th' \ subtree (RAG (t @ s)) (Th th)}. + the_preced (t @ s) x \ the_preced (t @ s) th" + proof + fix th' + assume "th' \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + hence "Th th' \ subtree (RAG (t @ s)) (Th th)" by auto + moreover have "... \ Field (RAG (t @ s)) \ {Th th}" + by (meson subtree_Field) + ultimately have "Th th' \ ..." by auto + hence "th' \ threads (t@s)" + proof + assume "Th th' \ {Th th}" + thus ?thesis using th_kept by auto next - from False show "(?f ` ?A) \ {}" by simp + assume "Th th' \ Field (RAG (t @ s))" + thus ?thesis using vat_t.not_in_thread_isolated by blast qed - moreover have "\ = Max (?f ` ?B)" - proof - - from max_preced have "?f th = Max (?f ` ?B)" . - moreover have "Max (?f ` ?A) \ \" - proof(rule Max_mono) - from False show "(?f ` ?A) \ {}" by simp - next - show "?f ` ?A \ ?f ` ?B" - proof - - have "?A \ ?B" by (rule dependants_threads[OF vt_t]) - thus ?thesis by auto - qed - next - from finite_threads[OF vt_t] - show "finite (?f ` ?B)" by simp - qed - ultimately show ?thesis - by (auto simp:max_def) - qed - ultimately show ?thesis by auto - next - case True - with max_preced show ?thesis by auto + thus "the_preced (t @ s) th' \ the_preced (t @ s) th" + by (metis Max_ge finite_imageI finite_threads image_eqI + max_kept th_kept the_preced_def) qed qed + also have "... = ?R" by (simp add: max_preced the_preced_def) finally show ?thesis . qed lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))" - by (unfold max_cp_eq[OF vt_t] th_cp_max_preced, simp) + using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger lemma th_cp_preced: "cp (t@s) th = preced th s" by (fold max_kept, unfold th_cp_max_preced, simp) lemma preced_less: - fixes th' assumes th'_in: "th' \ threads s" and neq_th': "th' \ th" shows "preced th' s < preced th s" -proof - - have "preced th' s \ Max ((\th'. preced th' s) ` threads s)" - proof(rule Max_ge) - from finite_threads [OF vt_s] - show "finite ((\th'. preced th' s) ` threads s)" by simp - next - from th'_in show "preced th' s \ (\th'. preced th' s) ` threads s" - by simp - qed - moreover have "preced th' s \ preced th s" - proof - assume "preced th' s = preced th s" - from preced_unique[OF this th'_in] neq_th' threads_s - show "False" by (auto simp:readys_def) - qed - ultimately show ?thesis using highest_preced_thread - by auto -qed + using assms +by (metis Max.coboundedI finite_imageI highest not_le order.trans + preced_linorder rev_image_eqI threads_s vat_s.finite_threads + vat_s.le_cp) + +text {* + Counting of the number of @{term "P"} and @{term "V"} operations + is the cornerstone of a large number of the following proofs. + The reason is that this counting is quite easy to calculate and + convenient to use in the reasoning. + + The following lemma shows that the counting controls whether + a thread is running or not. +*} lemma pv_blocked_pre: - fixes th' assumes th'_in: "th' \ threads (t@s)" and neq_th': "th' \ th" and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" shows "th' \ runing (t@s)" proof - assume "th' \ runing (t@s)" - hence "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" - by (auto simp:runing_def) - with max_cp_readys_threads [OF vt_t] - have "cp (t @ s) th' = Max (cp (t@s) ` threads (t@s))" - by auto - moreover from th_cp_max have "cp (t @ s) th = \" by simp - ultimately have "cp (t @ s) th' = cp (t @ s) th" by simp - moreover from th_cp_preced and th_kept have "\ = preced th (t @ s)" - by simp - finally have h: "cp (t @ s) th' = preced th (t @ s)" . + assume otherwise: "th' \ runing (t@s)" show False proof - - have "dependants (wq (t @ s)) th' = {}" - by (rule count_eq_dependants [OF vt_t eq_pv]) - moreover have "preced th' (t @ s) \ preced th (t @ s)" - proof - assume "preced th' (t @ s) = preced th (t @ s)" - hence "th' = th" - proof(rule preced_unique) - from th_kept show "th \ threads (t @ s)" by simp - next - from th'_in show "th' \ threads (t @ s)" by simp + have "th' = th" + proof(rule preced_unique) + show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") + proof - + have "?L = cp (t@s) th'" + by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) + also have "... = cp (t @ s) th" using otherwise + by (metis (mono_tags, lifting) mem_Collect_eq + runing_def th_cp_max vat_t.max_cp_readys_threads) + also have "... = ?R" by (metis th_cp_preced th_kept) + finally show ?thesis . qed - with assms show False by simp - qed - ultimately show ?thesis - by (insert h, unfold cp_eq_cpreced cpreced_def, simp) - qed + qed (auto simp: th'_in th_kept) + moreover have "th' \ th" using neq_th' . + ultimately show ?thesis by simp + qed qed -lemmas pv_blocked = pv_blocked_pre[folded detached_eq [OF vt_t]] +lemmas pv_blocked = pv_blocked_pre[folded detached_eq] lemma runing_precond_pre: fixes th' @@ -541,113 +503,102 @@ and neq_th': "th' \ th" shows "th' \ threads (t@s) \ cntP (t@s) th' = cntV (t@s) th'" -proof - - show ?thesis - proof(induct rule:ind) - case (Cons e t) - from Cons - have in_thread: "th' \ threads (t @ s)" - and not_holding: "cntP (t @ s) th' = cntV (t @ s) th'" by auto - from Cons have "extend_highest_gen s th prio tm t" by auto - then have not_runing: "th' \ runing (t @ s)" - apply(rule extend_highest_gen.pv_blocked) - using Cons(1) in_thread neq_th' not_holding - apply(simp_all add: detached_eq) - done +proof(induct rule:ind) + case (Cons e t) + interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp + interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp show ?case proof(cases e) - case (V thread cs) - from Cons and V have vt_v: "vt (V thread cs#(t@s))" by auto - + case (P thread cs) show ?thesis proof - - from Cons and V have "step (t@s) (V thread cs)" by auto - hence neq_th': "thread \ th'" - proof(cases) - assume "thread \ runing (t@s)" - moreover have "th' \ runing (t@s)" by fact - ultimately show ?thesis by auto + have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" + proof - + have "thread \ th'" + proof - + have "step (t@s) (P thread cs)" using Cons P by auto + thus ?thesis + proof(cases) + assume "thread \ runing (t@s)" + moreover have "th' \ runing (t@s)" using Cons(5) + by (metis neq_th' vat_t.pv_blocked_pre) + ultimately show ?thesis by auto + qed + qed with Cons show ?thesis + by (unfold P, simp add:cntP_def cntV_def count_def) qed - with not_holding have cnt_eq: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - by (unfold V, simp add:cntP_def cntV_def count_def) - moreover from in_thread - have in_thread': "th' \ threads ((e # t) @ s)" by (unfold V, simp) + moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold P, simp) ultimately show ?thesis by auto qed next - case (P thread cs) - from Cons and P have "step (t@s) (P thread cs)" by auto - hence neq_th': "thread \ th'" - proof(cases) - assume "thread \ runing (t@s)" - moreover note not_runing - ultimately show ?thesis by auto - qed - with Cons and P have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - by (auto simp:cntP_def cntV_def count_def) - moreover from Cons and P have in_thread': "th' \ threads ((e # t) @ s)" - by auto - ultimately show ?thesis by auto - next - case (Create thread prio') - from Cons and Create have "step (t@s) (Create thread prio')" by auto - hence neq_th': "thread \ th'" - proof(cases) - assume "thread \ threads (t @ s)" - moreover have "th' \ threads (t@s)" by fact + case (V thread cs) + show ?thesis + proof - + have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" + proof - + have "thread \ th'" + proof - + have "step (t@s) (V thread cs)" using Cons V by auto + thus ?thesis + proof(cases) + assume "thread \ runing (t@s)" + moreover have "th' \ runing (t@s)" using Cons(5) + by (metis neq_th' vat_t.pv_blocked_pre) + ultimately show ?thesis by auto + qed + qed with Cons show ?thesis + by (unfold V, simp add:cntP_def cntV_def count_def) + qed + moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold V, simp) ultimately show ?thesis by auto qed - with Cons and Create - have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - by (auto simp:cntP_def cntV_def count_def) - moreover from Cons and Create - have in_thread': "th' \ threads ((e # t) @ s)" by auto - ultimately show ?thesis by auto + next + case (Create thread prio') + show ?thesis + proof - + have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" + proof - + have "thread \ th'" + proof - + have "step (t@s) (Create thread prio')" using Cons Create by auto + thus ?thesis using Cons(5) by (cases, auto) + qed with Cons show ?thesis + by (unfold Create, simp add:cntP_def cntV_def count_def) + qed + moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold Create, simp) + ultimately show ?thesis by auto + qed next case (Exit thread) - from Cons and Exit have "step (t@s) (Exit thread)" by auto - hence neq_th': "thread \ th'" - proof(cases) - assume "thread \ runing (t @ s)" - moreover note not_runing + show ?thesis + proof - + have neq_thread: "thread \ th'" + proof - + have "step (t@s) (Exit thread)" using Cons Exit by auto + thus ?thesis apply (cases) using Cons(5) + by (metis neq_th' vat_t.pv_blocked_pre) + qed + hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons + by (unfold Exit, simp add:cntP_def cntV_def count_def) + moreover have "th' \ threads ((e # t) @ s)" using Cons neq_thread + by (unfold Exit, simp) ultimately show ?thesis by auto qed - with Cons and Exit - have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - by (auto simp:cntP_def cntV_def count_def) - moreover from Cons and Exit and neq_th' - have in_thread': "th' \ threads ((e # t) @ s)" - by auto - ultimately show ?thesis by auto next case (Set thread prio') with Cons show ?thesis by (auto simp:cntP_def cntV_def count_def) qed - next - case Nil - with assms - show ?case by auto - qed +next + case Nil + with assms + show ?case by auto qed -(* -lemma runing_precond: - fixes th' - assumes th'_in: "th' \ threads s" - and eq_pv: "cntP s th' = cntV s th'" - and neq_th': "th' \ th" - shows "th' \ runing (t@s)" -proof - - from runing_precond_pre[OF th'_in eq_pv neq_th'] - have h1: "th' \ threads (t @ s)" and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto - from pv_blocked[OF h1 neq_th' h2] - show ?thesis . -qed -*) - -lemmas runing_precond_pre_dtc = runing_precond_pre[folded detached_eq[OF vt_t] detached_eq[OF vt_s]] +text {* Changing counting balance to detachedness *} +lemmas runing_precond_pre_dtc = runing_precond_pre + [folded vat_t.detached_eq vat_s.detached_eq] lemma runing_precond: fixes th' @@ -655,18 +606,11 @@ and neq_th': "th' \ th" and is_runing: "th' \ runing (t@s)" shows "cntP s th' > cntV s th'" + using assms proof - have "cntP s th' \ cntV s th'" - proof - assume eq_pv: "cntP s th' = cntV s th'" - from runing_precond_pre[OF th'_in eq_pv neq_th'] - have h1: "th' \ threads (t @ s)" - and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto - from pv_blocked_pre[OF h1 neq_th' h2] have " th' \ runing (t @ s)" . - with is_runing show "False" by simp - qed - moreover from cnp_cnv_cncs[OF vt_s, of th'] - have "cntV s th' \ cntP s th'" by auto + by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in) + moreover have "cntV s th' \ cntP s th'" using vat_s.cnp_cnv_cncs by auto ultimately show ?thesis by auto qed @@ -676,95 +620,44 @@ and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \ th' \ threads ((moment (i+j) t)@s)" -proof(induct j) - case (Suc k) - show ?case - proof - - { assume True: "Suc (i+k) \ length t" - from moment_head [OF this] - obtain e where - eq_me: "moment (Suc(i+k)) t = e#(moment (i+k) t)" - by blast - from red_moment[of "Suc(i+k)"] - and eq_me have "extend_highest_gen s th prio tm (e # moment (i + k) t)" by simp - hence vt_e: "vt (e#(moment (i + k) t)@s)" - by (unfold extend_highest_gen_def extend_highest_gen_axioms_def - highest_gen_def, auto) - have not_runing': "th' \ runing (moment (i + k) t @ s)" - proof - - show "th' \ runing (moment (i + k) t @ s)" - proof(rule extend_highest_gen.pv_blocked) - from Suc show "th' \ threads (moment (i + k) t @ s)" - by simp - next - from neq_th' show "th' \ th" . - next - from red_moment show "extend_highest_gen s th prio tm (moment (i + k) t)" . - next - from Suc vt_e show "detached (moment (i + k) t @ s) th'" - apply(subst detached_eq) - apply(auto intro: vt_e evt_cons) - done - qed - qed - from step_back_step[OF vt_e] - have "step ((moment (i + k) t)@s) e" . - hence "cntP (e#(moment (i + k) t)@s) th' = cntV (e#(moment (i + k) t)@s) th' \ - th' \ threads (e#(moment (i + k) t)@s)" - proof(cases) - case (thread_create thread prio) - with Suc show ?thesis by (auto simp:cntP_def cntV_def count_def) - next - case (thread_exit thread) - moreover have "thread \ th'" - proof - - have "thread \ runing (moment (i + k) t @ s)" by fact - moreover note not_runing' - ultimately show ?thesis by auto - qed - moreover note Suc - ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def) - next - case (thread_P thread cs) - moreover have "thread \ th'" - proof - - have "thread \ runing (moment (i + k) t @ s)" by fact - moreover note not_runing' - ultimately show ?thesis by auto - qed - moreover note Suc - ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def) - next - case (thread_V thread cs) - moreover have "thread \ th'" - proof - - have "thread \ runing (moment (i + k) t @ s)" by fact - moreover note not_runing' - ultimately show ?thesis by auto - qed - moreover note Suc - ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def) - next - case (thread_set thread prio') - with Suc show ?thesis - by (auto simp:cntP_def cntV_def count_def) - qed - with eq_me have ?thesis using eq_me by auto - } note h = this - show ?thesis - proof(cases "Suc (i+k) \ length t") - case True - from h [OF this] show ?thesis . - next - case False - with moment_ge - have eq_m: "moment (i + Suc k) t = moment (i+k) t" by auto - with Suc show ?thesis by auto - qed +proof - + interpret h_i: red_extend_highest_gen _ _ _ _ _ i + by (unfold_locales) + interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j" + by (unfold_locales) + interpret h: extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)" + proof(unfold_locales) + show "vt (moment i t @ s)" by (metis h_i.vt_t) + next + show "th \ threads (moment i t @ s)" by (metis h_i.th_kept) + next + show "preced th (moment i t @ s) = + Max (cp (moment i t @ s) ` threads (moment i t @ s))" + by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept) + next + show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th) + next + show "vt (moment j (restm i t) @ moment i t @ s)" + using moment_plus_split by (metis add.commute append_assoc h_j.vt_t) + next + fix th' prio' + assume "Create th' prio' \ set (moment j (restm i t))" + thus "prio' \ prio" using assms + by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append) + next + fix th' prio' + assume "Set th' prio' \ set (moment j (restm i t))" + thus "th' \ th \ prio' \ prio" + by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append) + next + fix th' + assume "Exit th' \ set (moment j (restm i t))" + thus "th' \ th" + by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append) qed -next - case 0 - from assms show ?case by auto + show ?thesis + by (metis add.commute append_assoc eq_pv h.runing_precond_pre + moment_plus_split neq_th' th'_in) qed lemma moment_blocked_eqpv: @@ -778,14 +671,19 @@ proof - from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" - and h2: "th' \ threads ((moment j t)@s)" by auto - with extend_highest_gen.pv_blocked - show ?thesis - using red_moment [of j] h2 neq_th' h1 - apply(auto) - by (metis extend_highest_gen.pv_blocked_pre) + and h2: "th' \ threads ((moment j t)@s)" by auto + moreover have "th' \ runing ((moment j t)@s)" + proof - + interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) + show ?thesis + using h.pv_blocked_pre h1 h2 neq_th' by auto + qed + ultimately show ?thesis by auto qed +(* The foregoing two lemmas are preparation for this one, but + in long run can be combined. Maybe I am wrong. +*) lemma moment_blocked: assumes neq_th': "th' \ th" and th'_in: "th' \ threads ((moment i t)@s)" @@ -795,71 +693,119 @@ th' \ threads ((moment j t)@s) \ th' \ runing ((moment j t)@s)" proof - - from vt_moment[OF vt_t, of "i+length s"] moment_prefix[of i t s] - have vt_i: "vt (moment i t @ s)" by auto - from vt_moment[OF vt_t, of "j+length s"] moment_prefix[of j t s] - have vt_j: "vt (moment j t @ s)" by auto - from moment_blocked_eqpv [OF neq_th' th'_in detached_elim [OF vt_i dtc] le_ij, - folded detached_eq[OF vt_j]] - show ?thesis . + interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) + interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) + have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'" + by (metis dtc h_i.detached_elim) + from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij] + show ?thesis by (metis h_j.detached_intro) qed -lemma runing_inversion_1: +lemma runing_preced_inversion: + assumes runing': "th' \ runing (t@s)" + shows "cp (t@s) th' = preced th s" (is "?L = ?R") +proof - + have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms + by (unfold runing_def, auto) + also have "\ = ?R" + by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) + finally show ?thesis . +qed + +text {* + The situation when @{term "th"} is blocked is analyzed by the following lemmas. +*} + +text {* + The following lemmas shows the running thread @{text "th'"}, if it is different from + @{term th}, must be live at the very beginning. By the term {\em the very beginning}, + we mean the moment where the formal investigation starts, i.e. the moment (or state) + @{term s}. +*} + +lemma runing_inversion_0: assumes neq_th': "th' \ th" and runing': "th' \ runing (t@s)" - shows "th' \ threads s \ cntV s th' < cntP s th'" -proof(cases "th' \ threads s") - case True - with runing_precond [OF this neq_th' runing'] show ?thesis by simp -next - case False - let ?Q = "\ t. th' \ threads (t@s)" - let ?q = "moment 0 t" - from moment_eq and False have not_thread: "\ ?Q ?q" by simp - from runing' have "th' \ threads (t@s)" by (simp add:runing_def readys_def) - from p_split_gen [of ?Q, OF this not_thread] - obtain i where lt_its: "i < length t" - and le_i: "0 \ i" - and pre: " th' \ threads (moment i t @ s)" (is "th' \ threads ?pre") - and post: "(\i'>i. th' \ threads (moment i' t @ s))" by auto - from lt_its have "Suc i \ length t" by auto - from moment_head[OF this] obtain e where - eq_me: "moment (Suc i) t = e # moment i t" by blast - from red_moment[of "Suc i"] and eq_me - have "extend_highest_gen s th prio tm (e # moment i t)" by simp - hence vt_e: "vt (e#(moment i t)@s)" - by (unfold extend_highest_gen_def extend_highest_gen_axioms_def - highest_gen_def, auto) - from step_back_step[OF this] have stp_i: "step (moment i t @ s) e" . - from post[rule_format, of "Suc i"] and eq_me - have not_in': "th' \ threads (e # moment i t@s)" by auto - from create_pre[OF stp_i pre this] - obtain prio where eq_e: "e = Create th' prio" . - have "cntP (moment i t@s) th' = cntV (moment i t@s) th'" - proof(rule cnp_cnv_eq) - from step_back_vt [OF vt_e] - show "vt (moment i t @ s)" . - next - from eq_e and stp_i - have "step (moment i t @ s) (Create th' prio)" by simp - thus "th' \ threads (moment i t @ s)" by (cases, simp) - qed - with eq_e - have "cntP ((e#moment i t)@s) th' = cntV ((e#moment i t)@s) th'" - by (simp add:cntP_def cntV_def count_def) - with eq_me[symmetric] - have h1: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" - by simp - from eq_e have "th' \ threads ((e#moment i t)@s)" by simp - with eq_me [symmetric] - have h2: "th' \ threads (moment (Suc i) t @ s)" by simp - from moment_blocked_eqpv [OF neq_th' h2 h1, of "length t"] and lt_its - and moment_ge - have "th' \ runing (t @ s)" by auto - with runing' - show ?thesis by auto + shows "th' \ threads s" +proof - + -- {* The proof is by contradiction: *} + { assume otherwise: "\ ?thesis" + have "th' \ runing (t @ s)" + proof - + -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *} + have th'_in: "th' \ threads (t@s)" using runing' by (simp add:runing_def readys_def) + -- {* However, @{text "th'"} does not exist at very beginning. *} + have th'_notin: "th' \ threads (moment 0 t @ s)" using otherwise + by (metis append.simps(1) moment_zero) + -- {* Therefore, there must be a moment during @{text "t"}, when + @{text "th'"} came into being. *} + -- {* Let us suppose the moment being @{text "i"}: *} + from p_split_gen[OF th'_in th'_notin] + obtain i where lt_its: "i < length t" + and le_i: "0 \ i" + and pre: " th' \ threads (moment i t @ s)" (is "th' \ threads ?pre") + and post: "(\i'>i. th' \ threads (moment i' t @ s))" by (auto) + interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) + interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales) + from lt_its have "Suc i \ length t" by auto + -- {* Let us also suppose the event which makes this change is @{text e}: *} + from moment_head[OF this] obtain e where + eq_me: "moment (Suc i) t = e # moment i t" by blast + hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t) + hence "PIP (moment i t @ s) e" by (cases, simp) + -- {* It can be derived that this event @{text "e"}, which + gives birth to @{term "th'"} must be a @{term "Create"}: *} + from create_pre[OF this, of th'] + obtain prio where eq_e: "e = Create th' prio" + by (metis append_Cons eq_me lessI post pre) + have h1: "th' \ threads (moment (Suc i) t @ s)" using post by auto + have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" + proof - + have "cntP (moment i t@s) th' = cntV (moment i t@s) th'" + by (metis h_i.cnp_cnv_eq pre) + thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def) + qed + show ?thesis + using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge + by auto + qed + with `th' \ runing (t@s)` + have False by simp + } thus ?thesis by auto qed +text {* + The second lemma says, if the running thread @{text th'} is different from + @{term th}, then this @{text th'} must in the possession of some resources + at the very beginning. + + To ease the reasoning of resource possession of one particular thread, + we used two auxiliary functions @{term cntV} and @{term cntP}, + which are the counters of @{term P}-operations and + @{term V}-operations respectively. + If the number of @{term V}-operation is less than the number of + @{term "P"}-operations, the thread must have some unreleased resource. +*} + +lemma runing_inversion_1: (* ddd *) + assumes neq_th': "th' \ th" + and runing': "th' \ runing (t@s)" + -- {* thread @{term "th'"} is a live on in state @{term "s"} and + it has some unreleased resource. *} + shows "th' \ threads s \ cntV s th' < cntP s th'" +proof - + -- {* The proof is a simple composition of @{thm runing_inversion_0} and + @{thm runing_precond}: *} + -- {* By applying @{thm runing_inversion_0} to assumptions, + it can be shown that @{term th'} is live in state @{term s}: *} + have "th' \ threads s" using runing_inversion_0[OF assms(1,2)] . + -- {* Then the thesis is derived easily by applying @{thm runing_precond}: *} + with runing_precond [OF this neq_th' runing'] show ?thesis by simp +qed + +text {* + The following lemma is just a rephrasing of @{thm runing_inversion_1}: +*} lemma runing_inversion_2: assumes runing': "th' \ runing (t@s)" shows "th' = th \ (th' \ th \ th' \ threads s \ cntV s th' < cntP s th')" @@ -868,37 +814,11 @@ show ?thesis by auto qed -lemma runing_preced_inversion: - assumes runing': "th' \ runing (t@s)" - shows "cp (t@s) th' = preced th s" -proof - - from runing' have "cp (t@s) th' = Max (cp (t @ s) ` readys (t @ s))" - by (unfold runing_def, auto) - also have "\ = preced th s" - proof - - from max_cp_readys_threads[OF vt_t] - have "\ = Max (cp (t @ s) ` threads (t @ s))" . - also have "\ = preced th s" - proof - - from max_kept - and max_cp_eq [OF vt_t] - show ?thesis by auto - qed - finally show ?thesis . - qed - finally show ?thesis . -qed - lemma runing_inversion_3: assumes runing': "th' \ runing (t@s)" and neq_th: "th' \ th" shows "th' \ threads s \ (cntV s th' < cntP s th' \ cp (t@s) th' = preced th s)" -proof - - from runing_inversion_2 [OF runing'] - and neq_th - and runing_preced_inversion[OF runing'] - show ?thesis by auto -qed + by (metis neq_th runing' runing_inversion_2 runing_preced_inversion) lemma runing_inversion_4: assumes runing': "th' \ runing (t@s)" @@ -906,83 +826,93 @@ shows "th' \ threads s" and "\detached s th'" and "cp (t@s) th' = preced th s" -using runing_inversion_3 [OF runing'] - and neq_th - and runing_preced_inversion[OF runing'] -apply(auto simp add: detached_eq[OF vt_s]) -done + apply (metis neq_th runing' runing_inversion_2) + apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc) + by (metis neq_th runing' runing_inversion_3) + + +text {* + Suppose @{term th} is not running, it is first shown that + there is a path in RAG leading from node @{term th} to another thread @{text "th'"} + in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). + Now, since @{term readys}-set is non-empty, there must be + one in it which holds the highest @{term cp}-value, which, by definition, + is the @{term runing}-thread. However, we are going to show more: this running thread + is exactly @{term "th'"}. + *} +lemma th_blockedE: (* ddd *) + assumes "th \ runing (t@s)" + obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" + "th' \ runing (t@s)" +proof - + -- {* According to @{thm vat_t.th_chain_to_ready}, either + @{term "th"} is in @{term "readys"} or there is path leading from it to + one thread in @{term "readys"}. *} + have "th \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (RAG (t @ s))\<^sup>+)" + using th_kept vat_t.th_chain_to_ready by auto + -- {* However, @{term th} can not be in @{term readys}, because otherwise, since + @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *} + moreover have "th \ readys (t@s)" + using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto + -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in + term @{term readys}: *} + ultimately obtain th' where th'_in: "th' \ readys (t@s)" + and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto + -- {* We are going to show that this @{term th'} is running. *} + have "th' \ runing (t@s)" + proof - + -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *} + have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R") + proof - + have "?L = Max ((the_preced (t @ s) \ the_thread) ` subtree (tRAG (t @ s)) (Th th'))" + by (unfold cp_alt_def1, simp) + also have "... = (the_preced (t @ s) \ the_thread) (Th th)" + proof(rule image_Max_subset) + show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads) + next + show "subtree (tRAG (t @ s)) (Th th') \ Th ` threads (t @ s)" + by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) + next + show "Th th \ subtree (tRAG (t @ s)) (Th th')" using dp + by (unfold tRAG_subtree_eq, auto simp:subtree_def) + next + show "Max ((the_preced (t @ s) \ the_thread) ` Th ` threads (t @ s)) = + (the_preced (t @ s) \ the_thread) (Th th)" (is "Max ?L = _") + proof - + have "?L = the_preced (t @ s) ` threads (t @ s)" + by (unfold image_comp, rule image_cong, auto) + thus ?thesis using max_preced the_preced_def by auto + qed + qed + also have "... = ?R" + using th_cp_max th_cp_preced th_kept + the_preced_def vat_t.max_cp_readys_threads by auto + finally show ?thesis . + qed + -- {* Now, since @{term th'} holds the highest @{term cp} + and we have already show it is in @{term readys}, + it is @{term runing} by definition. *} + with `th' \ readys (t@s)` show ?thesis by (simp add: runing_def) + qed + -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} + moreover have "Th th' \ ancestors (RAG (t @ s)) (Th th)" + using `(Th th, Th th') \ (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) + ultimately show ?thesis using that by metis +qed + +text {* + Now it is easy to see there is always a thread to run by case analysis + on whether thread @{term th} is running: if the answer is Yes, the + the running thread is obviously @{term th} itself; otherwise, the running + thread is the @{text th'} given by lemma @{thm th_blockedE}. +*} lemma live: "runing (t@s) \ {}" -proof(cases "th \ runing (t@s)") +proof(cases "th \ runing (t@s)") case True thus ?thesis by auto next case False - then have not_ready: "th \ readys (t@s)" - apply (unfold runing_def, - insert th_cp_max max_cp_readys_threads[OF vt_t, symmetric]) - by auto - from th_kept have "th \ threads (t@s)" by auto - from th_chain_to_ready[OF vt_t this] and not_ready - obtain th' where th'_in: "th' \ readys (t@s)" - and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto - have "th' \ runing (t@s)" - proof - - have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" - proof - - have " Max ((\th. preced th (t @ s)) ` ({th'} \ dependants (wq (t @ s)) th')) = - preced th (t@s)" - proof(rule Max_eqI) - fix y - assume "y \ (\th. preced th (t @ s)) ` ({th'} \ dependants (wq (t @ s)) th')" - then obtain th1 where - h1: "th1 = th' \ th1 \ dependants (wq (t @ s)) th'" - and eq_y: "y = preced th1 (t@s)" by auto - show "y \ preced th (t @ s)" - proof - - from max_preced - have "preced th (t @ s) = Max ((\th'. preced th' (t @ s)) ` threads (t @ s))" . - moreover have "y \ \" - proof(rule Max_ge) - from h1 - have "th1 \ threads (t@s)" - proof - assume "th1 = th'" - with th'_in show ?thesis by (simp add:readys_def) - next - assume "th1 \ dependants (wq (t @ s)) th'" - with dependants_threads [OF vt_t] - show "th1 \ threads (t @ s)" by auto - qed - with eq_y show " y \ (\th'. preced th' (t @ s)) ` threads (t @ s)" by simp - next - from finite_threads[OF vt_t] - show "finite ((\th'. preced th' (t @ s)) ` threads (t @ s))" by simp - qed - ultimately show ?thesis by auto - qed - next - from finite_threads[OF vt_t] dependants_threads [OF vt_t, of th'] - show "finite ((\th. preced th (t @ s)) ` ({th'} \ dependants (wq (t @ s)) th'))" - by (auto intro:finite_subset) - next - from dp - have "th \ dependants (wq (t @ s)) th'" - by (unfold cs_dependants_def, auto simp:eq_RAG) - thus "preced th (t @ s) \ - (\th. preced th (t @ s)) ` ({th'} \ dependants (wq (t @ s)) th')" - by auto - qed - moreover have "\ = Max (cp (t @ s) ` readys (t @ s))" - proof - - from max_preced and max_cp_eq[OF vt_t, symmetric] - have "preced th (t @ s) = Max (cp (t @ s) ` threads (t @ s))" by simp - with max_cp_readys_threads[OF vt_t] show ?thesis by simp - qed - ultimately show ?thesis by (unfold cp_eq_cpreced cpreced_def, simp) - qed - with th'_in show ?thesis by (auto simp:runing_def) - qed - thus ?thesis by auto + thus ?thesis using th_blockedE by auto qed end diff -r 031d2ae9c9b8 -r b620a2a0806a Precedence_ord.thy --- a/Precedence_ord.thy Tue Dec 22 23:13:31 2015 +0800 +++ b/Precedence_ord.thy Wed Jan 06 20:46:14 2016 +0800 @@ -14,6 +14,19 @@ (Prc fx sx, Prc fy sy) \ fx < fy \ (fx \ fy \ sy \ sx))" +lemma preced_leI1[intro]: + assumes "fx < fy" + shows "Prc fx sx \ Prc fy sy" + using assms + by (simp add: precedence_le_def) + +lemma preced_leI2[intro]: + assumes "fx \ fy" + and "sy \ sx" + shows "Prc fx sx \ Prc fy sy" + using assms + by (simp add: precedence_le_def) + definition precedence_less_def: "x < y \ (case (x, y) of (Prc fx sx, Prc fy sy) \ diff -r 031d2ae9c9b8 -r b620a2a0806a PrioG.thy --- a/PrioG.thy Tue Dec 22 23:13:31 2015 +0800 +++ b/PrioG.thy Wed Jan 06 20:46:14 2016 +0800 @@ -2,6 +2,20 @@ imports PrioGDef begin +locale valid_trace = + fixes s + assumes vt : "vt s" + +locale valid_trace_e = valid_trace + + fixes e + assumes vt_e: "vt (e#s)" +begin + +lemma pip_e: "PIP s e" + using vt_e by (cases, simp) + +end + lemma runing_ready: shows "runing s \ readys s" unfolding runing_def readys_def @@ -16,8 +30,30 @@ "cs \ cs' \ wq (V thread cs#s) cs' = wq s cs'" by (auto simp:wq_def Let_def cp_def split:list.splits) -lemma wq_distinct: "vt s \ distinct (wq s cs)" -proof(erule_tac vt.induct, simp add:wq_def) +context valid_trace +begin + +lemma ind [consumes 0, case_names Nil Cons, induct type]: + assumes "PP []" + and "(\s e. valid_trace s \ valid_trace (e#s) \ + PP s \ PIP s e \ PP (e # s))" + shows "PP s" +proof(rule vt.induct[OF vt]) + from assms(1) show "PP []" . +next + fix s e + assume h: "vt s" "PP s" "PIP s e" + show "PP (e # s)" + proof(cases rule:assms(2)) + from h(1) show v1: "valid_trace s" by (unfold_locales, simp) + next + from h(1,3) have "vt (e#s)" by auto + thus "valid_trace (e # s)" by (unfold_locales, simp) + qed (insert h, auto) +qed + +lemma wq_distinct: "distinct (wq s cs)" +proof(rule ind, simp add:wq_def) fix s e assume h1: "step s e" and h2: "distinct (wq s cs)" @@ -51,6 +87,12 @@ qed qed +end + + +context valid_trace_e +begin + text {* The following lemma shows that only the @{text "P"} operation can add new thread into waiting queues. @@ -59,9 +101,7 @@ *} lemma block_pre: - fixes thread cs s - assumes vt_e: "vt (e#s)" - and s_ni: "thread \ set (wq s cs)" + assumes s_ni: "thread \ set (wq s cs)" and s_i: "thread \ set (wq (e#s) cs)" shows "e = P thread cs" proof - @@ -85,7 +125,7 @@ by (auto simp:wq_def Let_def split:if_splits) next case (V th cs) - with assms show ?thesis + with vt_e assms show ?thesis apply (auto simp:wq_def Let_def split:if_splits) proof - fix q qs @@ -98,7 +138,7 @@ proof - have "set (SOME q. distinct q \ set q = set qs) = set qs" proof(rule someI2) - from wq_distinct [OF step_back_vt[OF vt], of cs] + from wq_distinct [of cs] and h2[symmetric, folded wq_def] show "distinct qs \ set qs = set qs" by auto next @@ -112,6 +152,8 @@ qed qed +end + text {* The following lemmas is also obvious and shallow. It says that only running thread can request for a critical resource @@ -126,7 +168,6 @@ by auto lemma abs1: - fixes e es assumes ein: "e \ set es" and neq: "hd es \ hd (es @ [x])" shows "False" @@ -141,15 +182,17 @@ inductive_cases evt_cons: "vt (a#s)" +context valid_trace_e +begin + lemma abs2: - assumes vt: "vt (e#s)" - and inq: "thread \ set (wq s cs)" + assumes inq: "thread \ set (wq s cs)" and nh: "thread = hd (wq s cs)" and qt: "thread \ hd (wq (e#s) cs)" and inq': "thread \ set (wq (e#s) cs)" shows "False" proof - - from assms show "False" + from vt_e assms show "False" apply (cases e) apply ((simp split:if_splits add:Let_def wq_def)[1])+ apply (insert abs1, fast)[1] @@ -161,13 +204,13 @@ and eq_wq: "wq_fun (schs s) cs = thread # qs" show "False" proof - - from wq_distinct[OF step_back_vt[OF vt], of cs] + from wq_distinct[of cs] and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp moreover have "thread \ set qs" proof - have "set (SOME q. distinct q \ set q = set qs) = set qs" proof(rule someI2) - from wq_distinct [OF step_back_vt[OF vt], of cs] + from wq_distinct [of cs] and eq_wq [folded wq_def] show "distinct qs \ set qs = set qs" by auto next @@ -181,28 +224,33 @@ qed qed -lemma vt_moment: "\ t. \vt s\ \ vt (moment t s)" -proof(induct s, simp) - fix a s t - assume h: "\t.\vt s\ \ vt (moment t s)" - and vt_a: "vt (a # s)" - show "vt (moment t (a # s))" - proof(cases "t \ length (a#s)") +end + +context valid_trace +begin + +lemma vt_moment: "\ t. vt (moment t s)" +proof(induct rule:ind) + case Nil + thus ?case by (simp add:vt_nil) +next + case (Cons s e t) + show ?case + proof(cases "t \ length (e#s)") case True - from True have "moment t (a#s) = a#s" by simp - with vt_a show ?thesis by simp + from True have "moment t (e#s) = e#s" by simp + thus ?thesis using Cons + by (simp add:valid_trace_def) next case False - hence le_t1: "t \ length s" by simp - from vt_a have "vt s" - by (erule_tac evt_cons, simp) - from h [OF this] have "vt (moment t s)" . - moreover have "moment t (a#s) = moment t s" + from Cons have "vt (moment t s)" by simp + moreover have "moment t (e#s) = moment t s" proof - - from moment_app [OF le_t1, of "[a]"] + from False have "t \ length s" by simp + from moment_app [OF this, of "[e]"] show ?thesis by simp qed - ultimately show ?thesis by auto + ultimately show ?thesis by simp qed qed @@ -244,9 +292,7 @@ *} lemma waiting_unique_pre: - fixes cs1 cs2 s thread - assumes vt: "vt s" - and h11: "thread \ set (wq s cs1)" + assumes h11: "thread \ set (wq s cs1)" and h12: "thread \ hd (wq s cs1)" assumes h21: "thread \ set (wq s cs2)" and h22: "thread \ hd (wq s cs2)" @@ -282,25 +328,26 @@ from nn2 [rule_format, OF this] and eq_m have h1: "thread \ set (wq (e#moment t2 s) cs2)" and h2: "thread \ hd (wq (e#moment t2 s) cs2)" by auto - have vt_e: "vt (e#moment t2 s)" + have "vt (e#moment t2 s)" proof - - from vt_moment [OF vt] + from vt_moment have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed + then interpret vt_e: valid_trace_e "moment t2 s" "e" + by (unfold_locales, auto, cases, simp) have ?thesis proof(cases "thread \ set (wq (moment t2 s) cs2)") case True from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)" - by auto - thm abs2 - from abs2 [OF vt_e True eq_th h2 h1] + by auto + from vt_e.abs2 [OF True eq_th h2 h1] show ?thesis by auto next case False - from block_pre [OF vt_e False h1] + from vt_e.block_pre[OF False h1] have "e = P thread cs2" . - with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp + with vt_e.vt_e have "vt ((P thread cs2)# moment t2 s)" by simp from p_pre [OF this] have "thread \ runing (moment t2 s)" by simp with runing_ready have "thread \ readys (moment t2 s)" by auto with nn1 [rule_format, OF lt12] @@ -316,24 +363,26 @@ from nn1 [rule_format, OF this] and eq_m have h1: "thread \ set (wq (e#moment t1 s) cs1)" and h2: "thread \ hd (wq (e#moment t1 s) cs1)" by auto - have vt_e: "vt (e#moment t1 s)" + have "vt (e#moment t1 s)" proof - - from vt_moment [OF vt] + from vt_moment have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed + then interpret vt_e: valid_trace_e "moment t1 s" e + by (unfold_locales, auto, cases, auto) have ?thesis proof(cases "thread \ set (wq (moment t1 s) cs1)") case True from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)" by auto - from abs2 [OF vt_e True eq_th h2 h1] + from vt_e.abs2 True eq_th h2 h1 show ?thesis by auto next case False - from block_pre [OF vt_e False h1] + from vt_e.block_pre [OF False h1] have "e = P thread cs1" . - with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp + with vt_e.vt_e have "vt ((P thread cs1)# moment t1 s)" by simp from p_pre [OF this] have "thread \ runing (moment t1 s)" by simp with runing_ready have "thread \ readys (moment t1 s)" by auto with nn2 [rule_format, OF lt12] @@ -351,20 +400,22 @@ h2: "thread \ hd (wq (e#moment t1 s) cs1)" by auto have vt_e: "vt (e#moment t1 s)" proof - - from vt_moment [OF vt] + from vt_moment have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed + then interpret vt_e: valid_trace_e "moment t1 s" e + by (unfold_locales, auto, cases, auto) have ?thesis proof(cases "thread \ set (wq (moment t1 s) cs1)") case True from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)" by auto - from abs2 [OF vt_e True eq_th h2 h1] + from vt_e.abs2 [OF True eq_th h2 h1] show ?thesis by auto next case False - from block_pre [OF vt_e False h1] + from vt_e.block_pre [OF False h1] have eq_e1: "e = P thread cs1" . have lt_t3: "t1 < ?t3" by simp with eqt12 have "t2 < ?t3" by simp @@ -377,17 +428,21 @@ from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)" by auto from vt_e and eqt12 have "vt (e#moment t2 s)" by simp - from abs2 [OF this True eq_th h2 h1] + then interpret vt_e2: valid_trace_e "moment t2 s" e + by (unfold_locales, auto, cases, auto) + from vt_e2.abs2 [OF True eq_th h2 h1] show ?thesis . next case False - have vt_e: "vt (e#moment t2 s)" + have "vt (e#moment t2 s)" proof - - from vt_moment [OF vt] eqt12 + from vt_moment eqt12 have "vt (moment (Suc t2) s)" by auto with eq_m eqt12 show ?thesis by simp qed - from block_pre [OF vt_e False h1] + then interpret vt_e2: valid_trace_e "moment t2 s" e + by (unfold_locales, auto, cases, auto) + from vt_e2.block_pre [OF False h1] have "e = P thread cs2" . with eq_e1 neq12 show ?thesis by auto qed @@ -401,15 +456,15 @@ *} lemma waiting_unique: - fixes s cs1 cs2 - assumes "vt s" - and "waiting s th cs1" + assumes "waiting s th cs1" and "waiting s th cs2" shows "cs1 = cs2" using waiting_unique_pre assms unfolding wq_def s_waiting_def by auto +end + (* not used *) text {* Every thread can only be blocked on one critical resource, @@ -417,13 +472,10 @@ This fact is much more easier according to our definition. *} lemma held_unique: - fixes s::"state" - assumes "holding s th1 cs" + assumes "holding (s::event list) th1 cs" and "holding s th2 cs" shows "th1 = th2" -using assms -unfolding s_holding_def -by auto + by (insert assms, unfold s_holding_def, auto) lemma last_set_lt: "th \ threads s \ last_set th s < length s" @@ -642,6 +694,8 @@ assume vt: "vt (V th cs # s)" and nw: "\ waiting (wq (V th cs # s)) t c" and wt: "waiting (wq s) t c" + from vt interpret vt_v: valid_trace_e s "V th cs" + by (cases, unfold_locales, simp) show "next_th s th cs t \ cs = c" proof(cases "cs = c") case False @@ -659,7 +713,7 @@ and eq_wq: "wq_fun (schs s) cs = a # list" have " set (SOME q. distinct q \ set q = set list) = set list" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] + from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def] show "distinct list \ set list = set list" by auto next show "\x. distinct x \ set x = set list \ set x = set list" @@ -673,7 +727,7 @@ and eq_wq: "wq_fun (schs s) cs = a # list" have " set (SOME q. distinct q \ set q = set list) = set list" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] + from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def] show "distinct list \ set list = set list" by auto next show "\x. distinct x \ set x = set list \ set x = set list" @@ -704,6 +758,8 @@ proof - assume vt: "vt (V th cs # s)" and hd: "holding (wq (V th cs # s)) th cs" + from vt interpret vt_v: valid_trace_e s "V th cs" + by (cases, unfold_locales, simp+) from step_back_step [OF vt] and hd show "False" proof(cases) @@ -719,7 +775,7 @@ \ set (SOME q. distinct q \ set q = set list)" have "set (SOME q. distinct q \ set q = set list) = set list" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq + from vt_v.wq_distinct[of cs] and eq_wq show "distinct list \ set list = set list" by auto next show "\x. distinct x \ set x = set list \ set x = set list" @@ -727,7 +783,7 @@ qed moreover have "distinct (hd (SOME q. distinct q \ set q = set list) # list)" proof - - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq + from vt_v.wq_distinct[of cs] and eq_wq show ?thesis by auto qed moreover note eq_wq and hd_in @@ -747,9 +803,11 @@ and nrest: "rest \ []" and ni: "hd (SOME q. distinct q \ set q = set rest) \ set (SOME q. distinct q \ set q = set rest)" + from vt interpret vt_v: valid_trace_e s "V th cs" + by (cases, unfold_locales, simp+) have "(SOME q. distinct q \ set q = set rest) \ []" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq + from vt_v.wq_distinct[of cs] and eq_wq show "distinct rest \ set rest = set rest" by auto next fix x assume "distinct x \ set x = set rest" @@ -791,6 +849,8 @@ let ?s' = "(V th cs # s)" assume vt: "vt ?s'" and wt: "waiting (wq ?s') t c" + from vt interpret vt_v: valid_trace_e s "V th cs" + by (cases, unfold_locales, simp+) show "waiting (wq s) t c" proof(cases "c = cs") case False @@ -809,7 +869,7 @@ and eq_wq: "wq_fun (schs s) cs = a # list" have "set (SOME q. distinct q \ set q = set list) = set list" proof(rule someI2) - from wq_distinct [OF step_back_vt[OF vt], of cs] + from vt_v.wq_distinct [of cs] and eq_wq[folded wq_def] show "distinct list \ set list = set list" by auto next @@ -827,7 +887,7 @@ assume " t \ set (SOME q. distinct q \ set q = set list)" moreover have "\ = set list" proof(rule someI2) - from wq_distinct [OF step_back_vt[OF vt], of cs] + from vt_v.wq_distinct [of cs] and eq_wq[folded wq_def] show "distinct list \ set list = set list" by auto next @@ -836,7 +896,7 @@ qed ultimately show "t \ set list" by simp qed - with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def] + with eq_wq and vt_v.wq_distinct [of cs, unfolded wq_def] show False by auto qed qed @@ -885,19 +945,22 @@ lemma RAG_target_th: "(Th th, x) \ RAG (s::state) \ \ cs. x = Cs cs" by (unfold s_RAG_def, auto) +context valid_trace +begin + text {* The following lemma shows that @{text "RAG"} is acyclic. The overall structure is by induction on the formation of @{text "vt s"} and then case analysis on event @{text "e"}, where the non-trivial cases for those for @{text "V"} and @{text "P"} events. *} -lemma acyclic_RAG: - fixes s - assumes vt: "vt s" +lemma acyclic_RAG: shows "acyclic (RAG s)" -using assms +using vt proof(induct) case (vt_cons s e) + interpret vt_s: valid_trace s using vt_cons(1) + by (unfold_locales, simp) assume ih: "acyclic (RAG s)" and stp: "step s e" and vt: "vt s" @@ -949,8 +1012,8 @@ hence wt_th': "waiting s ?th' cs'" unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp hence "cs' = cs" - proof(rule waiting_unique [OF vt]) - from eq_wq wq_distinct[OF vt, of cs] + proof(rule vt_s.waiting_unique) + from eq_wq vt_s.wq_distinct[of cs] show "waiting s ?th' cs" apply (unfold s_waiting_def wq_def, auto) proof - @@ -958,7 +1021,7 @@ and eq_wq: "wq_fun (schs s) cs = th # rest" have "(SOME q. distinct q \ set q = set rest) \ []" proof(rule someI2) - from wq_distinct[OF vt, of cs] and eq_wq + from vt_s.wq_distinct[of cs] and eq_wq show "distinct rest \ set rest = set rest" unfolding wq_def by auto next fix x assume "distinct x \ set x = set rest" @@ -968,7 +1031,7 @@ set (SOME q. distinct q \ set q = set rest)" by auto moreover have "\ = set rest" proof(rule someI2) - from wq_distinct[OF vt, of cs] and eq_wq + from vt_s.wq_distinct[of cs] and eq_wq show "distinct rest \ set rest = set rest" unfolding wq_def by auto next show "\x. distinct x \ set x = set rest \ set x = set rest" by auto @@ -980,7 +1043,7 @@ and eq_wq: "wq s cs = hd (SOME q. distinct q \ set q = set rest) # rest" have "(SOME q. distinct q \ set q = set rest) \ []" proof(rule someI2) - from wq_distinct[OF vt, of cs] and eq_wq + from vt_s.wq_distinct[of cs] and eq_wq show "distinct rest \ set rest = set rest" by auto next fix x assume "distinct x \ set x = set rest" @@ -990,7 +1053,7 @@ set (SOME q. distinct q \ set q = set rest)" by auto moreover have "\ = set rest" proof(rule someI2) - from wq_distinct[OF vt, of cs] and eq_wq + from vt_s.wq_distinct[of cs] and eq_wq show "distinct rest \ set rest = set rest" by auto next show "\x. distinct x \ set x = set rest \ set x = set rest" by auto @@ -1066,14 +1129,14 @@ qed -lemma finite_RAG: - fixes s - assumes vt: "vt s" +lemma finite_RAG: shows "finite (RAG s)" proof - from vt show ?thesis proof(induct) case (vt_cons s e) + interpret vt_s: valid_trace s using vt_cons(1) + by (unfold_locales, simp) assume ih: "finite (RAG s)" and stp: "step s e" and vt: "vt s" @@ -1145,32 +1208,35 @@ text {* Several useful lemmas *} lemma wf_dep_converse: - fixes s - assumes vt: "vt s" shows "wf ((RAG s)^-1)" proof(rule finite_acyclic_wf_converse) - from finite_RAG [OF vt] + from finite_RAG show "finite (RAG s)" . next - from acyclic_RAG[OF vt] + from acyclic_RAG show "acyclic (RAG s)" . qed +end + lemma hd_np_in: "x \ set l \ hd l \ set l" -by (induct l, auto) + by (induct l, auto) lemma th_chasing: "(Th th, Cs cs) \ RAG (s::state) \ \ th'. (Cs cs, Th th') \ RAG s" by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in) +context valid_trace +begin + lemma wq_threads: - fixes s cs - assumes vt: "vt s" - and h: "th \ set (wq s cs)" + assumes h: "th \ set (wq s cs)" shows "th \ threads s" proof - from vt and h show ?thesis proof(induct arbitrary: th cs) case (vt_cons s e) + interpret vt_s: valid_trace s + using vt_cons(1) by (unfold_locales, auto) assume ih: "\th cs. th \ set (wq s cs) \ th \ threads s" and stp: "step s e" and vt: "vt s" @@ -1227,7 +1293,7 @@ assume th_in: "th \ set (SOME q. distinct q \ set q = set rest)" have "set (SOME q. distinct q \ set q = set rest) = set rest" proof(rule someI2) - from wq_distinct[OF vt, of cs'] and eq_wq[folded wq_def] + from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def] show "distinct rest \ set rest = set rest" by auto next show "\x. distinct x \ set x = set rest \ set x = set rest" @@ -1264,14 +1330,13 @@ qed qed -lemma range_in: "\vt s; (Th th) \ Range (RAG (s::state))\ \ th \ threads s" +lemma range_in: "\(Th th) \ Range (RAG (s::state))\ \ th \ threads s" apply(unfold s_RAG_def cs_waiting_def cs_holding_def) by (auto intro:wq_threads) lemma readys_v_eq: fixes th thread cs rest - assumes vt: "vt s" - and neq_th: "th \ thread" + assumes neq_th: "th \ thread" and eq_wq: "wq s cs = thread#rest" and not_in: "th \ set rest" shows "(th \ readys (V thread cs#s)) = (th \ readys s)" @@ -1292,7 +1357,7 @@ and eq_wq: "wq_fun (schs s) cs = thread # rest" have "set (SOME q. distinct q \ set q = set rest) = set rest" proof(rule someI2) - from wq_distinct[OF vt, of cs, unfolded wq_def] and eq_wq[unfolded wq_def] + from wq_distinct[of cs, unfolded wq_def] and eq_wq[unfolded wq_def] show "distinct rest \ set rest = set rest" by auto next show "\x. distinct x \ set x = set rest \ set x = set rest" by auto @@ -1308,10 +1373,9 @@ *} lemma chain_building: - assumes vt: "vt s" shows "node \ Domain (RAG s) \ (\ th'. th' \ readys s \ (node, Th th') \ (RAG s)^+)" proof - - from wf_dep_converse [OF vt] + from wf_dep_converse have h: "wf ((RAG s)\)" . show ?thesis proof(induct rule:wf_induct [OF h]) @@ -1342,7 +1406,7 @@ from True and th'_d show ?thesis by auto next case False - from th'_d and range_in [OF vt] have "th' \ threads s" by auto + from th'_d and range_in have "th' \ threads s" by auto with False have "Th th' \ Domain (RAG s)" by (auto simp:readys_def wq_def s_waiting_def s_RAG_def cs_waiting_def Domain_def) from ih [OF th'_d this] @@ -1362,9 +1426,7 @@ The following is just an instance of @{text "chain_building"}. *} lemma th_chain_to_ready: - fixes s th - assumes vt: "vt s" - and th_in: "th \ threads s" + assumes th_in: "th \ threads s" shows "th \ readys s \ (\ th'. th' \ readys s \ (Th th, Th th') \ (RAG s)^+)" proof(cases "th \ readys s") case True @@ -1373,10 +1435,12 @@ case False from False and th_in have "Th th \ Domain (RAG s)" by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def) - from chain_building [rule_format, OF vt this] + from chain_building [rule_format, OF this] show ?thesis by auto qed +end + lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs" by (unfold s_waiting_def cs_waiting_def wq_def, auto) @@ -1386,16 +1450,24 @@ lemma holding_unique: "\holding (s::state) th1 cs; holding s th2 cs\ \ th1 = th2" by (unfold s_holding_def cs_holding_def, auto) -lemma unique_RAG: "\vt s; (n, n1) \ RAG s; (n, n2) \ RAG s\ \ n1 = n2" +context valid_trace +begin + +lemma unique_RAG: "\(n, n1) \ RAG s; (n, n2) \ RAG s\ \ n1 = n2" apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq) by(auto elim:waiting_unique holding_unique) +end + + lemma trancl_split: "(a, b) \ r^+ \ \ c. (a, c) \ r" by (induct rule:trancl_induct, auto) +context valid_trace +begin + lemma dchain_unique: - assumes vt: "vt s" - and th1_d: "(n, Th th1) \ (RAG s)^+" + assumes th1_d: "(n, Th th1) \ (RAG s)^+" and th1_r: "th1 \ readys s" and th2_d: "(n, Th th2) \ (RAG s)^+" and th2_r: "th2 \ readys s" @@ -1403,7 +1475,7 @@ proof - { assume neq: "th1 \ th2" hence "Th th1 \ Th th2" by simp - from unique_chain [OF _ th1_d th2_d this] and unique_RAG [OF vt] + from unique_chain [OF _ th1_d th2_d this] and unique_RAG have "(Th th1, Th th2) \ (RAG s)\<^sup>+ \ (Th th2, Th th1) \ (RAG s)\<^sup>+" by auto hence "False" proof @@ -1427,6 +1499,8 @@ qed } thus ?thesis by auto qed + +end lemma step_holdents_p_add: @@ -1450,13 +1524,11 @@ qed -lemma finite_holding: - fixes s th cs - assumes vt: "vt s" +lemma (in valid_trace) finite_holding : shows "finite (holdents s th)" proof - let ?F = "\ (x, y). the_cs x" - from finite_RAG [OF vt] + from finite_RAG have "finite (RAG s)" . hence "finite (?F `(RAG s))" by simp moreover have "{cs . (Cs cs, Th th) \ RAG s} \ \" @@ -1476,13 +1548,17 @@ assumes vtv: "vt (V thread cs#s)" shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread" proof - + from vtv interpret vt_s: valid_trace s + by (cases, unfold_locales, simp) + from vtv interpret vt_v: valid_trace "V thread cs#s" + by (unfold_locales, simp) from step_back_step[OF vtv] have cs_in: "cs \ holdents s thread" apply (cases, unfold holdents_test s_RAG_def, simp) by (unfold cs_holding_def s_holding_def wq_def, auto) moreover have cs_not_in: "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" - apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) + apply (insert vt_s.wq_distinct[of cs]) apply (unfold holdents_test, unfold step_RAG_v[OF vtv], auto simp:next_th_def) proof - @@ -1536,7 +1612,7 @@ moreover have "card \ = Suc (card ((holdents (V thread cs#s) thread) - {cs}))" proof(rule card_insert) - from finite_holding [OF vtv] + from vt_v.finite_holding show " finite (holdents (V thread cs # s) thread)" . qed moreover from cs_not_in @@ -1544,20 +1620,22 @@ ultimately show ?thesis by (simp add:cntCS_def) qed +context valid_trace +begin + text {* (* ddd *) \noindent The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} of one particular thread. *} lemma cnp_cnv_cncs: - fixes s th - assumes vt: "vt s" shows "cntP s th = cntV s th + (if (th \ readys s \ th \ threads s) then cntCS s th else cntCS s th + 1)" proof - from vt show ?thesis proof(induct arbitrary:th) case (vt_cons s e) + interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp) assume vt: "vt s" and ih: "\th. cntP s th = cntV s th + (if (th \ readys s \ th \ threads s) then cntCS s th else cntCS s th + 1)" @@ -1571,7 +1649,7 @@ proof - { fix cs assume "thread \ set (wq s cs)" - from wq_threads [OF vt this] have "thread \ threads s" . + from vt_s.wq_threads [OF this] have "thread \ threads s" . with not_in have "False" by simp } with eq_e have eq_readys: "readys (e#s) = readys s \ {thread}" by (auto simp:readys_def threads.simps s_waiting_def @@ -1632,6 +1710,8 @@ and is_runing: "thread \ runing s" and no_dep: "(Cs cs, Th thread) \ (RAG s)\<^sup>+" from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto + then interpret vt_p: valid_trace "(P thread cs#s)" + by (unfold_locales, simp) show ?thesis proof - { have hh: "\ A B C. (B = C) \ (A \ B) = (A \ C)" by blast @@ -1679,7 +1759,7 @@ have "?L = insert cs ?R" by auto moreover have "card \ = Suc (card (?R - {cs}))" proof(rule card_insert) - from finite_holding [OF vt, of thread] + from vt_s.finite_holding [of thread] show " finite {cs. (Cs cs, Th thread) \ RAG s}" by (unfold holdents_test, simp) qed @@ -1718,7 +1798,7 @@ ultimately have "th = hd (wq (e#s) cs)" by blast with eq_wq have "th = hd (wq s cs @ [th])" by simp hence "th = hd (wq s cs)" using False by auto - with False eq_wq wq_distinct [OF vtp, of cs] + with False eq_wq vt_p.wq_distinct [of cs] show False by (fold eq_e, auto) qed moreover from is_runing have "th \ threads (e#s)" @@ -1737,6 +1817,7 @@ next case (thread_V thread cs) from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto + then interpret vt_v: valid_trace "(V thread cs # s)" by (unfold_locales, simp) assume eq_e: "e = V thread cs" and is_runing: "thread \ runing s" and hold: "holding s thread cs" @@ -1746,8 +1827,9 @@ have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e) have eq_set: "set (SOME q. distinct q \ set q = set rest) = set rest" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq - show "distinct rest \ set rest = set rest" by auto + from vt_v.wq_distinct[of cs] and eq_wq + show "distinct rest \ set rest = set rest" + by (metis distinct.simps(2) vt_s.wq_distinct) next show "\x. distinct x \ set x = set rest \ set x = set rest" by auto @@ -1782,8 +1864,9 @@ proof - assume "thread \ set (SOME q. distinct q \ set q = set rest)" with eq_set have "thread \ set rest" by simp - with wq_distinct[OF step_back_vt[OF vtv], of cs] - and eq_wq show False by auto + with vt_v.wq_distinct[of cs] + and eq_wq show False + by (metis distinct.simps(2) vt_s.wq_distinct) qed thus ?thesis by (simp add:wq_def s_waiting_def) qed @@ -1819,7 +1902,7 @@ case False have "(th \ readys (e # s)) = (th \ readys s)" apply (insert step_back_vt[OF vtv]) - by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto) + by (simp add: False eq_e eq_wq neq_th vt_s.readys_v_eq) moreover have "cntCS (e#s) th = cntCS s th" apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto) proof - @@ -1838,7 +1921,7 @@ " by simp moreover have "(SOME q. distinct q \ set q = set rest) \ []" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq + from vt_s.wq_distinct[ of cs] and eq_wq show "distinct rest \ set rest = set rest" by auto next fix x assume "distinct x \ set x = set rest" @@ -1870,7 +1953,7 @@ have "\ th \ readys s" apply (auto simp:readys_def s_waiting_def) apply (rule_tac x = cs in exI, auto) - by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp add: wq_def) + by (insert vt_s.wq_distinct[of cs], auto simp add: wq_def) moreover from eq_wq and th_in and neq_hd have "\ (th \ readys (e # s))" @@ -1885,7 +1968,7 @@ apply (unfold eq_e step_RAG_v[OF vtv], auto simp:next_th_def eq_set s_RAG_def holdents_test wq_def Let_def cs_holding_def) - by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def) + by (insert vt_s.wq_distinct[of cs], auto simp:wq_def) thus ?thesis by (simp add:cntCS_def) qed moreover note ih eq_cnp eq_cnv eq_threads @@ -1902,7 +1985,7 @@ assume eq_wq: "wq_fun (schs s) cs = thread # rest" and t_in: "?t \ set rest" show "?t \ threads s" - proof(rule wq_threads[OF step_back_vt[OF vtv]]) + proof(rule vt_s.wq_threads) from eq_wq and t_in show "?t \ set (wq s cs)" by (auto simp:wq_def) qed @@ -1915,7 +1998,7 @@ show "?t = hd (wq_fun (schs s) csa)" proof - { assume neq_hd': "?t \ hd (wq_fun (schs s) csa)" - from wq_distinct[OF step_back_vt[OF vtv], of cs] and + from vt_s.wq_distinct[of cs] and eq_wq[folded wq_def] and t_in eq_wq have "?t \ thread" by auto with eq_wq and t_in @@ -1924,7 +2007,7 @@ from t_in' neq_hd' have w2: "waiting s ?t csa" by (auto simp:s_waiting_def wq_def) - from waiting_unique[OF step_back_vt[OF vtv] w1 w2] + from vt_s.waiting_unique[OF w1 w2] and neq_cs have "False" by auto } thus ?thesis by auto qed @@ -1942,7 +2025,7 @@ proof - from th_in eq_wq have "th \ set (wq s cs)" by simp - from wq_threads [OF step_back_vt[OF vtv] this] + from vt_s.wq_threads [OF this] show ?thesis . qed ultimately show ?thesis using ih by auto @@ -1961,7 +2044,7 @@ have "?B \ ((\ (x, y). the_cs x) ` RAG s)" apply (auto simp:image_def) by (rule_tac x = "(Cs x, Th th)" in bexI, auto) - with finite_RAG[OF step_back_vt[OF vtv]] + with vt_s.finite_RAG show "finite {cs. (Cs cs, Th th) \ RAG s}" by (auto intro:finite_subset) next show "cs \ {cs. (Cs cs, Th th) \ RAG s}" @@ -2022,14 +2105,14 @@ qed lemma not_thread_cncs: - fixes th s - assumes vt: "vt s" - and not_in: "th \ threads s" + assumes not_in: "th \ threads s" shows "cntCS s th = 0" proof - from vt not_in show ?thesis proof(induct arbitrary:th) case (vt_cons s e th) + interpret vt_s: valid_trace s using vt_cons(1) + by (unfold_locales, simp) assume vt: "vt s" and ih: "\th. th \ threads s \ cntCS s th = 0" and stp: "step s e" @@ -2097,7 +2180,10 @@ by (simp add:runing_def readys_def) ultimately show ?thesis by auto qed - from assms thread_V vt stp ih have vtv: "vt (V thread cs#s)" by auto + from assms thread_V vt stp ih + have vtv: "vt (V thread cs#s)" by auto + then interpret vt_v: valid_trace "(V thread cs#s)" + by (unfold_locales, simp) from hold obtain rest where eq_wq: "wq s cs = thread # rest" by (case_tac "wq s cs", auto simp: wq_def s_holding_def) @@ -2109,15 +2195,18 @@ and ni: "hd (SOME q. distinct q \ set q = set rest) \ threads s" (is "?t \ threads s") have "?t \ set rest" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq - show "distinct rest \ set rest = set rest" by auto + from vt_v.wq_distinct[of cs] and eq_wq + show "distinct rest \ set rest = set rest" + by (metis distinct.simps(2) vt_s.wq_distinct) next fix x assume "distinct x \ set x = set rest" with ne show "hd x \ set rest" by (cases x, auto) qed with eq_wq have "?t \ set (wq s cs)" by simp - from wq_threads[OF step_back_vt[OF vtv], OF this] and ni - show False by auto + from vt_s.wq_threads[OF this] and ni + show False + using `hd (SOME q. distinct q \ set q = set rest) \ set (wq s cs)` + ni vt_s.wq_threads by blast qed moreover note neq_th eq_wq ultimately have "cntCS (e # s) th = cntCS s th" @@ -2146,13 +2235,16 @@ qed qed +end + lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs" by (auto simp:s_waiting_def cs_waiting_def wq_def) +context valid_trace +begin + lemma dm_RAG_threads: - fixes th s - assumes vt: "vt s" - and in_dom: "(Th th) \ Domain (RAG s)" + assumes in_dom: "(Th th) \ Domain (RAG s)" shows "th \ threads s" proof - from in_dom obtain n where "(Th th, n) \ RAG s" by auto @@ -2160,9 +2252,11 @@ ultimately have "(Th th, Cs cs) \ RAG s" by simp hence "th \ set (wq s cs)" by (unfold s_RAG_def, auto simp:cs_waiting_def) - from wq_threads [OF vt this] show ?thesis . + from wq_threads [OF this] show ?thesis . qed +end + lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th" unfolding cp_def wq_def apply(induct s rule: schs.induct) @@ -2177,11 +2271,11 @@ apply(simp add: Let_def) done -(* FIXME: NOT NEEDED *) +context valid_trace +begin + lemma runing_unique: - fixes th1 th2 s - assumes vt: "vt s" - and runing_1: "th1 \ runing s" + assumes runing_1: "th1 \ runing s" and runing_2: "th2 \ runing s" shows "th1 = th2" proof - @@ -2210,7 +2304,7 @@ by (rule_tac x = "(Th x, Th th1)" in bexI, auto) moreover have "finite \" proof - - from finite_RAG[OF vt] have "finite (RAG s)" . + from finite_RAG have "finite (RAG s)" . hence "finite ((RAG (wq s))\<^sup>+)" apply (unfold finite_trancl) by (auto simp: s_RAG_def cs_RAG_def wq_def) @@ -2254,7 +2348,7 @@ by (rule_tac x = "(Th x, Th th2)" in bexI, auto) moreover have "finite \" proof - - from finite_RAG[OF vt] have "finite (RAG s)" . + from finite_RAG have "finite (RAG s)" . hence "finite ((RAG (wq s))\<^sup>+)" apply (unfold finite_trancl) by (auto simp: s_RAG_def cs_RAG_def wq_def) @@ -2289,7 +2383,7 @@ apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) by (auto simp:Domain_def) hence "(Th th1') \ Domain (RAG s)" by (simp add:trancl_domain) - from dm_RAG_threads[OF vt this] show ?thesis . + from dm_RAG_threads[OF this] show ?thesis . next assume "th1' = th1" with runing_1 show ?thesis @@ -2304,7 +2398,7 @@ apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) by (auto simp:Domain_def) hence "(Th th2') \ Domain (RAG s)" by (simp add:trancl_domain) - from dm_RAG_threads[OF vt this] show ?thesis . + from dm_RAG_threads[OF this] show ?thesis . next assume "th2' = th2" with runing_2 show ?thesis @@ -2366,7 +2460,7 @@ from th1'_in have h2: "(Th th1', Th th1) \ (RAG s)^+" by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) show ?thesis - proof(rule dchain_unique[OF vt h1 _ h2, symmetric]) + proof(rule dchain_unique[OF h1 _ h2, symmetric]) from runing_1 show "th1 \ readys s" by (simp add:runing_def) from runing_2 show "th2 \ readys s" by (simp add:runing_def) qed @@ -2375,7 +2469,7 @@ qed -lemma "vt s \ card (runing s) \ 1" +lemma "card (runing s) \ 1" apply(subgoal_tac "finite (runing s)") prefer 2 apply (metis finite_nat_set_iff_bounded lessI runing_unique) @@ -2389,6 +2483,9 @@ apply(auto) done +end + + lemma create_pre: assumes stp: "step s e" and not_in: "th \ threads s" @@ -2447,28 +2544,35 @@ from that [OF this] show ?thesis . qed +context valid_trace +begin + lemma cnp_cnv_eq: - fixes th s - assumes "vt s" - and "th \ threads s" + assumes "th \ threads s" shows "cntP s th = cntV s th" - by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs) + using assms + using cnp_cnv_cncs not_thread_cncs by auto + +end + lemma eq_RAG: "RAG (wq s) = RAG s" by (unfold cs_RAG_def s_RAG_def, auto) +context valid_trace +begin + lemma count_eq_dependants: - assumes vt: "vt s" - and eq_pv: "cntP s th = cntV s th" + assumes eq_pv: "cntP s th = cntV s th" shows "dependants (wq s) th = {}" proof - - from cnp_cnv_cncs[OF vt] and eq_pv + from cnp_cnv_cncs and eq_pv have "cntCS s th = 0" by (auto split:if_splits) moreover have "finite {cs. (Cs cs, Th th) \ RAG s}" proof - - from finite_holding[OF vt, of th] show ?thesis + from finite_holding[of th] show ?thesis by (simp add:holdents_test) qed ultimately have h: "{cs. (Cs cs, Th th) \ RAG s} = {}" @@ -2492,8 +2596,6 @@ qed lemma dependants_threads: - fixes s th - assumes vt: "vt s" shows "dependants (wq s) th \ threads s" proof { fix th th' @@ -2505,7 +2607,7 @@ with trancl_domain have "(Th th) \ Domain (RAG (wq s))" by simp thus ?thesis using eq_RAG by simp qed - from dm_RAG_threads[OF vt this] + from dm_RAG_threads[OF this] have "th \ threads s" . } note hh = this fix th1 @@ -2516,10 +2618,10 @@ qed lemma finite_threads: - assumes vt: "vt s" shows "finite (threads s)" -using vt -by (induct) (auto elim: step.cases) +using vt by (induct) (auto elim: step.cases) + +end lemma Max_f_mono: assumes seq: "A \ B" @@ -2534,9 +2636,11 @@ from fnt and seq show "finite (f ` B)" by auto qed +context valid_trace +begin + lemma cp_le: - assumes vt: "vt s" - and th_in: "th \ threads s" + assumes th_in: "th \ threads s" shows "cp s th \ Max ((\ th. (preced th s)) ` threads s)" proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def) show "Max ((\th. preced th s) ` ({th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+})) @@ -2545,20 +2649,19 @@ proof(rule Max_f_mono) show "{th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} \ {}" by simp next - from finite_threads [OF vt] + from finite_threads show "finite (threads s)" . next from th_in show "{th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} \ threads s" apply (auto simp:Domain_def) - apply (rule_tac dm_RAG_threads[OF vt]) + apply (rule_tac dm_RAG_threads) apply (unfold trancl_domain [of "RAG s", symmetric]) by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def) qed qed lemma le_cp: - assumes vt: "vt s" shows "preced th s \ cp s th" proof(unfold cp_eq_cpreced preced_def cpreced_def, simp) show "Prc (priority th s) (last_set th s) @@ -2579,7 +2682,7 @@ by (rule_tac x = "(Th x, Th th)" in bexI, auto) moreover have "finite \" proof - - from finite_RAG[OF vt] have "finite (RAG s)" . + from finite_RAG have "finite (RAG s)" . hence "finite ((RAG (wq s))\<^sup>+)" apply (unfold finite_trancl) by (auto simp: s_RAG_def cs_RAG_def wq_def) @@ -2599,7 +2702,6 @@ qed lemma max_cp_eq: - assumes vt: "vt s" shows "Max ((cp s) ` threads s) = Max ((\ th. (preced th s)) ` threads s)" (is "?l = ?r") proof(cases "threads s = {}") @@ -2609,26 +2711,26 @@ case False have "?l \ ((cp s) ` threads s)" proof(rule Max_in) - from finite_threads[OF vt] + from finite_threads show "finite (cp s ` threads s)" by auto next from False show "cp s ` threads s \ {}" by auto qed then obtain th where th_in: "th \ threads s" and eq_l: "?l = cp s th" by auto - have "\ \ ?r" by (rule cp_le[OF vt th_in]) + have "\ \ ?r" by (rule cp_le[OF th_in]) moreover have "?r \ cp s th" (is "Max (?f ` ?A) \ cp s th") proof - have "?r \ (?f ` ?A)" proof(rule Max_in) - from finite_threads[OF vt] + from finite_threads show " finite ((\th. preced th s) ` threads s)" by auto next from False show " (\th. preced th s) ` threads s \ {}" by auto qed then obtain th' where th_in': "th' \ ?A " and eq_r: "?r = ?f th'" by auto - from le_cp [OF vt, of th'] eq_r + from le_cp [of th'] eq_r have "?r \ cp s th'" by auto moreover have "\ \ cp s th" proof(fold eq_l) @@ -2637,7 +2739,7 @@ from th_in' show "cp s th' \ cp s ` threads s" by auto next - from finite_threads[OF vt] + from finite_threads show "finite (cp s ` threads s)" by auto qed qed @@ -2647,23 +2749,22 @@ qed lemma max_cp_readys_threads_pre: - assumes vt: "vt s" - and np: "threads s \ {}" + assumes np: "threads s \ {}" shows "Max (cp s ` readys s) = Max (cp s ` threads s)" -proof(unfold max_cp_eq[OF vt]) +proof(unfold max_cp_eq) show "Max (cp s ` readys s) = Max ((\th. preced th s) ` threads s)" proof - let ?p = "Max ((\th. preced th s) ` threads s)" let ?f = "(\th. preced th s)" have "?p \ ((\th. preced th s) ` threads s)" proof(rule Max_in) - from finite_threads[OF vt] show "finite (?f ` threads s)" by simp + from finite_threads show "finite (?f ` threads s)" by simp next from np show "?f ` threads s \ {}" by simp qed then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \ threads s" by (auto simp:Image_def) - from th_chain_to_ready [OF vt tm_in] + from th_chain_to_ready [OF tm_in] have "tm \ readys s \ (\th'. th' \ readys s \ (Th tm, Th th') \ (RAG s)\<^sup>+)" . thus ?thesis proof @@ -2672,7 +2773,7 @@ and tm_chain:"(Th tm, Th th') \ (RAG s)\<^sup>+" by auto have "cp s th' = ?f tm" proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI) - from dependants_threads[OF vt] finite_threads[OF vt] + from dependants_threads finite_threads show "finite ((\th. preced th s) ` ({th'} \ dependants (wq s) th'))" by (auto intro:finite_subset) next @@ -2680,10 +2781,10 @@ from tm_max have " preced tm s = Max ((\th. preced th s) ` threads s)" . moreover have "p \ \" proof(rule Max_ge) - from finite_threads[OF vt] + from finite_threads show "finite ((\th. preced th s) ` threads s)" by simp next - from p_in and th'_in and dependants_threads[OF vt, of th'] + from p_in and th'_in and dependants_threads[of th'] show "p \ (\th. preced th s) ` threads s" by (auto simp:readys_def) qed @@ -2710,18 +2811,18 @@ apply (unfold cp_eq_cpreced cpreced_def) apply (rule Max_mono) proof - - from dependants_threads [OF vt, of th1] th1_in + from dependants_threads [of th1] th1_in show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ (\th. preced th s) ` threads s" by (auto simp:readys_def) next show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ {}" by simp next - from finite_threads[OF vt] + from finite_threads show " finite ((\th. preced th s) ` threads s)" by simp qed next - from finite_threads[OF vt] + from finite_threads show "finite (cp s ` readys s)" by (auto simp:readys_def) next from th'_in @@ -2741,16 +2842,16 @@ assume hy' : "y' \ ((\th. preced th s) ` dependants (wq s) tm)" have "y' \ preced tm s" proof(unfold tm_max, rule Max_ge) - from hy' dependants_threads[OF vt, of tm] + from hy' dependants_threads[of tm] show "y' \ (\th. preced th s) ` threads s" by auto next - from finite_threads[OF vt] + from finite_threads show "finite ((\th. preced th s) ` threads s)" by simp qed } with hy show ?thesis by auto qed next - from dependants_threads[OF vt, of tm] finite_threads[OF vt] + from dependants_threads[of tm] finite_threads show "finite ((\th. preced th s) ` ({tm} \ dependants (wq s) tm))" by (auto intro:finite_subset) next @@ -2761,7 +2862,7 @@ proof(rule Max_eqI) from tm_ready show "cp s tm \ cp s ` readys s" by simp next - from finite_threads[OF vt] + from finite_threads show "finite (cp s ` readys s)" by (auto simp:readys_def) next fix y assume "y \ cp s ` readys s" @@ -2771,13 +2872,13 @@ apply(unfold cp_eq_p h) apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono) proof - - from finite_threads[OF vt] + from finite_threads show "finite ((\th. preced th s) ` threads s)" by simp next show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ {}" by simp next - from dependants_threads[OF vt, of th1] th1_readys + from dependants_threads[of th1] th1_readys show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ (\th. preced th s) ` threads s" by (auto simp:readys_def) @@ -2794,7 +2895,6 @@ there must be one inside it has the maximum precedence of the whole system. *} lemma max_cp_readys_threads: - assumes vt: "vt s" shows "Max (cp s ` readys s) = Max (cp s ` threads s)" proof(cases "threads s = {}") case True @@ -2802,9 +2902,10 @@ by (auto simp:readys_def) next case False - show ?thesis by (rule max_cp_readys_threads_pre[OF vt False]) + show ?thesis by (rule max_cp_readys_threads_pre[OF False]) qed +end lemma eq_holding: "holding (wq s) th cs = holding s th cs" apply (unfold s_holding_def cs_holding_def wq_def, simp) @@ -2836,13 +2937,14 @@ apply(auto) done +context valid_trace +begin + lemma detached_intro: - fixes s th - assumes vt: "vt s" - and eq_pv: "cntP s th = cntV s th" + assumes eq_pv: "cntP s th = cntV s th" shows "detached s th" proof - - from cnp_cnv_cncs[OF vt] + from cnp_cnv_cncs have eq_cnt: "cntP s th = cntV s th + (if th \ readys s \ th \ threads s then cntCS s th else cntCS s th + 1)" . hence cncs_zero: "cntCS s th = 0" @@ -2852,14 +2954,14 @@ thus ?thesis proof assume "th \ threads s" - with range_in[OF vt] dm_RAG_threads[OF vt] + with range_in dm_RAG_threads show ?thesis by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff) next assume "th \ readys s" moreover have "Th th \ Range (RAG s)" proof - - from card_0_eq [OF finite_holding [OF vt]] and cncs_zero + from card_0_eq [OF finite_holding] and cncs_zero have "holdents s th = {}" by (simp add:cntCS_def) thus ?thesis @@ -2874,12 +2976,10 @@ qed lemma detached_elim: - fixes s th - assumes vt: "vt s" - and dtc: "detached s th" + assumes dtc: "detached s th" shows "cntP s th = cntV s th" proof - - from cnp_cnv_cncs[OF vt] + from cnp_cnv_cncs have eq_pv: " cntP s th = cntV s th + (if th \ readys s \ th \ threads s then cntCS s th else cntCS s th + 1)" . have cncs_z: "cntCS s th = 0" @@ -2904,11 +3004,11 @@ qed lemma detached_eq: - fixes s th - assumes vt: "vt s" shows "(detached s th) = (cntP s th = cntV s th)" by (insert vt, auto intro:detached_intro detached_elim) +end + text {* The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived from the concise and miniature model of PIP given in PrioGDef.thy. @@ -2923,5 +3023,29 @@ shows "th1 = th2" using assms by (unfold next_th_def, auto) - +lemma birth_time_lt: "s \ [] \ last_set th s < length s" + apply (induct s, simp) +proof - + fix a s + assume ih: "s \ [] \ last_set th s < length s" + and eq_as: "a # s \ []" + show "last_set th (a # s) < length (a # s)" + proof(cases "s \ []") + case False + from False show ?thesis + by (cases a, auto simp:last_set.simps) + next + case True + from ih [OF True] show ?thesis + by (cases a, auto simp:last_set.simps) + qed +qed + +lemma th_in_ne: "th \ threads s \ s \ []" + by (induct s, auto simp:threads.simps) + +lemma preced_tm_lt: "th \ threads s \ preced th s = Prc x y \ y < length s" + apply (drule_tac th_in_ne) + by (unfold preced_def, auto intro: birth_time_lt) + end diff -r 031d2ae9c9b8 -r b620a2a0806a PrioG.thy~ --- a/PrioG.thy~ Tue Dec 22 23:13:31 2015 +0800 +++ b/PrioG.thy~ Wed Jan 06 20:46:14 2016 +0800 @@ -2,6 +2,20 @@ imports PrioGDef begin +locale valid_trace = + fixes s + assumes vt : "vt s" + +locale valid_trace_e = valid_trace + + fixes e + assumes vt_e: "vt (e#s)" +begin + +lemma pip_e: "PIP s e" + using vt_e by (cases, simp) + +end + lemma runing_ready: shows "runing s \ readys s" unfolding runing_def readys_def @@ -16,8 +30,30 @@ "cs \ cs' \ wq (V thread cs#s) cs' = wq s cs'" by (auto simp:wq_def Let_def cp_def split:list.splits) -lemma wq_distinct: "vt s \ distinct (wq s cs)" -proof(erule_tac vt.induct, simp add:wq_def) +context valid_trace +begin + +lemma ind [consumes 0, case_names Nil Cons, induct type]: + assumes "PP []" + and "(\s e. valid_trace s \ valid_trace (e#s) \ + PP s \ PIP s e \ PP (e # s))" + shows "PP s" +proof(rule vt.induct[OF vt]) + from assms(1) show "PP []" . +next + fix s e + assume h: "vt s" "PP s" "PIP s e" + show "PP (e # s)" + proof(cases rule:assms(2)) + from h(1) show v1: "valid_trace s" by (unfold_locales, simp) + next + from h(1,3) have "vt (e#s)" by auto + thus "valid_trace (e # s)" by (unfold_locales, simp) + qed (insert h, auto) +qed + +lemma wq_distinct: "distinct (wq s cs)" +proof(rule ind, simp add:wq_def) fix s e assume h1: "step s e" and h2: "distinct (wq s cs)" @@ -51,6 +87,12 @@ qed qed +end + + +context valid_trace_e +begin + text {* The following lemma shows that only the @{text "P"} operation can add new thread into waiting queues. @@ -59,9 +101,7 @@ *} lemma block_pre: - fixes thread cs s - assumes vt_e: "vt (e#s)" - and s_ni: "thread \ set (wq s cs)" + assumes s_ni: "thread \ set (wq s cs)" and s_i: "thread \ set (wq (e#s) cs)" shows "e = P thread cs" proof - @@ -85,7 +125,7 @@ by (auto simp:wq_def Let_def split:if_splits) next case (V th cs) - with assms show ?thesis + with vt_e assms show ?thesis apply (auto simp:wq_def Let_def split:if_splits) proof - fix q qs @@ -98,7 +138,7 @@ proof - have "set (SOME q. distinct q \ set q = set qs) = set qs" proof(rule someI2) - from wq_distinct [OF step_back_vt[OF vt], of cs] + from wq_distinct [of cs] and h2[symmetric, folded wq_def] show "distinct qs \ set qs = set qs" by auto next @@ -112,6 +152,8 @@ qed qed +end + text {* The following lemmas is also obvious and shallow. It says that only running thread can request for a critical resource @@ -126,7 +168,6 @@ by auto lemma abs1: - fixes e es assumes ein: "e \ set es" and neq: "hd es \ hd (es @ [x])" shows "False" @@ -141,15 +182,17 @@ inductive_cases evt_cons: "vt (a#s)" +context valid_trace_e +begin + lemma abs2: - assumes vt: "vt (e#s)" - and inq: "thread \ set (wq s cs)" + assumes inq: "thread \ set (wq s cs)" and nh: "thread = hd (wq s cs)" and qt: "thread \ hd (wq (e#s) cs)" and inq': "thread \ set (wq (e#s) cs)" shows "False" proof - - from assms show "False" + from vt_e assms show "False" apply (cases e) apply ((simp split:if_splits add:Let_def wq_def)[1])+ apply (insert abs1, fast)[1] @@ -161,13 +204,13 @@ and eq_wq: "wq_fun (schs s) cs = thread # qs" show "False" proof - - from wq_distinct[OF step_back_vt[OF vt], of cs] + from wq_distinct[of cs] and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp moreover have "thread \ set qs" proof - have "set (SOME q. distinct q \ set q = set qs) = set qs" proof(rule someI2) - from wq_distinct [OF step_back_vt[OF vt], of cs] + from wq_distinct [of cs] and eq_wq [folded wq_def] show "distinct qs \ set qs = set qs" by auto next @@ -181,28 +224,33 @@ qed qed -lemma vt_moment: "\ t. \vt s\ \ vt (moment t s)" -proof(induct s, simp) - fix a s t - assume h: "\t.\vt s\ \ vt (moment t s)" - and vt_a: "vt (a # s)" - show "vt (moment t (a # s))" - proof(cases "t \ length (a#s)") +end + +context valid_trace +begin + +lemma vt_moment: "\ t. vt (moment t s)" +proof(induct rule:ind) + case Nil + thus ?case by (simp add:vt_nil) +next + case (Cons s e t) + show ?case + proof(cases "t \ length (e#s)") case True - from True have "moment t (a#s) = a#s" by simp - with vt_a show ?thesis by simp + from True have "moment t (e#s) = e#s" by simp + thus ?thesis using Cons + by (simp add:valid_trace_def) next case False - hence le_t1: "t \ length s" by simp - from vt_a have "vt s" - by (erule_tac evt_cons, simp) - from h [OF this] have "vt (moment t s)" . - moreover have "moment t (a#s) = moment t s" + from Cons have "vt (moment t s)" by simp + moreover have "moment t (e#s) = moment t s" proof - - from moment_app [OF le_t1, of "[a]"] + from False have "t \ length s" by simp + from moment_app [OF this, of "[e]"] show ?thesis by simp qed - ultimately show ?thesis by auto + ultimately show ?thesis by simp qed qed @@ -244,9 +292,7 @@ *} lemma waiting_unique_pre: - fixes cs1 cs2 s thread - assumes vt: "vt s" - and h11: "thread \ set (wq s cs1)" + assumes h11: "thread \ set (wq s cs1)" and h12: "thread \ hd (wq s cs1)" assumes h21: "thread \ set (wq s cs2)" and h22: "thread \ hd (wq s cs2)" @@ -282,25 +328,26 @@ from nn2 [rule_format, OF this] and eq_m have h1: "thread \ set (wq (e#moment t2 s) cs2)" and h2: "thread \ hd (wq (e#moment t2 s) cs2)" by auto - have vt_e: "vt (e#moment t2 s)" + have "vt (e#moment t2 s)" proof - - from vt_moment [OF vt] + from vt_moment have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed + then interpret vt_e: valid_trace_e "moment t2 s" "e" + by (unfold_locales, auto, cases, simp) have ?thesis proof(cases "thread \ set (wq (moment t2 s) cs2)") case True from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)" - by auto - thm abs2 - from abs2 [OF vt_e True eq_th h2 h1] + by auto + from vt_e.abs2 [OF True eq_th h2 h1] show ?thesis by auto next case False - from block_pre [OF vt_e False h1] + from vt_e.block_pre[OF False h1] have "e = P thread cs2" . - with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp + with vt_e.vt_e have "vt ((P thread cs2)# moment t2 s)" by simp from p_pre [OF this] have "thread \ runing (moment t2 s)" by simp with runing_ready have "thread \ readys (moment t2 s)" by auto with nn1 [rule_format, OF lt12] @@ -316,24 +363,26 @@ from nn1 [rule_format, OF this] and eq_m have h1: "thread \ set (wq (e#moment t1 s) cs1)" and h2: "thread \ hd (wq (e#moment t1 s) cs1)" by auto - have vt_e: "vt (e#moment t1 s)" + have "vt (e#moment t1 s)" proof - - from vt_moment [OF vt] + from vt_moment have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed + then interpret vt_e: valid_trace_e "moment t1 s" e + by (unfold_locales, auto, cases, auto) have ?thesis proof(cases "thread \ set (wq (moment t1 s) cs1)") case True from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)" by auto - from abs2 [OF vt_e True eq_th h2 h1] + from vt_e.abs2 True eq_th h2 h1 show ?thesis by auto next case False - from block_pre [OF vt_e False h1] + from vt_e.block_pre [OF False h1] have "e = P thread cs1" . - with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp + with vt_e.vt_e have "vt ((P thread cs1)# moment t1 s)" by simp from p_pre [OF this] have "thread \ runing (moment t1 s)" by simp with runing_ready have "thread \ readys (moment t1 s)" by auto with nn2 [rule_format, OF lt12] @@ -351,20 +400,22 @@ h2: "thread \ hd (wq (e#moment t1 s) cs1)" by auto have vt_e: "vt (e#moment t1 s)" proof - - from vt_moment [OF vt] + from vt_moment have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed + then interpret vt_e: valid_trace_e "moment t1 s" e + by (unfold_locales, auto, cases, auto) have ?thesis proof(cases "thread \ set (wq (moment t1 s) cs1)") case True from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)" by auto - from abs2 [OF vt_e True eq_th h2 h1] + from vt_e.abs2 [OF True eq_th h2 h1] show ?thesis by auto next case False - from block_pre [OF vt_e False h1] + from vt_e.block_pre [OF False h1] have eq_e1: "e = P thread cs1" . have lt_t3: "t1 < ?t3" by simp with eqt12 have "t2 < ?t3" by simp @@ -377,17 +428,21 @@ from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)" by auto from vt_e and eqt12 have "vt (e#moment t2 s)" by simp - from abs2 [OF this True eq_th h2 h1] + then interpret vt_e2: valid_trace_e "moment t2 s" e + by (unfold_locales, auto, cases, auto) + from vt_e2.abs2 [OF True eq_th h2 h1] show ?thesis . next case False - have vt_e: "vt (e#moment t2 s)" + have "vt (e#moment t2 s)" proof - - from vt_moment [OF vt] eqt12 + from vt_moment eqt12 have "vt (moment (Suc t2) s)" by auto with eq_m eqt12 show ?thesis by simp qed - from block_pre [OF vt_e False h1] + then interpret vt_e2: valid_trace_e "moment t2 s" e + by (unfold_locales, auto, cases, auto) + from vt_e2.block_pre [OF False h1] have "e = P thread cs2" . with eq_e1 neq12 show ?thesis by auto qed @@ -401,15 +456,15 @@ *} lemma waiting_unique: - fixes s cs1 cs2 - assumes "vt s" - and "waiting s th cs1" + assumes "waiting s th cs1" and "waiting s th cs2" shows "cs1 = cs2" using waiting_unique_pre assms unfolding wq_def s_waiting_def by auto +end + (* not used *) text {* Every thread can only be blocked on one critical resource, @@ -417,13 +472,10 @@ This fact is much more easier according to our definition. *} lemma held_unique: - fixes s::"state" - assumes "holding s th1 cs" + assumes "holding (s::event list) th1 cs" and "holding s th2 cs" shows "th1 = th2" -using assms -unfolding s_holding_def -by auto + by (insert assms, unfold s_holding_def, auto) lemma last_set_lt: "th \ threads s \ last_set th s < length s" @@ -642,6 +694,8 @@ assume vt: "vt (V th cs # s)" and nw: "\ waiting (wq (V th cs # s)) t c" and wt: "waiting (wq s) t c" + from vt interpret vt_v: valid_trace_e s "V th cs" + by (cases, unfold_locales, simp) show "next_th s th cs t \ cs = c" proof(cases "cs = c") case False @@ -659,7 +713,7 @@ and eq_wq: "wq_fun (schs s) cs = a # list" have " set (SOME q. distinct q \ set q = set list) = set list" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] + from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def] show "distinct list \ set list = set list" by auto next show "\x. distinct x \ set x = set list \ set x = set list" @@ -673,7 +727,7 @@ and eq_wq: "wq_fun (schs s) cs = a # list" have " set (SOME q. distinct q \ set q = set list) = set list" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] + from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def] show "distinct list \ set list = set list" by auto next show "\x. distinct x \ set x = set list \ set x = set list" @@ -704,6 +758,8 @@ proof - assume vt: "vt (V th cs # s)" and hd: "holding (wq (V th cs # s)) th cs" + from vt interpret vt_v: valid_trace_e s "V th cs" + by (cases, unfold_locales, simp+) from step_back_step [OF vt] and hd show "False" proof(cases) @@ -719,7 +775,7 @@ \ set (SOME q. distinct q \ set q = set list)" have "set (SOME q. distinct q \ set q = set list) = set list" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq + from vt_v.wq_distinct[of cs] and eq_wq show "distinct list \ set list = set list" by auto next show "\x. distinct x \ set x = set list \ set x = set list" @@ -727,7 +783,7 @@ qed moreover have "distinct (hd (SOME q. distinct q \ set q = set list) # list)" proof - - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq + from vt_v.wq_distinct[of cs] and eq_wq show ?thesis by auto qed moreover note eq_wq and hd_in @@ -747,9 +803,11 @@ and nrest: "rest \ []" and ni: "hd (SOME q. distinct q \ set q = set rest) \ set (SOME q. distinct q \ set q = set rest)" + from vt interpret vt_v: valid_trace_e s "V th cs" + by (cases, unfold_locales, simp+) have "(SOME q. distinct q \ set q = set rest) \ []" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq + from vt_v.wq_distinct[of cs] and eq_wq show "distinct rest \ set rest = set rest" by auto next fix x assume "distinct x \ set x = set rest" @@ -791,6 +849,8 @@ let ?s' = "(V th cs # s)" assume vt: "vt ?s'" and wt: "waiting (wq ?s') t c" + from vt interpret vt_v: valid_trace_e s "V th cs" + by (cases, unfold_locales, simp+) show "waiting (wq s) t c" proof(cases "c = cs") case False @@ -809,7 +869,7 @@ and eq_wq: "wq_fun (schs s) cs = a # list" have "set (SOME q. distinct q \ set q = set list) = set list" proof(rule someI2) - from wq_distinct [OF step_back_vt[OF vt], of cs] + from vt_v.wq_distinct [of cs] and eq_wq[folded wq_def] show "distinct list \ set list = set list" by auto next @@ -827,7 +887,7 @@ assume " t \ set (SOME q. distinct q \ set q = set list)" moreover have "\ = set list" proof(rule someI2) - from wq_distinct [OF step_back_vt[OF vt], of cs] + from vt_v.wq_distinct [of cs] and eq_wq[folded wq_def] show "distinct list \ set list = set list" by auto next @@ -836,7 +896,7 @@ qed ultimately show "t \ set list" by simp qed - with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def] + with eq_wq and vt_v.wq_distinct [of cs, unfolded wq_def] show False by auto qed qed @@ -885,19 +945,22 @@ lemma RAG_target_th: "(Th th, x) \ RAG (s::state) \ \ cs. x = Cs cs" by (unfold s_RAG_def, auto) +context valid_trace +begin + text {* The following lemma shows that @{text "RAG"} is acyclic. The overall structure is by induction on the formation of @{text "vt s"} and then case analysis on event @{text "e"}, where the non-trivial cases for those for @{text "V"} and @{text "P"} events. *} -lemma acyclic_RAG: - fixes s - assumes vt: "vt s" +lemma acyclic_RAG: shows "acyclic (RAG s)" -using assms +using vt proof(induct) case (vt_cons s e) + interpret vt_s: valid_trace s using vt_cons(1) + by (unfold_locales, simp) assume ih: "acyclic (RAG s)" and stp: "step s e" and vt: "vt s" @@ -949,8 +1012,8 @@ hence wt_th': "waiting s ?th' cs'" unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp hence "cs' = cs" - proof(rule waiting_unique [OF vt]) - from eq_wq wq_distinct[OF vt, of cs] + proof(rule vt_s.waiting_unique) + from eq_wq vt_s.wq_distinct[of cs] show "waiting s ?th' cs" apply (unfold s_waiting_def wq_def, auto) proof - @@ -958,7 +1021,7 @@ and eq_wq: "wq_fun (schs s) cs = th # rest" have "(SOME q. distinct q \ set q = set rest) \ []" proof(rule someI2) - from wq_distinct[OF vt, of cs] and eq_wq + from vt_s.wq_distinct[of cs] and eq_wq show "distinct rest \ set rest = set rest" unfolding wq_def by auto next fix x assume "distinct x \ set x = set rest" @@ -968,7 +1031,7 @@ set (SOME q. distinct q \ set q = set rest)" by auto moreover have "\ = set rest" proof(rule someI2) - from wq_distinct[OF vt, of cs] and eq_wq + from vt_s.wq_distinct[of cs] and eq_wq show "distinct rest \ set rest = set rest" unfolding wq_def by auto next show "\x. distinct x \ set x = set rest \ set x = set rest" by auto @@ -980,7 +1043,7 @@ and eq_wq: "wq s cs = hd (SOME q. distinct q \ set q = set rest) # rest" have "(SOME q. distinct q \ set q = set rest) \ []" proof(rule someI2) - from wq_distinct[OF vt, of cs] and eq_wq + from vt_s.wq_distinct[of cs] and eq_wq show "distinct rest \ set rest = set rest" by auto next fix x assume "distinct x \ set x = set rest" @@ -990,7 +1053,7 @@ set (SOME q. distinct q \ set q = set rest)" by auto moreover have "\ = set rest" proof(rule someI2) - from wq_distinct[OF vt, of cs] and eq_wq + from vt_s.wq_distinct[of cs] and eq_wq show "distinct rest \ set rest = set rest" by auto next show "\x. distinct x \ set x = set rest \ set x = set rest" by auto @@ -1066,14 +1129,14 @@ qed -lemma finite_RAG: - fixes s - assumes vt: "vt s" +lemma finite_RAG: shows "finite (RAG s)" proof - from vt show ?thesis proof(induct) case (vt_cons s e) + interpret vt_s: valid_trace s using vt_cons(1) + by (unfold_locales, simp) assume ih: "finite (RAG s)" and stp: "step s e" and vt: "vt s" @@ -1145,32 +1208,35 @@ text {* Several useful lemmas *} lemma wf_dep_converse: - fixes s - assumes vt: "vt s" shows "wf ((RAG s)^-1)" proof(rule finite_acyclic_wf_converse) - from finite_RAG [OF vt] + from finite_RAG show "finite (RAG s)" . next - from acyclic_RAG[OF vt] + from acyclic_RAG show "acyclic (RAG s)" . qed +end + lemma hd_np_in: "x \ set l \ hd l \ set l" -by (induct l, auto) + by (induct l, auto) lemma th_chasing: "(Th th, Cs cs) \ RAG (s::state) \ \ th'. (Cs cs, Th th') \ RAG s" by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in) +context valid_trace +begin + lemma wq_threads: - fixes s cs - assumes vt: "vt s" - and h: "th \ set (wq s cs)" + assumes h: "th \ set (wq s cs)" shows "th \ threads s" proof - from vt and h show ?thesis proof(induct arbitrary: th cs) case (vt_cons s e) + interpret vt_s: valid_trace s + using vt_cons(1) by (unfold_locales, auto) assume ih: "\th cs. th \ set (wq s cs) \ th \ threads s" and stp: "step s e" and vt: "vt s" @@ -1227,7 +1293,7 @@ assume th_in: "th \ set (SOME q. distinct q \ set q = set rest)" have "set (SOME q. distinct q \ set q = set rest) = set rest" proof(rule someI2) - from wq_distinct[OF vt, of cs'] and eq_wq[folded wq_def] + from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def] show "distinct rest \ set rest = set rest" by auto next show "\x. distinct x \ set x = set rest \ set x = set rest" @@ -1264,14 +1330,13 @@ qed qed -lemma range_in: "\vt s; (Th th) \ Range (RAG (s::state))\ \ th \ threads s" +lemma range_in: "\(Th th) \ Range (RAG (s::state))\ \ th \ threads s" apply(unfold s_RAG_def cs_waiting_def cs_holding_def) by (auto intro:wq_threads) lemma readys_v_eq: fixes th thread cs rest - assumes vt: "vt s" - and neq_th: "th \ thread" + assumes neq_th: "th \ thread" and eq_wq: "wq s cs = thread#rest" and not_in: "th \ set rest" shows "(th \ readys (V thread cs#s)) = (th \ readys s)" @@ -1292,7 +1357,7 @@ and eq_wq: "wq_fun (schs s) cs = thread # rest" have "set (SOME q. distinct q \ set q = set rest) = set rest" proof(rule someI2) - from wq_distinct[OF vt, of cs, unfolded wq_def] and eq_wq[unfolded wq_def] + from wq_distinct[of cs, unfolded wq_def] and eq_wq[unfolded wq_def] show "distinct rest \ set rest = set rest" by auto next show "\x. distinct x \ set x = set rest \ set x = set rest" by auto @@ -1308,10 +1373,9 @@ *} lemma chain_building: - assumes vt: "vt s" shows "node \ Domain (RAG s) \ (\ th'. th' \ readys s \ (node, Th th') \ (RAG s)^+)" proof - - from wf_dep_converse [OF vt] + from wf_dep_converse have h: "wf ((RAG s)\)" . show ?thesis proof(induct rule:wf_induct [OF h]) @@ -1342,7 +1406,7 @@ from True and th'_d show ?thesis by auto next case False - from th'_d and range_in [OF vt] have "th' \ threads s" by auto + from th'_d and range_in have "th' \ threads s" by auto with False have "Th th' \ Domain (RAG s)" by (auto simp:readys_def wq_def s_waiting_def s_RAG_def cs_waiting_def Domain_def) from ih [OF th'_d this] @@ -1362,9 +1426,7 @@ The following is just an instance of @{text "chain_building"}. *} lemma th_chain_to_ready: - fixes s th - assumes vt: "vt s" - and th_in: "th \ threads s" + assumes th_in: "th \ threads s" shows "th \ readys s \ (\ th'. th' \ readys s \ (Th th, Th th') \ (RAG s)^+)" proof(cases "th \ readys s") case True @@ -1373,10 +1435,12 @@ case False from False and th_in have "Th th \ Domain (RAG s)" by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def) - from chain_building [rule_format, OF vt this] + from chain_building [rule_format, OF this] show ?thesis by auto qed +end + lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs" by (unfold s_waiting_def cs_waiting_def wq_def, auto) @@ -1386,16 +1450,24 @@ lemma holding_unique: "\holding (s::state) th1 cs; holding s th2 cs\ \ th1 = th2" by (unfold s_holding_def cs_holding_def, auto) -lemma unique_RAG: "\vt s; (n, n1) \ RAG s; (n, n2) \ RAG s\ \ n1 = n2" +context valid_trace +begin + +lemma unique_RAG: "\(n, n1) \ RAG s; (n, n2) \ RAG s\ \ n1 = n2" apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq) by(auto elim:waiting_unique holding_unique) +end + + lemma trancl_split: "(a, b) \ r^+ \ \ c. (a, c) \ r" by (induct rule:trancl_induct, auto) +context valid_trace +begin + lemma dchain_unique: - assumes vt: "vt s" - and th1_d: "(n, Th th1) \ (RAG s)^+" + assumes th1_d: "(n, Th th1) \ (RAG s)^+" and th1_r: "th1 \ readys s" and th2_d: "(n, Th th2) \ (RAG s)^+" and th2_r: "th2 \ readys s" @@ -1403,7 +1475,7 @@ proof - { assume neq: "th1 \ th2" hence "Th th1 \ Th th2" by simp - from unique_chain [OF _ th1_d th2_d this] and unique_RAG [OF vt] + from unique_chain [OF _ th1_d th2_d this] and unique_RAG have "(Th th1, Th th2) \ (RAG s)\<^sup>+ \ (Th th2, Th th1) \ (RAG s)\<^sup>+" by auto hence "False" proof @@ -1427,6 +1499,8 @@ qed } thus ?thesis by auto qed + +end lemma step_holdents_p_add: @@ -1450,13 +1524,11 @@ qed -lemma finite_holding: - fixes s th cs - assumes vt: "vt s" +lemma (in valid_trace) finite_holding : shows "finite (holdents s th)" proof - let ?F = "\ (x, y). the_cs x" - from finite_RAG [OF vt] + from finite_RAG have "finite (RAG s)" . hence "finite (?F `(RAG s))" by simp moreover have "{cs . (Cs cs, Th th) \ RAG s} \ \" @@ -1476,13 +1548,17 @@ assumes vtv: "vt (V thread cs#s)" shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread" proof - + from vtv interpret vt_s: valid_trace s + by (cases, unfold_locales, simp) + from vtv interpret vt_v: valid_trace "V thread cs#s" + by (unfold_locales, simp) from step_back_step[OF vtv] have cs_in: "cs \ holdents s thread" apply (cases, unfold holdents_test s_RAG_def, simp) by (unfold cs_holding_def s_holding_def wq_def, auto) moreover have cs_not_in: "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" - apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) + apply (insert vt_s.wq_distinct[of cs]) apply (unfold holdents_test, unfold step_RAG_v[OF vtv], auto simp:next_th_def) proof - @@ -1536,7 +1612,7 @@ moreover have "card \ = Suc (card ((holdents (V thread cs#s) thread) - {cs}))" proof(rule card_insert) - from finite_holding [OF vtv] + from vt_v.finite_holding show " finite (holdents (V thread cs # s) thread)" . qed moreover from cs_not_in @@ -1544,20 +1620,22 @@ ultimately show ?thesis by (simp add:cntCS_def) qed +context valid_trace +begin + text {* (* ddd *) \noindent The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} of one particular thread. *} lemma cnp_cnv_cncs: - fixes s th - assumes vt: "vt s" shows "cntP s th = cntV s th + (if (th \ readys s \ th \ threads s) then cntCS s th else cntCS s th + 1)" proof - from vt show ?thesis proof(induct arbitrary:th) case (vt_cons s e) + interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp) assume vt: "vt s" and ih: "\th. cntP s th = cntV s th + (if (th \ readys s \ th \ threads s) then cntCS s th else cntCS s th + 1)" @@ -1571,7 +1649,7 @@ proof - { fix cs assume "thread \ set (wq s cs)" - from wq_threads [OF vt this] have "thread \ threads s" . + from vt_s.wq_threads [OF this] have "thread \ threads s" . with not_in have "False" by simp } with eq_e have eq_readys: "readys (e#s) = readys s \ {thread}" by (auto simp:readys_def threads.simps s_waiting_def @@ -1632,6 +1710,8 @@ and is_runing: "thread \ runing s" and no_dep: "(Cs cs, Th thread) \ (RAG s)\<^sup>+" from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto + then interpret vt_p: valid_trace "(P thread cs#s)" + by (unfold_locales, simp) show ?thesis proof - { have hh: "\ A B C. (B = C) \ (A \ B) = (A \ C)" by blast @@ -1679,7 +1759,7 @@ have "?L = insert cs ?R" by auto moreover have "card \ = Suc (card (?R - {cs}))" proof(rule card_insert) - from finite_holding [OF vt, of thread] + from vt_s.finite_holding [of thread] show " finite {cs. (Cs cs, Th thread) \ RAG s}" by (unfold holdents_test, simp) qed @@ -1718,7 +1798,7 @@ ultimately have "th = hd (wq (e#s) cs)" by blast with eq_wq have "th = hd (wq s cs @ [th])" by simp hence "th = hd (wq s cs)" using False by auto - with False eq_wq wq_distinct [OF vtp, of cs] + with False eq_wq vt_p.wq_distinct [of cs] show False by (fold eq_e, auto) qed moreover from is_runing have "th \ threads (e#s)" @@ -1737,6 +1817,7 @@ next case (thread_V thread cs) from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto + then interpret vt_v: valid_trace "(V thread cs # s)" by (unfold_locales, simp) assume eq_e: "e = V thread cs" and is_runing: "thread \ runing s" and hold: "holding s thread cs" @@ -1746,8 +1827,9 @@ have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e) have eq_set: "set (SOME q. distinct q \ set q = set rest) = set rest" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq - show "distinct rest \ set rest = set rest" by auto + from vt_v.wq_distinct[of cs] and eq_wq + show "distinct rest \ set rest = set rest" + by (metis distinct.simps(2) vt_s.wq_distinct) next show "\x. distinct x \ set x = set rest \ set x = set rest" by auto @@ -1782,8 +1864,9 @@ proof - assume "thread \ set (SOME q. distinct q \ set q = set rest)" with eq_set have "thread \ set rest" by simp - with wq_distinct[OF step_back_vt[OF vtv], of cs] - and eq_wq show False by auto + with vt_v.wq_distinct[of cs] + and eq_wq show False + by (metis distinct.simps(2) vt_s.wq_distinct) qed thus ?thesis by (simp add:wq_def s_waiting_def) qed @@ -1819,7 +1902,7 @@ case False have "(th \ readys (e # s)) = (th \ readys s)" apply (insert step_back_vt[OF vtv]) - by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto) + by (simp add: False eq_e eq_wq neq_th vt_s.readys_v_eq) moreover have "cntCS (e#s) th = cntCS s th" apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto) proof - @@ -1838,7 +1921,7 @@ " by simp moreover have "(SOME q. distinct q \ set q = set rest) \ []" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq + from vt_s.wq_distinct[ of cs] and eq_wq show "distinct rest \ set rest = set rest" by auto next fix x assume "distinct x \ set x = set rest" @@ -1870,7 +1953,7 @@ have "\ th \ readys s" apply (auto simp:readys_def s_waiting_def) apply (rule_tac x = cs in exI, auto) - by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp add: wq_def) + by (insert vt_s.wq_distinct[of cs], auto simp add: wq_def) moreover from eq_wq and th_in and neq_hd have "\ (th \ readys (e # s))" @@ -1885,7 +1968,7 @@ apply (unfold eq_e step_RAG_v[OF vtv], auto simp:next_th_def eq_set s_RAG_def holdents_test wq_def Let_def cs_holding_def) - by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def) + by (insert vt_s.wq_distinct[of cs], auto simp:wq_def) thus ?thesis by (simp add:cntCS_def) qed moreover note ih eq_cnp eq_cnv eq_threads @@ -1902,7 +1985,7 @@ assume eq_wq: "wq_fun (schs s) cs = thread # rest" and t_in: "?t \ set rest" show "?t \ threads s" - proof(rule wq_threads[OF step_back_vt[OF vtv]]) + proof(rule vt_s.wq_threads) from eq_wq and t_in show "?t \ set (wq s cs)" by (auto simp:wq_def) qed @@ -1915,7 +1998,7 @@ show "?t = hd (wq_fun (schs s) csa)" proof - { assume neq_hd': "?t \ hd (wq_fun (schs s) csa)" - from wq_distinct[OF step_back_vt[OF vtv], of cs] and + from vt_s.wq_distinct[of cs] and eq_wq[folded wq_def] and t_in eq_wq have "?t \ thread" by auto with eq_wq and t_in @@ -1924,7 +2007,7 @@ from t_in' neq_hd' have w2: "waiting s ?t csa" by (auto simp:s_waiting_def wq_def) - from waiting_unique[OF step_back_vt[OF vtv] w1 w2] + from vt_s.waiting_unique[OF w1 w2] and neq_cs have "False" by auto } thus ?thesis by auto qed @@ -1942,7 +2025,7 @@ proof - from th_in eq_wq have "th \ set (wq s cs)" by simp - from wq_threads [OF step_back_vt[OF vtv] this] + from vt_s.wq_threads [OF this] show ?thesis . qed ultimately show ?thesis using ih by auto @@ -1961,7 +2044,7 @@ have "?B \ ((\ (x, y). the_cs x) ` RAG s)" apply (auto simp:image_def) by (rule_tac x = "(Cs x, Th th)" in bexI, auto) - with finite_RAG[OF step_back_vt[OF vtv]] + with vt_s.finite_RAG show "finite {cs. (Cs cs, Th th) \ RAG s}" by (auto intro:finite_subset) next show "cs \ {cs. (Cs cs, Th th) \ RAG s}" @@ -2022,14 +2105,14 @@ qed lemma not_thread_cncs: - fixes th s - assumes vt: "vt s" - and not_in: "th \ threads s" + assumes not_in: "th \ threads s" shows "cntCS s th = 0" proof - from vt not_in show ?thesis proof(induct arbitrary:th) case (vt_cons s e th) + interpret vt_s: valid_trace s using vt_cons(1) + by (unfold_locales, simp) assume vt: "vt s" and ih: "\th. th \ threads s \ cntCS s th = 0" and stp: "step s e" @@ -2097,7 +2180,10 @@ by (simp add:runing_def readys_def) ultimately show ?thesis by auto qed - from assms thread_V vt stp ih have vtv: "vt (V thread cs#s)" by auto + from assms thread_V vt stp ih + have vtv: "vt (V thread cs#s)" by auto + then interpret vt_v: valid_trace "(V thread cs#s)" + by (unfold_locales, simp) from hold obtain rest where eq_wq: "wq s cs = thread # rest" by (case_tac "wq s cs", auto simp: wq_def s_holding_def) @@ -2109,15 +2195,18 @@ and ni: "hd (SOME q. distinct q \ set q = set rest) \ threads s" (is "?t \ threads s") have "?t \ set rest" proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq - show "distinct rest \ set rest = set rest" by auto + from vt_v.wq_distinct[of cs] and eq_wq + show "distinct rest \ set rest = set rest" + by (metis distinct.simps(2) vt_s.wq_distinct) next fix x assume "distinct x \ set x = set rest" with ne show "hd x \ set rest" by (cases x, auto) qed with eq_wq have "?t \ set (wq s cs)" by simp - from wq_threads[OF step_back_vt[OF vtv], OF this] and ni - show False by auto + from vt_s.wq_threads[OF this] and ni + show False + using `hd (SOME q. distinct q \ set q = set rest) \ set (wq s cs)` + ni vt_s.wq_threads by blast qed moreover note neq_th eq_wq ultimately have "cntCS (e # s) th = cntCS s th" @@ -2146,13 +2235,16 @@ qed qed +end + lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs" by (auto simp:s_waiting_def cs_waiting_def wq_def) +context valid_trace +begin + lemma dm_RAG_threads: - fixes th s - assumes vt: "vt s" - and in_dom: "(Th th) \ Domain (RAG s)" + assumes in_dom: "(Th th) \ Domain (RAG s)" shows "th \ threads s" proof - from in_dom obtain n where "(Th th, n) \ RAG s" by auto @@ -2160,9 +2252,11 @@ ultimately have "(Th th, Cs cs) \ RAG s" by simp hence "th \ set (wq s cs)" by (unfold s_RAG_def, auto simp:cs_waiting_def) - from wq_threads [OF vt this] show ?thesis . + from wq_threads [OF this] show ?thesis . qed +end + lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th" unfolding cp_def wq_def apply(induct s rule: schs.induct) @@ -2177,11 +2271,11 @@ apply(simp add: Let_def) done -(* FIXME: NOT NEEDED *) +context valid_trace +begin + lemma runing_unique: - fixes th1 th2 s - assumes vt: "vt s" - and runing_1: "th1 \ runing s" + assumes runing_1: "th1 \ runing s" and runing_2: "th2 \ runing s" shows "th1 = th2" proof - @@ -2210,7 +2304,7 @@ by (rule_tac x = "(Th x, Th th1)" in bexI, auto) moreover have "finite \" proof - - from finite_RAG[OF vt] have "finite (RAG s)" . + from finite_RAG have "finite (RAG s)" . hence "finite ((RAG (wq s))\<^sup>+)" apply (unfold finite_trancl) by (auto simp: s_RAG_def cs_RAG_def wq_def) @@ -2254,7 +2348,7 @@ by (rule_tac x = "(Th x, Th th2)" in bexI, auto) moreover have "finite \" proof - - from finite_RAG[OF vt] have "finite (RAG s)" . + from finite_RAG have "finite (RAG s)" . hence "finite ((RAG (wq s))\<^sup>+)" apply (unfold finite_trancl) by (auto simp: s_RAG_def cs_RAG_def wq_def) @@ -2289,7 +2383,7 @@ apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) by (auto simp:Domain_def) hence "(Th th1') \ Domain (RAG s)" by (simp add:trancl_domain) - from dm_RAG_threads[OF vt this] show ?thesis . + from dm_RAG_threads[OF this] show ?thesis . next assume "th1' = th1" with runing_1 show ?thesis @@ -2304,7 +2398,7 @@ apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) by (auto simp:Domain_def) hence "(Th th2') \ Domain (RAG s)" by (simp add:trancl_domain) - from dm_RAG_threads[OF vt this] show ?thesis . + from dm_RAG_threads[OF this] show ?thesis . next assume "th2' = th2" with runing_2 show ?thesis @@ -2366,7 +2460,7 @@ from th1'_in have h2: "(Th th1', Th th1) \ (RAG s)^+" by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) show ?thesis - proof(rule dchain_unique[OF vt h1 _ h2, symmetric]) + proof(rule dchain_unique[OF h1 _ h2, symmetric]) from runing_1 show "th1 \ readys s" by (simp add:runing_def) from runing_2 show "th2 \ readys s" by (simp add:runing_def) qed @@ -2375,7 +2469,7 @@ qed -lemma "vt s \ card (runing s) \ 1" +lemma "card (runing s) \ 1" apply(subgoal_tac "finite (runing s)") prefer 2 apply (metis finite_nat_set_iff_bounded lessI runing_unique) @@ -2389,6 +2483,9 @@ apply(auto) done +end + + lemma create_pre: assumes stp: "step s e" and not_in: "th \ threads s" @@ -2447,28 +2544,35 @@ from that [OF this] show ?thesis . qed +context valid_trace +begin + lemma cnp_cnv_eq: - fixes th s - assumes "vt s" - and "th \ threads s" + assumes "th \ threads s" shows "cntP s th = cntV s th" - by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs) + using assms + using cnp_cnv_cncs not_thread_cncs by auto + +end + lemma eq_RAG: "RAG (wq s) = RAG s" by (unfold cs_RAG_def s_RAG_def, auto) +context valid_trace +begin + lemma count_eq_dependants: - assumes vt: "vt s" - and eq_pv: "cntP s th = cntV s th" + assumes eq_pv: "cntP s th = cntV s th" shows "dependants (wq s) th = {}" proof - - from cnp_cnv_cncs[OF vt] and eq_pv + from cnp_cnv_cncs and eq_pv have "cntCS s th = 0" by (auto split:if_splits) moreover have "finite {cs. (Cs cs, Th th) \ RAG s}" proof - - from finite_holding[OF vt, of th] show ?thesis + from finite_holding[of th] show ?thesis by (simp add:holdents_test) qed ultimately have h: "{cs. (Cs cs, Th th) \ RAG s} = {}" @@ -2492,8 +2596,6 @@ qed lemma dependants_threads: - fixes s th - assumes vt: "vt s" shows "dependants (wq s) th \ threads s" proof { fix th th' @@ -2505,7 +2607,7 @@ with trancl_domain have "(Th th) \ Domain (RAG (wq s))" by simp thus ?thesis using eq_RAG by simp qed - from dm_RAG_threads[OF vt this] + from dm_RAG_threads[OF this] have "th \ threads s" . } note hh = this fix th1 @@ -2516,10 +2618,10 @@ qed lemma finite_threads: - assumes vt: "vt s" shows "finite (threads s)" -using vt -by (induct) (auto elim: step.cases) +using vt by (induct) (auto elim: step.cases) + +end lemma Max_f_mono: assumes seq: "A \ B" @@ -2534,9 +2636,11 @@ from fnt and seq show "finite (f ` B)" by auto qed +context valid_trace +begin + lemma cp_le: - assumes vt: "vt s" - and th_in: "th \ threads s" + assumes th_in: "th \ threads s" shows "cp s th \ Max ((\ th. (preced th s)) ` threads s)" proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def) show "Max ((\th. preced th s) ` ({th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+})) @@ -2545,20 +2649,19 @@ proof(rule Max_f_mono) show "{th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} \ {}" by simp next - from finite_threads [OF vt] + from finite_threads show "finite (threads s)" . next from th_in show "{th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} \ threads s" apply (auto simp:Domain_def) - apply (rule_tac dm_RAG_threads[OF vt]) + apply (rule_tac dm_RAG_threads) apply (unfold trancl_domain [of "RAG s", symmetric]) by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def) qed qed lemma le_cp: - assumes vt: "vt s" shows "preced th s \ cp s th" proof(unfold cp_eq_cpreced preced_def cpreced_def, simp) show "Prc (priority th s) (last_set th s) @@ -2579,7 +2682,7 @@ by (rule_tac x = "(Th x, Th th)" in bexI, auto) moreover have "finite \" proof - - from finite_RAG[OF vt] have "finite (RAG s)" . + from finite_RAG have "finite (RAG s)" . hence "finite ((RAG (wq s))\<^sup>+)" apply (unfold finite_trancl) by (auto simp: s_RAG_def cs_RAG_def wq_def) @@ -2599,7 +2702,6 @@ qed lemma max_cp_eq: - assumes vt: "vt s" shows "Max ((cp s) ` threads s) = Max ((\ th. (preced th s)) ` threads s)" (is "?l = ?r") proof(cases "threads s = {}") @@ -2609,26 +2711,26 @@ case False have "?l \ ((cp s) ` threads s)" proof(rule Max_in) - from finite_threads[OF vt] + from finite_threads show "finite (cp s ` threads s)" by auto next from False show "cp s ` threads s \ {}" by auto qed then obtain th where th_in: "th \ threads s" and eq_l: "?l = cp s th" by auto - have "\ \ ?r" by (rule cp_le[OF vt th_in]) + have "\ \ ?r" by (rule cp_le[OF th_in]) moreover have "?r \ cp s th" (is "Max (?f ` ?A) \ cp s th") proof - have "?r \ (?f ` ?A)" proof(rule Max_in) - from finite_threads[OF vt] + from finite_threads show " finite ((\th. preced th s) ` threads s)" by auto next from False show " (\th. preced th s) ` threads s \ {}" by auto qed then obtain th' where th_in': "th' \ ?A " and eq_r: "?r = ?f th'" by auto - from le_cp [OF vt, of th'] eq_r + from le_cp [of th'] eq_r have "?r \ cp s th'" by auto moreover have "\ \ cp s th" proof(fold eq_l) @@ -2637,7 +2739,7 @@ from th_in' show "cp s th' \ cp s ` threads s" by auto next - from finite_threads[OF vt] + from finite_threads show "finite (cp s ` threads s)" by auto qed qed @@ -2647,23 +2749,22 @@ qed lemma max_cp_readys_threads_pre: - assumes vt: "vt s" - and np: "threads s \ {}" + assumes np: "threads s \ {}" shows "Max (cp s ` readys s) = Max (cp s ` threads s)" -proof(unfold max_cp_eq[OF vt]) +proof(unfold max_cp_eq) show "Max (cp s ` readys s) = Max ((\th. preced th s) ` threads s)" proof - let ?p = "Max ((\th. preced th s) ` threads s)" let ?f = "(\th. preced th s)" have "?p \ ((\th. preced th s) ` threads s)" proof(rule Max_in) - from finite_threads[OF vt] show "finite (?f ` threads s)" by simp + from finite_threads show "finite (?f ` threads s)" by simp next from np show "?f ` threads s \ {}" by simp qed then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \ threads s" by (auto simp:Image_def) - from th_chain_to_ready [OF vt tm_in] + from th_chain_to_ready [OF tm_in] have "tm \ readys s \ (\th'. th' \ readys s \ (Th tm, Th th') \ (RAG s)\<^sup>+)" . thus ?thesis proof @@ -2672,7 +2773,7 @@ and tm_chain:"(Th tm, Th th') \ (RAG s)\<^sup>+" by auto have "cp s th' = ?f tm" proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI) - from dependants_threads[OF vt] finite_threads[OF vt] + from dependants_threads finite_threads show "finite ((\th. preced th s) ` ({th'} \ dependants (wq s) th'))" by (auto intro:finite_subset) next @@ -2680,10 +2781,10 @@ from tm_max have " preced tm s = Max ((\th. preced th s) ` threads s)" . moreover have "p \ \" proof(rule Max_ge) - from finite_threads[OF vt] + from finite_threads show "finite ((\th. preced th s) ` threads s)" by simp next - from p_in and th'_in and dependants_threads[OF vt, of th'] + from p_in and th'_in and dependants_threads[of th'] show "p \ (\th. preced th s) ` threads s" by (auto simp:readys_def) qed @@ -2710,18 +2811,18 @@ apply (unfold cp_eq_cpreced cpreced_def) apply (rule Max_mono) proof - - from dependants_threads [OF vt, of th1] th1_in + from dependants_threads [of th1] th1_in show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ (\th. preced th s) ` threads s" by (auto simp:readys_def) next show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ {}" by simp next - from finite_threads[OF vt] + from finite_threads show " finite ((\th. preced th s) ` threads s)" by simp qed next - from finite_threads[OF vt] + from finite_threads show "finite (cp s ` readys s)" by (auto simp:readys_def) next from th'_in @@ -2741,16 +2842,16 @@ assume hy' : "y' \ ((\th. preced th s) ` dependants (wq s) tm)" have "y' \ preced tm s" proof(unfold tm_max, rule Max_ge) - from hy' dependants_threads[OF vt, of tm] + from hy' dependants_threads[of tm] show "y' \ (\th. preced th s) ` threads s" by auto next - from finite_threads[OF vt] + from finite_threads show "finite ((\th. preced th s) ` threads s)" by simp qed } with hy show ?thesis by auto qed next - from dependants_threads[OF vt, of tm] finite_threads[OF vt] + from dependants_threads[of tm] finite_threads show "finite ((\th. preced th s) ` ({tm} \ dependants (wq s) tm))" by (auto intro:finite_subset) next @@ -2761,7 +2862,7 @@ proof(rule Max_eqI) from tm_ready show "cp s tm \ cp s ` readys s" by simp next - from finite_threads[OF vt] + from finite_threads show "finite (cp s ` readys s)" by (auto simp:readys_def) next fix y assume "y \ cp s ` readys s" @@ -2771,13 +2872,13 @@ apply(unfold cp_eq_p h) apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono) proof - - from finite_threads[OF vt] + from finite_threads show "finite ((\th. preced th s) ` threads s)" by simp next show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ {}" by simp next - from dependants_threads[OF vt, of th1] th1_readys + from dependants_threads[of th1] th1_readys show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ (\th. preced th s) ` threads s" by (auto simp:readys_def) @@ -2794,7 +2895,6 @@ there must be one inside it has the maximum precedence of the whole system. *} lemma max_cp_readys_threads: - assumes vt: "vt s" shows "Max (cp s ` readys s) = Max (cp s ` threads s)" proof(cases "threads s = {}") case True @@ -2802,9 +2902,10 @@ by (auto simp:readys_def) next case False - show ?thesis by (rule max_cp_readys_threads_pre[OF vt False]) + show ?thesis by (rule max_cp_readys_threads_pre[OF False]) qed +end lemma eq_holding: "holding (wq s) th cs = holding s th cs" apply (unfold s_holding_def cs_holding_def wq_def, simp) @@ -2836,13 +2937,14 @@ apply(auto) done +context valid_trace +begin + lemma detached_intro: - fixes s th - assumes vt: "vt s" - and eq_pv: "cntP s th = cntV s th" + assumes eq_pv: "cntP s th = cntV s th" shows "detached s th" proof - - from cnp_cnv_cncs[OF vt] + from cnp_cnv_cncs have eq_cnt: "cntP s th = cntV s th + (if th \ readys s \ th \ threads s then cntCS s th else cntCS s th + 1)" . hence cncs_zero: "cntCS s th = 0" @@ -2852,14 +2954,14 @@ thus ?thesis proof assume "th \ threads s" - with range_in[OF vt] dm_RAG_threads[OF vt] + with range_in dm_RAG_threads show ?thesis by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff) next assume "th \ readys s" moreover have "Th th \ Range (RAG s)" proof - - from card_0_eq [OF finite_holding [OF vt]] and cncs_zero + from card_0_eq [OF finite_holding] and cncs_zero have "holdents s th = {}" by (simp add:cntCS_def) thus ?thesis @@ -2874,12 +2976,10 @@ qed lemma detached_elim: - fixes s th - assumes vt: "vt s" - and dtc: "detached s th" + assumes dtc: "detached s th" shows "cntP s th = cntV s th" proof - - from cnp_cnv_cncs[OF vt] + from cnp_cnv_cncs have eq_pv: " cntP s th = cntV s th + (if th \ readys s \ th \ threads s then cntCS s th else cntCS s th + 1)" . have cncs_z: "cntCS s th = 0" @@ -2904,11 +3004,11 @@ qed lemma detached_eq: - fixes s th - assumes vt: "vt s" shows "(detached s th) = (cntP s th = cntV s th)" by (insert vt, auto intro:detached_intro detached_elim) +end + text {* The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived from the concise and miniature model of PIP given in PrioGDef.thy. @@ -2923,6 +3023,4 @@ shows "th1 = th2" using assms by (unfold next_th_def, auto) - - end diff -r 031d2ae9c9b8 -r b620a2a0806a RTree.thy --- a/RTree.thy Tue Dec 22 23:13:31 2015 +0800 +++ b/RTree.thy Wed Jan 06 20:46:14 2016 +0800 @@ -597,6 +597,23 @@ with that[unfolded ancestors_def] show ?thesis by auto qed + +lemma subtree_Field: + "subtree r x \ Field r \ {x}" +proof + fix y + assume "y \ subtree r x" + thus "y \ Field r \ {x}" + proof(cases rule:subtreeE) + case 1 + thus ?thesis by auto + next + case 2 + thus ?thesis apply (auto simp:ancestors_def) + using Field_def tranclD by fastforce + qed +qed + lemma subtree_ancestorsI: assumes "a \ subtree r b" and "a \ b"