--- a/PIPBasics.thy	Thu Sep 21 14:33:13 2017 +0100
+++ b/PIPBasics.thy	Fri Sep 22 03:08:30 2017 +0100
@@ -173,7 +173,7 @@
 lemma last_set_unique: 
   "\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>
           \<Longrightarrow> th1 = th2"
-  apply (induct s, auto)
+  apply (induct s, auto)  
   by (case_tac a, auto split:if_splits dest:last_set_lt)
 
 lemma preced_unique : 
@@ -1052,7 +1052,7 @@
 
 lemma wq_kept [simp]:
   shows "wq (e#s) cs' = wq s cs'"
-    using assms unfolding is_create wq_def
+  unfolding is_create wq_def
   by (auto simp:Let_def)
 
 lemma wq_distinct_kept:
@@ -1066,7 +1066,7 @@
 
 lemma wq_kept [simp]:
   shows "wq (e#s) cs' = wq s cs'"
-    using assms unfolding is_exit wq_def
+  unfolding is_exit wq_def
   by (auto simp:Let_def)
 
 lemma wq_distinct_kept:
@@ -1171,7 +1171,7 @@
 
 lemma wq_kept [simp]:
   shows "wq (e#s) cs' = wq s cs'"
-    using assms unfolding is_set wq_def
+  unfolding is_set wq_def
   by (auto simp:Let_def)
 
 lemma wq_distinct_kept:
@@ -3720,7 +3720,6 @@
 
 lemma KK:
   shows "(\<Union>x\<in>C. B x) = (\<Union> {B x |x. x \<in> C})"
-(*  and "\<Union>" *)
 by (simp_all add: Setcompr_eq_image)
 
 lemma Max_Segments: 
@@ -3731,7 +3730,7 @@
 apply(subst Max_Union)
 apply(auto)[3]
 apply(simp add: Setcompr_eq_image)
-apply(simp add: image_eq_UN)
+apply(auto simp add: image_image)
 done 
 
 lemma max_cp_readys_max_preced_tG:
@@ -4570,7 +4569,7 @@
 
 lemma readys_simp [simp]:
   shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
-  using readys_kept1[OF assms] readys_kept2[OF assms]
+  using readys_kept1 readys_kept2
   by metis
 
 lemma cnp_cnv_cncs_kept:
@@ -5109,7 +5108,9 @@
   assumes eq_pv: "cntP s th = cntV s th"
   shows "subtree (RAG s) (Th th) = {Th th}"
   using eq_pv_children[OF assms]
-    by (unfold subtree_children, simp)
+  apply(subst subtree_children)
+  apply(simp)
+  done  
 
 lemma count_eq_RAG_plus:
   assumes "cntP s th = cntV s th"
@@ -5320,7 +5321,11 @@
 proof(cases "children (tRAG s) x = {}")
   case True
   show ?thesis
-    by (unfold True cp_gen_def subtree_children, simp add:assms)
+    apply(subst True)
+    apply(subst cp_gen_def)
+    apply(subst subtree_children)
+    apply(simp add: assms)
+    using True assms by auto  
 next
   case False
   hence [simp]: "children (tRAG s) x \<noteq> {}" by auto
@@ -5349,9 +5354,10 @@
     proof -
       have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp
       also have "... =  (\<Union> x \<in> ?B. ?f ` (?g x))" by auto
-      finally have "Max ?L1 = Max ..." by simp
+      finally have "Max ?L1 = Max ..." 
+        by (simp add: \<open>(the_preced s \<circ> the_thread) ` (\<Union>x\<in>children (tRAG s) x. subtree (tRAG s) x) = (\<Union>x\<in>children (tRAG s) x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x)\<close>) 
       also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)"
-        by (subst Max_UNION, simp+)
+        by(subst Max_Union, auto)
       also have "... = Max (cp_gen s ` children (tRAG s) x)"
           by (unfold image_comp cp_gen_alt_def, simp)
       finally show ?thesis .
@@ -5486,16 +5492,15 @@
       have "?R = length (actions_of {actor e} (e # t)) +
                  (\<Sum>th'\<in>A - {actor e}. length (actions_of {th'} (e # t)))"
             (is "_ = ?F (e#t) + ?G (e#t)")
-            by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", 
-                OF assms True], simp)
+            by (meson True assms sum.remove)      
       moreover have "?F (e#t) = 1 + ?F t" using True
           by  (simp add:actions_of_def)
-      moreover have "?G (e#t) = ?G t"
-        by (rule setsum.cong, auto simp:actions_of_def)
+        moreover have "?G (e#t) = ?G t"
+        by (auto simp:actions_of_def) 
       moreover have "?F t + ?G t = ?T t"
-        by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", 
-              OF assms True], simp)
-      ultimately show ?thesis by simp
+        by (metis (no_types, lifting) True assms sum.remove) 
+      ultimately show ?thesis 
+        by simp
     qed
     ultimately show ?thesis by simp
   next
@@ -5504,7 +5509,8 @@
       by (simp add:actions_of_def)
     also have "... = (\<Sum>th'\<in>A. length (actions_of {th'} t))" by (simp add: h)
     also have "... = ?R"
-      by (rule setsum.cong; insert False, auto simp:actions_of_def)
+      unfolding actions_of_def
+      by (metis (no_types, lifting) False filter.simps(2) singletonD sum.cong) 
     finally show ?thesis .
   qed
 qed (auto simp:actions_of_def)