--- a/src/HOL/HOL.thy Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/HOL.thy Mon Sep 21 21:46:14 2015 +0200
@@ -1691,8 +1691,8 @@
\<close>
-text{* Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
-not to simplify the argument and to solve it by an assumption. *}
+text\<open>Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
+not to simplify the argument and to solve it by an assumption.\<close>
definition ASSUMPTION :: "bool \<Rightarrow> bool" where
"ASSUMPTION A \<equiv> A"
@@ -1706,7 +1706,7 @@
lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
by(simp add: ASSUMPTION_def)
-setup {*
+setup \<open>
let
val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
@@ -1714,7 +1714,7 @@
in
map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
end
-*}
+\<close>
subsection \<open>Code generator setup\<close>
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Sep 21 21:46:14 2015 +0200
@@ -81,7 +81,7 @@
using assms
by (auto simp: piecewise_differentiable_on_def)
have finabc: "finite ({a,b,c} \<union> (s \<union> t))"
- by (metis `finite s` `finite t` finite_Un finite_insert finite.emptyI)
+ by (metis \<open>finite s\<close> \<open>finite t\<close> finite_Un finite_insert finite.emptyI)
have "continuous_on {a..c} f" "continuous_on {c..b} g"
using assms piecewise_differentiable_on_def by auto
then have "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)"
@@ -462,7 +462,7 @@
by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
have "continuous_on {0..1} g1"
using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
- with `finite s` show ?thesis
+ with \<open>finite s\<close> show ?thesis
apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
apply (rule_tac x="insert 1 ((op*2)`s)" in exI)
apply (simp add: g1D con_g1)
@@ -509,7 +509,7 @@
by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
have "continuous_on {0..1} g2"
using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast
- with `finite s` show ?thesis
+ with \<open>finite s\<close> show ?thesis
apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
apply (rule_tac x="insert 0 ((\<lambda>x. 2 * x - 1) ` s)" in exI)
apply (simp add: g2D con_g2)
@@ -2253,11 +2253,11 @@
def shrink \<equiv> "\<lambda>x. x - e *\<^sub>R (x - d)"
let ?pathint = "\<lambda>x y. path_integral(linepath x y) f"
have e: "0 < e" "e \<le> 1" "e \<le> d1 / (4 * C)" "e \<le> cmod y / 24 / C / B"
- using d1_pos `C>0` `B>0` ynz by (simp_all add: e_def)
+ using d1_pos \<open>C>0\<close> \<open>B>0\<close> ynz by (simp_all add: e_def)
then have eCB: "24 * e * C * B \<le> cmod y"
- using `C>0` `B>0` by (simp add: field_simps)
+ using \<open>C>0\<close> \<open>B>0\<close> by (simp add: field_simps)
have e_le_d1: "e * (4 * C) \<le> d1"
- using e `C>0` by (simp add: field_simps)
+ using e \<open>C>0\<close> by (simp add: field_simps)
have "shrink a \<in> interior(convex hull {a,b,c})"
"shrink b \<in> interior(convex hull {a,b,c})"
"shrink c \<in> interior(convex hull {a,b,c})"
@@ -2276,10 +2276,10 @@
have sh_eq: "\<And>a b d::complex. (b - e *\<^sub>R (b - d)) - (a - e *\<^sub>R (a - d)) - (b - a) = e *\<^sub>R (a - b)"
by (simp add: algebra_simps)
have "cmod y / (24 * C) \<le> cmod y / cmod (b - a) / 12"
- using False `C>0` diff_2C [of b a] ynz
+ using False \<open>C>0\<close> diff_2C [of b a] ynz
by (auto simp: divide_simps hull_inc)
have less_C: "\<lbrakk>u \<in> convex hull {a, b, c}; 0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> x * cmod u < C" for x u
- apply (cases "x=0", simp add: `0<C`)
+ apply (cases "x=0", simp add: \<open>0<C\<close>)
using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast
{ fix u v
assume uv: "u \<in> convex hull {a, b, c}" "v \<in> convex hull {a, b, c}" "u\<noteq>v"
@@ -2292,7 +2292,7 @@
using shr_uv by (blast intro: Bnf linepath_in_convex_hull interior_subset [THEN subsetD])
have By_uv: "B * (12 * (e * cmod (u - v))) \<le> cmod y"
apply (rule order_trans [OF _ eCB])
- using e `B>0` diff_2C [of u v] uv
+ using e \<open>B>0\<close> diff_2C [of u v] uv
by (auto simp: field_simps)
{ fix x::real assume x: "0\<le>x" "x\<le>1"
have cmod_less_4C: "cmod ((1 - x) *\<^sub>R u - (1 - x) *\<^sub>R d) + cmod (x *\<^sub>R v - x *\<^sub>R d) < (C+C) + (C+C)"
@@ -2303,7 +2303,7 @@
have ll: "linepath (shrink u) (shrink v) x - linepath u v x = -e * ((1 - x) *\<^sub>R (u - d) + x *\<^sub>R (v - d))"
by (simp add: linepath_def shrink_def algebra_simps scaleR_conv_of_real)
have cmod_less_dt: "cmod (linepath (shrink u) (shrink v) x - linepath u v x) < d1"
- using `e>0`
+ using \<open>e>0\<close>
apply (simp add: ll norm_mult scaleR_diff_right)
apply (rule less_le_trans [OF _ e_le_d1])
using cmod_less_4C
@@ -2313,7 +2313,7 @@
using x uv shr_uv cmod_less_dt
by (auto simp: hull_inc intro: d1 interior_subset [THEN subsetD] linepath_in_convex_hull)
also have "... \<le> cmod y / cmod (v - u) / 12"
- using False uv `C>0` diff_2C [of v u] ynz
+ using False uv \<open>C>0\<close> diff_2C [of v u] ynz
by (auto simp: divide_simps hull_inc)
finally have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) \<le> cmod y / cmod (v - u) / 12"
by simp
@@ -2324,7 +2324,7 @@
\<le> cmod y / 6"
apply (rule order_trans [of _ "B*((norm y / 24 / C / B)*2*C) + (2*C)*(norm y /24 / C)"])
apply (rule add_mono [OF mult_mono])
- using By_uv e `0 < B` `0 < C` x ynz
+ using By_uv e \<open>0 < B\<close> \<open>0 < C\<close> x ynz
apply (simp_all add: cmod_fuv cmod_shr cmod_12_le hull_inc)
apply (simp add: field_simps)
done
@@ -2339,7 +2339,7 @@
[of "B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)"
"\<lambda>x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)"
_ 0 1 ])
- using ynz `0 < B` `0 < C`
+ using ynz \<open>0 < B\<close> \<open>0 < C\<close>
apply (simp_all del: le_divide_eq_numeral1)
apply (simp add: has_integral_sub has_path_integral_linepath [symmetric] has_path_integral_integral
fpi_uv f_uv path_integrable_continuous_linepath, clarify)
@@ -2376,7 +2376,7 @@
by (simp add: contf compact_convex_hull compact_uniformly_continuous)
ultimately have "False"
unfolding uniformly_continuous_on_def
- by (force simp: ynz `0 < C` dist_norm)
+ by (force simp: ynz \<open>0 < C\<close> dist_norm)
then show ?thesis ..
qed
}
@@ -2411,7 +2411,7 @@
case False
show "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
apply (rule less.hyps [of "s'"])
- using False d `finite s` interior_subset
+ using False d \<open>finite s\<close> interior_subset
apply (auto intro!: less.prems)
done
next
@@ -2420,7 +2420,7 @@
by (meson True hull_subset insert_subset convex_hull_subset)
have abd: "(f has_path_integral 0) (linepath a b +++ linepath b d +++ linepath d a)"
apply (rule less.hyps [of "s'"])
- using True d `finite s` not_in_interior_convex_hull_3
+ using True d \<open>finite s\<close> not_in_interior_convex_hull_3
apply (auto intro!: less.prems continuous_on_subset [OF _ *])
apply (metis * insert_absorb insert_subset interior_mono)
done
@@ -2428,7 +2428,7 @@
by (meson True hull_subset insert_subset convex_hull_subset)
have bcd: "(f has_path_integral 0) (linepath b c +++ linepath c d +++ linepath d b)"
apply (rule less.hyps [of "s'"])
- using True d `finite s` not_in_interior_convex_hull_3
+ using True d \<open>finite s\<close> not_in_interior_convex_hull_3
apply (auto intro!: less.prems continuous_on_subset [OF _ *])
apply (metis * insert_absorb insert_subset interior_mono)
done
@@ -2436,7 +2436,7 @@
by (meson True hull_subset insert_subset convex_hull_subset)
have cad: "(f has_path_integral 0) (linepath c a +++ linepath a d +++ linepath d c)"
apply (rule less.hyps [of "s'"])
- using True d `finite s` not_in_interior_convex_hull_3
+ using True d \<open>finite s\<close> not_in_interior_convex_hull_3
apply (auto intro!: less.prems continuous_on_subset [OF _ *])
apply (metis * insert_absorb insert_subset interior_mono)
done
@@ -2518,7 +2518,7 @@
then obtain d1 where d1: "d1>0" and d1_less: "\<And>y. cmod (y - x) < d1 \<Longrightarrow> cmod (f y - f x) < e/2"
unfolding continuous_at Lim_at dist_norm using e
by (drule_tac x="e/2" in spec) force
- obtain d2 where d2: "d2>0" "ball x d2 \<subseteq> s" using `open s` x
+ obtain d2 where d2: "d2>0" "ball x d2 \<subseteq> s" using \<open>open s\<close> x
by (auto simp: open_contains_ball)
have dpos: "min d1 d2 > 0" using d1 d2 by simp
{ fix y
@@ -2556,7 +2556,7 @@
apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right)
apply (rule Lim_transform [OF * Lim_eventually])
apply (simp add: inverse_eq_divide [symmetric] eventually_at)
- using `open s` x
+ using \<open>open s\<close> x
apply (force simp: dist_norm open_contains_ball)
done
qed
@@ -2802,7 +2802,7 @@
proof -
{ fix z
assume z: "z \<in> s"
- obtain d where d: "d>0" "ball z d \<subseteq> s" using `open s` z
+ obtain d where d: "d>0" "ball z d \<subseteq> s" using \<open>open s\<close> z
by (auto simp: open_contains_ball)
then have contfb: "continuous_on (ball z d) f"
using contf continuous_on_subset by blast
@@ -2839,16 +2839,16 @@
apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros)
done
-text{*Key fact that path integral is the same for a "nearby" path. This is the
+text\<open>Key fact that path integral is the same for a "nearby" path. This is the
main lemma for the homotopy form of Cauchy's theorem and is also useful
if we want "without loss of generality" to assume some nice properties of a
path (e.g. smoothness). It can also be used to define the integrals of
analytic functions over arbitrary continuous paths. This is just done for
winding numbers now.
-*}
+\<close>
-text{*This formulation covers two cases: @{term g} and @{term h} share their
- start and end points; @{term g} and @{term h} both loop upon themselves. *}
+text\<open>This formulation covers two cases: @{term g} and @{term h} share their
+ start and end points; @{term g} and @{term h} both loop upon themselves.\<close>
lemma path_integral_nearby:
assumes os: "open s"
and p: "path p" "path_image p \<subseteq> s"
@@ -2876,7 +2876,7 @@
by blast
then obtain k where k: "k \<subseteq> {0..1}" "finite k" and D_eq: "D = ((\<lambda>z. ball z (ee z / 3)) \<circ> p) ` k"
apply (simp add: cover_def path_image_def image_comp)
- apply (blast dest!: finite_subset_image [OF `finite D`])
+ apply (blast dest!: finite_subset_image [OF \<open>finite D\<close>])
done
then have kne: "k \<noteq> {}"
using D by auto
@@ -2905,7 +2905,7 @@
{ fix t::real
assume t: "0 \<le> t" "t \<le> 1"
then obtain u where u: "u \<in> k" and ptu: "p t \<in> ball(p u) (ee(p u) / 3)"
- using `path_image p \<subseteq> \<Union>D` D_eq by (force simp: path_image_def)
+ using \<open>path_image p \<subseteq> \<Union>D\<close> D_eq by (force simp: path_image_def)
then have ele: "e \<le> ee (p u)" using fin_eep
by (simp add: e_def)
have "cmod (g t - p t) < e / 3" "cmod (h t - p t) < e / 3"
@@ -2950,7 +2950,7 @@
next
case (Suc n)
obtain t where t: "t \<in> k" and "p (n/N) \<in> ball(p t) (ee(p t) / 3)"
- using `path_image p \<subseteq> \<Union>D` [THEN subsetD, where c="p (n/N)"] D_eq N Suc.prems
+ using \<open>path_image p \<subseteq> \<Union>D\<close> [THEN subsetD, where c="p (n/N)"] D_eq N Suc.prems
by (force simp: path_image_def)
then have ptu: "cmod (p t - p (n/N)) < ee (p t) / 3"
by (simp add: dist_norm)
@@ -2988,7 +2988,7 @@
using ptgh_ee [of "n/N"] Suc.prems
by (auto simp: field_simps real_of_nat_def dist_norm dest: segment_furthest_le [where y="p t"])
then have gh_ns: "closed_segment (g (n/N)) (h (n/N)) \<subseteq> s"
- using `N>0` Suc.prems
+ using \<open>N>0\<close> Suc.prems
apply (simp add: real_of_nat_def path_image_join field_simps closed_segment_commute)
apply (erule order_trans)
apply (simp add: ee pi t)
@@ -2998,14 +2998,14 @@
using ptgh_ee [of "(1+n)/N"] Suc.prems
by (auto simp: field_simps real_of_nat_def dist_norm dest: segment_furthest_le [where y="p t"])
then have gh_n's: "closed_segment (g ((1 + n) / N)) (h ((1 + n) / N)) \<subseteq> s"
- using `N>0` Suc.prems ee pi t
+ using \<open>N>0\<close> Suc.prems ee pi t
by (auto simp: Path_Connected.path_image_join field_simps)
have pi_subset_ball:
"path_image (subpath (n/N) ((1+n) / N) g +++ linepath (g ((1+n) / N)) (h ((1+n) / N)) +++
subpath ((1+n) / N) (n/N) h +++ linepath (h (n/N)) (g (n/N)))
\<subseteq> ball (p t) (ee (p t))"
apply (intro subset_path_image_join pi_hgn pi_ghn')
- using `N>0` Suc.prems
+ using \<open>N>0\<close> Suc.prems
apply (auto simp: dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
done
have pi0: "(f has_path_integral 0)
@@ -3126,7 +3126,7 @@
where d: "0 < d"
and p: "polynomial_function p" "path_image p \<subseteq> s"
and pi: "\<And>f. f holomorphic_on s \<Longrightarrow> path_integral g f = path_integral p f"
- using path_integral_nearby_ends [OF s `path g` pag]
+ using path_integral_nearby_ends [OF s \<open>path g\<close> pag]
apply clarify
apply (drule_tac x=g in spec)
apply (simp only: assms)
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Sep 21 21:46:14 2015 +0200
@@ -9467,7 +9467,7 @@
using g by (simp add: Fun.image_comp)
then show "coplanar s"
unfolding coplanar_def
- using affine_hull_linear_image [of g "{u,v,w}" for u v w] `linear g` linear_conv_bounded_linear
+ using affine_hull_linear_image [of g "{u,v,w}" for u v w] \<open>linear g\<close> linear_conv_bounded_linear
by fastforce
qed
(*The HOL Light proof is simply
@@ -9651,7 +9651,7 @@
then have *: "\<And>x. x \<in> closure s \<Longrightarrow> setdist s t \<le> dist x y"
apply (rule continuous_ge_on_closure)
apply assumption
- apply (blast intro: setdist_le_dist `y \<in> t` )
+ apply (blast intro: setdist_le_dist \<open>y \<in> t\<close> )
done
} note * = this
show ?thesis
@@ -9687,7 +9687,7 @@
assumes s: "closed s" and t: "compact t"
and "s \<noteq> {}" "t \<noteq> {}"
shows "\<exists>x \<in> s. \<exists>y \<in> t. dist x y = setdist s t"
- using setdist_compact_closed [OF t s `t \<noteq> {}` `s \<noteq> {}`]
+ using setdist_compact_closed [OF t s \<open>t \<noteq> {}\<close> \<open>s \<noteq> {}\<close>]
by (metis dist_commute setdist_sym)
lemma setdist_eq_0I: "\<lbrakk>x \<in> s; x \<in> t\<rbrakk> \<Longrightarrow> setdist s t = 0"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Sep 21 21:46:14 2015 +0200
@@ -2889,7 +2889,7 @@
apply (rule less_trans[OF _ *])
apply (subst N1', rule d(2)[of "p (N1+N2)"])
using N1' as(1) as(2) dp
- apply (simp add: `\<forall>x. p x tagged_division_of cbox a b \<and> (\<lambda>xa. \<Inter>{d i xa |i. i \<in> {0..x}}) fine p x`)
+ apply (simp add: \<open>\<forall>x. p x tagged_division_of cbox a b \<and> (\<lambda>xa. \<Inter>{d i xa |i. i \<in> {0..x}}) fine p x\<close>)
using N2 le_add2 by blast
}
ultimately show "\<exists>d. gauge d \<and>
@@ -3602,11 +3602,11 @@
proof (cases "f x = neutral opp")
case True
then show ?thesis
- using assms `x \<notin> s`
+ using assms \<open>x \<notin> s\<close>
by (auto simp: iterate_def support_clauses)
next
case False
- with `x \<notin> s` \<open>finite s\<close> support_subset show ?thesis
+ with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis
apply (simp add: iterate_def fold'_def support_clauses)
apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
apply (force simp add: )+
@@ -3962,7 +3962,7 @@
case True
show "iterate opp d f = f (cbox a b)"
unfolding operativeD(1)[OF assms(2) True]
- proof (rule iterate_eq_neutral[OF `monoidal opp`])
+ proof (rule iterate_eq_neutral[OF \<open>monoidal opp\<close>])
fix x
assume x: "x \<in> d"
then show "f x = neutral opp"
@@ -3990,9 +3990,9 @@
note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
moreover
have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
- using division_ofD(2,2,3)[OF `d division_of cbox a b` as]
+ using division_ofD(2,2,3)[OF \<open>d division_of cbox a b\<close> as]
apply (metis j subset_box(1) uv(1))
- by (metis `cbox u v \<subseteq> cbox a b` j subset_box(1) uv(1))
+ by (metis \<open>cbox u v \<subseteq> cbox a b\<close> j subset_box(1) uv(1))
ultimately have "u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j"
unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
then have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
@@ -4001,7 +4001,7 @@
by blast
have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps)
- note this[unfolded division_ofD(6)[OF `d division_of cbox a b`,symmetric] Union_iff]
+ note this[unfolded division_ofD(6)[OF \<open>d division_of cbox a b\<close>,symmetric] Union_iff]
then guess i .. note i=this
guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this
have "cbox a b \<in> d"
@@ -4059,18 +4059,18 @@
def d2 \<equiv> "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
def cb \<equiv> "(\<Sum>i\<in>Basis. (if i = k then c else b\<bullet>i) *\<^sub>R i)::'a"
def ca \<equiv> "(\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)::'a"
- note division_points_psubset[OF `d division_of cbox a b` ab kc(1-2) j]
+ note division_points_psubset[OF \<open>d division_of cbox a b\<close> ab kc(1-2) j]
note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)]
then have *: "(iterate opp d1 f) = f (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
"(iterate opp d2 f) = f (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
unfolding interval_split[OF kc(4)]
apply (rule_tac[!] "1.hyps"[rule_format])
- using division_split[OF `d division_of cbox a b`, where k=k and c=c]
- apply (simp_all add: interval_split 1 kc d1_def d2_def division_points_finite[OF `d division_of cbox a b`])
+ using division_split[OF \<open>d division_of cbox a b\<close>, where k=k and c=c]
+ apply (simp_all add: interval_split 1 kc d1_def d2_def division_points_finite[OF \<open>d division_of cbox a b\<close>])
done
{ fix l y
assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} = y \<inter> {x. x \<bullet> k \<le> c}" "l \<noteq> y"
- from division_ofD(4)[OF `d division_of cbox a b` this(1)] guess u v by (elim exE) note leq=this
+ from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
have "f (l \<inter> {x. x \<bullet> k \<le> c}) = neutral opp"
unfolding leq interval_split[OF kc(4)]
apply (rule operativeD(1) 1)+
@@ -4079,7 +4079,7 @@
} note fxk_le = this
{ fix l y
assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} = y \<inter> {x. c \<le> x \<bullet> k}" "l \<noteq> y"
- from division_ofD(4)[OF `d division_of cbox a b` this(1)] guess u v by (elim exE) note leq=this
+ from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
have "f (l \<inter> {x. x \<bullet> k \<ge> c}) = neutral opp"
unfolding leq interval_split[OF kc(4)]
apply (rule operativeD(1) 1)+
@@ -4102,7 +4102,7 @@
apply (force simp add: empty_as_interval[symmetric] fxk_ge)+
done
also have *: "\<forall>x\<in>d. f x = opp (f (x \<inter> {x. x \<bullet> k \<le> c})) (f (x \<inter> {x. c \<le> x \<bullet> k}))"
- unfolding forall_in_division[OF `d division_of cbox a b`]
+ unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
using assms(2) kc(4) by blast
have "opp (iterate opp d (\<lambda>l. f (l \<inter> {x. x \<bullet> k \<le> c}))) (iterate opp d (\<lambda>l. f (l \<inter> {x. c \<le> x \<bullet> k}))) =
iterate opp d f"
@@ -4689,7 +4689,7 @@
proof (cases "content (cbox a b) = 0")
case True
then have ce: "content (cbox a b) < e"
- by (metis `0 < e`)
+ by (metis \<open>0 < e\<close>)
show ?thesis
apply (rule that[of 1])
apply simp
@@ -6112,10 +6112,10 @@
have one: "(- 1) ^ p' * (- 1) ^ p' = (1::real)"
and "{..<p} \<inter> {i. p = Suc i} = {p - 1}"
for p'
- using `p > 0`
+ using \<open>p > 0\<close>
by (auto simp: power_mult_distrib[symmetric])
then have "?sum b = f b"
- using Suc_pred'[OF `p > 0`]
+ using Suc_pred'[OF \<open>p > 0\<close>]
by (simp add: diff_eq_eq Dg_def power_0_left le_Suc_eq if_distrib
cond_application_beta setsum.If_cases f0)
also
@@ -6428,7 +6428,7 @@
{ fix e::real
assume "e > 0"
obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {a..b}; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> norm(f x' - f x) \<le> e"
- using `e>0` fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
+ using \<open>e>0\<close> fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
have "norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
if y: "y \<in> {a..b}" and yx: "\<bar>y - x\<bar> < d" for y
proof (cases "y < x")
@@ -6447,7 +6447,7 @@
using False
apply (simp add: abs_eq_content del: content_real_if)
apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
- using yx False d x y `e>0` apply (auto simp add: Idiff fux_int)
+ using yx False d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
done
next
case True
@@ -6465,13 +6465,13 @@
using True
apply (simp add: abs_eq_content del: content_real_if)
apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
- using yx True d x y `e>0` apply (auto simp add: Idiff fux_int)
+ using yx True d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
done
then show ?thesis
by (simp add: algebra_simps norm_minus_commute)
qed
then have "\<exists>d>0. \<forall>y\<in>{a..b}. \<bar>y - x\<bar> < d \<longrightarrow> norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
- using `d>0` by blast
+ using \<open>d>0\<close> by blast
}
then show ?thesis
by (simp add: has_vector_derivative_def has_derivative_within_alt bounded_linear_scaleR_left)
@@ -11913,7 +11913,7 @@
by simp
qed
-subsection{*Compute a double integral using iterated integrals and switching the order of integration*}
+subsection\<open>Compute a double integral using iterated integrals and switching the order of integration\<close>
lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
by auto
@@ -12197,7 +12197,7 @@
using compact_uniformly_continuous [OF assms compact_cbox]
apply (simp add: uniformly_continuous_on_def dist_norm)
apply (drule_tac x="e / 2 / content?CBOX" in spec)
- using cbp `0 < e`
+ using cbp \<open>0 < e\<close>
apply (auto simp: zero_less_mult_iff)
apply (rename_tac k)
apply (rule_tac e1=k in fine_division_exists [OF gauge_ball, where a = "(a,c)" and b = "(b,d)"])
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Sep 21 21:46:14 2015 +0200
@@ -462,7 +462,7 @@
apply auto
done
-lemma approachable_lt_le2: --{*like the above, but pushes aside an extra formula*}
+lemma approachable_lt_le2: --\<open>like the above, but pushes aside an extra formula\<close>
"(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
apply auto
apply (rule_tac x="d/2" in exI, auto)
@@ -562,7 +562,7 @@
using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
by (auto simp add: field_simps cong: conj_cong)
-text{*Bernoulli's inequality*}
+text\<open>Bernoulli's inequality\<close>
lemma Bernoulli_inequality:
fixes x :: real
assumes "-1 \<le> x"
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Sep 21 21:46:14 2015 +0200
@@ -58,15 +58,15 @@
def e' \<equiv> "e/3"
assume "0 < e"
then have "0 < e'" by (simp add: e'_def)
- from uniform_limitD[OF uc `0 < e'`]
+ from uniform_limitD[OF uc \<open>0 < e'\<close>]
have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (h x) (f n x) < e'"
by (simp add: dist_commute)
moreover
from f
have "\<forall>\<^sub>F n in F. \<forall>\<^sub>F x in at x within S. dist (g n) (f n x) < e'"
- by eventually_elim (auto dest!: tendstoD[OF _ `0 < e'`] simp: dist_commute)
+ by eventually_elim (auto dest!: tendstoD[OF _ \<open>0 < e'\<close>] simp: dist_commute)
moreover
- from tendstoD[OF g `0 < e'`] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
+ from tendstoD[OF g \<open>0 < e'\<close>] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
by (simp add: dist_commute)
ultimately
have "\<forall>\<^sub>F _ in F. \<forall>\<^sub>F x in at x within S. dist (h x) l < e"
@@ -80,7 +80,7 @@
show ?case
proof eventually_elim
case (elim x)
- from fh[rule_format, OF `x \<in> S`] elim(1)
+ from fh[rule_format, OF \<open>x \<in> S\<close>] elim(1)
have "dist (h x) (g n) < e' + e'"
by (rule dist_triangle_lt[OF add_strict_mono])
from dist_triangle_lt[OF add_strict_mono, OF this gl]
@@ -88,7 +88,7 @@
qed
qed
thus "\<forall>\<^sub>F x in at x within S. dist (h x) l < e"
- using eventually_happens by (metis `\<not>trivial_limit F`)
+ using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
qed
lemma
@@ -122,7 +122,7 @@
proof (rule uniform_limitI)
fix e :: real
assume "0 < e"
- from suminf_exist_split[OF `0 < e` `summable M`]
+ from suminf_exist_split[OF \<open>0 < e\<close> \<open>summable M\<close>]
have "\<forall>\<^sub>F k in sequentially. norm (\<Sum>i. M (i + k)) < e"
by (auto simp: eventually_sequentially)
thus "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
@@ -132,16 +132,16 @@
proof safe
fix x assume "x \<in> A"
have "\<exists>N. \<forall>n\<ge>N. norm (f n x) \<le> M n"
- using assms(1)[OF `x \<in> A`] by simp
+ using assms(1)[OF \<open>x \<in> A\<close>] by simp
hence summable_norm_f: "summable (\<lambda>n. norm (f n x))"
- by(rule summable_norm_comparison_test[OF _ `summable M`])
+ by(rule summable_norm_comparison_test[OF _ \<open>summable M\<close>])
have summable_f: "summable (\<lambda>n. f n x)"
using summable_norm_cancel[OF summable_norm_f] .
have summable_norm_f_plus_k: "summable (\<lambda>i. norm (f (i + k) x))"
using summable_ignore_initial_segment[OF summable_norm_f]
by auto
have summable_M_plus_k: "summable (\<lambda>i. M (i + k))"
- using summable_ignore_initial_segment[OF `summable M`]
+ using summable_ignore_initial_segment[OF \<open>summable M\<close>]
by auto
have "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) = norm ((\<Sum>i. f i x) - (\<Sum>i<k. f i x))"
@@ -152,7 +152,7 @@
using summable_norm[OF summable_norm_f_plus_k] .
also have "... \<le> (\<Sum>i. M (i + k))"
by (rule suminf_le[OF _ summable_norm_f_plus_k summable_M_plus_k])
- (simp add: assms(1)[OF `x \<in> A`])
+ (simp add: assms(1)[OF \<open>x \<in> A\<close>])
finally show "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) < e"
using elim by auto
qed
@@ -163,12 +163,12 @@
by simp
named_theorems uniform_limit_intros "introduction rules for uniform_limit"
-setup {*
+setup \<open>
Global_Theory.add_thms_dynamic (@{binding uniform_limit_eq_intros},
fn context =>
Named_Theorems.get (Context.proof_of context) @{named_theorems uniform_limit_intros}
|> map_filter (try (fn thm => @{thm uniform_limit_eq_rhs} OF [thm])))
-*}
+\<close>
lemma (in bounded_linear) uniform_limit[uniform_limit_intros]:
assumes "uniform_limit X g l F"
@@ -178,7 +178,7 @@
from pos_bounded obtain K
where K: "\<And>x y. dist (f x) (f y) \<le> K * dist x y" "K > 0"
by (auto simp: ac_simps dist_norm diff[symmetric])
- assume "0 < e" with `K > 0` have "e / K > 0" by simp
+ assume "0 < e" with \<open>K > 0\<close> have "e / K > 0" by simp
from uniform_limitD[OF assms this]
show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f (g n x)) (f (l x)) < e"
by eventually_elim (metis le_less_trans mult.commute pos_less_divide_eq K)
@@ -245,15 +245,15 @@
and Kl: "Kl > 0" "\<And>x. x \<in> X \<Longrightarrow> norm (l x) \<le> Kl"
by (auto simp: bounded_pos)
hence "K * Km * 4 > 0" "K * Kl * 4 > 0"
- using `K > 0`
+ using \<open>K > 0\<close>
by simp_all
assume "0 < e"
hence "sqrt e > 0" by simp
- from uniform_limitD[OF assms(1) divide_pos_pos[OF this `sqrt (K*4) > 0`]]
- uniform_limitD[OF assms(2) divide_pos_pos[OF this `sqrt (K*4) > 0`]]
- uniform_limitD[OF assms(1) divide_pos_pos[OF `e > 0` `K * Km * 4 > 0`]]
- uniform_limitD[OF assms(2) divide_pos_pos[OF `e > 0` `K * Kl * 4 > 0`]]
+ from uniform_limitD[OF assms(1) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
+ uniform_limitD[OF assms(2) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
+ uniform_limitD[OF assms(1) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Km * 4 > 0\<close>]]
+ uniform_limitD[OF assms(2) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Kl * 4 > 0\<close>]]
show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
proof eventually_elim
case (elim n)
@@ -266,31 +266,31 @@
norm (prod (l x) (g n x - m x))"
by (auto simp: dist_norm prod_diff_prod intro: order_trans norm_triangle_ineq add_mono)
also note K(2)[of "f n x - l x" "g n x - m x"]
- also from elim(1)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
+ also from elim(1)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
have "norm (f n x - l x) \<le> sqrt e / sqrt (K * 4)"
by simp
- also from elim(2)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
+ also from elim(2)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
have "norm (g n x - m x) \<le> sqrt e / sqrt (K * 4)"
by simp
also have "sqrt e / sqrt (K * 4) * (sqrt e / sqrt (K * 4)) * K = e / 4"
- using `K > 0` `e > 0` by auto
+ using \<open>K > 0\<close> \<open>e > 0\<close> by auto
also note K(2)[of "f n x - l x" "m x"]
also note K(2)[of "l x" "g n x - m x"]
- also from elim(3)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
+ also from elim(3)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
have "norm (f n x - l x) \<le> e / (K * Km * 4)"
by simp
- also from elim(4)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
+ also from elim(4)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
have "norm (g n x - m x) \<le> e / (K * Kl * 4)"
by simp
- also note Kl(2)[OF `_ \<in> X`]
- also note Km(2)[OF `_ \<in> X`]
+ also note Kl(2)[OF \<open>_ \<in> X\<close>]
+ also note Km(2)[OF \<open>_ \<in> X\<close>]
also have "e / (K * Km * 4) * Km * K = e / 4"
- using `K > 0` `Km > 0` by simp
+ using \<open>K > 0\<close> \<open>Km > 0\<close> by simp
also have " Kl * (e / (K * Kl * 4)) * K = e / 4"
- using `K > 0` `Kl > 0` by simp
- also have "e / 4 + e / 4 + e / 4 < e" using `e > 0` by simp
+ using \<open>K > 0\<close> \<open>Kl > 0\<close> by simp
+ also have "e / 4 + e / 4 + e / 4 < e" using \<open>e > 0\<close> by simp
finally show "dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
- using `K > 0` `Kl > 0` `Km > 0` `e > 0`
+ using \<open>K > 0\<close> \<open>Kl > 0\<close> \<open>Km > 0\<close> \<open>e > 0\<close>
by (simp add: algebra_simps mult_right_mono divide_right_mono)
qed
qed
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy Mon Sep 21 21:46:14 2015 +0200
@@ -1,4 +1,4 @@
-section{*Bernstein-Weierstrass and Stone-Weierstrass Theorems*}
+section\<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
theory Weierstrass
imports Uniform_Limit Path_Connected
@@ -11,7 +11,7 @@
(*Power.thy:*)
declare power_divide [where b = "numeral w" for w, simp del]
-subsection {*Bernstein polynomials*}
+subsection \<open>Bernstein polynomials\<close>
definition Bernstein :: "[nat,nat,real] \<Rightarrow> real" where
"Bernstein n k x \<equiv> of_nat (n choose k) * x ^ k * (1 - x) ^ (n - k)"
@@ -65,7 +65,7 @@
by auto
qed
-subsection {*Explicit Bernstein version of the 1D Weierstrass approximation theorem*}
+subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
lemma Bernstein_Weierstrass:
fixes f :: "real \<Rightarrow> real"
@@ -87,11 +87,11 @@
assume n: "Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>) \<le> n" and x: "0 \<le> x" "x \<le> 1"
have "0 < n" using n by simp
have ed0: "- (e * d\<^sup>2) < 0"
- using e `0<d` by simp
+ using e \<open>0<d\<close> by simp
also have "... \<le> M * 4"
- using `0\<le>M` by simp
+ using \<open>0\<le>M\<close> by simp
finally have [simp]: "real (nat \<lceil>4 * M / (e * d\<^sup>2)\<rceil>) = real \<lceil>4 * M / (e * d\<^sup>2)\<rceil>"
- using `0\<le>M` e `0<d`
+ using \<open>0\<le>M\<close> e \<open>0<d\<close>
by (simp add: Real.real_of_nat_Suc field_simps)
have "4*M/(e*d\<^sup>2) + 1 \<le> real (Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>))"
by (simp add: Real.real_of_nat_Suc)
@@ -137,7 +137,7 @@
also have "... \<le> 2 * M * ((x - k/n)\<^sup>2 / d\<^sup>2)"
apply simp
apply (rule Rings.ordered_semiring_class.mult_left_mono [of 1 "((x - k/n)\<^sup>2 / d\<^sup>2)", simplified])
- using dle `d>0` `M\<ge>0` by auto
+ using dle \<open>d>0\<close> \<open>M\<ge>0\<close> by auto
also have "... \<le> e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2"
using e by simp
finally show ?thesis .
@@ -152,12 +152,12 @@
done
also have "... \<le> e/2 + (2 * M) / (d\<^sup>2 * n)"
apply (simp only: setsum.distrib Rings.semiring_class.distrib_right setsum_right_distrib [symmetric] mult.assoc sum_bern)
- using `d>0` x
+ using \<open>d>0\<close> x
apply (simp add: divide_simps Mge0 mult_le_one mult_left_le)
done
also have "... < e"
apply (simp add: field_simps)
- using `d>0` nbig e `n>0`
+ using \<open>d>0\<close> nbig e \<open>n>0\<close>
apply (simp add: divide_simps algebra_simps)
using ed0 by linarith
finally have "\<bar>f x - (\<Sum>k = 0..n. f (real k / real n) * Bernstein n k x)\<bar> < e" .
@@ -167,7 +167,7 @@
qed
-subsection {*General Stone-Weierstrass theorem*}
+subsection \<open>General Stone-Weierstrass theorem\<close>
text\<open>Source:
Bruno Brosowski and Frank Deutsch.
@@ -282,7 +282,7 @@
show ?thesis
using subU i t
apply (clarsimp simp: p_def divide_simps)
- apply (rule setsum_pos2 [OF `finite subU`])
+ apply (rule setsum_pos2 [OF \<open>finite subU\<close>])
using Uf t pf01 apply auto
apply (force elim!: subsetCE)
done
@@ -345,10 +345,10 @@
using t0 pf by (simp add: q_def power_0_left)
{ fix t and n::nat
assume t: "t \<in> s \<inter> V"
- with `k>0` V have "k * p t < k * \<delta> / 2"
+ with \<open>k>0\<close> V have "k * p t < k * \<delta> / 2"
by force
then have "1 - (k * \<delta> / 2)^n \<le> 1 - (k * p t)^n"
- using `k>0` p01 t by (simp add: power_mono)
+ using \<open>k>0\<close> p01 t by (simp add: power_mono)
also have "... \<le> q n t"
using Bernoulli_inequality [of "- ((p t)^n)" "k^n"]
apply (simp add: q_def)
@@ -357,7 +357,7 @@
} note limitV = this
{ fix t and n::nat
assume t: "t \<in> s - U"
- with `k>0` U have "k * \<delta> \<le> k * p t"
+ with \<open>k>0\<close> U have "k * \<delta> \<le> k * p t"
by (simp add: pt_\<delta>)
with k\<delta> have kpt: "1 < k * p t"
by (blast intro: less_le_trans)
@@ -366,9 +366,9 @@
have ptn_le: "p t ^ n \<le> 1"
by (meson DiffE atLeastAtMost_iff p01 power_le_one t)
have "q n t = (1/(k^n * (p t)^n)) * (1 - p t ^ n) ^ (k^n) * k^n * (p t)^n"
- using pt_pos [OF t] `k>0` by (simp add: q_def)
+ using pt_pos [OF t] \<open>k>0\<close> by (simp add: q_def)
also have "... \<le> (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + k^n * (p t)^n)"
- using pt_pos [OF t] `k>0`
+ using pt_pos [OF t] \<open>k>0\<close>
apply simp
apply (simp only: times_divide_eq_right [symmetric])
apply (rule mult_left_mono [of "1::real", simplified])
@@ -377,20 +377,20 @@
using ptn_le by linarith
also have "... \<le> (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + (p t)^n) ^ (k^n)"
apply (rule mult_left_mono [OF Bernoulli_inequality [of "p t ^ n" "k^n"]])
- using `k>0` ptn_pos ptn_le
+ using \<open>k>0\<close> ptn_pos ptn_le
apply (auto simp: power_mult_distrib)
done
also have "... = (1/(k * (p t))^n) * (1 - p t ^ (2*n)) ^ (k^n)"
- using pt_pos [OF t] `k>0`
+ using pt_pos [OF t] \<open>k>0\<close>
by (simp add: algebra_simps power_mult power2_eq_square power_mult_distrib [symmetric])
also have "... \<le> (1/(k * (p t))^n) * 1"
apply (rule mult_left_mono [OF power_le_one])
apply (metis diff_le_iff(1) less_eq_real_def mult.commute power_le_one power_mult ptn_pos ptn_le)
- using pt_pos [OF t] `k>0`
+ using pt_pos [OF t] \<open>k>0\<close>
apply auto
done
also have "... \<le> (1 / (k*\<delta>))^n"
- using `k>0` \<delta>01 power_mono pt_\<delta> t
+ using \<open>k>0\<close> \<delta>01 power_mono pt_\<delta> t
by (fastforce simp: field_simps)
finally have "q n t \<le> (1 / (real k * \<delta>)) ^ n " .
} note limitNonU = this
@@ -401,13 +401,13 @@
have NN1: "\<And>e. e>0 \<Longrightarrow> (k * \<delta> / 2)^NN e < e"
apply (subst Transcendental.ln_less_cancel_iff [symmetric])
prefer 3 apply (subst ln_realpow)
- using `k>0` `\<delta>>0` NN k\<delta>
+ using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta>
apply (force simp add: field_simps)+
done
have NN0: "\<And>e. e>0 \<Longrightarrow> (1/(k*\<delta>))^NN e < e"
apply (subst Transcendental.ln_less_cancel_iff [symmetric])
prefer 3 apply (subst ln_realpow)
- using `k>0` `\<delta>>0` NN k\<delta>
+ using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta>
apply (force simp add: field_simps ln_div)+
done
{ fix t and e::real
@@ -416,11 +416,11 @@
proof -
assume t: "t \<in> s \<inter> V"
show "1 - q (NN e) t < e"
- by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF `e>0`]])
+ by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF \<open>e>0\<close>]])
next
assume t: "t \<in> s - U"
show "q (NN e) t < e"
- using limitNonU [OF t] less_le_trans [OF NN0 [OF `e>0`]] not_le by blast
+ using limitNonU [OF t] less_le_trans [OF NN0 [OF \<open>e>0\<close>]] not_le by blast
qed
} then have "\<And>e. e > 0 \<Longrightarrow> \<exists>f\<in>R. f ` s \<subseteq> {0..1} \<and> (\<forall>t \<in> s \<inter> V. f t < e) \<and> (\<forall>t \<in> s - U. 1 - e < f t)"
using q01
@@ -445,7 +445,7 @@
using assms by auto
then have "\<exists>V. open V \<and> w \<in> V \<and> s \<inter> V \<subseteq> -B \<and>
(\<forall>e>0. \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> s \<inter> V. f x < e) \<and> (\<forall>x \<in> s \<inter> B. f x > 1 - e))"
- using one [of "-B" w b] assms `w \<in> A` by simp
+ using one [of "-B" w b] assms \<open>w \<in> A\<close> by simp
}
then obtain Vf where Vf:
"\<And>w. w \<in> A \<Longrightarrow> open (Vf w) \<and> w \<in> Vf w \<and> s \<inter> Vf w \<subseteq> -B \<and>
@@ -462,7 +462,7 @@
obtain subA where subA: "subA \<subseteq> A" "finite subA" "A \<subseteq> (\<Union>x \<in> subA. Vf x)"
by (blast intro: that open_Vf compactE_image [OF com_A _ setsum_max_0])
then have [simp]: "subA \<noteq> {}"
- using `a \<in> A` by auto
+ using \<open>a \<in> A\<close> by auto
then have cardp: "card subA > 0" using subA
by (simp add: card_gt_0_iff)
have "\<And>w. w \<in> A \<Longrightarrow> \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> s \<inter> Vf w. f x < e / card subA) \<and> (\<forall>x \<in> s \<inter> B. f x > 1 - e / card subA)"
@@ -623,7 +623,7 @@
then have fj1: "f t \<le> (j - 1/3)*e"
by (simp add: A_def)
then have Anj: "t \<notin> A i" if "i<j" for i
- using Aj `i<j`
+ using Aj \<open>i<j\<close>
apply (simp add: j_def)
using not_less_Least by blast
have j1: "1 \<le> j"
@@ -639,7 +639,7 @@
then obtain d where "i+2+d = j"
using le_Suc_ex that by blast
then have "t \<in> B i"
- using Anj e ge_fx [OF t] `1 \<le> n` fpos [OF t] t
+ using Anj e ge_fx [OF t] \<open>1 \<le> n\<close> fpos [OF t] t
apply (simp add: A_def B_def)
apply (clarsimp simp add: field_simps real_of_nat_diff not_le real_of_nat_Suc)
apply (rule order_trans [of _ "e * 2 + (e * (real d * 3) + e * (real i * 3))"])
@@ -664,9 +664,9 @@
apply simp
done
also have "... \<le> j*e + e*(n - j + 1)*e/n "
- using `1 \<le> n` e by (simp add: field_simps)
+ using \<open>1 \<le> n\<close> e by (simp add: field_simps)
also have "... \<le> j*e + e*e"
- using `1 \<le> n` e j1 by (simp add: field_simps)
+ using \<open>1 \<le> n\<close> e j1 by (simp add: field_simps)
also have "... < (j + 1/3)*e"
using e by (auto simp: field_simps)
finally have gj1: "g t < (j + 1 / 3) * e" .
@@ -737,7 +737,7 @@
assume n: "N \<le> n" "\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + real n)"
assume x: "x \<in> s"
have "\<not> real (Suc n) < inverse e"
- using `N \<le> n` N using less_imp_inverse_less by force
+ using \<open>N \<le> n\<close> N using less_imp_inverse_less by force
then have "1 / (1 + real n) \<le> e"
using e by (simp add: field_simps real_of_nat_Suc)
then have "\<bar>f x - g x\<bar> < e"
@@ -756,7 +756,7 @@
done
qed
-text{*A HOL Light formulation*}
+text\<open>A HOL Light formulation\<close>
corollary Stone_Weierstrass_HOL:
fixes R :: "('a::t2_space \<Rightarrow> real) set" and s :: "'a set"
assumes "compact s" "\<And>c. P(\<lambda>x. c::real)"
@@ -772,12 +772,12 @@
using assms
by auto
show ?thesis
- using PR.Stone_Weierstrass_basic [OF `continuous_on s f` `0 < e`]
+ using PR.Stone_Weierstrass_basic [OF \<open>continuous_on s f\<close> \<open>0 < e\<close>]
by blast
qed
-subsection {*Polynomial functions*}
+subsection \<open>Polynomial functions\<close>
inductive real_polynomial_function :: "('a::real_normed_vector \<Rightarrow> real) \<Rightarrow> bool" where
linear: "bounded_linear f \<Longrightarrow> real_polynomial_function f"
@@ -978,7 +978,7 @@
by (simp add: euclidean_representation_setsum_fun)
qed
-subsection {*Stone-Weierstrass theorem for polynomial functions*}
+subsection \<open>Stone-Weierstrass theorem for polynomial functions\<close>
text\<open>First, we need to show that they are continous, differentiable and separable.\<close>
@@ -1048,12 +1048,12 @@
assume "b \<in> Basis"
then
obtain p' where p': "real_polynomial_function p'" and pd: "\<And>x. ((\<lambda>x. p x \<bullet> b) has_real_derivative p' x) (at x)"
- using assms [unfolded polynomial_function_iff_Basis_inner, rule_format] `b \<in> Basis`
+ using assms [unfolded polynomial_function_iff_Basis_inner, rule_format] \<open>b \<in> Basis\<close>
has_real_derivative_polynomial_function
by blast
have "\<exists>q. polynomial_function q \<and> (\<forall>x. ((\<lambda>u. (p u \<bullet> b) *\<^sub>R b) has_vector_derivative q x) (at x))"
apply (rule_tac x="\<lambda>x. p' x *\<^sub>R b" in exI)
- using `b \<in> Basis` p'
+ using \<open>b \<in> Basis\<close> p'
apply (simp add: polynomial_function_iff_Basis_inner inner_Basis)
apply (auto intro: derivative_eq_intros pd)
done
@@ -1096,7 +1096,7 @@
apply (auto intro: real_polynomial_function_separable)
done
show ?thesis
- using PR.Stone_Weierstrass_basic [OF `continuous_on s f` `0 < e`]
+ using PR.Stone_Weierstrass_basic [OF \<open>continuous_on s f\<close> \<open>0 < e\<close>]
by blast
qed
@@ -1131,7 +1131,7 @@
by (rule norm_setsum)
also have "... < of_nat DIM('b) * (e / DIM('b))"
apply (rule setsum_bounded_above_strict)
- apply (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf `x \<in> s`)
+ apply (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf \<open>x \<in> s\<close>)
apply (rule DIM_positive)
done
also have "... = e"
@@ -1149,8 +1149,8 @@
subsection\<open>Polynomial functions as paths\<close>
-text{*One application is to pick a smooth approximation to a path,
-or just pick a smooth path anyway in an open connected set*}
+text\<open>One application is to pick a smooth approximation to a path,
+or just pick a smooth path anyway in an open connected set\<close>
lemma path_polynomial_function:
fixes g :: "real \<Rightarrow> 'b::euclidean_space"
@@ -1192,7 +1192,7 @@
proof -
have "path_connected s" using assms
by (simp add: connected_open_path_connected)
- with `x \<in> s` `y \<in> s` obtain p where p: "path p" "path_image p \<subseteq> s" "pathstart p = x" "pathfinish p = y"
+ with \<open>x \<in> s\<close> \<open>y \<in> s\<close> obtain p where p: "path p" "path_image p \<subseteq> s" "pathstart p = x" "pathfinish p = y"
by (force simp: path_connected_def)
have "\<exists>e. 0 < e \<and> (\<forall>x \<in> path_image p. ball x e \<subseteq> s)"
proof (cases "s = UNIV")
@@ -1211,7 +1211,7 @@
then obtain e where "0 < e"and eb: "\<And>x. x \<in> path_image p \<Longrightarrow> ball x e \<subseteq> s"
by auto
show ?thesis
- using path_approx_polynomial_function [OF `path p` `0 < e`]
+ using path_approx_polynomial_function [OF \<open>path p\<close> \<open>0 < e\<close>]
apply clarify
apply (intro exI conjI, assumption)
using p