diff -r c3a42076b164 -r b32b3bd99150 Test.thy --- a/Test.thy Thu Sep 07 16:04:03 2017 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,789 +0,0 @@ -theory Test -imports Precedence_ord Graphs -begin - -type_synonym thread = nat -- {* Type for thread identifiers. *} -type_synonym priority = nat -- {* Type for priorities. *} -type_synonym cs = nat -- {* Type for critical sections (or resources). *} - --- {* Schedulling Events *} - -datatype event = - Create thread priority -| Exit thread -| P thread cs -| V thread cs -| Set thread priority - -type_synonym state = "event list" - -fun threads :: "state \ thread set" - where - "threads [] = {}" -| "threads (Create th prio#s) = {th} \ threads s" -| "threads (Exit th # s) = (threads s) - {th}" -| "threads (_#s) = threads s" - -fun priority :: "thread \ state \ priority" - where - "priority th [] = 0" -| "priority th (Create th' prio#s) = (if th' = th then prio else priority th s)" -| "priority th (Set th' prio#s) = (if th' = th then prio else priority th s)" -| "priority th (_#s) = priority th s" - -fun last_set :: "thread \ state \ nat" - where - "last_set th [] = 0" -| "last_set th ((Create th' prio)#s) = (if (th = th') then length s else last_set th s)" -| "last_set th ((Set th' prio)#s) = (if (th = th') then length s else last_set th s)" -| "last_set th (_#s) = last_set th s" - - -definition preced :: "thread \ state \ precedence" - where "preced th s \ Prc (priority th s) (last_set th s)" - -abbreviation - "preceds s ths \ {preced th s | th. th \ ths}" - -definition - "holds wq th cs \ th \ set (wq cs) \ th = hd (wq cs)" - -definition - "waits wq th cs \ th \ set (wq cs) \ th \ hd (wq cs)" - ---{* Nodes in Resource Graph *} -datatype node = - Th "thread" -| Cs "cs" - -definition - "RAG wq \ {(Th th, Cs cs) | th cs. waits wq th cs} \ {(Cs cs, Th th) | cs th. holds wq th cs}" - -definition - "dependants wq th \ {th' . (Th th', Th th) \ (RAG wq)^+}" - -record schedule_state = - wq_fun :: "cs \ thread list" - cprec_fun :: "thread \ precedence" - -definition cpreced :: "(cs \ thread list) \ state \ thread \ precedence" - where - "cpreced wq s th \ Max ({preced th s} \ {preced th' s | th'. th' \ dependants wq th})" - -abbreviation - "all_unlocked \ \_::cs. ([]::thread list)" - -abbreviation - "initial_cprec \ \_::thread. Prc 0 0" - -abbreviation - "release qs \ case qs of - [] => [] - | (_ # 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(rule iffI) -apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)+ -done - -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) |)" -| "schs (Create th prio # s) = - (let wq = wq_fun (schs s) in - (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))" -| "schs (Exit th # s) = - (let wq = wq_fun (schs s) in - (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))" -| "schs (Set th prio # s) = - (let wq = wq_fun (schs s) in - (|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))" -| "schs (P th cs # s) = - (let wq = wq_fun (schs s) in - let new_wq = wq(cs := (wq cs @ [th])) in - (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))" -| "schs (V th cs # s) = - (let wq = wq_fun (schs s) in - let new_wq = wq(cs := release (wq cs)) in - (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))" - -definition wq :: "state \ cs \ thread list" - where "wq s = wq_fun (schs s)" - -definition cpreced2 :: "state \ thread \ precedence" - where "cpreced2 s \ cprec_fun (schs s)" - -abbreviation - "cpreceds2 s ths \ {cpreced2 s th | th. th \ ths}" - -definition - "holds2 s \ holds (wq_fun (schs s))" - -definition - "waits2 s \ waits (wq_fun (schs s))" - -definition - "RAG2 s \ RAG (wq_fun (schs s))" - -definition - "dependants2 s \ dependants (wq_fun (schs s))" - -(* ready -> is a thread that is not waiting for any resource *) -definition readys :: "state \ thread set" - where "readys s \ {th . th \ threads s \ (\ cs. \ waits2 s th cs)}" - -definition runing :: "state \ thread set" - where "runing s \ {th . th \ readys s \ cpreced2 s th = Max (cpreceds2 s (readys s))}" - -(* all resources a thread hols in a state *) -definition holding :: "state \ thread \ cs set" - where "holding s th \ {cs . holds2 s th cs}" - - -lemma exists_distinct: - obtains ys where "distinct ys" "set ys = set xs" -by (metis List.finite_set finite_distinct_list) - -lemma next_to_run_set [simp]: - "wts \ [] \ next_to_run wts \ set wts" -apply(rule exists_distinct[of wts]) -by (metis (mono_tags, lifting) hd_in_set set_empty some_eq_ex) - -lemma holding_RAG: - "holding s th = {cs . (Cs cs, Th th) \ RAG2 s}" -unfolding holding_def RAG2_def RAG_def -unfolding holds2_def holds_def waits_def -by auto - -inductive step :: "state \ event \ bool" - where - step_Create: "\th \ threads s\ \ step s (Create th prio)" -| step_Exit: "\th \ runing s; holding s th = {}\ \ step s (Exit th)" -| step_P: "\th \ runing s; (Cs cs, Th th) \ (RAG2 s)^+\ \ step s (P th cs)" -| step_V: "\th \ runing s; holds2 s th cs\ \ step s (V th cs)" -| step_Set: "\th \ runing s\ \ step s (Set th prio)" - -(* valid states *) -inductive vt :: "state \ bool" - where - vt_nil[intro]: "vt []" -| vt_cons[intro]: "\vt s; step s e\ \ vt (e#s)" - -lemma runing_ready: - shows "runing s \ readys s" - unfolding runing_def readys_def - by auto - -lemma readys_threads: - shows "readys s \ threads s" - 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(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) -apply(rule someI2) -apply(auto) -done - -lemma wq_distinct: - assumes "vt s" - shows "distinct (wq s cs)" -using assms -apply(induct) -apply(simp add: wq_def) -apply(simp add: wq_distinct_step) -done - - -section {* Single_Valuedness of @{const waits2}, @{const holds2}, @{const RAG2} *} - -lemma waits2_unique: - assumes "vt s" - and "waits2 s th cs1" - and "waits2 s th cs2" - shows "cs1 = cs2" -using assms -apply(induct) -apply(simp add: waits2_def waits_def) -apply(erule step.cases) -apply(auto simp add: Let_def waits2_def waits_def holds_def RAG2_def RAG_def - readys_def runing_def split: if_splits) -apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list) -apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list) -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 (simp add: Product_Type.Collect_case_prodD 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 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 -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" - and stp: "step s e" - and ac: "acyclic (RAG2 s)" - shows "acyclic (RAG2 (e # s))" -using stp vt ac -proof (induct) - case (step_P th s cs) - have ac: "acyclic (RAG2 s)" by fact - have ds: "(Cs cs, Th th) \ (RAG2 s)\<^sup>+" by fact - { assume wq_empty: "wq s cs = []" -- "case waiting queue is empty" - then have "(Th th, Cs cs) \ (RAG2 s)\<^sup>+" - proof (rule_tac notI) - assume "(Th th, Cs cs) \ (RAG2 s)\<^sup>+" - then obtain x where "(x, Cs cs) \ RAG2 s" using tranclD2 by metis - 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] - 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] - by (rule acyclic_subset) - } - ultimately show "acyclic (RAG2 (P th cs # s))" by metis -next - case (step_V th s cs) -- "case for release of a lock" - have vt: "vt s" by fact - have ac: "acyclic (RAG2 s)" by fact - have hd: "holds2 s th cs" by fact - from vt have wq_distinct:"distinct (wq s cs)" by (rule wq_distinct) - from hd have "th \ set (wq s cs)" "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto - then obtain wts where eq_wq: "wq s cs = th # wts" by (cases "wq s cs") (auto) - -- "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) - 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) - } - moreover - -- "at least one thread present to take over" - { def nth \ "next_to_run wts" - assume wq_not_empty: "wts \ []" - 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) - moreover - have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \ {(Cs cs, Th nth)})" - proof - - have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})" using ac by (auto intro: acyclic_subset) - moreover - have "(Th nth, Cs cs) \ (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+" - proof (rule notI) - assume "(Th nth, Cs cs) \ (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+" - 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 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 - qed - ultimately have "acyclic (RAG2 (V th cs # s))" - by (rule_tac acyclic_subset) - } - ultimately show "acyclic (RAG2 (V th cs # s))" by metis -qed (simp_all) - - -lemma finite_RAG: - assumes "vt s" - shows "finite (RAG2 s)" -using assms -apply(induct) -apply(simp add: RAG2_def RAG_def waits_def holds_def) -apply(erule step.cases) -apply(auto) -apply(case_tac "wq sa cs = []") -apply(rule finite_subset) -apply(rule RAG_P1) -apply(simp) -apply(simp) -apply(rule finite_subset) -apply(rule RAG_P2) -apply(simp) -apply(simp) -apply(simp) -apply(subgoal_tac "\wts. wq sa cs = th # wts") -apply(erule exE) -apply(case_tac "wts = []") -apply(rule finite_subset) -apply(rule RAG_V1) -apply(simp) -apply(simp) -apply(rule finite_subset) -apply(rule RAG_V2) -apply(simp) -apply(simp) -apply(simp) -apply(subgoal_tac "th \ set (wq sa cs) \ th = hd (wq sa cs)") -apply(case_tac "wq sa cs") -apply(auto)[2] -apply(auto simp add: holds2_def holds_def wq_def) -done - - - -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" - 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 cpreced2_cpreced: "cpreced2 s th = cpreced (wq s) s th" -unfolding cpreced2_def wq_def -apply(induct s rule: schs.induct) -apply(simp add: Let_def cpreced_def dependants_def RAG_def waits_def holds_def preced_def) -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 cpreced_Exit: - shows "cpreced2 (Exit th # s) th' = cpreced2 s th'" -by (simp add: cpreced2_cpreced cpreced_def preced_def wq_def Let_def) - -lemma readys_Exit: - shows "readys (Exit th # s) = readys s - {th}" -by (auto simp add: readys_def waits2_def Let_def) - -lemma readys_Create: - shows "readys (Create th prio # s) \ {th} \ readys s" -apply (auto simp add: readys_def waits2_def Let_def waits_def) -done - -lemma readys_Set: - shows "readys (Set th prio # s) = readys s" -by (auto simp add: readys_def waits2_def Let_def) - - -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 - - -fun the_th :: "node \ thread" - where "the_th (Th th) = th" - -lemma image_Collect2: - "f ` A = {f x | x. x \ A}" -apply(auto) -done - -lemma Collect_disj_eq2: - "{f x | x. x = y \ x \ A} = {f y} \ {f x | x. x \ A}" -by (auto) - -lemma last_set_lt: - "th \ threads s \ last_set th s < length s" - apply(induct rule: threads.induct) - apply(auto) - done - -lemma last_set_eq_iff: - assumes "th1 \ threads s" "th2 \ threads s" - shows "last_set th1 s = last_set th2 s \ th1 = th2" - using assms - apply(induct s rule: threads.induct) - apply(auto split:if_splits dest:last_set_lt) - done - -lemma preced_eq_iff: - assumes th_in1: "th1 \ threads s" - and th_in2: "th2 \ threads s" - shows "preced th1 s = preced th2 s \ th1 = th2" -using assms -by (auto simp add: preced_def last_set_eq_iff) - -lemma dm_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 a: "(Th th, n) \ RAG2 s" by auto - then obtain cs where "n = Cs cs" - unfolding RAG2_def RAG_def - by auto - then have "(Th th, Cs cs) \ RAG2 s" using a by simp - hence "th \ set (wq s cs)" - unfolding RAG2_def wq_def RAG_def waits_def - by (auto) - then show ?thesis - apply(rule_tac wq_threads) - apply(rule assms) - apply(simp) - done -qed - -lemma cpreced_eq_iff: - assumes "th1 \ readys s" "th2 \ readys s" "vt s" - shows "cpreced2 s th1 = cpreced2 s th2 \ th1 = th2" -proof - def S1\"({th1} \ dependants (wq s) th1)" - def S2\"({th2} \ dependants (wq s) th2)" - have fin: "finite ((the_th o fst) ` ((RAG (wq s))\<^sup>+))" - apply(rule) - apply(simp add: finite_trancl) - apply(simp add: wq_def) - apply(rule finite_RAG[simplified RAG2_def]) - apply(rule assms) - done - - from fin have h: "finite (preceds s S1)" "finite (preceds s S2)" - apply(simp_all add: S2_def S1_def Collect_disj_eq2 image_Collect[symmetric]) - apply(rule) - apply(simp add: dependants_def) - apply(rule rev_finite_subset) - apply(assumption) - apply(auto simp add: image_def)[1] - apply(metis fst_conv the_th.simps) - apply(rule) - apply(simp add: dependants_def) - apply(rule rev_finite_subset) - apply(assumption) - apply(auto simp add: image_def)[1] - apply(metis fst_conv the_th.simps) - done - moreover have "S1 \ {}" "S2 \ {}" by (simp_all add: S1_def S2_def) - then have "(preceds s S1) \ {}" "(preceds s S2) \ {}" by simp_all - ultimately have m: "Max (preceds s S1) \ (preceds s S1)" "Max (preceds s S2) \ (preceds s S2)" - apply(rule_tac [!] Max_in) - apply(simp_all) - done - - assume q: "cpreced2 s th1 = cpreced2 s th2" - then have eq_max: "Max (preceds s S1) = Max (preceds s S2)" - unfolding cpreced2_cpreced cpreced_def - apply(simp only: S1_def S2_def) - apply(simp add: Collect_disj_eq2) - done - - obtain th0 where th0_in: "th0 \ S1" "th0 \ S2" and - eq_f_th1: "preced th0 s = Max (preceds s S1)" - "preced th0 s = Max (preceds s S2)" - using m - apply(clarify) - apply(simp add: eq_max) - apply(subst (asm) (2) preced_eq_iff) - apply(insert assms(2))[1] - apply(simp add: S2_def) - apply(auto)[1] - apply (metis contra_subsetD readys_threads) - apply(simp add: dependants_def) - apply(subgoal_tac "Th tha \ Domain ((RAG2 s)^+)") - apply(simp add: trancl_domain) - apply (metis Domain_RAG_threads assms(3)) - apply(simp only: RAG2_def wq_def) - apply (metis Domain_iff) - apply(insert assms(1))[1] - apply(simp add: S1_def) - apply(auto)[1] - apply (metis contra_subsetD readys_threads) - apply(simp add: dependants_def) - apply(subgoal_tac "Th th \ Domain ((RAG2 s)^+)") - apply(simp add: trancl_domain) - apply (metis Domain_RAG_threads assms(3)) - apply(simp only: RAG2_def wq_def) - apply (metis Domain_iff) - apply(simp) - done - then show "th1 = th2" - apply - - apply(insert th0_in assms(1, 2))[1] - apply(simp add: S1_def S2_def) - apply(auto) - --"first case" - prefer 2 - apply(subgoal_tac "Th th2 \ Domain (RAG2 s)") - apply(subgoal_tac "\cs. (Th th2, Cs cs) \ RAG2 s") - apply(erule exE) - apply(simp add: runing_def RAG2_def RAG_def readys_def waits2_def)[1] - apply(auto simp add: RAG2_def RAG_def)[1] - apply(subgoal_tac "Th th2 \ Domain ((RAG2 s)^+)") - apply (metis trancl_domain) - apply(subgoal_tac "(Th th2, Th th1) \ (RAG2 s)^+") - apply (metis Domain_iff) - apply(simp add: dependants_def RAG2_def wq_def) - --"second case" - apply(subgoal_tac "Th th1 \ Domain (RAG2 s)") - apply(subgoal_tac "\cs. (Th th1, Cs cs) \ RAG2 s") - apply(erule exE) - apply(insert assms(1))[1] - apply(simp add: runing_def RAG2_def RAG_def readys_def waits2_def)[1] - apply(auto simp add: RAG2_def RAG_def)[1] - apply(subgoal_tac "Th th1 \ Domain ((RAG2 s)^+)") - apply (metis trancl_domain) - apply(subgoal_tac "(Th th1, Th th2) \ (RAG2 s)^+") - apply (metis Domain_iff) - apply(simp add: dependants_def RAG2_def wq_def) - --"third case" - apply(rule dchain_unique) - apply(rule assms(3)) - apply(simp add: dependants_def RAG2_def wq_def) - apply(simp) - apply(simp add: dependants_def RAG2_def wq_def) - apply(simp) - done -next - assume "th1 = th2" - then show "cpreced2 s th1 = cpreced2 s th2" by simp -qed - -lemma at_most_one_running: - 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)" - by (metis `\ card (runing s) \ 1` card_infinite le0) - ultimately obtain th1 th2 where a: - "th1 \ th2" "th1 \ runing s" "th2 \ runing s" - "cpreced2 s th1 = cpreced2 s th2" - apply(auto simp add: numerals card_le_Suc_iff runing_def) - apply(blast) - done - then have "th1 = th2" - apply(subst (asm) cpreced_eq_iff) - apply(auto intro: assms a) - apply (metis contra_subsetD runing_ready)+ - done - then show "False" using a(1) by auto -qed - - - - (* - obtain th0 where th0_in: "th0 \ S1 \ th0 \ S2" - and eq_f_th0: "preced th0 s = Max ((\th. preced th s) ` (S1 \ S2))" - proof - - from fin have h1: "finite ((\th. preced th s) ` (S1 \ S2))" - apply(simp only: S1_def S2_def) - apply(rule) - apply(rule) - apply(rule) - apply(simp add: dependants_def) - apply(rule rev_finite_subset) - apply(assumption) - apply(auto simp add: image_def) - apply (metis fst_conv the_th.simps) - done - moreover - have "S1 \ S2 \ {}" apply (simp add: S1_def S2_def) - apply(auto) - - done - then have h2: "((\th. preced th s) ` (S1 \ S2)) \ {}" by simp - ultimately have "Max ((\th. preced th s) ` (S1 \ S2)) \ ((\th. preced th s) ` (S1 \ S2))" - apply(rule Max_in) - done - then show ?thesis using that[intro] apply(auto) - - apply(erule_tac preced_unique) - done - qed - *) - -thm waits_def waits2_def - -end