--- a/PrioG.thy	Thu Jun 12 10:14:50 2014 +0100
+++ b/PrioG.thy	Tue Jul 15 17:25:53 2014 +0200
@@ -1542,8 +1542,8 @@
           with eq_e
           have eq_readys: "(th \<in> readys (e#s)) = (th \<in> readys (s))"
             apply (simp add:readys_def s_waiting_def wq_def Let_def)
-            apply (rule_tac hh, clarify)
-            apply (intro iffI allI, clarify)
+            apply (rule_tac hh)
+             apply (intro iffI allI, clarify)
             apply (erule_tac x = csa in allE, auto)
             apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto)
             apply (erule_tac x = cs in allE, auto)
@@ -2069,6 +2069,7 @@
 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
 unfolding cp_def wq_def
 apply(induct s rule: schs.induct)
+thm cpreced_initial
 apply(simp add: Let_def cpreced_initial)
 apply(simp add: Let_def)
 apply(simp add: Let_def)
@@ -2088,12 +2089,17 @@
   shows "th1 = th2"
 proof -
   from runing_1 and runing_2 have "cp s th1 = cp s th2"
-    by (unfold runing_def, simp)
+    unfolding runing_def
+    apply(simp)
+    done
   hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) =
                  Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))"
     (is "Max (?f ` ?A) = Max (?f ` ?B)")
-    by (unfold cp_eq_cpreced cpreced_def)
+    thm cp_def image_Collect
+    unfolding cp_eq_cpreced 
+    unfolding cpreced_def .
   obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)"
+    thm Max_in
   proof -
     have h1: "finite (?f ` ?A)"
     proof -
@@ -2128,9 +2134,15 @@
       have "?A \<noteq> {}" by simp
       thus ?thesis by simp
     qed
+    thm Max_in
     from Max_in [OF h1 h2]
     have "Max (?f ` ?A) \<in> (?f ` ?A)" .
-    thus ?thesis by (auto intro:that)
+    thus ?thesis 
+      thm cpreced_def
+      unfolding cpreced_def[symmetric] 
+      unfolding cp_eq_cpreced[symmetric] 
+      unfolding cpreced_def 
+      using that[intro] by (auto)
   qed
   obtain th2' where th2_in: "th2' \<in> ?B" and eq_f_th2: "?f th2' = Max (?f ` ?B)"
   proof -
@@ -2273,6 +2285,8 @@
 apply(subgoal_tac "finite (runing s)")
 prefer 2
 apply (metis finite_nat_set_iff_bounded lessI runing_unique)
+apply(rule ccontr)
+apply(simp)
 apply(case_tac "Suc (Suc 0) \<le> card (runing s)")
 apply(subst (asm) card_le_Suc_iff)
 apply(simp)