# HG changeset patch # User zhangx # Date 1454472243 -28800 # Node ID c7db2ccba18a535274362e90b61e8d8af785c900 # Parent 3d2b59f15f2687706e5889795c0e7a5ee2538cae Reorganzing PIPBasics.thy intro sections. diff -r 3d2b59f15f26 -r c7db2ccba18a PIPBasics.thy --- a/PIPBasics.thy Mon Feb 01 20:56:39 2016 +0800 +++ b/PIPBasics.thy Wed Feb 03 12:04:03 2016 +0800 @@ -171,6 +171,19 @@ lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs" by (unfold s_holding_def wq_def cs_holding_def, simp) +lemma children_RAG_alt_def: + "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}" + by (unfold s_RAG_def, auto simp:children_def holding_eq) + +lemma holdents_alt_def: + "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))" + by (unfold children_RAG_alt_def holdents_def, simp add: image_image) + +lemma cntCS_alt_def: + "cntCS s th = card (children (RAG s) (Th th))" + apply (unfold children_RAG_alt_def cntCS_def holdents_def) + by (rule card_image[symmetric], auto simp:inj_on_def) + lemma runing_ready: shows "runing s \ readys s" unfolding runing_def readys_def @@ -273,6 +286,81 @@ using assms[unfolded s_RAG_def, folded waiting_eq holding_eq] by auto +lemma count_rec1 [simp]: + assumes "Q e" + shows "count Q (e#es) = Suc (count Q es)" + using assms + by (unfold count_def, auto) + +lemma count_rec2 [simp]: + assumes "\Q e" + shows "count Q (e#es) = (count Q es)" + using assms + by (unfold count_def, auto) + +lemma count_rec3 [simp]: + shows "count Q [] = 0" + by (unfold count_def, auto) + +lemma cntP_simp1[simp]: + "cntP (P th cs'#s) th = cntP s th + 1" + by (unfold cntP_def, simp) + +lemma cntP_simp2[simp]: + assumes "th' \ th" + shows "cntP (P th cs'#s) th' = cntP s th'" + using assms + by (unfold cntP_def, simp) + +lemma cntP_simp3[simp]: + assumes "\ isP e" + shows "cntP (e#s) th' = cntP s th'" + using assms + by (unfold cntP_def, cases e, simp+) + +lemma cntV_simp1[simp]: + "cntV (V th cs'#s) th = cntV s th + 1" + by (unfold cntV_def, simp) + +lemma cntV_simp2[simp]: + assumes "th' \ th" + shows "cntV (V th cs'#s) th' = cntV s th'" + using assms + by (unfold cntV_def, simp) + +lemma cntV_simp3[simp]: + assumes "\ isV e" + shows "cntV (e#s) th' = cntV s th'" + using assms + by (unfold cntV_def, cases e, simp+) + +lemma cntP_diff_inv: + assumes "cntP (e#s) th \ cntP s th" + shows "isP e \ actor e = th" +proof(cases e) + case (P th' pty) + show ?thesis + by (cases "(\e. \cs. e = P th cs) (P th' pty)", + insert assms P, auto simp:cntP_def) +qed (insert assms, auto simp:cntP_def) + +lemma cntV_diff_inv: + assumes "cntV (e#s) th \ cntV s th" + shows "isV e \ actor e = th" +proof(cases e) + case (V th' pty) + show ?thesis + by (cases "(\e. \cs. e = V th cs) (V th' pty)", + insert assms V, auto simp:cntV_def) +qed (insert assms, auto simp:cntV_def) + +lemma eq_dependants: "dependants (wq s) = dependants s" + by (simp add: s_dependants_abv wq_def) + +lemma inj_the_preced: + "inj_on (the_preced s) (threads s)" + by (metis inj_onI preced_unique the_preced_def) + (* ccc *) section {* Locales used to investigate the execution of PIP *} @@ -706,6 +794,13 @@ context valid_trace begin +lemma finite_threads: + shows "finite (threads s)" + using vt by (induct) (auto elim: step.cases) + +lemma finite_readys [simp]: "finite (readys s)" + using finite_threads readys_threads rev_finite_subset by blast + lemma wq_distinct: "distinct (wq s cs)" proof(induct rule:ind) case (Cons s e) @@ -2075,7 +2170,7 @@ by (unfold s_RAG_def, auto) hence "waiting s th cs'" by (unfold s_RAG_def, fold waiting_eq, auto) - with th_not_waiting show False by auto (* ccc *) + with th_not_waiting show False by auto qed ultimately show ?thesis by auto qed @@ -2247,6 +2342,7 @@ qed qed + section {* Derived properties for parts of RAG *} context valid_trace @@ -2314,139 +2410,199 @@ from this[folded tRAG_def] show "fsubtree (tRAG s)" . qed - -(* ccc *) - -context valid_trace_p -begin - -lemma ready_th_s: "th \ readys s" - using runing_th_s - by (unfold runing_def, auto) - -lemma live_th_s: "th \ threads s" - using readys_threads ready_th_s by auto - -lemma live_th_es: "th \ threads (e#s)" - using live_th_s - by (unfold is_p, simp) - - -lemma waiting_neq_th: - assumes "waiting s t c" - shows "t \ th" - using assms using th_not_waiting by blast - -end - -context valid_trace_v -begin - -lemma th_not_waiting: - "\ waiting s th c" +lemma tRAG_nodeE: + assumes "(n1, n2) \ tRAG s" + obtains th1 th2 where "n1 = Th th1" "n2 = Th th2" + using assms + by (auto simp: tRAG_def wRAG_def hRAG_def) + +lemma tRAG_ancestorsE: + assumes "x \ ancestors (tRAG s) u" + obtains th where "x = Th th" +proof - + from assms have "(u, x) \ (tRAG s)^+" + by (unfold ancestors_def, auto) + from tranclE[OF this] obtain c where "(c, x) \ tRAG s" by auto + then obtain th where "x = Th th" + by (unfold tRAG_alt_def, auto) + from that[OF this] show ?thesis . +qed + +lemma subtree_nodeE: + assumes "n \ subtree (tRAG s) (Th th)" + obtains th1 where "n = Th th1" +proof - + show ?thesis + proof(rule subtreeE[OF assms]) + assume "n = Th th" + from that[OF this] show ?thesis . + next + assume "Th th \ ancestors (tRAG s) n" + hence "(n, Th th) \ (tRAG s)^+" by (auto simp:ancestors_def) + hence "\ th1. n = Th th1" + proof(induct) + case (base y) + from tRAG_nodeE[OF this] show ?case by metis + next + case (step y z) + thus ?case by auto + qed + with that show ?thesis by auto + qed +qed + +lemma tRAG_star_RAG: "(tRAG s)^* \ (RAG s)^*" +proof - + have "(wRAG s O hRAG s)^* \ (RAG s O RAG s)^*" + by (rule rtrancl_mono, auto simp:RAG_split) + also have "... \ ((RAG s)^*)^*" + by (rule rtrancl_mono, auto) + also have "... = (RAG s)^*" by simp + finally show ?thesis by (unfold tRAG_def, simp) +qed + +lemma tRAG_subtree_RAG: "subtree (tRAG s) x \ subtree (RAG s) x" +proof - + { fix a + assume "a \ subtree (tRAG s) x" + hence "(a, x) \ (tRAG s)^*" by (auto simp:subtree_def) + with tRAG_star_RAG + have "(a, x) \ (RAG s)^*" by auto + hence "a \ subtree (RAG s) x" by (auto simp:subtree_def) + } thus ?thesis by auto +qed + +lemma tRAG_trancl_eq: + "{th'. (Th th', Th th) \ (tRAG s)^+} = + {th'. (Th th', Th th) \ (RAG s)^+}" + (is "?L = ?R") proof - - have "th \ readys s" - using runing_ready runing_th_s by blast - thus ?thesis - by (unfold readys_def, auto) + { 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 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, auto) + 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 waiting_neq_th: - assumes "waiting s t c" - shows "t \ th" - using assms using th_not_waiting by blast - -end - - -context valid_trace_e -begin - -lemma actor_inv: - assumes "\ isCreate e" - shows "actor e \ runing s" - using pip_e assms - by (induct, auto) - -end - - -(* ccc *) - -(* drag more from before to here *) - - -section {* ccc *} - +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 tRAG_Field: + "Field (tRAG s) \ Field (RAG s)" + by (unfold tRAG_alt_def Field_def, auto) + +lemma tRAG_mono: + assumes "RAG s' \ RAG s" + shows "tRAG s' \ tRAG s" + using assms + by (unfold tRAG_alt_def, auto) + +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 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)^*" + by (auto simp:subtree_def) + 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 + +lemma threads_set_eq: + "the_thread ` (subtree (tRAG s) (Th th)) = + {th'. Th th' \ (subtree (RAG s) (Th th))}" (is "?L = ?R") + by (auto intro:rev_image_eqI simp:tRAG_subtree_eq) + +lemma dependants_alt_def: + "dependants s th = {th'. (Th th', Th th) \ (tRAG s)^+}" + by (metis eq_RAG s_dependants_def tRAG_trancl_eq) + +lemma dependants_alt_def1: + "dependants (s::state) th = {th'. (Th th', Th th) \ (RAG s)^+}" + using dependants_alt_def tRAG_trancl_eq by auto + +section {* Chain to readys *} context valid_trace begin -lemma finite_subtree_threads: - "finite {th'. Th th' \ subtree (RAG s) (Th th)}" (is "finite ?A") -proof - - have "?A = the_thread ` {Th th' | th' . Th th' \ subtree (RAG s) (Th th)}" - by (auto, insert image_iff, fastforce) - moreover have "finite {Th th' | th' . Th th' \ subtree (RAG s) (Th th)}" - (is "finite ?B") - proof - - have "?B = (subtree (RAG s) (Th th)) \ {Th th' | th'. True}" - by auto - moreover have "... \ (subtree (RAG s) (Th th))" by auto - moreover have "finite ..." by (simp add: fsbtRAGs.finite_subtree) - ultimately show ?thesis by auto - qed - ultimately show ?thesis by auto -qed - -lemma le_cp: - shows "preced th s \ cp s th" - proof(unfold cp_alt_def, rule Max_ge) - show "finite (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)})" - by (simp add: finite_subtree_threads) - next - show "preced th s \ the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)}" - by (simp add: subtree_def the_preced_def) - qed - -lemma finite_threads: - shows "finite (threads s)" - using vt by (induct) (auto elim: step.cases) - -lemma cp_le: - assumes th_in: "th \ threads s" - shows "cp s th \ Max (the_preced s ` threads s)" -proof(unfold cp_alt_def, rule Max_f_mono) - show "finite (threads s)" by (simp add: finite_threads) -next - show " {th'. Th th' \ subtree (RAG s) (Th th)} \ {}" - using subtree_def by fastforce -next - show "{th'. Th th' \ subtree (RAG s) (Th th)} \ threads s" - using assms - by (smt Domain.DomainI dm_RAG_threads mem_Collect_eq - node.inject(1) rtranclD subsetI subtree_def trancl_domain) -qed - -lemma max_cp_eq: - shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" - (is "?L = ?R") -proof - - have "?L \ ?R" - proof(cases "threads s = {}") - case False - show ?thesis - by (rule Max.boundedI, - insert cp_le, - auto simp:finite_threads False) - qed auto - moreover have "?R \ ?L" - by (rule Max_fg_mono, - simp add: finite_threads, - simp add: le_cp the_preced_def) - ultimately show ?thesis by auto -qed - lemma chain_building: assumes "node \ Domain (RAG s)" obtains th' where "th' \ readys s" "(node, Th th') \ (RAG s)^+" @@ -2507,89 +2663,204 @@ show ?thesis by auto qed +lemma finite_subtree_threads: + "finite {th'. Th th' \ subtree (RAG s) (Th th)}" (is "finite ?A") +proof - + have "?A = the_thread ` {Th th' | th' . Th th' \ subtree (RAG s) (Th th)}" + by (auto, insert image_iff, fastforce) + moreover have "finite {Th th' | th' . Th th' \ subtree (RAG s) (Th th)}" + (is "finite ?B") + proof - + have "?B = (subtree (RAG s) (Th th)) \ {Th th' | th'. True}" + by auto + moreover have "... \ (subtree (RAG s) (Th th))" by auto + moreover have "finite ..." by (simp add: fsbtRAGs.finite_subtree) + ultimately show ?thesis by auto + qed + ultimately show ?thesis by auto +qed + +lemma runing_unique: + assumes runing_1: "th1 \ runing s" + and runing_2: "th2 \ runing s" + shows "th1 = th2" +proof - + from runing_1 and runing_2 have "cp s th1 = cp s th2" + unfolding runing_def by auto + from this[unfolded cp_alt_def] + have eq_max: + "Max (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th1)}) = + Max (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th2)})" + (is "Max ?L = Max ?R") . + have "Max ?L \ ?L" + proof(rule Max_in) + show "finite ?L" by (simp add: finite_subtree_threads) + next + show "?L \ {}" using subtree_def by fastforce + qed + then obtain th1' where + h_1: "Th th1' \ subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L" + by auto + have "Max ?R \ ?R" + proof(rule Max_in) + show "finite ?R" by (simp add: finite_subtree_threads) + next + show "?R \ {}" using subtree_def by fastforce + qed + then obtain th2' where + h_2: "Th th2' \ subtree (RAG s) (Th th2)" "the_preced s th2' = Max ?R" + by auto + have "th1' = th2'" + proof(rule preced_unique) + from h_1(1) + show "th1' \ threads s" + proof(cases rule:subtreeE) + case 1 + hence "th1' = th1" by simp + with runing_1 show ?thesis by (auto simp:runing_def readys_def) + next + case 2 + from this(2) + have "(Th th1', Th th1) \ (RAG s)^+" by (auto simp:ancestors_def) + from tranclD[OF this] + have "(Th th1') \ Domain (RAG s)" by auto + from dm_RAG_threads[OF this] show ?thesis . + qed + next + from h_2(1) + show "th2' \ threads s" + proof(cases rule:subtreeE) + case 1 + hence "th2' = th2" by simp + with runing_2 show ?thesis by (auto simp:runing_def readys_def) + next + case 2 + from this(2) + have "(Th th2', Th th2) \ (RAG s)^+" by (auto simp:ancestors_def) + from tranclD[OF this] + have "(Th th2') \ Domain (RAG s)" by auto + from dm_RAG_threads[OF this] show ?thesis . + qed + next + have "the_preced s th1' = the_preced s th2'" + using eq_max h_1(2) h_2(2) by metis + thus "preced th1' s = preced th2' s" by (simp add:the_preced_def) + qed + from h_1(1)[unfolded this] + have star1: "(Th th2', Th th1) \ (RAG s)^*" by (auto simp:subtree_def) + from h_2(1)[unfolded this] + have star2: "(Th th2', Th th2) \ (RAG s)^*" by (auto simp:subtree_def) + from star_rpath[OF star1] obtain xs1 + where rp1: "rpath (RAG s) (Th th2') xs1 (Th th1)" + by auto + from star_rpath[OF star2] obtain xs2 + where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)" + by auto + from rp1 rp2 + show ?thesis + proof(cases) + case (less_1 xs') + moreover have "xs' = []" + proof(rule ccontr) + assume otherwise: "xs' \ []" + from rpath_plus[OF less_1(3) this] + have "(Th th1, Th th2) \ (RAG s)\<^sup>+" . + from tranclD[OF this] + obtain cs where "waiting s th1 cs" + by (unfold s_RAG_def, fold waiting_eq, auto) + with runing_1 show False + by (unfold runing_def readys_def, auto) + qed + ultimately have "xs2 = xs1" by simp + from rpath_dest_eq[OF rp1 rp2[unfolded this]] + show ?thesis by simp + next + case (less_2 xs') + moreover have "xs' = []" + proof(rule ccontr) + assume otherwise: "xs' \ []" + from rpath_plus[OF less_2(3) this] + have "(Th th2, Th th1) \ (RAG s)\<^sup>+" . + from tranclD[OF this] + obtain cs where "waiting s th2 cs" + by (unfold s_RAG_def, fold waiting_eq, auto) + with runing_2 show False + by (unfold runing_def readys_def, auto) + qed + ultimately have "xs2 = xs1" by simp + from rpath_dest_eq[OF rp1 rp2[unfolded this]] + show ?thesis by simp + qed +qed + +lemma card_runing: "card (runing s) \ 1" +proof(cases "runing s = {}") + case True + thus ?thesis by auto +next + case False + then obtain th where [simp]: "th \ runing s" by auto + from runing_unique[OF this] + have "runing s = {th}" by auto + thus ?thesis by auto +qed + end -lemma count_rec1 [simp]: - assumes "Q e" - shows "count Q (e#es) = Suc (count Q es)" - using assms - by (unfold count_def, auto) - -lemma count_rec2 [simp]: - assumes "\Q e" - shows "count Q (e#es) = (count Q es)" - using assms - by (unfold count_def, auto) - -lemma count_rec3 [simp]: - shows "count Q [] = 0" - by (unfold count_def, auto) - -lemma cntP_simp1[simp]: - "cntP (P th cs'#s) th = cntP s th + 1" - by (unfold cntP_def, simp) - -lemma cntP_simp2[simp]: - assumes "th' \ th" - shows "cntP (P th cs'#s) th' = cntP s th'" - using assms - by (unfold cntP_def, simp) - -lemma cntP_simp3[simp]: - assumes "\ isP e" - shows "cntP (e#s) th' = cntP s th'" - using assms - by (unfold cntP_def, cases e, simp+) - -lemma cntV_simp1[simp]: - "cntV (V th cs'#s) th = cntV s th + 1" - by (unfold cntV_def, simp) - -lemma cntV_simp2[simp]: - assumes "th' \ th" - shows "cntV (V th cs'#s) th' = cntV s th'" - using assms - by (unfold cntV_def, simp) - -lemma cntV_simp3[simp]: - assumes "\ isV e" - shows "cntV (e#s) th' = cntV s th'" - using assms - by (unfold cntV_def, cases e, simp+) - -lemma cntP_diff_inv: - assumes "cntP (e#s) th \ cntP s th" - shows "isP e \ actor e = th" -proof(cases e) - case (P th' pty) - show ?thesis - by (cases "(\e. \cs. e = P th cs) (P th' pty)", - insert assms P, auto simp:cntP_def) -qed (insert assms, auto simp:cntP_def) - -lemma cntV_diff_inv: - assumes "cntV (e#s) th \ cntV s th" - shows "isV e \ actor e = th" -proof(cases e) - case (V th' pty) - show ?thesis - by (cases "(\e. \cs. e = V th cs) (V th' pty)", - insert assms V, auto simp:cntV_def) -qed (insert assms, auto simp:cntV_def) - -lemma children_RAG_alt_def: - "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}" - by (unfold s_RAG_def, auto simp:children_def holding_eq) - -lemma holdents_alt_def: - "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))" - by (unfold children_RAG_alt_def holdents_def, simp add: image_image) - -lemma cntCS_alt_def: - "cntCS s th = card (children (RAG s) (Th th))" - apply (unfold children_RAG_alt_def cntCS_def holdents_def) - by (rule card_image[symmetric], auto simp:inj_on_def) - + +section {* Relating @{term cp} and @{term the_preced} and @{term preced} *} + +context valid_trace +begin + +lemma le_cp: + shows "preced th s \ cp s th" + proof(unfold cp_alt_def, rule Max_ge) + show "finite (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)})" + by (simp add: finite_subtree_threads) + next + show "preced th s \ the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)}" + by (simp add: subtree_def the_preced_def) + qed + + +lemma cp_le: + assumes th_in: "th \ threads s" + shows "cp s th \ Max (the_preced s ` threads s)" +proof(unfold cp_alt_def, rule Max_f_mono) + show "finite (threads s)" by (simp add: finite_threads) +next + show " {th'. Th th' \ subtree (RAG s) (Th th)} \ {}" + using subtree_def by fastforce +next + show "{th'. Th th' \ subtree (RAG s) (Th th)} \ threads s" + using assms + by (smt Domain.DomainI dm_RAG_threads mem_Collect_eq + node.inject(1) rtranclD subsetI subtree_def trancl_domain) +qed + +lemma max_cp_eq: + shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" + (is "?L = ?R") +proof - + have "?L \ ?R" + proof(cases "threads s = {}") + case False + show ?thesis + by (rule Max.boundedI, + insert cp_le, + auto simp:finite_threads False) + qed auto + moreover have "?R \ ?L" + by (rule Max_fg_mono, + simp add: finite_threads, + simp add: le_cp the_preced_def) + ultimately show ?thesis by auto +qed + +end + +section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *} context valid_trace_p_w begin @@ -2656,6 +2927,27 @@ lemma (in valid_trace) finite_holdents: "finite (holdents s th)" by (unfold holdents_alt_def, insert fsbtRAGs.finite_children, auto) +context valid_trace_p +begin + +lemma ready_th_s: "th \ readys s" + using runing_th_s + by (unfold runing_def, auto) + +lemma live_th_s: "th \ threads s" + using readys_threads ready_th_s by auto + +lemma live_th_es: "th \ threads (e#s)" + using live_th_s + by (unfold is_p, simp) + +lemma waiting_neq_th: + assumes "waiting s t c" + shows "t \ th" + using assms using th_not_waiting by blast + +end + context valid_trace_p_h begin @@ -2906,7 +3198,7 @@ proof - have "cs \ holdents s th" using holding_th_cs_s by (unfold holdents_def, simp) - moreover have "finite (holdents s th)" using finite_holdents (* ccc *) + moreover have "finite (holdents s th)" using finite_holdents by simp ultimately show ?thesis by (unfold cntCS_def, @@ -2915,6 +3207,25 @@ end +context valid_trace_v +begin + +lemma th_not_waiting: + "\ waiting s th c" +proof - + have "th \ readys s" + using runing_ready runing_th_s by blast + thus ?thesis + by (unfold readys_def, auto) +qed + +lemma waiting_neq_th: + assumes "waiting s t c" + shows "t \ th" + using assms using th_not_waiting by blast + +end + context valid_trace_v_n begin @@ -2949,7 +3260,7 @@ qed lemma neq_taker_th: "taker \ th" - using th_not_waiting waiting_taker by blast + using th_not_waiting waiting_taker by blast lemma not_holding_taker_s_cs: shows "\ holding s taker cs" @@ -3797,6 +4108,13 @@ qed qed +end + +section {* Corollaries of @{thm valid_trace.cnp_cnv_cncs} *} + +context valid_trace +begin + lemma not_thread_holdents: assumes not_in: "th \ threads s" shows "holdents s th = {}" @@ -3824,158 +4142,6 @@ using assms cnp_cnv_cncs not_thread_cncs pvD_def by (auto) -lemma runing_unique: - assumes runing_1: "th1 \ runing s" - and runing_2: "th2 \ runing s" - shows "th1 = th2" -proof - - from runing_1 and runing_2 have "cp s th1 = cp s th2" - unfolding runing_def by auto - from this[unfolded cp_alt_def] - have eq_max: - "Max (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th1)}) = - Max (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th2)})" - (is "Max ?L = Max ?R") . - have "Max ?L \ ?L" - proof(rule Max_in) - show "finite ?L" by (simp add: finite_subtree_threads) - next - show "?L \ {}" using subtree_def by fastforce - qed - then obtain th1' where - h_1: "Th th1' \ subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L" - by auto - have "Max ?R \ ?R" - proof(rule Max_in) - show "finite ?R" by (simp add: finite_subtree_threads) - next - show "?R \ {}" using subtree_def by fastforce - qed - then obtain th2' where - h_2: "Th th2' \ subtree (RAG s) (Th th2)" "the_preced s th2' = Max ?R" - by auto - have "th1' = th2'" - proof(rule preced_unique) - from h_1(1) - show "th1' \ threads s" - proof(cases rule:subtreeE) - case 1 - hence "th1' = th1" by simp - with runing_1 show ?thesis by (auto simp:runing_def readys_def) - next - case 2 - from this(2) - have "(Th th1', Th th1) \ (RAG s)^+" by (auto simp:ancestors_def) - from tranclD[OF this] - have "(Th th1') \ Domain (RAG s)" by auto - from dm_RAG_threads[OF this] show ?thesis . - qed - next - from h_2(1) - show "th2' \ threads s" - proof(cases rule:subtreeE) - case 1 - hence "th2' = th2" by simp - with runing_2 show ?thesis by (auto simp:runing_def readys_def) - next - case 2 - from this(2) - have "(Th th2', Th th2) \ (RAG s)^+" by (auto simp:ancestors_def) - from tranclD[OF this] - have "(Th th2') \ Domain (RAG s)" by auto - from dm_RAG_threads[OF this] show ?thesis . - qed - next - have "the_preced s th1' = the_preced s th2'" - using eq_max h_1(2) h_2(2) by metis - thus "preced th1' s = preced th2' s" by (simp add:the_preced_def) - qed - from h_1(1)[unfolded this] - have star1: "(Th th2', Th th1) \ (RAG s)^*" by (auto simp:subtree_def) - from h_2(1)[unfolded this] - have star2: "(Th th2', Th th2) \ (RAG s)^*" by (auto simp:subtree_def) - from star_rpath[OF star1] obtain xs1 - where rp1: "rpath (RAG s) (Th th2') xs1 (Th th1)" - by auto - from star_rpath[OF star2] obtain xs2 - where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)" - by auto - from rp1 rp2 - show ?thesis - proof(cases) - case (less_1 xs') - moreover have "xs' = []" - proof(rule ccontr) - assume otherwise: "xs' \ []" - from rpath_plus[OF less_1(3) this] - have "(Th th1, Th th2) \ (RAG s)\<^sup>+" . - from tranclD[OF this] - obtain cs where "waiting s th1 cs" - by (unfold s_RAG_def, fold waiting_eq, auto) - with runing_1 show False - by (unfold runing_def readys_def, auto) - qed - ultimately have "xs2 = xs1" by simp - from rpath_dest_eq[OF rp1 rp2[unfolded this]] - show ?thesis by simp - next - case (less_2 xs') - moreover have "xs' = []" - proof(rule ccontr) - assume otherwise: "xs' \ []" - from rpath_plus[OF less_2(3) this] - have "(Th th2, Th th1) \ (RAG s)\<^sup>+" . - from tranclD[OF this] - obtain cs where "waiting s th2 cs" - by (unfold s_RAG_def, fold waiting_eq, auto) - with runing_2 show False - by (unfold runing_def readys_def, auto) - qed - ultimately have "xs2 = xs1" by simp - from rpath_dest_eq[OF rp1 rp2[unfolded this]] - show ?thesis by simp - qed -qed - -lemma card_runing: "card (runing s) \ 1" -proof(cases "runing s = {}") - case True - thus ?thesis by auto -next - case False - then obtain th where [simp]: "th \ runing s" by auto - from runing_unique[OF this] - have "runing s = {th}" by auto - thus ?thesis by auto -qed - -lemma create_pre: - assumes stp: "step s e" - and not_in: "th \ threads s" - and is_in: "th \ threads (e#s)" - obtains prio where "e = Create th prio" -proof - - from assms - show ?thesis - proof(cases) - case (thread_create thread prio) - with is_in not_in have "e = Create th prio" by simp - from that[OF this] show ?thesis . - next - case (thread_exit thread) - with assms show ?thesis by (auto intro!:that) - next - case (thread_P thread) - with assms show ?thesis by (auto intro!:that) - next - case (thread_V thread) - with assms show ?thesis by (auto intro!:that) - next - case (thread_set thread) - with assms show ?thesis by (auto intro!:that) - qed -qed - lemma eq_pv_children: assumes eq_pv: "cntP s th = cntV s th" shows "children (RAG s) (Th th) = {}" @@ -4002,151 +4168,6 @@ using eq_pv_children[OF assms] by (unfold subtree_children, simp) -end - -lemma cp_gen_alt_def: - "cp_gen s = (Max \ (\x. (the_preced s \ the_thread) ` subtree (tRAG s) x))" - by (auto simp:cp_gen_def) - -lemma tRAG_nodeE: - assumes "(n1, n2) \ tRAG s" - obtains th1 th2 where "n1 = Th th1" "n2 = Th th2" - using assms - by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def) - -lemma subtree_nodeE: - assumes "n \ subtree (tRAG s) (Th th)" - obtains th1 where "n = Th th1" -proof - - show ?thesis - proof(rule subtreeE[OF assms]) - assume "n = Th th" - from that[OF this] show ?thesis . - next - assume "Th th \ ancestors (tRAG s) n" - hence "(n, Th th) \ (tRAG s)^+" by (auto simp:ancestors_def) - hence "\ th1. n = Th th1" - proof(induct) - case (base y) - from tRAG_nodeE[OF this] show ?case by metis - next - case (step y z) - thus ?case by auto - qed - with that show ?thesis by auto - qed -qed - -lemma tRAG_star_RAG: "(tRAG s)^* \ (RAG s)^*" -proof - - have "(wRAG s O hRAG s)^* \ (RAG s O RAG s)^*" - by (rule rtrancl_mono, auto simp:RAG_split) - also have "... \ ((RAG s)^*)^*" - by (rule rtrancl_mono, auto) - also have "... = (RAG s)^*" by simp - finally show ?thesis by (unfold tRAG_def, simp) -qed - -lemma tRAG_subtree_RAG: "subtree (tRAG s) x \ subtree (RAG s) x" -proof - - { fix a - assume "a \ subtree (tRAG s) x" - hence "(a, x) \ (tRAG s)^*" by (auto simp:subtree_def) - with tRAG_star_RAG - have "(a, x) \ (RAG s)^*" by auto - hence "a \ subtree (RAG s) x" by (auto simp:subtree_def) - } thus ?thesis by auto -qed - -lemma tRAG_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 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, auto) - 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) - -lemma dependants_alt_def1: - "dependants (s::state) th = {th'. (Th th', Th th) \ (RAG s)^+}" - using dependants_alt_def tRAG_trancl_eq by auto - -context valid_trace -begin lemma count_eq_RAG_plus: assumes "cntP s th = cntV s th" shows "{th'. (Th th', Th th) \ (RAG s)^+} = {}" @@ -4168,14 +4189,6 @@ show ?thesis . qed -end - -lemma eq_dependants: "dependants (wq s) = dependants s" - by (simp add: s_dependants_abv wq_def) - -context valid_trace -begin - lemma count_eq_tRAG_plus: assumes "cntP s th = cntV s th" shows "{th'. (Th th', Th th) \ (tRAG s)^+} = {}" @@ -4190,50 +4203,10 @@ 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 inj_the_preced: - "inj_on (the_preced s) (threads s)" - by (metis inj_onI preced_unique the_preced_def) - -lemma tRAG_Field: - "Field (tRAG s) \ Field (RAG s)" - by (unfold tRAG_alt_def Field_def, auto) - -lemma tRAG_ancestorsE: - assumes "x \ ancestors (tRAG s) u" - obtains th where "x = Th th" -proof - - from assms have "(u, x) \ (tRAG s)^+" - by (unfold ancestors_def, auto) - from tranclE[OF this] obtain c where "(c, x) \ tRAG s" by auto - then obtain th where "x = Th th" - by (unfold tRAG_alt_def, auto) - from that[OF this] show ?thesis . -qed - -lemma tRAG_mono: - assumes "RAG s' \ RAG s" - shows "tRAG s' \ tRAG s" - using assms - by (unfold tRAG_alt_def, auto) - -lemma holding_next_thI: - assumes "holding s th cs" - and "length (wq s cs) > 1" - obtains th' where "next_th s th cs th'" -proof - - from assms(1)[folded holding_eq, unfolded cs_holding_def] - have " th \ set (wq s cs) \ th = hd (wq s cs)" - by (unfold s_holding_def, fold wq_def, auto) - then obtain rest where h1: "wq s cs = th#rest" - by (cases "wq s cs", auto) - with assms(2) have h2: "rest \ []" by auto - let ?th' = "hd (SOME q. distinct q \ set q = set rest)" - have "next_th s th cs ?th'" using h1(1) h2 - by (unfold next_th_def, auto) - from that[OF this] show ?thesis . -qed +section {* hhh *} lemma RAG_tRAG_transfer: assumes "vt s'" @@ -4300,34 +4273,6 @@ 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 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)^*" - by (auto simp:subtree_def) - 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 - -lemma threads_set_eq: - "the_thread ` (subtree (tRAG s) (Th th)) = - {th'. Th th' \ (subtree (RAG s) (Th th))}" (is "?L = ?R") - by (auto intro:rev_image_eqI simp:tRAG_subtree_eq) - lemma cp_alt_def1: "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))" proof - @@ -4660,8 +4605,6 @@ } ultimately show ?thesis by auto qed -lemma finite_readys [simp]: "finite (readys s)" - using finite_threads readys_threads rev_finite_subset by blast text {* (* ccc *) \noindent Since the current precedence of the threads in ready queue will always be boosted, @@ -4702,6 +4645,63 @@ finally show ?thesis by simp qed (auto simp:threads_alt_def) +lemma create_pre: + assumes stp: "step s e" + and not_in: "th \ threads s" + and is_in: "th \ threads (e#s)" + obtains prio where "e = Create th prio" +proof - + from assms + show ?thesis + proof(cases) + case (thread_create thread prio) + with is_in not_in have "e = Create th prio" by simp + from that[OF this] show ?thesis . + next + case (thread_exit thread) + with assms show ?thesis by (auto intro!:that) + next + case (thread_P thread) + with assms show ?thesis by (auto intro!:that) + next + case (thread_V thread) + with assms show ?thesis by (auto intro!:that) + next + case (thread_set thread) + with assms show ?thesis by (auto intro!:that) + qed +qed + +end + +section {* Pending properties *} + +lemma holding_next_thI: + assumes "holding s th cs" + and "length (wq s cs) > 1" + obtains th' where "next_th s th cs th'" +proof - + from assms(1)[folded holding_eq, unfolded cs_holding_def] + have " th \ set (wq s cs) \ th = hd (wq s cs)" + by (unfold s_holding_def, fold wq_def, auto) + then obtain rest where h1: "wq s cs = th#rest" + by (cases "wq s cs", auto) + with assms(2) have h2: "rest \ []" by auto + let ?th' = "hd (SOME q. distinct q \ set q = set rest)" + have "next_th s th cs ?th'" using h1(1) h2 + by (unfold next_th_def, auto) + from that[OF this] show ?thesis . +qed + +context valid_trace_e +begin + +lemma actor_inv: + assumes "\ isCreate e" + shows "actor e \ runing s" + using pip_e assms + by (induct, auto) + end end diff -r 3d2b59f15f26 -r c7db2ccba18a PIPDefs.thy --- a/PIPDefs.thy Mon Feb 01 20:56:39 2016 +0800 +++ b/PIPDefs.thy Wed Feb 03 12:04:03 2016 +0800 @@ -665,6 +665,11 @@ definition "cp_gen s x = Max ((the_preced s \ the_thread) ` subtree (tRAG s) x)" +lemma cp_gen_alt_def: + "cp_gen s = (Max \ (\x. (the_preced s \ the_thread) ` subtree (tRAG s) x))" + by (auto simp:cp_gen_def) + + (*<*) end