
diff -r cab43c4a96d2 -r bc5bf9e9ada2 prio/PrioG.thy
--- a/prio/PrioG.thy	Sat Feb 11 09:14:14 2012 +0000
+++ b/prio/PrioG.thy	Sat Feb 11 09:34:46 2012 +0000
@@ -18,14 +18,14 @@
   proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits)
     fix thread s
     assume h1: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+"
-      and h2: "thread \<in> set (waiting_queue (schs s) cs)"
+      and h2: "thread \<in> set (wq_fun (schs s) cs)"
       and h3: "thread \<in> runing s"
     show "False" 
     proof -
-      from h3 have "\<And> cs. thread \<in>  set (waiting_queue (schs s) cs) \<Longrightarrow> 
-                             thread = hd ((waiting_queue (schs s) cs))" 
+      from h3 have "\<And> cs. thread \<in>  set (wq_fun (schs s) cs) \<Longrightarrow> 
+                             thread = hd ((wq_fun (schs s) cs))" 
         by (simp add:runing_def readys_def s_waiting_def wq_def)
-      from this [OF h2] have "thread = hd (waiting_queue (schs s) cs)" .
+      from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" .
       with h2
       have "(Cs cs, Th thread) \<in> (depend s)"
         by (simp add:s_depend_def s_holding_def wq_def cs_holding_def)
@@ -81,8 +81,8 @@
       apply (auto simp:wq_def Let_def split:if_splits)
     proof -
       fix q qs
-      assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"
-        and h2: "q # qs = waiting_queue (schs s) cs"
+      assume h1: "thread \<notin> set (wq_fun (schs s) cs)"
+        and h2: "q # qs = wq_fun (schs s) cs"
         and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
         and vt: "vt step (V th cs # s)"
       from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp
@@ -143,7 +143,7 @@
     fix th qs
     assume vt: "vt step (V th cs # s)"
       and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
-      and eq_wq: "waiting_queue (schs s) cs = thread # qs"
+      and eq_wq: "wq_fun (schs s) cs = thread # qs"
     show "False"
     proof -
       from wq_distinct[OF step_back_vt[OF vt], of cs]
@@ -193,7 +193,7 @@
 qed
 
 (* Wrong:
-    lemma \<lbrakk>thread \<in> set (waiting_queue cs1 s); thread \<in> set (waiting_queue cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
+    lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
 *)
 
 lemma waiting_unique_pre:
@@ -583,7 +583,7 @@
       fix a list
       assume t_in: "t \<in> set list"
         and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"
-        and eq_wq: "waiting_queue (schs s) cs = a # list"
+        and eq_wq: "wq_fun (schs s) cs = a # list"
       have " set (SOME q. distinct q \<and> set q = set list) = set list"
       proof(rule someI2)
         from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
@@ -597,7 +597,7 @@
       fix a list
       assume t_in: "t \<in> set list"
         and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"
-        and eq_wq: "waiting_queue (schs s) cs = a # list"
+        and eq_wq: "wq_fun (schs s) cs = a # list"
       have " set (SOME q. distinct q \<and> set q = set list) = set list"
       proof(rule someI2)
         from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
@@ -609,7 +609,7 @@
       with t_ni and t_in show "t = hd (SOME q. distinct q \<and> set q = set list)" by auto
     next
       fix a list
-      assume eq_wq: "waiting_queue (schs s) cs = a # list"
+      assume eq_wq: "wq_fun (schs s) cs = a # list"
       from step_back_step[OF vt]
       show "a = th"
       proof(cases)
@@ -641,7 +641,7 @@
     proof -
       fix list
       assume eq_wq[folded wq_def]: 
-        "waiting_queue (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list"
+        "wq_fun (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list"
       and hd_in: "hd (SOME q. distinct q \<and> set q = set list)
             \<in> set (SOME q. distinct q \<and> set q = set list)"
       have "set (SOME q. distinct q \<and> set q = set list) = set list"
@@ -670,7 +670,7 @@
 proof -
   fix rest
   assume vt: "vt step (V th cs # s)"
-    and eq_wq[folded wq_def]: " waiting_queue (schs s) cs = th # rest"
+    and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest"
     and nrest: "rest \<noteq> []"
     and ni: "hd (SOME q. distinct q \<and> set q = set rest)
             \<notin> set (SOME q. distinct q \<and> set q = set rest)"
@@ -693,7 +693,7 @@
   apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits)
   proof -
     fix a list
-    assume vt: "vt step (V th cs # s)" and eq_wq: "waiting_queue (schs s) cs = a # list"
+    assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
     from step_back_step [OF vt] show "a = th"
     proof(cases)
       assume "holding s th cs" with eq_wq
@@ -702,7 +702,7 @@
     qed
   next
     fix a list
-    assume vt: "vt step (V th cs # s)" and eq_wq: "waiting_queue (schs s) cs = a # list"
+    assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
     from step_back_step [OF vt] show "a = th"
     proof(cases)
       assume "holding s th cs" with eq_wq
@@ -733,7 +733,7 @@
       fix a list
       assume not_in: "t \<notin> set list"
         and is_in: "t \<in> set (SOME q. distinct q \<and> set q = set list)"
-        and eq_wq: "waiting_queue (schs s) cs = a # list"
+        and eq_wq: "wq_fun (schs s) cs = a # list"
       have "set (SOME q. distinct q \<and> set q = set list) = set list"
       proof(rule someI2)
         from wq_distinct [OF step_back_vt[OF vt], of cs]
@@ -747,7 +747,7 @@
     next
       fix list
       assume is_waiting: "waiting (wq (V th cs # s)) t cs"
-      and eq_wq: "waiting_queue (schs s) cs = t # list"
+      and eq_wq: "wq_fun (schs s) cs = t # list"
       hence "t \<in> set list"
         apply (unfold wq_def, auto simp:Let_def cs_waiting_def)
       proof -
@@ -1125,25 +1125,25 @@
         from h
         show ?thesis
         proof(unfold V wq_def)
-          assume th_in: "th \<in> set (waiting_queue (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l")
+          assume th_in: "th \<in> set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l")
           show "th \<in> threads (V th' cs' # s)"
           proof(cases "cs = cs'")
             case False
-            hence "?l = waiting_queue (schs s) cs" by (simp add:Let_def)
+            hence "?l = wq_fun (schs s) cs" by (simp add:Let_def)
             with th_in have " th \<in> set (wq s cs)" 
               by (fold wq_def, simp)
             from ih [OF this] show ?thesis by simp
           next
             case True
             show ?thesis
-            proof(cases "waiting_queue (schs s) cs'")
+            proof(cases "wq_fun (schs s) cs'")
               case Nil
               with h V show ?thesis
                 apply (auto simp:wq_def Let_def split:if_splits)
                 by (fold wq_def, drule_tac ih, simp)
             next
               case (Cons a rest)
-              assume eq_wq: "waiting_queue (schs s) cs' = a # rest"
+              assume eq_wq: "wq_fun (schs s) cs' = a # rest"
               with h V show ?thesis
                 apply (auto simp:Let_def wq_def split:if_splits)
               proof -
@@ -1156,10 +1156,10 @@
                   show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
                     by auto
                 qed
-                with eq_wq th_in have "th \<in> set (waiting_queue (schs s) cs')" by auto
+                with eq_wq th_in have "th \<in> set (wq_fun (schs s) cs')" by auto
                 from ih[OF this[folded wq_def]] show "th \<in> threads s" .
               next
-                assume th_in: "th \<in> set (waiting_queue (schs s) cs)"
+                assume th_in: "th \<in> set (wq_fun (schs s) cs)"
                 from ih[OF this[folded wq_def]]
                 show "th \<in> threads s" .
               qed
@@ -1210,7 +1210,7 @@
     proof -
       assume th_nin: "th \<notin> set rest"
         and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
-        and eq_wq: "waiting_queue (schs s) cs = thread # rest"
+        and eq_wq: "wq_fun (schs s) cs = thread # rest"
       have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
       proof(rule someI2)
         from wq_distinct[OF vt, of cs] and eq_wq[folded wq_def]
@@ -1550,9 +1550,9 @@
             apply (rule_tac hh, clarify)
             apply (intro iffI allI, clarify)
             apply (erule_tac x = csa in allE, auto)
-            apply (subgoal_tac "waiting_queue (schs s) cs \<noteq> []", auto)
+            apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto)
             apply (erule_tac x = cs in allE, auto)
-            by (case_tac "(waiting_queue (schs s) cs)", 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)
             by (unfold  step_depend_p [OF vtp], auto)
@@ -1807,7 +1807,7 @@
                 apply (auto simp:eq_e readys_def s_waiting_def wq_def
                         Let_def next_th_def)
               proof -
-                assume eq_wq: "waiting_queue (schs s) cs = thread # rest"
+                assume eq_wq: "wq_fun (schs s) cs = thread # rest"
                   and t_in: "?t \<in> set rest"
                 show "?t \<in> threads s"
                 proof(rule wq_threads[OF step_back_vt[OF vtv]])
@@ -1816,13 +1816,13 @@
                 qed
               next
                 fix csa
-                assume eq_wq: "waiting_queue (schs s) cs = thread # rest"
+                assume eq_wq: "wq_fun (schs s) cs = thread # rest"
                   and t_in: "?t \<in> set rest"
                   and neq_cs: "csa \<noteq> cs"
-                  and t_in': "?t \<in>  set (waiting_queue (schs s) csa)"
-                show "?t = hd (waiting_queue (schs s) csa)"
+                  and t_in': "?t \<in>  set (wq_fun (schs s) csa)"
+                show "?t = hd (wq_fun (schs s) csa)"
                 proof -
-                  { assume neq_hd': "?t \<noteq> hd (waiting_queue (schs s) csa)"
+                  { assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)"
                     from wq_distinct[OF step_back_vt[OF vtv], of cs] and 
                     eq_wq[folded wq_def] and t_in eq_wq
                     have "?t \<noteq> thread" by auto




