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 \<Rightarrow> thread set" - where - "threads [] = {}" -| "threads (Create th prio#s) = {th} \<union> threads s" -| "threads (Exit th # s) = (threads s) - {th}" -| "threads (_#s) = threads s" - -fun priority :: "thread \<Rightarrow> state \<Rightarrow> 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 \<Rightarrow> state \<Rightarrow> 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 \<Rightarrow> state \<Rightarrow> precedence" - where "preced th s \<equiv> Prc (priority th s) (last_set th s)" - -abbreviation - "preceds s ths \<equiv> {preced th s | th. th \<in> ths}" - -definition - "holds wq th cs \<equiv> th \<in> set (wq cs) \<and> th = hd (wq cs)" - -definition - "waits wq th cs \<equiv> th \<in> set (wq cs) \<and> th \<noteq> hd (wq cs)" - ---{* Nodes in Resource Graph *} -datatype node = - Th "thread" -| Cs "cs" - -definition - "RAG wq \<equiv> {(Th th, Cs cs) | th cs. waits wq th cs} \<union> {(Cs cs, Th th) | cs th. holds wq th cs}" - -definition - "dependants wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}" - -record schedule_state = - wq_fun :: "cs \<Rightarrow> thread list" - cprec_fun :: "thread \<Rightarrow> precedence" - -definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence" - where - "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})" - -abbreviation - "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)" - -abbreviation - "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0" - -abbreviation - "release qs \<equiv> case qs of - [] => [] - | (_ # qs) => SOME q. distinct q \<and> set q = set qs" - -lemma [simp]: - "(SOME q. distinct q \<and> q = []) = []" -by auto - -lemma [simp]: - "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> 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 \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)" - - -fun schs :: "state \<Rightarrow> schedule_state" - where - "schs [] = (| wq_fun = \<lambda> cs. [], cprec_fun = (\<lambda>_. 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 \<Rightarrow> cs \<Rightarrow> thread list" - where "wq s = wq_fun (schs s)" - -definition cpreced2 :: "state \<Rightarrow> thread \<Rightarrow> precedence" - where "cpreced2 s \<equiv> cprec_fun (schs s)" - -abbreviation - "cpreceds2 s ths \<equiv> {cpreced2 s th | th. th \<in> ths}" - -definition - "holds2 s \<equiv> holds (wq_fun (schs s))" - -definition - "waits2 s \<equiv> waits (wq_fun (schs s))" - -definition - "RAG2 s \<equiv> RAG (wq_fun (schs s))" - -definition - "dependants2 s \<equiv> dependants (wq_fun (schs s))" - -(* ready -> is a thread that is not waiting for any resource *) -definition readys :: "state \<Rightarrow> thread set" - where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waits2 s th cs)}" - -definition runing :: "state \<Rightarrow> thread set" - where "runing s \<equiv> {th . th \<in> readys s \<and> cpreced2 s th = Max (cpreceds2 s (readys s))}" - -(* all resources a thread hols in a state *) -definition holding :: "state \<Rightarrow> thread \<Rightarrow> cs set" - where "holding s th \<equiv> {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 \<noteq> [] \<Longrightarrow> next_to_run wts \<in> 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) \<in> RAG2 s}" -unfolding holding_def RAG2_def RAG_def -unfolding holds2_def holds_def waits_def -by auto - -inductive step :: "state \<Rightarrow> event \<Rightarrow> bool" - where - step_Create: "\<lbrakk>th \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create th prio)" -| step_Exit: "\<lbrakk>th \<in> runing s; holding s th = {}\<rbrakk> \<Longrightarrow> step s (Exit th)" -| step_P: "\<lbrakk>th \<in> runing s; (Cs cs, Th th) \<notin> (RAG2 s)^+\<rbrakk> \<Longrightarrow> step s (P th cs)" -| step_V: "\<lbrakk>th \<in> runing s; holds2 s th cs\<rbrakk> \<Longrightarrow> step s (V th cs)" -| step_Set: "\<lbrakk>th \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set th prio)" - -(* valid states *) -inductive vt :: "state \<Rightarrow> bool" - where - vt_nil[intro]: "vt []" -| vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)" - -lemma runing_ready: - shows "runing s \<subseteq> readys s" - unfolding runing_def readys_def - by auto - -lemma readys_threads: - shows "readys s \<subseteq> threads s" - unfolding readys_def - by auto - -lemma wq_threads: - assumes vt: "vt s" - and h: "th \<in> set (wq s cs)" - shows "th \<in> 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) \<in> Domain (RAG2 s)" - shows "th \<in> threads s" -proof - - from in_dom obtain n where "(Th th, n) \<in> RAG2 s" by auto - then obtain cs where "n = Cs cs" "(Th th, Cs cs) \<in> RAG2 s" - unfolding RAG2_def RAG_def by auto - then have "th \<in> 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 \<subseteq> threads s" -proof - fix th1 - assume "th1 \<in> dependants2 s th" - then have h: "(Th th1, Th th) \<in> (RAG2 s)\<^sup>+" - unfolding dependants2_def dependants_def RAG2_def by simp - then have "Th th1 \<in> Domain ((RAG2 s)\<^sup>+)" unfolding Domain_def by auto - then have "Th th1 \<in> Domain (RAG2 s)" using trancl_domain by simp - then show "th1 \<in> 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 (\<lambda>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) \<subseteq> RAG2 s \<union> {(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) \<notin> (RAG2 s)\<^sup>+" "wq s cs \<noteq> []" - shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(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) \<subseteq> 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 \<and> wts \<noteq> []" -shows "RAG2 (V th cs # s) \<subseteq> - RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \<union> {(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) \<notin> (RAG2 s)\<^sup>+" by fact - { assume wq_empty: "wq s cs = []" -- "case waiting queue is empty" - then have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>+" - proof (rule_tac notI) - assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+" - then obtain x where "(x, Cs cs) \<in> 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 \<union> {(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 \<noteq> []" -- "case waiting queue is not empty" - from ac ds - have "acyclic (RAG2 s \<union> {(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 \<in> 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) \<subseteq> 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 \<equiv> "next_to_run wts" - assume wq_not_empty: "wts \<noteq> []" - 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) \<in> RAG2 s" - unfolding RAG2_def RAG_def waits2_def by auto - have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(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)} \<union> {(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) \<notin> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+" - proof (rule notI) - assume "(Th nth, Cs cs) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+" - then obtain z where a: "(Th nth, z) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})" - by (metis converse_tranclE) - then have "(Th nth, z) \<in> 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)} \<union> {(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 "\<exists>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 \<in> set (wq sa cs) \<and> 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) \<in> (RAG2 s)^+" - and th1_r: "th1 \<in> readys s" - and th2_d: "(n, Th th2) \<in> (RAG2 s)^+" - and th2_r: "th2 \<in> readys s" - shows "th1 = th2" -proof(rule ccontr) - assume neq: "th1 \<noteq> th2" - with single_valued_confluent2 [OF single_valued_RAG2 [OF vt]] th1_d th2_d - have "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG2 s)\<^sup>+" by auto - moreover - { assume "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+" - then obtain n where dd: "(Th th1, n) \<in> 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 \<notin> 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) \<in> (RAG2 s)\<^sup>+" - then obtain n where dd: "(Th th2, n) \<in> 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 \<notin> 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) \<subseteq> {th} \<union> 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) \<subseteq> 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) \<subseteq> readys s \<union> set (wq s cs)" -apply(auto simp add: readys_def waits2_def waits_def Let_def wq_def) -done - - -fun the_th :: "node \<Rightarrow> thread" - where "the_th (Th th) = th" - -lemma image_Collect2: - "f ` A = {f x | x. x \<in> A}" -apply(auto) -done - -lemma Collect_disj_eq2: - "{f x | x. x = y \<or> x \<in> A} = {f y} \<union> {f x | x. x \<in> A}" -by (auto) - -lemma last_set_lt: - "th \<in> threads s \<Longrightarrow> last_set th s < length s" - apply(induct rule: threads.induct) - apply(auto) - done - -lemma last_set_eq_iff: - assumes "th1 \<in> threads s" "th2 \<in> threads s" - shows "last_set th1 s = last_set th2 s \<longleftrightarrow> 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 \<in> threads s" - and th_in2: "th2 \<in> threads s" - shows "preced th1 s = preced th2 s \<longleftrightarrow> 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) \<in> Domain (RAG2 s)" - shows "th \<in> threads s" -proof - - from in_dom obtain n where a: "(Th th, n) \<in> RAG2 s" by auto - then obtain cs where "n = Cs cs" - unfolding RAG2_def RAG_def - by auto - then have "(Th th, Cs cs) \<in> RAG2 s" using a by simp - hence "th \<in> 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 \<in> readys s" "th2 \<in> readys s" "vt s" - shows "cpreced2 s th1 = cpreced2 s th2 \<longleftrightarrow> th1 = th2" -proof - def S1\<equiv>"({th1} \<union> dependants (wq s) th1)" - def S2\<equiv>"({th2} \<union> 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 \<noteq> {}" "S2 \<noteq> {}" by (simp_all add: S1_def S2_def) - then have "(preceds s S1) \<noteq> {}" "(preceds s S2) \<noteq> {}" by simp_all - ultimately have m: "Max (preceds s S1) \<in> (preceds s S1)" "Max (preceds s S2) \<in> (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 \<in> S1" "th0 \<in> 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 \<in> 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 \<in> 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 \<in> Domain (RAG2 s)") - apply(subgoal_tac "\<exists>cs. (Th th2, Cs cs) \<in> 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 \<in> Domain ((RAG2 s)^+)") - apply (metis trancl_domain) - apply(subgoal_tac "(Th th2, Th th1) \<in> (RAG2 s)^+") - apply (metis Domain_iff) - apply(simp add: dependants_def RAG2_def wq_def) - --"second case" - apply(subgoal_tac "Th th1 \<in> Domain (RAG2 s)") - apply(subgoal_tac "\<exists>cs. (Th th1, Cs cs) \<in> 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 \<in> Domain ((RAG2 s)^+)") - apply (metis trancl_domain) - apply(subgoal_tac "(Th th1, Th th2) \<in> (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) \<le> 1" -proof (rule ccontr) - assume "\<not> card (runing s) \<le> 1" - then have "2 \<le> card (runing s)" by auto - moreover - have "finite (runing s)" - by (metis `\<not> card (runing s) \<le> 1` card_infinite le0) - ultimately obtain th1 th2 where a: - "th1 \<noteq> th2" "th1 \<in> runing s" "th2 \<in> 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 \<in> S1 \<and> th0 \<in> S2" - and eq_f_th0: "preced th0 s = Max ((\<lambda>th. preced th s) ` (S1 \<inter> S2))" - proof - - from fin have h1: "finite ((\<lambda>th. preced th s) ` (S1 \<inter> 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 \<inter> S2 \<noteq> {}" apply (simp add: S1_def S2_def) - apply(auto) - - done - then have h2: "((\<lambda>th. preced th s) ` (S1 \<union> S2)) \<noteq> {}" by simp - ultimately have "Max ((\<lambda>th. preced th s) ` (S1 \<union> S2)) \<in> ((\<lambda>th. preced th s) ` (S1 \<union> 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