# HG changeset patch
# User haftmann
# Date 1548940139 0
# Node ID 7e4966eaf78105c1e115c9d74c717786c16d2a76
# Parent  d10fafeb93c0c08e12eee6b08183a430393a8e74
proper congruence rule for image operator

diff -r d10fafeb93c0 -r 7e4966eaf781 NEWS
--- a/NEWS	Thu Jan 31 09:30:15 2019 +0100
+++ b/NEWS	Thu Jan 31 13:08:59 2019 +0000
@@ -104,6 +104,11 @@
 * Code generation: slightly more conventional syntax for
 'code_stmts' antiquotation.  Minor INCOMPATIBILITY.
 
+* The simplifier uses image_cong_simp as a congruence rule. The historic
+and not really well-formed congruence rules INF_cong*, SUP_cong*,
+are not used by default any longer.  INCOMPATIBILITY; consider using
+declare image_cong_simp [cong del] in extreme situations.
+
 * Simplified syntax setup for big operators under image. In rare
 situations, type conversions are not inserted implicitly any longer
 and need to be given explicitly. Auxiliary abbreviations INFIMUM,
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Analysis/Caratheodory.thy
--- a/src/HOL/Analysis/Caratheodory.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Analysis/Caratheodory.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -736,8 +736,7 @@
         have Ai_eq: "A i = (\<Union>x<card C. f x)"
           using f C Ai unfolding bij_betw_def by auto
         then have "\<Union>(range f) = A i"
-          using f C Ai unfolding bij_betw_def
-            by (auto simp add: f_def cong del: SUP_cong_simp)
+          using f by (auto simp add: f_def)
         moreover
         { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
             using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -1492,8 +1492,8 @@
 qed
 
 lemma affine_parallel_expl: "affine_parallel S T \<longleftrightarrow> (\<exists>a. \<forall>x. x \<in> S \<longleftrightarrow> a + x \<in> T)"
-  unfolding affine_parallel_def
-  using affine_parallel_expl_aux[of S _ T] by auto
+  by (auto simp add: affine_parallel_def)
+    (use affine_parallel_expl_aux [of S _ T] in blast)
 
 lemma affine_parallel_reflex: "affine_parallel S S"
   unfolding affine_parallel_def
@@ -1508,7 +1508,7 @@
   have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
   from B show ?thesis
     using translation_galois [of B a A]
-    unfolding affine_parallel_def by auto
+    unfolding affine_parallel_def by blast
 qed
 
 lemma affine_parallel_assoc:
@@ -1629,7 +1629,7 @@
 proof -
   have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
   have "affine ((\<lambda>x. (-a)+x) ` S)"
-    using  affine_translation assms by auto
+    using affine_translation assms by blast
   moreover have "0 \<in> ((\<lambda>x. (-a)+x) ` S)"
     using assms exI[of "(\<lambda>x. x\<in>S \<and> -a+x = 0)" a] by auto
   ultimately show ?thesis using subspace_affine by auto
@@ -1781,7 +1781,7 @@
           using \<open>cone S\<close> \<open>c > 0\<close>
           unfolding cone_def image_def \<open>c > 0\<close> by auto
       }
-      ultimately have "((*\<^sub>R) c) ` S = S" by auto
+      ultimately have "((*\<^sub>R) c) ` S = S" by blast
     }
     then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
       using \<open>cone S\<close> cone_contains_0[of S] assms by auto
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -2495,14 +2495,15 @@
 unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros)
 
 lemma homeomorphism_ident: "homeomorphism T T (\<lambda>a. a) (\<lambda>a. a)"
-  by (rule homeomorphismI) (auto simp: continuous_on_id)
+  by (rule homeomorphismI) auto
 
 lemma homeomorphism_compose:
   assumes "homeomorphism S T f g" "homeomorphism T U h k"
     shows "homeomorphism S U (h o f) (g o k)"
   using assms
   unfolding homeomorphism_def
-  by (intro conjI ballI continuous_on_compose) (auto simp: image_comp [symmetric])
+  by (intro conjI ballI continuous_on_compose) (auto simp: image_iff)
+
 
 lemma homeomorphism_symD: "homeomorphism S t f g \<Longrightarrow> homeomorphism t S g f"
   by (simp add: homeomorphism_def)
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Analysis/Embed_Measure.thy
--- a/src/HOL/Analysis/Embed_Measure.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Analysis/Embed_Measure.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -263,8 +263,6 @@
                 simp del: map_prod_simp
                 del: prod_fun_imageE) []
     apply auto []
-    apply (subst image_insert)
-    apply simp
     apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)
     apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)
     apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Analysis/Homotopy.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -3168,11 +3168,11 @@
   have dd: "dim ((+) (- a) ` S) = dim ((+) (- b) ` T)"
     using assms ab  by (simp add: aff_dim_eq_dim  [OF hull_inc] image_def)
   have "S homeomorphic ((+) (- a) ` S)"
-    by (simp add: homeomorphic_translation)
+    by (fact homeomorphic_translation)
   also have "\<dots> homeomorphic ((+) (- b) ` T)"
     by (rule homeomorphic_subspaces [OF ss dd])
   also have "\<dots> homeomorphic T"
-    using homeomorphic_sym homeomorphic_translation by auto
+    using homeomorphic_translation [of T "- b"] by (simp add: homeomorphic_sym [of T])
   finally show ?thesis .
 qed
 
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -446,12 +446,30 @@
   by (simp add: range_binary_eq cong del: INF_cong_simp)
 
 lemma sigma_algebra_iff2:
-     "sigma_algebra \<Omega> M \<longleftrightarrow>
-       M \<subseteq> Pow \<Omega> \<and>
-       {} \<in> M \<and> (\<forall>s \<in> M. \<Omega> - s \<in> M) \<and>
-       (\<forall>A. range A \<subseteq> M \<longrightarrow> (\<Union>i::nat. A i) \<in> M)"
-  by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
-         algebra_iff_Un Un_range_binary)
+  "sigma_algebra \<Omega> M \<longleftrightarrow>
+    M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>s \<in> M. \<Omega> - s \<in> M)
+    \<and> (\<forall>A. range A \<subseteq> M \<longrightarrow>(\<Union> i::nat. A i) \<in> M)" (is "?P \<longleftrightarrow> ?R \<and> ?S \<and> ?V \<and> ?W")
+proof
+  assume ?P
+  then interpret sigma_algebra \<Omega> M .
+  from space_closed show "?R \<and> ?S \<and> ?V \<and> ?W"
+    by auto
+next
+  assume "?R \<and> ?S \<and> ?V \<and> ?W"
+  then have ?R ?S ?V ?W
+    by simp_all
+  show ?P
+  proof (rule sigma_algebra.intro)
+    show "sigma_algebra_axioms M"
+      by standard (use \<open>?W\<close> in simp)
+    from \<open>?W\<close> have *: "range (binary a b) \<subseteq> M \<Longrightarrow> \<Union> (range (binary a b)) \<in> M" for a b
+      by auto
+    show "algebra \<Omega> M"
+      unfolding algebra_iff_Un using \<open>?R\<close> \<open>?S\<close> \<open>?V\<close> *
+      by (auto simp add: range_binary_eq)
+  qed
+qed
+
 
 subsubsection \<open>Initial Sigma Algebra\<close>
 
@@ -1204,7 +1222,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 UN by auto
+    using sets UN by auto fastforce
   also have "\<Omega> - (D \<union> (\<Omega> - E)) = E - D"
     using assms sets_into_space by auto
   finally show ?thesis .
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Binomial.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -1070,7 +1070,7 @@
   also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
     using assms by (subst sum.Sigma) auto
   also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
-    by (rule sum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta)
+    by (rule sum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI)
   also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
     using assms
     by (auto intro!: sum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Complete_Lattices.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -61,7 +61,7 @@
 lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
   by (simp add: image_def)
 
-lemma INF_cong_simp [cong]:
+lemma INF_cong_simp:
   "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
   unfolding simp_implies_def by (fact INF_cong)
 
@@ -82,7 +82,7 @@
 lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
 by (fact Inf.INF_cong)
 
-lemma SUP_cong_simp [cong]:
+lemma SUP_cong_simp:
   "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
 by (fact Inf.INF_cong_simp)
 
@@ -436,12 +436,10 @@
   by (auto intro: SUP_eqI)
 
 lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> \<Sqinter>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
-  using INF_eq_const [of I f c] INF_lower [of _ I f]
-  by (auto intro: antisym cong del: INF_cong_simp)
+  by (auto intro: INF_eq_const INF_lower antisym)
 
 lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> \<Squnion>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
-  using SUP_eq_const [of I f c] SUP_upper [of _ I f]
-  by (auto intro: antisym cong del: SUP_cong_simp)
+  by (auto intro: SUP_eq_const SUP_upper antisym)
 
 end
 
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Enum.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -859,9 +859,10 @@
   from this have B: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> fa b f ` ({x} \<union> F) \<in> {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)}"
     by blast
   have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> b \<sqinter> (\<Sqinter>x\<in>F. f x)  \<le> \<Squnion>(Inf ` {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)})"
-    using B apply (rule SUP_upper2, simp_all)
-    by (simp_all add: INF_greatest Inf_lower inf.coboundedI2 fa_def)
-
+    using B apply (rule SUP_upper2)
+    using \<open>x \<notin> F\<close> apply (simp_all add: fa_def Inf_union_distrib)
+    apply (simp add: image_mono Inf_superset_mono inf.coboundedI2)
+    done
   assume "\<Sqinter>(Sup ` F) \<le> \<Squnion>(Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y})"
 
   from this have "\<Squnion>x \<sqinter> \<Sqinter>(Sup ` F) \<le> \<Squnion>x \<sqinter> \<Squnion>(Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y})"
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Fun.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -314,7 +314,7 @@
   by (simp add: surj_def) blast
 
 lemma comp_surj: "surj f \<Longrightarrow> surj g \<Longrightarrow> surj (g \<circ> f)"
-  by (simp add: image_comp [symmetric])
+  using image_comp [of g f UNIV] by simp
 
 lemma bij_betw_imageI: "inj_on f A \<Longrightarrow> f ` A = B \<Longrightarrow> bij_betw f A B"
   unfolding bij_betw_def by clarify
@@ -629,7 +629,7 @@
 
 lemma surj_plus [simp]:
   "surj ((+) a)"
-  by (auto intro: range_eqI [of b "(+) a" "b - a" for b] simp add: algebra_simps)
+  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>
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/GCD.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -1030,12 +1030,11 @@
   also from x have "c * x dvd Lcm ((*) c ` A)"
     by (intro dvd_Lcm) auto
   finally have dvd: "c dvd Lcm ((*) c ` A)" .
-
-  have "Lcm A dvd Lcm ((*) c ` A) div c"
+  moreover have "Lcm A dvd Lcm ((*) c ` A) div c"
     by (intro Lcm_least dvd_mult_imp_div)
       (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
-  then have "c * Lcm A dvd Lcm ((*) c ` A)"
-    by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
+  ultimately have "c * Lcm A dvd Lcm ((*) c ` A)"
+    by auto
   also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
   also have "\<dots> dvd Lcm ((*) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm ((*) c ` A)"
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -1055,9 +1055,9 @@
         using B by blast
       show "(\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
         using A apply (rule SUP_upper2)
-        apply (simp add: F_def)
         apply (rule INF_greatest)
-        apply (auto simp add: * **)
+        using * **
+        apply (auto simp add: F_def)
         done
     qed
 
@@ -1066,8 +1066,11 @@
       proof (cases "x \<in> A")
         case True
         then show ?thesis
-          apply (rule INF_lower2, simp_all)
-          by (rule SUP_least, rule SUP_upper2, auto)
+          apply (rule INF_lower2)
+          apply (rule SUP_least)
+          apply (rule SUP_upper2)
+           apply auto
+          done
       next
         case False
         then show ?thesis by simp
@@ -1076,9 +1079,11 @@
     from this have "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Sqinter>x. \<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
       by (rule INF_greatest)
     also have "... = (\<Squnion>x. \<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>)"
-      by (simp add: INF_SUP)
+      by (simp only: INF_SUP)
     also have "... \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
-      by (rule SUP_least, simp add: ***)
+      apply (rule SUP_least)
+      using *** apply simp
+      done
     finally show ?thesis by simp
   qed
 qed
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Hoare_Parallel/RG_Examples.thy
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -320,8 +320,8 @@
       \<lbrace>True\<rbrace>,
       \<lbrace>\<forall>i<n. (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and>
         (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i)\<rbrace>]"
-apply (rule Parallel)
-apply (auto cong del: INF_cong_simp SUP_cong_simp)
+  apply (rule Parallel)
+apply (auto cong del: image_cong_simp)
 apply force
 apply (rule While)
     apply force
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Probability/ex/Dining_Cryptographers.thy
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -438,7 +438,7 @@
       by (auto simp: simple_function_def space_uniform_count_measure sets_uniform_count_measure)
     fix z assume "z \<in> payer ` space (uniform_count_measure dc_crypto)"
     then have "payer -` {z} \<inter> dc_crypto = {z} \<times> {xs. length xs = n}"
-      by (auto simp: dc_crypto payer_def space_uniform_count_measure)
+      by (auto simp: dc_crypto payer_def space_uniform_count_measure cong del: image_cong_simp)
     hence "card (payer -` {z} \<inter> dc_crypto) = 2^n"
       using card_lists_length_eq[where A="UNIV::bool set"]
       by (simp add: card_cartesian_product_singleton)
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Set.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -930,11 +930,13 @@
   "(\<lambda>x. if P x then f x else g x) ` S = f ` (S \<inter> {x. P x}) \<union> g ` (S \<inter> {x. \<not> P x})"
   by auto
 
-lemma image_cong: "\<lbrakk> M = N;  \<And>x. x \<in> N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> f ` M = g ` N"
-by (simp add: image_def)
-
-lemma image_cong_simp: "\<lbrakk> M = N; \<And>x. x \<in> N =simp=> f x = g x\<rbrakk> \<Longrightarrow> f ` M = g ` N"
-by (simp add: image_def simp_implies_def)
+lemma image_cong:
+  "f ` M = g ` N" if "M = N" "\<And>x. x \<in> N \<Longrightarrow> f x = g x"
+  using that by (simp add: image_def)
+
+lemma image_cong_simp [cong]:
+  "f ` M = g ` N" if "M = N" "\<And>x. x \<in> N =simp=> f x = g x"
+  using that image_cong [of M N f g] by (simp add: simp_implies_def)
 
 lemma image_Int_subset: "f ` (A \<inter> B) \<subseteq> f ` A \<inter> f ` B"
   by blast
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -1039,38 +1039,51 @@
 lemma image_mult_atLeastAtMost_if:
   "(*) c ` {x .. y} =
     (if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
-proof -
-  consider "c < 0" "x \<le> y" | "c = 0" "x \<le> y" | "c > 0" "x \<le> y" | "x > y"
-    using local.antisym_conv3 local.leI by blast
+proof (cases "c = 0 \<or> x > y")
+  case True
+  then show ?thesis
+    by auto
+next
+  case False
+  then have "x \<le> y"
+    by auto
+  from False consider "c < 0"| "c > 0"
+    by (auto simp add: neq_iff)
   then show ?thesis
   proof cases
     case 1
-    have "(*) c ` {x .. y} = uminus ` (*) (- c) ` {x .. y}"
-      by (simp add: image_image)
-    also have "\<dots> = {c * y .. c * x}"
-      using \<open>c < 0\<close>
-      by simp
-    finally show ?thesis
-      using \<open>c < 0\<close> by auto
-  qed (auto simp: not_le local.mult_less_cancel_left_pos)
+    have "(*) c ` {x..y} = {c * y..c * x}"
+    proof (rule set_eqI)
+      fix d
+      from 1 have "inj (\<lambda>z. z / c)"
+        by (auto intro: injI)
+      then have "d \<in> (*) c ` {x..y} \<longleftrightarrow> d / c \<in> (\<lambda>z. z div c) ` (*) c ` {x..y}"
+        by (subst inj_image_mem_iff) simp_all
+      also have "\<dots> \<longleftrightarrow> d / c \<in> {x..y}"
+        using 1 by (simp add: image_image)
+      also have "\<dots> \<longleftrightarrow> d \<in> {c * y..c * x}"
+        by (auto simp add: field_simps 1)
+      finally show "d \<in> (*) c ` {x..y} \<longleftrightarrow> d \<in> {c * y..c * x}" .
+    qed
+    with \<open>x \<le> y\<close> show ?thesis
+      by auto
+  qed (simp add: mult_left_mono_neg)
 qed
 
 lemma image_mult_atLeastAtMost_if':
   "(\<lambda>x. x * c) ` {x..y} =
     (if x \<le> y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})"
-  by (subst mult.commute)
-    (simp add: image_mult_atLeastAtMost_if mult.commute mult_le_cancel_left_pos)
+  using image_mult_atLeastAtMost_if [of c x y] by (auto simp add: ac_simps)
 
 lemma image_affinity_atLeastAtMost:
-  "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {m*a + c .. m *b + c}
-            else {m*b + c .. m*a + c})"
+  "((\<lambda>x. m * x + c) ` {a..b}) = (if {a..b} = {} then {}
+            else if 0 \<le> m then {m * a + c .. m * b + c}
+            else {m * b + c .. m * a + c})"
 proof -
-  have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o (*) m)"
-    unfolding image_comp[symmetric]
-    by (simp add: o_def)
-  then show ?thesis
-    by (auto simp add: image_comp[symmetric] image_mult_atLeastAtMost_if mult_le_cancel_left)
+  have *: "(\<lambda>x. m * x + c) = ((\<lambda>x. x + c) \<circ> (*) m)"
+    by (simp add: fun_eq_iff)
+  show ?thesis by (simp only: * image_comp [symmetric] image_mult_atLeastAtMost_if)
+    (auto simp add: mult_le_cancel_left)
 qed
 
 lemma image_affinity_atLeastAtMost_diff:
diff -r d10fafeb93c0 -r 7e4966eaf781 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -926,8 +926,7 @@
     ==> rename sysOfClient (plam x: I. rename client_map Client) \<in>
           UNIV  guarantees
           Always {s. \<forall>elt \<in> set ((ask o sub i o client) s). elt \<le> NbT}"
-  by rename_client_map
-
+  using image_cong_simp [cong del] by rename_client_map
 
 lemma System_Bounded_ask: "i < Nclients
       ==> System \<in> Always
@@ -963,6 +962,7 @@
           (INT h. {s. h \<le> (giv o sub i o client) s &
                             h pfixGe (ask o sub i o client) s}
                   LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})"
+  using image_cong_simp [cong del]
   apply rename_client_map
   apply (simp add: Client_Progress [simplified o_def])
   done