--- 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''"
--- 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"
--- 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
--- 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
--- 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))"
--- 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)
--- 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"]
--- 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>
--- 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)
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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>
--- 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
--- 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)"
--- 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"
--- 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")
--- 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"
--- 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 .
--- 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)"
--- 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)
--- 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
--- 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)
--- 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"
--- 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
--- 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"
--- 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)
--- 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"
--- 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]:
--- 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)" .
--- 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
--- 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"
--- 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
--- 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>
--- 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"
--- 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)
}
--- 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]:
--- 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
--- 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
--- 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)
--- 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"
--- 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:
--- 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
--- 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
--- 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)
--- 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
--- 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"