--- a/prio/CpsG.thy	Tue Apr 17 15:55:37 2012 +0000
+++ b/prio/CpsG.thy	Fri Apr 20 11:27:49 2012 +0000
@@ -2,7 +2,6 @@
 imports PrioG 
 begin
 
-
 lemma not_thread_holdents:
   fixes th s
   assumes vt: "vt s"

--- a/prio/ExtGG.thy	Tue Apr 17 15:55:37 2012 +0000
+++ b/prio/ExtGG.thy	Fri Apr 20 11:27:49 2012 +0000
@@ -546,7 +546,7 @@
     by auto
 qed
 
-lemma pv_blocked:
+lemma pv_blocked_pre:
   fixes th'
   assumes th'_in: "th' \<in> threads (t@s)"
   and neq_th': "th' \<noteq> th"
@@ -584,6 +584,8 @@
   qed
 qed
 
+lemmas pv_blocked = pv_blocked_pre[folded detached_eq [OF vt_t]]
+
 lemma runing_precond_pre:
   fixes th'
   assumes th'_in: "th' \<in> threads s"
@@ -695,6 +697,8 @@
 qed
 *)
 
+lemmas runing_precond_pre_dtc = runing_precond_pre[folded detached_eq[OF vt_t] detached_eq[OF vt_s]]
+
 lemma runing_precond:
   fixes th'
   assumes th'_in: "th' \<in> threads s"
@@ -708,7 +712,7 @@
     from runing_precond_pre[OF th'_in eq_pv neq_th']
     have h1: "th' \<in> threads (t @ s)"  
       and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto
-    from pv_blocked[OF h1 neq_th' h2] have " th' \<notin> runing (t @ s)" .
+    from pv_blocked_pre[OF h1 neq_th' h2] have " th' \<notin> runing (t @ s)" .
     with is_runing show "False" by simp
   qed
   moreover from cnp_cnv_cncs[OF vt_s, of th'] 
@@ -812,7 +816,7 @@
   from assms show ?case by auto
 qed
 
-lemma moment_blocked:
+lemma moment_blocked_eqpv:
   assumes neq_th': "th' \<noteq> th"
   and th'_in: "th' \<in> threads ((moment i t)@s)"
   and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"
@@ -828,6 +832,24 @@
   show ?thesis by auto
 qed
 
+lemma moment_blocked:
+  assumes neq_th': "th' \<noteq> th"
+  and th'_in: "th' \<in> threads ((moment i t)@s)"
+  and dtc: "detached (moment i t @ s) th'"
+  and le_ij: "i \<le> j"
+  shows "detached (moment j t @ s) th' \<and>
+         th' \<in> threads ((moment j t)@s) \<and>
+         th' \<notin> runing ((moment j t)@s)"
+proof -
+  from vt_moment[OF vt_t, of "i+length s"] moment_prefix[of i t s]
+  have vt_i: "vt (moment i t @ s)" by auto
+  from vt_moment[OF vt_t, of "j+length s"] moment_prefix[of j t s]
+  have vt_j: "vt  (moment j t @ s)" by auto
+  from moment_blocked_eqpv [OF neq_th' th'_in detached_elim [OF vt_i dtc] le_ij, 
+  folded detached_eq[OF vt_j]]
+  show ?thesis .
+qed
+
 lemma runing_inversion_1:
   assumes neq_th': "th' \<noteq> th"
   and runing': "th' \<in> runing (t@s)"
@@ -877,7 +899,7 @@
   from eq_e have "th' \<in> threads ((e#moment i t)@s)" by simp
   with eq_me [symmetric]
   have h2: "th' \<in> threads (moment (Suc i) t @ s)" by simp
-  from moment_blocked [OF neq_th' h2 h1, of "length t"] and lt_its
+  from moment_blocked_eqpv [OF neq_th' h2 h1, of "length t"] and lt_its
   and moment_ge
   have "th' \<notin> runing (t @ s)" by auto
   with runing'
@@ -924,7 +946,6 @@
   show ?thesis by auto
 qed
 
-
 lemma live: "runing (t@s) \<noteq> {}"
 proof(cases "th \<in> runing (t@s)")
   case True thus ?thesis by auto
@@ -1002,3 +1023,4 @@
 end
 
 
+

--- a/prio/Moment.thy	Tue Apr 17 15:55:37 2012 +0000
+++ b/prio/Moment.thy	Fri Apr 20 11:27:49 2012 +0000
@@ -770,4 +770,14 @@
   thus ?thesis by (simp add:restm_def)
 qed
 
+lemma moment_prefix: "(moment i t @ s) = moment (i + length s) (t @ s)"
+proof -
+  from moment_plus_split [of i "length s" "t@s"]
+  have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)"
+    by auto
+  with app_moment_restm[of t s]
+  have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" by simp
+  with moment_app show ?thesis by auto
+qed
+
 end
\ No newline at end of file

--- a/prio/PrioG.thy	Tue Apr 17 15:55:37 2012 +0000
+++ b/prio/PrioG.thy	Fri Apr 20 11:27:49 2012 +0000
@@ -173,23 +173,22 @@
   qed
 qed
 
-lemma vt_moment: "\<And> t. \<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)"
+lemma vt_moment: "\<And> t. \<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
 proof(induct s, simp)
   fix a s t
-  assume h: "\<And>t.\<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)"
+  assume h: "\<And>t.\<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
     and vt_a: "vt (a # s)"
-    and le_t: "t \<le> length (a # s)"
   show "vt (moment t (a # s))"
-  proof(cases "t = length (a#s)")
+  proof(cases "t \<ge> length (a#s)")
     case True
     from True have "moment t (a#s) = a#s" by simp
     with vt_a show ?thesis by simp
   next
     case False
-    with le_t have le_t1: "t \<le> length s" by simp
+    hence le_t1: "t \<le> length s" by simp
     from vt_a have "vt s"
       by (erule_tac evt_cons, simp)
-    from h [OF this le_t1] have "vt (moment t s)" .
+    from h [OF this] have "vt (moment t s)" .
     moreover have "moment t (a#s) = moment t s"
     proof -
       from moment_app [OF le_t1, of "[a]"] 
@@ -244,7 +243,7 @@
         h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
       have vt_e: "vt (e#moment t2 s)"
       proof -
-        from vt_moment [OF vt le_t3]
+        from vt_moment [OF vt]
         have "vt (moment ?t3 s)" .
         with eq_m show ?thesis by simp
       qed
@@ -277,7 +276,7 @@
         h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
       have vt_e: "vt  (e#moment t1 s)"
       proof -
-        from vt_moment [OF vt le_t3]
+        from vt_moment [OF vt]
         have "vt (moment ?t3 s)" .
         with eq_m show ?thesis by simp
       qed
@@ -310,7 +309,7 @@
         h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
       have vt_e: "vt (e#moment t1 s)"
       proof -
-        from vt_moment [OF vt le_t3]
+        from vt_moment [OF vt]
         have "vt (moment ?t3 s)" .
         with eq_m show ?thesis by simp
       qed
@@ -342,7 +341,7 @@
           case False
           have vt_e: "vt (e#moment t2 s)"
           proof -
-            from vt_moment [OF vt le_t3] eqt12
+            from vt_moment [OF vt] eqt12
             have "vt (moment (Suc t2) s)" by auto
             with eq_m eqt12 show ?thesis by simp
           qed
@@ -2771,7 +2770,82 @@
     by(rule image_subsetI, auto intro:h)
 next
   show "g ` A \<subseteq> f ` A"
-   by(rule image_subsetI, auto intro:h[symmetric])
+   by (rule image_subsetI, auto intro:h[symmetric])
 qed
 
+definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
+  where "detached s th \<equiv> (Th th \<notin> Field (depend s))"
+
+lemma detached_intro:
+  fixes s th
+  assumes vt: "vt s"
+  and eq_pv: "cntP s th = cntV s th"
+  shows "detached s th"
+proof -
+ from cnp_cnv_cncs[OF vt]
+  have eq_cnt: "cntP s th =
+    cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
+  hence cncs_zero: "cntCS s th = 0"
+    by (auto simp:eq_pv split:if_splits)
+  with eq_cnt
+  have "th \<in> readys s \<or> th \<notin> threads s" by (auto simp:eq_pv)
+  thus ?thesis
+  proof
+    assume "th \<notin> threads s"
+    with range_in[OF vt] dm_depend_threads[OF vt]
+    show ?thesis
+      by (auto simp:detached_def Field_def Domain_def Range_def)
+  next
+    assume "th \<in> readys s"
+    moreover have "Th th \<notin> Range (depend s)"
+    proof -
+      from card_0_eq [OF finite_holding [OF vt]] and cncs_zero
+      have "holdents s th = {}"
+        by (simp add:cntCS_def)
+      thus ?thesis
+        by (auto simp:holdents_def, case_tac x, 
+          auto simp:holdents_def s_depend_def)
+    qed
+    ultimately show ?thesis
+      apply (auto simp:detached_def Field_def Domain_def readys_def)
+      apply (case_tac y, auto simp:s_depend_def)
+      by (erule_tac x = "nat" in allE, simp add: eq_waiting)
+  qed
+qed
+
+lemma detached_elim:
+  fixes s th
+  assumes vt: "vt s"
+  and dtc: "detached s th"
+  shows "cntP s th = cntV s th"
+proof -
+  from cnp_cnv_cncs[OF vt]
+  have eq_pv: " cntP s th =
+    cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
+  have cncs_z: "cntCS s th = 0"
+  proof -
+    from dtc have "holdents s th = {}"
+      by (unfold detached_def holdents_def, auto simp:Field_def Domain_def Range_def)
+    thus ?thesis by (auto simp:cntCS_def)
+  qed
+  show ?thesis
+  proof(cases "th \<in> threads s")
+    case True
+    with dtc 
+    have "th \<in> readys s"
+      by (unfold readys_def detached_def Field_def Domain_def Range_def, 
+           auto simp:eq_waiting s_depend_def)
+    with cncs_z and eq_pv show ?thesis by simp
+  next
+    case False
+    with cncs_z and eq_pv show ?thesis by simp
+  qed
+qed
+
+lemma detached_eq:
+  fixes s th
+  assumes vt: "vt s"
+  shows "(detached s th) = (cntP s th = cntV s th)"
+  by (insert vt, auto intro:detached_intro detached_elim)
+
 end
\ No newline at end of file