--- a/prio/PrioGDef.thy	Thu Feb 09 16:34:18 2012 +0000
+++ b/prio/PrioGDef.thy	Fri Feb 10 11:30:47 2012 +0000
@@ -110,7 +110,7 @@
   This explains the following definition:
   *}
 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
-  where "preced thread s = Prc (original_priority thread s) (birthtime thread s)"
+  where "preced thread s \<equiv> Prc (original_priority thread s) (birthtime thread s)"
 
 
 text {*
@@ -189,15 +189,25 @@
   @{text "th"}'s {\em current precedence} equals its original precedence, i.e. 
   @{text "preced th s"}.
   *}
-definition cpreced :: "state \<Rightarrow> (cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> precedence"
-  where "cpreced s wq = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))"
+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})"
+  unfolding cpreced_def image_def
+  apply(rule arg_cong)
+  back
+  by (auto)
 
 text {* \noindent
   The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}.
   It is the key function to model Priority Inheritance:
   *}
 fun schs :: "state \<Rightarrow> schedule_state"
-  where "schs [] = \<lparr>waiting_queue = \<lambda> cs. [],  cur_preced = cpreced [] (\<lambda> cs. [])\<rparr>" |
+  where 
+  "schs [] = (| waiting_queue = \<lambda> cs. [],  cur_preced = cpreced (\<lambda> cs. []) [] |)" |
+
   -- {*
   \begin{minipage}{0.9\textwidth}
   \begin{enumerate}
@@ -227,13 +237,13 @@
                   let pwq = waiting_queue ps in 
                   let pcp = cur_preced ps in
                   let nwq = case e of
-                             P thread cs \<Rightarrow>  pwq(cs:=(pwq cs @ [thread])) |
-                             V thread cs \<Rightarrow> let nq = case (pwq cs) of
+                             P th cs \<Rightarrow>  pwq(cs:=(pwq cs @ [th])) |
+                             V th cs \<Rightarrow> let nq = case (pwq cs) of
                                                       [] \<Rightarrow> [] | 
-                                                      (th'#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs)
+                                                      (_#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs)
                                             in pwq(cs:=nq)                 |
                               _ \<Rightarrow> pwq
-                  in let ncp = cpreced (e#s) nwq in 
+                  in let ncp = cpreced nwq (e#s) in 
                      \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>
                  )"