--- a/prio/CpsG.thy	Mon Jan 30 09:44:33 2012 +0000
+++ b/prio/CpsG.thy	Wed Feb 01 08:16:00 2012 +0000
@@ -1356,6 +1356,142 @@
 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