# HG changeset patch # User zhangx # Date 1452349167 -28800 # Node ID 25fd656667a7a20c3a111d7370adf16ccf87789c # Parent 2af87bb52fca617d2939ddda7b4fb720bcfb7438 Correctness simplified a great deal. diff -r 2af87bb52fca -r 25fd656667a7 Correctness.thy --- a/Correctness.thy Thu Jan 07 22:10:06 2016 +0800 +++ b/Correctness.thy Sat Jan 09 22:19:27 2016 +0800 @@ -79,7 +79,6 @@ 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, unfold eq_cp_s_th, insert highest, simp) @@ -135,7 +134,6 @@ apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) by (unfold highest_gen_def, auto dest:step_back_vt_app) - context extend_highest_gen begin @@ -458,268 +456,6 @@ 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: (* ddd *) - 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 otherwise: "th' \ runing (t@s)" - show False - proof - - 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 - 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] - -lemma runing_precond_pre: (* ddd *) - fixes th' - assumes th'_in: "th' \ threads s" - and eq_pv: "cntP s th' = cntV s th'" - and neq_th': "th' \ th" - shows "th' \ threads (t@s) \ - cntP (t@s) th' = cntV (t@s) th'" -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 (P 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) (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 - moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold P, simp) - ultimately show ?thesis by auto - qed - next - 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 - 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) - 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 - 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 - -text {* Changing counting balance to detachedness *} -lemmas runing_precond_pre_dtc = runing_precond_pre - [folded vat_t.detached_eq vat_s.detached_eq] - -section {* The blocking thread *} - -text {* - The purpose of PIP is to ensure that the most - urgent thread @{term th} is not blocked unreasonably. - Therefore, a clear picture of the blocking thread is essential - to assure people that the purpose is fulfilled. - - The following lemmas will give us such a picture: -*} - -(* ccc *) - -text {* - The following lemma shows the blocking thread @{term th'} - must hold some resource in the very beginning. -*} -lemma runing_cntP_cntV_inv: (* ddd *) - assumes th'_in: "th' \ threads s" - 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'" - 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 - -lemma moment_blocked_pre: - 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'" - shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \ - th' \ threads ((moment (i+j) t)@s)" -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 - 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: (* ddd *) - 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'" - and le_ij: "i \ j" - shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \ - th' \ threads ((moment j t)@s) \ - th' \ runing ((moment j t)@s)" -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 - 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. - This one is useless (* XY *) -*) -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 - - 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 - - -text {* The following lemmas shows that the @{term cp}-value of the blocking thread @{text th'} equals to the highest precedence in the whole system. @@ -735,67 +471,190 @@ finally show ?thesis . qed +section {* The `blocking thread` *} + +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. +*} (* ccc *) + +lemma eq_pv_blocked: (* ddd *) + assumes neq_th': "th' \ th" + and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" + shows "th' \ runing (t@s)" +proof + assume otherwise: "th' \ runing (t@s)" + show False + proof - + have th'_in: "th' \ threads (t@s)" + using otherwise readys_threads runing_def by auto + have "th' = th" + proof(rule preced_unique) + -- {* The proof goes like this: + it is first shown that the @{term preced}-value of @{term th'} + equals to that of @{term th}, then by uniqueness + of @{term preced}-values (given by lemma @{thm preced_unique}), + @{term th'} equals to @{term th}: *} + show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") + proof - + -- {* Since the counts of @{term th'} are balanced, the subtree + of it contains only itself, so, its @{term cp}-value + equals its @{term preced}-value: *} + have "?L = cp (t@s) th'" + by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) + -- {* Since @{term "th'"} is running by @{thm otherwise}, + it has the highest @{term cp}-value, by definition, + which in turn equals to the @{term cp}-value of @{term th}. *} + also have "... = ?R" + using runing_preced_inversion[OF otherwise] th_kept by simp + finally show ?thesis . + qed + qed (auto simp: th'_in th_kept) + moreover have "th' \ th" using neq_th' . + ultimately show ?thesis by simp + qed +qed + +text {* + The following lemma is the extrapolation of @{thm eq_pv_blocked}. + It says if a thread, different from @{term th}, + does not hold any resource at the very beginning, + it will keep hand-emptied in the future @{term "t@s"}. +*} +lemma eq_pv_persist: (* ddd *) + assumes neq_th': "th' \ th" + and eq_pv: "cntP s th' = cntV s th'" + shows "cntP (t@s) th' = cntV (t@s) th'" +proof(induction rule:ind) -- {* The proof goes by induction. *} + -- {* The nontrivial case is for the @{term Cons}: *} + case (Cons e t) + -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *} + 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 - + -- {* It can be proved that @{term cntP}-value of @{term th'} does not change + by the happening of event @{term e}: *} + have "cntP ((e#t)@s) th' = cntP (t@s) th'" + proof(rule ccontr) -- {* Proof by contradiction. *} + -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *} + assume otherwise: "cntP ((e # t) @ s) th' \ cntP (t @ s) th'" + -- {* Then the actor of @{term e} must be @{term th'} and @{term e} + must be a @{term P}-event: *} + hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) + with vat_t.actor_inv[OF Cons(2)] + -- {* According to @{thm actor_inv}, @{term th'} must be running at + the moment @{term "t@s"}: *} + have "th' \ runing (t@s)" by (cases e, auto) + -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis + shows @{term th'} can not be running at moment @{term "t@s"}: *} + moreover have "th' \ runing (t@s)" + using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . + -- {* Contradiction is finally derived: *} + ultimately show False by simp + qed + -- {* It can also be proved that @{term cntV}-value of @{term th'} does not change + by the happening of event @{term e}: *} + -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *} + moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'" + proof(rule ccontr) -- {* Proof by contradiction. *} + assume otherwise: "cntV ((e # t) @ s) th' \ cntV (t @ s) th'" + hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) + with vat_t.actor_inv[OF Cons(2)] + have "th' \ runing (t@s)" by (cases e, auto) + moreover have "th' \ runing (t@s)" + using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . + ultimately show False by simp + qed + -- {* Finally, it can be shown that the @{term cntP} and @{term cntV} + value for @{term th'} are still in balance, so @{term th'} + is still hand-emptied after the execution of event @{term e}: *} + ultimately show ?thesis using Cons(5) by metis + qed +qed (auto simp:eq_pv) + +text {* + By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, + it can be derived easily that @{term th'} can not be running in the future: +*} +lemma eq_pv_blocked_persist: + assumes neq_th': "th' \ th" + and eq_pv: "cntP s th' = cntV s th'" + shows "th' \ runing (t@s)" + using assms + by (simp add: eq_pv_blocked eq_pv_persist) + +text {* + The purpose of PIP is to ensure that the most + urgent thread @{term th} is not blocked unreasonably. + Therefore, a clear picture of the blocking thread is essential + to assure people that the purpose is fulfilled. + + The following lemmas will give us such a picture: +*} + +text {* + The following lemma shows the blocking thread @{term th'} + must hold some resource in the very beginning. +*} +lemma runing_cntP_cntV_inv: (* ddd *) + assumes is_runing: "th' \ runing (t@s)" + and neq_th': "th' \ th" + shows "cntP s th' > cntV s th'" + using assms +proof - + -- {* First, it can be shown that the number of @{term P} and + @{term V} operations can not be equal for thred @{term th'} *} + have "cntP s th' \ cntV s th'" + proof + -- {* The proof goes by contradiction, suppose otherwise: *} + assume otherwise: "cntP s th' = cntV s th'" + -- {* By applying @{thm eq_pv_blocked_persist} to this: *} + from eq_pv_blocked_persist[OF neq_th' otherwise] + -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *} + have "th' \ runing (t@s)" . + -- {* This is obvious in contradiction with assumption @{thm is_runing} *} + thus False using is_runing by simp + qed + -- {* However, the number of @{term V} is always less or equal to @{term P}: *} + moreover have "cntV s th' \ cntP s th'" using vat_s.cnp_cnv_cncs by auto + -- {* Thesis is finally derived by combining the these two results: *} + ultimately show ?thesis by auto +qed + text {* The following lemmas shows the blocking thread @{text th'} must be live at the very beginning, i.e. the moment (or state) @{term s}. + + The proof is a simple combination of the results above: *} -lemma runing_threads_inv: (* ddd *) +lemma runing_threads_inv: assumes runing': "th' \ runing (t@s)" and neq_th': "th' \ th" 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 +proof(rule ccontr) -- {* Proof by contradiction: *} + assume otherwise: "th' \ threads s" + have "th' \ runing (t @ s)" + proof - + from vat_s.cnp_cnv_eq[OF otherwise] + have "cntP s th' = cntV s th'" . + from eq_pv_blocked_persist[OF neq_th' this] + show ?thesis . + qed + with runing' show False by simp qed text {* The following lemma summarizes several foregoing lemmas to give an overall picture of the blocking thread @{text "th'"}: *} -lemma runing_inversion: +lemma runing_inversion: (* ddd, one of the main lemmas to present *) assumes runing': "th' \ runing (t@s)" and neq_th: "th' \ th" shows "th' \ threads s" @@ -805,13 +664,15 @@ from runing_threads_inv[OF assms] show "th' \ threads s" . next - from runing_cntP_cntV_inv[OF runing_threads_inv[OF assms] neq_th runing'] + from runing_cntP_cntV_inv[OF runing' neq_th] show "\detached s th'" using vat_s.detached_eq by simp next from runing_preced_inversion[OF runing'] show "cp (t@s) th' = preced th s" . qed +section {* The existence of `blocking thread` *} + 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'"} @@ -822,7 +683,7 @@ is the @{term runing}-thread. However, we are going to show more: this running thread is exactly @{term "th'"}. *} -lemma th_blockedE: (* ddd *) +lemma th_blockedE: (* ddd, the other main lemma to be presented: *) assumes "th \ runing (t@s)" obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" "th' \ runing (t@s)" @@ -898,6 +759,3 @@ end end - - - diff -r 2af87bb52fca -r 25fd656667a7 Correctness.thy~ --- a/Correctness.thy~ Thu Jan 07 22:10:06 2016 +0800 +++ b/Correctness.thy~ Sat Jan 09 22:19:27 2016 +0800 @@ -79,7 +79,6 @@ 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, unfold eq_cp_s_th, insert highest, simp) @@ -135,7 +134,6 @@ apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) by (unfold highest_gen_def, auto dest:step_back_vt_app) - context extend_highest_gen begin @@ -458,6 +456,23 @@ vat_s.le_cp) text {* + The following lemmas shows that the @{term cp}-value + of the blocking thread @{text th'} equals to the highest + precedence in the whole system. +*} +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 {* 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 @@ -465,27 +480,37 @@ The following lemma shows that the counting controls whether a thread is running or not. -*} - -lemma pv_blocked_pre: (* ddd *) - assumes th'_in: "th' \ threads (t@s)" - and neq_th': "th' \ th" +*} (* ccc *) + +lemma eq_pv_blocked: (* ddd *) + assumes neq_th': "th' \ th" and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" shows "th' \ runing (t@s)" proof assume otherwise: "th' \ runing (t@s)" show False proof - + have th'_in: "th' \ threads (t@s)" + using otherwise readys_threads runing_def by auto have "th' = th" proof(rule preced_unique) + -- {* The proof goes like this: + it is first shown that the @{term preced}-value of @{term th'} + equals to that of @{term th}, then by uniqueness + of @{term preced}-values (given by lemma @{thm preced_unique}), + @{term th'} equals to @{term th}: *} show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") proof - + -- {* Since the counts of @{term th'} are balanced, the subtree + of it contains only itself, so, its @{term cp}-value + equals its @{term preced}-value: *} 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) + -- {* Since @{term "th'"} is running by @{thm otherwise}, + it has the highest @{term cp}-value, by definition, + which in turn equals to the @{term cp}-value of @{term th}. *} + also have "... = ?R" + using runing_preced_inversion[OF otherwise] th_kept by simp finally show ?thesis . qed qed (auto simp: th'_in th_kept) @@ -494,10 +519,11 @@ qed qed -lemmas pv_blocked = pv_blocked_pre[folded detached_eq] +lemmas eq_pv_blocked_dtc = eq_pv_blocked[folded detached_eq] + -lemma runing_precond_pre: (* ddd *) - fixes th' + +lemma eq_pv_kept: (* ddd *) assumes th'_in: "th' \ threads s" and eq_pv: "cntP s th' = cntV s th'" and neq_th': "th' \ th" @@ -521,7 +547,7 @@ 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) + by (metis neq_th' vat_t.eq_pv_blocked) ultimately show ?thesis by auto qed qed with Cons show ?thesis @@ -543,7 +569,7 @@ 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) + by (metis neq_th' vat_t.eq_pv_blocked) ultimately show ?thesis by auto qed qed with Cons show ?thesis @@ -576,7 +602,7 @@ 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) + by (metis neq_th' vat_t.eq_pv_blocked) 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) @@ -596,20 +622,53 @@ show ?case by auto qed +(* runing_precond has changed to eq_pv_kept *) + text {* Changing counting balance to detachedness *} -lemmas runing_precond_pre_dtc = runing_precond_pre +lemmas eq_pv_kept_dtc = eq_pv_kept [folded vat_t.detached_eq vat_s.detached_eq] -lemma runing_precond: (* ddd *) - fixes th' +section {* The blocking thread *} + +text {* + The purpose of PIP is to ensure that the most + urgent thread @{term th} is not blocked unreasonably. + Therefore, a clear picture of the blocking thread is essential + to assure people that the purpose is fulfilled. + + The following lemmas will give us such a picture: +*} + +(* ccc *) + +text {* + The following lemma shows the blocking thread @{term th'} + must hold some resource in the very beginning. +*} +lemma runing_cntP_cntV_inv: (* ddd *) assumes th'_in: "th' \ threads s" and neq_th': "th' \ th" and is_runing: "th' \ runing (t@s)" shows "cntP s th' > cntV s th'" using assms -proof - +proof - (* ccc *) + -- {* First, it can be shown that the number of @{term P} and + @{term V} operations can not be equal for thred @{term th'} *} have "cntP s th' \ cntV s th'" - by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in) + proof + assume otherwise: "cntP s th' = cntV s th'" + -- {* The proof goes by contradiction. *} + -- {* We can show that @{term th'} can not be running at moment @{term "t@s"}: *} + have "th' \ runing (t@s)" + proof(rule eq_pv_blocked) + show "th' \ th" using neq_th' by simp + next + show "cntP (t @ s) th' = cntV (t @ s) th'" + using eq_pv_kept[OF th'_in otherwise neq_th'] by simp + qed + -- {* This is obvious in contradiction with assumption @{thm is_runing} *} + thus False using is_runing by simp + qed moreover have "cntV s th' \ cntP s th'" using vat_s.cnp_cnv_cncs by auto ultimately show ?thesis by auto qed @@ -656,7 +715,7 @@ by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append) qed show ?thesis - by (metis add.commute append_assoc eq_pv h.runing_precond_pre + by (metis add.commute append_assoc eq_pv h.eq_pv_kept moment_plus_split neq_th' th'_in) qed @@ -676,13 +735,14 @@ proof - interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) show ?thesis - using h.pv_blocked_pre h1 h2 neq_th' by auto + using h.eq_pv_blocked 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. + This one is useless (* XY *) *) lemma moment_blocked: assumes neq_th': "th' \ th" @@ -701,31 +761,13 @@ show ?thesis by (metis h_j.detached_intro) qed -lemma runing_preced_inversion: +text {* + The following lemmas shows the blocking thread @{text th'} must be live + at the very beginning, i.e. the moment (or state) @{term s}. +*} +lemma runing_threads_inv: (* ddd *) (* ccc *) 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)" + and neq_th': "th' \ th" shows "th' \ threads s" proof - -- {* The proof is by contradiction: *} @@ -774,61 +816,26 @@ } 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. +text {* + The following lemma summarizes several foregoing + lemmas to give an overall picture of the blocking thread @{text "th'"}: *} - -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')" -proof - - from runing_inversion_1[OF _ runing'] - show ?thesis by auto -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)" - by (metis neq_th runing' runing_inversion_2 runing_preced_inversion) - -lemma runing_inversion_4: +lemma runing_inversion: assumes runing': "th' \ runing (t@s)" and neq_th: "th' \ th" shows "th' \ threads s" and "\detached s th'" and "cp (t@s) th' = preced th s" - 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) +proof - + from runing_threads_inv[OF assms] + show "th' \ threads s" . +next + from runing_cntP_cntV_inv[OF runing_threads_inv[OF assms] neq_th runing'] + show "\detached s th'" using vat_s.detached_eq by simp +next + from runing_preced_inversion[OF runing'] + show "cp (t@s) th' = preced th s" . +qed text {* Suppose @{term th} is not running, it is first shown that diff -r 2af87bb52fca -r 25fd656667a7 Moment.thy --- a/Moment.thy Thu Jan 07 22:10:06 2016 +0800 +++ b/Moment.thy Sat Jan 09 22:19:27 2016 +0800 @@ -8,6 +8,91 @@ "firstn (Suc n) [] = []" | "firstn (Suc n) (e#s) = e#(firstn n s)" +lemma upto_map_plus: "map (op + k) [i..j] = [i+k..j+k]" +proof(induct "[i..j]" arbitrary:i j rule:length_induct) + case (1 i j) + thus ?case + proof(cases "i \ j") + case True + hence le_k: "i + k \ j + k" by simp + show ?thesis (is "?L = ?R") + proof - + have "?L = (k + i) # map (op + k) [i + 1..j]" + by (simp add: upto_rec1[OF True]) + moreover have "?R = (i + k) # [i + k + 1..j + k]" + by (simp add: upto_rec1[OF le_k]) + moreover have "map (op + k) [i + 1..j] = [i + k + 1..j + k]" + proof - + have h: "i + k + 1 = (i + 1) + k" by simp + show ?thesis + proof(unfold h, rule 1[rule_format]) + show "length [i + 1..j] < length [i..j]" + using upto_rec1[OF True] by simp + qed simp + qed + ultimately show ?thesis by simp + qed + qed auto +qed + +lemma firstn_alt_def: + "firstn n s = map (\ i. s!(nat i)) [0..(int (min (length s) n)) - 1]" +proof(induct n arbitrary:s) + case (0 s) + thus ?case by auto +next + case (Suc n s) + thus ?case (is "?L = ?R") + proof(cases s) + case Nil + thus ?thesis by simp + next + case (Cons e es) + with Suc + have "?L = e # map (\i. es ! nat i) [0..int (min (length es) n) - 1]" + by simp + also have "... = map (\i. (e # es) ! nat i) [0..int (min (length es) n)]" + (is "?L1 = ?R1") + proof - + have "?R1 = e # map (\i. (e # es) ! nat i) + [1..int (min (length es) n)]" + proof - + have "[0..int (min (length es) n)] = 0#[1..int (min (length es) n)]" + by (simp add: upto.simps) + thus ?thesis by simp + qed + also have "... = ?L1" (is "_#?L2 = _#?R2") + proof - + have "?L2 = ?R2" + proof - + have "map (\i. (e # es) ! nat i) [1..int (min (length es) n)] = + map ((\i. (e # es) ! nat i) \ op + 1) [0..int (min (length es) n) - 1]" + proof - + have "[1..int (min (length es) n)] = + map (op + 1) [0..int (min (length es) n) - 1]" + by (unfold upto_map_plus, simp) + thus ?thesis by simp + qed + also have "... = map (\i. es ! nat i) [0..int (min (length es) n) - 1]" + proof(rule map_cong) + fix x + assume "x \ set [0..int (min (length es) n) - 1]" + thus "((\i. (e # es) ! nat i) \ op + 1) x = es ! nat x" + by (metis atLeastLessThan_iff atLeastLessThan_upto + comp_apply local.Cons nat_0_le nat_int nth_Cons_Suc of_nat_Suc) + qed auto + finally show ?thesis . + qed + thus ?thesis by simp + qed + finally show ?thesis by simp + qed + also have "... = ?R" + by (unfold Cons, simp) + finally show ?thesis . + qed +qed + fun restn :: "nat \ 'a list \ 'a list" where "restn n s = rev (firstn (length s - n) (rev s))" @@ -23,10 +108,8 @@ definition down_to :: "nat \ nat \ 'a list \ 'a list" where "down_to j i s = rev (from_to i j (rev s))" -(* value "down_to 6 2 [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]" value "from_to 2 6 [0, 1, 2, 3, 4, 5, 6, 7]" -*) lemma length_eq_elim_l: "\length xs = length ys; xs@us = ys@vs\ \ xs = ys \ us = vs" by auto @@ -37,10 +120,9 @@ lemma firstn_nil [simp]: "firstn n [] = []" by (cases n, simp+) -(* + value "from_to 0 2 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] @ from_to 2 5 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]" -*) lemma firstn_le: "\ n s'. n \ length s \ firstn n (s@s') = firstn n s" proof (induct s, simp) diff -r 2af87bb52fca -r 25fd656667a7 PIPBasics.thy --- a/PIPBasics.thy Thu Jan 07 22:10:06 2016 +0800 +++ b/PIPBasics.thy Sat Jan 09 22:19:27 2016 +0800 @@ -33,6 +33,13 @@ context valid_trace begin +lemma actor_inv: + assumes "PIP s e" + and "\ isCreate e" + shows "actor e \ runing s" + using assms + by (induct, auto) + lemma ind [consumes 0, case_names Nil Cons, induct type]: assumes "PP []" and "(\s e. valid_trace s \ valid_trace (e#s) \ @@ -1620,6 +1627,52 @@ ultimately show ?thesis by (simp add:cntCS_def) qed +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_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 isP_E: + assumes "isP e" + obtains cs where "e = P (actor e) cs" + using assms by (cases e, auto) + +lemma isV_E: + assumes "isV e" + obtains cs where "e = V (actor e) cs" + using assms by (cases e, auto) (* ccc *) + +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) + context valid_trace begin diff -r 2af87bb52fca -r 25fd656667a7 PIPBasics.thy~ --- a/PIPBasics.thy~ Thu Jan 07 22:10:06 2016 +0800 +++ b/PIPBasics.thy~ Sat Jan 09 22:19:27 2016 +0800 @@ -3048,4 +3048,693 @@ apply (drule_tac th_in_ne) by (unfold preced_def, auto intro: birth_time_lt) +lemma inj_the_preced: + "inj_on (the_preced s) (threads s)" + by (metis inj_onI preced_unique the_preced_def) + +lemma tRAG_alt_def: + "tRAG s = {(Th th1, Th th2) | th1 th2. + \ cs. (Th th1, Cs cs) \ RAG s \ (Cs cs, Th th2) \ RAG s}" + by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) + +lemma tRAG_Field: + "Field (tRAG s) \ Field (RAG s)" + by (unfold tRAG_alt_def Field_def, auto) + +lemma tRAG_ancestorsE: + assumes "x \ ancestors (tRAG s) u" + obtains th where "x = Th th" +proof - + from assms have "(u, x) \ (tRAG s)^+" + by (unfold ancestors_def, auto) + from tranclE[OF this] obtain c where "(c, x) \ tRAG s" by auto + then obtain th where "x = Th th" + by (unfold tRAG_alt_def, auto) + from that[OF this] show ?thesis . +qed + +lemma tRAG_mono: + assumes "RAG s' \ RAG s" + shows "tRAG s' \ tRAG s" + 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 eq_holding, unfolded cs_holding_def] + have " th \ set (wq s cs) \ th = hd (wq s cs)" . + 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 + +lemma RAG_tRAG_transfer: + assumes "vt s'" + assumes "RAG s = RAG s' \ {(Th th, Cs cs)}" + 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:vt_s'.unique_RAG) + + show "acyclic (RAG s')" + by (rule vt_s'.acyclic_RAG) + qed + { fix n1 n2 + assume "(n1, n2) \ ?L" + from this[unfolded tRAG_alt_def] + obtain th1 th2 cs' where + h: "n1 = Th th1" "n2 = Th th2" + "(Th th1, Cs cs') \ RAG s" + "(Cs cs', Th th2) \ RAG s" by auto + from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \ RAG s'" by auto + from h(3) and assms(2) + have "(Th th1, Cs cs') = (Th th, Cs cs) \ + (Th th1, Cs cs') \ RAG s'" by auto + hence "(n1, n2) \ ?R" + proof + assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)" + hence eq_th1: "th1 = th" by simp + moreover have "th2 = th''" + proof - + from h1 have "cs' = cs" by simp + from assms(3) cs_in[unfolded this] rtree.sgv + show ?thesis + by (unfold single_valued_def, auto) + qed + ultimately show ?thesis using h(1,2) by auto + next + assume "(Th th1, Cs cs') \ RAG s'" + with cs_in have "(Th th1, Th th2) \ tRAG s'" + by (unfold tRAG_alt_def, auto) + from this[folded h(1, 2)] show ?thesis by auto + qed + } moreover { + fix n1 n2 + assume "(n1, n2) \ ?R" + hence "(n1, n2) \tRAG s' \ (n1, n2) = (Th th, Th th'')" by auto + hence "(n1, n2) \ ?L" + proof + assume "(n1, n2) \ tRAG s'" + moreover have "... \ ?L" + proof(rule tRAG_mono) + show "RAG s' \ RAG s" by (unfold assms(2), auto) + qed + ultimately show ?thesis by auto + next + assume eq_n: "(n1, n2) = (Th th, Th th'')" + from assms(2, 3) have "(Cs cs, Th th'') \ RAG s" by auto + moreover have "(Th th, Cs cs) \ RAG s" using assms(2) by auto + ultimately show ?thesis + by (unfold eq_n tRAG_alt_def, auto) + qed + } 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))})" +proof - + have "Max (the_preced s ` ({th} \ dependants (wq s) th)) = + Max (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)})" + (is "Max (_ ` ?L) = Max (_ ` ?R)") + proof - + have "?L = ?R" + by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def) + thus ?thesis by simp + qed + thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp) +qed + +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[of s] + have "(a, x) \ (RAG s)^*" by auto + hence "a \ subtree (RAG s) x" by (auto simp:subtree_def) + } thus ?thesis by auto +qed + +lemma tRAG_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 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 - + have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) = + ((the_preced s \ the_thread) ` subtree (tRAG s) (Th th))" + by auto + thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto) +qed + +lemma cp_gen_def_cond: + assumes "x = Th th" + shows "cp s th = cp_gen s (Th th)" +by (unfold cp_alt_def1 cp_gen_def, simp) + +lemma cp_gen_over_set: + assumes "\ x \ A. \ th. x = Th th" + shows "cp_gen s ` A = (cp s \ the_thread) ` A" +proof(rule f_image_eq) + fix a + assume "a \ A" + from assms[rule_format, OF this] + obtain th where eq_a: "a = Th th" by auto + show "cp_gen s a = (cp s \ the_thread) a" + by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) +qed + + +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)" +proof - + { fix x + assume "x \ ancestors (RAG s) (Th th)" + hence h: "(Th th, x) \ (RAG s)^+" by (auto simp:ancestors_def) + from tranclD[OF this] + obtain z where "(Th th, z) \ RAG s" by auto + with assms(1) have False + apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) + by (fold wq_def, blast) + } thus ?thesis by (unfold root_def, auto) +qed + +lemma readys_in_no_subtree: + assumes "th \ readys s" + and "th' \ th" + shows "Th th \ subtree (RAG s) (Th th')" +proof + assume "Th th \ subtree (RAG s) (Th th')" + thus False + proof(cases rule:subtreeE) + case 1 + with assms show ?thesis by auto + next + case 2 + with readys_root[OF assms(1)] + show ?thesis by (auto simp:root_def) + qed +qed + +lemma not_in_thread_isolated: + assumes "th \ threads s" + shows "(Th th) \ Field (RAG s)" +proof + assume "(Th th) \ Field (RAG s)" + with dm_RAG_threads 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 show "finite (RAG s)" . +next + from acyclic_RAG show "acyclic (RAG s)" . +qed + +lemma sgv_wRAG: "single_valued (wRAG s)" + using waiting_unique + by (unfold single_valued_def wRAG_def, auto) + +lemma sgv_hRAG: "single_valued (hRAG s)" + using holding_unique + by (unfold single_valued_def hRAG_def, auto) + +lemma sgv_tRAG: "single_valued (tRAG s)" + by (unfold tRAG_def, rule single_valued_relcomp, + insert sgv_wRAG sgv_hRAG, auto) + +lemma acyclic_tRAG: "acyclic (tRAG s)" +proof(unfold tRAG_def, rule acyclic_compose) + show "acyclic (RAG s)" using acyclic_RAG . +next + show "wRAG s \ RAG s" unfolding RAG_split by auto +next + show "hRAG s \ RAG s" unfolding RAG_split by auto +qed + +lemma sgv_RAG: "single_valued (RAG s)" + using unique_RAG by (auto simp:single_valued_def) + +lemma rtree_RAG: "rtree (RAG s)" + using sgv_RAG acyclic_RAG + by (unfold rtree_def rtree_axioms_def sgv_def, auto) + +end + +sublocale valid_trace < rtree_RAG: rtree "RAG s" +proof + show "single_valued (RAG s)" + apply (intro_locales) + by (unfold single_valued_def, + auto intro:unique_RAG) + + show "acyclic (RAG s)" + by (rule acyclic_RAG) +qed + +sublocale valid_trace < rtree_s: rtree "tRAG s" +proof(unfold_locales) + from sgv_tRAG show "single_valued (tRAG s)" . +next + from acyclic_tRAG show "acyclic (tRAG s)" . +qed + +sublocale valid_trace < fsbtRAGs : fsubtree "RAG s" +proof - + show "fsubtree (RAG s)" + proof(intro_locales) + show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] . + next + show "fsubtree_axioms (RAG s)" + proof(unfold fsubtree_axioms_def) + from wf_RAG show "wf (RAG s)" . + qed + qed +qed + +sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s" +proof - + have "fsubtree (tRAG s)" + proof - + have "fbranch (tRAG s)" + proof(unfold tRAG_def, rule fbranch_compose) + show "fbranch (wRAG s)" + proof(rule finite_fbranchI) + 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 + show "finite (hRAG s)" by (unfold RAG_split, auto) + qed + qed + moreover have "wf (tRAG s)" + proof(rule wf_subset) + show "wf (RAG s O RAG s)" using wf_RAG + by (fold wf_comp_self, simp) + next + show "tRAG s \ (RAG s O RAG s)" + by (unfold tRAG_alt_def, auto) + qed + ultimately show ?thesis + by (unfold fsubtree_def fsubtree_axioms_def,auto) + qed + from this[folded tRAG_def] show "fsubtree (tRAG s)" . +qed + +lemma Max_UNION: + assumes "finite A" + and "A \ {}" + and "\ M \ f ` A. finite M" + and "\ M \ f ` A. M \ {}" + shows "Max (\x\ A. f x) = Max (Max ` f ` A)" (is "?L = ?R") + using assms[simp] +proof - + have "?L = Max (\(f ` A))" + by (fold Union_image_eq, simp) + also have "... = ?R" + by (subst Max_Union, simp+) + finally show ?thesis . +qed + +lemma max_Max_eq: + assumes "finite A" + and "A \ {}" + and "x = y" + shows "max x (Max A) = Max ({y} \ A)" (is "?L = ?R") +proof - + have "?R = Max (insert y A)" by simp + also from assms have "... = ?L" + by (subst Max.insert, simp+) + finally show ?thesis by simp +qed + +context valid_trace +begin + +(* ddd *) +lemma cp_gen_rec: + assumes "x = Th th" + shows "cp_gen s x = Max ({the_preced s th} \ (cp_gen s) ` children (tRAG s) x)" +proof(cases "children (tRAG s) x = {}") + case True + show ?thesis + by (unfold True cp_gen_def subtree_children, simp add:assms) +next + case False + hence [simp]: "children (tRAG s) x \ {}" by auto + note fsbttRAGs.finite_subtree[simp] + have [simp]: "finite (children (tRAG s) x)" + by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], + rule children_subtree) + { fix r x + have "subtree r x \ {}" by (auto simp:subtree_def) + } note this[simp] + have [simp]: "\x\children (tRAG s) x. subtree (tRAG s) x \ {}" + proof - + from False obtain q where "q \ children (tRAG s) x" by blast + moreover have "subtree (tRAG s) q \ {}" by simp + ultimately show ?thesis by blast + qed + have h: "Max ((the_preced s \ the_thread) ` + ({x} \ \(subtree (tRAG s) ` children (tRAG s) x))) = + Max ({the_preced s th} \ cp_gen s ` children (tRAG s) x)" + (is "?L = ?R") + proof - + let "Max (?f ` (?A \ \ (?g ` ?B)))" = ?L + let "Max (_ \ (?h ` ?B))" = ?R + let ?L1 = "?f ` \(?g ` ?B)" + have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" + proof - + have "?L1 = ?f ` (\ x \ ?B.(?g x))" by simp + also have "... = (\ x \ ?B. ?f ` (?g x))" by auto + finally have "Max ?L1 = Max ..." by simp + also have "... = Max (Max ` (\x. ?f ` subtree (tRAG s) x) ` ?B)" + by (subst Max_UNION, simp+) + also have "... = Max (cp_gen s ` children (tRAG s) x)" + by (unfold image_comp cp_gen_alt_def, simp) + finally show ?thesis . + qed + show ?thesis + proof - + have "?L = Max (?f ` ?A \ ?L1)" by simp + also have "... = max (the_preced s (the_thread x)) (Max ?L1)" + by (subst Max_Un, simp+) + also have "... = max (?f x) (Max (?h ` ?B))" + by (unfold eq_Max_L1, simp) + also have "... =?R" + by (rule max_Max_eq, (simp)+, unfold assms, simp) + finally show ?thesis . + qed + qed thus ?thesis + by (fold h subtree_children, unfold cp_gen_def, simp) +qed + +lemma cp_rec: + "cp s th = Max ({the_preced s th} \ + (cp s o the_thread) ` children (tRAG s) (Th th))" +proof - + have "Th th = Th th" by simp + note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this] + show ?thesis + proof - + have "cp_gen s ` children (tRAG s) (Th th) = + (cp s \ the_thread) ` children (tRAG s) (Th th)" + proof(rule cp_gen_over_set) + show " \x\children (tRAG s) (Th th). \th. x = Th th" + by (unfold tRAG_alt_def, auto simp:children_def) + qed + thus ?thesis by (subst (1) h(1), unfold h(2), simp) + qed +qed + +end + +(* keep *) +lemma next_th_holding: + assumes vt: "vt s" + and nxt: "next_th s th cs th'" + shows "holding (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 + thus ?thesis + by (unfold cs_holding_def, auto) +qed + +context valid_trace +begin + +lemma next_th_waiting: + 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 cs, unfolded h] + have dst: "distinct (th # rest)" . + have in_rest: "th' \ set rest" + proof(unfold h, rule someI2) + show "distinct rest \ set rest = set rest" using dst by auto + next + fix x assume "distinct x \ set x = set rest" + with h(2) + show "hd x \ set (rest)" by (cases x, auto) + qed + hence "th' \ set (wq s cs)" by (unfold h(1), auto) + moreover have "th' \ hd (wq s cs)" + by (unfold h(1), insert in_rest dst, auto) + ultimately show ?thesis by (auto simp:cs_waiting_def) +qed + +lemma next_th_RAG: + assumes nxt: "next_th (s::event list) th cs th'" + shows "{(Cs cs, Th th), (Th th', Cs cs)} \ RAG s" + 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" +where "cps s = {(th, cp s th) | th . th \ threads s}" + +end diff -r 2af87bb52fca -r 25fd656667a7 PIPDefs.thy --- a/PIPDefs.thy Thu Jan 07 22:10:06 2016 +0800 +++ b/PIPDefs.thy Sat Jan 09 22:19:27 2016 +0800 @@ -37,6 +37,24 @@ V thread cs | -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *} Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *} +fun actor :: "event \ thread" where + "actor (Create th pty) = th" | + "actor (Exit th) = th" | + "actor (P th cs) = th" | + "actor (V th cs) = th" | + "actor (Set th pty) = th" + +fun isCreate :: "event \ bool" where + "isCreate (Create th pty) = True" | + "isCreate _ = False" + +fun isP :: "event \ bool" where + "isP (P th cs) = True" | + "isP _ = False" + +fun isV :: "event \ bool" where + "isV (V th cs) = True" | + "isV _ = False" text {* As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists of events, diff -r 2af87bb52fca -r 25fd656667a7 PIPDefs.thy~ --- a/PIPDefs.thy~ Thu Jan 07 22:10:06 2016 +0800 +++ b/PIPDefs.thy~ Sat Jan 09 22:19:27 2016 +0800 @@ -1,7 +1,7 @@ chapter {* Definitions *} (*<*) theory PIPDefs -imports Precedence_ord Moment +imports Precedence_ord Moment RTree Max begin (*>*) @@ -607,6 +607,37 @@ *} definition cntV :: "state \ thread \ nat" where "cntV s th = count (\ e. \ cs. e = V th cs) s" + +text {* @{text "the_preced"} is also the same as @{text "preced"}, the only + difference is the order of arguemts. *} +definition "the_preced s th = preced th s" + +text {* @{term "the_thread"} extracts thread out of RAG node. *} +fun the_thread :: "node \ thread" where + "the_thread (Th th) = th" + +text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *} +definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" + +text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *} +definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}" + +text {* + The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}. + It characterizes the dependency between threads when calculating current + precedences. It is defined as the composition of the above two sub-graphs, + names @{term "wRAG"} and @{term "hRAG"}. + *} +definition "tRAG s = wRAG s O hRAG s" + +text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *} +lemma RAG_split: "RAG s = (wRAG s \ hRAG s)" + by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv + s_holding_abv cs_RAG_def, auto) + +definition "cp_gen s x = + Max ((the_preced s \ the_thread) ` subtree (tRAG s) x)" + (*<*) end