diff -r 031d2ae9c9b8 -r b620a2a0806a ExtGG.thy --- a/ExtGG.thy Tue Dec 22 23:13:31 2015 +0800 +++ b/ExtGG.thy Wed Jan 06 20:46:14 2016 +0800 @@ -2,67 +2,93 @@ imports PrioG CpsG begin -lemma birth_time_lt: "s \ [] \ last_set th s < length s" - apply (induct s, simp) -proof - - fix a s - assume ih: "s \ [] \ last_set th s < length s" - and eq_as: "a # s \ []" - show "last_set th (a # s) < length (a # s)" - proof(cases "s \ []") - case False - from False show ?thesis - by (cases a, auto simp:last_set.simps) - next - case True - from ih [OF True] show ?thesis - by (cases a, auto simp:last_set.simps) - qed +text {* + The following two auxiliary lemmas are used to reason about @{term Max}. +*} +lemma image_Max_eqI: + assumes "finite B" + and "b \ B" + and "\ x \ B. f x \ f b" + shows "Max (f ` B) = f b" + using assms + using Max_eqI by blast + +lemma image_Max_subset: + assumes "finite A" + and "B \ A" + and "a \ B" + and "Max (f ` A) = f a" + shows "Max (f ` B) = f a" +proof(rule image_Max_eqI) + show "finite B" + using assms(1) assms(2) finite_subset by auto +next + show "a \ B" using assms by simp +next + show "\x\B. f x \ f a" + by (metis Max_ge assms(1) assms(2) assms(4) + finite_imageI image_eqI subsetCE) qed -lemma th_in_ne: "th \ threads s \ s \ []" - by (induct s, auto simp:threads.simps) - -lemma preced_tm_lt: "th \ threads s \ preced th s = Prc x y \ y < length s" - apply (drule_tac th_in_ne) - by (unfold preced_def, auto intro: birth_time_lt) - +text {* + The following locale @{text "highest_gen"} sets the basic context for our + investigation: supposing thread @{text th} holds the highest @{term cp}-value + in state @{text s}, which means the task for @{text th} is the + most urgent. We want to show that + @{text th} is treated correctly by PIP, which means + @{text th} will not be blocked unreasonably by other less urgent + threads. +*} locale highest_gen = fixes s th prio tm assumes vt_s: "vt s" and threads_s: "th \ threads s" and highest: "preced th s = Max ((cp s)`threads s)" - and preced_th: "preced th s = Prc prio tm" + -- {* The internal structure of @{term th}'s precedence is exposed:*} + and preced_th: "preced th s = Prc prio tm" +-- {* @{term s} is a valid trace, so it will inherit all results derived for + a valid trace: *} sublocale highest_gen < vat_s: valid_trace "s" by (unfold_locales, insert vt_s, simp) context highest_gen begin +text {* + @{term tm} is the time when the precedence of @{term th} is set, so + @{term tm} must be a valid moment index into @{term s}. +*} lemma lt_tm: "tm < length s" by (insert preced_tm_lt[OF threads_s preced_th], simp) +text {* + Since @{term th} holds the highest precedence and @{text "cp"} + is the highest precedence of all threads in the sub-tree of + @{text "th"} and @{text th} is among these threads, + its @{term cp} must equal to its precedence: +*} lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R") proof - have "?L \ ?R" by (unfold highest, rule Max_ge, - auto simp:threads_s finite_threads[OF vt_s]) + auto simp:threads_s finite_threads) moreover have "?R \ ?L" by (unfold vat_s.cp_rec, rule Max_ge, auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) ultimately show ?thesis by auto qed +(* ccc *) lemma highest_cp_preced: "cp s th = Max ((\ th'. preced th' s) ` threads s)" - by (fold max_cp_eq[OF vt_s], unfold eq_cp_s_th, insert highest, simp) + by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp) lemma highest_preced_thread: "preced th s = Max ((\ th'. preced th' s) ` threads s)" by (fold eq_cp_s_th, unfold highest_cp_preced, simp) lemma highest': "cp s th = Max (cp s ` threads s)" proof - - from highest_cp_preced max_cp_eq[OF vt_s, symmetric] + from highest_cp_preced max_cp_eq[symmetric] show ?thesis by simp qed @@ -75,6 +101,9 @@ and set_diff_low: "Set th' prio' \ set t \ th' \ th \ prio' \ prio" and exit_diff: "Exit th' \ set t \ th' \ th" +sublocale extend_highest_gen < vat_t: valid_trace "t@s" + by (unfold_locales, insert vt_t, simp) + lemma step_back_vt_app: assumes vt_ts: "vt (t@s)" shows "vt s" @@ -110,14 +139,6 @@ context extend_highest_gen begin -(* - lemma red_moment: - "extend_highest_gen s th prio tm (moment i t)" - apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) - apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) - by (unfold highest_gen_def, auto dest:step_back_vt_app) -*) - lemma ind [consumes 0, case_names Nil Cons, induct type]: assumes h0: "R []" @@ -218,48 +239,21 @@ qed qed -lemma Max_remove_less: - assumes "finite A" - and "a \ A" - and "b \ A" - and "a \ b" - and "inj_on f A" - and "f a = Max (f ` A)" - shows "Max (f ` (A - {b})) = (Max (f ` A))" -proof - - have "Max (f ` (A - {b})) = Max (f`A - {f b})" - proof - - have "f ` (A - {b}) = f ` A - f ` {b}" - by (rule inj_on_image_set_diff[OF assms(5)], insert assms(3), auto) - thus ?thesis by simp - qed - also have "... = - (if f ` A - {f b} - {f a} = {} then f a else max (f a) (Max (f ` A - {f b} - {f a})))" - proof(subst Max.remove) - from assms show "f a \ f ` A - {f b}" - by (meson DiffI empty_iff imageI inj_on_eq_iff insert_iff) - next - from assms(1) show "finite (f ` A - {f b})" by auto - qed auto - also have "... = Max (f ` A)" (is "?L = ?R") - proof(cases "f ` A - {f b} - {f a} = {}") - case True - with assms show ?thesis by auto - next - case False - hence "?L = max (f a) (Max (f ` A - {f b} - {f a}))" - by simp - also have "... = ?R" - proof - - from assms False - have "(Max (f ` A - {f b} - {f a})) \ f a" by auto - thus ?thesis by (simp add: assms(6) max_def) - qed - finally show ?thesis . - qed - finally show ?thesis . -qed +text {* + According to @{thm th_kept}, thread @{text "th"} has its living status + and precedence kept along the way of @{text "t"}. The following lemma + shows that this preserved precedence of @{text "th"} remains as the highest + along the way of @{text "t"}. + The proof goes by induction over @{text "t"} using the specialized + induction rule @{thm ind}, followed by case analysis of each possible + operations of PIP. All cases follow the same pattern rendered by the + generalized introduction rule @{thm "image_Max_eqI"}. + + The very essence is to show that precedences, no matter whether they are newly introduced + or modified, are always lower than the one held by @{term "th"}, + which by @{thm th_kept} is preserved along the way. +*} lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" proof(induct rule:ind) case Nil @@ -273,62 +267,74 @@ show ?case proof(cases e) case (Create thread prio') - from Cons(2)[unfolded this] - have thread_not_in: "thread \ threads (t@s)" by (cases, simp) show ?thesis (is "Max (?f ` ?A) = ?t") proof - - have "Max (?f ` ?A) = Max (insert (?f thread) (?f ` (threads (t@s))))" - by (unfold Create, simp) - moreover have "\ = max (?f thread) (Max (?f ` (threads (t@s))))" - proof(rule Max.insert) - from finite_threads[OF Cons(1)] - show "finite (?f ` (threads (t@s)))" by simp - qed (insert h_t.th_kept, auto) - moreover have "(Max (?f ` (threads (t@s)))) = ?t" - proof - - have "(\th'. preced th' ((e # t) @ s)) ` threads (t @ s) = - (\th'. preced th' (t @ s)) ` threads (t @ s)" - by (intro f_image_eq, insert thread_not_in, auto simp:Create preced_def) - with Cons show ?thesis by (auto simp:the_preced_def) + -- {* The following is the common pattern of each branch of the case analysis. *} + -- {* The major part is to show that @{text "th"} holds the highest precedence: *} + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto + next + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume "x \ ?A" + hence "x = thread \ x \ threads (t@s)" by (auto simp:Create) + thus "?f x \ ?f th" + proof + assume "x = thread" + thus ?thesis + apply (simp add:Create the_preced_def preced_def, fold preced_def) + using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force + next + assume h: "x \ threads (t @ s)" + from Cons(2)[unfolded Create] + have "x \ thread" using h by (cases, auto) + hence "?f x = the_preced (t@s) x" + by (simp add:Create the_preced_def preced_def) + hence "?f x \ Max (the_preced (t@s) ` threads (t@s))" + by (simp add: h_t.finite_threads h) + also have "... = ?f th" + by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + finally show ?thesis . + qed + qed qed - moreover have "?f thread < ?t" - proof - - from h_e.create_low and Create - have "prio' \ prio" by auto - thus ?thesis - by (unfold preced_th, unfold Create, insert lt_tm, - auto simp:preced_def precedence_less_def preced_th the_preced_def) - qed - ultimately show ?thesis by (auto simp:max_def) - qed + -- {* The minor part is to show that the precedence of @{text "th"} + equals to preserved one, given by the foregoing lemma @{thm th_kept} *} + also have "... = ?t" using h_e.th_kept the_preced_def by auto + -- {* Then it follows trivially that the precedence preserved + for @{term "th"} remains the maximum of all living threads along the way. *} + finally show ?thesis . + qed next case (Exit thread) - show ?thesis + show ?thesis (is "Max (?f ` ?A) = ?t") proof - - have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = - Max (the_preced (t @ s) ` (threads (t @ s)))" - proof(rule Max_remove_less) - show "th \ thread" using Exit h_e.exit_diff by auto + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto next - from Cons(2)[unfolded Exit] - show "thread \ threads (t @ s)" - by (cases, simp add: readys_def runing_def) - next - show "finite (threads (t @ s))" by (simp add: finite_threads h_t.vt_t) + show "th \ ?A" using h_e.th_kept by auto next - show "th \ threads (t @ s)" by (simp add: h_t.th_kept) - next - show "inj_on (the_preced (t @ s)) (threads (t @ s))" by (simp add: inj_the_preced) - next - show "the_preced (t @ s) th = Max (the_preced (t @ s) ` threads (t @ s))" - by (simp add: Cons.hyps(5) h_t.th_kept the_preced_def) + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume "x \ ?A" + hence "x \ threads (t@s)" by (simp add: Exit) + hence "?f x \ Max (?f ` threads (t@s))" + by (simp add: h_t.finite_threads) + also have "... \ ?f th" + apply (simp add:Exit the_preced_def preced_def, fold preced_def) + using Cons.hyps(5) h_t.th_kept the_preced_def by auto + finally show "?f x \ ?f th" . + qed qed - from this[unfolded Cons(5)] - have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = preced th s" . - moreover have "the_preced ((e # t) @ s) = the_preced (t@s)" - by (auto simp:Exit the_preced_def preced_def) - ultimately show ?thesis by (simp add:Exit) - qed + also have "... = ?t" using h_e.th_kept the_preced_def by auto + finally show ?thesis . + qed next case (P thread cs) with Cons @@ -337,202 +343,158 @@ case (V thread cs) with Cons show ?thesis by (auto simp:preced_def the_preced_def) - next (* ccc *) + next case (Set thread prio') - show ?thesis - apply (unfold Set, simp, insert Cons(5)) (* ccc *) - find_theorems priority Set - find_theorems preced Set + show ?thesis (is "Max (?f ` ?A) = ?t") proof - - let ?B = "threads (t@s)" - from Cons have "extend_highest_gen s th prio tm (e # t)" by auto - from extend_highest_gen.set_diff_low[OF this] and Set - have neq_thread: "thread \ th" and le_p: "prio' \ prio" by auto - from Set have "Max (?f ` ?A) = Max (?f ` ?B)" by simp - also have "\ = ?t" - proof(rule Max_eqI) - fix y - assume y_in: "y \ ?f ` ?B" - then obtain th1 where - th1_in: "th1 \ ?B" and eq_y: "y = ?f th1" by auto - show "y \ ?t" - proof(cases "th1 = thread") - case True - with neq_thread le_p eq_y Set - show ?thesis - apply (subst preced_th, insert lt_tm) - by (auto simp:preced_def precedence_le_def) - next - case False - with Set eq_y - have "y = preced th1 (t@s)" - by (simp add:preced_def) - moreover have "\ \ ?t" - proof - - from Cons - have "?t = Max ((\ th'. preced th' (t@s)) ` (threads (t@s)))" - by auto - moreover have "preced th1 (t@s) \ \" - proof(rule Max_ge) - from th1_in - show "preced th1 (t @ s) \ (\th'. preced th' (t @ s)) ` threads (t @ s)" - by simp - next - show "finite ((\th'. preced th' (t @ s)) ` threads (t @ s))" - proof - - from Cons have "vt (t @ s)" by auto - from finite_threads[OF this] show ?thesis by auto - qed + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto + next + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume h: "x \ ?A" + show "?f x \ ?f th" + proof(cases "x = thread") + case True + moreover have "the_preced (Set thread prio' # t @ s) thread \ the_preced (t @ s) th" + proof - + have "the_preced (t @ s) th = Prc prio tm" + using h_t.th_kept preced_th by (simp add:the_preced_def) + moreover have "prio' \ prio" using Set h_e.set_diff_low by auto + ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def) qed - ultimately show ?thesis by auto + ultimately show ?thesis + by (unfold Set, simp add:the_preced_def preced_def) + next + case False + then have "?f x = the_preced (t@s) x" + by (simp add:the_preced_def preced_def Set) + also have "... \ Max (the_preced (t@s) ` threads (t@s))" + using Set h h_t.finite_threads by auto + also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + finally show ?thesis . qed - ultimately show ?thesis by auto - qed - next - from Cons and finite_threads - show "finite (?f ` ?B)" by auto - next - from Cons have "extend_highest_gen s th prio tm t" by auto - from extend_highest_gen.th_kept [OF this] - have h: "th \ threads (t @ s) \ preced th (t @ s) = preced th s" . - show "?t \ (?f ` ?B)" - proof - - from neq_thread Set h - have "?t = ?f th" by (auto simp:preced_def) - with h show ?thesis by auto qed qed + also have "... = ?t" using h_e.th_kept the_preced_def by auto finally show ?thesis . - qed + qed qed qed -lemma max_preced: "preced th (t@s) = Max ((\ th'. preced th' (t @ s)) ` (threads (t@s)))" +lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))" by (insert th_kept max_kept, auto) -lemma th_cp_max_preced: "cp (t@s) th = Max ((\ th'. preced th' (t @ s)) ` (threads (t@s)))" - (is "?L = ?R") +text {* + The reason behind the following lemma is that: + Since @{term "cp"} is defined as the maximum precedence + of those threads contained in the sub-tree of node @{term "Th th"} + in @{term "RAG (t@s)"}, and all these threads are living threads, and + @{term "th"} is also among them, the maximum precedence of + them all must be the one for @{text "th"}. +*} +lemma th_cp_max_preced: + "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R") proof - - have "?L = cpreced (wq (t@s)) (t@s) th" - by (unfold cp_eq_cpreced, simp) - also have "\ = ?R" - proof(unfold cpreced_def) - show "Max ((\th. preced th (t @ s)) ` ({th} \ dependants (wq (t @ s)) th)) = - Max ((\th'. preced th' (t @ s)) ` threads (t @ s))" - (is "Max (?f ` ({th} \ ?A)) = Max (?f ` ?B)") - proof(cases "?A = {}") - case False - have "Max (?f ` ({th} \ ?A)) = Max (insert (?f th) (?f ` ?A))" by simp - moreover have "\ = max (?f th) (Max (?f ` ?A))" - proof(rule Max_insert) - show "finite (?f ` ?A)" - proof - - from dependants_threads[OF vt_t] - have "?A \ threads (t@s)" . - moreover from finite_threads[OF vt_t] have "finite \" . - ultimately show ?thesis - by (auto simp:finite_subset) - qed + let ?f = "the_preced (t@s)" + have "?L = ?f th" + proof(unfold cp_alt_def, rule image_Max_eqI) + show "finite {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + proof - + have "{th'. Th th' \ subtree (RAG (t @ s)) (Th th)} = + the_thread ` {n . n \ subtree (RAG (t @ s)) (Th th) \ + (\ th'. n = Th th')}" + by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps) + moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) + ultimately show ?thesis by simp + qed + next + show "th \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + by (auto simp:subtree_def) + next + show "\x\{th'. Th th' \ subtree (RAG (t @ s)) (Th th)}. + the_preced (t @ s) x \ the_preced (t @ s) th" + proof + fix th' + assume "th' \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + hence "Th th' \ subtree (RAG (t @ s)) (Th th)" by auto + moreover have "... \ Field (RAG (t @ s)) \ {Th th}" + by (meson subtree_Field) + ultimately have "Th th' \ ..." by auto + hence "th' \ threads (t@s)" + proof + assume "Th th' \ {Th th}" + thus ?thesis using th_kept by auto next - from False show "(?f ` ?A) \ {}" by simp + assume "Th th' \ Field (RAG (t @ s))" + thus ?thesis using vat_t.not_in_thread_isolated by blast qed - moreover have "\ = Max (?f ` ?B)" - proof - - from max_preced have "?f th = Max (?f ` ?B)" . - moreover have "Max (?f ` ?A) \ \" - proof(rule Max_mono) - from False show "(?f ` ?A) \ {}" by simp - next - show "?f ` ?A \ ?f ` ?B" - proof - - have "?A \ ?B" by (rule dependants_threads[OF vt_t]) - thus ?thesis by auto - qed - next - from finite_threads[OF vt_t] - show "finite (?f ` ?B)" by simp - qed - ultimately show ?thesis - by (auto simp:max_def) - qed - ultimately show ?thesis by auto - next - case True - with max_preced show ?thesis by auto + thus "the_preced (t @ s) th' \ the_preced (t @ s) th" + by (metis Max_ge finite_imageI finite_threads image_eqI + max_kept th_kept the_preced_def) qed qed + also have "... = ?R" by (simp add: max_preced the_preced_def) finally show ?thesis . qed lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))" - by (unfold max_cp_eq[OF vt_t] th_cp_max_preced, simp) + using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger lemma th_cp_preced: "cp (t@s) th = preced th s" by (fold max_kept, unfold th_cp_max_preced, simp) lemma preced_less: - fixes th' assumes th'_in: "th' \ threads s" and neq_th': "th' \ th" shows "preced th' s < preced th s" -proof - - have "preced th' s \ Max ((\th'. preced th' s) ` threads s)" - proof(rule Max_ge) - from finite_threads [OF vt_s] - show "finite ((\th'. preced th' s) ` threads s)" by simp - next - from th'_in show "preced th' s \ (\th'. preced th' s) ` threads s" - by simp - qed - moreover have "preced th' s \ preced th s" - proof - assume "preced th' s = preced th s" - from preced_unique[OF this th'_in] neq_th' threads_s - show "False" by (auto simp:readys_def) - qed - ultimately show ?thesis using highest_preced_thread - by auto -qed + using assms +by (metis Max.coboundedI finite_imageI highest not_le order.trans + preced_linorder rev_image_eqI threads_s vat_s.finite_threads + vat_s.le_cp) + +text {* + Counting of the number of @{term "P"} and @{term "V"} operations + is the cornerstone of a large number of the following proofs. + The reason is that this counting is quite easy to calculate and + convenient to use in the reasoning. + + The following lemma shows that the counting controls whether + a thread is running or not. +*} lemma pv_blocked_pre: - fixes th' assumes th'_in: "th' \ threads (t@s)" and neq_th': "th' \ th" and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" shows "th' \ runing (t@s)" proof - assume "th' \ runing (t@s)" - hence "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" - by (auto simp:runing_def) - with max_cp_readys_threads [OF vt_t] - have "cp (t @ s) th' = Max (cp (t@s) ` threads (t@s))" - by auto - moreover from th_cp_max have "cp (t @ s) th = \" by simp - ultimately have "cp (t @ s) th' = cp (t @ s) th" by simp - moreover from th_cp_preced and th_kept have "\ = preced th (t @ s)" - by simp - finally have h: "cp (t @ s) th' = preced th (t @ s)" . + assume otherwise: "th' \ runing (t@s)" show False proof - - have "dependants (wq (t @ s)) th' = {}" - by (rule count_eq_dependants [OF vt_t eq_pv]) - moreover have "preced th' (t @ s) \ preced th (t @ s)" - proof - assume "preced th' (t @ s) = preced th (t @ s)" - hence "th' = th" - proof(rule preced_unique) - from th_kept show "th \ threads (t @ s)" by simp - next - from th'_in show "th' \ threads (t @ s)" by simp + have "th' = th" + proof(rule preced_unique) + show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") + proof - + have "?L = cp (t@s) th'" + by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) + also have "... = cp (t @ s) th" using otherwise + by (metis (mono_tags, lifting) mem_Collect_eq + runing_def th_cp_max vat_t.max_cp_readys_threads) + also have "... = ?R" by (metis th_cp_preced th_kept) + finally show ?thesis . qed - with assms show False by simp - qed - ultimately show ?thesis - by (insert h, unfold cp_eq_cpreced cpreced_def, simp) - qed + qed (auto simp: th'_in th_kept) + moreover have "th' \ th" using neq_th' . + ultimately show ?thesis by simp + qed qed -lemmas pv_blocked = pv_blocked_pre[folded detached_eq [OF vt_t]] +lemmas pv_blocked = pv_blocked_pre[folded detached_eq] lemma runing_precond_pre: fixes th' @@ -541,113 +503,102 @@ and neq_th': "th' \ th" shows "th' \ threads (t@s) \ cntP (t@s) th' = cntV (t@s) th'" -proof - - show ?thesis - proof(induct rule:ind) - case (Cons e t) - from Cons - have in_thread: "th' \ threads (t @ s)" - and not_holding: "cntP (t @ s) th' = cntV (t @ s) th'" by auto - from Cons have "extend_highest_gen s th prio tm t" by auto - then have not_runing: "th' \ runing (t @ s)" - apply(rule extend_highest_gen.pv_blocked) - using Cons(1) in_thread neq_th' not_holding - apply(simp_all add: detached_eq) - done +proof(induct rule:ind) + case (Cons e t) + interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp + interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp show ?case proof(cases e) - case (V thread cs) - from Cons and V have vt_v: "vt (V thread cs#(t@s))" by auto - + case (P thread cs) show ?thesis proof - - from Cons and V have "step (t@s) (V thread cs)" by auto - hence neq_th': "thread \ th'" - proof(cases) - assume "thread \ runing (t@s)" - moreover have "th' \ runing (t@s)" by fact - ultimately show ?thesis by auto + have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" + proof - + have "thread \ th'" + proof - + have "step (t@s) (P thread cs)" using Cons P by auto + thus ?thesis + proof(cases) + assume "thread \ runing (t@s)" + moreover have "th' \ runing (t@s)" using Cons(5) + by (metis neq_th' vat_t.pv_blocked_pre) + ultimately show ?thesis by auto + qed + qed with Cons show ?thesis + by (unfold P, simp add:cntP_def cntV_def count_def) qed - with not_holding have cnt_eq: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - by (unfold V, simp add:cntP_def cntV_def count_def) - moreover from in_thread - have in_thread': "th' \ threads ((e # t) @ s)" by (unfold V, simp) + moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold P, simp) ultimately show ?thesis by auto qed next - case (P thread cs) - from Cons and P have "step (t@s) (P thread cs)" by auto - hence neq_th': "thread \ th'" - proof(cases) - assume "thread \ runing (t@s)" - moreover note not_runing - ultimately show ?thesis by auto - qed - with Cons and P have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - by (auto simp:cntP_def cntV_def count_def) - moreover from Cons and P have in_thread': "th' \ threads ((e # t) @ s)" - by auto - ultimately show ?thesis by auto - next - case (Create thread prio') - from Cons and Create have "step (t@s) (Create thread prio')" by auto - hence neq_th': "thread \ th'" - proof(cases) - assume "thread \ threads (t @ s)" - moreover have "th' \ threads (t@s)" by fact + case (V thread cs) + show ?thesis + proof - + have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" + proof - + have "thread \ th'" + proof - + have "step (t@s) (V thread cs)" using Cons V by auto + thus ?thesis + proof(cases) + assume "thread \ runing (t@s)" + moreover have "th' \ runing (t@s)" using Cons(5) + by (metis neq_th' vat_t.pv_blocked_pre) + ultimately show ?thesis by auto + qed + qed with Cons show ?thesis + by (unfold V, simp add:cntP_def cntV_def count_def) + qed + moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold V, simp) ultimately show ?thesis by auto qed - with Cons and Create - have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - by (auto simp:cntP_def cntV_def count_def) - moreover from Cons and Create - have in_thread': "th' \ threads ((e # t) @ s)" by auto - ultimately show ?thesis by auto + next + case (Create thread prio') + show ?thesis + proof - + have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" + proof - + have "thread \ th'" + proof - + have "step (t@s) (Create thread prio')" using Cons Create by auto + thus ?thesis using Cons(5) by (cases, auto) + qed with Cons show ?thesis + by (unfold Create, simp add:cntP_def cntV_def count_def) + qed + moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold Create, simp) + ultimately show ?thesis by auto + qed next case (Exit thread) - from Cons and Exit have "step (t@s) (Exit thread)" by auto - hence neq_th': "thread \ th'" - proof(cases) - assume "thread \ runing (t @ s)" - moreover note not_runing + show ?thesis + proof - + have neq_thread: "thread \ th'" + proof - + have "step (t@s) (Exit thread)" using Cons Exit by auto + thus ?thesis apply (cases) using Cons(5) + by (metis neq_th' vat_t.pv_blocked_pre) + qed + hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons + by (unfold Exit, simp add:cntP_def cntV_def count_def) + moreover have "th' \ threads ((e # t) @ s)" using Cons neq_thread + by (unfold Exit, simp) ultimately show ?thesis by auto qed - with Cons and Exit - have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - by (auto simp:cntP_def cntV_def count_def) - moreover from Cons and Exit and neq_th' - have in_thread': "th' \ threads ((e # t) @ s)" - by auto - ultimately show ?thesis by auto next case (Set thread prio') with Cons show ?thesis by (auto simp:cntP_def cntV_def count_def) qed - next - case Nil - with assms - show ?case by auto - qed +next + case Nil + with assms + show ?case by auto qed -(* -lemma runing_precond: - fixes th' - assumes th'_in: "th' \ threads s" - and eq_pv: "cntP s th' = cntV s th'" - and neq_th': "th' \ th" - shows "th' \ runing (t@s)" -proof - - from runing_precond_pre[OF th'_in eq_pv neq_th'] - have h1: "th' \ threads (t @ s)" and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto - from pv_blocked[OF h1 neq_th' h2] - show ?thesis . -qed -*) - -lemmas runing_precond_pre_dtc = runing_precond_pre[folded detached_eq[OF vt_t] detached_eq[OF vt_s]] +text {* Changing counting balance to detachedness *} +lemmas runing_precond_pre_dtc = runing_precond_pre + [folded vat_t.detached_eq vat_s.detached_eq] lemma runing_precond: fixes th' @@ -655,18 +606,11 @@ and neq_th': "th' \ th" and is_runing: "th' \ runing (t@s)" shows "cntP s th' > cntV s th'" + using assms proof - have "cntP s th' \ cntV s th'" - proof - assume eq_pv: "cntP s th' = cntV s th'" - from runing_precond_pre[OF th'_in eq_pv neq_th'] - have h1: "th' \ threads (t @ s)" - and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto - from pv_blocked_pre[OF h1 neq_th' h2] have " th' \ runing (t @ s)" . - with is_runing show "False" by simp - qed - moreover from cnp_cnv_cncs[OF vt_s, of th'] - have "cntV s th' \ cntP s th'" by auto + by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in) + moreover have "cntV s th' \ cntP s th'" using vat_s.cnp_cnv_cncs by auto ultimately show ?thesis by auto qed @@ -676,95 +620,44 @@ and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \ th' \ threads ((moment (i+j) t)@s)" -proof(induct j) - case (Suc k) - show ?case - proof - - { assume True: "Suc (i+k) \ length t" - from moment_head [OF this] - obtain e where - eq_me: "moment (Suc(i+k)) t = e#(moment (i+k) t)" - by blast - from red_moment[of "Suc(i+k)"] - and eq_me have "extend_highest_gen s th prio tm (e # moment (i + k) t)" by simp - hence vt_e: "vt (e#(moment (i + k) t)@s)" - by (unfold extend_highest_gen_def extend_highest_gen_axioms_def - highest_gen_def, auto) - have not_runing': "th' \ runing (moment (i + k) t @ s)" - proof - - show "th' \ runing (moment (i + k) t @ s)" - proof(rule extend_highest_gen.pv_blocked) - from Suc show "th' \ threads (moment (i + k) t @ s)" - by simp - next - from neq_th' show "th' \ th" . - next - from red_moment show "extend_highest_gen s th prio tm (moment (i + k) t)" . - next - from Suc vt_e show "detached (moment (i + k) t @ s) th'" - apply(subst detached_eq) - apply(auto intro: vt_e evt_cons) - done - qed - qed - from step_back_step[OF vt_e] - have "step ((moment (i + k) t)@s) e" . - hence "cntP (e#(moment (i + k) t)@s) th' = cntV (e#(moment (i + k) t)@s) th' \ - th' \ threads (e#(moment (i + k) t)@s)" - proof(cases) - case (thread_create thread prio) - with Suc show ?thesis by (auto simp:cntP_def cntV_def count_def) - next - case (thread_exit thread) - moreover have "thread \ th'" - proof - - have "thread \ runing (moment (i + k) t @ s)" by fact - moreover note not_runing' - ultimately show ?thesis by auto - qed - moreover note Suc - ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def) - next - case (thread_P thread cs) - moreover have "thread \ th'" - proof - - have "thread \ runing (moment (i + k) t @ s)" by fact - moreover note not_runing' - ultimately show ?thesis by auto - qed - moreover note Suc - ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def) - next - case (thread_V thread cs) - moreover have "thread \ th'" - proof - - have "thread \ runing (moment (i + k) t @ s)" by fact - moreover note not_runing' - ultimately show ?thesis by auto - qed - moreover note Suc - ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def) - next - case (thread_set thread prio') - with Suc show ?thesis - by (auto simp:cntP_def cntV_def count_def) - qed - with eq_me have ?thesis using eq_me by auto - } note h = this - show ?thesis - proof(cases "Suc (i+k) \ length t") - case True - from h [OF this] show ?thesis . - next - case False - with moment_ge - have eq_m: "moment (i + Suc k) t = moment (i+k) t" by auto - with Suc show ?thesis by auto - qed +proof - + interpret h_i: red_extend_highest_gen _ _ _ _ _ i + by (unfold_locales) + interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j" + by (unfold_locales) + interpret h: extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)" + proof(unfold_locales) + show "vt (moment i t @ s)" by (metis h_i.vt_t) + next + show "th \ threads (moment i t @ s)" by (metis h_i.th_kept) + next + show "preced th (moment i t @ s) = + Max (cp (moment i t @ s) ` threads (moment i t @ s))" + by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept) + next + show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th) + next + show "vt (moment j (restm i t) @ moment i t @ s)" + using moment_plus_split by (metis add.commute append_assoc h_j.vt_t) + next + fix th' prio' + assume "Create th' prio' \ set (moment j (restm i t))" + thus "prio' \ prio" using assms + by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append) + next + fix th' prio' + assume "Set th' prio' \ set (moment j (restm i t))" + thus "th' \ th \ prio' \ prio" + by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append) + next + fix th' + assume "Exit th' \ set (moment j (restm i t))" + thus "th' \ th" + by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append) qed -next - case 0 - from assms show ?case by auto + show ?thesis + by (metis add.commute append_assoc eq_pv h.runing_precond_pre + moment_plus_split neq_th' th'_in) qed lemma moment_blocked_eqpv: @@ -778,14 +671,19 @@ proof - from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" - and h2: "th' \ threads ((moment j t)@s)" by auto - with extend_highest_gen.pv_blocked - show ?thesis - using red_moment [of j] h2 neq_th' h1 - apply(auto) - by (metis extend_highest_gen.pv_blocked_pre) + and h2: "th' \ threads ((moment j t)@s)" by auto + moreover have "th' \ runing ((moment j t)@s)" + proof - + interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) + show ?thesis + using h.pv_blocked_pre h1 h2 neq_th' by auto + qed + ultimately show ?thesis by auto qed +(* The foregoing two lemmas are preparation for this one, but + in long run can be combined. Maybe I am wrong. +*) lemma moment_blocked: assumes neq_th': "th' \ th" and th'_in: "th' \ threads ((moment i t)@s)" @@ -795,71 +693,119 @@ th' \ threads ((moment j t)@s) \ th' \ runing ((moment j t)@s)" proof - - from vt_moment[OF vt_t, of "i+length s"] moment_prefix[of i t s] - have vt_i: "vt (moment i t @ s)" by auto - from vt_moment[OF vt_t, of "j+length s"] moment_prefix[of j t s] - have vt_j: "vt (moment j t @ s)" by auto - from moment_blocked_eqpv [OF neq_th' th'_in detached_elim [OF vt_i dtc] le_ij, - folded detached_eq[OF vt_j]] - show ?thesis . + interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) + interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) + have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'" + by (metis dtc h_i.detached_elim) + from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij] + show ?thesis by (metis h_j.detached_intro) qed -lemma runing_inversion_1: +lemma runing_preced_inversion: + assumes runing': "th' \ runing (t@s)" + shows "cp (t@s) th' = preced th s" (is "?L = ?R") +proof - + have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms + by (unfold runing_def, auto) + also have "\ = ?R" + by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) + finally show ?thesis . +qed + +text {* + The situation when @{term "th"} is blocked is analyzed by the following lemmas. +*} + +text {* + The following lemmas shows the running thread @{text "th'"}, if it is different from + @{term th}, must be live at the very beginning. By the term {\em the very beginning}, + we mean the moment where the formal investigation starts, i.e. the moment (or state) + @{term s}. +*} + +lemma runing_inversion_0: assumes neq_th': "th' \ th" and runing': "th' \ runing (t@s)" - shows "th' \ threads s \ cntV s th' < cntP s th'" -proof(cases "th' \ threads s") - case True - with runing_precond [OF this neq_th' runing'] show ?thesis by simp -next - case False - let ?Q = "\ t. th' \ threads (t@s)" - let ?q = "moment 0 t" - from moment_eq and False have not_thread: "\ ?Q ?q" by simp - from runing' have "th' \ threads (t@s)" by (simp add:runing_def readys_def) - from p_split_gen [of ?Q, OF this not_thread] - obtain i where lt_its: "i < length t" - and le_i: "0 \ i" - and pre: " th' \ threads (moment i t @ s)" (is "th' \ threads ?pre") - and post: "(\i'>i. th' \ threads (moment i' t @ s))" by auto - from lt_its have "Suc i \ length t" by auto - from moment_head[OF this] obtain e where - eq_me: "moment (Suc i) t = e # moment i t" by blast - from red_moment[of "Suc i"] and eq_me - have "extend_highest_gen s th prio tm (e # moment i t)" by simp - hence vt_e: "vt (e#(moment i t)@s)" - by (unfold extend_highest_gen_def extend_highest_gen_axioms_def - highest_gen_def, auto) - from step_back_step[OF this] have stp_i: "step (moment i t @ s) e" . - from post[rule_format, of "Suc i"] and eq_me - have not_in': "th' \ threads (e # moment i t@s)" by auto - from create_pre[OF stp_i pre this] - obtain prio where eq_e: "e = Create th' prio" . - have "cntP (moment i t@s) th' = cntV (moment i t@s) th'" - proof(rule cnp_cnv_eq) - from step_back_vt [OF vt_e] - show "vt (moment i t @ s)" . - next - from eq_e and stp_i - have "step (moment i t @ s) (Create th' prio)" by simp - thus "th' \ threads (moment i t @ s)" by (cases, simp) - qed - with eq_e - have "cntP ((e#moment i t)@s) th' = cntV ((e#moment i t)@s) th'" - by (simp add:cntP_def cntV_def count_def) - with eq_me[symmetric] - have h1: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" - by simp - from eq_e have "th' \ threads ((e#moment i t)@s)" by simp - with eq_me [symmetric] - have h2: "th' \ threads (moment (Suc i) t @ s)" by simp - from moment_blocked_eqpv [OF neq_th' h2 h1, of "length t"] and lt_its - and moment_ge - have "th' \ runing (t @ s)" by auto - with runing' - show ?thesis by auto + shows "th' \ threads s" +proof - + -- {* The proof is by contradiction: *} + { assume otherwise: "\ ?thesis" + have "th' \ runing (t @ s)" + proof - + -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *} + have th'_in: "th' \ threads (t@s)" using runing' by (simp add:runing_def readys_def) + -- {* However, @{text "th'"} does not exist at very beginning. *} + have th'_notin: "th' \ threads (moment 0 t @ s)" using otherwise + by (metis append.simps(1) moment_zero) + -- {* Therefore, there must be a moment during @{text "t"}, when + @{text "th'"} came into being. *} + -- {* Let us suppose the moment being @{text "i"}: *} + from p_split_gen[OF th'_in th'_notin] + obtain i where lt_its: "i < length t" + and le_i: "0 \ i" + and pre: " th' \ threads (moment i t @ s)" (is "th' \ threads ?pre") + and post: "(\i'>i. th' \ threads (moment i' t @ s))" by (auto) + interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) + interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales) + from lt_its have "Suc i \ length t" by auto + -- {* Let us also suppose the event which makes this change is @{text e}: *} + from moment_head[OF this] obtain e where + eq_me: "moment (Suc i) t = e # moment i t" by blast + hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t) + hence "PIP (moment i t @ s) e" by (cases, simp) + -- {* It can be derived that this event @{text "e"}, which + gives birth to @{term "th'"} must be a @{term "Create"}: *} + from create_pre[OF this, of th'] + obtain prio where eq_e: "e = Create th' prio" + by (metis append_Cons eq_me lessI post pre) + have h1: "th' \ threads (moment (Suc i) t @ s)" using post by auto + have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" + proof - + have "cntP (moment i t@s) th' = cntV (moment i t@s) th'" + by (metis h_i.cnp_cnv_eq pre) + thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def) + qed + show ?thesis + using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge + by auto + qed + with `th' \ runing (t@s)` + have False by simp + } thus ?thesis by auto qed +text {* + The second lemma says, if the running thread @{text th'} is different from + @{term th}, then this @{text th'} must in the possession of some resources + at the very beginning. + + To ease the reasoning of resource possession of one particular thread, + we used two auxiliary functions @{term cntV} and @{term cntP}, + which are the counters of @{term P}-operations and + @{term V}-operations respectively. + If the number of @{term V}-operation is less than the number of + @{term "P"}-operations, the thread must have some unreleased resource. +*} + +lemma runing_inversion_1: (* ddd *) + assumes neq_th': "th' \ th" + and runing': "th' \ runing (t@s)" + -- {* thread @{term "th'"} is a live on in state @{term "s"} and + it has some unreleased resource. *} + shows "th' \ threads s \ cntV s th' < cntP s th'" +proof - + -- {* The proof is a simple composition of @{thm runing_inversion_0} and + @{thm runing_precond}: *} + -- {* By applying @{thm runing_inversion_0} to assumptions, + it can be shown that @{term th'} is live in state @{term s}: *} + have "th' \ threads s" using runing_inversion_0[OF assms(1,2)] . + -- {* Then the thesis is derived easily by applying @{thm runing_precond}: *} + with runing_precond [OF this neq_th' runing'] show ?thesis by simp +qed + +text {* + The following lemma is just a rephrasing of @{thm runing_inversion_1}: +*} lemma runing_inversion_2: assumes runing': "th' \ runing (t@s)" shows "th' = th \ (th' \ th \ th' \ threads s \ cntV s th' < cntP s th')" @@ -868,37 +814,11 @@ show ?thesis by auto qed -lemma runing_preced_inversion: - assumes runing': "th' \ runing (t@s)" - shows "cp (t@s) th' = preced th s" -proof - - from runing' have "cp (t@s) th' = Max (cp (t @ s) ` readys (t @ s))" - by (unfold runing_def, auto) - also have "\ = preced th s" - proof - - from max_cp_readys_threads[OF vt_t] - have "\ = Max (cp (t @ s) ` threads (t @ s))" . - also have "\ = preced th s" - proof - - from max_kept - and max_cp_eq [OF vt_t] - show ?thesis by auto - qed - finally show ?thesis . - qed - finally show ?thesis . -qed - lemma runing_inversion_3: assumes runing': "th' \ runing (t@s)" and neq_th: "th' \ th" shows "th' \ threads s \ (cntV s th' < cntP s th' \ cp (t@s) th' = preced th s)" -proof - - from runing_inversion_2 [OF runing'] - and neq_th - and runing_preced_inversion[OF runing'] - show ?thesis by auto -qed + by (metis neq_th runing' runing_inversion_2 runing_preced_inversion) lemma runing_inversion_4: assumes runing': "th' \ runing (t@s)" @@ -906,83 +826,93 @@ shows "th' \ threads s" and "\detached s th'" and "cp (t@s) th' = preced th s" -using runing_inversion_3 [OF runing'] - and neq_th - and runing_preced_inversion[OF runing'] -apply(auto simp add: detached_eq[OF vt_s]) -done + apply (metis neq_th runing' runing_inversion_2) + apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc) + by (metis neq_th runing' runing_inversion_3) + + +text {* + Suppose @{term th} is not running, it is first shown that + there is a path in RAG leading from node @{term th} to another thread @{text "th'"} + in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). + Now, since @{term readys}-set is non-empty, there must be + one in it which holds the highest @{term cp}-value, which, by definition, + is the @{term runing}-thread. However, we are going to show more: this running thread + is exactly @{term "th'"}. + *} +lemma th_blockedE: (* ddd *) + assumes "th \ runing (t@s)" + obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" + "th' \ runing (t@s)" +proof - + -- {* According to @{thm vat_t.th_chain_to_ready}, either + @{term "th"} is in @{term "readys"} or there is path leading from it to + one thread in @{term "readys"}. *} + have "th \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (RAG (t @ s))\<^sup>+)" + using th_kept vat_t.th_chain_to_ready by auto + -- {* However, @{term th} can not be in @{term readys}, because otherwise, since + @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *} + moreover have "th \ readys (t@s)" + using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto + -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in + term @{term readys}: *} + ultimately obtain th' where th'_in: "th' \ readys (t@s)" + and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto + -- {* We are going to show that this @{term th'} is running. *} + have "th' \ runing (t@s)" + proof - + -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *} + have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R") + proof - + have "?L = Max ((the_preced (t @ s) \ the_thread) ` subtree (tRAG (t @ s)) (Th th'))" + by (unfold cp_alt_def1, simp) + also have "... = (the_preced (t @ s) \ the_thread) (Th th)" + proof(rule image_Max_subset) + show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads) + next + show "subtree (tRAG (t @ s)) (Th th') \ Th ` threads (t @ s)" + by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) + next + show "Th th \ subtree (tRAG (t @ s)) (Th th')" using dp + by (unfold tRAG_subtree_eq, auto simp:subtree_def) + next + show "Max ((the_preced (t @ s) \ the_thread) ` Th ` threads (t @ s)) = + (the_preced (t @ s) \ the_thread) (Th th)" (is "Max ?L = _") + proof - + have "?L = the_preced (t @ s) ` threads (t @ s)" + by (unfold image_comp, rule image_cong, auto) + thus ?thesis using max_preced the_preced_def by auto + qed + qed + also have "... = ?R" + using th_cp_max th_cp_preced th_kept + the_preced_def vat_t.max_cp_readys_threads by auto + finally show ?thesis . + qed + -- {* Now, since @{term th'} holds the highest @{term cp} + and we have already show it is in @{term readys}, + it is @{term runing} by definition. *} + with `th' \ readys (t@s)` show ?thesis by (simp add: runing_def) + qed + -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} + moreover have "Th th' \ ancestors (RAG (t @ s)) (Th th)" + using `(Th th, Th th') \ (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) + ultimately show ?thesis using that by metis +qed + +text {* + Now it is easy to see there is always a thread to run by case analysis + on whether thread @{term th} is running: if the answer is Yes, the + the running thread is obviously @{term th} itself; otherwise, the running + thread is the @{text th'} given by lemma @{thm th_blockedE}. +*} lemma live: "runing (t@s) \ {}" -proof(cases "th \ runing (t@s)") +proof(cases "th \ runing (t@s)") case True thus ?thesis by auto next case False - then have not_ready: "th \ readys (t@s)" - apply (unfold runing_def, - insert th_cp_max max_cp_readys_threads[OF vt_t, symmetric]) - by auto - from th_kept have "th \ threads (t@s)" by auto - from th_chain_to_ready[OF vt_t this] and not_ready - obtain th' where th'_in: "th' \ readys (t@s)" - and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto - have "th' \ runing (t@s)" - proof - - have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" - proof - - have " Max ((\th. preced th (t @ s)) ` ({th'} \ dependants (wq (t @ s)) th')) = - preced th (t@s)" - proof(rule Max_eqI) - fix y - assume "y \ (\th. preced th (t @ s)) ` ({th'} \ dependants (wq (t @ s)) th')" - then obtain th1 where - h1: "th1 = th' \ th1 \ dependants (wq (t @ s)) th'" - and eq_y: "y = preced th1 (t@s)" by auto - show "y \ preced th (t @ s)" - proof - - from max_preced - have "preced th (t @ s) = Max ((\th'. preced th' (t @ s)) ` threads (t @ s))" . - moreover have "y \ \" - proof(rule Max_ge) - from h1 - have "th1 \ threads (t@s)" - proof - assume "th1 = th'" - with th'_in show ?thesis by (simp add:readys_def) - next - assume "th1 \ dependants (wq (t @ s)) th'" - with dependants_threads [OF vt_t] - show "th1 \ threads (t @ s)" by auto - qed - with eq_y show " y \ (\th'. preced th' (t @ s)) ` threads (t @ s)" by simp - next - from finite_threads[OF vt_t] - show "finite ((\th'. preced th' (t @ s)) ` threads (t @ s))" by simp - qed - ultimately show ?thesis by auto - qed - next - from finite_threads[OF vt_t] dependants_threads [OF vt_t, of th'] - show "finite ((\th. preced th (t @ s)) ` ({th'} \ dependants (wq (t @ s)) th'))" - by (auto intro:finite_subset) - next - from dp - have "th \ dependants (wq (t @ s)) th'" - by (unfold cs_dependants_def, auto simp:eq_RAG) - thus "preced th (t @ s) \ - (\th. preced th (t @ s)) ` ({th'} \ dependants (wq (t @ s)) th')" - by auto - qed - moreover have "\ = Max (cp (t @ s) ` readys (t @ s))" - proof - - from max_preced and max_cp_eq[OF vt_t, symmetric] - have "preced th (t @ s) = Max (cp (t @ s) ` threads (t @ s))" by simp - with max_cp_readys_threads[OF vt_t] show ?thesis by simp - qed - ultimately show ?thesis by (unfold cp_eq_cpreced cpreced_def, simp) - qed - with th'_in show ?thesis by (auto simp:runing_def) - qed - thus ?thesis by auto + thus ?thesis using th_blockedE by auto qed end