--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/CpsG.thy Thu Dec 06 15:11:21 2012 +0000
@@ -0,0 +1,1997 @@
+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
+