diff -r 440382eb6427 -r 64c9f151acf5 prio/PrioGDef.thy
--- 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
 (*>*)