isabelle update_cartouches;
authorwenzelm
Mon Sep 21 21:46:14 2015 +0200 (2015-09-21)
changeset 6122205d28dc76e5c
parent 61221 bf194f7c4c8e
child 61223 dfccf6c06201
isabelle update_cartouches;
src/HOL/HOL.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Uniform_Limit.thy
src/HOL/Multivariate_Analysis/Weierstrass.thy
     1.1 --- a/src/HOL/HOL.thy	Mon Sep 21 21:43:09 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Sep 21 21:46:14 2015 +0200
     1.3 @@ -1691,8 +1691,8 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 -text{* Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
     1.8 -not to simplify the argument and to solve it by an assumption. *}
     1.9 +text\<open>Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
    1.10 +not to simplify the argument and to solve it by an assumption.\<close>
    1.11  
    1.12  definition ASSUMPTION :: "bool \<Rightarrow> bool" where
    1.13  "ASSUMPTION A \<equiv> A"
    1.14 @@ -1706,7 +1706,7 @@
    1.15  lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
    1.16  by(simp add: ASSUMPTION_def)
    1.17  
    1.18 -setup {*
    1.19 +setup \<open>
    1.20  let
    1.21    val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
    1.22      resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
    1.23 @@ -1714,7 +1714,7 @@
    1.24  in
    1.25    map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
    1.26  end
    1.27 -*}
    1.28 +\<close>
    1.29  
    1.30  
    1.31  subsection \<open>Code generator setup\<close>
     2.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Sep 21 21:43:09 2015 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Sep 21 21:46:14 2015 +0200
     2.3 @@ -81,7 +81,7 @@
     2.4      using assms
     2.5      by (auto simp: piecewise_differentiable_on_def)
     2.6    have finabc: "finite ({a,b,c} \<union> (s \<union> t))"
     2.7 -    by (metis `finite s` `finite t` finite_Un finite_insert finite.emptyI)
     2.8 +    by (metis \<open>finite s\<close> \<open>finite t\<close> finite_Un finite_insert finite.emptyI)
     2.9    have "continuous_on {a..c} f" "continuous_on {c..b} g"
    2.10      using assms piecewise_differentiable_on_def by auto
    2.11    then have "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)"
    2.12 @@ -462,7 +462,7 @@
    2.13      by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
    2.14    have "continuous_on {0..1} g1"
    2.15      using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
    2.16 -  with `finite s` show ?thesis
    2.17 +  with \<open>finite s\<close> show ?thesis
    2.18      apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
    2.19      apply (rule_tac x="insert 1 ((op*2)`s)" in exI)
    2.20      apply (simp add: g1D con_g1)
    2.21 @@ -509,7 +509,7 @@
    2.22      by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
    2.23    have "continuous_on {0..1} g2"
    2.24      using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast
    2.25 -  with `finite s` show ?thesis
    2.26 +  with \<open>finite s\<close> show ?thesis
    2.27      apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
    2.28      apply (rule_tac x="insert 0 ((\<lambda>x. 2 * x - 1) ` s)" in exI)
    2.29      apply (simp add: g2D con_g2)
    2.30 @@ -2253,11 +2253,11 @@
    2.31          def shrink \<equiv> "\<lambda>x. x - e *\<^sub>R (x - d)"
    2.32          let ?pathint = "\<lambda>x y. path_integral(linepath x y) f"
    2.33          have e: "0 < e" "e \<le> 1" "e \<le> d1 / (4 * C)" "e \<le> cmod y / 24 / C / B"
    2.34 -          using d1_pos `C>0` `B>0` ynz by (simp_all add: e_def)
    2.35 +          using d1_pos \<open>C>0\<close> \<open>B>0\<close> ynz by (simp_all add: e_def)
    2.36          then have eCB: "24 * e * C * B \<le> cmod y"
    2.37 -          using `C>0` `B>0`  by (simp add: field_simps)
    2.38 +          using \<open>C>0\<close> \<open>B>0\<close>  by (simp add: field_simps)
    2.39          have e_le_d1: "e * (4 * C) \<le> d1"
    2.40 -          using e `C>0` by (simp add: field_simps)
    2.41 +          using e \<open>C>0\<close> by (simp add: field_simps)
    2.42          have "shrink a \<in> interior(convex hull {a,b,c})"
    2.43               "shrink b \<in> interior(convex hull {a,b,c})"
    2.44               "shrink c \<in> interior(convex hull {a,b,c})"
    2.45 @@ -2276,10 +2276,10 @@
    2.46          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)"
    2.47            by (simp add: algebra_simps)
    2.48          have "cmod y / (24 * C) \<le> cmod y / cmod (b - a) / 12"
    2.49 -          using False `C>0` diff_2C [of b a] ynz
    2.50 +          using False \<open>C>0\<close> diff_2C [of b a] ynz
    2.51            by (auto simp: divide_simps hull_inc)
    2.52          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
    2.53 -          apply (cases "x=0", simp add: `0<C`)
    2.54 +          apply (cases "x=0", simp add: \<open>0<C\<close>)
    2.55            using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast
    2.56          { fix u v
    2.57            assume uv: "u \<in> convex hull {a, b, c}" "v \<in> convex hull {a, b, c}" "u\<noteq>v"
    2.58 @@ -2292,7 +2292,7 @@
    2.59              using shr_uv by (blast intro: Bnf linepath_in_convex_hull interior_subset [THEN subsetD])
    2.60            have By_uv: "B * (12 * (e * cmod (u - v))) \<le> cmod y"
    2.61              apply (rule order_trans [OF _ eCB])
    2.62 -            using e `B>0` diff_2C [of u v] uv
    2.63 +            using e \<open>B>0\<close> diff_2C [of u v] uv
    2.64              by (auto simp: field_simps)
    2.65            { fix x::real   assume x: "0\<le>x" "x\<le>1"
    2.66              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)"
    2.67 @@ -2303,7 +2303,7 @@
    2.68              have ll: "linepath (shrink u) (shrink v) x - linepath u v x = -e * ((1 - x) *\<^sub>R (u - d) + x *\<^sub>R (v - d))"
    2.69                by (simp add: linepath_def shrink_def algebra_simps scaleR_conv_of_real)
    2.70              have cmod_less_dt: "cmod (linepath (shrink u) (shrink v) x - linepath u v x) < d1"
    2.71 -              using `e>0`
    2.72 +              using \<open>e>0\<close>
    2.73                apply (simp add: ll norm_mult scaleR_diff_right)
    2.74                apply (rule less_le_trans [OF _ e_le_d1])
    2.75                using cmod_less_4C
    2.76 @@ -2313,7 +2313,7 @@
    2.77                using x uv shr_uv cmod_less_dt
    2.78                by (auto simp: hull_inc intro: d1 interior_subset [THEN subsetD] linepath_in_convex_hull)
    2.79              also have "... \<le> cmod y / cmod (v - u) / 12"
    2.80 -              using False uv `C>0` diff_2C [of v u] ynz
    2.81 +              using False uv \<open>C>0\<close> diff_2C [of v u] ynz
    2.82                by (auto simp: divide_simps hull_inc)
    2.83              finally have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) \<le> cmod y / cmod (v - u) / 12"
    2.84                by simp
    2.85 @@ -2324,7 +2324,7 @@
    2.86                    \<le> cmod y / 6"
    2.87                apply (rule order_trans [of _ "B*((norm y / 24 / C / B)*2*C) + (2*C)*(norm y /24 / C)"])
    2.88                apply (rule add_mono [OF mult_mono])
    2.89 -              using By_uv e `0 < B` `0 < C` x ynz
    2.90 +              using By_uv e \<open>0 < B\<close> \<open>0 < C\<close> x ynz
    2.91                apply (simp_all add: cmod_fuv cmod_shr cmod_12_le hull_inc)
    2.92                apply (simp add: field_simps)
    2.93                done
    2.94 @@ -2339,7 +2339,7 @@
    2.95                      [of "B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)"
    2.96                          "\<lambda>x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)"
    2.97                          _ 0 1 ])
    2.98 -            using ynz `0 < B` `0 < C`
    2.99 +            using ynz \<open>0 < B\<close> \<open>0 < C\<close>
   2.100              apply (simp_all del: le_divide_eq_numeral1)
   2.101              apply (simp add: has_integral_sub has_path_integral_linepath [symmetric] has_path_integral_integral
   2.102                               fpi_uv f_uv path_integrable_continuous_linepath, clarify)
   2.103 @@ -2376,7 +2376,7 @@
   2.104            by (simp add: contf compact_convex_hull compact_uniformly_continuous)
   2.105          ultimately have "False"
   2.106            unfolding uniformly_continuous_on_def
   2.107 -          by (force simp: ynz `0 < C` dist_norm)
   2.108 +          by (force simp: ynz \<open>0 < C\<close> dist_norm)
   2.109          then show ?thesis ..
   2.110        qed
   2.111    }
   2.112 @@ -2411,7 +2411,7 @@
   2.113        case False
   2.114        show "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
   2.115          apply (rule less.hyps [of "s'"])
   2.116 -        using False d `finite s` interior_subset
   2.117 +        using False d \<open>finite s\<close> interior_subset
   2.118          apply (auto intro!: less.prems)
   2.119          done
   2.120      next
   2.121 @@ -2420,7 +2420,7 @@
   2.122          by (meson True hull_subset insert_subset convex_hull_subset)
   2.123        have abd: "(f has_path_integral 0) (linepath a b +++ linepath b d +++ linepath d a)"
   2.124          apply (rule less.hyps [of "s'"])
   2.125 -        using True d  `finite s` not_in_interior_convex_hull_3
   2.126 +        using True d  \<open>finite s\<close> not_in_interior_convex_hull_3
   2.127          apply (auto intro!: less.prems continuous_on_subset [OF  _ *])
   2.128          apply (metis * insert_absorb insert_subset interior_mono)
   2.129          done
   2.130 @@ -2428,7 +2428,7 @@
   2.131          by (meson True hull_subset insert_subset convex_hull_subset)
   2.132        have bcd: "(f has_path_integral 0) (linepath b c +++ linepath c d +++ linepath d b)"
   2.133          apply (rule less.hyps [of "s'"])
   2.134 -        using True d  `finite s` not_in_interior_convex_hull_3
   2.135 +        using True d  \<open>finite s\<close> not_in_interior_convex_hull_3
   2.136          apply (auto intro!: less.prems continuous_on_subset [OF _ *])
   2.137          apply (metis * insert_absorb insert_subset interior_mono)
   2.138          done
   2.139 @@ -2436,7 +2436,7 @@
   2.140          by (meson True hull_subset insert_subset convex_hull_subset)
   2.141        have cad: "(f has_path_integral 0) (linepath c a +++ linepath a d +++ linepath d c)"
   2.142          apply (rule less.hyps [of "s'"])
   2.143 -        using True d  `finite s` not_in_interior_convex_hull_3
   2.144 +        using True d  \<open>finite s\<close> not_in_interior_convex_hull_3
   2.145          apply (auto intro!: less.prems continuous_on_subset [OF _ *])
   2.146          apply (metis * insert_absorb insert_subset interior_mono)
   2.147          done
   2.148 @@ -2518,7 +2518,7 @@
   2.149      then obtain d1 where d1: "d1>0" and d1_less: "\<And>y. cmod (y - x) < d1 \<Longrightarrow> cmod (f y - f x) < e/2"
   2.150        unfolding continuous_at Lim_at dist_norm  using e
   2.151        by (drule_tac x="e/2" in spec) force
   2.152 -    obtain d2 where d2: "d2>0" "ball x d2 \<subseteq> s" using  `open s` x
   2.153 +    obtain d2 where d2: "d2>0" "ball x d2 \<subseteq> s" using  \<open>open s\<close> x
   2.154        by (auto simp: open_contains_ball)
   2.155      have dpos: "min d1 d2 > 0" using d1 d2 by simp
   2.156      { fix y
   2.157 @@ -2556,7 +2556,7 @@
   2.158      apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right)
   2.159      apply (rule Lim_transform [OF * Lim_eventually])
   2.160      apply (simp add: inverse_eq_divide [symmetric] eventually_at)
   2.161 -    using `open s` x
   2.162 +    using \<open>open s\<close> x
   2.163      apply (force simp: dist_norm open_contains_ball)
   2.164      done
   2.165  qed
   2.166 @@ -2802,7 +2802,7 @@
   2.167  proof -
   2.168    { fix z
   2.169      assume z: "z \<in> s"
   2.170 -    obtain d where d: "d>0" "ball z d \<subseteq> s" using  `open s` z
   2.171 +    obtain d where d: "d>0" "ball z d \<subseteq> s" using  \<open>open s\<close> z
   2.172        by (auto simp: open_contains_ball)
   2.173      then have contfb: "continuous_on (ball z d) f"
   2.174        using contf continuous_on_subset by blast
   2.175 @@ -2839,16 +2839,16 @@
   2.176  apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros)
   2.177  done
   2.178  
   2.179 -text{*Key fact that path integral is the same for a "nearby" path. This is the
   2.180 +text\<open>Key fact that path integral is the same for a "nearby" path. This is the
   2.181   main lemma for the homotopy form of Cauchy's theorem and is also useful
   2.182   if we want "without loss of generality" to assume some nice properties of a
   2.183   path (e.g. smoothness). It can also be used to define the integrals of
   2.184   analytic functions over arbitrary continuous paths. This is just done for
   2.185   winding numbers now.
   2.186 -*}
   2.187 +\<close>
   2.188  
   2.189 -text{*This formulation covers two cases: @{term g} and @{term h} share their
   2.190 -      start and end points; @{term g} and @{term h} both loop upon themselves. *}
   2.191 +text\<open>This formulation covers two cases: @{term g} and @{term h} share their
   2.192 +      start and end points; @{term g} and @{term h} both loop upon themselves.\<close>
   2.193  lemma path_integral_nearby:
   2.194    assumes os: "open s"
   2.195        and p: "path p" "path_image p \<subseteq> s"
   2.196 @@ -2876,7 +2876,7 @@
   2.197      by blast
   2.198    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"
   2.199      apply (simp add: cover_def path_image_def image_comp)
   2.200 -    apply (blast dest!: finite_subset_image [OF `finite D`])
   2.201 +    apply (blast dest!: finite_subset_image [OF \<open>finite D\<close>])
   2.202      done
   2.203    then have kne: "k \<noteq> {}"
   2.204      using D by auto
   2.205 @@ -2905,7 +2905,7 @@
   2.206      { fix t::real
   2.207        assume t: "0 \<le> t" "t \<le> 1"
   2.208        then obtain u where u: "u \<in> k" and ptu: "p t \<in> ball(p u) (ee(p u) / 3)"
   2.209 -        using `path_image p \<subseteq> \<Union>D` D_eq by (force simp: path_image_def)
   2.210 +        using \<open>path_image p \<subseteq> \<Union>D\<close> D_eq by (force simp: path_image_def)
   2.211        then have ele: "e \<le> ee (p u)" using fin_eep
   2.212          by (simp add: e_def)
   2.213        have "cmod (g t - p t) < e / 3" "cmod (h t - p t) < e / 3"
   2.214 @@ -2950,7 +2950,7 @@
   2.215          next
   2.216            case (Suc n)
   2.217            obtain t where t: "t \<in> k" and "p (n/N) \<in> ball(p t) (ee(p t) / 3)"
   2.218 -            using `path_image p \<subseteq> \<Union>D` [THEN subsetD, where c="p (n/N)"] D_eq N Suc.prems
   2.219 +            using \<open>path_image p \<subseteq> \<Union>D\<close> [THEN subsetD, where c="p (n/N)"] D_eq N Suc.prems
   2.220              by (force simp: path_image_def)
   2.221            then have ptu: "cmod (p t - p (n/N)) < ee (p t) / 3"
   2.222              by (simp add: dist_norm)
   2.223 @@ -2988,7 +2988,7 @@
   2.224              using ptgh_ee [of "n/N"] Suc.prems
   2.225              by (auto simp: field_simps real_of_nat_def dist_norm dest: segment_furthest_le [where y="p t"])
   2.226            then have gh_ns: "closed_segment (g (n/N)) (h (n/N)) \<subseteq> s"
   2.227 -            using `N>0` Suc.prems
   2.228 +            using \<open>N>0\<close> Suc.prems
   2.229              apply (simp add: real_of_nat_def path_image_join field_simps closed_segment_commute)
   2.230              apply (erule order_trans)
   2.231              apply (simp add: ee pi t)
   2.232 @@ -2998,14 +2998,14 @@
   2.233              using ptgh_ee [of "(1+n)/N"] Suc.prems
   2.234              by (auto simp: field_simps real_of_nat_def dist_norm dest: segment_furthest_le [where y="p t"])
   2.235            then have gh_n's: "closed_segment (g ((1 + n) / N)) (h ((1 + n) / N)) \<subseteq> s"
   2.236 -            using `N>0` Suc.prems ee pi t
   2.237 +            using \<open>N>0\<close> Suc.prems ee pi t
   2.238              by (auto simp: Path_Connected.path_image_join field_simps)
   2.239            have pi_subset_ball:
   2.240                  "path_image (subpath (n/N) ((1+n) / N) g +++ linepath (g ((1+n) / N)) (h ((1+n) / N)) +++
   2.241                               subpath ((1+n) / N) (n/N) h +++ linepath (h (n/N)) (g (n/N)))
   2.242                   \<subseteq> ball (p t) (ee (p t))"
   2.243              apply (intro subset_path_image_join pi_hgn pi_ghn')
   2.244 -            using `N>0` Suc.prems
   2.245 +            using \<open>N>0\<close> Suc.prems
   2.246              apply (auto simp: dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
   2.247              done
   2.248            have pi0: "(f has_path_integral 0)
   2.249 @@ -3126,7 +3126,7 @@
   2.250    where d: "0 < d"
   2.251      and p: "polynomial_function p" "path_image p \<subseteq> s"
   2.252      and pi: "\<And>f. f holomorphic_on s \<Longrightarrow> path_integral g f = path_integral p f"
   2.253 -  using path_integral_nearby_ends [OF s `path g` pag]
   2.254 +  using path_integral_nearby_ends [OF s \<open>path g\<close> pag]
   2.255    apply clarify
   2.256    apply (drule_tac x=g in spec)
   2.257    apply (simp only: assms)
     3.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Sep 21 21:43:09 2015 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Sep 21 21:46:14 2015 +0200
     3.3 @@ -9467,7 +9467,7 @@
     3.4      using g by (simp add: Fun.image_comp)
     3.5    then show "coplanar s"
     3.6      unfolding coplanar_def
     3.7 -    using affine_hull_linear_image [of g "{u,v,w}" for u v w]  `linear g` linear_conv_bounded_linear
     3.8 +    using affine_hull_linear_image [of g "{u,v,w}" for u v w]  \<open>linear g\<close> linear_conv_bounded_linear
     3.9      by fastforce
    3.10  qed
    3.11  (*The HOL Light proof is simply
    3.12 @@ -9651,7 +9651,7 @@
    3.13      then have *: "\<And>x. x \<in> closure s \<Longrightarrow> setdist s t \<le> dist x y"
    3.14        apply (rule continuous_ge_on_closure)
    3.15        apply assumption
    3.16 -      apply (blast intro: setdist_le_dist `y \<in> t` )
    3.17 +      apply (blast intro: setdist_le_dist \<open>y \<in> t\<close> )
    3.18        done
    3.19    } note * = this
    3.20    show ?thesis
    3.21 @@ -9687,7 +9687,7 @@
    3.22    assumes s: "closed s" and t: "compact t"
    3.23        and "s \<noteq> {}" "t \<noteq> {}"
    3.24      shows "\<exists>x \<in> s. \<exists>y \<in> t. dist x y = setdist s t"
    3.25 -  using setdist_compact_closed [OF t s `t \<noteq> {}` `s \<noteq> {}`]
    3.26 +  using setdist_compact_closed [OF t s \<open>t \<noteq> {}\<close> \<open>s \<noteq> {}\<close>]
    3.27    by (metis dist_commute setdist_sym)
    3.28  
    3.29  lemma setdist_eq_0I: "\<lbrakk>x \<in> s; x \<in> t\<rbrakk> \<Longrightarrow> setdist s t = 0"
     4.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Sep 21 21:43:09 2015 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Sep 21 21:46:14 2015 +0200
     4.3 @@ -2889,7 +2889,7 @@
     4.4          apply (rule less_trans[OF _ *])
     4.5          apply (subst N1', rule d(2)[of "p (N1+N2)"])
     4.6          using N1' as(1) as(2) dp
     4.7 -        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`)
     4.8 +        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>)
     4.9          using N2 le_add2 by blast
    4.10      }
    4.11      ultimately show "\<exists>d. gauge d \<and>
    4.12 @@ -3602,11 +3602,11 @@
    4.13    proof (cases "f x = neutral opp")
    4.14      case True
    4.15      then show ?thesis
    4.16 -      using assms `x \<notin> s`
    4.17 +      using assms \<open>x \<notin> s\<close>
    4.18        by (auto simp: iterate_def support_clauses)
    4.19    next
    4.20      case False
    4.21 -    with `x \<notin> s` \<open>finite s\<close> support_subset show ?thesis
    4.22 +    with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis
    4.23        apply (simp add: iterate_def fold'_def support_clauses)
    4.24        apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
    4.25        apply (force simp add: )+
    4.26 @@ -3962,7 +3962,7 @@
    4.27        case True
    4.28        show "iterate opp d f = f (cbox a b)"
    4.29          unfolding operativeD(1)[OF assms(2) True]
    4.30 -      proof (rule iterate_eq_neutral[OF `monoidal opp`])
    4.31 +      proof (rule iterate_eq_neutral[OF \<open>monoidal opp\<close>])
    4.32          fix x
    4.33          assume x: "x \<in> d"
    4.34          then show "f x = neutral opp"
    4.35 @@ -3990,9 +3990,9 @@
    4.36            note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
    4.37            moreover
    4.38            have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
    4.39 -            using division_ofD(2,2,3)[OF `d division_of cbox a b` as]
    4.40 +            using division_ofD(2,2,3)[OF \<open>d division_of cbox a b\<close> as]
    4.41              apply (metis j subset_box(1) uv(1))
    4.42 -            by (metis `cbox u v \<subseteq> cbox a b` j subset_box(1) uv(1))
    4.43 +            by (metis \<open>cbox u v \<subseteq> cbox a b\<close> j subset_box(1) uv(1))
    4.44            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"
    4.45              unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
    4.46          then have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
    4.47 @@ -4001,7 +4001,7 @@
    4.48            by blast
    4.49          have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
    4.50            unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps)
    4.51 -        note this[unfolded division_ofD(6)[OF `d division_of cbox a b`,symmetric] Union_iff]
    4.52 +        note this[unfolded division_ofD(6)[OF \<open>d division_of cbox a b\<close>,symmetric] Union_iff]
    4.53          then guess i .. note i=this
    4.54          guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this
    4.55          have "cbox a b \<in> d"
    4.56 @@ -4059,18 +4059,18 @@
    4.57          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> {}}"
    4.58          def cb \<equiv> "(\<Sum>i\<in>Basis. (if i = k then c else b\<bullet>i) *\<^sub>R i)::'a"
    4.59          def ca \<equiv> "(\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)::'a"
    4.60 -        note division_points_psubset[OF `d division_of cbox a b` ab kc(1-2) j]
    4.61 +        note division_points_psubset[OF \<open>d division_of cbox a b\<close> ab kc(1-2) j]
    4.62          note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)]
    4.63          then have *: "(iterate opp d1 f) = f (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
    4.64            "(iterate opp d2 f) = f (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
    4.65            unfolding interval_split[OF kc(4)]
    4.66            apply (rule_tac[!] "1.hyps"[rule_format])
    4.67 -          using division_split[OF `d division_of cbox a b`, where k=k and c=c]
    4.68 -          apply (simp_all add: interval_split 1 kc d1_def d2_def division_points_finite[OF `d division_of cbox a b`])
    4.69 +          using division_split[OF \<open>d division_of cbox a b\<close>, where k=k and c=c]
    4.70 +          apply (simp_all add: interval_split 1 kc d1_def d2_def division_points_finite[OF \<open>d division_of cbox a b\<close>])
    4.71            done
    4.72          { fix l y
    4.73            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"
    4.74 -          from division_ofD(4)[OF `d division_of cbox a b` this(1)] guess u v by (elim exE) note leq=this
    4.75 +          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
    4.76            have "f (l \<inter> {x. x \<bullet> k \<le> c}) = neutral opp"
    4.77              unfolding leq interval_split[OF kc(4)]
    4.78              apply (rule operativeD(1) 1)+
    4.79 @@ -4079,7 +4079,7 @@
    4.80          } note fxk_le = this
    4.81          { fix l y
    4.82            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"
    4.83 -          from division_ofD(4)[OF `d division_of cbox a b` this(1)] guess u v by (elim exE) note leq=this
    4.84 +          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
    4.85            have "f (l \<inter> {x. x \<bullet> k \<ge> c}) = neutral opp"
    4.86              unfolding leq interval_split[OF kc(4)]
    4.87              apply (rule operativeD(1) 1)+
    4.88 @@ -4102,7 +4102,7 @@
    4.89            apply (force simp add: empty_as_interval[symmetric] fxk_ge)+
    4.90            done
    4.91          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}))"
    4.92 -          unfolding forall_in_division[OF `d division_of cbox a b`]
    4.93 +          unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
    4.94            using assms(2) kc(4) by blast
    4.95          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}))) =
    4.96            iterate opp d f"
    4.97 @@ -4689,7 +4689,7 @@
    4.98  proof (cases "content (cbox a b) = 0")
    4.99    case True
   4.100    then have ce: "content (cbox a b) < e"
   4.101 -    by (metis `0 < e`)
   4.102 +    by (metis \<open>0 < e\<close>)
   4.103    show ?thesis
   4.104      apply (rule that[of 1])
   4.105      apply simp
   4.106 @@ -6112,10 +6112,10 @@
   4.107    have one: "(- 1) ^ p' * (- 1) ^ p' = (1::real)"
   4.108      and "{..<p} \<inter> {i. p = Suc i} = {p - 1}"
   4.109      for p'
   4.110 -    using `p > 0`
   4.111 +    using \<open>p > 0\<close>
   4.112      by (auto simp: power_mult_distrib[symmetric])
   4.113    then have "?sum b = f b"
   4.114 -    using Suc_pred'[OF `p > 0`]
   4.115 +    using Suc_pred'[OF \<open>p > 0\<close>]
   4.116      by (simp add: diff_eq_eq Dg_def power_0_left le_Suc_eq if_distrib
   4.117          cond_application_beta setsum.If_cases f0)
   4.118    also
   4.119 @@ -6428,7 +6428,7 @@
   4.120    { fix e::real 
   4.121      assume "e > 0"
   4.122      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"
   4.123 -      using `e>0` fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
   4.124 +      using \<open>e>0\<close> fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
   4.125      have "norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
   4.126             if y: "y \<in> {a..b}" and yx: "\<bar>y - x\<bar> < d" for y  
   4.127      proof (cases "y < x")
   4.128 @@ -6447,7 +6447,7 @@
   4.129          using False
   4.130          apply (simp add: abs_eq_content del: content_real_if)
   4.131          apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
   4.132 -        using yx False d x y `e>0` apply (auto simp add: Idiff fux_int)
   4.133 +        using yx False d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
   4.134          done
   4.135      next
   4.136        case True
   4.137 @@ -6465,13 +6465,13 @@
   4.138          using True
   4.139          apply (simp add: abs_eq_content del: content_real_if)
   4.140          apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
   4.141 -        using yx True d x y `e>0` apply (auto simp add: Idiff fux_int)
   4.142 +        using yx True d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
   4.143          done
   4.144        then show ?thesis
   4.145          by (simp add: algebra_simps norm_minus_commute)
   4.146      qed
   4.147      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>"
   4.148 -      using `d>0` by blast 
   4.149 +      using \<open>d>0\<close> by blast 
   4.150    } 
   4.151    then show ?thesis
   4.152      by (simp add: has_vector_derivative_def has_derivative_within_alt bounded_linear_scaleR_left)
   4.153 @@ -11913,7 +11913,7 @@
   4.154      by simp
   4.155  qed
   4.156  
   4.157 -subsection{*Compute a double integral using iterated integrals and switching the order of integration*}
   4.158 +subsection\<open>Compute a double integral using iterated integrals and switching the order of integration\<close>
   4.159  
   4.160  lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
   4.161    by auto
   4.162 @@ -12197,7 +12197,7 @@
   4.163        using compact_uniformly_continuous [OF assms compact_cbox]
   4.164        apply (simp add: uniformly_continuous_on_def dist_norm)
   4.165        apply (drule_tac x="e / 2 / content?CBOX" in spec)
   4.166 -      using cbp `0 < e`
   4.167 +      using cbp \<open>0 < e\<close>
   4.168        apply (auto simp: zero_less_mult_iff)
   4.169        apply (rename_tac k)
   4.170        apply (rule_tac e1=k in fine_division_exists [OF gauge_ball, where a = "(a,c)" and b = "(b,d)"])
     5.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Sep 21 21:43:09 2015 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Sep 21 21:46:14 2015 +0200
     5.3 @@ -462,7 +462,7 @@
     5.4    apply auto
     5.5    done
     5.6  
     5.7 -lemma approachable_lt_le2:  --{*like the above, but pushes aside an extra formula*}
     5.8 +lemma approachable_lt_le2:  --\<open>like the above, but pushes aside an extra formula\<close>
     5.9      "(\<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)"
    5.10    apply auto
    5.11    apply (rule_tac x="d/2" in exI, auto)
    5.12 @@ -562,7 +562,7 @@
    5.13    using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
    5.14    by (auto simp add: field_simps cong: conj_cong)
    5.15  
    5.16 -text{*Bernoulli's inequality*}
    5.17 +text\<open>Bernoulli's inequality\<close>
    5.18  lemma Bernoulli_inequality:
    5.19    fixes x :: real
    5.20    assumes "-1 \<le> x"
     6.1 --- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Sep 21 21:43:09 2015 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Sep 21 21:46:14 2015 +0200
     6.3 @@ -58,15 +58,15 @@
     6.4    def e' \<equiv> "e/3"
     6.5    assume "0 < e"
     6.6    then have "0 < e'" by (simp add: e'_def)
     6.7 -  from uniform_limitD[OF uc `0 < e'`]
     6.8 +  from uniform_limitD[OF uc \<open>0 < e'\<close>]
     6.9    have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (h x) (f n x) < e'"
    6.10      by (simp add: dist_commute)
    6.11    moreover
    6.12    from f
    6.13    have "\<forall>\<^sub>F n in F. \<forall>\<^sub>F x in at x within S. dist (g n) (f n x) < e'"
    6.14 -    by eventually_elim (auto dest!: tendstoD[OF _ `0 < e'`] simp: dist_commute)
    6.15 +    by eventually_elim (auto dest!: tendstoD[OF _ \<open>0 < e'\<close>] simp: dist_commute)
    6.16    moreover
    6.17 -  from tendstoD[OF g `0 < e'`] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
    6.18 +  from tendstoD[OF g \<open>0 < e'\<close>] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
    6.19      by (simp add: dist_commute)
    6.20    ultimately
    6.21    have "\<forall>\<^sub>F _ in F. \<forall>\<^sub>F x in at x within S. dist (h x) l < e"
    6.22 @@ -80,7 +80,7 @@
    6.23      show ?case
    6.24      proof eventually_elim
    6.25        case (elim x)
    6.26 -      from fh[rule_format, OF `x \<in> S`] elim(1)
    6.27 +      from fh[rule_format, OF \<open>x \<in> S\<close>] elim(1)
    6.28        have "dist (h x) (g n) < e' + e'"
    6.29          by (rule dist_triangle_lt[OF add_strict_mono])
    6.30        from dist_triangle_lt[OF add_strict_mono, OF this gl]
    6.31 @@ -88,7 +88,7 @@
    6.32      qed
    6.33    qed
    6.34    thus "\<forall>\<^sub>F x in at x within S. dist (h x) l < e"
    6.35 -    using eventually_happens by (metis `\<not>trivial_limit F`)
    6.36 +    using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
    6.37  qed
    6.38  
    6.39  lemma
    6.40 @@ -122,7 +122,7 @@
    6.41  proof (rule uniform_limitI)
    6.42    fix e :: real
    6.43    assume "0 < e"
    6.44 -  from suminf_exist_split[OF `0 < e` `summable M`]
    6.45 +  from suminf_exist_split[OF \<open>0 < e\<close> \<open>summable M\<close>]
    6.46    have "\<forall>\<^sub>F k in sequentially. norm (\<Sum>i. M (i + k)) < e"
    6.47      by (auto simp: eventually_sequentially)
    6.48    thus "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
    6.49 @@ -132,16 +132,16 @@
    6.50      proof safe
    6.51        fix x assume "x \<in> A"
    6.52        have "\<exists>N. \<forall>n\<ge>N. norm (f n x) \<le> M n"
    6.53 -        using assms(1)[OF `x \<in> A`] by simp
    6.54 +        using assms(1)[OF \<open>x \<in> A\<close>] by simp
    6.55        hence summable_norm_f: "summable (\<lambda>n. norm (f n x))"
    6.56 -        by(rule summable_norm_comparison_test[OF _ `summable M`])
    6.57 +        by(rule summable_norm_comparison_test[OF _ \<open>summable M\<close>])
    6.58        have summable_f: "summable (\<lambda>n. f n x)"
    6.59          using summable_norm_cancel[OF summable_norm_f] .
    6.60        have summable_norm_f_plus_k: "summable (\<lambda>i. norm (f (i + k) x))"
    6.61          using summable_ignore_initial_segment[OF summable_norm_f]
    6.62          by auto
    6.63        have summable_M_plus_k: "summable (\<lambda>i. M (i + k))"
    6.64 -        using summable_ignore_initial_segment[OF `summable M`]
    6.65 +        using summable_ignore_initial_segment[OF \<open>summable M\<close>]
    6.66          by auto
    6.67  
    6.68        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))"
    6.69 @@ -152,7 +152,7 @@
    6.70          using summable_norm[OF summable_norm_f_plus_k] .
    6.71        also have "... \<le> (\<Sum>i. M (i + k))"
    6.72          by (rule suminf_le[OF _ summable_norm_f_plus_k summable_M_plus_k])
    6.73 -           (simp add: assms(1)[OF `x \<in> A`])
    6.74 +           (simp add: assms(1)[OF \<open>x \<in> A\<close>])
    6.75        finally show "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) < e"
    6.76          using elim by auto
    6.77      qed
    6.78 @@ -163,12 +163,12 @@
    6.79    by simp
    6.80  
    6.81  named_theorems uniform_limit_intros "introduction rules for uniform_limit"
    6.82 -setup {*
    6.83 +setup \<open>
    6.84    Global_Theory.add_thms_dynamic (@{binding uniform_limit_eq_intros},
    6.85      fn context =>
    6.86        Named_Theorems.get (Context.proof_of context) @{named_theorems uniform_limit_intros}
    6.87        |> map_filter (try (fn thm => @{thm uniform_limit_eq_rhs} OF [thm])))
    6.88 -*}
    6.89 +\<close>
    6.90  
    6.91  lemma (in bounded_linear) uniform_limit[uniform_limit_intros]:
    6.92    assumes "uniform_limit X g l F"
    6.93 @@ -178,7 +178,7 @@
    6.94    from pos_bounded obtain K
    6.95      where K: "\<And>x y. dist (f x) (f y) \<le> K * dist x y" "K > 0"
    6.96      by (auto simp: ac_simps dist_norm diff[symmetric])
    6.97 -  assume "0 < e" with `K > 0` have "e / K > 0" by simp
    6.98 +  assume "0 < e" with \<open>K > 0\<close> have "e / K > 0" by simp
    6.99    from uniform_limitD[OF assms this]
   6.100    show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f (g n x)) (f (l x)) < e"
   6.101      by eventually_elim (metis le_less_trans mult.commute pos_less_divide_eq K)
   6.102 @@ -245,15 +245,15 @@
   6.103      and Kl: "Kl > 0" "\<And>x. x \<in> X \<Longrightarrow> norm (l x) \<le> Kl"
   6.104      by (auto simp: bounded_pos)
   6.105    hence "K * Km * 4 > 0" "K * Kl * 4 > 0"
   6.106 -    using `K > 0`
   6.107 +    using \<open>K > 0\<close>
   6.108      by simp_all
   6.109    assume "0 < e"
   6.110  
   6.111    hence "sqrt e > 0" by simp
   6.112 -  from uniform_limitD[OF assms(1) divide_pos_pos[OF this `sqrt (K*4) > 0`]]
   6.113 -    uniform_limitD[OF assms(2) divide_pos_pos[OF this `sqrt (K*4) > 0`]]
   6.114 -    uniform_limitD[OF assms(1) divide_pos_pos[OF `e > 0` `K * Km * 4 > 0`]]
   6.115 -    uniform_limitD[OF assms(2) divide_pos_pos[OF `e > 0` `K * Kl * 4 > 0`]]
   6.116 +  from uniform_limitD[OF assms(1) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
   6.117 +    uniform_limitD[OF assms(2) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
   6.118 +    uniform_limitD[OF assms(1) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Km * 4 > 0\<close>]]
   6.119 +    uniform_limitD[OF assms(2) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Kl * 4 > 0\<close>]]
   6.120    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"
   6.121    proof eventually_elim
   6.122      case (elim n)
   6.123 @@ -266,31 +266,31 @@
   6.124          norm (prod (l x) (g n x - m x))"
   6.125          by (auto simp: dist_norm prod_diff_prod intro: order_trans norm_triangle_ineq add_mono)
   6.126        also note K(2)[of "f n x - l x" "g n x - m x"]
   6.127 -      also from elim(1)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
   6.128 +      also from elim(1)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
   6.129        have "norm (f n x - l x) \<le> sqrt e / sqrt (K * 4)"
   6.130          by simp
   6.131 -      also from elim(2)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
   6.132 +      also from elim(2)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
   6.133        have "norm (g n x - m x) \<le> sqrt e / sqrt (K * 4)"
   6.134          by simp
   6.135        also have "sqrt e / sqrt (K * 4) * (sqrt e / sqrt (K * 4)) * K = e / 4"
   6.136 -        using `K > 0` `e > 0` by auto
   6.137 +        using \<open>K > 0\<close> \<open>e > 0\<close> by auto
   6.138        also note K(2)[of "f n x - l x" "m x"]
   6.139        also note K(2)[of "l x" "g n x - m x"]
   6.140 -      also from elim(3)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
   6.141 +      also from elim(3)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
   6.142        have "norm (f n x - l x) \<le> e / (K * Km * 4)"
   6.143          by simp
   6.144 -      also from elim(4)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
   6.145 +      also from elim(4)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
   6.146        have "norm (g n x - m x) \<le> e / (K * Kl * 4)"
   6.147          by simp
   6.148 -      also note Kl(2)[OF `_ \<in> X`]
   6.149 -      also note Km(2)[OF `_ \<in> X`]
   6.150 +      also note Kl(2)[OF \<open>_ \<in> X\<close>]
   6.151 +      also note Km(2)[OF \<open>_ \<in> X\<close>]
   6.152        also have "e / (K * Km * 4) * Km * K = e / 4"
   6.153 -        using `K > 0` `Km > 0` by simp
   6.154 +        using \<open>K > 0\<close> \<open>Km > 0\<close> by simp
   6.155        also have " Kl * (e / (K * Kl * 4)) * K = e / 4"
   6.156 -        using `K > 0` `Kl > 0` by simp
   6.157 -      also have "e / 4 + e / 4 + e / 4 < e" using `e > 0` by simp
   6.158 +        using \<open>K > 0\<close> \<open>Kl > 0\<close> by simp
   6.159 +      also have "e / 4 + e / 4 + e / 4 < e" using \<open>e > 0\<close> by simp
   6.160        finally show "dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
   6.161 -        using `K > 0` `Kl > 0` `Km > 0` `e > 0`
   6.162 +        using \<open>K > 0\<close> \<open>Kl > 0\<close> \<open>Km > 0\<close> \<open>e > 0\<close>
   6.163          by (simp add: algebra_simps mult_right_mono divide_right_mono)
   6.164      qed
   6.165    qed
     7.1 --- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Mon Sep 21 21:43:09 2015 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Mon Sep 21 21:46:14 2015 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -section{*Bernstein-Weierstrass and Stone-Weierstrass Theorems*}
     7.5 +section\<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
     7.6  
     7.7  theory Weierstrass
     7.8  imports Uniform_Limit Path_Connected
     7.9 @@ -11,7 +11,7 @@
    7.10  (*Power.thy:*)
    7.11  declare power_divide [where b = "numeral w" for w, simp del]
    7.12  
    7.13 -subsection {*Bernstein polynomials*}
    7.14 +subsection \<open>Bernstein polynomials\<close>
    7.15  
    7.16  definition Bernstein :: "[nat,nat,real] \<Rightarrow> real" where
    7.17    "Bernstein n k x \<equiv> of_nat (n choose k) * x ^ k * (1 - x) ^ (n - k)"
    7.18 @@ -65,7 +65,7 @@
    7.19      by auto
    7.20  qed
    7.21  
    7.22 -subsection {*Explicit Bernstein version of the 1D Weierstrass approximation theorem*}
    7.23 +subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
    7.24  
    7.25  lemma Bernstein_Weierstrass:
    7.26    fixes f :: "real \<Rightarrow> real"
    7.27 @@ -87,11 +87,11 @@
    7.28      assume n: "Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>) \<le> n" and x: "0 \<le> x" "x \<le> 1"
    7.29      have "0 < n" using n by simp
    7.30      have ed0: "- (e * d\<^sup>2) < 0"
    7.31 -      using e `0<d` by simp
    7.32 +      using e \<open>0<d\<close> by simp
    7.33      also have "... \<le> M * 4"
    7.34 -      using `0\<le>M` by simp
    7.35 +      using \<open>0\<le>M\<close> by simp
    7.36      finally have [simp]: "real (nat \<lceil>4 * M / (e * d\<^sup>2)\<rceil>) = real \<lceil>4 * M / (e * d\<^sup>2)\<rceil>"
    7.37 -      using `0\<le>M` e `0<d`
    7.38 +      using \<open>0\<le>M\<close> e \<open>0<d\<close>
    7.39        by (simp add: Real.real_of_nat_Suc field_simps)
    7.40      have "4*M/(e*d\<^sup>2) + 1 \<le> real (Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>))"
    7.41        by (simp add: Real.real_of_nat_Suc)
    7.42 @@ -137,7 +137,7 @@
    7.43          also have "... \<le> 2 * M * ((x - k/n)\<^sup>2 / d\<^sup>2)"
    7.44            apply simp
    7.45            apply (rule Rings.ordered_semiring_class.mult_left_mono [of 1 "((x - k/n)\<^sup>2 / d\<^sup>2)", simplified])
    7.46 -          using dle `d>0` `M\<ge>0` by auto
    7.47 +          using dle \<open>d>0\<close> \<open>M\<ge>0\<close> by auto
    7.48          also have "... \<le> e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2"
    7.49            using e  by simp
    7.50          finally show ?thesis .
    7.51 @@ -152,12 +152,12 @@
    7.52        done
    7.53      also have "... \<le> e/2 + (2 * M) / (d\<^sup>2 * n)"
    7.54        apply (simp only: setsum.distrib Rings.semiring_class.distrib_right setsum_right_distrib [symmetric] mult.assoc sum_bern)
    7.55 -      using `d>0` x
    7.56 +      using \<open>d>0\<close> x
    7.57        apply (simp add: divide_simps Mge0 mult_le_one mult_left_le)
    7.58        done
    7.59      also have "... < e"
    7.60        apply (simp add: field_simps)
    7.61 -      using `d>0` nbig e `n>0`
    7.62 +      using \<open>d>0\<close> nbig e \<open>n>0\<close>
    7.63        apply (simp add: divide_simps algebra_simps)
    7.64        using ed0 by linarith
    7.65      finally have "\<bar>f x - (\<Sum>k = 0..n. f (real k / real n) * Bernstein n k x)\<bar> < e" .
    7.66 @@ -167,7 +167,7 @@
    7.67  qed
    7.68  
    7.69  
    7.70 -subsection {*General Stone-Weierstrass theorem*}
    7.71 +subsection \<open>General Stone-Weierstrass theorem\<close>
    7.72  
    7.73  text\<open>Source:
    7.74  Bruno Brosowski and Frank Deutsch.
    7.75 @@ -282,7 +282,7 @@
    7.76      show ?thesis
    7.77        using subU i t
    7.78        apply (clarsimp simp: p_def divide_simps)
    7.79 -      apply (rule setsum_pos2 [OF `finite subU`])
    7.80 +      apply (rule setsum_pos2 [OF \<open>finite subU\<close>])
    7.81        using Uf t pf01 apply auto
    7.82        apply (force elim!: subsetCE)
    7.83        done
    7.84 @@ -345,10 +345,10 @@
    7.85      using t0 pf by (simp add: q_def power_0_left)
    7.86    { fix t and n::nat
    7.87      assume t: "t \<in> s \<inter> V"
    7.88 -    with `k>0` V have "k * p t < k * \<delta> / 2"
    7.89 +    with \<open>k>0\<close> V have "k * p t < k * \<delta> / 2"
    7.90         by force
    7.91      then have "1 - (k * \<delta> / 2)^n \<le> 1 - (k * p t)^n"
    7.92 -      using  `k>0` p01 t by (simp add: power_mono)
    7.93 +      using  \<open>k>0\<close> p01 t by (simp add: power_mono)
    7.94      also have "... \<le> q n t"
    7.95        using Bernoulli_inequality [of "- ((p t)^n)" "k^n"]
    7.96        apply (simp add: q_def)
    7.97 @@ -357,7 +357,7 @@
    7.98    } note limitV = this
    7.99    { fix t and n::nat
   7.100      assume t: "t \<in> s - U"
   7.101 -    with `k>0` U have "k * \<delta> \<le> k * p t"
   7.102 +    with \<open>k>0\<close> U have "k * \<delta> \<le> k * p t"
   7.103        by (simp add: pt_\<delta>)
   7.104      with k\<delta> have kpt: "1 < k * p t"
   7.105        by (blast intro: less_le_trans)
   7.106 @@ -366,9 +366,9 @@
   7.107      have ptn_le: "p t ^ n \<le> 1"
   7.108        by (meson DiffE atLeastAtMost_iff p01 power_le_one t)
   7.109      have "q n t = (1/(k^n * (p t)^n)) * (1 - p t ^ n) ^ (k^n) * k^n * (p t)^n"
   7.110 -      using pt_pos [OF t] `k>0` by (simp add: q_def)
   7.111 +      using pt_pos [OF t] \<open>k>0\<close> by (simp add: q_def)
   7.112      also have "... \<le> (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + k^n * (p t)^n)"
   7.113 -      using pt_pos [OF t] `k>0`
   7.114 +      using pt_pos [OF t] \<open>k>0\<close>
   7.115        apply simp
   7.116        apply (simp only: times_divide_eq_right [symmetric])
   7.117        apply (rule mult_left_mono [of "1::real", simplified])
   7.118 @@ -377,20 +377,20 @@
   7.119        using ptn_le by linarith
   7.120      also have "... \<le> (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + (p t)^n) ^ (k^n)"
   7.121        apply (rule mult_left_mono [OF Bernoulli_inequality [of "p t ^ n" "k^n"]])
   7.122 -      using `k>0` ptn_pos ptn_le
   7.123 +      using \<open>k>0\<close> ptn_pos ptn_le
   7.124        apply (auto simp: power_mult_distrib)
   7.125        done
   7.126      also have "... = (1/(k * (p t))^n) * (1 - p t ^ (2*n)) ^ (k^n)"
   7.127 -      using pt_pos [OF t] `k>0`
   7.128 +      using pt_pos [OF t] \<open>k>0\<close>
   7.129        by (simp add: algebra_simps power_mult power2_eq_square power_mult_distrib [symmetric])
   7.130      also have "... \<le> (1/(k * (p t))^n) * 1"
   7.131        apply (rule mult_left_mono [OF power_le_one])
   7.132        apply (metis diff_le_iff(1) less_eq_real_def mult.commute power_le_one power_mult ptn_pos ptn_le)
   7.133 -      using pt_pos [OF t] `k>0`
   7.134 +      using pt_pos [OF t] \<open>k>0\<close>
   7.135        apply auto
   7.136        done
   7.137      also have "... \<le> (1 / (k*\<delta>))^n"
   7.138 -      using `k>0` \<delta>01  power_mono pt_\<delta> t
   7.139 +      using \<open>k>0\<close> \<delta>01  power_mono pt_\<delta> t
   7.140        by (fastforce simp: field_simps)
   7.141      finally have "q n t \<le> (1 / (real k * \<delta>)) ^ n " .
   7.142    } note limitNonU = this
   7.143 @@ -401,13 +401,13 @@
   7.144    have NN1: "\<And>e. e>0 \<Longrightarrow> (k * \<delta> / 2)^NN e < e"
   7.145      apply (subst Transcendental.ln_less_cancel_iff [symmetric])
   7.146        prefer 3 apply (subst ln_realpow)
   7.147 -    using `k>0` `\<delta>>0` NN  k\<delta>
   7.148 +    using \<open>k>0\<close> \<open>\<delta>>0\<close> NN  k\<delta>
   7.149      apply (force simp add: field_simps)+
   7.150      done
   7.151    have NN0: "\<And>e. e>0 \<Longrightarrow> (1/(k*\<delta>))^NN e < e"
   7.152      apply (subst Transcendental.ln_less_cancel_iff [symmetric])
   7.153        prefer 3 apply (subst ln_realpow)
   7.154 -    using `k>0` `\<delta>>0` NN k\<delta>
   7.155 +    using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta>
   7.156      apply (force simp add: field_simps ln_div)+
   7.157      done
   7.158    { fix t and e::real
   7.159 @@ -416,11 +416,11 @@
   7.160      proof -
   7.161        assume t: "t \<in> s \<inter> V"
   7.162        show "1 - q (NN e) t < e"
   7.163 -        by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF `e>0`]])
   7.164 +        by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF \<open>e>0\<close>]])
   7.165      next
   7.166        assume t: "t \<in> s - U"
   7.167        show "q (NN e) t < e"
   7.168 -      using  limitNonU [OF t] less_le_trans [OF NN0 [OF `e>0`]] not_le by blast
   7.169 +      using  limitNonU [OF t] less_le_trans [OF NN0 [OF \<open>e>0\<close>]] not_le by blast
   7.170      qed
   7.171    } 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)"
   7.172      using q01
   7.173 @@ -445,7 +445,7 @@
   7.174        using assms by auto
   7.175      then have "\<exists>V. open V \<and> w \<in> V \<and> s \<inter> V \<subseteq> -B \<and>
   7.176                 (\<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))"
   7.177 -      using one [of "-B" w b] assms `w \<in> A` by simp
   7.178 +      using one [of "-B" w b] assms \<open>w \<in> A\<close> by simp
   7.179    }
   7.180    then obtain Vf where Vf:
   7.181           "\<And>w. w \<in> A \<Longrightarrow> open (Vf w) \<and> w \<in> Vf w \<and> s \<inter> Vf w \<subseteq> -B \<and>
   7.182 @@ -462,7 +462,7 @@
   7.183    obtain subA where subA: "subA \<subseteq> A" "finite subA" "A \<subseteq> (\<Union>x \<in> subA. Vf x)"
   7.184      by (blast intro: that open_Vf compactE_image [OF com_A _ setsum_max_0])
   7.185    then have [simp]: "subA \<noteq> {}"
   7.186 -    using `a \<in> A` by auto
   7.187 +    using \<open>a \<in> A\<close> by auto
   7.188    then have cardp: "card subA > 0" using subA
   7.189      by (simp add: card_gt_0_iff)
   7.190    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)"
   7.191 @@ -623,7 +623,7 @@
   7.192      then have fj1: "f t \<le> (j - 1/3)*e"
   7.193        by (simp add: A_def)
   7.194      then have Anj: "t \<notin> A i" if "i<j" for i
   7.195 -      using  Aj  `i<j`
   7.196 +      using  Aj  \<open>i<j\<close>
   7.197        apply (simp add: j_def)
   7.198        using not_less_Least by blast
   7.199      have j1: "1 \<le> j"
   7.200 @@ -639,7 +639,7 @@
   7.201        then obtain d where "i+2+d = j"
   7.202          using le_Suc_ex that by blast
   7.203        then have "t \<in> B i"
   7.204 -        using Anj e ge_fx [OF t] `1 \<le> n` fpos [OF t] t
   7.205 +        using Anj e ge_fx [OF t] \<open>1 \<le> n\<close> fpos [OF t] t
   7.206          apply (simp add: A_def B_def)
   7.207          apply (clarsimp simp add: field_simps real_of_nat_diff not_le real_of_nat_Suc)
   7.208          apply (rule order_trans [of _ "e * 2 + (e * (real d * 3) + e * (real i * 3))"])
   7.209 @@ -664,9 +664,9 @@
   7.210        apply simp
   7.211        done
   7.212      also have "... \<le> j*e + e*(n - j + 1)*e/n "
   7.213 -      using `1 \<le> n` e  by (simp add: field_simps)
   7.214 +      using \<open>1 \<le> n\<close> e  by (simp add: field_simps)
   7.215      also have "... \<le> j*e + e*e"
   7.216 -      using `1 \<le> n` e j1 by (simp add: field_simps)
   7.217 +      using \<open>1 \<le> n\<close> e j1 by (simp add: field_simps)
   7.218      also have "... < (j + 1/3)*e"
   7.219        using e by (auto simp: field_simps)
   7.220      finally have gj1: "g t < (j + 1 / 3) * e" .
   7.221 @@ -737,7 +737,7 @@
   7.222        assume n: "N \<le> n"  "\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + real n)"
   7.223        assume x: "x \<in> s"
   7.224        have "\<not> real (Suc n) < inverse e"
   7.225 -        using `N \<le> n` N using less_imp_inverse_less by force
   7.226 +        using \<open>N \<le> n\<close> N using less_imp_inverse_less by force
   7.227        then have "1 / (1 + real n) \<le> e"
   7.228          using e by (simp add: field_simps real_of_nat_Suc)
   7.229        then have "\<bar>f x - g x\<bar> < e"
   7.230 @@ -756,7 +756,7 @@
   7.231      done
   7.232  qed
   7.233  
   7.234 -text{*A HOL Light formulation*}
   7.235 +text\<open>A HOL Light formulation\<close>
   7.236  corollary Stone_Weierstrass_HOL:
   7.237    fixes R :: "('a::t2_space \<Rightarrow> real) set" and s :: "'a set"
   7.238    assumes "compact s"  "\<And>c. P(\<lambda>x. c::real)"
   7.239 @@ -772,12 +772,12 @@
   7.240      using assms
   7.241      by auto
   7.242    show ?thesis
   7.243 -    using PR.Stone_Weierstrass_basic [OF `continuous_on s f` `0 < e`]
   7.244 +    using PR.Stone_Weierstrass_basic [OF \<open>continuous_on s f\<close> \<open>0 < e\<close>]
   7.245      by blast
   7.246  qed
   7.247  
   7.248  
   7.249 -subsection {*Polynomial functions*}
   7.250 +subsection \<open>Polynomial functions\<close>
   7.251  
   7.252  inductive real_polynomial_function :: "('a::real_normed_vector \<Rightarrow> real) \<Rightarrow> bool" where
   7.253      linear: "bounded_linear f \<Longrightarrow> real_polynomial_function f"
   7.254 @@ -978,7 +978,7 @@
   7.255      by (simp add: euclidean_representation_setsum_fun)
   7.256  qed
   7.257  
   7.258 -subsection {*Stone-Weierstrass theorem for polynomial functions*}
   7.259 +subsection \<open>Stone-Weierstrass theorem for polynomial functions\<close>
   7.260  
   7.261  text\<open>First, we need to show that they are continous, differentiable and separable.\<close>
   7.262  
   7.263 @@ -1048,12 +1048,12 @@
   7.264      assume "b \<in> Basis"
   7.265      then
   7.266      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)"
   7.267 -      using assms [unfolded polynomial_function_iff_Basis_inner, rule_format]  `b \<in> Basis`
   7.268 +      using assms [unfolded polynomial_function_iff_Basis_inner, rule_format]  \<open>b \<in> Basis\<close>
   7.269        has_real_derivative_polynomial_function
   7.270        by blast
   7.271      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))"
   7.272        apply (rule_tac x="\<lambda>x. p' x *\<^sub>R b" in exI)
   7.273 -      using `b \<in> Basis` p'
   7.274 +      using \<open>b \<in> Basis\<close> p'
   7.275        apply (simp add: polynomial_function_iff_Basis_inner inner_Basis)
   7.276        apply (auto intro: derivative_eq_intros pd)
   7.277        done
   7.278 @@ -1096,7 +1096,7 @@
   7.279      apply (auto intro: real_polynomial_function_separable)
   7.280      done
   7.281    show ?thesis
   7.282 -    using PR.Stone_Weierstrass_basic [OF `continuous_on s f` `0 < e`]
   7.283 +    using PR.Stone_Weierstrass_basic [OF \<open>continuous_on s f\<close> \<open>0 < e\<close>]
   7.284      by blast
   7.285  qed
   7.286  
   7.287 @@ -1131,7 +1131,7 @@
   7.288        by (rule norm_setsum)
   7.289      also have "... < of_nat DIM('b) * (e / DIM('b))"
   7.290        apply (rule setsum_bounded_above_strict)
   7.291 -      apply (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf `x \<in> s`)
   7.292 +      apply (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf \<open>x \<in> s\<close>)
   7.293        apply (rule DIM_positive)
   7.294        done
   7.295      also have "... = e"
   7.296 @@ -1149,8 +1149,8 @@
   7.297  
   7.298  subsection\<open>Polynomial functions as paths\<close>
   7.299  
   7.300 -text{*One application is to pick a smooth approximation to a path,
   7.301 -or just pick a smooth path anyway in an open connected set*}
   7.302 +text\<open>One application is to pick a smooth approximation to a path,
   7.303 +or just pick a smooth path anyway in an open connected set\<close>
   7.304  
   7.305  lemma path_polynomial_function:
   7.306      fixes g  :: "real \<Rightarrow> 'b::euclidean_space"
   7.307 @@ -1192,7 +1192,7 @@
   7.308  proof -
   7.309    have "path_connected s" using assms
   7.310      by (simp add: connected_open_path_connected)
   7.311 -  with `x \<in> s` `y \<in> s` obtain p where p: "path p" "path_image p \<subseteq> s" "pathstart p = x" "pathfinish p = y"
   7.312 +  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"
   7.313      by (force simp: path_connected_def)
   7.314    have "\<exists>e. 0 < e \<and> (\<forall>x \<in> path_image p. ball x e \<subseteq> s)"
   7.315    proof (cases "s = UNIV")
   7.316 @@ -1211,7 +1211,7 @@
   7.317    then obtain e where "0 < e"and eb: "\<And>x. x \<in> path_image p \<Longrightarrow> ball x e \<subseteq> s"
   7.318      by auto
   7.319    show ?thesis
   7.320 -    using path_approx_polynomial_function [OF `path p` `0 < e`]
   7.321 +    using path_approx_polynomial_function [OF \<open>path p\<close> \<open>0 < e\<close>]
   7.322      apply clarify
   7.323      apply (intro exI conjI, assumption)
   7.324      using p