# HG changeset patch
# User haftmann
# Date 1547490903 0
# Node ID a03a63b81f446eafc88b91b29cf6eeed4a080dd9
# Parent  2bc2a85993693dcc98e5fdf7f20324c9ce77de9d
tuned proofs

diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1713,7 +1713,7 @@
   unfolding quotient_map_def
 proof (intro conjI allI impI)
   show "(g \<circ> f) ` topspace X = topspace X''"
-    using assms image_comp unfolding quotient_map_def by force
+    using assms by (simp only: image_comp [symmetric]) (simp add: quotient_map_def)
 next
   fix U''
   assume "U'' \<subseteq> topspace X''"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -107,18 +107,45 @@
 qed
 
 lemma retraction:
-   "retraction S T r \<longleftrightarrow>
+  "retraction S T r \<longleftrightarrow>
     T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
-by (force simp: retraction_def)
+  by (force simp: retraction_def)
+
+lemma retractionE: \<comment> \<open>yields properties normalized wrt. simp – less likely to loop\<close>
+  assumes "retraction S T r"
+  obtains "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
+proof (rule that)
+  from retraction [of S T r] assms
+  have "T \<subseteq> S" "continuous_on S r" "r ` S = T" and "\<forall>x \<in> T. r x = x"
+    by simp_all
+  then show "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r"
+    by simp_all
+  from \<open>\<forall>x \<in> T. r x = x\<close> have "r x = x" if "x \<in> T" for x
+    using that by simp
+  with \<open>r ` S = T\<close> show "r (r x) = r x" if "x \<in> S" for x
+    using that by auto
+qed
+
+lemma retract_ofE: \<comment> \<open>yields properties normalized wrt. simp – less likely to loop\<close>
+  assumes "T retract_of S"
+  obtains r where "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
+proof -
+  from assms obtain r where "retraction S T r"
+    by (auto simp add: retract_of_def)
+  with that show thesis
+    by (auto elim: retractionE)
+qed
 
 lemma retract_of_imp_extensible:
   assumes "S retract_of T" and "continuous_on S f" and "f ` S \<subseteq> U"
   obtains g where "continuous_on T g" "g ` T \<subseteq> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-using assms
-apply (clarsimp simp add: retract_of_def retraction)
-apply (rule_tac g = "f \<circ> r" in that)
-apply (auto simp: continuous_on_compose2)
-done
+proof -
+  from \<open>S retract_of T\<close> obtain r where "retraction T S r"
+    by (auto simp add: retract_of_def)
+  show thesis
+    by (rule that [of "f \<circ> r"])
+      (use \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> U\<close> \<open>retraction T S r\<close> in \<open>auto simp: continuous_on_compose2 retraction\<close>)
+qed
 
 lemma idempotent_imp_retraction:
   assumes "continuous_on S f" and "f ` S \<subseteq> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x"
@@ -259,14 +286,12 @@
 qed
 
 lemma retraction_imp_quotient_map:
-   "retraction S T r
-    \<Longrightarrow> U \<subseteq> T
-            \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> r -` U) \<longleftrightarrow>
-                 openin (subtopology euclidean T) U)"
-apply (clarsimp simp add: retraction)
-apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
-apply (auto simp: elim: continuous_on_subset)
-done
+  "openin (subtopology euclidean S) (S \<inter> r -` U) \<longleftrightarrow> openin (subtopology euclidean T) U"
+  if retraction: "retraction S T r" and "U \<subseteq> T"
+  using retraction apply (rule retractionE)
+  apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
+  using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset)
+  done
 
 lemma retract_of_locally_compact:
     fixes S :: "'a :: {heine_borel,real_normed_vector} set"
@@ -292,15 +317,15 @@
 
 lemma retract_of_locally_connected:
   assumes "locally connected T" "S retract_of T"
-    shows "locally connected S"
+  shows "locally connected S"
   using assms
-  by (auto simp: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_connected_quotient_image)
+  by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_connected_quotient_image retract_ofE)
 
 lemma retract_of_locally_path_connected:
   assumes "locally path_connected T" "S retract_of T"
-    shows "locally path_connected S"
+  shows "locally path_connected S"
   using assms
-  by (auto simp: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image)
+  by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image retract_ofE)
 
 text \<open>A few simple lemmas about deformation retracts\<close>
 
@@ -1741,7 +1766,7 @@
 lemma swap_image:
   "Fun.swap i j f ` A = (if i \<in> A then (if j \<in> A then f ` A else f ` ((A - {i}) \<union> {j}))
                                   else (if j \<in> A then f ` ((A - {j}) \<union> {i}) else f ` A))"
-  by (auto simp: swap_def image_def) metis
+  by (auto simp: swap_def cong: image_cong_simp)
 
 lemmas swap_apply1 = swap_apply(1)
 lemmas swap_apply2 = swap_apply(2)
@@ -2273,16 +2298,18 @@
       have "\<And>i. Suc ` {..< i} = {..< Suc i} - {0}"
         by (auto simp: image_iff Ball_def) arith
       then have upd_Suc: "\<And>i. i \<le> n \<Longrightarrow> (upd\<circ>Suc) ` {..< i} = upd ` {..< Suc i} - {n}"
-        using \<open>upd 0 = n\<close> upd_inj
-        by (auto simp: image_comp[symmetric] inj_on_image_set_diff[OF inj_upd])
+        using \<open>upd 0 = n\<close> upd_inj by (auto simp add: image_iff less_Suc_eq_0_disj)
       have n_in_upd: "\<And>i. n \<in> upd ` {..< Suc i}"
         using \<open>upd 0 = n\<close> by auto
 
       define f' where "f' i j =
         (if j \<in> (upd\<circ>Suc)`{..< i} then Suc ((base(n := p)) j) else (base(n := p)) j)" for i j
-      { fix x i assume i[arith]: "i \<le> n" then have "enum (Suc i) x = f' i x"
-          unfolding f'_def enum_def using \<open>a n < p\<close> \<open>a = enum 0\<close> \<open>upd 0 = n\<close> \<open>a n = p - 1\<close>
-          by (simp add: upd_Suc enum_0 n_in_upd) }
+      { fix x i
+        assume i [arith]: "i \<le> n"
+        with upd_Suc have "(upd \<circ> Suc) ` {..<i} = upd ` {..<Suc i} - {n}" .
+        with \<open>a n < p\<close> \<open>a = enum 0\<close> \<open>upd 0 = n\<close> \<open>a n = p - 1\<close>
+        have "enum (Suc i) x = f' i x"
+          by (auto simp add: f'_def enum_def)  }
       then show "s - {a} = f' ` {.. n}"
         unfolding s_eq image_comp by (intro image_cong) auto
     qed
@@ -2435,14 +2462,14 @@
     have b_enum: "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
     with b.inj_enum have inj_f': "inj_on f' {.. n}" by simp
 
-    have [simp]: "\<And>j. j < n \<Longrightarrow> rot ` {..< j} = {0 <..< Suc j}"
-      by (auto simp: rot_def image_iff Ball_def)
-         arith
-
-    { fix j assume j: "j < n"
-      from j \<open>n \<noteq> 0\<close> have "f' j = enum (Suc j)"
-        by (auto simp: f'_def enum_def upd_inj in_upd_image image_comp[symmetric] fun_eq_iff) }
-    note f'_eq_enum = this
+    have f'_eq_enum: "f' j = enum (Suc j)" if "j < n" for j
+    proof -
+      from that have "rot ` {..< j} = {0 <..< Suc j}"
+        by (auto simp: rot_def image_Suc_lessThan cong: image_cong_simp)
+      with that \<open>n \<noteq> 0\<close> show ?thesis
+        by (simp only: f'_def enum_def fun_eq_iff image_comp [symmetric])
+          (auto simp add: upd_inj)
+    qed
     then have "enum ` Suc ` {..< n} = f' ` {..< n}"
       by (force simp: enum_inj)
     also have "Suc ` {..< n} = {.. n} - {0}"
@@ -3021,7 +3048,7 @@
   have "odd (card ?A)"
     using assms by (intro kuhn_combinatorial[of p n label]) auto
   then have "?A \<noteq> {}"
-    by fastforce
+    by (rule odd_card_imp_not_empty)
   then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}"
     by (auto elim: ksimplex.cases)
   interpret kuhn_simplex p n b u s by fact
@@ -3642,7 +3669,7 @@
       proof -
         have "k \<noteq> 0" "a + k *\<^sub>R x \<in> closure S"
           using k closure_translation [of "-a"]
-          by (auto simp: rel_frontier_def)
+          by (auto simp: rel_frontier_def cong: image_cong_simp)
         then have segsub: "open_segment a (a + k *\<^sub>R x) \<subseteq> rel_interior S"
           by (metis rel_interior_closure_convex_segment [OF \<open>convex S\<close> arelS])
         have "x \<noteq> 0" and xaffS: "a + x \<in> affine hull S"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Caratheodory.thy
--- a/src/HOL/Analysis/Caratheodory.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Caratheodory.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -664,7 +664,7 @@
     then have "disjoint_family F"
       using F'_disj by (auto simp: disjoint_family_on_def)
     moreover from F' have "(\<Union>i. F i) = \<Union>C"
-      by (auto simp add: F_def split: if_split_asm) blast
+      by (auto simp add: F_def split: if_split_asm cong del: SUP_cong)
     moreover have sets_F: "\<And>i. F i \<in> M"
       using F' sets_C by (auto simp: F_def)
     moreover note sets_C
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -258,6 +258,7 @@
       have "g1 +++ g2 differentiable at (x / 2) within {0..1/2}"
         by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+
       then show "g1 +++ g2 \<circ> (*) (inverse 2) differentiable at x within {0..1}"
+        using image_affinity_atLeastAtMost_div [of 2 0 "0::real" 1]
         by (auto intro: differentiable_chain_within)
     qed (use that in \<open>auto simp: joinpaths_def\<close>)
   qed
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1049,7 +1049,8 @@
             then show fsb: "f ` (S \<inter> ball x r) \<in> lmeasurable"
               by (simp add: image_comp o_def)
             have "?\<mu> (f ` (S \<inter> ball x r)) = ?\<mu> (?rfs) * r ^ CARD('n)"
-              using \<open>r > 0\<close> by (simp add: measure_translation measure_linear_image measurable_translation fsb field_simps)
+              using \<open>r > 0\<close> fsb
+              by (simp add: measure_linear_image measure_translation_subtract measurable_translation_subtract field_simps cong: image_cong_simp)
             also have "\<dots> \<le> (\<bar>det (matrix (f' x))\<bar> * unit_ball_vol (CARD('n)) + e * unit_ball_vol (CARD('n))) * r ^ CARD('n)"
             proof -
               have "?\<mu> (?rfs) < ?\<mu> (f' x ` ball 0 1) + e * unit_ball_vol (CARD('n))"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -977,17 +977,27 @@
       proof -
         have DIM_complex[intro]: "2 \<le> DIM(complex)"  \<comment> \<open>should not be necessary!\<close>
           by simp
+        from lt1 have "f (inverse x) \<noteq> 0 \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> cmod x < r \<Longrightarrow> 1 < cmod (f (inverse x))" for x
+          using one_less_inverse by force
+        then have **: "cmod (f (inverse x)) \<le> 1 \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> cmod x < r \<Longrightarrow> f (inverse x) = 0" for x
+          by force
+        then have *: "(f \<circ> inverse) ` (ball 0 r - {0}) \<subseteq> {0} \<union> - ball 0 1"
+          by force
         have "continuous_on (inverse ` (ball 0 r - {0})) f"
           using continuous_on_subset holf holomorphic_on_imp_continuous_on by blast
         then have "connected ((f \<circ> inverse) ` (ball 0 r - {0}))"
           apply (intro connected_continuous_image continuous_intros)
           apply (force intro: connected_punctured_ball)+
           done
-        then have "\<lbrakk>w \<noteq> 0; cmod w < r\<rbrakk> \<Longrightarrow> f (inverse w) = 0" for w
-          apply (rule disjE [OF connected_closedD [where A = "{0}" and B = "- ball 0 1"]], auto)
-          apply (metis (mono_tags, hide_lams) not_less_iff_gr_or_eq one_less_inverse lt1 zero_less_norm_iff)
-          using False \<open>0 < r\<close> apply fastforce
-          by (metis (no_types, hide_lams) Compl_iff IntI comp_apply empty_iff image_eqI insert_Diff_single insert_iff mem_ball_0 not_less_iff_gr_or_eq one_less_inverse that(2) zero_less_norm_iff)
+        then have "{0} \<inter> (f \<circ> inverse) ` (ball 0 r - {0}) = {} \<or> - ball 0 1 \<inter> (f \<circ> inverse) ` (ball 0 r - {0}) = {}"
+          by (rule connected_closedD) (use * in auto)
+        then have "w \<noteq> 0 \<Longrightarrow> cmod w < r \<Longrightarrow> f (inverse w) = 0" for w
+          using fi0 **[of w] \<open>0 < r\<close>
+          apply (auto simp add: inf.commute [of "- ball 0 1"] Diff_eq [symmetric] image_subset_iff dest: less_imp_le)
+           apply fastforce
+          apply (drule bspec [of _ _ w])
+           apply (auto dest: less_imp_le)
+          done
         then show ?thesis
           apply (simp add: lim_at_infinity_0)
           apply (rule Lim_eventually)
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Convex.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -613,15 +613,18 @@
 qed
 
 lemma convex_translation:
-  assumes "convex S"
-  shows "convex ((\<lambda>x. a + x) ` S)"
+  "convex ((+) a ` S)" if "convex S"
 proof -
-  have "(\<Union> x\<in> {a}. \<Union>y \<in> S. {x + y}) = (\<lambda>x. a + x) ` S"
+  have "(\<Union> x\<in> {a}. \<Union>y \<in> S. {x + y}) = (+) a ` S"
     by auto
   then show ?thesis
-    using convex_sums[OF convex_singleton[of a] assms] by auto
+    using convex_sums [OF convex_singleton [of a] that] by auto
 qed
 
+lemma convex_translation_subtract:
+  "convex ((\<lambda>b. b - a) ` S)" if "convex S"
+  using convex_translation [of S "- a"] that by (simp cong: image_cong_simp)
+
 lemma convex_affinity:
   assumes "convex S"
   shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` S)"
@@ -1106,9 +1109,14 @@
   finally show ?thesis .
 qed (insert assms(2), simp_all)
 
-lemma convex_translation_eq [simp]: "convex ((\<lambda>x. a + x) ` s) \<longleftrightarrow> convex s"
+lemma convex_translation_eq [simp]:
+  "convex ((+) a ` s) \<longleftrightarrow> convex s"
   by (metis convex_translation translation_galois)
 
+lemma convex_translation_subtract_eq [simp]:
+  "convex ((\<lambda>b. b - a) ` s) \<longleftrightarrow> convex s"
+  using convex_translation_eq [of "- a"] by (simp cong: image_cong_simp)
+
 lemma convex_linear_image_eq [simp]:
     fixes f :: "'a::real_vector \<Rightarrow> 'b::real_vector"
     shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> convex (f ` s) \<longleftrightarrow> convex s"
@@ -1614,13 +1622,13 @@
 qed
 
 lemma affine_translation:
-  fixes a :: "'a::real_vector"
-  shows "affine S \<longleftrightarrow> affine ((\<lambda>x. a + x) ` S)"
-proof -
-  have "affine S \<Longrightarrow> affine ((\<lambda>x. a + x) ` S)"
-    using affine_translation_aux[of "-a" "((\<lambda>x. a + x) ` S)"]
-    using translation_assoc[of "-a" a S] by auto
-  then show ?thesis using affine_translation_aux by auto
+  "affine S \<longleftrightarrow> affine ((+) a ` S)" for a :: "'a::real_vector"
+proof
+  show "affine ((+) a ` S)" if "affine S"
+    using that translation_assoc [of "- a" a S]
+    by (auto intro: affine_translation_aux [of "- a" "((+) a ` S)"])
+  show "affine S" if "affine ((+) a ` S)"
+    using that by (rule affine_translation_aux)
 qed
 
 lemma parallel_is_affine:
@@ -1700,6 +1708,10 @@
   ultimately show ?thesis using subspace_affine by auto
 qed
 
+lemma affine_diffs_subspace_subtract:
+  "subspace ((\<lambda>x. x - a) ` S)" if "affine S" "a \<in> S"
+  using that affine_diffs_subspace [of _ a] by simp
+
 lemma parallel_subspace_explicit:
   assumes "affine S"
     and "a \<in> S"
@@ -3235,8 +3247,7 @@
 qed
 
 lemma aff_dim_translation_eq:
-  fixes a :: "'n::euclidean_space"
-  shows "aff_dim ((\<lambda>x. a + x) ` S) = aff_dim S"
+  "aff_dim ((+) a ` S) = aff_dim S" for a :: "'n::euclidean_space"
 proof -
   have "affine_parallel (affine hull S) (affine hull ((\<lambda>x. a + x) ` S))"
     unfolding affine_parallel_def
@@ -3248,6 +3259,10 @@
     using aff_dim_parallel_eq[of S "(\<lambda>x. a + x) ` S"] by auto
 qed
 
+lemma aff_dim_translation_eq_subtract:
+  "aff_dim ((\<lambda>x. x - a) ` S) = aff_dim S" for a :: "'n::euclidean_space"
+  using aff_dim_translation_eq [of "- a"] by (simp cong: image_cong_simp)
+
 lemma aff_dim_affine:
   fixes S L :: "'n::euclidean_space set"
   assumes "S \<noteq> {}"
@@ -3306,17 +3321,21 @@
 qed
 
 lemma aff_dim_eq_dim:
-  fixes S :: "'n::euclidean_space set"
-  assumes "a \<in> affine hull S"
-  shows "aff_dim S = int (dim ((\<lambda>x. -a+x) ` S))"
+  "aff_dim S = int (dim ((+) (- a) ` S))" if "a \<in> affine hull S"
+    for S :: "'n::euclidean_space set"
 proof -
-  have "0 \<in> affine hull ((\<lambda>x. -a+x) ` S)"
+  have "0 \<in> affine hull (+) (- a) ` S"
     unfolding affine_hull_translation
-    using assms by (simp add: ab_group_add_class.ab_left_minus image_iff)
+    using that by (simp add: ac_simps)
   with aff_dim_zero show ?thesis
     by (metis aff_dim_translation_eq)
 qed
 
+lemma aff_dim_eq_dim_subtract:
+  "aff_dim S = int (dim ((\<lambda>x. x - a) ` S))" if "a \<in> affine hull S"
+    for S :: "'n::euclidean_space set"
+  using aff_dim_eq_dim [of a] that by (simp cong: image_cong_simp)
+
 lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
   using aff_dim_subspace[of "(UNIV :: 'n::euclidean_space set)"]
     dim_UNIV[where 'a="'n::euclidean_space"]
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1215,8 +1215,7 @@
 qed
 
 lemma interior_translation:
-  fixes S :: "'a::real_normed_vector set"
-  shows "interior ((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (interior S)"
+  "interior ((+) a ` S) = (+) a ` (interior S)" for S :: "'a::real_normed_vector set"
 proof (rule set_eqI, rule)
   fix x
   assume "x \<in> interior ((+) a ` S)"
@@ -1254,6 +1253,11 @@
     unfolding mem_interior using \<open>e > 0\<close> by auto
 qed
 
+lemma interior_translation_subtract:
+  "interior ((\<lambda>x. x - a) ` S) = (\<lambda>x. x - a) ` interior S" for S :: "'a::real_normed_vector set"
+  using interior_translation [of "- a"] by (simp cong: image_cong_simp)
+
+
 lemma compact_scaling:
   fixes s :: "'a::real_normed_vector set"
   assumes "compact s"
@@ -1306,16 +1310,18 @@
 qed
 
 lemma compact_translation:
-  fixes s :: "'a::real_normed_vector set"
-  assumes "compact s"
-  shows "compact ((\<lambda>x. a + x) ` s)"
+  "compact ((+) a ` s)" if "compact s" for s :: "'a::real_normed_vector set"
 proof -
   have "{x + y |x y. x \<in> s \<and> y \<in> {a}} = (\<lambda>x. a + x) ` s"
     by auto
   then show ?thesis
-    using compact_sums[OF assms compact_sing[of a]] by auto
+    using compact_sums [OF that compact_sing [of a]] by auto
 qed
 
+lemma compact_translation_subtract:
+  "compact ((\<lambda>x. x - a) ` s)" if "compact s" for s :: "'a::real_normed_vector set"
+  using that compact_translation [of s "- a"] by (simp cong: image_cong_simp)
+
 lemma compact_affinity:
   fixes s :: "'a::real_normed_vector set"
   assumes "compact s"
@@ -1420,48 +1426,62 @@
 qed
 
 lemma closed_translation:
-  fixes a :: "'a::real_normed_vector"
-  assumes "closed S"
-  shows "closed ((\<lambda>x. a + x) ` S)"
+  "closed ((+) a ` S)" if "closed S" for a :: "'a::real_normed_vector"
 proof -
   have "(\<Union>x\<in> {a}. \<Union>y \<in> S. {x + y}) = ((+) a ` S)" by auto
   then show ?thesis
-    using compact_closed_sums[OF compact_sing[of a] assms] by auto
+    using compact_closed_sums [OF compact_sing [of a] that] by auto
 qed
 
+lemma closed_translation_subtract:
+  "closed ((\<lambda>x. x - a) ` S)" if "closed S" for a :: "'a::real_normed_vector"
+  using that closed_translation [of S "- a"] by (simp cong: image_cong_simp)
+
 lemma closure_translation:
-  fixes a :: "'a::real_normed_vector"
-  shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
+  "closure ((+) a ` s) = (+) a ` closure s" for a :: "'a::real_normed_vector"
 proof -
   have *: "(+) a ` (- s) = - (+) a ` s"
-    by (auto intro!: image_eqI[where x="x - a" for x])
+    by (auto intro!: image_eqI [where x = "x - a" for x])
   show ?thesis
-    unfolding closure_interior translation_Compl
-    using interior_translation[of a "- s"]
-    unfolding *
-    by auto
+    using interior_translation [of a "- s", symmetric]
+    by (simp add: closure_interior translation_Compl *)
 qed
 
+lemma closure_translation_subtract:
+  "closure ((\<lambda>x. x - a) ` s) = (\<lambda>x. x - a) ` closure s" for a :: "'a::real_normed_vector"
+  using closure_translation [of "- a" s] by (simp cong: image_cong_simp)
+
 lemma frontier_translation:
-  fixes a :: "'a::real_normed_vector"
-  shows "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)"
-  unfolding frontier_def translation_diff interior_translation closure_translation
-  by auto
+  "frontier ((+) a ` s) = (+) a ` frontier s" for a :: "'a::real_normed_vector"
+  by (auto simp add: frontier_def translation_diff interior_translation closure_translation)
+
+lemma frontier_translation_subtract:
+  "frontier ((+) a ` s) = (+) a ` frontier s" for a :: "'a::real_normed_vector"
+  by (auto simp add: frontier_def translation_diff interior_translation closure_translation)
 
 lemma sphere_translation:
-  fixes a :: "'n::real_normed_vector"
-  shows "sphere (a+c) r = (+) a ` sphere c r"
-  by (auto simp: dist_norm algebra_simps intro!: image_eqI[where x="x - a" for x])
+  "sphere (a + c) r = (+) a ` sphere c r" for a :: "'n::real_normed_vector"
+  by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x = "x - a" for x])
+
+lemma sphere_translation_subtract:
+  "sphere (c - a) r = (\<lambda>x. x - a) ` sphere c r" for a :: "'n::real_normed_vector"
+  using sphere_translation [of "- a" c] by (simp cong: image_cong_simp)
 
 lemma cball_translation:
-  fixes a :: "'n::real_normed_vector"
-  shows "cball (a+c) r = (+) a ` cball c r"
-  by (auto simp: dist_norm algebra_simps intro!: image_eqI[where x="x - a" for x])
+  "cball (a + c) r = (+) a ` cball c r" for a :: "'n::real_normed_vector"
+  by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x = "x - a" for x])
+
+lemma cball_translation_subtract:
+  "cball (c - a) r = (\<lambda>x. x - a) ` cball c r" for a :: "'n::real_normed_vector"
+  using cball_translation [of "- a" c] by (simp cong: image_cong_simp)
 
 lemma ball_translation:
-  fixes a :: "'n::real_normed_vector"
-  shows "ball (a+c) r = (+) a ` ball c r"
-  by (auto simp: dist_norm algebra_simps intro!: image_eqI[where x="x - a" for x])
+  "ball (a + c) r = (+) a ` ball c r" for a :: "'n::real_normed_vector"
+  by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x = "x - a" for x])
+
+lemma ball_translation_subtract:
+  "ball (c - a) r = (\<lambda>x. x - a) ` ball c r" for a :: "'n::real_normed_vector"
+  using ball_translation [of "- a" c] by (simp cong: image_cong_simp)
 
 
 subsection%unimportant\<open>Homeomorphisms\<close>
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1170,17 +1170,15 @@
 
 lemma starlike_negligible:
   assumes "closed S"
-      and eq1: "\<And>c x. \<lbrakk>(a + c *\<^sub>R x) \<in> S; 0 \<le> c; a + x \<in> S\<rbrakk> \<Longrightarrow> c = 1"
+      and eq1: "\<And>c x. (a + c *\<^sub>R x) \<in> S \<Longrightarrow> 0 \<le> c \<Longrightarrow> a + x \<in> S \<Longrightarrow> c = 1"
     shows "negligible S"
 proof -
   have "negligible ((+) (-a) ` S)"
   proof (subst negligible_on_intervals, intro allI)
     fix u v
     show "negligible ((+) (- a) ` S \<inter> cbox u v)"
-      unfolding negligible_iff_null_sets
-      apply (rule starlike_negligible_compact)
-       apply (simp add: assms closed_translation closed_Int_compact, clarify)
-      by (metis eq1 minus_add_cancel)
+      using \<open>closed S\<close> eq1 by (auto simp add: negligible_iff_null_sets field_simps
+        intro!: closed_translation_subtract starlike_negligible_compact cong: image_cong_simp)
   qed
   then show ?thesis
     by (rule negligible_translation_rev)
@@ -1478,7 +1476,7 @@
   have 3: "\<And>x. (\<lambda>k. indicat_real (\<Union>m\<le>k. S m) x) \<longlonglongrightarrow> (indicat_real (\<Union>n. S n) x)"
     by (force simp: indicator_def eventually_sequentially intro: Lim_eventually)
   have 4: "bounded (range (\<lambda>k. integral UNIV (indicat_real (\<Union>m\<le>k. S m))))"
-    by (simp add: 0 image_def)
+    by (simp add: 0)
   have *: "indicat_real (\<Union>n. S n) integrable_on UNIV \<and>
         (\<lambda>k. integral UNIV (indicat_real (\<Union>m\<le>k. S m))) \<longlonglongrightarrow> (integral UNIV (indicat_real (\<Union>n. S n)))"
     by (intro monotone_convergence_increasing 1 2 3 4)
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -349,14 +349,11 @@
 lemma min_Liminf_at:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_linorder"
   shows "min (f x) (Liminf (at x) f) = (SUP e\<in>{0<..}. INF y\<in>ball x e. f y)"
-  unfolding inf_min[symmetric] Liminf_at
+  apply (simp add: inf_min [symmetric] Liminf_at)
   apply (subst inf_commute)
   apply (subst SUP_inf)
-  apply (intro SUP_cong[OF refl])
-  apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
-  apply (drule sym)
   apply auto
-  apply (metis INF_absorb centre_in_ball)
+  apply (metis (no_types, lifting) INF_insert centre_in_ball greaterThan_iff image_cong inf_commute insert_Diff)
   done
 
 
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -395,9 +395,8 @@
   apply auto []
   apply auto []
   apply simp
-  apply (subst SUP_cong[OF refl])
+  apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl])
   apply (rule sets_vimage_algebra2)
-  apply auto []
   apply (auto intro!: arg_cong2[where f=sigma_sets])
   done
 
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1926,7 +1926,8 @@
     then have "open ((h \<circ> f) ` ball a r)"
       by (simp add: image_comp \<open>\<And>x. k (h x) = x\<close> cong: image_cong)
     then show ?thesis
-      apply (simp add: image_comp [symmetric])
+      apply (simp only: image_comp [symmetric])
+
       apply (metis open_bijective_linear_image_eq \<open>linear h\<close> \<open>\<And>x. k (h x) = x\<close> \<open>range h = UNIV\<close> bijI inj_on_def)
       done
 next
@@ -2042,9 +2043,8 @@
   qed
   moreover
   have eq: "f ` U = h ` (k \<circ> f \<circ> h \<circ> k) ` U"
-    apply (auto simp: image_comp [symmetric])
-    apply (metis homkh \<open>U \<subseteq> S\<close> fim homeomorphism_image2 homeomorphism_of_subsets homhk imageI subset_UNIV)
-    by (metis \<open>U \<subseteq> S\<close> subsetD fim homeomorphism_def homhk image_eqI)
+    unfolding image_comp [symmetric] using \<open>U \<subseteq> S\<close> fim
+    by (metis homeomorphism_image2 homeomorphism_of_subsets homkh subset_image_iff)
   ultimately show ?thesis
     by (metis (no_types, hide_lams) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
 qed
@@ -2159,11 +2159,16 @@
       apply (clarsimp simp: inj_on_def)
       by (metis fim homeomorphism_apply1 homhk image_subset_iff inj_onD injf)
     ultimately have ope_hf: "openin (subtopology euclidean U) ((h \<circ> f) ` S)"
-      using invariance_of_domain_subspaces [OF ope \<open>subspace U\<close> \<open>subspace U\<close>] by auto
+      using invariance_of_domain_subspaces [OF ope \<open>subspace U\<close> \<open>subspace U\<close>] by blast
     have "(h \<circ> f) ` S \<subseteq> T"
       using fim homeomorphism_image1 homhk by fastforce
-    then show ?thesis
-      by (metis dim_openin \<open>dim T = dim V\<close> ope_hf \<open>subspace U\<close> \<open>S \<noteq> {}\<close> dim_subset image_is_empty not_le that)
+    then have "dim ((h \<circ> f) ` S) \<le> dim T"
+      by (rule dim_subset)
+    also have "dim ((h \<circ> f) ` S) = dim U"
+      using \<open>S \<noteq> {}\<close> \<open>subspace U\<close>
+      by (blast intro: dim_openin ope_hf)
+    finally show False
+      using \<open>dim V < dim U\<close> \<open>dim T = dim V\<close> by simp
   qed
   then show ?thesis
     using not_less by blast
@@ -2188,9 +2193,9 @@
     show "openin (subtopology euclidean ((+) (- a) ` U)) ((+) (- a) ` S)"
       by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
     show "subspace ((+) (- a) ` U)"
-      by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace \<open>affine U\<close>)
+      by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace_subtract \<open>affine U\<close> cong: image_cong_simp)
     show "subspace ((+) (- b) ` V)"
-      by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace \<open>affine V\<close>)
+      by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace_subtract \<open>affine V\<close> cong: image_cong_simp)
     show "dim ((+) (- b) ` V) \<le> dim ((+) (- a) ` U)"
       by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
     show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
@@ -2219,9 +2224,9 @@
     show "openin (subtopology euclidean ((+) (- a) ` U)) ((+) (- a) ` S)"
       by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
     show "subspace ((+) (- a) ` U)"
-      by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace \<open>affine U\<close>)
+      by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace_subtract \<open>affine U\<close> cong: image_cong_simp)
     show "subspace ((+) (- b) ` V)"
-      by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace \<open>affine V\<close>)
+      by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace_subtract \<open>affine V\<close> cong: image_cong_simp)
     show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
       by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
     show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
@@ -3474,7 +3479,6 @@
           apply (intro conjI ballI eq1 continuous_on_exp [OF continuous_on_id])
              apply (auto simp: \<gamma>exp exp2n cont n)
            apply (simp add:  homeomorphism_apply1 [OF hom])
-          apply (simp add: image_comp [symmetric])
           using hom homeomorphism_apply1  apply (force simp: image_iff)
           done
       qed
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -4825,7 +4825,7 @@
     show "(indicator ((+) c ` S) has_integral 0) (cbox a b)"
       using has_integral_affinity [OF *, of 1 "-c"]
             cbox_translation [of "c" "-c+a" "-c+b"]
-      by (simp add: eq add.commute)
+      by (simp add: eq) (simp add: ac_simps)
   qed
 qed
 
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Homeomorphism.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -551,13 +551,13 @@
 proof%unimportant -
   have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation)
   have 2: "0 \<in> rel_interior ((+) (-a) ` S)"
-    by (simp add: a rel_interior_translation)
+    using a rel_interior_translation [of "- a" S] by (simp cong: image_cong_simp)
   have 3: "open_segment 0 x \<subseteq> rel_interior ((+) (-a) ` S)" if "x \<in> ((+) (-a) ` S)" for x
   proof -
     have "x+a \<in> S" using that by auto
     then have "open_segment a (x+a) \<subseteq> rel_interior S" by (metis star)
-    then show ?thesis using open_segment_translation
-      using rel_interior_translation by fastforce
+    then show ?thesis using open_segment_translation [of a 0 x]
+      using rel_interior_translation [of "- a" S] by (fastforce simp add: ac_simps image_iff cong: image_cong_simp)
   qed
   have "S - rel_interior S homeomorphic ((+) (-a) ` S) - rel_interior ((+) (-a) ` S)"
     by (metis rel_interior_translation translation_diff homeomorphic_translation)
@@ -841,8 +841,8 @@
     using assms by (auto simp: dist_norm norm_minus_commute divide_simps)
   also have "... homeomorphic p"
     apply (rule homeomorphic_punctured_affine_sphere_affine_01)
-    using assms
-    apply (auto simp: dist_norm norm_minus_commute affine_scaling affine_translation [symmetric] aff_dim_translation_eq inj)
+    using assms affine_translation [symmetric, of "- a"] aff_dim_translation_eq [of "- a"]
+         apply (auto simp: dist_norm norm_minus_commute affine_scaling inj)
     done
   finally show ?thesis .
 qed
@@ -931,16 +931,16 @@
   then have "dim ((+) (- a) ` S) = aff_dim ((+) (- a) ` S)"
     by (simp add: aff_dim_zero)
   also have "... < DIM('n)"
-    by (simp add: aff_dim_translation_eq assms)
+    by (simp add: aff_dim_translation_eq_subtract assms cong: image_cong_simp)
   finally have dd: "dim ((+) (- a) ` S) < DIM('n)"
     by linarith
-  obtain T where "subspace T" and Tsub: "T \<subseteq> {x. i \<bullet> x = 0}"
-             and dimT: "dim T = dim ((+) (- a) ` S)"
-    apply (rule choose_subspace_of_subspace [of "dim ((+) (- a) ` S)" "{x::'n. i \<bullet> x = 0}"])
-     apply (simp add: dim_hyperplane [OF \<open>i \<noteq> 0\<close>])
-     apply (metis DIM_positive Suc_pred dd not_le not_less_eq_eq)
-    apply (metis span_eq_iff subspace_hyperplane)
-    done
+  have span: "span {x. i \<bullet> x = 0} = {x. i \<bullet> x = 0}"
+    using span_eq_iff [symmetric, of "{x. i \<bullet> x = 0}"] subspace_hyperplane [of i] by simp
+  have "dim ((+) (- a) ` S) \<le> dim {x. i \<bullet> x = 0}"
+    using dd by (simp add: dim_hyperplane [OF \<open>i \<noteq> 0\<close>])
+  then obtain T where "subspace T" and Tsub: "T \<subseteq> {x. i \<bullet> x = 0}"
+    and dimT: "dim T = dim ((+) (- a) ` S)"
+    by (rule choose_subspace_of_subspace) (simp add: span)
   have "subspace (span ((+) (- a) ` S))"
     using subspace_span by blast
   then obtain h k where "linear h" "linear k"
@@ -974,23 +974,23 @@
     by (metis Diff_subset order_trans sphere_cball)
   have [simp]: "\<And>u. u \<in> S \<Longrightarrow> norm (g (h (u - a))) = 1"
     using gh_sub_sph [THEN subsetD] by (auto simp: o_def)
-  have ghcont: "continuous_on ((+) (- a) ` S) (\<lambda>x. g (h x))"
+  have ghcont: "continuous_on ((\<lambda>x. x - a) ` S) (\<lambda>x. g (h x))"
     apply (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force)
     done
-  have kfcont: "continuous_on ((g \<circ> h \<circ> (+) (- a)) ` S) (\<lambda>x. k (f x))"
+  have kfcont: "continuous_on ((\<lambda>x. g (h (x - a))) ` S) (\<lambda>x. k (f x))"
     apply (rule continuous_on_compose2 [OF kcont])
     using homeomorphism_cont1 [OF fg] gh_sub_sph apply (force intro: continuous_on_subset, blast)
     done
   have "S homeomorphic (+) (- a) ` S"
-    by (simp add: homeomorphic_translation)
-  also have Shom: "\<dots> homeomorphic (g \<circ> h) ` (+) (- a) ` S"
-    apply (simp add: homeomorphic_def homeomorphism_def)
+    by (fact homeomorphic_translation)
+  also have "\<dots> homeomorphic (g \<circ> h) ` (+) (- a) ` S"
+    apply (simp add: homeomorphic_def homeomorphism_def cong: image_cong_simp)
     apply (rule_tac x="g \<circ> h" in exI)
     apply (rule_tac x="k \<circ> f" in exI)
-    apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp)
-    apply (force simp: o_def homeomorphism_apply2 [OF fg] span_base)
+    apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp cong: image_cong_simp)
     done
-  finally have Shom: "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" .
+  finally have Shom: "S homeomorphic (\<lambda>x. g (h x)) ` (\<lambda>x. x - a) ` S"
+    by (simp cong: image_cong_simp)
   show ?thesis
     apply (rule_tac U = "ball 0 1 \<union> image (g o h) ((+) (- a) ` S)"
                 and T = "image (g o h) ((+) (- a) ` S)"
@@ -1000,7 +1000,7 @@
     apply force
     apply (simp add: closedin_closed)
     apply (rule_tac x="sphere 0 1" in exI)
-    apply (auto simp: Shom)
+     apply (auto simp: Shom cong: image_cong_simp)
     done
 qed
 
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1104,16 +1104,24 @@
 qed
 
 lemma measurable_translation:
-   "S \<in> lmeasurable \<Longrightarrow> ((\<lambda>x. a + x) ` S) \<in> lmeasurable"
-  unfolding fmeasurable_def
-apply (auto intro: lebesgue_sets_translation)
-  using  emeasure_lebesgue_affine [of 1 a S]
-  by (auto simp: add.commute [of _ a])
+   "S \<in> lmeasurable \<Longrightarrow> ((+) a ` S) \<in> lmeasurable"
+  using emeasure_lebesgue_affine [of 1 a S]
+  apply (auto intro: lebesgue_sets_translation simp add: fmeasurable_def cong: image_cong_simp)
+  apply (simp add: ac_simps)
+  done
+
+lemma measurable_translation_subtract:
+   "S \<in> lmeasurable \<Longrightarrow> ((\<lambda>x. x - a) ` S) \<in> lmeasurable"
+  using measurable_translation [of S "- a"] by (simp cong: image_cong_simp)
 
 lemma measure_translation:
-   "measure lebesgue ((\<lambda>x. a + x) ` S) = measure lebesgue S"
-  using measure_lebesgue_affine [of 1 a S]
-  by (auto simp: add.commute [of _ a])
+  "measure lebesgue ((+) a ` S) = measure lebesgue S"
+  using measure_lebesgue_affine [of 1 a S] by (simp add: ac_simps cong: image_cong_simp)
+
+lemma measure_translation_subtract:
+  "measure lebesgue ((\<lambda>x. x - a) ` S) = measure lebesgue S"
+  using measure_translation [of "- a"] by (simp cong: image_cong_simp)
+
 
 subsection \<open>A nice lemma for negligibility proofs\<close>
 
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Measure_Space.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -2368,8 +2368,8 @@
         by (rule infinite_super[OF _ 1]) auto
       then have "infinite (\<Union>i. F i)"
         by auto
-
-      ultimately show ?thesis by auto
+      ultimately show ?thesis by (simp only:) simp
+         
     qed
   qed
 qed
@@ -2899,6 +2899,8 @@
       case (1 X)
       then have [measurable]: "\<And>i. X i \<in> sets A" and "disjoint_family X"
         by auto
+      have disjoint: "disjoint_family (\<lambda>i. X i \<inter> Y)" "disjoint_family (\<lambda>i. X i - Y)" for Y
+        by (auto intro: disjoint_family_on_bisimulation [OF \<open>disjoint_family X\<close>, simplified])
       have "(\<Sum>i. ?S (X i)) = (SUP Y\<in>sets A. \<Sum>i. ?d (X i) Y)"
       proof (rule ennreal_suminf_SUP_eq_directed)
         fix J :: "nat set" and a b assume "finite J" and [measurable]: "a \<in> sets A" "b \<in> sets A"
@@ -2966,10 +2968,13 @@
           done
       qed
       also have "\<dots> = ?S (\<Union>i. X i)"
-        unfolding UN_extend_simps(4)
-        by (auto simp add: suminf_add[symmetric] Diff_eq[symmetric] simp del: UN_simps
-                 intro!: SUP_cong arg_cong2[where f="(+)"] suminf_emeasure
-                         disjoint_family_on_bisimulation[OF \<open>disjoint_family X\<close>])
+        apply (simp only: UN_extend_simps(4))
+        apply (rule arg_cong [of _ _ Sup])
+        apply (rule image_cong)
+         apply (fact refl)
+        using disjoint
+        apply (auto simp add: suminf_add [symmetric] Diff_eq [symmetric] image_subset_iff suminf_emeasure simp del: UN_simps)
+        done
       finally show "(\<Sum>i. ?S (X i)) = ?S (\<Union>i. X i)" .
     qed
   qed (auto dest: sets.sets_into_space simp: positive_def intro!: SUP_const)
@@ -3250,7 +3255,7 @@
         by (safe intro!: bexI[of _ "i \<union> j"]) auto
     next
       show "(SUP P \<in> {P. finite P \<and> P \<subseteq> M}. \<Sum>n. ?\<mu> P (F n)) = (SUP P \<in> {P. finite P \<and> P \<subseteq> M}. ?\<mu> P (\<Union>(F ` UNIV)))"
-      proof (intro SUP_cong refl)
+      proof (intro arg_cong [of _ _ Sup] image_cong refl)
         fix i assume i: "i \<in> {P. finite P \<and> P \<subseteq> M}"
         show "(\<Sum>n. ?\<mu> i (F n)) = ?\<mu> i (\<Union>(F ` UNIV))"
         proof cases
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -177,7 +177,7 @@
   have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto
   hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset)
   have "?h -` {0} \<inter> space M = space M" by auto
-  thus ?thesis unfolding simple_function_def by auto
+  thus ?thesis unfolding simple_function_def by (auto simp add: image_constant_conv)
 qed
 
 lemma simple_function_cong:
@@ -220,7 +220,7 @@
   unfolding simple_function_def
 proof safe
   show "finite ((g \<circ> f) ` space M)"
-    using assms unfolding simple_function_def by (auto simp: image_comp [symmetric])
+    using assms unfolding simple_function_def image_comp [symmetric] by auto
 next
   fix x assume "x \<in> space M"
   let ?G = "g -` {g (f x)} \<inter> (f`space M)"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -767,10 +767,7 @@
 lemma path_image_subpath_gen:
   fixes g :: "_ \<Rightarrow> 'a::real_normed_vector"
   shows "path_image(subpath u v g) = g ` (closed_segment u v)"
-  apply (simp add: closed_segment_real_eq path_image_def subpath_def)
-  apply (subst o_def [of g, symmetric])
-  apply (simp add: image_comp [symmetric])
-  done
+  by (auto simp add: closed_segment_real_eq path_image_def subpath_def)
 
 lemma path_image_subpath:
   fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Polytope.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -935,6 +935,12 @@
 using%unimportant extreme_point_of_translation_eq
 by%unimportant auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
 
+lemma%important extreme_points_of_translation_subtract:
+   "{x. x extreme_point_of (image (\<lambda>x. x - a) S)} =
+    (\<lambda>x. x - a) ` {x. x extreme_point_of S}"
+using%unimportant extreme_points_of_translation [of "- a" S]
+by%unimportant simp
+
 lemma%unimportant extreme_point_of_Int:
    "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
 by (simp add: extreme_point_of_def)
@@ -1206,13 +1212,13 @@
   proof
     fix a assume [simp]: "a \<in> S"
     have 1: "compact ((+) (- a) ` S)"
-      by (simp add: \<open>compact S\<close> compact_translation)
+      by (simp add: \<open>compact S\<close> compact_translation_subtract cong: image_cong_simp)
     have 2: "convex ((+) (- a) ` S)"
-      by (simp add: \<open>convex S\<close> convex_translation)
+      by (simp add: \<open>convex S\<close> compact_translation_subtract)
     show a_invex: "a \<in> convex hull {x. x extreme_point_of S}"
       using Krein_Milman_Minkowski_aux [OF refl 1 2]
             convex_hull_translation [of "-a"]
-      by (auto simp: extreme_points_of_translation translation_assoc)
+      by (auto simp: extreme_points_of_translation_subtract translation_assoc cong: image_cong_simp)
     qed
 next
   show "convex hull {x. x extreme_point_of S} \<subseteq> S"
@@ -2079,19 +2085,27 @@
         next
           case False
           then obtain h' where h': "h' \<in> F - {h}" by auto
-          define inff where "inff =
-            (INF j\<in>F - {h}.
-              if 0 < a j \<bullet> y - a j \<bullet> w
+          let ?body = "(\<lambda>j. if 0 < a j \<bullet> y - a j \<bullet> w
               then (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)
-              else 1)"
-          have "0 < inff"
-            apply (simp add: inff_def)
-            apply (rule finite_imp_less_Inf)
-              using \<open>finite F\<close> apply blast
-             using h' apply blast
-            apply simp
-            using awlt apply (force simp: divide_simps)
-            done
+              else 1) ` (F - {h})"
+          define inff where "inff = Inf ?body"
+          from \<open>finite F\<close> have "finite ?body"
+            by blast
+          moreover from h' have "?body \<noteq> {}"
+            by blast
+          moreover have "j > 0" if "j \<in> ?body" for j
+          proof -
+            from that obtain x where "x \<in> F" and "x \<noteq> h" and *: "j =
+              (if 0 < a x \<bullet> y - a x \<bullet> w
+                then (b x - a x \<bullet> w) / (a x \<bullet> y - a x \<bullet> w) else 1)"
+              by blast
+            with awlt [of x] have "a x \<bullet> w < b x"
+              by simp
+            with * show ?thesis
+              by simp
+          qed
+          ultimately have "0 < inff"
+            by (simp_all add: finite_less_Inf_iff inff_def)
           moreover have "inff * (a j \<bullet> y - a j \<bullet> w) \<le> b j - a j \<bullet> w"
                         if "j \<in> F" "j \<noteq> h" for j
           proof (cases "a j \<bullet> w < a j \<bullet> y")
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Regularity.thy
--- a/src/HOL/Analysis/Regularity.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Regularity.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -220,13 +220,18 @@
     also have "\<dots> = (INF K\<in>{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
       by (subst ennreal_SUP_const_minus) (auto simp: less_top[symmetric] inner)
     also have "\<dots> = (INF U\<in>{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
-      by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
+      by (auto simp add: emeasure_compl sb compact_imp_closed)
     also have "\<dots> \<ge> (INF U\<in>{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
       by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
     also have "(INF U\<in>{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
         (INF U\<in>{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
-      unfolding INF_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
-        by (rule INF_cong) (auto simp add: sU Compl_eq_Diff_UNIV [symmetric, simp])
+      apply (rule arg_cong [of _ _ Inf])
+      using sU
+      apply (auto simp add: image_iff)
+      apply (rule exI [of _ "UNIV - y" for y])
+      apply safe
+        apply (auto simp add: double_diff)
+      done
     finally have
       "(INF U\<in>{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
     moreover have
@@ -239,10 +244,12 @@
     also have "\<dots> = (SUP U\<in> {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
       unfolding outer by (subst ennreal_INF_const_minus) auto
     also have "\<dots> = (SUP U\<in>{U. B \<subseteq> U \<and> open U}. M (space M - U))"
-      by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
+      by (auto simp add: emeasure_compl sb compact_imp_closed)
     also have "\<dots> = (SUP K\<in>{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
       unfolding SUP_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
-        by (rule SUP_cong) (auto simp add: sU)
+      apply (rule arg_cong [of _ _ Sup])
+      using sU apply (auto intro!: imageI)
+      done
     also have "\<dots> = (SUP K\<in>{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
     proof (safe intro!: antisym SUP_least)
       fix K assume "closed K" "K \<subseteq> space M - B"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -258,9 +258,10 @@
     fix x i assume "x \<in> ?A' i" thus "x \<in> ?r"
       by (auto intro!: exI[of _ "from_nat i"])
   qed
-  have **: "range ?A' = range A"
-    using surj_from_nat
-    by (auto simp: image_comp [symmetric] intro!: imageI)
+  have "A ` range from_nat = range A"
+    using surj_from_nat by simp
+  then have **: "range ?A' = range A"
+    by (simp only: image_comp [symmetric])
   show ?thesis unfolding * ** ..
 qed
 
@@ -269,7 +270,7 @@
 proof cases
   assume "X \<noteq> {}"
   hence "\<Union>X = (\<Union>n. from_nat_into X n)"
-    using assms by (auto intro: from_nat_into) (metis from_nat_into_surj)
+    using assms by (auto cong del: SUP_cong)
   also have "\<dots> \<in> M" using assms
     by (auto intro!: countable_nat_UN) (metis \<open>X \<noteq> {}\<close> from_nat_into set_mp)
   finally show ?thesis .
@@ -501,11 +502,13 @@
 lemma sigma_sets_top: "sp \<in> sigma_sets sp A"
   by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
 
+lemma binary_in_sigma_sets:
+  "binary a b i \<in> sigma_sets sp A" if "a \<in> sigma_sets sp A" and "b \<in> sigma_sets sp A"
+  using that by (simp add: binary_def)
+
 lemma sigma_sets_Un:
-  "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
-apply (simp add: Un_range_binary range_binary_eq)
-apply (rule Union, simp add: binary_def)
-done
+  "a \<union> b \<in> sigma_sets sp A" if "a \<in> sigma_sets sp A" and "b \<in> sigma_sets sp A"
+  using that by (simp add: Un_range_binary binary_in_sigma_sets Union)
 
 lemma sigma_sets_Inter:
   assumes Asb: "A \<subseteq> Pow sp"
@@ -540,14 +543,9 @@
 qed
 
 lemma sigma_sets_UNION:
-  "countable B \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets X A) \<Longrightarrow> (\<Union>B) \<in> sigma_sets X A"
-  apply (cases "B = {}")
-  apply (simp add: sigma_sets.Empty)
+  "countable B \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets X A) \<Longrightarrow> \<Union> B \<in> sigma_sets X A"
   using from_nat_into [of B] range_from_nat_into [of B] sigma_sets.Union [of "from_nat_into B" X A]
-  apply simp
-  apply auto
-  apply (metis Sup_bot_conv(1) Union_empty \<open>\<lbrakk>B \<noteq> {}; countable B\<rbrakk> \<Longrightarrow> range (from_nat_into B) = B\<close>)
-  done
+  by (cases "B = {}") (simp_all add: sigma_sets.Empty cong del: SUP_cong)
 
 lemma (in sigma_algebra) sigma_sets_eq:
      "sigma_sets \<Omega> M = M"
@@ -1203,7 +1201,7 @@
   have "disjoint_family ?f" unfolding disjoint_family_on_def
     using \<open>D \<in> M\<close>[THEN sets_into_space] \<open>D \<subseteq> E\<close> by auto
   ultimately have "\<Omega> - (D \<union> (\<Omega> - E)) \<in> M"
-    using sets by auto
+    using sets UN by auto
   also have "\<Omega> - (D \<union> (\<Omega> - E)) = E - D"
     using assms sets_into_space by auto
   finally show ?thesis .
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -551,16 +551,25 @@
 by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute)
 
 lemma closure_open_segment [simp]:
-    fixes a :: "'a::euclidean_space"
-    shows "closure(open_segment a b) = (if a = b then {} else closed_segment a b)"
-proof -
-  have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}" if "a \<noteq> b"
+  "closure (open_segment a b) = (if a = b then {} else closed_segment a b)"
+    for a :: "'a::euclidean_space"
+proof (cases "a = b")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}"
     apply (rule closure_injective_linear_image [symmetric])
-    apply (simp add:)
-    using that by (simp add: inj_on_def)
+     apply (use False in \<open>auto intro!: injI\<close>)
+    done
+  then have "closure
+     ((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) =
+    (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}"
+    using closure_translation [of a "((\<lambda>x. x *\<^sub>R b - x *\<^sub>R a) ` {0<..<1})"]
+    by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image)
   then show ?thesis
-    by (simp add: segment_image_interval segment_eq_compose closure_greaterThanLessThan [symmetric]
-         closure_translation image_comp [symmetric] del: closure_greaterThanLessThan)
+    by (simp add: segment_image_interval closure_greaterThanLessThan [symmetric] del: closure_greaterThanLessThan)
 qed
 
 lemma closed_open_segment_iff [simp]:
@@ -574,13 +583,14 @@
 lemma convex_closed_segment [iff]: "convex (closed_segment a b)"
   unfolding segment_convex_hull by(rule convex_convex_hull)
 
-lemma convex_open_segment [iff]: "convex(open_segment a b)"
-proof -
-  have "convex ((\<lambda>u. u *\<^sub>R (b-a)) ` {0<..<1})"
+lemma convex_open_segment [iff]: "convex (open_segment a b)"
+proof -
+  have "convex ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})"
     by (rule convex_linear_image) auto
+  then have "convex ((+) a ` (\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})"
+    by (rule convex_translation)
   then show ?thesis
-    apply (simp add: open_segment_image_interval segment_eq_compose)
-    by (metis image_comp convex_translation)
+    by (simp add: image_image open_segment_image_interval segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right)
 qed
 
 lemmas convex_segment = convex_closed_segment convex_open_segment
@@ -1705,7 +1715,7 @@
         convex_translation[of S "-a"] assms
       by auto
     then have "rel_interior S \<noteq> {}"
-      using rel_interior_translation by auto
+      using rel_interior_translation [of "- a"] by simp
   }
   then show ?thesis
     using rel_interior_empty by auto
@@ -5568,11 +5578,11 @@
   show ?thesis
   proof (cases "c = 0")
     case True show ?thesis
-    apply (simp add: aff_dim_eq_dim [of c] affine_hull_span_gen [of c] \<open>c \<in> S\<close> hull_inc dim_eq_hyperplane
-                del: One_nat_def)
-    apply (rule ex_cong)
-    apply (metis (mono_tags) span_0 \<open>c = 0\<close> image_add_0 inner_zero_right mem_Collect_eq)
-    done
+      using span_zero [of S]
+        apply (simp add: aff_dim_eq_dim [of c] affine_hull_span_gen [of c] \<open>c \<in> S\<close> hull_inc dim_eq_hyperplane
+          del: One_nat_def)
+        apply (auto simp add: \<open>c = 0\<close>)
+        done
   next
     case False
     have xc_im: "x \<in> (+) c ` {y. a \<bullet> y = 0}" if "a \<bullet> x = a \<bullet> c" for a x
@@ -5598,7 +5608,7 @@
     qed
     show ?thesis
       apply (simp add: aff_dim_eq_dim [of c] affine_hull_span_gen [of c] \<open>c \<in> S\<close> hull_inc dim_eq_hyperplane
-                  del: One_nat_def, safe)
+                  del: One_nat_def cong: image_cong_simp, safe)
       apply (fastforce simp add: inner_distrib intro: xc_im)
       apply (force simp: intro!: 2)
       done
@@ -5625,7 +5635,8 @@
   show ?thesis using S
     apply (simp add: hull_redundant cong: aff_dim_affine_hull2)
     apply (simp add: affine_hull_insert_span_gen hull_inc)
-    by (force simp add:span_zero insert_commute [of a] hull_inc aff_dim_eq_dim [of x] dim_insert)
+    by (force simp add: span_zero insert_commute [of a] hull_inc aff_dim_eq_dim [of x] dim_insert
+      cong: image_cong_simp)
 qed
 
 lemma affine_dependent_choose:
@@ -5844,9 +5855,9 @@
                 and "a \<noteq> 0" and "a \<bullet> z \<le> b"
                 and "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b"
 proof -
-from separating_hyperplane_set_0_inspan [of "image (\<lambda>x. -z + x) S"]
+  from separating_hyperplane_set_0_inspan [of "image (\<lambda>x. -z + x) S"]
   have "convex ((+) (- z) ` S)"
-    by (simp add: \<open>convex S\<close>)
+    using \<open>convex S\<close> by simp
   moreover have "(+) (- z) ` S \<noteq> {}"
     by (simp add: \<open>S \<noteq> {}\<close>)
   moreover have "0 \<notin> (+) (- z) ` S"
@@ -6351,10 +6362,10 @@
     by (metis add.left_commute c inner_right_distrib pth_d)
   ultimately have "{x + y |x y. x \<in> S \<and> a \<bullet> y = b} = ?U"
     by (fastforce simp: algebra_simps)
-  also have "... = (+) (c+c) ` UNIV"
-    by (simp add: affine_hyperplane_sums_eq_UNIV_0 [OF aff 0 dc adc])
+  also have "... = range ((+) (c + c))"
+    by (simp only: affine_hyperplane_sums_eq_UNIV_0 [OF aff 0 dc adc])
   also have "... = UNIV"
-    by (simp add: translation_UNIV)
+    by simp
   finally show ?thesis .
 qed
 
@@ -6382,17 +6393,17 @@
 proof -
   obtain a where a: "a \<in> S" "a \<in> T" using assms by force
   have aff: "affine ((+) (-a) ` S)"  "affine ((+) (-a) ` T)"
-    using assms by (auto simp: affine_translation [symmetric])
+    using affine_translation [symmetric, of "- a"] assms by (simp_all cong: image_cong_simp)
   have zero: "0 \<in> ((+) (-a) ` S)"  "0 \<in> ((+) (-a) ` T)"
     using a assms by auto
-  have [simp]: "{x + y |x y. x \<in> (+) (- a) ` S \<and> y \<in> (+) (- a) ` T} =
-        (+) (- 2 *\<^sub>R a) ` {x + y| x y. x \<in> S \<and> y \<in> T}"
+  have "{x + y |x y. x \<in> (+) (- a) ` S \<and> y \<in> (+) (- a) ` T} =
+      (+) (- 2 *\<^sub>R a) ` {x + y| x y. x \<in> S \<and> y \<in> T}"
     by (force simp: algebra_simps scaleR_2)
-  have [simp]: "(+) (- a) ` S \<inter> (+) (- a) ` T = (+) (- a) ` (S \<inter> T)"
+  moreover have "(+) (- a) ` S \<inter> (+) (- a) ` T = (+) (- a) ` (S \<inter> T)"
     by auto
-  show ?thesis
-    using aff_dim_sums_Int_0 [OF aff zero]
-    by (auto simp: aff_dim_translation_eq)
+  ultimately show ?thesis
+    using aff_dim_sums_Int_0 [OF aff zero] aff_dim_translation_eq
+    by (metis (lifting))
 qed
 
 lemma aff_dim_affine_Int_hyperplane:
@@ -6910,7 +6921,7 @@
         using \<open>0 < e\<close> inj_on_def by fastforce
     qed
     also have "... = aff_dim S"
-      using \<open>a \<in> S\<close> aff_dim_eq_dim hull_inc by force
+      using \<open>a \<in> S\<close> aff_dim_eq_dim hull_inc by (force cong: image_cong_simp)
     finally show "aff_dim T \<le> aff_dim S" .
   qed
 qed
@@ -7002,7 +7013,8 @@
   then have "subspace ((+) (- z) ` S)"
     by (meson IntD1 affine_diffs_subspace \<open>affine S\<close>)
   moreover have "int (dim ((+) (- z) ` T)) < int (dim ((+) (- z) ` S))"
-    using z less by (simp add: aff_dim_eq_dim [symmetric] hull_inc)
+thm aff_dim_eq_dim
+    using z less by (simp add: aff_dim_eq_dim_subtract [of z] hull_inc cong: image_cong_simp)
   ultimately have "closure(((+) (- z) ` S) - ((+) (- z) ` T)) = ((+) (- z) ` S)"
     by (simp add: dense_complement_subspace)
   then show ?thesis
@@ -7082,9 +7094,9 @@
     by (auto simp: subspace_imp_affine)
   obtain a' a'' where a': "a' \<in> span ((+) (- z) ` S)" and a: "a = a' + a''"
                   and "\<And>w. w \<in> span ((+) (- z) ` S) \<Longrightarrow> orthogonal a'' w"
-      using orthogonal_subspace_decomp_exists [of "(+) (- z) ` S" "a"] by metis
+    using orthogonal_subspace_decomp_exists [of "(+) (- z) ` S" "a"] by metis
   then have "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> (w-z) = 0"
-    by (simp add: imageI orthogonal_def span)
+    by (simp add: span_base orthogonal_def)
   then have a'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = (a - a') \<bullet> z"
     by (simp add: a inner_diff_right)
   then have ba'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = b - a' \<bullet> z"
@@ -7168,7 +7180,7 @@
     have 2: "{x - f a| x. x \<in> f ` T} = f ` {x - a| x. x \<in> T}"
       by (force simp: linear_diff [OF assms])
     have "aff_dim (f ` T) = int (dim {x - f a |x. x \<in> f ` T})"
-      by (simp add: \<open>a \<in> T\<close> hull_inc aff_dim_eq_dim [of "f a"] 1)
+      by (simp add: \<open>a \<in> T\<close> hull_inc aff_dim_eq_dim [of "f a"] 1 cong: image_cong_simp)
     also have "... = int (dim (f ` {x - a| x. x \<in> T}))"
       by (force simp: linear_diff [OF assms] 2)
     also have "... \<le> int (dim {x - a| x. x \<in> T})"
@@ -7211,7 +7223,7 @@
   case False
   with assms obtain a where "a \<in> S" "0 \<le> d" by auto
   with assms have ss: "subspace ((+) (- a) ` S)"
-    by (simp add: affine_diffs_subspace)
+    by (simp add: affine_diffs_subspace_subtract cong: image_cong_simp)
   have "nat d \<le> dim ((+) (- a) ` S)"
     by (metis aff_dim_subspace aff_dim_translation_eq dle nat_int nat_mono ss)
   then obtain T where "subspace T" and Tsb: "T \<subseteq> span ((+) (- a) ` S)"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1531,11 +1531,11 @@
   then show ?thesis
     apply (rule **)
     subgoal
-      apply (simp add: abs_diff_le_iff field_simps Collect_conj_eq setcompr_eq_image[symmetric])
+      apply (simp add: abs_diff_le_iff field_simps Collect_conj_eq setcompr_eq_image [symmetric] cong: image_cong_simp)
       apply (rule equalityI)
       apply blast
       apply clarsimp
-      apply (rule_tac x="l \<inter> {x. c + e \<ge> x \<bullet> k}" in exI)
+      apply (rule_tac x="xa \<inter> {x. c + e \<ge> x \<bullet> k}" in exI)
       apply auto
       done
     by (simp add: interval_split k interval_doublesplit)
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Analysis/Winding_Numbers.thy
--- a/src/HOL/Analysis/Winding_Numbers.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Winding_Numbers.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -105,7 +105,7 @@
   have 0: "0 \<in> interior(convex hull {a-z, b-z, c-z})"
     using assms convex_hull_translation [of "-z" "{a,b,c}"]
                 interior_translation [of "-z"]
-    by simp
+    by (simp cong: image_cong_simp)
   show ?thesis using wn_triangle2_0 [OF 0]
     by simp
 qed
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1069,9 +1069,9 @@
   assumes "r =o oone" and s: "Well_order s"
   shows "r ^o s =o oone" (is "?L =o ?R")
 proof -
-  from assms obtain f where *: "\<forall>x\<in>Field r. \<forall>y\<in>Field r. x = y" and "f ` Field r = {()}"
+  from \<open>r =o oone\<close> obtain f where *: "\<forall>x\<in>Field r. \<forall>y\<in>Field r. x = y" and "f ` Field r = {()}"
     and r: "Well_order r"
-    unfolding ordIso_def oone_def by (auto simp: iso_def bij_betw_def inj_on_def)
+    unfolding ordIso_def oone_def by (auto simp add: iso_def [abs_def] bij_betw_def inj_on_def)
   then obtain x where "x \<in> Field r" by auto
   with * have Fr: "Field r = {x}" by auto
   interpret r: wo_rel r by unfold_locales (rule r)
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -950,7 +950,7 @@
      unfolding underS_def Field_def bij_betw_def by auto
      have fa: "f a \<in> Field s" using f[OF a] by auto
      have g: "g a = suc s (g ` underS r a)"
-     using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by simp
+       using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by blast
      have A0: "g ` underS r a \<subseteq> Field s"
      using IH1b by (metis IH2 image_subsetI in_mono under_Field)
      {fix a1 assume a1: "a1 \<in> underS r a"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Fun.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -599,15 +599,33 @@
 context cancel_semigroup_add
 begin
 
-lemma inj_add_left [simp]: \<open>inj ((+) a)\<close>
-  by (rule injI) simp
+lemma inj_on_add [simp]:
+  "inj_on ((+) a) A"
+  by (rule inj_onI) simp
+
+lemma inj_add_left:
+  \<open>inj ((+) a)\<close>
+  by simp
+
+lemma inj_on_add' [simp]:
+  "inj_on (\<lambda>b. b + a) A"
+  by (rule inj_onI) simp
+
+lemma bij_betw_add [simp]:
+  "bij_betw ((+) a) A B \<longleftrightarrow> (+) a ` A = B"
+  by (simp add: bij_betw_def)
 
 end
 
 context ab_group_add
 begin
 
-lemma inj_diff_right [simp]: \<open>inj (\<lambda>b. b - a)\<close>
+lemma surj_plus [simp]:
+  "surj ((+) a)"
+  by (auto intro: range_eqI [of b "(+) a" "b - a" for b] simp add: algebra_simps)
+
+lemma inj_diff_right [simp]:
+  \<open>inj (\<lambda>b. b - a)\<close>
 proof -
   have \<open>inj ((+) (- a))\<close>
     by (fact inj_add_left)
@@ -616,6 +634,38 @@
   finally show ?thesis .
 qed
 
+lemma surj_diff_right [simp]:
+  "surj (\<lambda>x. x - a)"
+  using surj_plus [of "- a"] by (simp cong: image_cong_simp)
+
+lemma translation_Compl:
+  "(+) a ` (- t) = - ((+) a ` t)"
+proof (rule set_eqI)
+  fix b
+  show "b \<in> (+) a ` (- t) \<longleftrightarrow> b \<in> - (+) a ` t"
+    by (auto simp: image_iff algebra_simps intro!: bexI [of _ "b - a"])
+qed
+
+lemma translation_subtract_Compl:
+  "(\<lambda>x. x - a) ` (- t) = - ((\<lambda>x. x - a) ` t)"
+  using translation_Compl [of "- a" t] by (simp cong: image_cong_simp)
+
+lemma translation_diff:
+  "(+) a ` (s - t) = ((+) a ` s) - ((+) a ` t)"
+  by auto
+
+lemma translation_subtract_diff:
+  "(\<lambda>x. x - a) ` (s - t) = ((\<lambda>x. x - a) ` s) - ((\<lambda>x. x - a) ` t)"
+  using translation_diff [of "- a"] by (simp cong: image_cong_simp)
+
+lemma translation_Int:
+  "(+) a ` (s \<inter> t) = ((+) a ` s) \<inter> ((+) a ` t)"
+  by auto
+
+lemma translation_subtract_Int:
+  "(\<lambda>x. x - a) ` (s \<inter> t) = ((\<lambda>x. x - a) ` s) \<inter> ((\<lambda>x. x - a) ` t)"
+  using translation_Int [of " -a"] by (simp cong: image_cong_simp)
+
 end
 
 
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/HOLCF/Universal.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -620,24 +620,29 @@
 apply (erule cb_take_mono)
 done
 
-function
-  basis_emb :: "'a compact_basis \<Rightarrow> ubasis"
-where
-  "basis_emb x = (if x = compact_bot then 0 else
+function basis_emb :: "'a compact_basis \<Rightarrow> ubasis"
+  where "basis_emb x = (if x = compact_bot then 0 else
     node (place x) (basis_emb (sub x))
       (basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y}))"
-by auto
+  by simp_all
 
 termination basis_emb
-apply (relation "measure place", simp)
-apply (simp add: place_sub_less)
-apply simp
-done
+  by (relation "measure place") (simp_all add: place_sub_less)
 
 declare basis_emb.simps [simp del]
 
-lemma basis_emb_compact_bot [simp]: "basis_emb compact_bot = 0"
-by (simp add: basis_emb.simps)
+lemma basis_emb_compact_bot [simp]:
+  "basis_emb compact_bot = 0"
+  using basis_emb.simps [of compact_bot] by simp
+
+lemma basis_emb_rec:
+  "basis_emb x = node (place x) (basis_emb (sub x)) (basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y})"
+  if "x \<noteq> compact_bot"
+  using that basis_emb.simps [of x] by simp
+
+lemma basis_emb_eq_0_iff [simp]:
+  "basis_emb x = 0 \<longleftrightarrow> x = compact_bot"
+  by (cases "x = compact_bot") (simp_all add: basis_emb_rec)
 
 lemma fin1: "finite {y. place y < place x \<and> x \<sqsubseteq> y}"
 apply (subst Collect_conj_eq)
@@ -700,15 +705,12 @@
 qed
 
 lemma inj_basis_emb: "inj basis_emb"
- apply (rule inj_onI)
- apply (case_tac "x = compact_bot")
-  apply (case_tac [!] "y = compact_bot")
-    apply simp
-   apply (simp add: basis_emb.simps)
-  apply (simp add: basis_emb.simps)
- apply (simp add: basis_emb.simps)
- apply (simp add: fin2 inj_eq [OF inj_place])
-done
+proof (rule injI)
+  fix x y
+  assume "basis_emb x = basis_emb y"
+  then show "x = y"
+    by (cases "x = compact_bot \<or> y = compact_bot") (auto simp add: basis_emb_rec fin2 place_eqD)
+qed
 
 definition
   basis_prj :: "ubasis \<Rightarrow> 'a compact_basis"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/IMP/Denotational.thy
--- a/src/HOL/IMP/Denotational.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/IMP/Denotational.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -81,7 +81,7 @@
   let ?S = "\<lambda>n::nat. if n=0 then a else b"
   have "chain ?S" using \<open>a \<subseteq> b\<close> by(auto simp: chain_def)
   hence "f(UN n. ?S n) = (UN n. f(?S n))"
-    using assms by(simp add: cont_def)
+    using assms by (simp add: cont_def del: if_image_distrib)
   moreover have "(UN n. ?S n) = b" using \<open>a \<subseteq> b\<close> by (auto split: if_splits)
   moreover have "(UN n. f(?S n)) = f a \<union> f b" by (auto split: if_splits)
   ultimately show "f a \<subseteq> f b" by (metis Un_upper1)
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/AList.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -82,7 +82,7 @@
   by (simp add: update_conv' map_upd_Some_unfold)
 
 lemma image_update [simp]: "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
-  by (simp add: update_conv')
+  by (auto simp add: update_conv')
 
 qualified definition updates ::
     "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/Countable_Set.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -334,16 +334,13 @@
   using S[THEN subset_range_from_nat_into] by auto
 
 lemma finite_sequence_to_countable_set:
-   assumes "countable X" obtains F where "\<And>i. F i \<subseteq> X" "\<And>i. F i \<subseteq> F (Suc i)" "\<And>i. finite (F i)" "(\<Union>i. F i) = X"
-proof -  show thesis
+  assumes "countable X"
+  obtains F where "\<And>i. F i \<subseteq> X" "\<And>i. F i \<subseteq> F (Suc i)" "\<And>i. finite (F i)" "(\<Union>i. F i) = X"
+proof -
+  show thesis
     apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"])
-    apply (auto simp: image_iff Ball_def intro: from_nat_into split: if_split_asm)
-  proof -
-    fix x n assume "x \<in> X" "\<forall>i m. m \<le> i \<longrightarrow> x \<noteq> from_nat_into X m"
-    with from_nat_into_surj[OF \<open>countable X\<close> \<open>x \<in> X\<close>]
-    show False
-      by auto
-  qed
+       apply (auto simp add: image_iff intro: from_nat_into split: if_splits)
+    using assms from_nat_into_surj by (fastforce cong: image_cong)
 qed
 
 lemma transfer_countable[transfer_rule]:
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1954,7 +1954,7 @@
     have "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) = (SUP i\<in>I. f i + (SUP i\<in>I. g i))"
       by (intro ennreal_SUP_add_left[symmetric] \<open>I \<noteq> {}\<close>)
     also have "\<dots> = (SUP i\<in>I. (SUP j\<in>I. f i + g j))"
-      by (intro SUP_cong refl ennreal_SUP_add_right \<open>I \<noteq> {}\<close>)
+      using \<open>I \<noteq> {}\<close> by (simp add: ennreal_SUP_add_right)
     also have "\<dots> \<le> (SUP i\<in>I. f i + g i)"
       using directed by (intro SUP_least) (blast intro: SUP_upper2)
     finally show "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) \<le> (SUP i\<in>I. f i + g i)" .
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/Extended_Real.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -2396,7 +2396,7 @@
     have "(INF i\<in>I. f i + g i) \<le> (INF i\<in>I. (INF j\<in>I. f i + g j))"
       using directed by (intro INF_greatest) (blast intro: INF_lower2)
     also have "\<dots> = (INF i\<in>I. f i + (INF i\<in>I. g i))"
-      using nonneg by (intro INF_cong refl INF_ereal_add_right \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
+      using nonneg \<open>I \<noteq> {}\<close> by (auto simp: INF_ereal_add_right)
     also have "\<dots> = (INF i\<in>I. f i) + (INF i\<in>I. g i)"
       using nonneg by (intro INF_ereal_add_left \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
     finally show "(INF i\<in>I. f i + g i) \<le> (INF i\<in>I. f i) + (INF i\<in>I. g i)" .
@@ -3691,7 +3691,7 @@
     then have "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) = (SUP i\<in>I. f i + (SUP i\<in>I. g i))"
       by (intro SUP_ereal_add_left[symmetric] \<open>I \<noteq> {}\<close>) auto
     also have "\<dots> = (SUP i\<in>I. (SUP j\<in>I. f i + g j))"
-      using nonneg(1) by (intro SUP_cong refl SUP_ereal_add_right[symmetric] \<open>I \<noteq> {}\<close>) auto
+      using nonneg(1) \<open>I \<noteq> {}\<close> by (simp add: SUP_ereal_add_right)
     also have "\<dots> \<le> (SUP i\<in>I. f i + g i)"
       using directed by (intro SUP_least) (blast intro: SUP_upper2)
     finally show "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) \<le> (SUP i\<in>I. f i + g i)" .
@@ -4228,7 +4228,7 @@
   assume "?lhs" "x \<in> A"
   from \<open>x \<in> A\<close> have "f x \<le> (SUP x\<in>A. f x)" by(rule SUP_upper)
   with \<open>?lhs\<close> show "f x = 0" using nonneg \<open>x \<in> A\<close> by auto
-qed(simp cong: SUP_cong add: A)
+qed (simp add: A)
 
 lemma ereal_divide_le_posI:
   fixes x y z :: ereal
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -64,12 +64,17 @@
 
 lemma infinite_int_iff_infinite_nat_abs: "infinite S \<longleftrightarrow> infinite ((nat \<circ> abs) ` S)"
   for S :: "int set"
-proof -
-  have "inj_on nat (abs ` A)" for A
+proof (unfold Not_eq_iff, rule iffI)
+  assume "finite ((nat \<circ> abs) ` S)"
+  then have "finite (nat ` (abs ` S))"
+    by (simp add: image_image cong: image_cong)
+  moreover have "inj_on nat (abs ` S)"
     by (rule inj_onI) auto
-  then show ?thesis
-    by (auto simp flip: image_comp dest: finite_image_absD finite_imageD)
-qed
+  ultimately have "finite (abs ` S)"
+    by (rule finite_imageD)
+  then show "finite S"
+    by (rule finite_image_absD)
+qed simp
 
 proposition infinite_int_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
   for S :: "int set"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/Liminf_Limsup.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -114,9 +114,11 @@
   have "\<And>P. eventually P F \<Longrightarrow> (SUP x \<in> {x. P x}. c) = c"
     using ntriv by (intro SUP_const) (auto simp: eventually_False *)
   then show ?thesis
-    unfolding Limsup_def using eventually_True
-    by (subst INF_cong[where D="\<lambda>x. c"])
-       (auto intro!: INF_const simp del: eventually_True)
+    apply (auto simp add: Limsup_def)
+    apply (rule INF_const)
+    apply auto
+    using eventually_True apply blast
+    done
 qed
 
 lemma Liminf_const:
@@ -127,9 +129,11 @@
   have "\<And>P. eventually P F \<Longrightarrow> (INF x \<in> {x. P x}. c) = c"
     using ntriv by (intro INF_const) (auto simp: eventually_False *)
   then show ?thesis
-    unfolding Liminf_def using eventually_True
-    by (subst SUP_cong[where D="\<lambda>x. c"])
-       (auto intro!: SUP_const simp del: eventually_True)
+    apply (auto simp add: Liminf_def)
+    apply (rule SUP_const)
+    apply auto
+    using eventually_True apply blast
+    done
 qed
 
 lemma Liminf_mono:
@@ -436,8 +440,8 @@
     by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
   also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
-    by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
-       (auto dest!: eventually_happens simp: F)
+    using * continuous_at_Inf_mono [OF am continuous_on_imp_continuous_within [OF c]]
+    by auto 
   finally show ?thesis by (auto simp: Liminf_def)
 qed
 
@@ -461,8 +465,8 @@
     by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
   also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
-    by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
-       (auto dest!: eventually_happens simp: F)
+    using * continuous_at_Sup_mono [OF am continuous_on_imp_continuous_within [OF c]]
+    by auto
   finally show ?thesis by (auto simp: Limsup_def)
 qed
 
@@ -485,8 +489,8 @@
     by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
   also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
-    by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
-       (auto dest!: eventually_happens simp: F)
+    using * continuous_at_Sup_antimono [OF am continuous_on_imp_continuous_within [OF c]]
+    by auto
   finally show ?thesis
     by (auto simp: Liminf_def)
 qed
@@ -511,8 +515,8 @@
     by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
   also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
-    by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
-       (auto dest!: eventually_happens simp: F)
+    using * continuous_at_Inf_antimono [OF am continuous_on_imp_continuous_within [OF c]]
+    by auto
   finally show ?thesis
     by (auto simp: Limsup_def)
 qed
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/Multiset_Permutations.thy
--- a/src/HOL/Library/Multiset_Permutations.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/Multiset_Permutations.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -170,7 +170,7 @@
           (\<Prod>y\<in>set_mset (A+{#x#}). (if y = x then count A x + 1 else 1) * fact (count A y))"
     by (intro prod.cong) simp_all
   also have "\<dots> = (count A x + 1) * (\<Prod>y\<in>set_mset (A+{#x#}). fact (count A y))"
-    by (simp add: prod.distrib prod.delta)
+    by (simp add: prod.distrib)
   also have "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count A y)) = (\<Prod>y\<in>set_mset A. fact (count A y))"
     by (intro prod.mono_neutral_right) (auto simp: not_in_iff)
   finally show ?thesis .
@@ -436,7 +436,11 @@
                 (\<Union>y\<in>A. permutations_of_set_aux (y#acc) (A - {y}))"
         by (subst permutations_of_set_aux.simps) simp_all
       also have "\<dots> = (\<Union>y\<in>A. (\<lambda>xs. rev xs @ acc) ` (\<lambda>xs. y # xs) ` permutations_of_set (A - {y}))"
-        by (intro SUP_cong refl, subst psubset) (auto simp: image_image)
+        apply (rule arg_cong [of _ _ Union], rule image_cong)
+         apply (simp_all add: image_image)
+        apply (subst psubset)
+         apply auto
+        done
       also from False have "\<dots> = (\<lambda>xs. rev xs @ acc) ` permutations_of_set A"
         by (subst (2) permutations_of_set_nonempty) (simp_all add: image_UN)
       finally show ?thesis .
@@ -473,7 +477,7 @@
   by (induction acc xs rule: permutations_of_set_aux_list.induct)
      (subst permutations_of_set_aux_list.simps,
       subst permutations_of_set_aux.simps,
-      simp_all add: set_list_bind cong: SUP_cong)
+      simp_all add: set_list_bind)
 
 
 text \<open>
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/Numeral_Type.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -408,15 +408,22 @@
 definition "enum_class.enum_all P = (\<forall>b :: 'a bit0 \<in> set enum_class.enum. P b)"
 definition "enum_class.enum_ex P = (\<exists>b :: 'a bit0 \<in> set enum_class.enum. P b)"
 
-instance
-proof(intro_classes)
+instance proof
   show "distinct (enum_class.enum :: 'a bit0 list)"
     by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject)
 
-  show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
-    unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
-    by (simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
-      (auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def)
+  let ?Abs = "Abs_bit0 :: _ \<Rightarrow> 'a bit0"
+  interpret type_definition Rep_bit0 ?Abs "{0..<2 * int CARD('a)}"
+    by (fact type_definition_bit0)
+  have "UNIV = ?Abs ` {0..<2 * int CARD('a)}"
+    by (simp add: Abs_image)
+  also have "\<dots> = ?Abs ` (int ` {0..<2 * CARD('a)})"
+    by (simp add: image_int_atLeastLessThan)
+  also have "\<dots> = (?Abs \<circ> int) ` {0..<2 * CARD('a)}"
+    by (simp add: image_image cong: image_cong)
+  also have "\<dots> = set enum_class.enum"
+    by (simp add: enum_bit0_def Abs_bit0'_def cong: image_cong_simp)
+  finally show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum" .
 
   fix P :: "'a bit0 \<Rightarrow> bool"
   show "enum_class.enum_all P = Ball UNIV P"
@@ -437,10 +444,17 @@
     by(simp only: Abs_bit1'_def zmod_int[symmetric] enum_bit1_def distinct_map Suc_eq_plus1 card_bit1 o_apply inj_on_def)
       (clarsimp simp add: Abs_bit1_inject)
 
-  show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
-    unfolding enum_bit1_def type_definition.Abs_image[OF type_definition_bit1, symmetric]
-    by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
-      (auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def)
+  let ?Abs = "Abs_bit1 :: _ \<Rightarrow> 'a bit1"
+  interpret type_definition Rep_bit1 ?Abs "{0..<1 + 2 * int CARD('a)}"
+    by (fact type_definition_bit1)
+  have "UNIV = ?Abs ` {0..<1 + 2 * int CARD('a)}"
+    by (simp add: Abs_image)
+  also have "\<dots> = ?Abs ` (int ` {0..<1 + 2 * CARD('a)})"
+    by (simp add: image_int_atLeastLessThan)
+  also have "\<dots> = (?Abs \<circ> int) ` {0..<1 + 2 * CARD('a)}"
+    by (simp add: image_image cong: image_cong)
+  finally show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
+    by (simp only: enum_bit1_def set_map set_upt) (simp add: Abs_bit1'_def cong: image_cong_simp)
 
   fix P :: "'a bit1 \<Rightarrow> bool"
   show "enum_class.enum_all P = Ball UNIV P"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/Option_ord.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -401,12 +401,13 @@
       from this have [simp]: "(\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None}))))"
         apply (simp add: Inf_option_def image_def Option.these_def)
         by (rule Inf_greatest, clarsimp)
-
       have [simp]: "the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None})))) \<in> Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
-        apply (simp add:  Option.these_def image_def)
-        apply (rule exI [of _ "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x}))"], simp)
-        by (simp add: Inf_option_def)
-
+        apply (auto simp add: Option.these_def)
+        apply (rule imageI)
+        apply auto
+        using \<open>\<And>Y. Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y\<close> apply blast
+        apply (auto simp add: Some_INF [symmetric])
+        done
       have "(\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
         by (rule Sup_upper2 [of "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))"], simp_all)
     }
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/Order_Continuity.thy
--- a/src/HOL/Library/Order_Continuity.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/Order_Continuity.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -12,21 +12,15 @@
 (* TODO: Generalize theory to chain-complete partial orders *)
 
 lemma SUP_nat_binary:
-  "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::countable_complete_lattice)"
-  apply (auto intro!: antisym ccSUP_least)
-  apply (rule ccSUP_upper2[where i=0])
-  apply simp_all
-  apply (rule ccSUP_upper2[where i=1])
-  apply simp_all
+  "(sup A (SUP x\<in>Collect ((<) (0::nat)). B)) = (sup A B::'a::countable_complete_lattice)"
+  apply (subst image_constant)
+   apply auto
   done
 
 lemma INF_nat_binary:
-  "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::countable_complete_lattice)"
-  apply (auto intro!: antisym ccINF_greatest)
-  apply (rule ccINF_lower2[where i=0])
-  apply simp_all
-  apply (rule ccINF_lower2[where i=1])
-  apply simp_all
+  "inf A (INF x\<in>Collect ((<) (0::nat)). B) = (inf A B::'a::countable_complete_lattice)"
+  apply (subst image_constant)
+   apply auto
   done
 
 text \<open>
@@ -48,15 +42,24 @@
   by (auto simp: sup_continuous_def)
 
 lemma sup_continuous_mono:
-  assumes [simp]: "sup_continuous F" shows "mono F"
+  "mono F" if "sup_continuous F"
 proof
-  fix A B :: "'a" assume [simp]: "A \<le> B"
-  have "F B = F (SUP n::nat. if n = 0 then A else B)"
-    by (simp add: sup_absorb2 SUP_nat_binary)
-  also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
-    by (auto simp: sup_continuousD mono_def intro!: SUP_cong)
+  fix A B :: "'a"
+  assume "A \<le> B"
+  let ?f = "\<lambda>n::nat. if n = 0 then A else B"
+  from \<open>A \<le> B\<close> have "incseq ?f"
+    by (auto intro: monoI)
+  with \<open>sup_continuous F\<close> have *: "F (SUP i. ?f i) = (SUP i. F (?f i))"
+    by (auto dest: sup_continuousD)
+  thm this [simplified, simplified SUP_nat_binary]
+  from \<open>A \<le> B\<close> have "B = sup A B"
+    by (simp add: le_iff_sup)
+  then have "F B = F (sup A B)"
+    by simp
+  also have "\<dots> = sup (F A) (F B)"
+    using * by (simp add: if_distrib SUP_nat_binary cong del: SUP_cong)
   finally show "F A \<le> F B"
-    by (simp add: SUP_nat_binary le_iff_sup)
+    by (simp add: le_iff_sup)
 qed
 
 lemma [order_continuous_intros]:
@@ -214,15 +217,23 @@
   by (auto simp: inf_continuous_def)
 
 lemma inf_continuous_mono:
-  assumes [simp]: "inf_continuous F" shows "mono F"
+  "mono F" if "inf_continuous F"
 proof
-  fix A B :: "'a" assume [simp]: "A \<le> B"
-  have "F A = F (INF n::nat. if n = 0 then B else A)"
-    by (simp add: inf_absorb2 INF_nat_binary)
-  also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
-    by (auto simp: inf_continuousD antimono_def intro!: INF_cong)
+  fix A B :: "'a"
+  assume "A \<le> B"
+  let ?f = "\<lambda>n::nat. if n = 0 then B else A"
+  from \<open>A \<le> B\<close> have "decseq ?f"
+    by (auto intro: antimonoI)
+  with \<open>inf_continuous F\<close> have *: "F (INF i. ?f i) = (INF i. F (?f i))"
+    by (auto dest: inf_continuousD)
+  from \<open>A \<le> B\<close> have "A = inf B A"
+    by (simp add: inf.absorb_iff2)
+  then have "F A = F (inf B A)"
+    by simp
+  also have "\<dots> = inf (F B) (F A)"
+    using * by (simp add: if_distrib INF_nat_binary cong del: INF_cong)
   finally show "F A \<le> F B"
-    by (simp add: INF_nat_binary le_iff_inf inf_commute)
+    by (simp add: inf.absorb_iff2)
 qed
 
 lemma [order_continuous_intros]:
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/Ramsey.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -231,8 +231,8 @@
       then obtain n where "x = ?gt n" ..
       with pg [of n] show "x \<in> {..<s}" by (cases "g n") auto
     qed
-    have "finite (range ?gt)"
-      by (simp add: finite_nat_iff_bounded rangeg)
+    from rangeg have "finite (range ?gt)"
+      by (simp add: finite_nat_iff_bounded)
     then obtain s' and n' where s': "s' = ?gt n'" and infeqs': "infinite {n. ?gt n = s'}"
       by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: infinite_UNIV_nat)
     with pg [of n'] have less': "s'<s" by (cases "g n'") auto
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -167,12 +167,8 @@
 
 
 lemma comp_wf_syscls: "wf_syscls (comp G) = wf_syscls G"
-  apply (simp add: wf_syscls_def comp_def compClass_def split_beta)
-  apply (simp add: image_comp)
-  apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
-                      (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
-   apply simp
-  apply (simp add: fun_eq_iff split_beta)
+  apply (simp add: wf_syscls_def comp_def compClass_def split_beta cong: image_cong_simp)
+  apply (simp add: image_comp cong: image_cong_simp)
   done
 
 
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Nat.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -166,78 +166,6 @@
 
 text \<open>Injectiveness and distinctness lemmas\<close>
 
-context cancel_ab_semigroup_add
-begin
-
-lemma inj_on_add [simp]:
-  "inj_on (plus a) A"
-proof (rule inj_onI)
-  fix b c
-  assume "a + b = a + c"
-  then have "a + b - a = a + c - a"
-    by (simp only:)
-  then show "b = c"
-    by simp
-qed
-
-lemma inj_on_add' [simp]:
-  "inj_on (\<lambda>b. b + a) A"
-  using inj_on_add [of a A] by (simp add: add.commute [of _ a])
-
-lemma bij_betw_add [simp]:
-  "bij_betw (plus a) A B \<longleftrightarrow> plus a ` A = B"
-  by (simp add: bij_betw_def)
-
-end
-
-text \<open>Translation lemmas\<close>
-
-context ab_group_add
-begin
-
-lemma surj_plus [simp]: "surj (plus a)"
-  by (auto intro: range_eqI [of b "plus a" "b - a" for b] simp add: algebra_simps)
-
-end
-
-lemma translation_Compl:
-  fixes a :: "'a::ab_group_add"
-  shows "(\<lambda>x. a + x) ` (- t) = - ((\<lambda>x. a + x) ` t)"
-  apply (auto simp: image_iff)
-  apply (rule_tac x="x - a" in bexI, auto)
-  done
-
-lemma translation_UNIV:
-  fixes a :: "'a::ab_group_add"
-  shows "range (\<lambda>x. a + x) = UNIV"
-  by (fact surj_plus)
-
-lemma translation_diff:
-  fixes a :: "'a::ab_group_add"
-  shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
-  by auto
-
-lemma translation_Int:
-  fixes a :: "'a::ab_group_add"
-  shows "(\<lambda>x. a + x) ` (s \<inter> t) = ((\<lambda>x. a + x) ` s) \<inter> ((\<lambda>x. a + x) ` t)"
-  by auto
-
-context semidom_divide
-begin
-
-lemma inj_on_mult:
-  "inj_on (times a) A" if "a \<noteq> 0"
-proof (rule inj_onI)
-  fix b c
-  assume "a * b = a * c"
-  then have "a * b div a = a * c div a"
-    by (simp only:)
-  with that show "b = c"
-    by simp
-qed
-
-end
-
 lemma inj_Suc [simp]:
   "inj_on Suc N"
   by (simp add: inj_on_def)
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Probability/Fin_Map.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1037,18 +1037,18 @@
       show "\<forall>A\<in>E i. (\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P \<in> sets ?P"
       proof
         fix A assume A: "A \<in> E i"
-        then have "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P = (\<Pi>' j\<in>I. if i = j then A else space (M j))"
+        from T have *: "\<exists>xs. length xs = card I
+          \<and> (\<forall>j\<in>I. (g)\<^sub>F j \<in> (if i = j then A else S j (xs ! T j)))"
+          if "domain g = I" and "\<forall>j\<in>I. (g)\<^sub>F j \<in> (if i = j then A else S j (f j))" for g f
+          using that by (auto intro!: exI [of _ "map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]"])
+        from A have "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P = (\<Pi>' j\<in>I. if i = j then A else space (M j))"
           using E_closed \<open>i \<in> I\<close> by (auto simp: space_P Pi_iff subset_eq split: if_split_asm)
         also have "\<dots> = (\<Pi>' j\<in>I. \<Union>n. if i = j then A else S j n)"
           by (intro Pi'_cong) (simp_all add: S_union)
+        also have "\<dots> = {g. domain g = I \<and> (\<exists>f. \<forall>j\<in>I. (g)\<^sub>F j \<in> (if i = j then A else S j (f j)))}"
+          by (rule set_eqI) (simp del: if_image_distrib add: Pi'_iff bchoice_iff)
         also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>' j\<in>I. if i = j then A else S j (xs ! T j))"
-          using T
-          apply (auto simp del: Union_iff)
-          apply (simp_all add: Pi'_iff bchoice_iff del: Union_iff)
-          apply (erule conjE exE)+
-          apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
-          apply (auto simp: bij_betw_def)
-          done
+          using * by (auto simp add: Pi'_iff split del: if_split)
         also have "\<dots> \<in> sets ?P"
         proof (safe intro!: sets.countable_UN)
           fix xs show "(\<Pi>' j\<in>I. if i = j then A else S j (xs ! T j)) \<in> sets ?P"
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Probability/Information.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1943,7 +1943,7 @@
   note fX = simple_function_compose[OF X, of f]
   from X have "\<H>(X) = \<H>(f\<circ>X) + \<H>(X|f\<circ>X)" by (rule entropy_partition)
   then show "\<H>(f \<circ> X) \<le> \<H>(X)"
-    by (auto intro: conditional_entropy_nonneg[OF X fX])
+    by (simp only: conditional_entropy_nonneg [OF X fX] le_add_same_cancel1)
 qed
 
 corollary (in information_space) entropy_of_inj:
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Probability/SPMF.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -1350,7 +1350,7 @@
 
   have "(\<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x)) \<partial>count_space UNIV) =
         (\<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x) * indicator ?B x) \<partial>count_space UNIV)"
-    by(intro nn_integral_cong SUP_cong)(auto split: split_indicator simp add: spmf_eq_0_set_spmf)
+    by (intro nn_integral_cong arg_cong [of _ _ Sup]) (auto split: split_indicator simp add: spmf_eq_0_set_spmf)
   also have "\<dots> = (\<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x)) \<partial>count_space ?B)"
     unfolding ennreal_indicator[symmetric] using False
     by(subst SUP_mult_right_ennreal[symmetric])(simp add: ennreal_indicator nn_integral_count_space_indicator)
@@ -1456,7 +1456,7 @@
     finally show "Complete_Partial_Order.chain (\<le>) ((\<lambda>i x. ennreal (spmf i x) * indicator A x) ` Y)" .
   qed simp
   also have "\<dots> = (SUP y\<in>Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>count_space UNIV)"
-    by(auto simp add: nn_integral_count_space_indicator set_lub_spmf spmf_eq_0_set_spmf split: split_indicator intro!: SUP_cong nn_integral_cong)
+    by(auto simp add: nn_integral_count_space_indicator set_lub_spmf spmf_eq_0_set_spmf split: split_indicator intro!: arg_cong [of _ _ Sup] image_cong nn_integral_cong)
   also have "\<dots> = ?rhs"
     by(auto simp add: nn_integral_indicator[symmetric] nn_integral_measure_spmf)
   finally show ?thesis .
@@ -1588,7 +1588,7 @@
     also have "\<dots> = (SUP p\<in>Y. \<integral>\<^sup>+ x. ennreal (spmf p x * spmf (f x) i) \<partial>?M)"
       using Y chain' by(rule nn_integral_monotone_convergence_SUP_countable) simp
     also have "\<dots> = (SUP p\<in>Y. ennreal (spmf (bind_spmf p f) i))"
-      by(auto simp add: ennreal_spmf_bind nn_integral_measure_spmf nn_integral_count_space_indicator set_lub_spmf[OF chain] in_set_spmf_iff_spmf ennreal_mult intro!: SUP_cong nn_integral_cong split: split_indicator)
+      by(auto simp add: ennreal_spmf_bind nn_integral_measure_spmf nn_integral_count_space_indicator set_lub_spmf[OF chain] in_set_spmf_iff_spmf ennreal_mult intro!: arg_cong [of _ _ Sup] image_cong nn_integral_cong split: split_indicator)
     also have "\<dots> = ennreal (spmf ?rhs i)" using chain'' by(simp add: ennreal_spmf_lub_spmf Y)
     finally show "spmf ?lhs i = spmf ?rhs i" by simp
   qed
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Rings.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -10,7 +10,7 @@
 section \<open>Rings\<close>
 
 theory Rings
-  imports Groups Set
+  imports Groups Set Fun
 begin
 
 class semiring = ab_semigroup_add + semigroup_mult +
@@ -733,6 +733,17 @@
   "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
   by (elim dvdE, cases "c = 0") simp_all
 
+lemma inj_on_mult:
+  "inj_on ((*) a) A" if "a \<noteq> 0"
+proof (rule inj_onI)
+  fix b c
+  assume "a * b = a * c"
+  then have "a * b div a = a * c div a"
+    by (simp only:)
+  with that show "b = c"
+    by simp
+qed
+
 end
 
 class idom_divide = idom + semidom_divide
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/UNITY/FP.thy
--- a/src/HOL/UNITY/FP.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/UNITY/FP.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -25,13 +25,16 @@
 by (simp add: FP_Orig_def stable_def, blast)
 
 lemma stable_FP_Int: "F \<in> stable (FP F \<inter> B)"
-apply (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x}) ")
-prefer 2 apply blast
-apply (simp (no_asm_simp) add: Int_insert_right)
-apply (simp add: FP_def stable_def)
-apply (rule constrains_UN)
-apply (simp (no_asm))
-done
+proof -
+  have "F \<in> stable (\<Union>x\<in>B. FP F \<inter> {x})"
+    apply (simp only: Int_insert_right FP_def stable_def)
+    apply (rule constrains_UN)
+    apply simp
+    done
+  also have "(\<Union>x\<in>B. FP F \<inter> {x}) = FP F \<inter> B"
+    by simp
+  finally show ?thesis .
+qed
 
 lemma FP_equivalence: "FP F = FP_Orig F"
 apply (rule equalityI) 
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/UNITY/Transformers.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -359,8 +359,7 @@
       "single_valued act
        ==> wens_single_finite act B (Suc k) =
            wens_single_finite act B k \<union> wp act (wens_single_finite act B k)"
-apply (simp add: wens_single_finite_def image_def 
-                 wp_UN_eq [OF _ atMost_nat_nonempty]) 
+apply (simp add: wens_single_finite_def wp_UN_eq [OF _ atMost_nat_nonempty])
 apply (force elim!: le_SucE)
 done
 
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/ZF/Zet.thy
--- a/src/HOL/ZF/Zet.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/ZF/Zet.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -37,7 +37,7 @@
   apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
   apply (simp add: explode_Repl_eq)
   apply (subgoal_tac "explode z = f ` A")
-  apply (simp_all add: image_comp [symmetric])
+  apply (simp_all add: image_image cong: image_cong_simp)
   done
 
 lemma zet_image_mem:
@@ -98,7 +98,7 @@
 lemma zimplode_zexplode: "zimplode (zexplode z) = z"
   apply (simp add: zimplode_def zexplode_def)
   apply (subst Abs_zet_inverse)
-  apply (auto simp add: explode_mem_zet implode_explode)
+  apply (auto simp add: explode_mem_zet)
   done  
 
 lemma zin_zexplode_eq: "zin x (zexplode A) = Elem x A"