diff -r e3cf792db636 -r 0f124691c191 PIPBasics.thy --- a/PIPBasics.thy Tue Jun 14 15:06:16 2016 +0100 +++ b/PIPBasics.thy Fri Jun 17 09:46:25 2016 +0100 @@ -1,5 +1,5 @@ theory PIPBasics -imports PIPDefs +imports PIPDefs RTree begin text {* (* ddd *) @@ -147,7 +147,7 @@ obtain th' where "th' \ set (wq s cs)" "th' = hd (wq s cs)" by (metis empty_iff hd_in_set list.set(1)) hence "holding s th' cs" - by (unfold s_holding_def, fold wq_def, auto) + unfolding s_holding_def by auto from that[OF this] show ?thesis . qed @@ -159,7 +159,7 @@ *} 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) + by (unfold s_RAG_def, auto simp:children_def s_holding_abv) text {* The following two lemmas relate @{term holdents} and @{term cntCS} @@ -279,8 +279,8 @@ lemma in_RAG_E: assumes "(n1, n2) \ RAG (s::state)" obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs" - | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs" - using assms[unfolded s_RAG_def, folded waiting_eq holding_eq] + | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs" + using assms[unfolded s_RAG_def, folded s_waiting_abv s_holding_abv] by auto text {* @@ -584,8 +584,8 @@ thus ?thesis by simp qed thus ?thesis - by (metis (no_types, lifting) cp_eq cpreced_def eq_dependants - f_image_eq the_preced_def) + by (metis (no_types, lifting) cp_eq cpreced_def2 f_image_eq + s_dependants_abv the_preced_def) qed text {* @@ -625,7 +625,7 @@ from h1 have "cs' = cs" by simp from assms(2) cs_in[unfolded this] have "holding s th'' cs" "holding s th2 cs" - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) from held_unique[OF this] show ?thesis by simp qed @@ -990,9 +990,9 @@ obtain rest where eq_wq: "wq s cs = th#rest" by blast with otherwise have "holding s th cs" - by (unfold s_holding_def, fold wq_def, simp) + unfolding s_holding_def by auto hence cs_th_RAG: "(Cs cs, Th th) \ RAG s" - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) from pip_e[unfolded is_p] show False proof(cases) @@ -1033,8 +1033,8 @@ proof(cases) case (thread_V) from this(2) show ?thesis - by (unfold rest_def s_holding_def, fold wq_def, - metis empty_iff list.collapse list.set(1)) + unfolding s_holding_def + by (metis empty_iff empty_set hd_Cons_tl rest_def) qed qed @@ -1168,8 +1168,9 @@ proof - from pip_e[unfolded is_exit] show ?thesis - by (cases, unfold holdents_def s_holding_def, fold wq_def, - auto elim!:running_wqE) + apply(cases) + unfolding holdents_def s_holding_def + by (metis (mono_tags, lifting) empty_iff list.sel(1) mem_Collect_eq running_wqE) qed lemma wq_threads_kept: @@ -1562,7 +1563,7 @@ proof - from assms(1) have "wq (e#s) c = wq s c" by auto from assms(2)[unfolded s_holding_def, folded wq_def, - folded this, unfolded wq_def, folded s_holding_def] + folded this, folded s_holding_def] show ?thesis . qed @@ -1624,7 +1625,7 @@ lemma holding_taker: shows "holding (e#s) taker cs" - by (unfold s_holding_def, fold wq_def, unfold wq_es_cs, + by (unfold s_holding_def, unfold wq_es_cs, auto simp:neq_wq' taker_def) lemma waiting_esI2: @@ -1692,7 +1693,7 @@ case False hence "wq (e#s) c = wq s c" by auto from assms[unfolded s_holding_def, folded wq_def, - unfolded this, unfolded wq_def, folded s_holding_def] + unfolded this, folded s_holding_def] have "holding s t c" . from that(2)[OF False this] show ?thesis . qed @@ -1795,7 +1796,7 @@ case False hence "wq (e#s) c = wq s c" by auto from assms[unfolded s_holding_def, folded wq_def, - unfolded this, unfolded wq_def, folded s_holding_def] + unfolded this, folded s_holding_def] have "holding s t c" . from that[OF False this] show ?thesis . qed @@ -1829,13 +1830,13 @@ with waiting(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, - fold waiting_eq, auto) + fold s_waiting_abv, auto) next case 2 with waiting(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, - fold waiting_eq, auto) + fold s_waiting_abv, auto) qed next case True @@ -1848,7 +1849,7 @@ with waiting(1,2) show ?thesis by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, - fold waiting_eq, auto) + fold s_waiting_abv, auto) qed qed next @@ -1865,13 +1866,13 @@ with holding(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, - fold waiting_eq, auto) + fold s_waiting_abv, auto) next case 2 with holding(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, - fold holding_eq, auto) + fold s_holding_abv, auto) qed next case True @@ -1884,7 +1885,7 @@ with holding(1,2) show ?thesis by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, - fold holding_eq, auto) + fold s_holding_abv, auto) qed qed qed @@ -1906,7 +1907,7 @@ assume "n2 = Th h_n.taker \ n1 = Cs cs" with h_n.holding_taker show ?thesis - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) next assume h: "(n1, n2) \ RAG s \ (n1 \ Cs cs \ n2 \ Th th) \ (n1 \ Th h_n.taker \ n2 \ Cs cs)" @@ -1935,7 +1936,7 @@ qed qed thus ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) next case (holding th' cs') from h this(1,2) @@ -1951,7 +1952,7 @@ show ?thesis . qed thus ?thesis using holding(1,2) - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) qed qed next @@ -1967,7 +1968,7 @@ case (waiting th' cs') from h_e.waiting_esI2[OF this(3)] show ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) next case (holding th' cs') with h_s(2) @@ -1977,12 +1978,12 @@ assume neq_cs: "cs' \ cs" from holding_esI2[OF this holding(3)] show ?thesis using holding(1,2) - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) next assume "th' \ th" from holding_esI1[OF holding(3) this] show ?thesis using holding(1,2) - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) qed qed qed @@ -2006,7 +2007,7 @@ proof(cases "cs' = cs") case False hence "wq (e#s) cs' = wq s cs'" by simp - with assms show ?thesis unfolding holding_raw_def holding_eq by auto + with assms show ?thesis unfolding holding_raw_def s_holding_abv by auto next case True from assms[unfolded s_holding_def, folded wq_def] @@ -2015,7 +2016,7 @@ hence "wq (e#s) cs' = th'#(rest@[th])" by (simp add: True wq_es_cs) thus ?thesis - by (simp add: holding_raw_def holding_eq) + by (simp add: holding_raw_def s_holding_abv) qed end @@ -2038,11 +2039,11 @@ proof - from wq_es_cs' have "th \ set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto - thus ?thesis unfolding holding_raw_def holding_eq by blast + thus ?thesis unfolding holding_raw_def s_holding_abv by blast qed lemma RAG_edge: "(Cs cs, Th th) \ RAG (e#s)" - by (unfold s_RAG_def, fold holding_eq, insert holding_es_th_cs, auto) + by (unfold s_RAG_def, fold s_holding_abv, insert holding_es_th_cs, auto) lemma waiting_esE: assumes "waiting (e#s) th' cs'" @@ -2063,7 +2064,7 @@ next case False have "holding s th' cs'" using assms - using False unfolding holding_raw_def holding_eq by auto + using False unfolding holding_raw_def s_holding_abv by auto from that(1)[OF False this] show ?thesis . qed @@ -2079,7 +2080,7 @@ proof(cases rule:waiting_esE) case 1 thus ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) qed next case (holding th' cs') @@ -2088,7 +2089,7 @@ proof(cases rule:holding_esE) case 1 with holding(1,2) - show ?thesis by (unfold s_RAG_def, fold holding_eq, auto) + show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto) next case 2 with holding(1,2) show ?thesis by auto @@ -2106,18 +2107,18 @@ case (waiting th' cs') from waiting_kept[OF this(3)] show ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) next case (holding th' cs') from holding_kept[OF this(3)] show ?thesis using holding(1,2) - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) qed next assume "n1 = Cs cs \ n2 = Th th" with holding_es_th_cs show ?thesis - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) qed qed @@ -2133,11 +2134,12 @@ by (simp add: wq_es_cs wq_s_cs) lemma waiting_es_th_cs: "waiting (e#s) th cs" - using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs - by (simp add: s_waiting_def wq_def wq_es_cs) + using th_not_in_wq s_waiting_abv wq_es_cs' wq_s_cs + using Un_iff list.sel(1) list.set_intros(1) s_waiting_def + set_append wq_def wq_es_cs by auto lemma RAG_edge: "(Th th, Cs cs) \ RAG (e#s)" - by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto) + by (unfold s_RAG_def, fold s_waiting_abv, insert waiting_es_th_cs, auto) lemma holding_esE: assumes "holding (e#s) th' cs'" @@ -2187,7 +2189,7 @@ proof(cases rule:waiting_esE) case 1 thus ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) next case 2 thus ?thesis using waiting(1,2) by auto @@ -2199,7 +2201,7 @@ proof(cases rule:holding_esE) case 1 with holding(1,2) - show ?thesis by (unfold s_RAG_def, fold holding_eq, auto) + show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto) qed qed next @@ -2214,12 +2216,12 @@ case (waiting th' cs') from waiting_kept[OF this(3)] show ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) next case (holding th' cs') from holding_kept[OF this(3)] show ?thesis using holding(1,2) - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) qed next assume "n1 = Th th \ n2 = Cs cs" @@ -2620,7 +2622,7 @@ "(Th taker, Cs cs') \ RAG s" by (unfold s_RAG_def, auto) from this(2) have "waiting s taker cs'" - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) from waiting_unique[OF this waiting_taker] have "cs' = cs" . from h(1)[unfolded this] show False by auto @@ -2655,7 +2657,7 @@ obtain cs' where h: "(Th th, Cs cs') \ RAG s" by (unfold s_RAG_def, auto) hence "waiting s th cs'" - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) with th_not_waiting show False by auto qed ultimately show ?thesis by auto @@ -2784,7 +2786,7 @@ 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) + apply(unfold s_RAG_def, auto, fold s_waiting_abv s_holding_abv) by(auto elim:waiting_unique held_unique) lemma sgv_RAG: "single_valued (RAG s)" @@ -2962,11 +2964,11 @@ obtain n where "(n, b) \ RAG s" by auto from this[unfolded Cs] obtain th1 where "waiting s th1 cs" - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) from waiting_holding[OF this] obtain th2 where "holding s th2 cs" . hence "(Cs cs, Th th2) \ RAG s" - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) with h_b(2)[unfolded Cs, rule_format] have False by auto thus ?thesis by auto @@ -2975,7 +2977,7 @@ proof - from h_b(2)[unfolded eq_b] have "\cs. \ waiting s th' cs" - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) moreover have "th' \ threads s" proof(rule rg_RAG_threads) from tranclD[OF h_b(1), unfolded eq_b] @@ -3123,7 +3125,7 @@ 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) + by (unfold s_RAG_def, fold s_waiting_abv, auto) with running_1 show False by (unfold running_def readys_def, auto) qed @@ -3139,7 +3141,7 @@ 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) + by (unfold s_RAG_def, fold s_waiting_abv, auto) with running_2 show False by (unfold running_def readys_def, auto) qed @@ -3232,7 +3234,7 @@ obtain z where "(Th th1, z) \ RAG s" by auto from this[unfolded s_RAG_def, folded wq_def] obtain cs' where "waiting s th1 cs'" - by (auto simp:waiting_eq) + by (auto simp:s_waiting_abv) with assms(1) show False by (auto simp:readys_def) qed next @@ -3251,7 +3253,7 @@ obtain z where "(Th th2, z) \ RAG s" by auto from this[unfolded s_RAG_def, folded wq_def] obtain cs' where "waiting s th2 cs'" - by (auto simp:waiting_eq) + by (auto simp:s_waiting_abv) with assms(2) show False by (auto simp:readys_def) qed qed @@ -3425,10 +3427,10 @@ begin lemma holding_s_holder: "holding s holder cs" - by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto) + by (unfold s_holding_def, unfold wq_s_cs, auto) lemma holding_es_holder: "holding (e#s) holder cs" - by (unfold s_holding_def, fold wq_def, unfold wq_es_cs wq_s_cs, auto) + by (unfold s_holding_def, unfold wq_es_cs wq_s_cs, auto) lemma holdents_es: shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") @@ -3448,7 +3450,7 @@ hence "wq (e#s) cs' = wq s cs'" by simp from h[unfolded s_holding_def, folded wq_def, unfolded this] show ?thesis - by (unfold s_holding_def, fold wq_def, auto) + by (unfold s_holding_def, auto) qed hence "cs' \ ?R" by (auto simp:holdents_def) } moreover { @@ -3467,7 +3469,7 @@ hence "wq s cs' = wq (e#s) cs'" by simp from h[unfolded s_holding_def, folded wq_def, unfolded this] show ?thesis - by (unfold s_holding_def, fold wq_def, auto) + by (unfold s_holding_def, auto) qed hence "cs' \ ?L" by (auto simp:holdents_def) } ultimately show ?thesis by auto @@ -3598,7 +3600,7 @@ from h_e[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp[OF this]] have "th' \ set (wq s cs') \ th' = hd (wq s cs')" . hence "cs' \ ?R" - by (unfold holdents_def s_holding_def, fold wq_def, auto) + by (unfold holdents_def s_holding_def, auto) } moreover { fix cs' assume "cs' \ ?R" @@ -3738,7 +3740,7 @@ lemma holding_th_cs_s: "holding s th cs" - by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto) + by (unfold s_holding_def, unfold wq_s_cs, auto) lemma th_ready_s [simp]: "th \ readys s" using running_th_s @@ -3931,7 +3933,7 @@ from h have "holding (e#s) th' cs'" by (auto simp:holdents_def) from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] show ?thesis - by (unfold holdents_def s_holding_def, fold wq_def, auto) + by (unfold holdents_def s_holding_def, auto) next case True from h[unfolded this] @@ -3950,7 +3952,7 @@ from h have "holding s th' cs'" by (auto simp:holdents_def) from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] show ?thesis - by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp) + by (unfold holdents_def s_holding_def, insert eq_wq, simp) next case True from h[unfolded this] @@ -4107,7 +4109,7 @@ from h have "holding (e#s) th' cs'" by (auto simp:holdents_def) from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] show ?thesis - by (unfold holdents_def s_holding_def, fold wq_def, auto) + by (unfold holdents_def s_holding_def, auto) next case True from h[unfolded this] @@ -4126,7 +4128,7 @@ from h have "holding s th' cs'" by (auto simp:holdents_def) from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] show ?thesis - by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp) + by (unfold holdents_def s_holding_def, insert eq_wq, simp) next case True from h[unfolded this] @@ -4315,14 +4317,12 @@ { fix cs' assume h: "cs' \ ?L" hence "cs' \ ?R" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } moreover { fix cs' assume h: "cs' \ ?R" hence "cs' \ ?L" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } ultimately show ?thesis by auto qed @@ -4432,7 +4432,7 @@ assume "holding (e # s) th cs'" from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept] have "holding s th cs'" - by (unfold s_holding_def, fold wq_def, auto) + by (unfold s_holding_def, auto) with not_holding_th_s show False by simp qed @@ -4462,14 +4462,12 @@ { fix cs' assume h: "cs' \ ?L" hence "cs' \ ?R" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } moreover { fix cs' assume h: "cs' \ ?R" hence "cs' \ ?L" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } ultimately show ?thesis by auto qed @@ -4567,14 +4565,12 @@ { fix cs' assume h: "cs' \ ?L" hence "cs' \ ?R" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } moreover { fix cs' assume h: "cs' \ ?R" hence "cs' \ ?L" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } ultimately show ?thesis by auto qed @@ -4639,8 +4635,8 @@ proof(induct rule:ind) case Nil thus ?case - by (unfold cntP_def cntV_def pvD_def cntCS_def holdents_def - s_holding_def, simp) + unfolding cntP_def cntV_def pvD_def cntCS_def holdents_def s_holding_def + by(simp add: wq_def) next case (Cons s e) interpret vt_e: valid_trace_e s e using Cons by simp @@ -4772,7 +4768,7 @@ lemma count_eq_tRAG_plus: assumes "cntP s th = cntV s th" shows "{th'. (Th th', Th th) \ (tRAG s)^+} = {}" - using assms eq_pv_dependants dependants_alt_def eq_dependants by auto + using assms count_eq_RAG_plus dependants_alt_def s_dependants_def by blast lemma count_eq_tRAG_plus_Th: assumes "cntP s th = cntV s th" @@ -4880,7 +4876,7 @@ with dtc have "th \ readys s" by (unfold readys_def detached_def Field_def Domain_def Range_def, - auto simp:waiting_eq s_RAG_def) + auto simp:s_waiting_abv s_RAG_def) with cncs_z show ?thesis using cnp_cnv_cncs by (simp add:pvD_def) next case False