--- 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