--- a/src/HOL/Analysis/Abstract_Topology_2.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Fri Nov 29 15:06:04 2019 +0100
@@ -706,7 +706,7 @@
unfolding continuous_map_openin_preimage_eq
proof (intro conjI allI impI)
show "g ` topspace X \<subseteq> topspace Y"
- using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce
+ using g cont continuous_map_image_subset_topspace by fastforce
next
fix U
assume Y: "openin Y U"
@@ -747,7 +747,7 @@
unfolding continuous_map_closedin_preimage_eq
proof (intro conjI allI impI)
show "g ` topspace X \<subseteq> topspace Y"
- using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce
+ using g cont continuous_map_image_subset_topspace by fastforce
next
fix U
assume Y: "closedin Y U"
--- a/src/HOL/Analysis/Convex.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy Fri Nov 29 15:06:04 2019 +0100
@@ -1998,7 +1998,7 @@
lemma convex_hull_subset:
"s \<subseteq> convex hull t \<Longrightarrow> convex hull s \<subseteq> convex hull t"
- by (simp add: convex_convex_hull subset_hull)
+ by (simp add: subset_hull)
lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
by (metis convex_convex_hull hull_same)
--- a/src/HOL/Analysis/Derivative.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy Fri Nov 29 15:06:04 2019 +0100
@@ -2441,7 +2441,7 @@
moreover
have ev_dist: "\<forall>\<^sub>F xy in at (x, y) within X \<times> Y. dist xy (x, y) < d" if "d > 0" for d
using eventually_at_ball[OF that]
- by (rule eventually_elim2) (auto simp: dist_commute mem_ball intro!: eventually_True)
+ by (rule eventually_elim2) (auto simp: dist_commute intro!: eventually_True)
note ev_dist[OF \<open>0 < d\<close>]
ultimately
have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Fri Nov 29 15:06:04 2019 +0100
@@ -63,7 +63,7 @@
by (simp add: subset_eq)
lemma mem_ball_imp_mem_cball: "x \<in> ball y e \<Longrightarrow> x \<in> cball y e"
- by (auto simp: mem_ball mem_cball)
+ by (auto)
lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
by force
@@ -78,10 +78,10 @@
by (simp add: subset_eq)
lemma mem_ball_leI: "x \<in> ball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> ball y f"
- by (auto simp: mem_ball mem_cball)
+ by (auto)
lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"
- by (auto simp: mem_ball mem_cball)
+ by (auto)
lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"
by metric
@@ -177,7 +177,7 @@
lemma atLeastAtMost_eq_cball:
fixes a b::real
shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
- by (auto simp: dist_real_def field_simps mem_cball)
+ by (auto simp: dist_real_def field_simps)
lemma cball_eq_atLeastAtMost:
fixes a b::real
@@ -187,7 +187,7 @@
lemma greaterThanLessThan_eq_ball:
fixes a b::real
shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
- by (auto simp: dist_real_def field_simps mem_ball)
+ by (auto simp: dist_real_def field_simps)
lemma ball_eq_greaterThanLessThan:
fixes a b::real
@@ -251,7 +251,7 @@
apply (drule_tac x="e/2" in spec)
apply (auto simp: simp del: less_divide_eq_numeral1)
apply (drule_tac x="dist x' x" in spec)
- apply (auto simp: zero_less_dist_iff simp del: less_divide_eq_numeral1)
+ apply (auto simp del: less_divide_eq_numeral1)
apply metric
done
@@ -1713,7 +1713,7 @@
fix r :: real and N n m
assume "1 / Suc N < r" "Suc N \<le> n" "Suc N \<le> m"
then have "(f \<circ> t) n \<in> F (Suc N)" "(f \<circ> t) m \<in> F (Suc N)" "2 * e N < r"
- using F_dec t by (auto simp: e_def field_simps of_nat_Suc)
+ using F_dec t by (auto simp: e_def field_simps)
with F[of N] obtain x where "dist x ((f \<circ> t) n) < e N" "dist x ((f \<circ> t) m) < e N"
by (auto simp: subset_eq)
with \<open>2 * e N < r\<close> show "dist ((f \<circ> t) m) ((f \<circ> t) n) < r"
@@ -3164,7 +3164,7 @@
apply (rule antisym)
using False closure_subset apply (blast intro: setdist_subset_left)
using False *
- apply (force simp add: closure_eq_empty intro!: le_setdistI)
+ apply (force intro!: le_setdistI)
done
qed
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Nov 29 15:06:04 2019 +0100
@@ -1779,7 +1779,7 @@
have 0: "0 \<le> prj1 (vf X - uf X)"
using \<open>X \<in> \<D>\<close> prj1_def vu_pos by fastforce
have "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))"
- apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> prod_constant)
+ apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close>)
apply (simp add: power_mult_distrib \<open>0 < B\<close> prj1_eq [symmetric])
using MleN 0 1 uvz \<open>X \<in> \<D>\<close>
apply (fastforce simp add: box_ne_empty power_decreasing)
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Fri Nov 29 15:06:04 2019 +0100
@@ -796,8 +796,7 @@
[@{thm plus_vec_def}, @{thm times_vec_def},
@{thm minus_vec_def}, @{thm uminus_vec_def},
@{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def},
- @{thm scaleR_vec_def},
- @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}])
+ @{thm scaleR_vec_def}, @{thm vector_scalar_mult_def}])
fun vector_arith_tac ctxt ths =
simp_tac (put_simpset ss1 ctxt)
THEN' (fn i => resolve_tac ctxt @{thms Finite_Cartesian_Product.sum_cong_aux} i
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Nov 29 15:06:04 2019 +0100
@@ -3492,7 +3492,7 @@
by (simp add: inner_simps field_simps)
ultimately show ?thesis
by (simp add: image_affinity_cbox True content_cbox'
- prod.distrib prod_constant inner_diff_left)
+ prod.distrib inner_diff_left)
next
case False
with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
--- a/src/HOL/Analysis/Lipschitz.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Lipschitz.thy Fri Nov 29 15:06:04 2019 +0100
@@ -544,7 +544,7 @@
show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f (g t))"
using d \<open>0 < u\<close>
by (fastforce intro: exI[where x="(min d u)/2"] exI[where x=L]
- intro!: less_imp_le[OF d(2)] lipschitz_on_subset[OF l] simp: dist_commute mem_ball mem_cball)
+ intro!: less_imp_le[OF d(2)] lipschitz_on_subset[OF l] simp: dist_commute)
qed
context
@@ -610,7 +610,7 @@
finally have "dist x a < u" .
then have "x \<in> cball a u \<inter> T"
using \<open>x \<in> T\<close>
- by (auto simp: dist_commute mem_cball)
+ by (auto simp: dist_commute)
have "dist (f x y) (f a b) \<le> dist (f x y) (f x b) + dist (f x b) (f a b)"
by (rule dist_triangle)
also have "(L + 1)-lipschitz_on (cball b u \<inter> X) (f x)"
@@ -711,7 +711,7 @@
"eventually (\<lambda>n. ?t n \<in> ball lt u) sequentially"
"eventually (\<lambda>n. ?y n \<in> ball lx u) sequentially"
"eventually (\<lambda>n. ?x n \<in> ball lx u) sequentially"
- by (auto simp: dist_commute Lim mem_ball)
+ by (auto simp: dist_commute Lim)
moreover have "eventually (\<lambda>n. n > L) sequentially"
by (metis filterlim_at_top_dense filterlim_real_sequentially)
ultimately
@@ -721,7 +721,7 @@
hence "dist (f (?t n) (?y n)) (f (?t n) (?x n)) \<le> L * dist (?y n) (?x n)"
using assms xy t
unfolding dist_norm[symmetric]
- by (intro lipschitz_onD[OF L(2)]) (auto simp: mem_ball mem_cball)
+ by (intro lipschitz_onD[OF L(2)]) (auto)
also have "\<dots> \<le> n * dist (?y n) (?x n)"
using elim by (intro mult_right_mono) auto
also have "\<dots> \<le> rx (ry (rt n)) * dist (?y n) (?x n)"
@@ -772,7 +772,7 @@
by metis
then show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> A. L-lipschitz_on (cball x u \<inter> B) (\<lambda>b. (f t b, g t b))"
by (intro exI[where x="min u v"])
- (force intro: lipschitz_on_subset intro!: lipschitz_on_Pair simp: mem_cball)
+ (force intro: lipschitz_on_subset intro!: lipschitz_on_Pair)
qed
lemma local_lipschitz_constI: "local_lipschitz S T (\<lambda>t x. f t)"
@@ -809,7 +809,7 @@
then have "compact (f' ` (cball t v \<times> cball x u))"
by (auto intro!: compact_continuous_image continuous_on_subset[OF cont_f'])
then obtain B where B: "B > 0" "\<And>s y. s \<in> cball t v \<Longrightarrow> y \<in> cball x u \<Longrightarrow> norm (f' (s, y)) \<le> B"
- by (auto dest!: compact_imp_bounded simp: bounded_pos simp: mem_ball)
+ by (auto dest!: compact_imp_bounded simp: bounded_pos)
have lipschitz: "B-lipschitz_on (cball x (min u v) \<inter> X) (f s)" if s: "s \<in> cball t v" for s
proof -
@@ -824,13 +824,13 @@
for y z
using s that
by (intro differentiable_bound[OF convex_cball deriv])
- (auto intro!: B simp: norm_blinfun.rep_eq[symmetric] mem_cball)
+ (auto intro!: B simp: norm_blinfun.rep_eq[symmetric])
then show ?thesis
using \<open>0 < B\<close>
- by (auto intro!: lipschitz_onI simp: dist_norm mem_cball)
+ by (auto intro!: lipschitz_onI simp: dist_norm)
qed
show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f t)"
- by (force intro: exI[where x="min u v"] exI[where x=B] intro!: lipschitz simp: u v mem_cball)
+ by (force intro: exI[where x="min u v"] exI[where x=B] intro!: lipschitz simp: u v)
qed
end
--- a/src/HOL/Analysis/Product_Vector.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy Fri Nov 29 15:06:04 2019 +0100
@@ -522,8 +522,7 @@
lemma dimension_pair: "p.dimension = vs1.dimension + vs2.dimension"
using dim_Times[OF vs1.subspace_UNIV vs2.subspace_UNIV]
- by (auto simp: p.dim_UNIV vs1.dim_UNIV vs2.dim_UNIV
- p.dimension_def vs1.dimension_def vs2.dimension_def)
+ by (auto simp: p.dimension_def vs1.dimension_def vs2.dimension_def)
end
--- a/src/HOL/Analysis/Riemann_Mapping.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Riemann_Mapping.thy Fri Nov 29 15:06:04 2019 +0100
@@ -99,7 +99,7 @@
"\<And>z. z \<in> ball 0 1 \<Longrightarrow> g (f z) = z"
proof
show "Moebius_function 0 a holomorphic_on ball 0 1" "Moebius_function 0 (-a) holomorphic_on ball 0 1"
- using Moebius_function_holomorphic assms mem_ball_0 by auto
+ using Moebius_function_holomorphic assms by auto
show "Moebius_function 0 a a = 0"
by (simp add: Moebius_function_eq_zero)
show "Moebius_function 0 a ` ball 0 1 \<subseteq> ball 0 1"
--- a/src/HOL/Analysis/Starlike.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy Fri Nov 29 15:06:04 2019 +0100
@@ -1143,7 +1143,7 @@
hence *: "0 < e/norm(z-x)" using e False by auto
define y where "y = z + (e/norm(z-x)) *\<^sub>R (z-x)"
have yball: "y \<in> cball z e"
- using mem_cball y_def dist_norm[of z y] e by auto
+ using y_def dist_norm[of z y] e by auto
have "x \<in> affine hull closure S"
using x rel_interior_subset_closure hull_inc[of x "closure S"] by blast
moreover have "z \<in> affine hull closure S"
--- a/src/HOL/Library/Cardinality.thy Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Library/Cardinality.thy Fri Nov 29 15:06:04 2019 +0100
@@ -236,7 +236,7 @@
instance
by standard
(auto simp add: finite_UNIV_integer_def card_UNIV_integer_def card_eq_0_iff
- type_definition.univ [OF type_definition_integer] infinite_UNIV_int
+ type_definition.univ [OF type_definition_integer]
dest!: finite_imageD intro: inj_onI)
end