# HG changeset patch # User zhangx # Date 1454506902 -28800 # Node ID d5e9653fbf19c43e1b1bdcc671e7135707e2f658 # Parent 3a801bbd26871ed5512b7debad45a0eea9bc8eec PIPBasics.thy reorganized into sections. The structure is now stable. Next step is to put in more comments. diff -r 3a801bbd2687 -r d5e9653fbf19 PIPBasics.thy --- a/PIPBasics.thy Wed Feb 03 21:05:15 2016 +0800 +++ b/PIPBasics.thy Wed Feb 03 21:41:42 2016 +0800 @@ -361,6 +361,23 @@ "inj_on (the_preced s) (threads s)" by (metis inj_onI preced_unique the_preced_def) +lemma holding_next_thI: + assumes "holding s th cs" + and "length (wq s cs) > 1" + obtains th' where "next_th s th cs th'" +proof - + from assms(1)[folded holding_eq, unfolded cs_holding_def] + have " th \ set (wq s cs) \ th = hd (wq s cs)" + by (unfold s_holding_def, fold wq_def, auto) + then obtain rest where h1: "wq s cs = th#rest" + by (cases "wq s cs", auto) + with assms(2) have h2: "rest \ []" by auto + let ?th' = "hd (SOME q. distinct q \ set q = set rest)" + have "next_th s th cs ?th'" using h1(1) h2 + by (unfold next_th_def, auto) + from that[OF this] show ?thesis . +qed + (* ccc *) section {* Locales used to investigate the execution of PIP *} @@ -2648,6 +2665,30 @@ } ultimately show ?thesis by auto qed +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 dependants_alt_def: "dependants s th = {th'. (Th th', Th th) \ (tRAG s)^+}" by (metis eq_RAG s_dependants_def tRAG_trancl_eq) @@ -2918,6 +2959,75 @@ ultimately show ?thesis by auto qed +lemma threads_alt_def: + "(threads s) = (\ th \ readys s. {th'. Th th' \ subtree (RAG s) (Th th)})" + (is "?L = ?R") +proof - + { fix th1 + assume "th1 \ ?L" + from th_chain_to_ready[OF this] + have "th1 \ readys s \ (\th'. th' \ readys s \ (Th th1, Th th') \ (RAG s)\<^sup>+)" . + hence "th1 \ ?R" by (auto simp:subtree_def) + } moreover + { fix th' + assume "th' \ ?R" + then obtain th where h: "th \ readys s" " Th th' \ subtree (RAG s) (Th th)" + by auto + from this(2) + have "th' \ ?L" + proof(cases rule:subtreeE) + case 1 + with h(1) show ?thesis by (auto simp:readys_def) + next + case 2 + from tranclD[OF this(2)[unfolded ancestors_def, simplified]] + have "Th th' \ Domain (RAG s)" by auto + from dm_RAG_threads[OF this] + show ?thesis . + qed + } ultimately show ?thesis by auto +qed + + +text {* (* ccc *) \noindent + Since the current precedence of the threads in ready queue will always be boosted, + there must be one inside it has the maximum precedence of the whole system. +*} +lemma max_cp_readys_threads: + shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R") +proof(cases "readys s = {}") + case False + have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp) + also have "... = + Max (the_preced s ` (\th\readys s. {th'. Th th' \ subtree (RAG s) (Th th)}))" + by (unfold threads_alt_def, simp) + also have "... = + Max ((\th\readys s. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)}))" + by (unfold image_UN, simp) + also have "... = + Max (Max ` (\th. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)}) ` readys s)" + proof(rule Max_UNION) + show "\M\(\x. the_preced s ` + {th'. Th th' \ subtree (RAG s) (Th x)}) ` readys s. finite M" + using finite_subtree_threads by auto + qed (auto simp:False subtree_def) + also have "... = + Max ((Max \ (\th. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)})) ` readys s)" + by (unfold image_comp, simp) + also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)") + proof - + have "(?f ` ?A) = (?g ` ?A)" + proof(rule f_image_eq) + fix th1 + assume "th1 \ ?A" + thus "?f th1 = ?g th1" + by (unfold cp_alt_def, simp) + qed + thus ?thesis by simp + qed + finally show ?thesis by simp +qed (auto simp:threads_alt_def) + end section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *} @@ -4341,7 +4451,7 @@ end -section {* hhh *} +section {* Recursive definition of @{term "cp"} *} lemma cp_alt_def1: "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))" @@ -4447,104 +4557,9 @@ thus ?thesis by (subst (1) h(1), unfold h(2), simp) qed qed - -section {* Relating @{term cp}-values of @{term threads} and @{term readys }*} - -lemma threads_alt_def: - "(threads s) = (\ th \ readys s. {th'. Th th' \ subtree (RAG s) (Th th)})" - (is "?L = ?R") -proof - - { fix th1 - assume "th1 \ ?L" - from th_chain_to_ready[OF this] - have "th1 \ readys s \ (\th'. th' \ readys s \ (Th th1, Th th') \ (RAG s)\<^sup>+)" . - hence "th1 \ ?R" by (auto simp:subtree_def) - } moreover - { fix th' - assume "th' \ ?R" - then obtain th where h: "th \ readys s" " Th th' \ subtree (RAG s) (Th th)" - by auto - from this(2) - have "th' \ ?L" - proof(cases rule:subtreeE) - case 1 - with h(1) show ?thesis by (auto simp:readys_def) - next - case 2 - from tranclD[OF this(2)[unfolded ancestors_def, simplified]] - have "Th th' \ Domain (RAG s)" by auto - from dm_RAG_threads[OF this] - show ?thesis . - qed - } ultimately show ?thesis by auto -qed - - -text {* (* ccc *) \noindent - Since the current precedence of the threads in ready queue will always be boosted, - there must be one inside it has the maximum precedence of the whole system. -*} -lemma max_cp_readys_threads: - shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R") -proof(cases "readys s = {}") - case False - have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp) - also have "... = - Max (the_preced s ` (\th\readys s. {th'. Th th' \ subtree (RAG s) (Th th)}))" - by (unfold threads_alt_def, simp) - also have "... = - Max ((\th\readys s. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)}))" - by (unfold image_UN, simp) - also have "... = - Max (Max ` (\th. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)}) ` readys s)" - proof(rule Max_UNION) - show "\M\(\x. the_preced s ` - {th'. Th th' \ subtree (RAG s) (Th x)}) ` readys s. finite M" - using finite_subtree_threads by auto - qed (auto simp:False subtree_def) - also have "... = - Max ((Max \ (\th. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)})) ` readys s)" - by (unfold image_comp, simp) - also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)") - proof - - have "(?f ` ?A) = (?g ` ?A)" - proof(rule f_image_eq) - fix th1 - assume "th1 \ ?A" - thus "?f th1 = ?g th1" - by (unfold cp_alt_def, simp) - qed - thus ?thesis by simp - qed - finally show ?thesis by simp -qed (auto simp:threads_alt_def) - end -section {* Pending properties *} - -lemma next_th_unique: - assumes nt1: "next_th s th cs th1" - and nt2: "next_th s th cs th2" - shows "th1 = th2" -using assms by (unfold next_th_def, auto) - -lemma holding_next_thI: - assumes "holding s th cs" - and "length (wq s cs) > 1" - obtains th' where "next_th s th cs th'" -proof - - from assms(1)[folded holding_eq, unfolded cs_holding_def] - have " th \ set (wq s cs) \ th = hd (wq s cs)" - by (unfold s_holding_def, fold wq_def, auto) - then obtain rest where h1: "wq s cs = th#rest" - by (cases "wq s cs", auto) - with assms(2) have h2: "rest \ []" by auto - let ?th' = "hd (SOME q. distinct q \ set q = set rest)" - have "next_th s th cs ?th'" using h1(1) h2 - by (unfold next_th_def, auto) - from that[OF this] show ?thesis . -qed +section {* Other properties useful in Implementation.thy or Correctness.thy *} context valid_trace_e begin @@ -4554,63 +4569,11 @@ shows "actor e \ runing s" using pip_e assms by (induct, auto) - end context valid_trace begin -lemma create_pre: - assumes stp: "step s e" - and not_in: "th \ threads s" - and is_in: "th \ threads (e#s)" - obtains prio where "e = Create th prio" -proof - - from assms - show ?thesis - proof(cases) - case (thread_create thread prio) - with is_in not_in have "e = Create th prio" by simp - from that[OF this] show ?thesis . - next - case (thread_exit thread) - with assms show ?thesis by (auto intro!:that) - next - case (thread_P thread) - with assms show ?thesis by (auto intro!:that) - next - case (thread_V thread) - with assms show ?thesis by (auto intro!:that) - next - case (thread_set thread) - with assms show ?thesis by (auto intro!:that) - qed -qed - -lemma 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)"