pip: comparison Test.thy

equal deleted inserted replaced

-:c820ac0f3088
+:c89013dca1aa
 imports Precedence_ord
 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 critical resources). *}
+type_synonym cs = nat -- {* Type for critical sections (or resources). *}
 datatype event =
 Create thread priority
 | Exit thread
 | P thread cs
 (|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 cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
+definition cpreced2 :: "state \<Rightarrow> thread \<Rightarrow> precedence"
-where "cp s \<equiv> cprec_fun (schs s)"
+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
 "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> cp s th = Max ((cp s) ` (readys s))}"
+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}"
 abbreviation
 "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)"
+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
+unfolding holding_def RAG2_def RAG_def
-unfolding holds2_def
+unfolding holds2_def holds_def waits_def
-unfolding RAG2_def RAG_def
-unfolding 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 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(auto simp add: wq_def Let_def)
+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)[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
 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))}"
+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)
 lemma waiting_unique:
 assumes "vt s"
 and "waits2 s th cs1"
 and "waits2 s th cs2"
 shows "cs1 = cs2"
-sorry
+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 rtrancl_eq_trancl [simp]:
+assumes "x \<noteq> y"
+shows "(x, y) \<in> r\<^sup>* \<longleftrightarrow> (x, y) \<in> r\<^sup>+"
+using assms by (metis rtrancl_eq_or_trancl)
 lemma acyclic_RAG_step:
 assumes vt: "vt s"
 and     stp: "step s e"
 and     ac: "acyclic (RAG2 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 a: "wq s cs = []" -- "case waiting queue is empty"
+{ assume wq_empty: "wq s cs = []" -- "case waiting queue is empty"
-have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>*"
+then have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>+"
-proof
+proof (rule_tac notI)
-assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>*"
+assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+"
-then have "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
 then obtain x where "(x, Cs cs) \<in> RAG2 s" using tranclD2 by metis
-with a show False by (auto simp: RAG2_def RAG_def wq_def waits_def)
+with wq_empty show False by (auto simp: RAG2_def RAG_def wq_def waits_def)
 qed
-with acyclic_insert ac
+with ac have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp
-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]
-then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a]
 by (rule acyclic_subset)
 }
 moreover
-{ assume a: "wq s cs \<noteq> []" -- "case waiting queue is not empty"
+{ assume wq_not_empty: "wq s cs \<noteq> []" -- "case waiting queue is not empty"
-from ds have "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>*" by (metis node.distinct(1) rtranclD)
+from ac ds
-with acyclic_insert ac
+have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by simp
-have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by auto
+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 a]
 by (rule acyclic_subset)
 }
 ultimately show "acyclic (RAG2 (P th cs # s))" by metis
 next
-case (step_V th s cs)
+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 rn: "th \<in> runing s" by fact
 have hd: "holds2 s th cs" by fact
-from hd have th_in: "th \<in> set (wq s cs)" and
+from vt have wq_distinct:"distinct (wq s cs)" by (rule wq_distinct)
-eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto
+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
+then obtain wts where eq_wq: "wq s cs = th # wts"  by (cases "wq s cs") (auto)
-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 = []" -- "case no thread present 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 aa: "wts \<noteq> []" -- "at least one thread present to take over"
+assume wq_not_empty: "wts \<noteq> []"
-with vt eq_wq
+have waits2_cs: "waits2 s nth cs"
-have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)} \<union> {(Cs cs, Th nth)}"
+using eq_wq wq_not_empty wq_distinct
-unfolding nth_def by (rule_tac RAG_v2) (auto)
+unfolding nth_def waits2_def waits_def wq_def[symmetric] 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 (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))"
+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)
+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>+"
+have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+"
-proof
+proof (rule notI)
-assume "(Th nth, Cs cs) \<in> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>+"
+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)})"
+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 obtain cs' where b: "z = Cs cs'" "(Th nth, Cs cs') \<in> RAG2 s"
 unfolding RAG2_def RAG_def by auto
-then have "cs = cs'"
+moreover
-apply(rule_tac waiting_unique[OF vt])
+have "waits2 s nth cs'"
-using eq_wq aa
+using b(2) unfolding RAG2_def RAG_def waits2_def by simp
-apply(auto simp add: nth_def RAG2_def RAG_def waits2_def waits_def wq_def)
+ultimately have "cs = cs'"
-apply (metis (mono_tags, lifting) `\<And>thesis. (\<And>wts. wq s cs = th # wts \<Longrightarrow> thesis) \<Longrightarrow> thesis` distinct.simps(2) hd_in_set list.inject set_empty2 tfl_some vt wq_def wq_distinct)
+by (rule_tac waiting_unique[OF vt waits2_cs])
-by (metis (mono_tags, lifting) `\<And>thesis. (\<And>wts. wq s cs = th # wts \<Longrightarrow> thesis) \<Longrightarrow> thesis` distinct.simps(2) hd_in_set list.sel(1) set_empty2 tfl_some vt wq_def wq_distinct)
+then show "False" using a b(1) by simp
-then show "False" using a b by simp
+qed
-qed
-then have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>*"
-by (metis node.distinct(1) rtranclD)
 ultimately
-show "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))"
+show "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth) })" by simp
-by (simp add: acyclic_insert)
 qed
-ultimately have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
+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)

changeset 38	c89013dca1aa
parent 37	c820ac0f3088
child 39	7ea6b019ce24