# HG changeset patch
# User urbanc
# Date 1328952886 0
# Node ID bc5bf9e9ada2c72728c6d0a1ea39640377ccbeea
# Parent  cab43c4a96d2fb95f4dd9c0b8a9836d0b3773e27
renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun

diff -r cab43c4a96d2 -r bc5bf9e9ada2 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Sat Feb 11 09:14:14 2012 +0000
+++ b/prio/Paper/Paper.thy	Sat Feb 11 09:34:46 2012 +0000
@@ -23,8 +23,6 @@
   preced ("prec") and
   cpreced ("cprec") and
   dependents ("dependants") and
-  waiting_queue ("wq_fun") and
-  cur_preced ("cprec_fun") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 (*>*)
 
@@ -362,13 +360,16 @@
   @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
   \end{isabelle}
 
+  \noindent
+  We have the usual getter and setter methods for such records.
+
   In the initial state, the scheduler starts with all resources unlocked and the
   precedence of every thread is initialised with @{term "Prc 0 0"}. 
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\ 
-  \hspace{5mm}@{term "(|waiting_queue = all_unlocked, cur_preced = (\<lambda>_::thread. Prc 0 0)|)"}
+  \hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"}
   \end{tabular}
   \end{isabelle}
 
@@ -382,14 +383,14 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\ 
-  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
-  \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Create th prio # s)|)"}\\
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\\
   @{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\
-  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
-  \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
   @{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\ 
-  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
-  \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Set th prio # s)|)"}
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"}
   \end{tabular}
   \end{isabelle}
 
@@ -403,9 +404,9 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\ 
-  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
   \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\
-  \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|)"}
+  \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"}
   \end{tabular}
   \end{isabelle}
 
@@ -423,9 +424,9 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
-  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
   \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
-  \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|)"}
+  \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
   \end{tabular}
   \end{isabelle}
 
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
diff -r cab43c4a96d2 -r bc5bf9e9ada2 prio/PrioGDef.thy
--- a/prio/PrioGDef.thy	Sat Feb 11 09:14:14 2012 +0000
+++ b/prio/PrioGDef.thy	Sat Feb 11 09:34:46 2012 +0000
@@ -176,8 +176,8 @@
   threads:
   *}
 record schedule_state = 
-    waiting_queue :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
-    cur_preced :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
+    wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
+    cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
 
 text {* \noindent 
   The following
@@ -220,7 +220,7 @@
   *}
 fun schs :: "state \<Rightarrow> schedule_state"
   where 
-  "schs [] = (| waiting_queue = \<lambda> cs. [],  cur_preced = (\<lambda>_. Prc 0 0) |)" |
+  "schs [] = (| wq_fun = \<lambda> cs. [],  cprec_fun = (\<lambda>_. Prc 0 0) |)" |
 
   -- {*
   \begin{minipage}{0.9\textwidth}
@@ -248,22 +248,22 @@
   \end{minipage}
      *}
    "schs (Create th prio # s) = 
-       (let wq = waiting_queue (schs s) in
-          (|waiting_queue = wq, cur_preced = cpreced wq (Create th prio # s)|))"
+       (let wq = wq_fun (schs s) in
+          (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"
 |  "schs (Exit th # s) = 
-       (let wq = waiting_queue (schs s) in
-          (|waiting_queue = wq, cur_preced = cpreced wq (Exit th # s)|))"
+       (let wq = wq_fun (schs s) in
+          (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"
 |  "schs (Set th prio # s) = 
-       (let wq = waiting_queue (schs s) in
-          (|waiting_queue = wq, cur_preced = cpreced wq (Set th prio # s)|))"
+       (let wq = wq_fun (schs s) in
+          (|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))"
 |  "schs (P th cs # s) = 
-       (let wq = waiting_queue (schs s) in
+       (let wq = wq_fun (schs s) in
         let new_wq = wq(cs := (wq cs @ [th])) in
-          (|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|))"
+          (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))"
 |  "schs (V th cs # s) = 
-       (let wq = waiting_queue (schs s) in
+       (let wq = wq_fun (schs s) in
         let new_wq = wq(cs := release (wq cs)) in
-          (|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|))"
+          (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"
 
 lemma cpreced_initial: 
   "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
@@ -274,7 +274,7 @@
 
 lemma sch_old_def:
   "schs (e#s) = (let ps = schs s in 
-                  let pwq = waiting_queue ps in 
+                  let pwq = wq_fun ps in 
                   let nwq = case e of
                              P th cs \<Rightarrow>  pwq(cs:=(pwq cs @ [th])) |
                              V th cs \<Rightarrow> let nq = case (pwq cs) of
@@ -283,7 +283,7 @@
                                             in pwq(cs:=nq)                 |
                               _ \<Rightarrow> pwq
                   in let ncp = cpreced nwq (e#s) in 
-                     \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>
+                     \<lparr>wq_fun = nwq, cprec_fun = ncp\<rparr>
                  )"
 apply(cases e)
 apply(simp_all)
@@ -292,16 +292,16 @@
 
 text {* 
   \noindent
-  The following @{text "wq"} is a shorthand for @{text "waiting_queue"}. 
+  The following @{text "wq"} is a shorthand for @{text "wq_fun"}. 
   *}
 definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" 
-  where "wq s = waiting_queue (schs s)"
+  where "wq s = wq_fun (schs s)"
 
 text {* \noindent 
-  The following @{text "cp"} is a shorthand for @{text "cur_preced"}. 
+  The following @{text "cp"} is a shorthand for @{text "cprec_fun"}. 
   *}
 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
-  where "cp s = cur_preced (schs s)"
+  where "cp s = cprec_fun (schs s)"
 
 text {* \noindent
   Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and 
diff -r cab43c4a96d2 -r bc5bf9e9ada2 prio/paper.pdf
Binary file prio/paper.pdf has changed