--- a/prio/PrioG.thy	Mon Feb 13 04:22:52 2012 +0000
+++ b/prio/PrioG.thy	Mon Feb 13 05:41:53 2012 +0000
@@ -2,8 +2,15 @@
 imports PrioGDef 
 begin
 
-lemma runing_ready: "runing s \<subseteq> readys s"
-  by (auto simp only:runing_def readys_def)
+lemma runing_ready: 
+  shows "runing s \<subseteq> readys s"
+  unfolding runing_def readys_def
+  by auto 
+
+lemma readys_threads:
+  shows "readys s \<subseteq> threads s"
+  unfolding readys_def
+  by auto
 
 lemma wq_v_neq:
    "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
@@ -354,22 +361,20 @@
   and "waiting s th cs1"
   and "waiting s th cs2"
   shows "cs1 = cs2"
-proof -
-  from waiting_unique_pre and prems
-  show ?thesis
-    by (auto simp add: wq_def s_waiting_def)
-qed
+using waiting_unique_pre prems
+unfolding wq_def s_waiting_def
+by auto
 
+(* not used *)
 lemma held_unique:
-  assumes "vt s"
-  and "holding s th1 cs"
+  fixes s::"state"
+  assumes "holding s th1 cs"
   and "holding s th2 cs"
   shows "th1 = th2"
-proof -
-  from prems show ?thesis
-    unfolding s_holding_def
-    by auto
-qed
+using prems
+unfolding s_holding_def
+by auto
+
 
 lemma birthtime_lt: "th \<in> threads s \<Longrightarrow> birthtime th s < length s"
   apply (induct s, auto)
@@ -2468,42 +2473,8 @@
 lemma finite_threads:
   assumes vt: "vt s"
   shows "finite (threads s)"
-proof -
-  from vt show ?thesis
-  proof(induct)
-    case (vt_cons s e)
-    assume vt: "vt s"
-    and step: "step s e"
-    and ih: "finite (threads s)"
-    from step
-    show ?case
-    proof(cases)
-      case (thread_create thread prio)
-      assume eq_e: "e = Create thread prio"
-      with ih
-      show ?thesis by (unfold eq_e, auto)
-    next
-      case (thread_exit thread)
-      assume eq_e: "e = Exit thread"
-      with ih show ?thesis 
-        by (unfold eq_e, auto)
-    next
-      case (thread_P thread cs)
-      assume eq_e: "e = P thread cs"
-      with ih show ?thesis by (unfold eq_e, auto)
-    next
-      case (thread_V thread cs)
-      assume eq_e: "e = V thread cs"
-      with ih show ?thesis by (unfold eq_e, auto)
-    next 
-      case (thread_set thread prio)
-      from vt_cons thread_set show ?thesis by simp
-    qed
-  next
-    case vt_nil
-    show ?case by (auto)
-  qed
-qed
+using vt
+by (induct) (auto elim: step.cases)
 
 lemma Max_f_mono:
   assumes seq: "A \<subseteq> B"
@@ -2785,14 +2756,6 @@
   show ?thesis by (rule max_cp_readys_threads_pre[OF vt False])
 qed
 
-lemma readys_threads:
-  shows "readys s \<subseteq> threads s"
-proof
-  fix th
-  assume "th \<in> readys s"
-  thus "th \<in> threads s"
-    by (unfold readys_def, auto)
-qed
 
 lemma eq_holding: "holding (wq s) th cs = holding s th cs"
   apply (unfold s_holding_def cs_holding_def wq_def, simp)