
diff -r 8ce9a432680b -r e6b13c7b9494 prio/PrioG.thy
--- a/prio/PrioG.thy	Mon Apr 23 08:01:37 2012 +0000
+++ b/prio/PrioG.thy	Mon Apr 30 15:32:34 2012 +0000
@@ -1114,7 +1114,7 @@
         apply (ind_cases "step s (Exit th')")
         apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def
                s_depend_def s_holding_def cs_holding_def)
-        by (fold wq_def, auto)
+        done
     next
       case (V th' cs')
       show ?thesis
@@ -1354,7 +1354,7 @@
   shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"
 proof -
   from assms show ?thesis
-  unfolding  holdents_def step_depend_p[OF vt] by auto
+  unfolding  holdents_test step_depend_p[OF vt] by (auto)
 qed
 
 lemma step_holdents_p_eq:
@@ -1364,7 +1364,7 @@
   shows "holdents (P th cs#s) th = holdents s th"
 proof -
   from assms show ?thesis
-  unfolding  holdents_def step_depend_p[OF vt] by auto
+  unfolding  holdents_test step_depend_p[OF vt] by auto
 qed
 
 
@@ -1386,7 +1386,7 @@
       ultimately have "x \<in> (\<lambda>(x, y). the_cs x) ` depend s" by simp 
     } thus ?thesis by auto
   qed
-  ultimately show ?thesis by (unfold holdents_def, auto intro:finite_subset)
+  ultimately show ?thesis by (unfold holdents_test, auto intro:finite_subset)
 qed
 
 lemma cntCS_v_dec: 
@@ -1396,12 +1396,12 @@
 proof -
   from step_back_step[OF vtv]
   have cs_in: "cs \<in> holdents s thread" 
-    apply (cases, unfold holdents_def s_depend_def, simp)
+    apply (cases, unfold holdents_test s_depend_def, simp)
     by (unfold cs_holding_def s_holding_def wq_def, auto)
   moreover have cs_not_in: 
     "(holdents (V thread cs#s) thread) = holdents s thread - {cs}"
     apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs])
-    apply (unfold holdents_def, unfold step_depend_v[OF vtv],
+    apply (unfold holdents_test, unfold step_depend_v[OF vtv],
             auto simp:next_th_def)
   proof -
     fix rest
@@ -1492,7 +1492,7 @@
         from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
         from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
         have eq_cncs: "cntCS (e#s) th = cntCS s th"
-          unfolding cntCS_def holdents_def
+          unfolding cntCS_def holdents_test
           by (simp add:depend_create_unchanged eq_e)
         { assume "th \<noteq> thread"
           with eq_readys eq_e
@@ -1517,7 +1517,7 @@
       from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
       from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
       have eq_cncs: "cntCS (e#s) th = cntCS s th"
-        unfolding cntCS_def holdents_def
+        unfolding cntCS_def holdents_test
         by (simp add:depend_exit_unchanged eq_e)
       { assume "th \<noteq> thread"
         with eq_e
@@ -1559,7 +1559,7 @@
             apply (erule_tac x = cs in allE, auto)
             by (case_tac "(wq_fun (schs s) cs)", auto)
           moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th"
-            apply (simp add:cntCS_def holdents_def)
+            apply (simp add:cntCS_def holdents_test)
             by (unfold  step_depend_p [OF vtp], auto)
           moreover from eq_e neq_th have "cntP (e # s) th = cntP s th"
             by (simp add:cntP_def count_def)
@@ -1594,7 +1594,7 @@
                   proof(rule card_insert)
                     from finite_holding [OF vt, of thread]
                     show " finite {cs. (Cs cs, Th thread) \<in> depend s}"
-                      by (unfold holdents_def, simp)
+                      by (unfold holdents_test, simp)
                   qed
                   moreover have "?R - {cs} = ?R"
                   proof -
@@ -1609,7 +1609,7 @@
                 qed
                 thus ?thesis
                   apply (unfold eq_e eq_th cntCS_def)
-                  apply (simp add: holdents_def)
+                  apply (simp add: holdents_test)
                   by (unfold step_depend_p [OF vtp], auto simp:True)
               qed
               moreover from is_runing have "th \<in> readys s"
@@ -1637,7 +1637,7 @@
               moreover from is_runing have "th \<in> threads (e#s)" 
                 by (unfold eq_e, auto simp:runing_def readys_def eq_th)
               moreover have "cntCS (e # s) th = cntCS s th"
-                apply (unfold cntCS_def holdents_def eq_e step_depend_p[OF vtp])
+                apply (unfold cntCS_def holdents_test eq_e step_depend_p[OF vtp])
                 by (auto simp:False)
               moreover note eq_cnp eq_cnv ih[of th]
               moreover from is_runing have "th \<in> readys s"
@@ -1734,7 +1734,7 @@
               apply (insert step_back_vt[OF vtv])
               by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto)
             moreover have "cntCS (e#s) th = cntCS s th"
-              apply (insert neq_th, unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto)
+              apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto)
               proof -
                 have "{csa. (Cs csa, Th th) \<in> depend s \<or> csa = cs \<and> next_th s thread cs th} =
                       {cs. (Cs cs, Th th) \<in> depend s}"
@@ -1796,7 +1796,7 @@
                 from eq_wq and  th_in and neq_hd
                 have "(holdents (e # s) th) = (holdents s th)"
                   apply (unfold eq_e step_depend_v[OF vtv], 
-                         auto simp:next_th_def eq_set s_depend_def holdents_def wq_def
+                         auto simp:next_th_def eq_set s_depend_def holdents_test wq_def
                                    Let_def cs_holding_def)
                   by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def)
                 thus ?thesis by (simp add:cntCS_def)
@@ -1861,7 +1861,7 @@
                 ultimately show ?thesis using ih by auto
               qed
               moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th"
-                apply (unfold cntCS_def holdents_def eq_e step_depend_v[OF vtv], auto)
+                apply (unfold cntCS_def holdents_test eq_e step_depend_v[OF vtv], auto)
               proof -
                 show "card {csa. (Cs csa, Th th) \<in> depend s \<or> csa = cs} =
                                Suc (card {cs. (Cs cs, Th th) \<in> depend s})"
@@ -1903,7 +1903,7 @@
         from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
         from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
         have eq_cncs: "cntCS (e#s) th = cntCS s th"
-          unfolding cntCS_def holdents_def
+          unfolding cntCS_def holdents_test
           by (simp add:depend_set_unchanged eq_e)
         from eq_e have eq_readys: "readys (e#s) = readys s" 
           by (simp add:readys_def cs_waiting_def s_waiting_def wq_def,
@@ -1930,7 +1930,7 @@
     case vt_nil
     show ?case 
       by (unfold cntP_def cntV_def cntCS_def, 
-        auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)
+        auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)
   qed
 qed
 
@@ -1953,7 +1953,7 @@
       assume eq_e: "e = Create thread prio"
         and not_in': "thread \<notin> threads s"
       have "cntCS (e # s) th = cntCS s th"
-        apply (unfold eq_e cntCS_def holdents_def)
+        apply (unfold eq_e cntCS_def holdents_test)
         by (simp add:depend_create_unchanged)
       moreover have "th \<notin> threads s" 
       proof -
@@ -1965,7 +1965,7 @@
       assume eq_e: "e = Exit thread"
       and nh: "holdents s thread = {}"
       have eq_cns: "cntCS (e # s) th = cntCS s th"
-        apply (unfold eq_e cntCS_def holdents_def)
+        apply (unfold eq_e cntCS_def holdents_test)
         by (simp add:depend_exit_unchanged)
       show ?thesis
       proof(cases "th = thread")
@@ -1991,7 +1991,7 @@
         ultimately show ?thesis by auto
       qed
       hence "cntCS (e # s) th  = cntCS s th "
-        apply (unfold cntCS_def holdents_def eq_e)
+        apply (unfold cntCS_def holdents_test eq_e)
         by (unfold step_depend_p[OF vtp], auto)
       moreover have "cntCS s th = 0"
       proof(rule ih)
@@ -2034,7 +2034,7 @@
       qed
       moreover note neq_th eq_wq
       ultimately have "cntCS (e # s) th  = cntCS s th"
-        by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto)
+        by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto)
       moreover have "cntCS s th = 0"
       proof(rule ih)
         from not_in eq_e show "th \<notin> threads s" by simp
@@ -2048,14 +2048,14 @@
       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_def)
+        apply (unfold eq_e cntCS_def holdents_test)
         by (simp add:depend_set_unchanged)
     qed
     next
       case vt_nil
       show ?case
       by (unfold cntCS_def, 
-        auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)
+        auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)
   qed
 qed
 
@@ -2425,10 +2425,10 @@
   moreover have "finite {cs. (Cs cs, Th th) \<in> depend s}"
   proof -
     from finite_holding[OF vt, of th] show ?thesis
-      by (simp add:holdents_def)
+      by (simp add:holdents_test)
   qed
   ultimately have h: "{cs. (Cs cs, Th th) \<in> depend s} = {}"
-    by (unfold cntCS_def holdents_def cs_dependents_def, auto)
+    by (unfold cntCS_def holdents_test cs_dependents_def, auto)
   show ?thesis
   proof(unfold cs_dependents_def)
     { assume "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<noteq> {}"
@@ -2773,10 +2773,20 @@
    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))"
+  where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"
+
 
-thm Field_def
+lemma detached_test:
+  shows "detached s th = (Th th \<notin> Field (depend s))"
+apply(simp add: detached_def Field_def)
+apply(simp add: s_depend_def)
+apply(simp add: s_holding_abv s_waiting_abv)
+apply(simp add: Domain_iff Range_iff)
+apply(simp add: wq_def)
+apply(auto)
+done
 
 lemma detached_intro:
   fixes s th
@@ -2796,7 +2806,7 @@
     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)
+      by (auto simp add: detached_def s_depend_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff)
   next
     assume "th \<in> readys s"
     moreover have "Th th \<notin> Range (depend s)"
@@ -2805,15 +2815,13 @@
       have "holdents s th = {}"
         by (simp add:cntCS_def)
       thus ?thesis
-        apply(auto simp:holdents_def)
+        apply(auto simp:holdents_test)
         apply(case_tac a)
-        apply(auto simp:holdents_def s_depend_def)
+        apply(auto simp:holdents_test s_depend_def)
         done
     qed
     ultimately show ?thesis
-      apply (auto simp:detached_def Field_def Domain_def readys_def)
-      apply (case_tac b, auto simp:s_depend_def)
-      by (erule_tac x = "nat" in allE, simp add: eq_waiting)
+      by (auto simp add: detached_def s_depend_def s_waiting_abv s_holding_abv wq_def readys_def)
   qed
 qed
 
@@ -2829,7 +2837,8 @@
   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)
+      unfolding detached_def holdents_test s_depend_def
+      by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff)
     thus ?thesis by (auto simp:cntCS_def)
   qed
   show ?thesis




