--- a/NEWS Thu Jan 31 21:33:24 2019 +0100
+++ b/NEWS Thu Jan 31 21:59:30 2019 +0100
@@ -107,6 +107,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,
--- a/src/HOL/Analysis/Caratheodory.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Analysis/Caratheodory.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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)
--- a/src/HOL/Analysis/Convex.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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
--- a/src/HOL/Analysis/Elementary_Topology.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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)
--- a/src/HOL/Analysis/Embed_Measure.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Analysis/Embed_Measure.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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
--- a/src/HOL/Analysis/Homotopy.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Analysis/Homotopy.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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
--- a/src/HOL/Analysis/Sigma_Algebra.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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 .
--- a/src/HOL/Binomial.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Binomial.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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"])
--- a/src/HOL/Complete_Lattices.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Complete_Lattices.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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
--- a/src/HOL/Enum.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Enum.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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})"
--- a/src/HOL/Fun.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Fun.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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>
--- a/src/HOL/GCD.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/GCD.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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)"
--- a/src/HOL/Hilbert_Choice.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Hilbert_Choice.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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)
--- a/src/HOL/Set.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Set.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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
--- a/src/HOL/Set_Interval.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/Set_Interval.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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:
--- a/src/HOL/UNITY/Comp/Alloc.thy Thu Jan 31 21:33:24 2019 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Thu Jan 31 21:59:30 2019 +0100
@@ -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