--- a/PIPBasics.thy	Fri Oct 07 21:15:35 2016 +0100
+++ b/PIPBasics.thy	Fri Oct 21 14:47:01 2016 +0100
@@ -33,76 +33,7 @@
    by (rule image_subsetI, auto intro:h[symmetric])
 qed
 
-lemma Max_fg_mono:
-  assumes "finite A"
-  and "\<forall> a \<in> A. f a \<le> g a"
-  shows "Max (f ` A) \<le> Max (g ` A)"
-proof(cases "A = {}")
-  case True
-  thus ?thesis by auto
-next
-  case False
-  show ?thesis
-  proof(rule Max.boundedI)
-    from assms show "finite (f ` A)" by auto
-  next
-    from False show "f ` A \<noteq> {}" by auto
-  next
-    fix fa
-    assume "fa \<in> f ` A"
-    then obtain a where h_fa: "a \<in> A" "fa = f a" by auto
-    show "fa \<le> Max (g ` A)"
-    proof(rule Max_ge_iff[THEN iffD2])
-      from assms show "finite (g ` A)" by auto
-    next
-      from False show "g ` A \<noteq> {}" by auto
-    next
-      from h_fa have "g a \<in> g ` A" by auto
-      moreover have "fa \<le> g a" using h_fa assms(2) by auto
-      ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto
-    qed
-  qed
-qed 
-
-lemma Max_f_mono:
-  assumes seq: "A \<subseteq> B"
-  and np: "A \<noteq> {}"
-  and fnt: "finite B"
-  shows "Max (f ` A) \<le> Max (f ` B)"
-proof(rule Max_mono)
-  from seq show "f ` A \<subseteq> f ` B" by auto
-next
-  from np show "f ` A \<noteq> {}" by auto
-next
-  from fnt and seq show "finite (f ` B)" by auto
-qed
-
-lemma Max_UNION: 
-  assumes "finite A"
-  and "A \<noteq> {}"
-  and "\<forall> M \<in> f ` A. finite M"
-  and "\<forall> M \<in> f ` A. M \<noteq> {}"
-  shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R")
-  using assms[simp]
-proof -
-  have "?L = Max (\<Union>(f ` A))"
-    by (fold Union_image_eq, simp)
-  also have "... = ?R"
-    by (subst Max_Union, simp+)
-  finally show ?thesis .
-qed
-
-lemma max_Max_eq:
-  assumes "finite A"
-    and "A \<noteq> {}"
-    and "x = y"
-  shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R")
-proof -
-  have "?R = Max (insert y A)" by simp
-  also from assms have "... = ?L"
-      by (subst Max.insert, simp+)
-  finally show ?thesis by simp
-qed
+
 
 section {* Lemmas do not depend on trace validity *}
 
@@ -3821,46 +3752,68 @@
   over the union of subtrees, the following equation can be derived:
 *}
 
-thm the_preced_def cpreceds_def
+
+lemma cp_alt_def3:
+  shows "cp s th = Max (preceds (subtree (tG s) th) s)"
+unfolding cp_alt_def2
+unfolding image_def
+unfolding the_preced_def
+by meson
+
+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: 
+  assumes "finite C" "\<forall>x\<in> C. finite (B x)" "\<forall>x\<in> C. B x \<noteq> {}" "{B x |x. x \<in> C} \<noteq> {}" 
+  shows "Max (\<Union>x \<in> C. B x) = Max {Max (B x) | x. x \<in> C}"
+using assms
+apply(subst KK(1))
+apply(subst Max_Union)
+apply(auto)[3]
+apply(simp add: Setcompr_eq_image)
+apply(simp add: image_eq_UN)
+done 
 
 lemma max_cp_readys_max_preced_tG:
-  shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R")
+  shows "Max (cp s ` readys s) = Max (preceds (threads s) s)" (is "?L = ?R")
 proof(cases "readys s = {}")
   case False
-  have "?R = 
-    Max (the_preced s ` (\<Union>th\<in>readys s. subtree (tG s) th))"
-    by (simp add: threads_alt_def1)  
-  also have "... = Max (\<Union>x\<in>readys s. the_preced s ` subtree (tG s) x) "
-    by (unfold image_UN, simp)
-  also have "... = Max (Max ` (\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s)" 
-  proof(rule Max_UNION)
-    show "\<forall>M\<in>(\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s. finite M"
-      using fsbttGs.finite_subtree by auto
-  qed (auto simp:False subtree_def finite_readys)
-  also have "... = Max ((Max \<circ> (\<lambda>x. the_preced s ` subtree (tG s) x)) ` readys s)"
-    by (simp add: image_comp)
-  also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
-  proof -
-    have "(?f ` ?A) = (?g ` ?A)"
-    proof(rule f_image_eq)
-      fix th1 
-      assume "th1 \<in> ?A"
-      thus "?f th1 = ?g th1"
-        by (unfold cp_alt_def2, simp)
-    qed
-    thus ?thesis by simp
-  qed
-  finally show ?thesis by simp
+  have "Max (preceds (threads s) s) = Max (preceds (\<Union>th\<in>readys s. subtree (tG s) th) s)"
+    unfolding threads_alt_def1 by simp
+  also have "... = Max {Max (preceds (subtree (tG s) th) s) | th. th \<in> readys s}"
+    apply(subst Max_Segments[symmetric])
+    prefer 5  
+    apply(rule arg_cong)
+    back
+    apply(blast)
+    apply (simp add: finite_readys)
+    apply (simp add: fsbttGs.finite_subtree)
+    apply blast
+    using False by blast
+  also have "... = Max {cp s th | th. th \<in> readys s}"
+    unfolding cp_alt_def3 ..
+  finally show "Max (cp s ` readys s) = Max (preceds (threads s) s)"
+   by (simp add: Setcompr_eq_image image_def) 
 qed (auto simp:threads_alt_def)
 
 
+lemma LL:
+shows "the_preced s ` threads s = preceds (threads s) s"
+using the_preced_def by auto
+
+
 text {*
   The following lemma is simply a corollary of @{thm max_cp_readys_max_preced_tG}
   and @{thm max_cp_eq}:
 *}
 lemma max_cp_readys_threads:
   shows "Max (cp s ` readys s) = Max (cp s ` threads s)" 
-    using max_cp_readys_max_preced_tG max_cp_eq by auto
+    apply(simp add: max_cp_readys_max_preced_tG)
+    apply(simp add: max_cp_eq)
+    apply(simp add: LL)
+    done
 
 end