--- a/prio/CpsG.thy Mon Dec 03 08:16:58 2012 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1997 +0,0 @@
-theory CpsG
-imports PrioG
-begin
-
-lemma not_thread_holdents:
- fixes th s
- assumes vt: "vt s"
- and not_in: "th \<notin> threads s"
- shows "holdents s th = {}"
-proof -
- from vt not_in show ?thesis
- proof(induct arbitrary:th)
- case (vt_cons s e th)
- assume vt: "vt s"
- and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"
- and stp: "step s e"
- and not_in: "th \<notin> threads (e # s)"
- from stp show ?case
- proof(cases)
- case (thread_create thread prio)
- assume eq_e: "e = Create thread prio"
- and not_in': "thread \<notin> threads s"
- have "holdents (e # s) th = holdents s th"
- apply (unfold eq_e holdents_test)
- by (simp add:depend_create_unchanged)
- moreover have "th \<notin> threads s"
- proof -
- from not_in eq_e show ?thesis by simp
- qed
- moreover note ih ultimately show ?thesis by auto
- next
- case (thread_exit thread)
- assume eq_e: "e = Exit thread"
- and nh: "holdents s thread = {}"
- show ?thesis
- proof(cases "th = thread")
- case True
- with nh eq_e
- show ?thesis
- by (auto simp:holdents_test depend_exit_unchanged)
- next
- case False
- with not_in and eq_e
- have "th \<notin> threads s" by simp
- from ih[OF this] False eq_e show ?thesis
- by (auto simp:holdents_test depend_exit_unchanged)
- qed
- next
- case (thread_P thread cs)
- assume eq_e: "e = P thread cs"
- and is_runing: "thread \<in> runing s"
- from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto
- have neq_th: "th \<noteq> thread"
- proof -
- from not_in eq_e have "th \<notin> threads s" by simp
- moreover from is_runing have "thread \<in> threads s"
- by (simp add:runing_def readys_def)
- ultimately show ?thesis by auto
- qed
- hence "holdents (e # s) th = holdents s th "
- apply (unfold cntCS_def holdents_test eq_e)
- by (unfold step_depend_p[OF vtp], auto)
- moreover have "holdents s th = {}"
- proof(rule ih)
- from not_in eq_e show "th \<notin> threads s" by simp
- qed
- ultimately show ?thesis by simp
- next
- case (thread_V thread cs)
- assume eq_e: "e = V thread cs"
- and is_runing: "thread \<in> runing s"
- and hold: "holding s thread cs"
- have neq_th: "th \<noteq> thread"
- proof -
- from not_in eq_e have "th \<notin> threads s" by simp
- moreover from is_runing have "thread \<in> threads s"
- by (simp add:runing_def readys_def)
- ultimately show ?thesis by auto
- qed
- from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto
- from hold obtain rest
- where eq_wq: "wq s cs = thread # rest"
- by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
- from not_in eq_e eq_wq
- have "\<not> next_th s thread cs th"
- apply (auto simp:next_th_def)
- proof -
- assume ne: "rest \<noteq> []"
- and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")
- have "?t \<in> set rest"
- proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
- next
- fix x assume "distinct x \<and> set x = set rest" with ne
- show "hd x \<in> set rest" by (cases x, auto)
- qed
- with eq_wq have "?t \<in> set (wq s cs)" by simp
- from wq_threads[OF step_back_vt[OF vtv], OF this] and ni
- show False by auto
- qed
- moreover note neq_th eq_wq
- ultimately have "holdents (e # s) th = holdents s th"
- by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto)
- moreover have "holdents s th = {}"
- proof(rule ih)
- from not_in eq_e show "th \<notin> threads s" by simp
- qed
- ultimately show ?thesis by simp
- next
- case (thread_set thread prio)
- print_facts
- assume eq_e: "e = Set thread prio"
- and is_runing: "thread \<in> runing s"
- from not_in and eq_e have "th \<notin> threads s" by auto
- from ih [OF this] and eq_e
- show ?thesis
- apply (unfold eq_e cntCS_def holdents_test)
- by (simp add:depend_set_unchanged)
- qed
- next
- case vt_nil
- show ?case
- by (auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)
- qed
-qed
-
-
-
-lemma next_th_neq:
- assumes vt: "vt s"
- and nt: "next_th s th cs th'"
- shows "th' \<noteq> th"
-proof -
- from nt show ?thesis
- apply (auto simp:next_th_def)
- proof -
- fix rest
- assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
- and ne: "rest \<noteq> []"
- have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest"
- proof(rule someI2)
- from wq_distinct[OF vt, of cs] eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
- next
- fix x
- assume "distinct x \<and> set x = set rest"
- hence eq_set: "set x = set rest" by auto
- with ne have "x \<noteq> []" by auto
- hence "hd x \<in> set x" by auto
- with eq_set show "hd x \<in> set rest" by auto
- qed
- with wq_distinct[OF vt, of cs] eq_wq show False by auto
- qed
-qed
-
-lemma next_th_unique:
- assumes nt1: "next_th s th cs th1"
- and nt2: "next_th s th cs th2"
- shows "th1 = th2"
-proof -
- from assms show ?thesis
- by (unfold next_th_def, auto)
-qed
-
-lemma pp_sub: "(r^+)^+ \<subseteq> r^+"
- by auto
-
-lemma wf_depend:
- assumes vt: "vt s"
- shows "wf (depend s)"
-proof(rule finite_acyclic_wf)
- from finite_depend[OF vt] show "finite (depend s)" .
-next
- from acyclic_depend[OF vt] show "acyclic (depend s)" .
-qed
-
-lemma Max_Union:
- assumes fc: "finite C"
- and ne: "C \<noteq> {}"
- and fa: "\<And> A. A \<in> C \<Longrightarrow> finite A \<and> A \<noteq> {}"
- shows "Max (\<Union> C) = Max (Max ` C)"
-proof -
- from fc ne fa show ?thesis
- proof(induct)
- case (insert x F)
- assume ih: "\<lbrakk>F \<noteq> {}; \<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}\<rbrakk> \<Longrightarrow> Max (\<Union>F) = Max (Max ` F)"
- and h: "\<And> A. A \<in> insert x F \<Longrightarrow> finite A \<and> A \<noteq> {}"
- show ?case (is "?L = ?R")
- proof(cases "F = {}")
- case False
- from Union_insert have "?L = Max (x \<union> (\<Union> F))" by simp
- also have "\<dots> = max (Max x) (Max(\<Union> F))"
- proof(rule Max_Un)
- from h[of x] show "finite x" by auto
- next
- from h[of x] show "x \<noteq> {}" by auto
- next
- show "finite (\<Union>F)"
- proof(rule finite_Union)
- show "finite F" by fact
- next
- from h show "\<And>M. M \<in> F \<Longrightarrow> finite M" by auto
- qed
- next
- from False and h show "\<Union>F \<noteq> {}" by auto
- qed
- also have "\<dots> = ?R"
- proof -
- have "?R = Max (Max ` ({x} \<union> F))" by simp
- also have "\<dots> = Max ({Max x} \<union> (Max ` F))" by simp
- also have "\<dots> = max (Max x) (Max (\<Union>F))"
- proof -
- have "Max ({Max x} \<union> Max ` F) = max (Max {Max x}) (Max (Max ` F))"
- proof(rule Max_Un)
- show "finite {Max x}" by simp
- next
- show "{Max x} \<noteq> {}" by simp
- next
- from insert show "finite (Max ` F)" by auto
- next
- from False show "Max ` F \<noteq> {}" by auto
- qed
- moreover have "Max {Max x} = Max x" by simp
- moreover have "Max (\<Union>F) = Max (Max ` F)"
- proof(rule ih)
- show "F \<noteq> {}" by fact
- next
- from h show "\<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}"
- by auto
- qed
- ultimately show ?thesis by auto
- qed
- finally show ?thesis by simp
- qed
- finally show ?thesis by simp
- next
- case True
- thus ?thesis by auto
- qed
- next
- case empty
- assume "{} \<noteq> {}" show ?case by auto
- qed
-qed
-
-definition child :: "state \<Rightarrow> (node \<times> node) set"
- where "child s \<equiv>
- {(Th th', Th th) | th th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
-
-definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
- where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"
-
-lemma children_def2:
- "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
-unfolding child_def children_def by simp
-
-lemma children_dependents: "children s th \<subseteq> dependents (wq s) th"
- by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
-
-lemma child_unique:
- assumes vt: "vt s"
- and ch1: "(Th th, Th th1) \<in> child s"
- and ch2: "(Th th, Th th2) \<in> child s"
- shows "th1 = th2"
-proof -
- from ch1 ch2 show ?thesis
- proof(unfold child_def, clarsimp)
- fix cs csa
- assume h1: "(Th th, Cs cs) \<in> depend s"
- and h2: "(Cs cs, Th th1) \<in> depend s"
- and h3: "(Th th, Cs csa) \<in> depend s"
- and h4: "(Cs csa, Th th2) \<in> depend s"
- from unique_depend[OF vt h1 h3] have "cs = csa" by simp
- with h4 have "(Cs cs, Th th2) \<in> depend s" by simp
- from unique_depend[OF vt h2 this]
- show "th1 = th2" by simp
- qed
-qed
-
-
-lemma cp_eq_cpreced_f: "cp s = cpreced (wq s) s"
-proof -
- from fun_eq_iff
- have h:"\<And>f g. (\<forall> x. f x = g x) \<Longrightarrow> f = g" by auto
- show ?thesis
- proof(rule h)
- from cp_eq_cpreced show "\<forall>x. cp s x = cpreced (wq s) s x" by auto
- qed
-qed
-
-lemma depend_children:
- assumes h: "(Th th1, Th th2) \<in> (depend s)^+"
- shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)^+)"
-proof -
- from h show ?thesis
- proof(induct rule: tranclE)
- fix c th2
- assume h1: "(Th th1, c) \<in> (depend s)\<^sup>+"
- and h2: "(c, Th th2) \<in> depend s"
- from h2 obtain cs where eq_c: "c = Cs cs"
- by (case_tac c, auto simp:s_depend_def)
- show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)"
- proof(rule tranclE[OF h1])
- fix ca
- assume h3: "(Th th1, ca) \<in> (depend s)\<^sup>+"
- and h4: "(ca, c) \<in> depend s"
- show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)"
- proof -
- from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"
- by (case_tac ca, auto simp:s_depend_def)
- from eq_ca h4 h2 eq_c
- have "th3 \<in> children s th2" by (auto simp:children_def child_def)
- moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (depend s)\<^sup>+" by simp
- ultimately show ?thesis by auto
- qed
- next
- assume "(Th th1, c) \<in> depend s"
- with h2 eq_c
- have "th1 \<in> children s th2"
- by (auto simp:children_def child_def)
- thus ?thesis by auto
- qed
- next
- assume "(Th th1, Th th2) \<in> depend s"
- thus ?thesis
- by (auto simp:s_depend_def)
- qed
-qed
-
-lemma sub_child: "child s \<subseteq> (depend s)^+"
- by (unfold child_def, auto)
-
-lemma wf_child:
- assumes vt: "vt s"
- shows "wf (child s)"
-proof(rule wf_subset)
- from wf_trancl[OF wf_depend[OF vt]]
- show "wf ((depend s)\<^sup>+)" .
-next
- from sub_child show "child s \<subseteq> (depend s)\<^sup>+" .
-qed
-
-lemma depend_child_pre:
- assumes vt: "vt s"
- shows
- "(Th th, n) \<in> (depend s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
-proof -
- from wf_trancl[OF wf_depend[OF vt]]
- have wf: "wf ((depend s)^+)" .
- show ?thesis
- proof(rule wf_induct[OF wf, of ?P], clarsimp)
- fix th'
- assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (depend s)\<^sup>+ \<longrightarrow>
- (Th th, y) \<in> (depend s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"
- and h: "(Th th, Th th') \<in> (depend s)\<^sup>+"
- show "(Th th, Th th') \<in> (child s)\<^sup>+"
- proof -
- from depend_children[OF h]
- have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (depend s)\<^sup>+)" .
- thus ?thesis
- proof
- assume "th \<in> children s th'"
- thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
- next
- assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (depend s)\<^sup>+"
- then obtain th3 where th3_in: "th3 \<in> children s th'"
- and th_dp: "(Th th, Th th3) \<in> (depend s)\<^sup>+" by auto
- from th3_in have "(Th th3, Th th') \<in> (depend s)^+" by (auto simp:children_def child_def)
- from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp
- with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
- qed
- qed
- qed
-qed
-
-lemma depend_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
- by (insert depend_child_pre, auto)
-
-lemma child_depend_p:
- assumes "(n1, n2) \<in> (child s)^+"
- shows "(n1, n2) \<in> (depend s)^+"
-proof -
- from assms show ?thesis
- proof(induct)
- case (base y)
- with sub_child show ?case by auto
- next
- case (step y z)
- assume "(y, z) \<in> child s"
- with sub_child have "(y, z) \<in> (depend s)^+" by auto
- moreover have "(n1, y) \<in> (depend s)^+" by fact
- ultimately show ?case by auto
- qed
-qed
-
-lemma child_depend_eq:
- assumes vt: "vt s"
- shows
- "((Th th1, Th th2) \<in> (child s)^+) =
- ((Th th1, Th th2) \<in> (depend s)^+)"
- by (auto intro: depend_child[OF vt] child_depend_p)
-
-lemma children_no_dep:
- fixes s th th1 th2 th3
- assumes vt: "vt s"
- and ch1: "(Th th1, Th th) \<in> child s"
- and ch2: "(Th th2, Th th) \<in> child s"
- and ch3: "(Th th1, Th th2) \<in> (depend s)^+"
- shows "False"
-proof -
- from depend_child[OF vt ch3]
- have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .
- thus ?thesis
- proof(rule converse_tranclE)
- thm tranclD
- assume "(Th th1, Th th2) \<in> child s"
- from child_unique[OF vt ch1 this] have "th = th2" by simp
- with ch2 have "(Th th2, Th th2) \<in> child s" by simp
- with wf_child[OF vt] show ?thesis by auto
- next
- fix c
- assume h1: "(Th th1, c) \<in> child s"
- and h2: "(c, Th th2) \<in> (child s)\<^sup>+"
- from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)
- with h1 have "(Th th1, Th th3) \<in> child s" by simp
- from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp
- with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp
- with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto
- moreover have "wf ((child s)\<^sup>+)"
- proof(rule wf_trancl)
- from wf_child[OF vt] show "wf (child s)" .
- qed
- ultimately show False by auto
- qed
-qed
-
-lemma unique_depend_p:
- assumes vt: "vt s"
- and dp1: "(n, n1) \<in> (depend s)^+"
- and dp2: "(n, n2) \<in> (depend s)^+"
- and neq: "n1 \<noteq> n2"
- shows "(n1, n2) \<in> (depend s)^+ \<or> (n2, n1) \<in> (depend s)^+"
-proof(rule unique_chain [OF _ dp1 dp2 neq])
- from unique_depend[OF vt]
- show "\<And>a b c. \<lbrakk>(a, b) \<in> depend s; (a, c) \<in> depend s\<rbrakk> \<Longrightarrow> b = c" by auto
-qed
-
-lemma dependents_child_unique:
- fixes s th th1 th2 th3
- assumes vt: "vt s"
- and ch1: "(Th th1, Th th) \<in> child s"
- and ch2: "(Th th2, Th th) \<in> child s"
- and dp1: "th3 \<in> dependents s th1"
- and dp2: "th3 \<in> dependents s th2"
-shows "th1 = th2"
-proof -
- { assume neq: "th1 \<noteq> th2"
- from dp1 have dp1: "(Th th3, Th th1) \<in> (depend s)^+"
- by (simp add:s_dependents_def eq_depend)
- from dp2 have dp2: "(Th th3, Th th2) \<in> (depend s)^+"
- by (simp add:s_dependents_def eq_depend)
- from unique_depend_p[OF vt dp1 dp2] and neq
- have "(Th th1, Th th2) \<in> (depend s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (depend s)\<^sup>+" by auto
- hence False
- proof
- assume "(Th th1, Th th2) \<in> (depend s)\<^sup>+ "
- from children_no_dep[OF vt ch1 ch2 this] show ?thesis .
- next
- assume " (Th th2, Th th1) \<in> (depend s)\<^sup>+"
- from children_no_dep[OF vt ch2 ch1 this] show ?thesis .
- qed
- } thus ?thesis by auto
-qed
-
-lemma cp_rec:
- fixes s th
- assumes vt: "vt s"
- shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
-proof(unfold cp_eq_cpreced_f cpreced_def)
- let ?f = "(\<lambda>th. preced th s)"
- show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
- Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th)"
- proof(cases " children s th = {}")
- case False
- have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th =
- {Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"
- (is "?L = ?R")
- by auto
- also have "\<dots> =
- Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"
- (is "_ = Max ` ?C")
- by auto
- finally have "Max ?L = Max (Max ` ?C)" by auto
- also have "\<dots> = Max (\<Union> ?C)"
- proof(rule Max_Union[symmetric])
- from children_dependents[of s th] finite_threads[OF vt] and dependents_threads[OF vt, of th]
- show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
- by (auto simp:finite_subset)
- next
- from False
- show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<noteq> {}"
- by simp
- next
- show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow>
- finite A \<and> A \<noteq> {}"
- apply (auto simp:finite_subset)
- proof -
- fix th'
- from finite_threads[OF vt] and dependents_threads[OF vt, of th']
- show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th')" by (auto simp:finite_subset)
- qed
- qed
- also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependents (wq s) th)"
- (is "Max ?A = Max ?B")
- proof -
- have "?A = ?B"
- proof
- show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}
- \<subseteq> (\<lambda>th. preced th s) ` dependents (wq s) th"
- proof
- fix x
- assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
- then obtain th' where
- th'_in: "th' \<in> children s th"
- and x_in: "x \<in> ?f ` ({th'} \<union> dependents (wq s) th')" by auto
- hence "x = ?f th' \<or> x \<in> (?f ` dependents (wq s) th')" by auto
- thus "x \<in> ?f ` dependents (wq s) th"
- proof
- assume "x = preced th' s"
- with th'_in and children_dependents
- show "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th" by auto
- next
- assume "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th'"
- moreover note th'_in
- ultimately show " x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"
- by (unfold cs_dependents_def children_def child_def, auto simp:eq_depend)
- qed
- qed
- next
- show "?f ` dependents (wq s) th
- \<subseteq> \<Union>{?f ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
- proof
- fix x
- assume x_in: "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"
- then obtain th' where
- eq_x: "x = ?f th'" and dp: "(Th th', Th th) \<in> (depend s)^+"
- by (auto simp:cs_dependents_def eq_depend)
- from depend_children[OF dp]
- have "th' \<in> children s th \<or> (\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+)" .
- thus "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
- proof
- assume "th' \<in> children s th"
- with eq_x
- show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
- by auto
- next
- assume "\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+"
- then obtain th3 where th3_in: "th3 \<in> children s th"
- and dp3: "(Th th', Th th3) \<in> (depend s)\<^sup>+" by auto
- show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
- proof -
- from dp3
- have "th' \<in> dependents (wq s) th3"
- by (auto simp:cs_dependents_def eq_depend)
- with eq_x th3_in show ?thesis by auto
- qed
- qed
- qed
- qed
- thus ?thesis by simp
- qed
- finally have "Max ((\<lambda>th. preced th s) ` dependents (wq s) th) = Max (?L)"
- (is "?X = ?Y") by auto
- moreover have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
- max (?f th) ?X"
- proof -
- have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
- Max ({?f th} \<union> ?f ` (dependents (wq s) th))" by simp
- also have "\<dots> = max (Max {?f th}) (Max (?f ` (dependents (wq s) th)))"
- proof(rule Max_Un, auto)
- from finite_threads[OF vt] and dependents_threads[OF vt, of th]
- show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th)" by (auto simp:finite_subset)
- next
- assume "dependents (wq s) th = {}"
- with False and children_dependents show False by auto
- qed
- also have "\<dots> = max (?f th) ?X" by simp
- finally show ?thesis .
- qed
- moreover have "Max ({preced th s} \<union>
- (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) =
- max (?f th) ?Y"
- proof -
- have "Max ({preced th s} \<union>
- (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) =
- max (Max {preced th s}) ?Y"
- proof(rule Max_Un, auto)
- from finite_threads[OF vt] dependents_threads[OF vt, of th] children_dependents [of s th]
- show "finite ((\<lambda>th. Max (insert (preced th s) ((\<lambda>th. preced th s) ` dependents (wq s) th))) `
- children s th)"
- by (auto simp:finite_subset)
- next
- assume "children s th = {}"
- with False show False by auto
- qed
- thus ?thesis by simp
- qed
- ultimately show ?thesis by auto
- next
- case True
- moreover have "dependents (wq s) th = {}"
- proof -
- { fix th'
- assume "th' \<in> dependents (wq s) th"
- hence " (Th th', Th th) \<in> (depend s)\<^sup>+" by (simp add:cs_dependents_def eq_depend)
- from depend_children[OF this] and True
- have "False" by auto
- } thus ?thesis by auto
- qed
- ultimately show ?thesis by auto
- qed
-qed
-
-definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
-where "cps s = {(th, cp s th) | th . th \<in> threads s}"
-
-locale step_set_cps =
- fixes s' th prio s
- defines s_def : "s \<equiv> (Set th prio#s')"
- assumes vt_s: "vt s"
-
-context step_set_cps
-begin
-
-lemma eq_preced:
- fixes th'
- assumes "th' \<noteq> th"
- shows "preced th' s = preced th' s'"
-proof -
- from assms show ?thesis
- by (unfold s_def, auto simp:preced_def)
-qed
-
-lemma eq_dep: "depend s = depend s'"
- by (unfold s_def depend_set_unchanged, auto)
-
-lemma eq_cp_pre:
- fixes th'
- assumes neq_th: "th' \<noteq> th"
- and nd: "th \<notin> dependents s th'"
- shows "cp s th' = cp s' th'"
- apply (unfold cp_eq_cpreced cpreced_def)
-proof -
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
- moreover {
- fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
- hence "preced th1 s = preced th1 s'"
- proof
- assume "th1 = th'"
- with eq_preced[OF neq_th]
- show "preced th1 s = preced th1 s'" by simp
- next
- assume "th1 \<in> dependents (wq s') th'"
- with nd and eq_dp have "th1 \<noteq> th"
- by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
- from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp
- qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
- by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
-qed
-
-lemma no_dependents:
- assumes "th' \<noteq> th"
- shows "th \<notin> dependents s th'"
-proof
- assume h: "th \<in> dependents s th'"
- from step_back_step [OF vt_s[unfolded s_def]]
- have "step s' (Set th prio)" .
- hence "th \<in> runing s'" by (cases, simp)
- hence rd_th: "th \<in> readys s'"
- by (simp add:readys_def runing_def)
- from h have "(Th th, Th th') \<in> (depend s')\<^sup>+"
- by (unfold s_dependents_def, unfold eq_depend, unfold eq_dep, auto)
- from tranclD[OF this]
- obtain z where "(Th th, z) \<in> depend s'" by auto
- with rd_th show "False"
- apply (case_tac z, auto simp:readys_def s_waiting_def s_depend_def s_waiting_def cs_waiting_def)
- by (fold wq_def, blast)
-qed
-
-(* Result improved *)
-lemma eq_cp:
- fixes th'
- assumes neq_th: "th' \<noteq> th"
- shows "cp s th' = cp s' th'"
-proof(rule eq_cp_pre [OF neq_th])
- from no_dependents[OF neq_th]
- show "th \<notin> dependents s th'" .
-qed
-
-lemma eq_up:
- fixes th' th''
- assumes dp1: "th \<in> dependents s th'"
- and dp2: "th' \<in> dependents s th''"
- and eq_cps: "cp s th' = cp s' th'"
- shows "cp s th'' = cp s' th''"
-proof -
- from dp2
- have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
- from depend_child[OF vt_s this[unfolded eq_depend]]
- have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
- moreover { fix n th''
- have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
- (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
- proof(erule trancl_induct, auto)
- fix y th''
- assume y_ch: "(y, Th th'') \<in> child s"
- and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
- and ch': "(Th th', y) \<in> (child s)\<^sup>+"
- from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
- with ih have eq_cpy:"cp s thy = cp s' thy" by blast
- from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
- moreover from child_depend_p[OF ch'] and eq_y
- have "(Th th', Th thy) \<in> (depend s)^+" by simp
- ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
- show "cp s th'' = cp s' th''"
- apply (subst cp_rec[OF vt_s])
- proof -
- have "preced th'' s = preced th'' s'"
- proof(rule eq_preced)
- show "th'' \<noteq> th"
- proof
- assume "th'' = th"
- with dp_thy y_ch[unfolded eq_y]
- have "(Th th, Th th) \<in> (depend s)^+"
- by (auto simp:child_def)
- with wf_trancl[OF wf_depend[OF vt_s]]
- show False by auto
- qed
- qed
- moreover {
- fix th1
- assume th1_in: "th1 \<in> children s th''"
- have "cp s th1 = cp s' th1"
- proof(cases "th1 = thy")
- case True
- with eq_cpy show ?thesis by simp
- next
- case False
- have neq_th1: "th1 \<noteq> th"
- proof
- assume eq_th1: "th1 = th"
- with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
- from children_no_dep[OF vt_s _ _ this] and
- th1_in y_ch eq_y show False by (auto simp:children_def)
- qed
- have "th \<notin> dependents s th1"
- proof
- assume h:"th \<in> dependents s th1"
- from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
- from dependents_child_unique[OF vt_s _ _ h this]
- th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
- with False show False by auto
- qed
- from eq_cp_pre[OF neq_th1 this]
- show ?thesis .
- qed
- }
- ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
- {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
- moreover have "children s th'' = children s' th''"
- by (unfold children_def child_def s_def depend_set_unchanged, simp)
- ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
- by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
- qed
- next
- fix th''
- assume dp': "(Th th', Th th'') \<in> child s"
- show "cp s th'' = cp s' th''"
- apply (subst cp_rec[OF vt_s])
- proof -
- have "preced th'' s = preced th'' s'"
- proof(rule eq_preced)
- show "th'' \<noteq> th"
- proof
- assume "th'' = th"
- with dp1 dp'
- have "(Th th, Th th) \<in> (depend s)^+"
- by (auto simp:child_def s_dependents_def eq_depend)
- with wf_trancl[OF wf_depend[OF vt_s]]
- show False by auto
- qed
- qed
- moreover {
- fix th1
- assume th1_in: "th1 \<in> children s th''"
- have "cp s th1 = cp s' th1"
- proof(cases "th1 = th'")
- case True
- with eq_cps show ?thesis by simp
- next
- case False
- have neq_th1: "th1 \<noteq> th"
- proof
- assume eq_th1: "th1 = th"
- with dp1 have "(Th th1, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
- from children_no_dep[OF vt_s _ _ this]
- th1_in dp'
- show False by (auto simp:children_def)
- qed
- thus ?thesis
- proof(rule eq_cp_pre)
- show "th \<notin> dependents s th1"
- proof
- assume "th \<in> dependents s th1"
- from dependents_child_unique[OF vt_s _ _ this dp1]
- th1_in dp' have "th1 = th'"
- by (auto simp:children_def)
- with False show False by auto
- qed
- qed
- qed
- }
- ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
- {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
- moreover have "children s th'' = children s' th''"
- by (unfold children_def child_def s_def depend_set_unchanged, simp)
- ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
- by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
- qed
- qed
- }
- ultimately show ?thesis by auto
-qed
-
-lemma eq_up_self:
- fixes th' th''
- assumes dp: "th \<in> dependents s th''"
- and eq_cps: "cp s th = cp s' th"
- shows "cp s th'' = cp s' th''"
-proof -
- from dp
- have "(Th th, Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
- from depend_child[OF vt_s this[unfolded eq_depend]]
- have ch_th': "(Th th, Th th'') \<in> (child s)\<^sup>+" .
- moreover { fix n th''
- have "\<lbrakk>(Th th, n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
- (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
- proof(erule trancl_induct, auto)
- fix y th''
- assume y_ch: "(y, Th th'') \<in> child s"
- and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
- and ch': "(Th th, y) \<in> (child s)\<^sup>+"
- from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
- with ih have eq_cpy:"cp s thy = cp s' thy" by blast
- from child_depend_p[OF ch'] and eq_y
- have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by simp
- show "cp s th'' = cp s' th''"
- apply (subst cp_rec[OF vt_s])
- proof -
- have "preced th'' s = preced th'' s'"
- proof(rule eq_preced)
- show "th'' \<noteq> th"
- proof
- assume "th'' = th"
- with dp_thy y_ch[unfolded eq_y]
- have "(Th th, Th th) \<in> (depend s)^+"
- by (auto simp:child_def)
- with wf_trancl[OF wf_depend[OF vt_s]]
- show False by auto
- qed
- qed
- moreover {
- fix th1
- assume th1_in: "th1 \<in> children s th''"
- have "cp s th1 = cp s' th1"
- proof(cases "th1 = thy")
- case True
- with eq_cpy show ?thesis by simp
- next
- case False
- have neq_th1: "th1 \<noteq> th"
- proof
- assume eq_th1: "th1 = th"
- with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
- from children_no_dep[OF vt_s _ _ this] and
- th1_in y_ch eq_y show False by (auto simp:children_def)
- qed
- have "th \<notin> dependents s th1"
- proof
- assume h:"th \<in> dependents s th1"
- from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
- from dependents_child_unique[OF vt_s _ _ h this]
- th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
- with False show False by auto
- qed
- from eq_cp_pre[OF neq_th1 this]
- show ?thesis .
- qed
- }
- ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
- {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
- moreover have "children s th'' = children s' th''"
- by (unfold children_def child_def s_def depend_set_unchanged, simp)
- ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
- by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
- qed
- next
- fix th''
- assume dp': "(Th th, Th th'') \<in> child s"
- show "cp s th'' = cp s' th''"
- apply (subst cp_rec[OF vt_s])
- proof -
- have "preced th'' s = preced th'' s'"
- proof(rule eq_preced)
- show "th'' \<noteq> th"
- proof
- assume "th'' = th"
- with dp dp'
- have "(Th th, Th th) \<in> (depend s)^+"
- by (auto simp:child_def s_dependents_def eq_depend)
- with wf_trancl[OF wf_depend[OF vt_s]]
- show False by auto
- qed
- qed
- moreover {
- fix th1
- assume th1_in: "th1 \<in> children s th''"
- have "cp s th1 = cp s' th1"
- proof(cases "th1 = th")
- case True
- with eq_cps show ?thesis by simp
- next
- case False
- assume neq_th1: "th1 \<noteq> th"
- thus ?thesis
- proof(rule eq_cp_pre)
- show "th \<notin> dependents s th1"
- proof
- assume "th \<in> dependents s th1"
- hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
- from children_no_dep[OF vt_s _ _ this]
- and th1_in dp' show False
- by (auto simp:children_def)
- qed
- qed
- qed
- }
- ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
- {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
- moreover have "children s th'' = children s' th''"
- by (unfold children_def child_def s_def depend_set_unchanged, simp)
- ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
- by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
- qed
- qed
- }
- ultimately show ?thesis by auto
-qed
-end
-
-lemma next_waiting:
- assumes vt: "vt s"
- and nxt: "next_th s th cs th'"
- shows "waiting s th' cs"
-proof -
- from assms show ?thesis
- apply (auto simp:next_th_def s_waiting_def[folded wq_def])
- proof -
- fix rest
- assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
- and eq_wq: "wq s cs = th # rest"
- and ne: "rest \<noteq> []"
- have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
- proof(rule someI2)
- from wq_distinct[OF vt, of cs] eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
- next
- show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
- qed
- with ni
- have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set (SOME q. distinct q \<and> set q = set rest)"
- by simp
- moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
- proof(rule someI2)
- from wq_distinct[OF vt, of cs] eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
- next
- from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
- qed
- ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
- next
- fix rest
- assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
- and ne: "rest \<noteq> []"
- have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
- proof(rule someI2)
- from wq_distinct[OF vt, of cs] eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
- next
- from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
- qed
- hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)"
- by auto
- moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
- proof(rule someI2)
- from wq_distinct[OF vt, of cs] eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
- next
- show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
- qed
- ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp
- with eq_wq and wq_distinct[OF vt, of cs]
- show False by auto
- qed
-qed
-
-
-
-
-locale step_v_cps =
- fixes s' th cs s
- defines s_def : "s \<equiv> (V th cs#s')"
- assumes vt_s: "vt s"
-
-locale step_v_cps_nt = step_v_cps +
- fixes th'
- assumes nt: "next_th s' th cs th'"
-
-context step_v_cps_nt
-begin
-
-lemma depend_s:
- "depend s = (depend s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
- {(Cs cs, Th th')}"
-proof -
- from step_depend_v[OF vt_s[unfolded s_def], folded s_def]
- and nt show ?thesis by (auto intro:next_th_unique)
-qed
-
-lemma dependents_kept:
- fixes th''
- assumes neq1: "th'' \<noteq> th"
- and neq2: "th'' \<noteq> th'"
- shows "dependents (wq s) th'' = dependents (wq s') th''"
-proof(auto)
- fix x
- assume "x \<in> dependents (wq s) th''"
- hence dp: "(Th x, Th th'') \<in> (depend s)^+"
- by (auto simp:cs_dependents_def eq_depend)
- { fix n
- have "(n, Th th'') \<in> (depend s)^+ \<Longrightarrow> (n, Th th'') \<in> (depend s')^+"
- proof(induct rule:converse_trancl_induct)
- fix y
- assume "(y, Th th'') \<in> depend s"
- with depend_s neq1 neq2
- have "(y, Th th'') \<in> depend s'" by auto
- thus "(y, Th th'') \<in> (depend s')\<^sup>+" by auto
- next
- fix y z
- assume yz: "(y, z) \<in> depend s"
- and ztp: "(z, Th th'') \<in> (depend s)\<^sup>+"
- and ztp': "(z, Th th'') \<in> (depend s')\<^sup>+"
- have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"
- proof
- show "y \<noteq> Cs cs"
- proof
- assume eq_y: "y = Cs cs"
- with yz have dp_yz: "(Cs cs, z) \<in> depend s" by simp
- from depend_s
- have cst': "(Cs cs, Th th') \<in> depend s" by simp
- from unique_depend[OF vt_s this dp_yz]
- have eq_z: "z = Th th'" by simp
- with ztp have "(Th th', Th th'') \<in> (depend s)^+" by simp
- from converse_tranclE[OF this]
- obtain cs' where dp'': "(Th th', Cs cs') \<in> depend s"
- by (auto simp:s_depend_def)
- with depend_s have dp': "(Th th', Cs cs') \<in> depend s'" by auto
- from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (depend s)^+" by auto
- moreover have "cs' = cs"
- proof -
- from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
- have "(Th th', Cs cs) \<in> depend s'"
- by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
- from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']
- show ?thesis by simp
- qed
- ultimately have "(Cs cs, Cs cs) \<in> (depend s)^+" by simp
- moreover note wf_trancl[OF wf_depend[OF vt_s]]
- ultimately show False by auto
- qed
- next
- show "y \<noteq> Th th'"
- proof
- assume eq_y: "y = Th th'"
- with yz have dps: "(Th th', z) \<in> depend s" by simp
- with depend_s have dps': "(Th th', z) \<in> depend s'" by auto
- have "z = Cs cs"
- proof -
- from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
- have "(Th th', Cs cs) \<in> depend s'"
- by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
- from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
- show ?thesis .
- qed
- with dps depend_s show False by auto
- qed
- qed
- with depend_s yz have "(y, z) \<in> depend s'" by auto
- with ztp'
- show "(y, Th th'') \<in> (depend s')\<^sup>+" by auto
- qed
- }
- from this[OF dp]
- show "x \<in> dependents (wq s') th''"
- by (auto simp:cs_dependents_def eq_depend)
-next
- fix x
- assume "x \<in> dependents (wq s') th''"
- hence dp: "(Th x, Th th'') \<in> (depend s')^+"
- by (auto simp:cs_dependents_def eq_depend)
- { fix n
- have "(n, Th th'') \<in> (depend s')^+ \<Longrightarrow> (n, Th th'') \<in> (depend s)^+"
- proof(induct rule:converse_trancl_induct)
- fix y
- assume "(y, Th th'') \<in> depend s'"
- with depend_s neq1 neq2
- have "(y, Th th'') \<in> depend s" by auto
- thus "(y, Th th'') \<in> (depend s)\<^sup>+" by auto
- next
- fix y z
- assume yz: "(y, z) \<in> depend s'"
- and ztp: "(z, Th th'') \<in> (depend s')\<^sup>+"
- and ztp': "(z, Th th'') \<in> (depend s)\<^sup>+"
- have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"
- proof
- show "y \<noteq> Cs cs"
- proof
- assume eq_y: "y = Cs cs"
- with yz have dp_yz: "(Cs cs, z) \<in> depend s'" by simp
- from this have eq_z: "z = Th th"
- proof -
- from step_back_step[OF vt_s[unfolded s_def]]
- have "(Cs cs, Th th) \<in> depend s'"
- by(cases, auto simp: wq_def s_depend_def cs_holding_def s_holding_def)
- from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]
- show ?thesis by simp
- qed
- from converse_tranclE[OF ztp]
- obtain u where "(z, u) \<in> depend s'" by auto
- moreover
- from step_back_step[OF vt_s[unfolded s_def]]
- have "th \<in> readys s'" by (cases, simp add:runing_def)
- moreover note eq_z
- ultimately show False
- by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
- qed
- next
- show "y \<noteq> Th th'"
- proof
- assume eq_y: "y = Th th'"
- with yz have dps: "(Th th', z) \<in> depend s'" by simp
- have "z = Cs cs"
- proof -
- from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
- have "(Th th', Cs cs) \<in> depend s'"
- by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
- from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]
- show ?thesis .
- qed
- with ztp have cs_i: "(Cs cs, Th th'') \<in> (depend s')\<^sup>+" by simp
- from step_back_step[OF vt_s[unfolded s_def]]
- have cs_th: "(Cs cs, Th th) \<in> depend s'"
- by(cases, auto simp: s_depend_def wq_def cs_holding_def s_holding_def)
- have "(Cs cs, Th th'') \<notin> depend s'"
- proof
- assume "(Cs cs, Th th'') \<in> depend s'"
- from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th]
- and neq1 show "False" by simp
- qed
- with converse_tranclE[OF cs_i]
- obtain u where cu: "(Cs cs, u) \<in> depend s'"
- and u_t: "(u, Th th'') \<in> (depend s')\<^sup>+" by auto
- have "u = Th th"
- proof -
- from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] cu cs_th]
- show ?thesis .
- qed
- with u_t have "(Th th, Th th'') \<in> (depend s')\<^sup>+" by simp
- from converse_tranclE[OF this]
- obtain v where "(Th th, v) \<in> (depend s')" by auto
- moreover from step_back_step[OF vt_s[unfolded s_def]]
- have "th \<in> readys s'" by (cases, simp add:runing_def)
- ultimately show False
- by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
- qed
- qed
- with depend_s yz have "(y, z) \<in> depend s" by auto
- with ztp'
- show "(y, Th th'') \<in> (depend s)\<^sup>+" by auto
- qed
- }
- from this[OF dp]
- show "x \<in> dependents (wq s) th''"
- by (auto simp:cs_dependents_def eq_depend)
-qed
-
-lemma cp_kept:
- fixes th''
- assumes neq1: "th'' \<noteq> th"
- and neq2: "th'' \<noteq> th'"
- shows "cp s th'' = cp s' th''"
-proof -
- from dependents_kept[OF neq1 neq2]
- have "dependents (wq s) th'' = dependents (wq s') th''" .
- moreover {
- fix th1
- assume "th1 \<in> dependents (wq s) th''"
- have "preced th1 s = preced th1 s'"
- by (unfold s_def, auto simp:preced_def)
- }
- moreover have "preced th'' s = preced th'' s'"
- by (unfold s_def, auto simp:preced_def)
- ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependents (wq s) th'')) =
- ((\<lambda>th. preced th s') ` ({th''} \<union> dependents (wq s') th''))"
- by (auto simp:image_def)
- thus ?thesis
- by (unfold cp_eq_cpreced cpreced_def, simp)
-qed
-
-end
-
-locale step_v_cps_nnt = step_v_cps +
- assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"
-
-context step_v_cps_nnt
-begin
-
-lemma nw_cs: "(Th th1, Cs cs) \<notin> depend s'"
-proof
- assume "(Th th1, Cs cs) \<in> depend s'"
- thus "False"
- apply (auto simp:s_depend_def cs_waiting_def)
- proof -
- assume h1: "th1 \<in> set (wq s' cs)"
- and h2: "th1 \<noteq> hd (wq s' cs)"
- from step_back_step[OF vt_s[unfolded s_def]]
- show "False"
- proof(cases)
- assume "holding s' th cs"
- then obtain rest where
- eq_wq: "wq s' cs = th#rest"
- apply (unfold s_holding_def wq_def[symmetric])
- by (case_tac "(wq s' cs)", auto)
- with h1 h2 have ne: "rest \<noteq> []" by auto
- with eq_wq
- have "next_th s' th cs (hd (SOME q. distinct q \<and> set q = set rest))"
- by(unfold next_th_def, rule_tac x = "rest" in exI, auto)
- with nnt show ?thesis by auto
- qed
- qed
-qed
-
-lemma depend_s: "depend s = depend s' - {(Cs cs, Th th)}"
-proof -
- from nnt and step_depend_v[OF vt_s[unfolded s_def], folded s_def]
- show ?thesis by auto
-qed
-
-lemma child_kept_left:
- assumes
- "(n1, n2) \<in> (child s')^+"
- shows "(n1, n2) \<in> (child s)^+"
-proof -
- from assms show ?thesis
- proof(induct rule: converse_trancl_induct)
- case (base y)
- from base obtain th1 cs1 th2
- where h1: "(Th th1, Cs cs1) \<in> depend s'"
- and h2: "(Cs cs1, Th th2) \<in> depend s'"
- and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2" by (auto simp:child_def)
- have "cs1 \<noteq> cs"
- proof
- assume eq_cs: "cs1 = cs"
- with h1 have "(Th th1, Cs cs1) \<in> depend s'" by simp
- with nw_cs eq_cs show False by auto
- qed
- with h1 h2 depend_s have
- h1': "(Th th1, Cs cs1) \<in> depend s" and
- h2': "(Cs cs1, Th th2) \<in> depend s" by auto
- hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
- with eq_y eq_n2 have "(y, n2) \<in> child s" by simp
- thus ?case by auto
- next
- case (step y z)
- have "(y, z) \<in> child s'" by fact
- then obtain th1 cs1 th2
- where h1: "(Th th1, Cs cs1) \<in> depend s'"
- and h2: "(Cs cs1, Th th2) \<in> depend s'"
- and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def)
- have "cs1 \<noteq> cs"
- proof
- assume eq_cs: "cs1 = cs"
- with h1 have "(Th th1, Cs cs1) \<in> depend s'" by simp
- with nw_cs eq_cs show False by auto
- qed
- with h1 h2 depend_s have
- h1': "(Th th1, Cs cs1) \<in> depend s" and
- h2': "(Cs cs1, Th th2) \<in> depend s" by auto
- hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
- with eq_y eq_z have "(y, z) \<in> child s" by simp
- moreover have "(z, n2) \<in> (child s)^+" by fact
- ultimately show ?case by auto
- qed
-qed
-
-lemma child_kept_right:
- assumes
- "(n1, n2) \<in> (child s)^+"
- shows "(n1, n2) \<in> (child s')^+"
-proof -
- from assms show ?thesis
- proof(induct)
- case (base y)
- from base and depend_s
- have "(n1, y) \<in> child s'"
- by (auto simp:child_def)
- thus ?case by auto
- next
- case (step y z)
- have "(y, z) \<in> child s" by fact
- with depend_s have "(y, z) \<in> child s'"
- by (auto simp:child_def)
- moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact
- ultimately show ?case by auto
- qed
-qed
-
-lemma eq_child: "(child s)^+ = (child s')^+"
- by (insert child_kept_left child_kept_right, auto)
-
-lemma eq_cp:
- fixes th'
- shows "cp s th' = cp s' th'"
- apply (unfold cp_eq_cpreced cpreced_def)
-proof -
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- apply (unfold cs_dependents_def, unfold eq_depend)
- proof -
- from eq_child
- have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
- by simp
- with child_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
- show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"
- by simp
- qed
- moreover {
- fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
- hence "preced th1 s = preced th1 s'"
- proof
- assume "th1 = th'"
- show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
- next
- assume "th1 \<in> dependents (wq s') th'"
- show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
- qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
- by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
-qed
-
-end
-
-locale step_P_cps =
- fixes s' th cs s
- defines s_def : "s \<equiv> (P th cs#s')"
- assumes vt_s: "vt s"
-
-locale step_P_cps_ne =step_P_cps +
- assumes ne: "wq s' cs \<noteq> []"
-
-locale step_P_cps_e =step_P_cps +
- assumes ee: "wq s' cs = []"
-
-context step_P_cps_e
-begin
-
-lemma depend_s: "depend s = depend s' \<union> {(Cs cs, Th th)}"
-proof -
- from ee and step_depend_p[OF vt_s[unfolded s_def], folded s_def]
- show ?thesis by auto
-qed
-
-lemma child_kept_left:
- assumes
- "(n1, n2) \<in> (child s')^+"
- shows "(n1, n2) \<in> (child s)^+"
-proof -
- from assms show ?thesis
- proof(induct rule: converse_trancl_induct)
- case (base y)
- from base obtain th1 cs1 th2
- where h1: "(Th th1, Cs cs1) \<in> depend s'"
- and h2: "(Cs cs1, Th th2) \<in> depend s'"
- and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2" by (auto simp:child_def)
- have "cs1 \<noteq> cs"
- proof
- assume eq_cs: "cs1 = cs"
- with h1 have "(Th th1, Cs cs) \<in> depend s'" by simp
- with ee show False
- by (auto simp:s_depend_def cs_waiting_def)
- qed
- with h1 h2 depend_s have
- h1': "(Th th1, Cs cs1) \<in> depend s" and
- h2': "(Cs cs1, Th th2) \<in> depend s" by auto
- hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
- with eq_y eq_n2 have "(y, n2) \<in> child s" by simp
- thus ?case by auto
- next
- case (step y z)
- have "(y, z) \<in> child s'" by fact
- then obtain th1 cs1 th2
- where h1: "(Th th1, Cs cs1) \<in> depend s'"
- and h2: "(Cs cs1, Th th2) \<in> depend s'"
- and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def)
- have "cs1 \<noteq> cs"
- proof
- assume eq_cs: "cs1 = cs"
- with h1 have "(Th th1, Cs cs) \<in> depend s'" by simp
- with ee show False
- by (auto simp:s_depend_def cs_waiting_def)
- qed
- with h1 h2 depend_s have
- h1': "(Th th1, Cs cs1) \<in> depend s" and
- h2': "(Cs cs1, Th th2) \<in> depend s" by auto
- hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
- with eq_y eq_z have "(y, z) \<in> child s" by simp
- moreover have "(z, n2) \<in> (child s)^+" by fact
- ultimately show ?case by auto
- qed
-qed
-
-lemma child_kept_right:
- assumes
- "(n1, n2) \<in> (child s)^+"
- shows "(n1, n2) \<in> (child s')^+"
-proof -
- from assms show ?thesis
- proof(induct)
- case (base y)
- from base and depend_s
- have "(n1, y) \<in> child s'"
- apply (auto simp:child_def)
- proof -
- fix th'
- assume "(Th th', Cs cs) \<in> depend s'"
- with ee have "False"
- by (auto simp:s_depend_def cs_waiting_def)
- thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto
- qed
- thus ?case by auto
- next
- case (step y z)
- have "(y, z) \<in> child s" by fact
- with depend_s have "(y, z) \<in> child s'"
- apply (auto simp:child_def)
- proof -
- fix th'
- assume "(Th th', Cs cs) \<in> depend s'"
- with ee have "False"
- by (auto simp:s_depend_def cs_waiting_def)
- thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto
- qed
- moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact
- ultimately show ?case by auto
- qed
-qed
-
-lemma eq_child: "(child s)^+ = (child s')^+"
- by (insert child_kept_left child_kept_right, auto)
-
-lemma eq_cp:
- fixes th'
- shows "cp s th' = cp s' th'"
- apply (unfold cp_eq_cpreced cpreced_def)
-proof -
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- apply (unfold cs_dependents_def, unfold eq_depend)
- proof -
- from eq_child
- have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
- by auto
- with child_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
- show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"
- by simp
- qed
- moreover {
- fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
- hence "preced th1 s = preced th1 s'"
- proof
- assume "th1 = th'"
- show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
- next
- assume "th1 \<in> dependents (wq s') th'"
- show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
- qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
- by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
-qed
-
-end
-
-context step_P_cps_ne
-begin
-
-lemma depend_s: "depend s = depend s' \<union> {(Th th, Cs cs)}"
-proof -
- from step_depend_p[OF vt_s[unfolded s_def]] and ne
- show ?thesis by (simp add:s_def)
-qed
-
-lemma eq_child_left:
- assumes nd: "(Th th, Th th') \<notin> (child s)^+"
- shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"
-proof(induct rule:converse_trancl_induct)
- case (base y)
- from base obtain th1 cs1
- where h1: "(Th th1, Cs cs1) \<in> depend s"
- and h2: "(Cs cs1, Th th') \<in> depend s"
- and eq_y: "y = Th th1" by (auto simp:child_def)
- have "th1 \<noteq> th"
- proof
- assume "th1 = th"
- with base eq_y have "(Th th, Th th') \<in> child s" by simp
- with nd show False by auto
- qed
- with h1 h2 depend_s
- have h1': "(Th th1, Cs cs1) \<in> depend s'" and
- h2': "(Cs cs1, Th th') \<in> depend s'" by auto
- with eq_y show ?case by (auto simp:child_def)
-next
- case (step y z)
- have yz: "(y, z) \<in> child s" by fact
- then obtain th1 cs1 th2
- where h1: "(Th th1, Cs cs1) \<in> depend s"
- and h2: "(Cs cs1, Th th2) \<in> depend s"
- and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def)
- have "th1 \<noteq> th"
- proof
- assume "th1 = th"
- with yz eq_y have "(Th th, z) \<in> child s" by simp
- moreover have "(z, Th th') \<in> (child s)^+" by fact
- ultimately have "(Th th, Th th') \<in> (child s)^+" by auto
- with nd show False by auto
- qed
- with h1 h2 depend_s have h1': "(Th th1, Cs cs1) \<in> depend s'"
- and h2': "(Cs cs1, Th th2) \<in> depend s'" by auto
- with eq_y eq_z have "(y, z) \<in> child s'" by (auto simp:child_def)
- moreover have "(z, Th th') \<in> (child s')^+" by fact
- ultimately show ?case by auto
-qed
-
-lemma eq_child_right:
- shows "(n1, Th th') \<in> (child s')^+ \<Longrightarrow> (n1, Th th') \<in> (child s)^+"
-proof(induct rule:converse_trancl_induct)
- case (base y)
- with depend_s show ?case by (auto simp:child_def)
-next
- case (step y z)
- have "(y, z) \<in> child s'" by fact
- with depend_s have "(y, z) \<in> child s" by (auto simp:child_def)
- moreover have "(z, Th th') \<in> (child s)^+" by fact
- ultimately show ?case by auto
-qed
-
-lemma eq_child:
- assumes nd: "(Th th, Th th') \<notin> (child s)^+"
- shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)"
- by (insert eq_child_left[OF nd] eq_child_right, auto)
-
-lemma eq_cp:
- fixes th'
- assumes nd: "th \<notin> dependents s th'"
- shows "cp s th' = cp s' th'"
- apply (unfold cp_eq_cpreced cpreced_def)
-proof -
- have nd': "(Th th, Th th') \<notin> (child s)^+"
- proof
- assume "(Th th, Th th') \<in> (child s)\<^sup>+"
- with child_depend_eq[OF vt_s]
- have "(Th th, Th th') \<in> (depend s)\<^sup>+" by simp
- with nd show False
- by (simp add:s_dependents_def eq_depend)
- qed
- have eq_dp: "dependents (wq s) th' = dependents (wq s') th'"
- proof(auto)
- fix x assume " x \<in> dependents (wq s) th'"
- thus "x \<in> dependents (wq s') th'"
- apply (auto simp:cs_dependents_def eq_depend)
- proof -
- assume "(Th x, Th th') \<in> (depend s)\<^sup>+"
- with child_depend_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp
- with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s')^+" by simp
- with child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
- show "(Th x, Th th') \<in> (depend s')\<^sup>+" by simp
- qed
- next
- fix x assume "x \<in> dependents (wq s') th'"
- thus "x \<in> dependents (wq s) th'"
- apply (auto simp:cs_dependents_def eq_depend)
- proof -
- assume "(Th x, Th th') \<in> (depend s')\<^sup>+"
- with child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
- have "(Th x, Th th') \<in> (child s')\<^sup>+" by simp
- with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s)^+" by simp
- with child_depend_eq[OF vt_s]
- show "(Th x, Th th') \<in> (depend s)\<^sup>+" by simp
- qed
- qed
- moreover {
- fix th1 have "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
- by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
-qed
-
-lemma eq_up:
- fixes th' th''
- assumes dp1: "th \<in> dependents s th'"
- and dp2: "th' \<in> dependents s th''"
- and eq_cps: "cp s th' = cp s' th'"
- shows "cp s th'' = cp s' th''"
-proof -
- from dp2
- have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
- from depend_child[OF vt_s this[unfolded eq_depend]]
- have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
- moreover {
- fix n th''
- have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
- (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
- proof(erule trancl_induct, auto)
- fix y th''
- assume y_ch: "(y, Th th'') \<in> child s"
- and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
- and ch': "(Th th', y) \<in> (child s)\<^sup>+"
- from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
- with ih have eq_cpy:"cp s thy = cp s' thy" by blast
- from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
- moreover from child_depend_p[OF ch'] and eq_y
- have "(Th th', Th thy) \<in> (depend s)^+" by simp
- ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
- show "cp s th'' = cp s' th''"
- apply (subst cp_rec[OF vt_s])
- proof -
- have "preced th'' s = preced th'' s'"
- by (simp add:s_def preced_def)
- moreover {
- fix th1
- assume th1_in: "th1 \<in> children s th''"
- have "cp s th1 = cp s' th1"
- proof(cases "th1 = thy")
- case True
- with eq_cpy show ?thesis by simp
- next
- case False
- have neq_th1: "th1 \<noteq> th"
- proof
- assume eq_th1: "th1 = th"
- with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
- from children_no_dep[OF vt_s _ _ this] and
- th1_in y_ch eq_y show False by (auto simp:children_def)
- qed
- have "th \<notin> dependents s th1"
- proof
- assume h:"th \<in> dependents s th1"
- from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
- from dependents_child_unique[OF vt_s _ _ h this]
- th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
- with False show False by auto
- qed
- from eq_cp[OF this]
- show ?thesis .
- qed
- }
- ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
- {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
- moreover have "children s th'' = children s' th''"
- apply (unfold children_def child_def s_def depend_set_unchanged, simp)
- apply (fold s_def, auto simp:depend_s)
- proof -
- assume "(Cs cs, Th th'') \<in> depend s'"
- with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
- from dp1 have "(Th th, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
- from converse_tranclE[OF this]
- obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
- and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
- by (auto simp:s_depend_def)
- have eq_cs: "cs1 = cs"
- proof -
- from depend_s have "(Th th, Cs cs) \<in> depend s" by simp
- from unique_depend[OF vt_s this h1]
- show ?thesis by simp
- qed
- have False
- proof(rule converse_tranclE[OF h2])
- assume "(Cs cs1, Th th') \<in> depend s"
- with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp
- from unique_depend[OF vt_s this cs_th']
- have "th' = th''" by simp
- with ch' y_ch have "(Th th'', Th th'') \<in> (child s)^+" by auto
- with wf_trancl[OF wf_child[OF vt_s]]
- show False by auto
- next
- fix y
- assume "(Cs cs1, y) \<in> depend s"
- and ytd: " (y, Th th') \<in> (depend s)\<^sup>+"
- with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp
- from unique_depend[OF vt_s this cs_th']
- have "y = Th th''" .
- with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp
- from depend_child[OF vt_s this]
- have "(Th th'', Th th') \<in> (child s)\<^sup>+" .
- moreover from ch' y_ch have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto
- ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto
- with wf_trancl[OF wf_child[OF vt_s]]
- show False by auto
- qed
- thus "\<exists>cs. (Th th, Cs cs) \<in> depend s' \<and> (Cs cs, Th th'') \<in> depend s'" by auto
- qed
- ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
- by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
- qed
- next
- fix th''
- assume dp': "(Th th', Th th'') \<in> child s"
- show "cp s th'' = cp s' th''"
- apply (subst cp_rec[OF vt_s])
- proof -
- have "preced th'' s = preced th'' s'"
- by (simp add:s_def preced_def)
- moreover {
- fix th1
- assume th1_in: "th1 \<in> children s th''"
- have "cp s th1 = cp s' th1"
- proof(cases "th1 = th'")
- case True
- with eq_cps show ?thesis by simp
- next
- case False
- have neq_th1: "th1 \<noteq> th"
- proof
- assume eq_th1: "th1 = th"
- with dp1 have "(Th th1, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
- from children_no_dep[OF vt_s _ _ this]
- th1_in dp'
- show False by (auto simp:children_def)
- qed
- show ?thesis
- proof(rule eq_cp)
- show "th \<notin> dependents s th1"
- proof
- assume "th \<in> dependents s th1"
- from dependents_child_unique[OF vt_s _ _ this dp1]
- th1_in dp' have "th1 = th'"
- by (auto simp:children_def)
- with False show False by auto
- qed
- qed
- qed
- }
- ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
- {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
- moreover have "children s th'' = children s' th''"
- apply (unfold children_def child_def s_def depend_set_unchanged, simp)
- apply (fold s_def, auto simp:depend_s)
- proof -
- assume "(Cs cs, Th th'') \<in> depend s'"
- with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
- from dp1 have "(Th th, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
- from converse_tranclE[OF this]
- obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
- and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
- by (auto simp:s_depend_def)
- have eq_cs: "cs1 = cs"
- proof -
- from depend_s have "(Th th, Cs cs) \<in> depend s" by simp
- from unique_depend[OF vt_s this h1]
- show ?thesis by simp
- qed
- have False
- proof(rule converse_tranclE[OF h2])
- assume "(Cs cs1, Th th') \<in> depend s"
- with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp
- from unique_depend[OF vt_s this cs_th']
- have "th' = th''" by simp
- with dp' have "(Th th'', Th th'') \<in> (child s)^+" by auto
- with wf_trancl[OF wf_child[OF vt_s]]
- show False by auto
- next
- fix y
- assume "(Cs cs1, y) \<in> depend s"
- and ytd: " (y, Th th') \<in> (depend s)\<^sup>+"
- with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp
- from unique_depend[OF vt_s this cs_th']
- have "y = Th th''" .
- with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp
- from depend_child[OF vt_s this]
- have "(Th th'', Th th') \<in> (child s)\<^sup>+" .
- moreover from dp' have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto
- ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto
- with wf_trancl[OF wf_child[OF vt_s]]
- show False by auto
- qed
- thus "\<exists>cs. (Th th, Cs cs) \<in> depend s' \<and> (Cs cs, Th th'') \<in> depend s'" by auto
- qed
- ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
- by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
- qed
- qed
- }
- ultimately show ?thesis by auto
-qed
-
-end
-
-locale step_create_cps =
- fixes s' th prio s
- defines s_def : "s \<equiv> (Create th prio#s')"
- assumes vt_s: "vt s"
-
-context step_create_cps
-begin
-
-lemma eq_dep: "depend s = depend s'"
- by (unfold s_def depend_create_unchanged, auto)
-
-lemma eq_cp:
- fixes th'
- assumes neq_th: "th' \<noteq> th"
- shows "cp s th' = cp s' th'"
- apply (unfold cp_eq_cpreced cpreced_def)
-proof -
- have nd: "th \<notin> dependents s th'"
- proof
- assume "th \<in> dependents s th'"
- hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
- with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp
- from converse_tranclE[OF this]
- obtain y where "(Th th, y) \<in> depend s'" by auto
- with dm_depend_threads[OF step_back_vt[OF vt_s[unfolded s_def]]]
- have in_th: "th \<in> threads s'" by auto
- from step_back_step[OF vt_s[unfolded s_def]]
- show False
- proof(cases)
- assume "th \<notin> threads s'"
- with in_th show ?thesis by simp
- qed
- qed
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
- moreover {
- fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
- hence "preced th1 s = preced th1 s'"
- proof
- assume "th1 = th'"
- with neq_th
- show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
- next
- assume "th1 \<in> dependents (wq s') th'"
- with nd and eq_dp have "th1 \<noteq> th"
- by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
- thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
- qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
- by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
-qed
-
-lemma nil_dependents: "dependents s th = {}"
-proof -
- from step_back_step[OF vt_s[unfolded s_def]]
- show ?thesis
- proof(cases)
- assume "th \<notin> threads s'"
- from not_thread_holdents[OF step_back_vt[OF vt_s[unfolded s_def]] this]
- have hdn: " holdents s' th = {}" .
- have "dependents s' th = {}"
- proof -
- { assume "dependents s' th \<noteq> {}"
- then obtain th' where dp: "(Th th', Th th) \<in> (depend s')^+"
- by (auto simp:s_dependents_def eq_depend)
- from tranclE[OF this] obtain cs' where
- "(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def)
- with hdn
- have False by (auto simp:holdents_test)
- } thus ?thesis by auto
- qed
- thus ?thesis
- by (unfold s_def s_dependents_def eq_depend depend_create_unchanged, simp)
- qed
-qed
-
-lemma eq_cp_th: "cp s th = preced th s"
- apply (unfold cp_eq_cpreced cpreced_def)
- by (insert nil_dependents, unfold s_dependents_def cs_dependents_def, auto)
-
-end
-
-
-locale step_exit_cps =
- fixes s' th prio s
- defines s_def : "s \<equiv> (Exit th#s')"
- assumes vt_s: "vt s"
-
-context step_exit_cps
-begin
-
-lemma eq_dep: "depend s = depend s'"
- by (unfold s_def depend_exit_unchanged, auto)
-
-lemma eq_cp:
- fixes th'
- assumes neq_th: "th' \<noteq> th"
- shows "cp s th' = cp s' th'"
- apply (unfold cp_eq_cpreced cpreced_def)
-proof -
- have nd: "th \<notin> dependents s th'"
- proof
- assume "th \<in> dependents s th'"
- hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
- with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp
- from converse_tranclE[OF this]
- obtain cs' where bk: "(Th th, Cs cs') \<in> depend s'"
- by (auto simp:s_depend_def)
- from step_back_step[OF vt_s[unfolded s_def]]
- show False
- proof(cases)
- assume "th \<in> runing s'"
- with bk show ?thesis
- apply (unfold runing_def readys_def s_waiting_def s_depend_def)
- by (auto simp:cs_waiting_def wq_def)
- qed
- qed
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
- moreover {
- fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
- hence "preced th1 s = preced th1 s'"
- proof
- assume "th1 = th'"
- with neq_th
- show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
- next
- assume "th1 \<in> dependents (wq s') th'"
- with nd and eq_dp have "th1 \<noteq> th"
- by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
- thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
- qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
- by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
-qed
-
-end
-end
-