--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Test.thy Thu Sep 21 14:15:55 2017 +0100
@@ -0,0 +1,789 @@
+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