# HG changeset patch
# User zhang
# Date 1334566100 0
# Node ID 0244e76df2ca8ee2669115568343a9ddf8ccdd06
# Parent  b3add51e2e0f135594bcf291aa0ba0dd364ef243
The result for "Set" operation gets strengthened.

diff -r b3add51e2e0f -r 0244e76df2ca prio/CpsG.thy
--- a/prio/CpsG.thy	Sun Apr 15 21:53:12 2012 +0000
+++ b/prio/CpsG.thy	Mon Apr 16 08:48:20 2012 +0000
@@ -646,7 +646,7 @@
 lemma eq_dep: "depend s = depend s'"
   by (unfold s_def depend_set_unchanged, auto)
 
-lemma eq_cp:
+lemma eq_cp_pre:
   fixes th' 
   assumes neq_th: "th' \<noteq> th"
   and nd: "th \<notin> dependents s th'"
@@ -677,6 +677,35 @@
         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'"
@@ -741,7 +770,7 @@
               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 neq_th1 this]
+            from eq_cp_pre[OF neq_th1 this]
             show ?thesis .
           qed
         }
@@ -789,7 +818,7 @@
               show False by (auto simp:children_def)
             qed
             thus ?thesis
-            proof(rule eq_cp)
+            proof(rule eq_cp_pre)
               show "th \<notin> dependents s th1"
               proof
                 assume "th \<in> dependents s th1"
@@ -874,7 +903,7 @@
               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 neq_th1 this]
+            from eq_cp_pre[OF neq_th1 this]
             show ?thesis .
           qed
         }
@@ -914,7 +943,7 @@
             case False
             assume neq_th1: "th1 \<noteq> th"
             thus ?thesis
-            proof(rule eq_cp)
+            proof(rule eq_cp_pre)
               show "th \<notin> dependents s th1"
               proof
                 assume "th \<in> dependents s th1"
@@ -995,6 +1024,9 @@
   qed
 qed
 
+
+
+
 locale step_v_cps =
   fixes s' th cs s 
   defines s_def : "s \<equiv> (V th cs#s')"