# HG changeset patch # User Christian Urban # Date 1402326088 -3600 # Node ID 66ed924aaa5ccda429aa533612a2f01c69d04440 # Parent 0781a2fc93f13f17ebf53069aa88ae4024d3cd4e added another book that makes the error, some more proofs diff -r 0781a2fc93f1 -r 66ed924aaa5c Graphs.thy --- a/Graphs.thy Tue Jun 03 15:00:12 2014 +0100 +++ b/Graphs.thy Mon Jun 09 16:01:28 2014 +0100 @@ -7,49 +7,55 @@ shows "(x, y) \ r\<^sup>* \ (x, y) \ r\<^sup>+" using assms by (metis rtrancl_eq_or_trancl) +(* NOT NEEDED : FIXME *) lemma trancl_split: "(a, b) \ r^+ \ \ c. (a, c) \ r" by (induct rule:trancl_induct, auto) -lemma unique_minus: - assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" - and xy: "(x, y) \ r" - and xz: "(x, z) \ r^+" - and neq: "y \ z" - shows "(y, z) \ r^+" -by (metis converse_tranclE neq unique xy xz) + +section {* Single_Valuedness *} + +lemma single_valued_Collect: + assumes "single_valuedP r" + and "inj f" + shows "single_valued {(f x, g y) | x y. r x y}" +using assms +unfolding single_valued_def inj_on_def +apply(auto) +done -lemma unique_base: - assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" - and xy: "(x, y) \ r" - and xz: "(x, z) \ r^+" - and neq_yz: "y \ z" - shows "(y, z) \ r^+" -by (metis neq_yz unique unique_minus xy xz) +lemma single_valued_union: + assumes "single_valued r" "single_valued q" + and "Domain r \ Domain q = {}" + shows "single_valued (r \ q)" +using assms +unfolding single_valued_def +by auto -lemma unique_chain_star: - assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" - and xy: "(x, y) \ r^*" - and xz: "(x, z) \ r^*" - shows "(y, z) \ r^* \ (z, y) \ r^*" -thm single_valued_confluent single_valued_def unique xy xz -by (metis single_valued_confluent single_valued_def unique xy xz) +lemma single_valuedP_update: + assumes "single_valuedP r" + shows "single_valuedP (r(x := y))" +using assms +oops -lemma unique_chain: - assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" +lemma single_valued_confluent2: + assumes unique: "single_valued r" and xy: "(x, y) \ r^+" and xz: "(x, z) \ r^+" and neq_yz: "y \ z" shows "(y, z) \ r^+ \ (z, y) \ r^+" proof - - have xy_star: "(x, y) \ r^*" - and xz_star: "(x, z) \ r^*" using xy xz by simp_all - from unique_chain_star[OF unique xy_star xz_star] + have "(x, y) \ r^*" "(x, z) \ r^*" using xy xz by simp_all + with single_valued_confluent[OF unique] have "(y, z) \ r\<^sup>* \ (z, y) \ r\<^sup>*" by auto with neq_yz - show ?thesis by(auto) + show "(y, z) \ r^+ \ (z, y) \ r^+" by simp qed +lemmas unique_chain = single_valued_confluent2 + + + definition funof :: "[('a * 'b)set, 'a] => 'b" where "funof r == (\x. THE y. (x, y) \ r)" @@ -64,8 +70,7 @@ "[|r `` {x} \ A; single_valued r; x \ Domain r|] ==> funof r x \ A" by (force simp add: funof_eq) -lemma single_valuedP_update: - shows "single_valuedP r \ single_valuedP (r(x := y))" -oops + + end \ No newline at end of file diff -r 0781a2fc93f1 -r 66ed924aaa5c Journal/Paper.thy --- a/Journal/Paper.thy Tue Jun 03 15:00:12 2014 +0100 +++ b/Journal/Paper.thy Mon Jun 09 16:01:28 2014 +0100 @@ -152,9 +152,12 @@ \cite[Section 2.3.1]{book} which specifies for a process that inherited a higher priority and exits a critical section ``{\it it resumes the priority it had at the point of entry into the critical section}''. + The same error can also be found in the more recent textbook + \cite[Page 119]{Laplante11} which states ``{\it when [the task] exits the critical + section that caused the block, it reverts to the priority it had when + it entered that section}''. - While \cite{book} and - \cite{Sha90} are the only formal publications we have + While \cite{Laplante11,book,Sha90} are the only formal publications we have found that describe the incorrect behaviour, not all, but many informal\footnote{informal as in ``found on the Web''} descriptions of PIP overlook the possibility that another @@ -1564,7 +1567,7 @@ points out an error in a paper about Preemption Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was invaluable to us in order to be confident about the correctness of our reasoning - (no case can be overlooked). + (for example no corner case can be overlooked). The most closely related work to ours is the formal verification in PVS of the Priority Ceiling Protocol done by Dutertre \cite{dutertre99b}---another solution to the Priority Inversion diff -r 0781a2fc93f1 -r 66ed924aaa5c Journal/document/root.bib --- a/Journal/document/root.bib Tue Jun 03 15:00:12 2014 +0100 +++ b/Journal/document/root.bib Mon Jun 09 16:01:28 2014 +0100 @@ -1,5 +1,13 @@ +@Book{Laplante11, + author = {P.~A.~Laplante and S.~J.~Ovaska}, + title = {Real-Time Systems Design and Analysis: Tools for the Practitioner}, + publisher = {Wiley-IEEE Press}, + year = {2011}, + edition = {4th} +} + @TechReport{Xv6, author = {R.~Cox and F.~Kaashoek and R.~Morris}, title = {{X}v6: {A} {S}imple, {U}nix-like {T}eaching {O}perating {S}ystem}, diff -r 0781a2fc93f1 -r 66ed924aaa5c PrioG.thy --- a/PrioG.thy Tue Jun 03 15:00:12 2014 +0100 +++ b/PrioG.thy Mon Jun 09 16:01:28 2014 +0100 @@ -2269,6 +2269,20 @@ qed +lemma "vt s \ card (runing s) \ 1" +apply(subgoal_tac "finite (runing s)") +prefer 2 +apply (metis finite_nat_set_iff_bounded lessI runing_unique) +apply(case_tac "Suc (Suc 0) \ card (runing s)") +apply(subst (asm) card_le_Suc_iff) +apply(simp) +apply(auto)[1] +apply (metis insertCI runing_unique) +apply(auto) +done + + + lemma create_pre: assumes stp: "step s e" and not_in: "th \ threads s" diff -r 0781a2fc93f1 -r 66ed924aaa5c Test.thy --- a/Test.thy Tue Jun 03 15:00:12 2014 +0100 +++ b/Test.thy Mon Jun 09 16:01:28 2014 +0100 @@ -74,6 +74,20 @@ [] => [] | (_ # qs) => SOME q. distinct q \ set q = set qs" +lemma [simp]: + "(SOME q. distinct q \ q = []) = []" +by auto + +lemma [simp]: + "(x \ set (SOME q. distinct q \ set q = set p)) = (x \ set p)" +apply(auto) +apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) +by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) + +abbreviation + "next_to_run ths \ hd (SOME q::thread list. distinct q \ set q = set ths)" + + fun schs :: "state \ schedule_state" where "schs [] = (| wq_fun = \ cs. [], cprec_fun = (\_. Prc 0 0) |)" @@ -127,8 +141,6 @@ definition holding :: "state \ thread \ cs set" where "holding s th \ {cs . holds2 s th cs}" -abbreviation - "next_to_run ths \ hd (SOME q::thread list. distinct q \ set q = set ths)" lemma exists_distinct: obtains ys where "distinct ys" "set ys = set xs" @@ -169,12 +181,63 @@ unfolding readys_def by auto +lemma wq_threads: + assumes vt: "vt s" + and h: "th \ set (wq s cs)" + shows "th \ threads s" +using assms +apply(induct) +apply(simp add: wq_def) +apply(erule step.cases) +apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def) +apply(simp add: waits_def) +apply(auto simp add: waits_def split: if_splits)[1] +apply(auto split: if_splits) +apply(simp only: waits_def) +by (metis insert_iff set_simps(2)) + + + +lemma Domain_RAG_threads: + assumes vt: "vt s" + and in_dom: "(Th th) \ Domain (RAG2 s)" + shows "th \ threads s" +proof - + from in_dom obtain n where "(Th th, n) \ RAG2 s" by auto + then obtain cs where "n = Cs cs" "(Th th, Cs cs) \ RAG2 s" + unfolding RAG2_def RAG_def by auto + then have "th \ set (wq s cs)" + unfolding wq_def RAG_def RAG2_def waits_def by auto + with wq_threads [OF vt] show ?thesis . +qed + +lemma dependants_threads: + assumes vt: "vt s" + shows "dependants2 s th \ threads s" +proof + fix th1 + assume "th1 \ dependants2 s th" + then have h: "(Th th1, Th th) \ (RAG2 s)\<^sup>+" + unfolding dependants2_def dependants_def RAG2_def by simp + then have "Th th1 \ Domain ((RAG2 s)\<^sup>+)" unfolding Domain_def by auto + then have "Th th1 \ Domain (RAG2 s)" using trancl_domain by simp + then show "th1 \ threads s" using vt by (rule_tac Domain_RAG_threads) +qed + +lemma finite_threads: + assumes vt: "vt s" + shows "finite (threads s)" +using vt by (induct) (auto elim: step.cases) + + +section {* Distinctness of @{const wq} *} + lemma wq_distinct_step: assumes "step s e" "distinct (wq s cs)" shows "distinct (wq (e # s) cs)" using assms unfolding wq_def -apply(induct) +apply(erule_tac step.cases) apply(auto simp add: RAG2_def RAG_def Let_def)[1] apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def) apply(auto split: list.split) @@ -191,72 +254,8 @@ apply(simp add: wq_distinct_step) done -lemma RAG_set_unchanged[simp]: - shows "RAG2 (Set th prio # s) = RAG2 s" -unfolding RAG2_def -by (simp add: Let_def) -lemma RAG_create_unchanged[simp]: - "RAG2 (Create th prio # s) = RAG2 s" -unfolding RAG2_def -by (simp add: Let_def) - -lemma RAG_exit_unchanged[simp]: - shows "RAG2 (Exit th # s) = RAG2 s" -unfolding RAG2_def -by (simp add: Let_def) - -lemma RAG_p1: - assumes "wq s cs = []" - shows "RAG2 (P th cs # s) \ RAG2 s \ {(Cs cs, Th th)}" -using assms -unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def -by (auto simp add: Let_def) - - -lemma RAG_p2: - assumes "(Cs cs, Th th) \ (RAG2 s)\<^sup>+" "wq s cs \ []" - shows "RAG2 (P th cs # s) \ RAG2 s \ {(Th th, Cs cs)}" -using assms -unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def -by (auto simp add: Let_def) - -lemma [simp]: "(SOME q. distinct q \ q = []) = []" -by auto - -lemma [simp]: "(x \ set (SOME q. distinct q \ set q = set p)) = (x \ set p)" -apply auto -apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) -by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) - -lemma RAG_v1: -assumes vt: "wq s cs = [th]" -shows "RAG2 (V th cs # s) \ RAG2 s - {(Cs cs, Th th)}" -using assms -unfolding RAG2_def RAG_def waits_def holds_def wq_def -by (auto simp add: Let_def) - -lemma RAG_v2: -assumes vt:"vt s" "wq s cs = th # wts \ wts \ []" -shows "RAG2 (V th cs # s) \ - RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \ {(Cs cs, Th (next_to_run wts))}" -unfolding RAG2_def RAG_def waits_def holds_def -using assms wq_distinct[OF vt(1), of"cs"] -by (auto simp add: Let_def wq_def) - -(* -lemma single_valued_waits2: - assumes "vt s" - shows "single_valuedP (waits2 s)" -using assms -apply(induct) -apply(simp add: waits2_def waits_def) -apply(erule step.cases) -apply(auto simp add: Let_def waits2_def) -unfolding single_valued_def waits2_def waits_def -apply(auto) -*) - +section {* Single_Valuedness of @{const waits2}, @{const holds2}, @{const RAG2} *} lemma waits2_unique: assumes "vt s" @@ -274,34 +273,85 @@ apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) +lemma single_valued_waits2: + assumes "vt s" + shows "single_valuedP (waits2 s)" +using assms +unfolding single_valued_def +by (metis Collect_splitD fst_eqD sndI waits2_unique) + lemma single_valued_holds2: assumes "vt s" shows "single_valuedP (\cs th. holds2 s th cs)" unfolding single_valued_def holds2_def holds_def by simp - -lemma holds2_unique: - assumes "holds2 s th1 cs" - and "holds2 s th2 cs" - shows "th1 = th2" -using assms -unfolding holds2_def holds_def by auto - -lemma single_valued_waits2: - assumes "vt s" - shows "single_valuedP (waits2 s)" -by (metis (erased, hide_lams) assms mem_Collect_eq old.prod.case single_valued_def waits2_unique) - - -(* was unique_RAG2 *) lemma single_valued_RAG2: assumes "vt s" shows "single_valued (RAG2 s)" using single_valued_waits2[OF assms] single_valued_holds2[OF assms] -unfolding RAG2_def RAG_def -unfolding single_valued_def -unfolding holds2_def waits2_def -by auto +unfolding RAG2_def RAG_def +apply(rule_tac single_valued_union) +unfolding holds2_def[symmetric] waits2_def[symmetric] +apply(rule single_valued_Collect) +apply(simp) +apply(simp add: inj_on_def) +apply(rule single_valued_Collect) +apply(simp) +apply(simp add: inj_on_def) +apply(auto) +done + + +section {* Properties of @{const RAG2} under events *} + +lemma RAG_Set [simp]: + shows "RAG2 (Set th prio # s) = RAG2 s" +unfolding RAG2_def +by (simp add: Let_def) + +lemma RAG_Create [simp]: + "RAG2 (Create th prio # s) = RAG2 s" +unfolding RAG2_def +by (simp add: Let_def) + +lemma RAG_Exit [simp]: + shows "RAG2 (Exit th # s) = RAG2 s" +unfolding RAG2_def +by (simp add: Let_def) + +lemma RAG_P1: + assumes "wq s cs = []" + shows "RAG2 (P th cs # s) \ RAG2 s \ {(Cs cs, Th th)}" +using assms +unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def +by (auto simp add: Let_def) + +lemma RAG_P2: + assumes "(Cs cs, Th th) \ (RAG2 s)\<^sup>+" "wq s cs \ []" + shows "RAG2 (P th cs # s) \ RAG2 s \ {(Th th, Cs cs)}" +using assms +unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def +by (auto simp add: Let_def) + + +lemma RAG_V1: +assumes vt: "wq s cs = [th]" +shows "RAG2 (V th cs # s) \ RAG2 s - {(Cs cs, Th th)}" +using assms +unfolding RAG2_def RAG_def waits_def holds_def wq_def +by (auto simp add: Let_def) + +lemma RAG_V2: +assumes vt:"vt s" "wq s cs = th # wts \ wts \ []" +shows "RAG2 (V th cs # s) \ + RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \ {(Cs cs, Th (next_to_run wts))}" +unfolding RAG2_def RAG_def waits_def holds_def +using assms wq_distinct[OF vt(1), of"cs"] +by (auto simp add: Let_def wq_def) + + + +section {* Acyclicity of @{const RAG2} *} lemma acyclic_RAG_step: assumes vt: "vt s" @@ -321,14 +371,14 @@ with wq_empty show False by (auto simp: RAG2_def RAG_def wq_def waits_def) qed with ac have "acyclic (RAG2 s \ {(Cs cs, Th th)})" by simp - then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF wq_empty] + then have "acyclic (RAG2 (P th cs # s))" using RAG_P1[OF wq_empty] by (rule acyclic_subset) } moreover { assume wq_not_empty: "wq s cs \ []" -- "case waiting queue is not empty" from ac ds have "acyclic (RAG2 s \ {(Th th, Cs cs)})" by simp - then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds wq_not_empty] + then have "acyclic (RAG2 (P th cs # s))" using RAG_P2[OF ds wq_not_empty] by (rule acyclic_subset) } ultimately show "acyclic (RAG2 (P th cs # s))" by metis @@ -343,7 +393,7 @@ -- "case no thread present in the waiting queue to take over" { assume "wts = []" with eq_wq have "wq s cs = [th]" by simp - then have "RAG2 (V th cs # s) \ RAG2 s - {(Cs cs, Th th)}" by (rule RAG_v1) + then have "RAG2 (V th cs # s) \ RAG2 s - {(Cs cs, Th th)}" by (rule RAG_V1) moreover have "acyclic (RAG2 s - {(Cs cs, Th th)})" using ac by (auto intro: acyclic_subset) ultimately have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset) @@ -352,11 +402,13 @@ -- "at least one thread present to take over" { def nth \ "next_to_run wts" assume wq_not_empty: "wts \ []" - have waits2_cs: "waits2 s nth cs" + have "waits2 s nth cs" using eq_wq wq_not_empty wq_distinct unfolding nth_def waits2_def waits_def wq_def[symmetric] by auto + then have cs_in_RAG: "(Th nth, Cs cs) \ RAG2 s" + unfolding RAG2_def RAG_def waits2_def by auto have "RAG2 (V th cs # s) \ RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \ {(Cs cs, Th nth)}" - unfolding nth_def using vt wq_not_empty eq_wq by (rule_tac RAG_v2) (auto) + unfolding nth_def using vt wq_not_empty eq_wq by (rule_tac RAG_V2) (auto) moreover have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \ {(Cs cs, Th nth)})" proof - @@ -368,14 +420,9 @@ then obtain z where a: "(Th nth, z) \ (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})" by (metis converse_tranclE) then have "(Th nth, z) \ RAG2 s" by simp - then obtain cs' where b: "z = Cs cs'" "(Th nth, Cs cs') \ RAG2 s" - unfolding RAG2_def RAG_def by auto - moreover - have "waits2 s nth cs'" - using b(2) unfolding RAG2_def RAG_def waits2_def by simp - ultimately have "cs = cs'" - by (rule_tac waits2_unique[OF vt waits2_cs]) - then show "False" using a b(1) by simp + then have "z = Cs cs" using cs_in_RAG single_valued_RAG2[OF vt] + by (simp add: single_valued_def) + then show "False" using a by simp qed ultimately show "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \ {(Cs cs, Th nth) })" by simp @@ -397,11 +444,11 @@ apply(auto) apply(case_tac "wq sa cs = []") apply(rule finite_subset) -apply(rule RAG_p1) +apply(rule RAG_P1) apply(simp) apply(simp) apply(rule finite_subset) -apply(rule RAG_p2) +apply(rule RAG_P2) apply(simp) apply(simp) apply(simp) @@ -409,11 +456,11 @@ apply(erule exE) apply(case_tac "wts = []") apply(rule finite_subset) -apply(rule RAG_v1) +apply(rule RAG_V1) apply(simp) apply(simp) apply(rule finite_subset) -apply(rule RAG_v2) +apply(rule RAG_V2) apply(simp) apply(simp) apply(simp) @@ -423,20 +470,39 @@ apply(auto simp add: holds2_def holds_def wq_def) done -lemma wq_threads: + + +lemma dchain_unique: assumes vt: "vt s" - and h: "th \ set (wq s cs)" - shows "th \ threads s" -using assms -apply(induct) -apply(simp add: wq_def) -apply(erule step.cases) -apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def) -apply(simp add: waits_def) -apply(auto simp add: waits_def split: if_splits)[1] -apply(auto split: if_splits) -apply(simp only: waits_def) -by (metis insert_iff set_simps(2)) + and th1_d: "(n, Th th1) \ (RAG2 s)^+" + and th1_r: "th1 \ readys s" + and th2_d: "(n, Th th2) \ (RAG2 s)^+" + and th2_r: "th2 \ readys s" + shows "th1 = th2" +proof(rule ccontr) + assume neq: "th1 \ th2" + with single_valued_confluent2 [OF single_valued_RAG2 [OF vt]] th1_d th2_d + have "(Th th1, Th th2) \ (RAG2 s)\<^sup>+ \ (Th th2, Th th1) \ (RAG2 s)\<^sup>+" by auto + moreover + { assume "(Th th1, Th th2) \ (RAG2 s)\<^sup>+" + then obtain n where dd: "(Th th1, n) \ RAG2 s" by (metis converse_tranclE) + then obtain cs where eq_n: "n = Cs cs" + unfolding RAG2_def RAG_def by (case_tac n) (auto) + from dd eq_n have "th1 \ readys s" + unfolding RAG2_def RAG_def waits2_def readys_def by (auto) + with th1_r have "False" by auto + } + moreover + { assume "(Th th2, Th th1) \ (RAG2 s)\<^sup>+" + then obtain n where dd: "(Th th2, n) \ RAG2 s" by (metis converse_tranclE) + then obtain cs where eq_n: "n = Cs cs" + unfolding RAG2_def RAG_def by (case_tac n) (auto) + from dd eq_n have "th2 \ readys s" + unfolding RAG2_def RAG_def waits2_def readys_def by (auto) + with th2_r have "False" by auto + } + ultimately show "False" by metis +qed lemma max_cpreceds_readys_threads: assumes vt: "vt s" @@ -452,46 +518,51 @@ defer oops - +lemma readys_Exit: + shows "readys (Exit th # s) \ readys s" +by (auto simp add: readys_def waits2_def Let_def) +lemma readys_Create: + shows "readys (Create th prio # s) \ {th} \ readys s" +by (auto simp add: readys_def waits2_def Let_def) +lemma readys_Set: + shows "readys (Set th prio # s) \ readys s" +by (auto simp add: readys_def waits2_def Let_def) -lemma dchain_unique: - assumes vt: "vt s" - and th1_d: "(n, Th th1) \ (RAG2 s)^+" - and th1_r: "th1 \ readys s" - and th2_d: "(n, Th th2) \ (RAG2 s)^+" - and th2_r: "th2 \ readys s" - shows "th1 = th2" -proof(rule ccontr) - assume neq: "th1 \ th2" - hence "Th th1 \ Th th2" by simp - from unique_chain [OF _ th1_d th2_d this] and single_valued_RAG2 [OF vt] - have "(Th th1, Th th2) \ (RAG2 s)\<^sup>+ \ (Th th2, Th th1) \ (RAG2 s)\<^sup>+" - unfolding single_valued_def by auto - then show "False" - proof - assume "(Th th1, Th th2) \ (RAG2 s)\<^sup>+" - from trancl_split [OF this] - obtain n where dd: "(Th th1, n) \ RAG2 s" by auto - then obtain cs where eq_n: "n = Cs cs" - unfolding RAG2_def RAG_def by (case_tac n) (auto) - from dd eq_n have "th1 \ readys s" - unfolding RAG2_def RAG_def waits2_def readys_def by (auto) - with th1_r show ?thesis by auto - next - assume "(Th th2, Th th1) \ (RAG2 s)\<^sup>+" - from trancl_split [OF this] - obtain n where dd: "(Th th2, n) \ RAG2 s" by auto - then obtain cs where eq_n: "n = Cs cs" - unfolding RAG2_def RAG_def by (case_tac n) (auto) - from dd eq_n have "th2 \ readys s" - unfolding RAG2_def RAG_def waits2_def readys_def by (auto) - with th2_r show ?thesis by auto - qed -qed +lemma readys_P: + shows "readys (P th cs # s) \ readys s" +apply(auto simp add: readys_def waits2_def Let_def) +apply(simp add: waits_def) +apply(case_tac "csa = cs") +apply(simp) +apply(drule_tac x="cs" in spec) +apply(simp) +apply (metis hd_append2 in_set_insert insert_Nil list.sel(1)) +apply(drule_tac x="csa" in spec) +apply(simp) +done +lemma readys_V: + shows "readys (V th cs # s) \ readys s \ set (wq s cs)" +apply(auto simp add: readys_def waits2_def waits_def Let_def wq_def) +done + +lemma + assumes "vt s" + shows "card (runing s) \ 1" +proof (rule ccontr) + assume "\ card (runing s) \ 1" + then have "2 \ card (runing s)" by auto + moreover + have "finite (runing s)" sorry + ultimately obtain th1 th2 where "th1 \ th2" "th1 \ runing s" "th2 \ runing s" + by (auto simp add: numerals card_le_Suc_iff) (blast) + + show "False" +apply(simp) +oops end \ No newline at end of file diff -r 0781a2fc93f1 -r 66ed924aaa5c journal.pdf Binary file journal.pdf has changed