diff -r 2c56b20032a7 -r 0679a84b11ad prio/CpsG.thy
--- 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
-