proper congruence rule for image operator
authorhaftmann
Thu Jan 31 13:08:59 2019 +0000 (3 months ago)
changeset 697687e4966eaf781
parent 69767 d10fafeb93c0
child 69778 09ad02c0fbee
proper congruence rule for image operator
NEWS
src/HOL/Analysis/Caratheodory.thy
src/HOL/Analysis/Convex.thy
src/HOL/Analysis/Elementary_Topology.thy
src/HOL/Analysis/Embed_Measure.thy
src/HOL/Analysis/Homotopy.thy
src/HOL/Analysis/Sigma_Algebra.thy
src/HOL/Binomial.thy
src/HOL/Complete_Lattices.thy
src/HOL/Enum.thy
src/HOL/Fun.thy
src/HOL/GCD.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hoare_Parallel/RG_Examples.thy
src/HOL/Probability/ex/Dining_Cryptographers.thy
src/HOL/Set.thy
src/HOL/Set_Interval.thy
src/HOL/UNITY/Comp/Alloc.thy
     1.1 --- a/NEWS	Thu Jan 31 09:30:15 2019 +0100
     1.2 +++ b/NEWS	Thu Jan 31 13:08:59 2019 +0000
     1.3 @@ -104,6 +104,11 @@
     1.4  * Code generation: slightly more conventional syntax for
     1.5  'code_stmts' antiquotation.  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* The simplifier uses image_cong_simp as a congruence rule. The historic
     1.8 +and not really well-formed congruence rules INF_cong*, SUP_cong*,
     1.9 +are not used by default any longer.  INCOMPATIBILITY; consider using
    1.10 +declare image_cong_simp [cong del] in extreme situations.
    1.11 +
    1.12  * Simplified syntax setup for big operators under image. In rare
    1.13  situations, type conversions are not inserted implicitly any longer
    1.14  and need to be given explicitly. Auxiliary abbreviations INFIMUM,
     2.1 --- a/src/HOL/Analysis/Caratheodory.thy	Thu Jan 31 09:30:15 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Caratheodory.thy	Thu Jan 31 13:08:59 2019 +0000
     2.3 @@ -736,8 +736,7 @@
     2.4          have Ai_eq: "A i = (\<Union>x<card C. f x)"
     2.5            using f C Ai unfolding bij_betw_def by auto
     2.6          then have "\<Union>(range f) = A i"
     2.7 -          using f C Ai unfolding bij_betw_def
     2.8 -            by (auto simp add: f_def cong del: SUP_cong_simp)
     2.9 +          using f by (auto simp add: f_def)
    2.10          moreover
    2.11          { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
    2.12              using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
     3.1 --- a/src/HOL/Analysis/Convex.thy	Thu Jan 31 09:30:15 2019 +0100
     3.2 +++ b/src/HOL/Analysis/Convex.thy	Thu Jan 31 13:08:59 2019 +0000
     3.3 @@ -1492,8 +1492,8 @@
     3.4  qed
     3.5  
     3.6  lemma affine_parallel_expl: "affine_parallel S T \<longleftrightarrow> (\<exists>a. \<forall>x. x \<in> S \<longleftrightarrow> a + x \<in> T)"
     3.7 -  unfolding affine_parallel_def
     3.8 -  using affine_parallel_expl_aux[of S _ T] by auto
     3.9 +  by (auto simp add: affine_parallel_def)
    3.10 +    (use affine_parallel_expl_aux [of S _ T] in blast)
    3.11  
    3.12  lemma affine_parallel_reflex: "affine_parallel S S"
    3.13    unfolding affine_parallel_def
    3.14 @@ -1508,7 +1508,7 @@
    3.15    have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
    3.16    from B show ?thesis
    3.17      using translation_galois [of B a A]
    3.18 -    unfolding affine_parallel_def by auto
    3.19 +    unfolding affine_parallel_def by blast
    3.20  qed
    3.21  
    3.22  lemma affine_parallel_assoc:
    3.23 @@ -1629,7 +1629,7 @@
    3.24  proof -
    3.25    have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
    3.26    have "affine ((\<lambda>x. (-a)+x) ` S)"
    3.27 -    using  affine_translation assms by auto
    3.28 +    using affine_translation assms by blast
    3.29    moreover have "0 \<in> ((\<lambda>x. (-a)+x) ` S)"
    3.30      using assms exI[of "(\<lambda>x. x\<in>S \<and> -a+x = 0)" a] by auto
    3.31    ultimately show ?thesis using subspace_affine by auto
    3.32 @@ -1781,7 +1781,7 @@
    3.33            using \<open>cone S\<close> \<open>c > 0\<close>
    3.34            unfolding cone_def image_def \<open>c > 0\<close> by auto
    3.35        }
    3.36 -      ultimately have "((*\<^sub>R) c) ` S = S" by auto
    3.37 +      ultimately have "((*\<^sub>R) c) ` S = S" by blast
    3.38      }
    3.39      then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
    3.40        using \<open>cone S\<close> cone_contains_0[of S] assms by auto
     4.1 --- a/src/HOL/Analysis/Elementary_Topology.thy	Thu Jan 31 09:30:15 2019 +0100
     4.2 +++ b/src/HOL/Analysis/Elementary_Topology.thy	Thu Jan 31 13:08:59 2019 +0000
     4.3 @@ -2495,14 +2495,15 @@
     4.4  unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros)
     4.5  
     4.6  lemma homeomorphism_ident: "homeomorphism T T (\<lambda>a. a) (\<lambda>a. a)"
     4.7 -  by (rule homeomorphismI) (auto simp: continuous_on_id)
     4.8 +  by (rule homeomorphismI) auto
     4.9  
    4.10  lemma homeomorphism_compose:
    4.11    assumes "homeomorphism S T f g" "homeomorphism T U h k"
    4.12      shows "homeomorphism S U (h o f) (g o k)"
    4.13    using assms
    4.14    unfolding homeomorphism_def
    4.15 -  by (intro conjI ballI continuous_on_compose) (auto simp: image_comp [symmetric])
    4.16 +  by (intro conjI ballI continuous_on_compose) (auto simp: image_iff)
    4.17 +
    4.18  
    4.19  lemma homeomorphism_symD: "homeomorphism S t f g \<Longrightarrow> homeomorphism t S g f"
    4.20    by (simp add: homeomorphism_def)
     5.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Thu Jan 31 09:30:15 2019 +0100
     5.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Thu Jan 31 13:08:59 2019 +0000
     5.3 @@ -263,8 +263,6 @@
     5.4                  simp del: map_prod_simp
     5.5                  del: prod_fun_imageE) []
     5.6      apply auto []
     5.7 -    apply (subst image_insert)
     5.8 -    apply simp
     5.9      apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)
    5.10      apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)
    5.11      apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq
     6.1 --- a/src/HOL/Analysis/Homotopy.thy	Thu Jan 31 09:30:15 2019 +0100
     6.2 +++ b/src/HOL/Analysis/Homotopy.thy	Thu Jan 31 13:08:59 2019 +0000
     6.3 @@ -3168,11 +3168,11 @@
     6.4    have dd: "dim ((+) (- a) ` S) = dim ((+) (- b) ` T)"
     6.5      using assms ab  by (simp add: aff_dim_eq_dim  [OF hull_inc] image_def)
     6.6    have "S homeomorphic ((+) (- a) ` S)"
     6.7 -    by (simp add: homeomorphic_translation)
     6.8 +    by (fact homeomorphic_translation)
     6.9    also have "\<dots> homeomorphic ((+) (- b) ` T)"
    6.10      by (rule homeomorphic_subspaces [OF ss dd])
    6.11    also have "\<dots> homeomorphic T"
    6.12 -    using homeomorphic_sym homeomorphic_translation by auto
    6.13 +    using homeomorphic_translation [of T "- b"] by (simp add: homeomorphic_sym [of T])
    6.14    finally show ?thesis .
    6.15  qed
    6.16  
     7.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Thu Jan 31 09:30:15 2019 +0100
     7.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Thu Jan 31 13:08:59 2019 +0000
     7.3 @@ -446,12 +446,30 @@
     7.4    by (simp add: range_binary_eq cong del: INF_cong_simp)
     7.5  
     7.6  lemma sigma_algebra_iff2:
     7.7 -     "sigma_algebra \<Omega> M \<longleftrightarrow>
     7.8 -       M \<subseteq> Pow \<Omega> \<and>
     7.9 -       {} \<in> M \<and> (\<forall>s \<in> M. \<Omega> - s \<in> M) \<and>
    7.10 -       (\<forall>A. range A \<subseteq> M \<longrightarrow> (\<Union>i::nat. A i) \<in> M)"
    7.11 -  by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
    7.12 -         algebra_iff_Un Un_range_binary)
    7.13 +  "sigma_algebra \<Omega> M \<longleftrightarrow>
    7.14 +    M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>s \<in> M. \<Omega> - s \<in> M)
    7.15 +    \<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")
    7.16 +proof
    7.17 +  assume ?P
    7.18 +  then interpret sigma_algebra \<Omega> M .
    7.19 +  from space_closed show "?R \<and> ?S \<and> ?V \<and> ?W"
    7.20 +    by auto
    7.21 +next
    7.22 +  assume "?R \<and> ?S \<and> ?V \<and> ?W"
    7.23 +  then have ?R ?S ?V ?W
    7.24 +    by simp_all
    7.25 +  show ?P
    7.26 +  proof (rule sigma_algebra.intro)
    7.27 +    show "sigma_algebra_axioms M"
    7.28 +      by standard (use \<open>?W\<close> in simp)
    7.29 +    from \<open>?W\<close> have *: "range (binary a b) \<subseteq> M \<Longrightarrow> \<Union> (range (binary a b)) \<in> M" for a b
    7.30 +      by auto
    7.31 +    show "algebra \<Omega> M"
    7.32 +      unfolding algebra_iff_Un using \<open>?R\<close> \<open>?S\<close> \<open>?V\<close> *
    7.33 +      by (auto simp add: range_binary_eq)
    7.34 +  qed
    7.35 +qed
    7.36 +
    7.37  
    7.38  subsubsection \<open>Initial Sigma Algebra\<close>
    7.39  
    7.40 @@ -1204,7 +1222,7 @@
    7.41    have "disjoint_family ?f" unfolding disjoint_family_on_def
    7.42      using \<open>D \<in> M\<close>[THEN sets_into_space] \<open>D \<subseteq> E\<close> by auto
    7.43    ultimately have "\<Omega> - (D \<union> (\<Omega> - E)) \<in> M"
    7.44 -    using sets UN by auto
    7.45 +    using sets UN by auto fastforce
    7.46    also have "\<Omega> - (D \<union> (\<Omega> - E)) = E - D"
    7.47      using assms sets_into_space by auto
    7.48    finally show ?thesis .
     8.1 --- a/src/HOL/Binomial.thy	Thu Jan 31 09:30:15 2019 +0100
     8.2 +++ b/src/HOL/Binomial.thy	Thu Jan 31 13:08:59 2019 +0000
     8.3 @@ -1070,7 +1070,7 @@
     8.4    also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
     8.5      using assms by (subst sum.Sigma) auto
     8.6    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))"
     8.7 -    by (rule sum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta)
     8.8 +    by (rule sum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI)
     8.9    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))"
    8.10      using assms
    8.11      by (auto intro!: sum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
     9.1 --- a/src/HOL/Complete_Lattices.thy	Thu Jan 31 09:30:15 2019 +0100
     9.2 +++ b/src/HOL/Complete_Lattices.thy	Thu Jan 31 13:08:59 2019 +0000
     9.3 @@ -61,7 +61,7 @@
     9.4  lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
     9.5    by (simp add: image_def)
     9.6  
     9.7 -lemma INF_cong_simp [cong]:
     9.8 +lemma INF_cong_simp:
     9.9    "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
    9.10    unfolding simp_implies_def by (fact INF_cong)
    9.11  
    9.12 @@ -82,7 +82,7 @@
    9.13  lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
    9.14  by (fact Inf.INF_cong)
    9.15  
    9.16 -lemma SUP_cong_simp [cong]:
    9.17 +lemma SUP_cong_simp:
    9.18    "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
    9.19  by (fact Inf.INF_cong_simp)
    9.20  
    9.21 @@ -436,12 +436,10 @@
    9.22    by (auto intro: SUP_eqI)
    9.23  
    9.24  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)"
    9.25 -  using INF_eq_const [of I f c] INF_lower [of _ I f]
    9.26 -  by (auto intro: antisym cong del: INF_cong_simp)
    9.27 +  by (auto intro: INF_eq_const INF_lower antisym)
    9.28  
    9.29  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)"
    9.30 -  using SUP_eq_const [of I f c] SUP_upper [of _ I f]
    9.31 -  by (auto intro: antisym cong del: SUP_cong_simp)
    9.32 +  by (auto intro: SUP_eq_const SUP_upper antisym)
    9.33  
    9.34  end
    9.35  
    10.1 --- a/src/HOL/Enum.thy	Thu Jan 31 09:30:15 2019 +0100
    10.2 +++ b/src/HOL/Enum.thy	Thu Jan 31 13:08:59 2019 +0000
    10.3 @@ -859,9 +859,10 @@
    10.4    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)}"
    10.5      by blast
    10.6    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)})"
    10.7 -    using B apply (rule SUP_upper2, simp_all)
    10.8 -    by (simp_all add: INF_greatest Inf_lower inf.coboundedI2 fa_def)
    10.9 -
   10.10 +    using B apply (rule SUP_upper2)
   10.11 +    using \<open>x \<notin> F\<close> apply (simp_all add: fa_def Inf_union_distrib)
   10.12 +    apply (simp add: image_mono Inf_superset_mono inf.coboundedI2)
   10.13 +    done
   10.14    assume "\<Sqinter>(Sup ` F) \<le> \<Squnion>(Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y})"
   10.15  
   10.16    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})"
    11.1 --- a/src/HOL/Fun.thy	Thu Jan 31 09:30:15 2019 +0100
    11.2 +++ b/src/HOL/Fun.thy	Thu Jan 31 13:08:59 2019 +0000
    11.3 @@ -314,7 +314,7 @@
    11.4    by (simp add: surj_def) blast
    11.5  
    11.6  lemma comp_surj: "surj f \<Longrightarrow> surj g \<Longrightarrow> surj (g \<circ> f)"
    11.7 -  by (simp add: image_comp [symmetric])
    11.8 +  using image_comp [of g f UNIV] by simp
    11.9  
   11.10  lemma bij_betw_imageI: "inj_on f A \<Longrightarrow> f ` A = B \<Longrightarrow> bij_betw f A B"
   11.11    unfolding bij_betw_def by clarify
   11.12 @@ -629,7 +629,7 @@
   11.13  
   11.14  lemma surj_plus [simp]:
   11.15    "surj ((+) a)"
   11.16 -  by (auto intro: range_eqI [of b "(+) a" "b - a" for b] simp add: algebra_simps)
   11.17 +  by (auto intro!: range_eqI [of b "(+) a" "b - a" for b]) (simp add: algebra_simps)
   11.18  
   11.19  lemma inj_diff_right [simp]:
   11.20    \<open>inj (\<lambda>b. b - a)\<close>
    12.1 --- a/src/HOL/GCD.thy	Thu Jan 31 09:30:15 2019 +0100
    12.2 +++ b/src/HOL/GCD.thy	Thu Jan 31 13:08:59 2019 +0000
    12.3 @@ -1030,12 +1030,11 @@
    12.4    also from x have "c * x dvd Lcm ((*) c ` A)"
    12.5      by (intro dvd_Lcm) auto
    12.6    finally have dvd: "c dvd Lcm ((*) c ` A)" .
    12.7 -
    12.8 -  have "Lcm A dvd Lcm ((*) c ` A) div c"
    12.9 +  moreover have "Lcm A dvd Lcm ((*) c ` A) div c"
   12.10      by (intro Lcm_least dvd_mult_imp_div)
   12.11        (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
   12.12 -  then have "c * Lcm A dvd Lcm ((*) c ` A)"
   12.13 -    by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
   12.14 +  ultimately have "c * Lcm A dvd Lcm ((*) c ` A)"
   12.15 +    by auto
   12.16    also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
   12.17      by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
   12.18    also have "\<dots> dvd Lcm ((*) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm ((*) c ` A)"
    13.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Jan 31 09:30:15 2019 +0100
    13.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Jan 31 13:08:59 2019 +0000
    13.3 @@ -1055,9 +1055,9 @@
    13.4          using B by blast
    13.5        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)"
    13.6          using A apply (rule SUP_upper2)
    13.7 -        apply (simp add: F_def)
    13.8          apply (rule INF_greatest)
    13.9 -        apply (auto simp add: * **)
   13.10 +        using * **
   13.11 +        apply (auto simp add: F_def)
   13.12          done
   13.13      qed
   13.14  
   13.15 @@ -1066,8 +1066,11 @@
   13.16        proof (cases "x \<in> A")
   13.17          case True
   13.18          then show ?thesis
   13.19 -          apply (rule INF_lower2, simp_all)
   13.20 -          by (rule SUP_least, rule SUP_upper2, auto)
   13.21 +          apply (rule INF_lower2)
   13.22 +          apply (rule SUP_least)
   13.23 +          apply (rule SUP_upper2)
   13.24 +           apply auto
   13.25 +          done
   13.26        next
   13.27          case False
   13.28          then show ?thesis by simp
   13.29 @@ -1076,9 +1079,11 @@
   13.30      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>)"
   13.31        by (rule INF_greatest)
   13.32      also have "... = (\<Squnion>x. \<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>)"
   13.33 -      by (simp add: INF_SUP)
   13.34 +      by (simp only: INF_SUP)
   13.35      also have "... \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
   13.36 -      by (rule SUP_least, simp add: ***)
   13.37 +      apply (rule SUP_least)
   13.38 +      using *** apply simp
   13.39 +      done
   13.40      finally show ?thesis by simp
   13.41    qed
   13.42  qed
    14.1 --- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu Jan 31 09:30:15 2019 +0100
    14.2 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu Jan 31 13:08:59 2019 +0000
    14.3 @@ -320,8 +320,8 @@
    14.4        \<lbrace>True\<rbrace>,
    14.5        \<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>
    14.6          (\<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>]"
    14.7 -apply (rule Parallel)
    14.8 -apply (auto cong del: INF_cong_simp SUP_cong_simp)
    14.9 +  apply (rule Parallel)
   14.10 +apply (auto cong del: image_cong_simp)
   14.11  apply force
   14.12  apply (rule While)
   14.13      apply force
    15.1 --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Thu Jan 31 09:30:15 2019 +0100
    15.2 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Thu Jan 31 13:08:59 2019 +0000
    15.3 @@ -438,7 +438,7 @@
    15.4        by (auto simp: simple_function_def space_uniform_count_measure sets_uniform_count_measure)
    15.5      fix z assume "z \<in> payer ` space (uniform_count_measure dc_crypto)"
    15.6      then have "payer -` {z} \<inter> dc_crypto = {z} \<times> {xs. length xs = n}"
    15.7 -      by (auto simp: dc_crypto payer_def space_uniform_count_measure)
    15.8 +      by (auto simp: dc_crypto payer_def space_uniform_count_measure cong del: image_cong_simp)
    15.9      hence "card (payer -` {z} \<inter> dc_crypto) = 2^n"
   15.10        using card_lists_length_eq[where A="UNIV::bool set"]
   15.11        by (simp add: card_cartesian_product_singleton)
    16.1 --- a/src/HOL/Set.thy	Thu Jan 31 09:30:15 2019 +0100
    16.2 +++ b/src/HOL/Set.thy	Thu Jan 31 13:08:59 2019 +0000
    16.3 @@ -930,11 +930,13 @@
    16.4    "(\<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})"
    16.5    by auto
    16.6  
    16.7 -lemma image_cong: "\<lbrakk> M = N;  \<And>x. x \<in> N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> f ` M = g ` N"
    16.8 -by (simp add: image_def)
    16.9 -
   16.10 -lemma image_cong_simp: "\<lbrakk> M = N; \<And>x. x \<in> N =simp=> f x = g x\<rbrakk> \<Longrightarrow> f ` M = g ` N"
   16.11 -by (simp add: image_def simp_implies_def)
   16.12 +lemma image_cong:
   16.13 +  "f ` M = g ` N" if "M = N" "\<And>x. x \<in> N \<Longrightarrow> f x = g x"
   16.14 +  using that by (simp add: image_def)
   16.15 +
   16.16 +lemma image_cong_simp [cong]:
   16.17 +  "f ` M = g ` N" if "M = N" "\<And>x. x \<in> N =simp=> f x = g x"
   16.18 +  using that image_cong [of M N f g] by (simp add: simp_implies_def)
   16.19  
   16.20  lemma image_Int_subset: "f ` (A \<inter> B) \<subseteq> f ` A \<inter> f ` B"
   16.21    by blast
    17.1 --- a/src/HOL/Set_Interval.thy	Thu Jan 31 09:30:15 2019 +0100
    17.2 +++ b/src/HOL/Set_Interval.thy	Thu Jan 31 13:08:59 2019 +0000
    17.3 @@ -1039,38 +1039,51 @@
    17.4  lemma image_mult_atLeastAtMost_if:
    17.5    "(*) c ` {x .. y} =
    17.6      (if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
    17.7 -proof -
    17.8 -  consider "c < 0" "x \<le> y" | "c = 0" "x \<le> y" | "c > 0" "x \<le> y" | "x > y"
    17.9 -    using local.antisym_conv3 local.leI by blast
   17.10 +proof (cases "c = 0 \<or> x > y")
   17.11 +  case True
   17.12 +  then show ?thesis
   17.13 +    by auto
   17.14 +next
   17.15 +  case False
   17.16 +  then have "x \<le> y"
   17.17 +    by auto
   17.18 +  from False consider "c < 0"| "c > 0"
   17.19 +    by (auto simp add: neq_iff)
   17.20    then show ?thesis
   17.21    proof cases
   17.22      case 1
   17.23 -    have "(*) c ` {x .. y} = uminus ` (*) (- c) ` {x .. y}"
   17.24 -      by (simp add: image_image)
   17.25 -    also have "\<dots> = {c * y .. c * x}"
   17.26 -      using \<open>c < 0\<close>
   17.27 -      by simp
   17.28 -    finally show ?thesis
   17.29 -      using \<open>c < 0\<close> by auto
   17.30 -  qed (auto simp: not_le local.mult_less_cancel_left_pos)
   17.31 +    have "(*) c ` {x..y} = {c * y..c * x}"
   17.32 +    proof (rule set_eqI)
   17.33 +      fix d
   17.34 +      from 1 have "inj (\<lambda>z. z / c)"
   17.35 +        by (auto intro: injI)
   17.36 +      then have "d \<in> (*) c ` {x..y} \<longleftrightarrow> d / c \<in> (\<lambda>z. z div c) ` (*) c ` {x..y}"
   17.37 +        by (subst inj_image_mem_iff) simp_all
   17.38 +      also have "\<dots> \<longleftrightarrow> d / c \<in> {x..y}"
   17.39 +        using 1 by (simp add: image_image)
   17.40 +      also have "\<dots> \<longleftrightarrow> d \<in> {c * y..c * x}"
   17.41 +        by (auto simp add: field_simps 1)
   17.42 +      finally show "d \<in> (*) c ` {x..y} \<longleftrightarrow> d \<in> {c * y..c * x}" .
   17.43 +    qed
   17.44 +    with \<open>x \<le> y\<close> show ?thesis
   17.45 +      by auto
   17.46 +  qed (simp add: mult_left_mono_neg)
   17.47  qed
   17.48  
   17.49  lemma image_mult_atLeastAtMost_if':
   17.50    "(\<lambda>x. x * c) ` {x..y} =
   17.51      (if x \<le> y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})"
   17.52 -  by (subst mult.commute)
   17.53 -    (simp add: image_mult_atLeastAtMost_if mult.commute mult_le_cancel_left_pos)
   17.54 +  using image_mult_atLeastAtMost_if [of c x y] by (auto simp add: ac_simps)
   17.55  
   17.56  lemma image_affinity_atLeastAtMost:
   17.57 -  "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
   17.58 -            else if 0 \<le> m then {m*a + c .. m *b + c}
   17.59 -            else {m*b + c .. m*a + c})"
   17.60 +  "((\<lambda>x. m * x + c) ` {a..b}) = (if {a..b} = {} then {}
   17.61 +            else if 0 \<le> m then {m * a + c .. m * b + c}
   17.62 +            else {m * b + c .. m * a + c})"
   17.63  proof -
   17.64 -  have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o (*) m)"
   17.65 -    unfolding image_comp[symmetric]
   17.66 -    by (simp add: o_def)
   17.67 -  then show ?thesis
   17.68 -    by (auto simp add: image_comp[symmetric] image_mult_atLeastAtMost_if mult_le_cancel_left)
   17.69 +  have *: "(\<lambda>x. m * x + c) = ((\<lambda>x. x + c) \<circ> (*) m)"
   17.70 +    by (simp add: fun_eq_iff)
   17.71 +  show ?thesis by (simp only: * image_comp [symmetric] image_mult_atLeastAtMost_if)
   17.72 +    (auto simp add: mult_le_cancel_left)
   17.73  qed
   17.74  
   17.75  lemma image_affinity_atLeastAtMost_diff:
    18.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Thu Jan 31 09:30:15 2019 +0100
    18.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu Jan 31 13:08:59 2019 +0000
    18.3 @@ -926,8 +926,7 @@
    18.4      ==> rename sysOfClient (plam x: I. rename client_map Client) \<in>
    18.5            UNIV  guarantees
    18.6            Always {s. \<forall>elt \<in> set ((ask o sub i o client) s). elt \<le> NbT}"
    18.7 -  by rename_client_map
    18.8 -
    18.9 +  using image_cong_simp [cong del] by rename_client_map
   18.10  
   18.11  lemma System_Bounded_ask: "i < Nclients
   18.12        ==> System \<in> Always
   18.13 @@ -963,6 +962,7 @@
   18.14            (INT h. {s. h \<le> (giv o sub i o client) s &
   18.15                              h pfixGe (ask o sub i o client) s}
   18.16                    LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})"
   18.17 +  using image_cong_simp [cong del]
   18.18    apply rename_client_map
   18.19    apply (simp add: Client_Progress [simplified o_def])
   18.20    done