diff -r 83ba2d8c859a -r d37703e0c5c4 CpsG.thy~ --- a/CpsG.thy~ Thu Jan 14 00:55:54 2016 +0800 +++ b/CpsG.thy~ Sat Jan 16 10:59:03 2016 +0800 @@ -2,6 +2,19 @@ imports PIPDefs begin +lemma Max_f_mono: + assumes seq: "A \ B" + and np: "A \ {}" + and fnt: "finite B" + shows "Max (f ` A) \ Max (f ` B)" +proof(rule Max_mono) + from seq show "f ` A \ f ` B" by auto +next + from np show "f ` A \ {}" by auto +next + from fnt and seq show "finite (f ` B)" by auto +qed + (* I am going to use this file as a start point to retrofiting PIPBasics.thy, which is originally called CpsG.ghy *) @@ -9,6 +22,14 @@ fixes s assumes vt : "vt s" +lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs" + by (unfold s_waiting_def cs_waiting_def wq_def, auto) + +lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs" + by (unfold s_holding_def wq_def cs_holding_def, simp) + +thm s_waiting_def cs_waiting_def wq_def + locale valid_trace_e = valid_trace + fixes e assumes vt_e: "vt (e#s)" @@ -224,78 +245,6 @@ end -text {* - The following lemmas is also obvious and shallow. It says - that only running thread can request for a critical resource - and that the requested resource must be one which is - not current held by the thread. -*} - -lemma p_pre: "\vt ((P thread cs)#s)\ \ - thread \ runing s \ (Cs cs, Th thread) \ (RAG s)^+" -apply (ind_cases "vt ((P thread cs)#s)") -apply (ind_cases "step s (P thread cs)") -by auto - -lemma abs1: - assumes ein: "e \ set es" - and neq: "hd es \ hd (es @ [x])" - shows "False" -proof - - from ein have "es \ []" by auto - then obtain e ess where "es = e # ess" by (cases es, auto) - with neq show ?thesis by auto -qed - -lemma q_head: "Q (hd es) \ hd es = hd [th\es . Q th]" - by (cases es, auto) - -inductive_cases evt_cons: "vt (a#s)" - -context valid_trace_e -begin - -lemma abs2: - assumes inq: "thread \ set (wq s cs)" - and nh: "thread = hd (wq s cs)" - and qt: "thread \ hd (wq (e#s) cs)" - and inq': "thread \ set (wq (e#s) cs)" - shows "False" -proof - - from vt_e assms show "False" - apply (cases e) - apply ((simp split:if_splits add:Let_def wq_def)[1])+ - apply (insert abs1, fast)[1] - apply (auto simp:wq_def simp:Let_def split:if_splits list.splits) - proof - - fix th qs - assume vt: "vt (V th cs # s)" - and th_in: "thread \ set (SOME q. distinct q \ set q = set qs)" - and eq_wq: "wq_fun (schs s) cs = thread # qs" - show "False" - proof - - from wq_distinct[of cs] - and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp - moreover have "thread \ set qs" - proof - - have "set (SOME q. distinct q \ set q = set qs) = set qs" - proof(rule someI2) - from wq_distinct [of cs] - and eq_wq [folded wq_def] - show "distinct qs \ set qs = set qs" by auto - next - fix x assume "distinct x \ set x = set qs" - thus "set x = set qs" by auto - qed - with th_in show ?thesis by auto - qed - ultimately show ?thesis by auto - qed - qed -qed - -end - context valid_trace begin @@ -369,7 +318,7 @@ make any request and get blocked the second time: Contradiction. *} -lemma waiting_unique_pre: (* ccc *) +lemma waiting_unique_pre: (* ddd *) assumes h11: "thread \ set (wq s cs1)" and h12: "thread \ hd (wq s cs1)" assumes h21: "thread \ set (wq s cs2)" @@ -402,55 +351,76 @@ show False by (simp add: wq_def) qed } note q_not_runing = this - { fix i1 i2 - let ?i3 = "Suc i2" - assume lt12: "i1 < i2" - and "i1 < length s" "i2 < length s" - hence le_i3: "?i3 \ length s" by auto - from moment_plus [OF this] - obtain e where eq_m: "moment ?i3 s = e#moment i2 s" by auto - have "i2 < ?i3" by simp + { fix t1 t2 cs1 cs2 + assume lt1: "t1 < length s" + and np1: "\ ?Q cs1 (moment t1 s)" + and nn1: "(\i'>t1. ?Q cs1 (moment i' s))" + and lt2: "t2 < length s" + and np2: "\ ?Q cs2 (moment t2 s)" + and nn2: "(\i'>t2. ?Q cs2 (moment i' s))" + and lt12: "t1 < t2" + let ?t3 = "Suc t2" + from lt2 have le_t3: "?t3 \ length s" by auto + from moment_plus [OF this] + obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto + have "t2 < ?t3" by simp from nn2 [rule_format, OF this] and eq_m - have h1: "thread \ set (wq (e#moment t2 s) cs2)" and - h2: "thread \ hd (wq (e#moment t2 s) cs2)" by auto - have "vt (e#moment t2 s)" - proof - - from vt_moment - have "vt (moment ?t3 s)" . - with eq_m show ?thesis by simp - qed - then interpret vt_e: valid_trace_e "moment t2 s" "e" + have h1: "thread \ set (wq (e#moment t2 s) cs2)" and + h2: "thread \ hd (wq (e#moment t2 s) cs2)" by auto + have "vt (e#moment t2 s)" + proof - + from vt_moment + have "vt (moment ?t3 s)" . + with eq_m show ?thesis by simp + qed + then interpret vt_e: valid_trace_e "moment t2 s" "e" by (unfold_locales, auto, cases, simp) - have ?thesis + have ?thesis + proof - + have "thread \ runing (moment t2 s)" proof(cases "thread \ set (wq (moment t2 s) cs2)") case True - from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)" - by auto - from vt_e.abs2 [OF True eq_th h2 h1] - show ?thesis by auto + have "e = V thread cs2" + proof - + have eq_th: "thread = hd (wq (moment t2 s) cs2)" + using True and np2 by auto + from vt_e.wq_out_inv[OF True this h2] + show ?thesis . + qed + thus ?thesis using vt_e.actor_inv[OF vt_e.pip_e] by auto next case False - from vt_e.block_pre[OF False h1] - have "e = P thread cs2" . - with vt_e.vt_e have "vt ((P thread cs2)# moment t2 s)" by simp - from p_pre [OF this] have "thread \ runing (moment t2 s)" by simp - with runing_ready have "thread \ readys (moment t2 s)" by auto - with nn1 [rule_format, OF lt12] - show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto) + have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] . + with vt_e.actor_inv[OF vt_e.pip_e] + show ?thesis by auto qed - } + moreover have "thread \ runing (moment t2 s)" + by (rule q_not_runing[OF nn1[rule_format, OF lt12]]) + ultimately show ?thesis by simp + qed + } note lt_case = this show ?thesis proof - - { - assume lt12: "t1 < t2" + { assume "t1 < t2" + from lt_case[OF lt1 np1 nn1 lt2 np2 nn2 this] + have ?thesis . + } moreover { + assume "t2 < t1" + from lt_case[OF lt2 np2 nn2 lt1 np1 nn1 this] + have ?thesis . + } moreover { + assume eq_12: "t1 = t2" let ?t3 = "Suc t2" from lt2 have le_t3: "?t3 \ length s" by auto from moment_plus [OF this] obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto - have "t2 < ?t3" by simp + have lt_2: "t2 < ?t3" by simp from nn2 [rule_format, OF this] and eq_m have h1: "thread \ set (wq (e#moment t2 s) cs2)" and h2: "thread \ hd (wq (e#moment t2 s) cs2)" by auto + from nn1[rule_format, OF lt_2[folded eq_12]] eq_m[folded eq_12] + have g1: "thread \ set (wq (e#moment t1 s) cs1)" and + g2: "thread \ hd (wq (e#moment t1 s) cs1)" by auto have "vt (e#moment t2 s)" proof - from vt_moment @@ -458,119 +428,38 @@ with eq_m show ?thesis by simp qed then interpret vt_e: valid_trace_e "moment t2 s" "e" - by (unfold_locales, auto, cases, simp) - have ?thesis + by (unfold_locales, auto, cases, simp) + have "e = V thread cs2 \ e = P thread cs2" proof(cases "thread \ set (wq (moment t2 s) cs2)") case True - from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)" - by auto - from vt_e.abs2 [OF True eq_th h2 h1] - show ?thesis by auto - next - case False - from vt_e.block_pre[OF False h1] - have "e = P thread cs2" . - with vt_e.vt_e have "vt ((P thread cs2)# moment t2 s)" by simp - from p_pre [OF this] have "thread \ runing (moment t2 s)" by simp - with runing_ready have "thread \ readys (moment t2 s)" by auto - with nn1 [rule_format, OF lt12] - show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto) - qed - } moreover { - assume lt12: "t2 < t1" - let ?t3 = "Suc t1" - from lt1 have le_t3: "?t3 \ length s" by auto - from moment_plus [OF this] - obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto - have lt_t3: "t1 < ?t3" by simp - from nn1 [rule_format, OF this] and eq_m - have h1: "thread \ set (wq (e#moment t1 s) cs1)" and - h2: "thread \ hd (wq (e#moment t1 s) cs1)" by auto - have "vt (e#moment t1 s)" - proof - - from vt_moment - have "vt (moment ?t3 s)" . - with eq_m show ?thesis by simp - qed - then interpret vt_e: valid_trace_e "moment t1 s" e - by (unfold_locales, auto, cases, auto) - have ?thesis - proof(cases "thread \ set (wq (moment t1 s) cs1)") - case True - from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)" - by auto - from vt_e.abs2 True eq_th h2 h1 - show ?thesis by auto + have "e = V thread cs2" + proof - + have eq_th: "thread = hd (wq (moment t2 s) cs2)" + using True and np2 by auto + from vt_e.wq_out_inv[OF True this h2] + show ?thesis . + qed + thus ?thesis by auto next case False - from vt_e.block_pre [OF False h1] - have "e = P thread cs1" . - with vt_e.vt_e have "vt ((P thread cs1)# moment t1 s)" by simp - from p_pre [OF this] have "thread \ runing (moment t1 s)" by simp - with runing_ready have "thread \ readys (moment t1 s)" by auto - with nn2 [rule_format, OF lt12] - show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto) + have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] . + thus ?thesis by auto qed - } moreover { - assume eqt12: "t1 = t2" - let ?t3 = "Suc t1" - from lt1 have le_t3: "?t3 \ length s" by auto - from moment_plus [OF this] - obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto - have lt_t3: "t1 < ?t3" by simp - from nn1 [rule_format, OF this] and eq_m - have h1: "thread \ set (wq (e#moment t1 s) cs1)" and - h2: "thread \ hd (wq (e#moment t1 s) cs1)" by auto - have vt_e: "vt (e#moment t1 s)" - proof - - from vt_moment - have "vt (moment ?t3 s)" . - with eq_m show ?thesis by simp - qed - then interpret vt_e: valid_trace_e "moment t1 s" e - by (unfold_locales, auto, cases, auto) - have ?thesis + moreover have "e = V thread cs1 \ e = P thread cs1" proof(cases "thread \ set (wq (moment t1 s) cs1)") case True - from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)" - by auto - from vt_e.abs2 [OF True eq_th h2 h1] - show ?thesis by auto + have eq_th: "thread = hd (wq (moment t1 s) cs1)" + using True and np1 by auto + from vt_e.wq_out_inv[folded eq_12, OF True this g2] + have "e = V thread cs1" . + thus ?thesis by auto next case False - from vt_e.block_pre [OF False h1] - have eq_e1: "e = P thread cs1" . - have lt_t3: "t1 < ?t3" by simp - with eqt12 have "t2 < ?t3" by simp - from nn2 [rule_format, OF this] and eq_m and eqt12 - have h1: "thread \ set (wq (e#moment t2 s) cs2)" and - h2: "thread \ hd (wq (e#moment t2 s) cs2)" by auto - show ?thesis - proof(cases "thread \ set (wq (moment t2 s) cs2)") - case True - from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)" - by auto - from vt_e and eqt12 have "vt (e#moment t2 s)" by simp - then interpret vt_e2: valid_trace_e "moment t2 s" e - by (unfold_locales, auto, cases, auto) - from vt_e2.abs2 [OF True eq_th h2 h1] - show ?thesis . - next - case False - have "vt (e#moment t2 s)" - proof - - from vt_moment eqt12 - have "vt (moment (Suc t2) s)" by auto - with eq_m eqt12 show ?thesis by simp - qed - then interpret vt_e2: valid_trace_e "moment t2 s" e - by (unfold_locales, auto, cases, auto) - from vt_e2.block_pre [OF False h1] - have "e = P thread cs2" . - with eq_e1 neq12 show ?thesis by auto - qed + have "e = P thread cs1" using vt_e.wq_in_inv[folded eq_12, OF False g1] . + thus ?thesis by auto qed - } ultimately show ?thesis by arith + ultimately have ?thesis using neq12 by auto + } ultimately show ?thesis using nat_neq_iff by blast qed qed @@ -582,9 +471,9 @@ assumes "waiting s th cs1" and "waiting s th cs2" shows "cs1 = cs2" -using waiting_unique_pre assms -unfolding wq_def s_waiting_def -by auto + using waiting_unique_pre assms + unfolding wq_def s_waiting_def + by auto end @@ -621,7 +510,7 @@ from last_set_unique [OF this th_in1 th_in2] show ?thesis . qed - + lemma preced_linorder: assumes neq_12: "th1 \ th2" and th_in1: "th1 \ threads s" @@ -633,7 +522,7 @@ thus ?thesis by auto qed -(* An aux lemma used later *) +(* An aux lemma used later *) lemma unique_minus: assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" and xy: "(x, y) \ r" @@ -743,284 +632,758 @@ apply (unfold s_RAG_def s_waiting_def wq_def) by (simp add:Let_def) - -text {* - The following lemmas are used in the proof of - lemma @{text "step_RAG_v"}, which characterizes how the @{text "RAG"} is changed - by @{text "V"}-events. - However, since our model is very concise, such seemingly obvious lemmas need to be derived from scratch, - starting from the model definitions. -*} -lemma step_v_hold_inv[elim_format]: - "\c t. \vt (V th cs # s); - \ holding (wq s) t c; holding (wq (V th cs # s)) t c\ \ - next_th s th cs t \ c = cs" +context valid_trace +begin + +lemma finite_threads: + shows "finite (threads s)" +using vt by (induct) (auto elim: step.cases) + +lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th" +unfolding cp_def wq_def +apply(induct s rule: schs.induct) +thm cpreced_initial +apply(simp add: Let_def cpreced_initial) +apply(simp add: Let_def) +apply(simp add: Let_def) +apply(simp add: Let_def) +apply(subst (2) schs.simps) +apply(simp add: Let_def) +apply(subst (2) schs.simps) +apply(simp add: Let_def) +done + +lemma RAG_target_th: "(Th th, x) \ RAG (s::state) \ \ cs. x = Cs cs" + by (unfold s_RAG_def, auto) + +lemma wq_threads: + assumes h: "th \ set (wq s cs)" + shows "th \ threads s" proof - - fix c t - assume vt: "vt (V th cs # s)" - and nhd: "\ holding (wq s) t c" - and hd: "holding (wq (V th cs # s)) t c" - show "next_th s th cs t \ c = cs" - proof(cases "c = cs") - case False - with nhd hd show ?thesis - by (unfold cs_holding_def wq_def, auto simp:Let_def) + from vt and h show ?thesis + proof(induct arbitrary: th cs) + case (vt_cons s e) + interpret vt_s: valid_trace s + using vt_cons(1) by (unfold_locales, auto) + assume ih: "\th cs. th \ set (wq s cs) \ th \ threads s" + and stp: "step s e" + and vt: "vt s" + and h: "th \ set (wq (e # s) cs)" + show ?case + proof(cases e) + case (Create th' prio) + with ih h show ?thesis + by (auto simp:wq_def Let_def) + next + case (Exit th') + with stp ih h show ?thesis + apply (auto simp:wq_def Let_def) + apply (ind_cases "step s (Exit th')") + apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def + s_RAG_def s_holding_def cs_holding_def) + done + next + case (V th' cs') + show ?thesis + proof(cases "cs' = cs") + case False + with h + show ?thesis + apply(unfold wq_def V, auto simp:Let_def V split:prod.splits, fold wq_def) + by (drule_tac ih, simp) + next + case True + from h + show ?thesis + proof(unfold V wq_def) + assume th_in: "th \ set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \ set ?l") + show "th \ threads (V th' cs' # s)" + proof(cases "cs = cs'") + case False + hence "?l = wq_fun (schs s) cs" by (simp add:Let_def) + with th_in have " th \ set (wq s cs)" + by (fold wq_def, simp) + from ih [OF this] show ?thesis by simp + next + case True + show ?thesis + proof(cases "wq_fun (schs s) cs'") + case Nil + with h V show ?thesis + apply (auto simp:wq_def Let_def split:if_splits) + by (fold wq_def, drule_tac ih, simp) + next + case (Cons a rest) + assume eq_wq: "wq_fun (schs s) cs' = a # rest" + with h V show ?thesis + apply (auto simp:Let_def wq_def split:if_splits) + proof - + assume th_in: "th \ set (SOME q. distinct q \ set q = set rest)" + have "set (SOME q. distinct q \ set q = set rest) = set rest" + proof(rule someI2) + from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def] + show "distinct rest \ set rest = set rest" by auto + next + show "\x. distinct x \ set x = set rest \ set x = set rest" + by auto + qed + with eq_wq th_in have "th \ set (wq_fun (schs s) cs')" by auto + from ih[OF this[folded wq_def]] show "th \ threads s" . + next + assume th_in: "th \ set (wq_fun (schs s) cs)" + from ih[OF this[folded wq_def]] + show "th \ threads s" . + qed + qed + qed + qed + qed + next + case (P th' cs') + from h stp + show ?thesis + apply (unfold P wq_def) + apply (auto simp:Let_def split:if_splits, fold wq_def) + apply (auto intro:ih) + apply(ind_cases "step s (P th' cs')") + by (unfold runing_def readys_def, auto) + next + case (Set thread prio) + with ih h show ?thesis + by (auto simp:wq_def Let_def) + qed next - case True - with step_back_step [OF vt] - have "step s (V th c)" by simp - hence "next_th s th cs t" - proof(cases) - assume "holding s th c" - with nhd hd show ?thesis - apply (unfold s_holding_def cs_holding_def wq_def next_th_def, - auto simp:Let_def split:list.splits if_splits) - proof - - assume " hd (SOME q. distinct q \ q = []) \ set (SOME q. distinct q \ q = [])" - moreover have "\ = set []" - proof(rule someI2) - show "distinct [] \ [] = []" by auto - next - fix x assume "distinct x \ x = []" - thus "set x = set []" by auto - qed - ultimately show False by auto - next - assume " hd (SOME q. distinct q \ q = []) \ set (SOME q. distinct q \ q = [])" - moreover have "\ = set []" - proof(rule someI2) - show "distinct [] \ [] = []" by auto - next - fix x assume "distinct x \ x = []" - thus "set x = set []" by auto - qed - ultimately show False by auto - qed - qed - with True show ?thesis by auto + case vt_nil + thus ?case by (auto simp:wq_def) + qed +qed + +lemma dm_RAG_threads: + assumes in_dom: "(Th th) \ Domain (RAG s)" + shows "th \ threads s" +proof - + from in_dom obtain n where "(Th th, n) \ RAG s" by auto + moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto + ultimately have "(Th th, Cs cs) \ RAG s" by simp + hence "th \ set (wq s cs)" + by (unfold s_RAG_def, auto simp:cs_waiting_def) + from wq_threads [OF this] show ?thesis . +qed + + +lemma cp_le: + assumes th_in: "th \ threads s" + shows "cp s th \ Max ((\ th. (preced th s)) ` threads s)" +proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def) + show "Max ((\th. preced th s) ` ({th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+})) + \ Max ((\th. preced th s) ` threads s)" + (is "Max (?f ` ?A) \ Max (?f ` ?B)") + proof(rule Max_f_mono) + show "{th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} \ {}" by simp + next + from finite_threads + show "finite (threads s)" . + next + from th_in + show "{th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} \ threads s" + apply (auto simp:Domain_def) + apply (rule_tac dm_RAG_threads) + apply (unfold trancl_domain [of "RAG s", symmetric]) + by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def) qed qed -text {* - The following @{text "step_v_wait_inv"} is also an obvious lemma, which, however, needs to be - derived from scratch, which confirms the correctness of the definition of @{text "next_th"}. -*} -lemma step_v_wait_inv[elim_format]: - "\t c. \vt (V th cs # s); \ waiting (wq (V th cs # s)) t c; waiting (wq s) t c - \ - \ (next_th s th cs t \ cs = c)" -proof - - fix t c - assume vt: "vt (V th cs # s)" - and nw: "\ waiting (wq (V th cs # s)) t c" - and wt: "waiting (wq s) t c" - from vt interpret vt_v: valid_trace_e s "V th cs" - by (cases, unfold_locales, simp) - show "next_th s th cs t \ cs = c" - proof(cases "cs = c") +lemma le_cp: + shows "preced th s \ cp s th" +proof(unfold cp_eq_cpreced preced_def cpreced_def, simp) + show "Prc (priority th s) (last_set th s) + \ Max (insert (Prc (priority th s) (last_set th s)) + ((\th. Prc (priority th s) (last_set th s)) ` dependants (wq s) th))" + (is "?l \ Max (insert ?l ?A)") + proof(cases "?A = {}") case False - with nw wt show ?thesis - by (auto simp:cs_waiting_def wq_def Let_def) + have "finite ?A" (is "finite (?f ` ?B)") + proof - + have "finite ?B" + proof- + have "finite {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+}" + proof - + let ?F = "\ (x, y). the_th x" + have "{th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} \ ?F ` ((RAG (wq s))\<^sup>+)" + apply (auto simp:image_def) + by (rule_tac x = "(Th x, Th th)" in bexI, auto) + moreover have "finite \" + proof - + from finite_RAG have "finite (RAG s)" . + hence "finite ((RAG (wq s))\<^sup>+)" + apply (unfold finite_trancl) + by (auto simp: s_RAG_def cs_RAG_def wq_def) + thus ?thesis by auto + qed + ultimately show ?thesis by (auto intro:finite_subset) + qed + thus ?thesis by (simp add:cs_dependants_def) + qed + thus ?thesis by simp + qed + from Max_insert [OF this False, of ?l] show ?thesis by auto next case True - from nw[folded True] wt[folded True] - have "next_th s th cs t" - apply (unfold next_th_def, auto simp:cs_waiting_def wq_def Let_def split:list.splits) - proof - - fix a list - assume t_in: "t \ set list" - and t_ni: "t \ set (SOME q. distinct q \ set q = set list)" - and eq_wq: "wq_fun (schs s) cs = a # list" - have " set (SOME q. distinct q \ set q = set list) = set list" - proof(rule someI2) - from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def] - show "distinct list \ set list = set list" by auto - next - show "\x. distinct x \ set x = set list \ set x = set list" - by auto - qed - with t_ni and t_in show "a = th" by auto + thus ?thesis by auto + qed +qed + +lemma max_cp_eq: + shows "Max ((cp s) ` threads s) = Max ((\ th. (preced th s)) ` threads s)" + (is "?l = ?r") +proof(cases "threads s = {}") + case True + thus ?thesis by auto +next + case False + have "?l \ ((cp s) ` threads s)" + proof(rule Max_in) + from finite_threads + show "finite (cp s ` threads s)" by auto + next + from False show "cp s ` threads s \ {}" by auto + qed + then obtain th + where th_in: "th \ threads s" and eq_l: "?l = cp s th" by auto + have "\ \ ?r" by (rule cp_le[OF th_in]) + moreover have "?r \ cp s th" (is "Max (?f ` ?A) \ cp s th") + proof - + have "?r \ (?f ` ?A)" + proof(rule Max_in) + from finite_threads + show " finite ((\th. preced th s) ` threads s)" by auto next - fix a list - assume t_in: "t \ set list" - and t_ni: "t \ set (SOME q. distinct q \ set q = set list)" - and eq_wq: "wq_fun (schs s) cs = a # list" - have " set (SOME q. distinct q \ set q = set list) = set list" - proof(rule someI2) - from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def] - show "distinct list \ set list = set list" by auto - next - show "\x. distinct x \ set x = set list \ set x = set list" + from False show " (\th. preced th s) ` threads s \ {}" by auto + qed + then obtain th' where + th_in': "th' \ ?A " and eq_r: "?r = ?f th'" by auto + from le_cp [of th'] eq_r + have "?r \ cp s th'" by auto + moreover have "\ \ cp s th" + proof(fold eq_l) + show " cp s th' \ Max (cp s ` threads s)" + proof(rule Max_ge) + from th_in' show "cp s th' \ cp s ` threads s" by auto - qed - with t_ni and t_in show "t = hd (SOME q. distinct q \ set q = set list)" by auto - next - fix a list - assume eq_wq: "wq_fun (schs s) cs = a # list" - from step_back_step[OF vt] - show "a = th" - proof(cases) - assume "holding s th cs" - with eq_wq show ?thesis - by (unfold s_holding_def wq_def, auto) + next + from finite_threads + show "finite (cp s ` threads s)" by auto qed qed - with True show ?thesis by simp + ultimately show ?thesis by auto + qed + ultimately show ?thesis using eq_l by auto +qed + +lemma max_cp_eq_the_preced: + shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" + using max_cp_eq using the_preced_def by presburger + +end + +lemma preced_v [simp]: "preced th' (V th cs#s) = preced th' s" + by (unfold preced_def, simp) + +lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s" +proof + fix th' + show "the_preced (V th cs # s) th' = the_preced s th'" + by (unfold the_preced_def preced_def, simp) +qed + +locale valid_trace_v = valid_trace_e + + fixes th cs + assumes is_v: "e = V th cs" + +context valid_trace_v +begin + +definition "rest = tl (wq s cs)" + +definition "wq' = (SOME q. distinct q \ set q = set rest)" + +lemma distinct_rest: "distinct rest" + by (simp add: distinct_tl rest_def wq_distinct) + +lemma runing_th_s: + shows "th \ runing s" +proof - + from pip_e[unfolded is_v] + show ?thesis by (cases, simp) +qed + +lemma holding_cs_eq_th: + assumes "holding s t cs" + shows "t = th" +proof - + from pip_e[unfolded is_v] + show ?thesis + proof(cases) + case (thread_V) + from held_unique[OF this(2) assms] + show ?thesis by simp + qed +qed + +lemma th_not_waiting: + "\ waiting s th c" +proof - + have "th \ readys s" + using runing_ready runing_th_s by blast + thus ?thesis + by (unfold readys_def, auto) +qed + +lemma waiting_neq_th: + assumes "waiting s t c" + shows "t \ th" + using assms using th_not_waiting by blast + +lemma wq_s_cs: + "wq s cs = th#rest" +proof - + from pip_e[unfolded is_v] + show ?thesis + proof(cases) + case (thread_V) + from this(2) show ?thesis + by (unfold rest_def s_holding_def, fold wq_def, + metis empty_iff list.collapse list.set(1)) + qed +qed + +lemma wq_es_cs: + "wq (e#s) cs = wq'" + using wq_s_cs[unfolded wq_def] + by (auto simp:Let_def wq_def rest_def wq'_def is_v, simp) + +lemma distinct_wq': "distinct wq'" + by (metis (mono_tags, lifting) distinct_rest some_eq_ex wq'_def) + +lemma th'_in_inv: + assumes "th' \ set wq'" + shows "th' \ set rest" + using assms + by (metis (mono_tags, lifting) distinct.simps(2) + rest_def some_eq_ex wq'_def wq_distinct wq_s_cs) + +lemma neq_t_th: + assumes "waiting (e#s) t c" + shows "t \ th" +proof + assume otherwise: "t = th" + show False + proof(cases "c = cs") + case True + have "t \ set wq'" + using assms[unfolded True s_waiting_def, folded wq_def, unfolded wq_es_cs] + by simp + from th'_in_inv[OF this] have "t \ set rest" . + with wq_s_cs[folded otherwise] wq_distinct[of cs] + show ?thesis by simp + next + case False + have "wq (e#s) c = wq s c" using False + by (unfold is_v, simp) + hence "waiting s t c" using assms + by (simp add: cs_waiting_def waiting_eq) + hence "t \ readys s" by (unfold readys_def, auto) + hence "t \ runing s" using runing_ready by auto + with runing_th_s[folded otherwise] show ?thesis by auto qed qed -lemma step_v_not_wait[consumes 3]: - "\vt (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\ \ False" - by (unfold next_th_def cs_waiting_def wq_def, auto simp:Let_def) - -lemma step_v_release: - "\vt (V th cs # s); holding (wq (V th cs # s)) th cs\ \ False" +lemma waiting_esI1: + assumes "waiting s t c" + and "c \ cs" + shows "waiting (e#s) t c" +proof - + have "wq (e#s) c = wq s c" + using assms(2) is_v by auto + with assms(1) show ?thesis + using cs_waiting_def waiting_eq by auto +qed + +lemma holding_esI2: + assumes "c \ cs" + and "holding s t c" + shows "holding (e#s) t c" +proof - + from assms(1) have "wq (e#s) c = wq s c" using is_v by auto + from assms(2)[unfolded s_holding_def, folded wq_def, + folded this, unfolded wq_def, folded s_holding_def] + show ?thesis . +qed + +end + +locale valid_trace_v_n = valid_trace_v + + assumes rest_nnl: "rest \ []" +begin + +lemma neq_wq': "wq' \ []" +proof (unfold wq'_def, rule someI2) + show "distinct rest \ set rest = set rest" + by (simp add: distinct_rest) +next + fix x + assume " distinct x \ set x = set rest" + thus "x \ []" using rest_nnl by auto +qed + +definition "taker = hd wq'" + +definition "rest' = tl wq'" + +lemma eq_wq': "wq' = taker # rest'" + by (simp add: neq_wq' rest'_def taker_def) + +lemma next_th_taker: + shows "next_th s th cs taker" + using rest_nnl taker_def wq'_def wq_s_cs + by (auto simp:next_th_def) + +lemma taker_unique: + assumes "next_th s th cs taker'" + shows "taker' = taker" +proof - + from assms + obtain rest' where + h: "wq s cs = th # rest'" + "taker' = hd (SOME q. distinct q \ set q = set rest')" + by (unfold next_th_def, auto) + with wq_s_cs have "rest' = rest" by auto + thus ?thesis using h(2) taker_def wq'_def by auto +qed + +lemma waiting_set_eq: + "{(Th th', Cs cs) |th'. next_th s th cs th'} = {(Th taker, Cs cs)}" + by (smt all_not_in_conv bot.extremum insertI1 insert_subset + mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique) + +lemma holding_set_eq: + "{(Cs cs, Th th') |th'. next_th s th cs th'} = {(Cs cs, Th taker)}" + using next_th_taker taker_def waiting_set_eq + by fastforce + +lemma holding_taker: + shows "holding (e#s) taker cs" + by (unfold s_holding_def, fold wq_def, unfold wq_es_cs, + auto simp:neq_wq' taker_def) + +lemma waiting_esI2: + assumes "waiting s t cs" + and "t \ taker" + shows "waiting (e#s) t cs" +proof - + have "t \ set wq'" + proof(unfold wq'_def, rule someI2) + show "distinct rest \ set rest = set rest" + by (simp add: distinct_rest) + next + fix x + assume "distinct x \ set x = set rest" + moreover have "t \ set rest" + using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto + ultimately show "t \ set x" by simp + qed + moreover have "t \ hd wq'" + using assms(2) taker_def by auto + ultimately show ?thesis + by (unfold s_waiting_def, fold wq_def, unfold wq_es_cs, simp) +qed + +lemma waiting_esE: + assumes "waiting (e#s) t c" + obtains "c \ cs" "waiting s t c" + | "c = cs" "t \ taker" "waiting s t cs" "t \ set rest'" +proof(cases "c = cs") + case False + hence "wq (e#s) c = wq s c" using is_v by auto + with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto + from that(1)[OF False this] show ?thesis . +next + case True + from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs] + have "t \ hd wq'" "t \ set wq'" by auto + hence "t \ taker" by (simp add: taker_def) + moreover hence "t \ th" using assms neq_t_th by blast + moreover have "t \ set rest" by (simp add: `t \ set wq'` th'_in_inv) + ultimately have "waiting s t cs" + by (metis cs_waiting_def list.distinct(2) list.sel(1) + list.set_sel(2) rest_def waiting_eq wq_s_cs) + show ?thesis using that(2) + using True `t \ set wq'` `t \ taker` `waiting s t cs` eq_wq' by auto +qed + +lemma holding_esI1: + assumes "c = cs" + and "t = taker" + shows "holding (e#s) t c" + by (unfold assms, simp add: holding_taker) + +lemma holding_esE: + assumes "holding (e#s) t c" + obtains "c = cs" "t = taker" + | "c \ cs" "holding s t c" +proof(cases "c = cs") + case True + from assms[unfolded True, unfolded s_holding_def, + folded wq_def, unfolded wq_es_cs] + have "t = taker" by (simp add: taker_def) + from that(1)[OF True this] show ?thesis . +next + case False + hence "wq (e#s) c = wq s c" using is_v by auto + from assms[unfolded s_holding_def, folded wq_def, + unfolded this, unfolded wq_def, folded s_holding_def] + have "holding s t c" . + from that(2)[OF False this] show ?thesis . +qed + +end + +locale valid_trace_v_e = valid_trace_v + + assumes rest_nil: "rest = []" +begin + +lemma nil_wq': "wq' = []" +proof (unfold wq'_def, rule someI2) + show "distinct rest \ set rest = set rest" + by (simp add: distinct_rest) +next + fix x + assume " distinct x \ set x = set rest" + thus "x = []" using rest_nil by auto +qed + +lemma no_taker: + assumes "next_th s th cs taker" + shows "False" proof - - assume vt: "vt (V th cs # s)" - and hd: "holding (wq (V th cs # s)) th cs" - from vt interpret vt_v: valid_trace_e s "V th cs" - by (cases, unfold_locales, simp+) - from step_back_step [OF vt] and hd - show "False" - proof(cases) - assume "holding (wq (V th cs # s)) th cs" and "holding s th cs" + from assms[unfolded next_th_def] + obtain rest' where "wq s cs = th # rest'" "rest' \ []" + by auto + thus ?thesis using rest_def rest_nil by auto +qed + +lemma waiting_set_eq: + "{(Th th', Cs cs) |th'. next_th s th cs th'} = {}" + using no_taker by auto + +lemma holding_set_eq: + "{(Cs cs, Th th') |th'. next_th s th cs th'} = {}" + using no_taker by auto + +lemma no_holding: + assumes "holding (e#s) taker cs" + shows False +proof - + from wq_es_cs[unfolded nil_wq'] + have " wq (e # s) cs = []" . + from assms[unfolded s_holding_def, folded wq_def, unfolded this] + show ?thesis by auto +qed + +lemma no_waiting: + assumes "waiting (e#s) t cs" + shows False +proof - + from wq_es_cs[unfolded nil_wq'] + have " wq (e # s) cs = []" . + from assms[unfolded s_waiting_def, folded wq_def, unfolded this] + show ?thesis by auto +qed + +lemma waiting_esE: + assumes "waiting (e#s) t c" + obtains "c \ cs" "waiting s t c" +proof(cases "c = cs") + case False + hence "wq (e#s) c = wq s c" using is_v by auto + with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto + from that(1)[OF False this] show ?thesis . +next + case True + from no_waiting[OF assms[unfolded True]] + show ?thesis by auto +qed + +lemma holding_esE: + assumes "holding (e#s) t c" + obtains "c \ cs" "holding s t c" +proof(cases "c = cs") + case True + from no_holding[OF assms[unfolded True]] + show ?thesis by auto +next + case False + hence "wq (e#s) c = wq s c" using is_v by auto + from assms[unfolded s_holding_def, folded wq_def, + unfolded this, unfolded wq_def, folded s_holding_def] + have "holding s t c" . + from that[OF False this] show ?thesis . +qed + +end (* ccc *) + +lemma rel_eqI: + assumes "\ x y. (x,y) \ A \ (x,y) \ B" + and "\ x y. (x,y) \ B \ (x, y) \ A" + shows "A = B" + using assms by auto + +lemma in_RAG_E: + assumes "(n1, n2) \ RAG (s::state)" + obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs" + | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs" + using assms[unfolded s_RAG_def, folded waiting_eq holding_eq] + by auto + +context valid_trace_v +begin + +lemma + "RAG (e # s) = + RAG s - {(Cs cs, Th th)} - + {(Th th', Cs cs) |th'. next_th s th cs th'} \ + {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R") +proof(rule rel_eqI) + fix n1 n2 + assume "(n1, n2) \ ?L" + thus "(n1, n2) \ ?R" + proof(cases rule:in_RAG_E) + case (waiting th' cs') + show ?thesis + proof(cases "rest = []") + case False + interpret h_n: valid_trace_v_n s e th cs + by (unfold_locales, insert False, simp) + from waiting(3) + show ?thesis + proof(cases rule:h_n.waiting_esE) + case 1 + with waiting(1,2) + show ?thesis + by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, + fold waiting_eq, auto) + next + case 2 + with waiting(1,2) + show ?thesis + by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, + fold waiting_eq, auto) + qed + next + case True + interpret h_e: valid_trace_v_e s e th cs + by (unfold_locales, insert True, simp) + from waiting(3) + show ?thesis + proof(cases rule:h_e.waiting_esE) + case 1 + with waiting(1,2) + show ?thesis + by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, + fold waiting_eq, auto) + qed + qed + next + case (holding th' cs') + show ?thesis + proof(cases "rest = []") + case False + interpret h_n: valid_trace_v_n s e th cs + by (unfold_locales, insert False, simp) + from holding(3) + show ?thesis + proof(cases rule:h_n.holding_esE) + case 1 + with holding(1,2) + show ?thesis + by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, + fold waiting_eq, auto) + next + case 2 + with holding(1,2) + show ?thesis + by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, + fold holding_eq, auto) + qed + next + case True + interpret h_e: valid_trace_v_e s e th cs + by (unfold_locales, insert True, simp) + from holding(3) + show ?thesis + proof(cases rule:h_e.holding_esE) + case 1 + with holding(1,2) + show ?thesis + by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, + fold holding_eq, auto) + qed + qed + qed +next + fix n1 n2 + assume h: "(n1, n2) \ ?R" + show "(n1, n2) \ ?L" + proof(cases "rest = []") + case False + interpret h_n: valid_trace_v_n s e th cs + by (unfold_locales, insert False, simp) + from h[unfolded h_n.waiting_set_eq h_n.holding_set_eq] + have "((n1, n2) \ RAG s \ (n1 \ Cs cs \ n2 \ Th th) + \ (n1 \ Th h_n.taker \ n2 \ Cs cs)) \ + (n2 = Th h_n.taker \ n1 = Cs cs)" + by auto + thus ?thesis + proof + assume "n2 = Th h_n.taker \ n1 = Cs cs" + with h_n.holding_taker + show ?thesis + by (unfold s_RAG_def, fold holding_eq, auto) + next + assume h: "(n1, n2) \ RAG s \ + (n1 \ Cs cs \ n2 \ Th th) \ (n1 \ Th h_n.taker \ n2 \ Cs cs)" + hence "(n1, n2) \ RAG s" by simp thus ?thesis - apply (unfold s_holding_def wq_def cs_holding_def) - apply (auto simp:Let_def split:list.splits) - proof - - fix list - assume eq_wq[folded wq_def]: - "wq_fun (schs s) cs = hd (SOME q. distinct q \ set q = set list) # list" - and hd_in: "hd (SOME q. distinct q \ set q = set list) - \ set (SOME q. distinct q \ set q = set list)" - have "set (SOME q. distinct q \ set q = set list) = set list" - proof(rule someI2) - from vt_v.wq_distinct[of cs] and eq_wq - show "distinct list \ set list = set list" by auto - next - show "\x. distinct x \ set x = set list \ set x = set list" - by auto - qed - moreover have "distinct (hd (SOME q. distinct q \ set q = set list) # list)" - proof - - from vt_v.wq_distinct[of cs] and eq_wq - show ?thesis by auto - qed - moreover note eq_wq and hd_in - ultimately show "False" by auto + proof(cases rule:in_RAG_E) + case (waiting th' cs') + thus ?thesis qed + qed qed qed -lemma step_v_get_hold: - "\th'. \vt (V th cs # s); \ holding (wq (V th cs # s)) th' cs; next_th s th cs th'\ \ False" - apply (unfold cs_holding_def next_th_def wq_def, - auto simp:Let_def) -proof - - fix rest - assume vt: "vt (V th cs # s)" - and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest" - and nrest: "rest \ []" - and ni: "hd (SOME q. distinct q \ set q = set rest) - \ set (SOME q. distinct q \ set q = set rest)" - from vt interpret vt_v: valid_trace_e s "V th cs" - by (cases, unfold_locales, simp+) - have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from vt_v.wq_distinct[of cs] and eq_wq - show "distinct rest \ set rest = set rest" by auto - next - fix x assume "distinct x \ set x = set rest" - hence "set x = set rest" by auto - with nrest - show "x \ []" by (case_tac x, auto) - qed - with ni show "False" by auto +end + + +lemma step_RAG_v: (* ccc *) +assumes vt: + "vt (V th cs#s)" +shows " + RAG (V th cs # s) = + RAG s - {(Cs cs, Th th)} - + {(Th th', Cs cs) |th'. next_th s th cs th'} \ + {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R") +proof(rule rel_eqI) + fix n1 n2 + assume "(n1, n2) \ ?L" + show "(n1, n2) \ ?R" sorry +next + fix n1 n2 + assume "(n1, n2) \ ?R" + show "(n1, n2) \ ?L" sorry qed -lemma step_v_release_inv[elim_format]: -"\c t. \vt (V th cs # s); \ holding (wq (V th cs # s)) t c; holding (wq s) t c\ \ - c = cs \ t = th" - apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits) - proof - - fix a list - assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list" - from step_back_step [OF vt] show "a = th" - proof(cases) - assume "holding s th cs" with eq_wq - show ?thesis - by (unfold s_holding_def wq_def, auto) - qed - next - fix a list - assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list" - from step_back_step [OF vt] show "a = th" - proof(cases) - assume "holding s th cs" with eq_wq - show ?thesis - by (unfold s_holding_def wq_def, auto) - qed - qed - -lemma step_v_waiting_mono: - "\t c. \vt (V th cs # s); waiting (wq (V th cs # s)) t c\ \ waiting (wq s) t c" -proof - - fix t c - let ?s' = "(V th cs # s)" - assume vt: "vt ?s'" - and wt: "waiting (wq ?s') t c" - from vt interpret vt_v: valid_trace_e s "V th cs" - by (cases, unfold_locales, simp+) - show "waiting (wq s) t c" - proof(cases "c = cs") - case False - assume neq_cs: "c \ cs" - hence "waiting (wq ?s') t c = waiting (wq s) t c" - by (unfold cs_waiting_def wq_def, auto simp:Let_def) - with wt show ?thesis by simp - next - case True - with wt show ?thesis - apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits) - proof - - fix a list - assume not_in: "t \ set list" - and is_in: "t \ set (SOME q. distinct q \ set q = set list)" - and eq_wq: "wq_fun (schs s) cs = a # list" - have "set (SOME q. distinct q \ set q = set list) = set list" - proof(rule someI2) - from vt_v.wq_distinct [of cs] - and eq_wq[folded wq_def] - show "distinct list \ set list = set list" by auto - next - fix x assume "distinct x \ set x = set list" - thus "set x = set list" by auto - qed - with not_in is_in show "t = a" by auto - next - fix list - assume is_waiting: "waiting (wq (V th cs # s)) t cs" - and eq_wq: "wq_fun (schs s) cs = t # list" - hence "t \ set list" - apply (unfold wq_def, auto simp:Let_def cs_waiting_def) - proof - - assume " t \ set (SOME q. distinct q \ set q = set list)" - moreover have "\ = set list" - proof(rule someI2) - from vt_v.wq_distinct [of cs] - and eq_wq[folded wq_def] - show "distinct list \ set list = set list" by auto - next - fix x assume "distinct x \ set x = set list" - thus "set x = set list" by auto - qed - ultimately show "t \ set list" by simp - qed - with eq_wq and vt_v.wq_distinct [of cs, unfolded wq_def] - show False by auto - qed - qed -qed + text {* (* ddd *) The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed @@ -1036,7 +1399,7 @@ {(Cs cs, Th th') |th'. next_th s th cs th'}" apply (insert vt, unfold s_RAG_def) apply (auto split:if_splits list.splits simp:Let_def) - apply (auto elim: step_v_waiting_mono step_v_hold_inv + apply (auto elim: step_v_waiting_mono step_v_hold_inv step_v_release step_v_wait_inv step_v_get_hold step_v_release_inv) apply (erule_tac step_v_not_wait, auto) @@ -1559,11 +1922,7 @@ end -lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs" - by (unfold s_waiting_def cs_waiting_def wq_def, auto) - -lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs" - by (unfold s_holding_def wq_def cs_holding_def, simp) + lemma holding_unique: "\holding (s::state) th1 cs; holding s th2 cs\ \ th1 = th2" by (unfold s_holding_def cs_holding_def, auto) @@ -2388,8 +2747,6 @@ end -lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs" - by (auto simp:s_waiting_def cs_waiting_def wq_def) context valid_trace begin @@ -2579,7 +2936,7 @@ with d have "(Th th1, Cs cs') \ RAG s" by simp with runing_1 have "False" apply (unfold runing_def readys_def s_RAG_def) - by (auto simp:eq_waiting) + by (auto simp:waiting_eq) thus ?thesis by simp qed next @@ -2601,7 +2958,7 @@ with d have "(Th th2, Cs cs') \ RAG s" by simp with runing_2 have "False" apply (unfold runing_def readys_def s_RAG_def) - by (auto simp:eq_waiting) + by (auto simp:waiting_eq) thus ?thesis by simp next assume "th2' \ dependants (wq s) th2" @@ -2664,37 +3021,6 @@ qed qed -lemma length_down_to_in: - assumes le_ij: "i \ j" - and le_js: "j \ length s" - shows "length (down_to j i s) = j - i" -proof - - have "length (down_to j i s) = length (from_to i j (rev s))" - by (unfold down_to_def, auto) - also have "\ = j - i" - proof(rule length_from_to_in[OF le_ij]) - from le_js show "j \ length (rev s)" by simp - qed - finally show ?thesis . -qed - - -lemma moment_head: - assumes le_it: "Suc i \ length t" - obtains e where "moment (Suc i) t = e#moment i t" -proof - - have "i \ Suc i" by simp - from length_down_to_in [OF this le_it] - have "length (down_to (Suc i) i t) = 1" by auto - then obtain e where "down_to (Suc i) i t = [e]" - apply (cases "(down_to (Suc i) i t)") by auto - moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t" - by (rule down_to_conc[symmetric], auto) - ultimately have eq_me: "moment (Suc i) t = e#(moment i t)" - by (auto simp:down_to_moment) - from that [OF this] show ?thesis . -qed - context valid_trace begin @@ -3077,7 +3403,6 @@ definition detached :: "state \ thread \ bool" where "detached s th \ (\(\ cs. holding s th cs)) \ (\(\cs. waiting s th cs))" - lemma detached_test: shows "detached s th = (Th th \ Field (RAG s))" apply(simp add: detached_def Field_def) @@ -3146,7 +3471,7 @@ with dtc have "th \ readys s" by (unfold readys_def detached_def Field_def Domain_def Range_def, - auto simp:eq_waiting s_RAG_def) + auto simp:waiting_eq s_RAG_def) with cncs_z and eq_pv show ?thesis by simp next case False @@ -3888,4 +4213,10 @@ definition cps:: "state \ (thread \ precedence) set" where "cps s = {(th, cp s th) | th . th \ threads s}" +find_theorems release + +lemma "wq (V th cs # s) cs1 = ttt" + apply (unfold wq_def, auto simp:Let_def) + end +