--- a/prio/PrioG.thy	Thu Feb 09 13:05:51 2012 +0000
+++ b/prio/PrioG.thy	Thu Feb 09 15:00:19 2012 +0000
@@ -789,8 +789,8 @@
   "vt step (P th cs#s) \<Longrightarrow>
   depend (P th cs # s) =  (if (wq s cs = []) then depend s \<union> {(Cs cs, Th th)}
                                              else depend s \<union> {(Th th, Cs cs)})"
-  apply(unfold s_depend_def wq_def)
-  apply (auto split:list.splits prod.splits simp:Let_def cs_waiting_def cs_holding_def)
+  apply(simp only: s_depend_def wq_def)
+  apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def)
   apply(case_tac "csa = cs", auto)
   apply(fold wq_def)
   apply(drule_tac step_back_step)

--- a/prio/PrioGDef.thy	Thu Feb 09 13:05:51 2012 +0000
+++ b/prio/PrioGDef.thy	Thu Feb 09 15:00:19 2012 +0000
@@ -258,15 +258,37 @@
   @{text "wq"}, but on system state @{text "s"}.
   *}
 defs (overloaded) 
+  s_holding_abv: 
+  "holding (s::state) \<equiv> holding (wq s)"
+  s_waiting_abv: 
+  "waiting (s::state) \<equiv> waiting (wq s)"
+  s_depend_abv: 
+  "depend (s::state) \<equiv> depend (wq s)"
+  s_dependents_abv: 
+  "dependents (s::state) th \<equiv> dependents (wq s) th"
+
+
+text {* 
+  The following lemma can be proved easily:
+  *}
+lemma
   s_holding_def: 
-  "holding (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))"
-  s_waiting_def: 
-  "waiting (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))"
-  s_depend_def: 
-  "depend (s::state) \<equiv> 
+  "holding (s::state) thread cs = (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))"
+  by (auto simp:s_holding_abv wq_def cs_holding_def)
+
+lemma s_waiting_def: 
+  "waiting (s::state) thread cs = (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))"
+  by (auto simp:s_waiting_abv wq_def cs_waiting_def)
+
+lemma s_depend_def: 
+  "depend (s::state) =
     {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}"
+  by (auto simp:s_depend_abv wq_def cs_depend_def)
+
+lemma
   s_dependents_def: 
   "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
+  by (auto simp:s_dependents_abv wq_def cs_dependents_def)
 
 text {*
   The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready} 
@@ -396,6 +418,7 @@
 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"
   where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"
 (*<*)
+
 end
 (*>*)
 

Binary file prio/paper.pdf has changed