--- a/prio/PrioGDef.thy	Fri Feb 10 11:30:47 2012 +0000
+++ b/prio/PrioGDef.thy	Fri Feb 10 21:01:03 2012 +0000
@@ -192,13 +192,27 @@
 definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
   where "cpreced wq s = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))"
 
+(*<*)
 lemma 
   cpreced_def2:
-  "cpreced wq s th = Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})"
+  "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})"
   unfolding cpreced_def image_def
+  apply(rule eq_reflection)
   apply(rule arg_cong)
   back
   by (auto)
+(*>*)
+
+abbreviation
+  "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
+
+abbreviation 
+  "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"
+ 
+abbreviation
+  "release qs \<equiv> case qs of
+             [] => [] 
+          |  (_#qs) => (SOME q. distinct q \<and> set q = set qs)"
 
 text {* \noindent
   The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}.
@@ -206,14 +220,14 @@
   *}
 fun schs :: "state \<Rightarrow> schedule_state"
   where 
-  "schs [] = (| waiting_queue = \<lambda> cs. [],  cur_preced = cpreced (\<lambda> cs. []) [] |)" |
+  "schs [] = (| waiting_queue = \<lambda> cs. [],  cur_preced = (\<lambda>_. Prc 0 0) |)" |
 
   -- {*
   \begin{minipage}{0.9\textwidth}
   \begin{enumerate}
   \item @{text "ps"} is the schedule state of last moment.
   \item @{text "pwq"} is the waiting queue function of last moment.
-  \item @{text "pcp"} is the precedence function of last moment. 
+  \item @{text "pcp"} is the precedence function of last moment (NOT USED). 
   \item @{text "nwq"} is the new waiting queue function. It is calculated using a @{text "case"} statement:
   \begin{enumerate}
       \item If the happening event is @{text "P thread cs"}, @{text "thread"} is added to 
@@ -233,9 +247,34 @@
   \end{enumerate}
   \end{minipage}
      *}
-   "schs (e#s) = (let ps = schs s in 
+   "schs (Create th prio # s) = 
+       (let wq = waiting_queue (schs s) in
+          (|waiting_queue = wq, cur_preced = 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)|))"
+|  "schs (Set th prio # s) = 
+       (let wq = waiting_queue (schs s) in
+          (|waiting_queue = wq, cur_preced = cpreced wq (Set th prio # s)|))"
+|  "schs (P th cs # s) = 
+       (let wq = waiting_queue (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)|))"
+|  "schs (V th cs # s) = 
+       (let wq = waiting_queue (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)|))"
+
+lemma cpreced_initial: 
+  "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
+apply(simp add: cpreced_def)
+apply(simp add: cs_dependents_def cs_depend_def cs_waiting_def cs_holding_def)
+apply(simp add: preced_def)
+done
+
+lemma sch_old_def:
+  "schs (e#s) = (let ps = schs s in 
                   let pwq = waiting_queue ps in 
-                  let pcp = cur_preced 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
@@ -246,6 +285,10 @@
                   in let ncp = cpreced nwq (e#s) in 
                      \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>
                  )"
+apply(cases e)
+apply(simp_all)
+done
+
 
 text {* 
   \noindent