# HG changeset patch # User zhang # Date 1334921269 0 # Node ID 73127f5db18f200cd3f0fe8f5473971e145103c3 # Parent 61bd5d99c3ab87d79035e34f6aa1ab25985f6e3c Intuitive definition of "detached" is added to PrioG.thy. diff -r 61bd5d99c3ab -r 73127f5db18f prio/CpsG.thy --- a/prio/CpsG.thy Tue Apr 17 15:55:37 2012 +0000 +++ b/prio/CpsG.thy Fri Apr 20 11:27:49 2012 +0000 @@ -2,7 +2,6 @@ imports PrioG begin - lemma not_thread_holdents: fixes th s assumes vt: "vt s" diff -r 61bd5d99c3ab -r 73127f5db18f prio/ExtGG.thy --- a/prio/ExtGG.thy Tue Apr 17 15:55:37 2012 +0000 +++ b/prio/ExtGG.thy Fri Apr 20 11:27:49 2012 +0000 @@ -546,7 +546,7 @@ by auto qed -lemma pv_blocked: +lemma pv_blocked_pre: fixes th' assumes th'_in: "th' \ threads (t@s)" and neq_th': "th' \ th" @@ -584,6 +584,8 @@ qed qed +lemmas pv_blocked = pv_blocked_pre[folded detached_eq [OF vt_t]] + lemma runing_precond_pre: fixes th' assumes th'_in: "th' \ threads s" @@ -695,6 +697,8 @@ qed *) +lemmas runing_precond_pre_dtc = runing_precond_pre[folded detached_eq[OF vt_t] detached_eq[OF vt_s]] + lemma runing_precond: fixes th' assumes th'_in: "th' \ threads s" @@ -708,7 +712,7 @@ 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] have " th' \ runing (t @ s)" . + 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'] @@ -812,7 +816,7 @@ from assms show ?case by auto qed -lemma moment_blocked: +lemma moment_blocked_eqpv: assumes neq_th': "th' \ th" and th'_in: "th' \ threads ((moment i t)@s)" and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" @@ -828,6 +832,24 @@ show ?thesis by auto qed +lemma moment_blocked: + assumes neq_th': "th' \ th" + and th'_in: "th' \ threads ((moment i t)@s)" + and dtc: "detached (moment i t @ s) th'" + and le_ij: "i \ j" + shows "detached (moment j t @ s) th' \ + 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 . +qed + lemma runing_inversion_1: assumes neq_th': "th' \ th" and runing': "th' \ runing (t@s)" @@ -877,7 +899,7 @@ 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 [OF neq_th' h2 h1, of "length t"] and lt_its + 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' @@ -924,7 +946,6 @@ show ?thesis by auto qed - lemma live: "runing (t@s) \ {}" proof(cases "th \ runing (t@s)") case True thus ?thesis by auto @@ -1002,3 +1023,4 @@ end + diff -r 61bd5d99c3ab -r 73127f5db18f prio/Moment.thy --- a/prio/Moment.thy Tue Apr 17 15:55:37 2012 +0000 +++ b/prio/Moment.thy Fri Apr 20 11:27:49 2012 +0000 @@ -770,4 +770,14 @@ thus ?thesis by (simp add:restm_def) qed +lemma moment_prefix: "(moment i t @ s) = moment (i + length s) (t @ s)" +proof - + from moment_plus_split [of i "length s" "t@s"] + have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)" + by auto + with app_moment_restm[of t s] + have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" by simp + with moment_app show ?thesis by auto +qed + end \ No newline at end of file diff -r 61bd5d99c3ab -r 73127f5db18f prio/PrioG.thy --- a/prio/PrioG.thy Tue Apr 17 15:55:37 2012 +0000 +++ b/prio/PrioG.thy Fri Apr 20 11:27:49 2012 +0000 @@ -173,23 +173,22 @@ qed qed -lemma vt_moment: "\ t. \vt s; t \ length s\ \ vt (moment t s)" +lemma vt_moment: "\ t. \vt s\ \ vt (moment t s)" proof(induct s, simp) fix a s t - assume h: "\t.\vt s; t \ length s\ \ vt (moment t s)" + assume h: "\t.\vt s\ \ vt (moment t s)" and vt_a: "vt (a # s)" - and le_t: "t \ length (a # s)" show "vt (moment t (a # s))" - proof(cases "t = length (a#s)") + proof(cases "t \ length (a#s)") case True from True have "moment t (a#s) = a#s" by simp with vt_a show ?thesis by simp next case False - with le_t have le_t1: "t \ length s" by simp + hence le_t1: "t \ length s" by simp from vt_a have "vt s" by (erule_tac evt_cons, simp) - from h [OF this le_t1] have "vt (moment t s)" . + from h [OF this] have "vt (moment t s)" . moreover have "moment t (a#s) = moment t s" proof - from moment_app [OF le_t1, of "[a]"] @@ -244,7 +243,7 @@ h2: "thread \ hd (wq (e#moment t2 s) cs2)" by auto have vt_e: "vt (e#moment t2 s)" proof - - from vt_moment [OF vt le_t3] + from vt_moment [OF vt] have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed @@ -277,7 +276,7 @@ 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 le_t3] + from vt_moment [OF vt] have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed @@ -310,7 +309,7 @@ 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 le_t3] + from vt_moment [OF vt] have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed @@ -342,7 +341,7 @@ case False have vt_e: "vt (e#moment t2 s)" proof - - from vt_moment [OF vt le_t3] eqt12 + from vt_moment [OF vt] eqt12 have "vt (moment (Suc t2) s)" by auto with eq_m eqt12 show ?thesis by simp qed @@ -2771,7 +2770,82 @@ by(rule image_subsetI, auto intro:h) next show "g ` A \ f ` A" - by(rule image_subsetI, auto intro:h[symmetric]) + by (rule image_subsetI, auto intro:h[symmetric]) qed +definition detached :: "state \ thread \ bool" + where "detached s th \ (Th th \ Field (depend s))" + +lemma detached_intro: + fixes s th + assumes vt: "vt s" + and eq_pv: "cntP s th = cntV s th" + shows "detached s th" +proof - + from cnp_cnv_cncs[OF vt] + 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" + by (auto simp:eq_pv split:if_splits) + with eq_cnt + have "th \ readys s \ th \ threads s" by (auto simp:eq_pv) + thus ?thesis + proof + assume "th \ threads s" + with range_in[OF vt] dm_depend_threads[OF vt] + show ?thesis + by (auto simp:detached_def Field_def Domain_def Range_def) + next + assume "th \ readys s" + moreover have "Th th \ Range (depend s)" + proof - + from card_0_eq [OF finite_holding [OF vt]] and cncs_zero + have "holdents s th = {}" + by (simp add:cntCS_def) + thus ?thesis + by (auto simp:holdents_def, case_tac x, + auto simp:holdents_def s_depend_def) + qed + ultimately show ?thesis + apply (auto simp:detached_def Field_def Domain_def readys_def) + apply (case_tac y, auto simp:s_depend_def) + by (erule_tac x = "nat" in allE, simp add: eq_waiting) + qed +qed + +lemma detached_elim: + fixes s th + assumes vt: "vt s" + and dtc: "detached s th" + shows "cntP s th = cntV s th" +proof - + from cnp_cnv_cncs[OF vt] + 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" + proof - + from dtc have "holdents s th = {}" + by (unfold detached_def holdents_def, auto simp:Field_def Domain_def Range_def) + thus ?thesis by (auto simp:cntCS_def) + qed + show ?thesis + proof(cases "th \ threads s") + case True + with dtc + have "th \ readys s" + by (unfold readys_def detached_def Field_def Domain_def Range_def, + auto simp:eq_waiting s_depend_def) + with cncs_z and eq_pv show ?thesis by simp + next + case False + with cncs_z and eq_pv show ?thesis by simp + qed +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 \ No newline at end of file