merged
authorpaulson
Thu Aug 31 20:03:25 2017 +0100 (21 months ago)
changeset 66705193f1317c381
parent 66578 6a034c6c423f
parent 66704 7551bd9ff5c7
child 66706 bd7901f702c9
merged
     1.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Aug 31 20:19:55 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Aug 31 20:03:25 2017 +0100
     1.3 @@ -2253,9 +2253,7 @@
     1.4      have "(\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on S" 
     1.5        using assms integrable_component [OF fcomp, where y=i] that by simp
     1.6      then have "(\<lambda>x. f x \<bullet> i) absolutely_integrable_on S"
     1.7 -      apply -
     1.8 -      apply (rule abs_absolutely_integrableI_1, auto)
     1.9 -      by (simp add: f integrable_component)
    1.10 +      using abs_absolutely_integrableI_1 f integrable_component by blast
    1.11      then show ?thesis
    1.12        by (rule absolutely_integrable_scaleR_right)
    1.13    qed
     2.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 31 20:19:55 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 31 20:03:25 2017 +0100
     2.3 @@ -6049,8 +6049,7 @@
     2.4    have "norm (integral S f) \<le> integral S ((\<lambda>x. x \<bullet> k) \<circ> g)"
     2.5      apply (rule integral_norm_bound_integral[OF f integrable_linear[OF g]])
     2.6      apply (simp add: bounded_linear_inner_left)
     2.7 -    unfolding o_def
     2.8 -    apply (metis fg)
     2.9 +    apply (metis fg o_def)
    2.10      done
    2.11    then show ?thesis
    2.12      unfolding o_def integral_component_eq[OF g] .
    2.13 @@ -6167,7 +6166,6 @@
    2.14        have "closed_segment x0 x \<subseteq> U"
    2.15          by (rule \<open>convex U\<close>[unfolded convex_contains_segment, rule_format, OF \<open>x0 \<in> U\<close> \<open>x \<in> U\<close>])
    2.16        from elim have [intro]: "x \<in> U" by auto
    2.17 -
    2.18        have "?F x - ?F x0 - ?dF (x - x0) =
    2.19          integral (cbox a b) (\<lambda>y. f x y - f x0 y - fx x0 y (x - x0))"
    2.20          (is "_ = ?id")
    2.21 @@ -6204,7 +6202,7 @@
    2.22        also have "\<dots> < e' * norm (x - x0)"
    2.23          using \<open>e' > 0\<close>
    2.24          apply (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
    2.25 -        apply  (auto simp: divide_simps e_def)
    2.26 +        apply (auto simp: divide_simps e_def)
    2.27          by (metis \<open>0 < e\<close> e_def order.asym zero_less_divide_iff)
    2.28        finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
    2.29        then show ?case
    2.30 @@ -6293,14 +6291,12 @@
    2.31      by atomize_elim (auto simp: integrable_on_def intro!: choice)
    2.32  
    2.33    moreover
    2.34 -
    2.35    have gi[simp]: "g integrable_on (cbox a b)"
    2.36      by (auto intro!: integrable_continuous uniform_limit_theorem[OF _ u] eventuallyI c)
    2.37    then obtain J where J: "(g has_integral J) (cbox a b)"
    2.38      by blast
    2.39  
    2.40    moreover
    2.41 -
    2.42    have "(I \<longlongrightarrow> J) F"
    2.43    proof cases
    2.44      assume "content (cbox a b) = 0"
    2.45 @@ -6449,20 +6445,17 @@
    2.46            f integrable_continuous_real)+
    2.47    have deriv: "(((\<lambda>x. integral {c..x} f) \<circ> g) has_vector_derivative g' x *\<^sub>R f (g x))
    2.48                   (at x within {a..b})" if "x \<in> {a..b} - s" for x
    2.49 -    apply (rule has_vector_derivative_eq_rhs)
    2.50 -    apply (rule vector_diff_chain_within)
    2.51 -    apply (subst has_field_derivative_iff_has_vector_derivative [symmetric])
    2.52 -    apply (rule deriv that)+
    2.53 -    apply (rule has_vector_derivative_within_subset)
    2.54 -    apply (rule integral_has_vector_derivative f)+
    2.55 -    using that le subset
    2.56 -    apply blast+
    2.57 -    done
    2.58 +  proof (rule has_vector_derivative_eq_rhs [OF vector_diff_chain_within refl])
    2.59 +    show "(g has_vector_derivative g' x) (at x within {a..b})"
    2.60 +      using deriv has_field_derivative_iff_has_vector_derivative that by blast
    2.61 +    show "((\<lambda>x. integral {c..x} f) has_vector_derivative f (g x)) 
    2.62 +          (at (g x) within g ` {a..b})"
    2.63 +      using that le subset
    2.64 +      by (blast intro: has_vector_derivative_within_subset integral_has_vector_derivative f)
    2.65 +  qed
    2.66    have deriv: "(?F has_vector_derivative g' x *\<^sub>R f (g x))
    2.67                    (at x)" if "x \<in> {a..b} - (s \<union> {a,b})" for x
    2.68      using deriv[of x] that by (simp add: at_within_closed_interval o_def)
    2.69 -
    2.70 -
    2.71    have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
    2.72      using le cont_int s deriv cont_int
    2.73      by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all
    2.74 @@ -6794,20 +6787,21 @@
    2.75              \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX"
    2.76          by (rule norm_xx [OF integral_Pair_const 1 2])
    2.77      } note * = this
    2.78 -    show "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
    2.79 +    have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e" 
    2.80 +      if "\<forall>x\<in>?CBOX. \<forall>x'\<in>?CBOX. norm (x' - x) < k \<longrightarrow> norm (f x' - f x) < e /(2 * content (?CBOX))" "0 < k" for k
    2.81 +    proof -
    2.82 +      obtain p where ptag: "p tagged_division_of cbox (a, c) (b, d)" 
    2.83 +                 and fine: "(\<lambda>x. ball x k) fine p"
    2.84 +        using fine_division_exists \<open>0 < k\<close> by blast
    2.85 +      show ?thesis
    2.86 +        apply (rule op_acbd [OF division_of_tagged_division [OF ptag]])
    2.87 +        using that fine ptag \<open>0 < k\<close> by (auto simp: *)
    2.88 +    qed
    2.89 +    then show "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
    2.90        using compact_uniformly_continuous [OF assms compact_cbox]
    2.91        apply (simp add: uniformly_continuous_on_def dist_norm)
    2.92        apply (drule_tac x="e/2 / content?CBOX" in spec)
    2.93 -      using cbp \<open>0 < e\<close>
    2.94 -      apply (auto simp: zero_less_mult_iff)
    2.95 -      apply (rename_tac k)
    2.96 -      apply (rule_tac e1=k in fine_division_exists [OF gauge_ball, where a = "(a,c)" and b = "(b,d)"])
    2.97 -      apply assumption
    2.98 -      apply (rule op_acbd)
    2.99 -      apply (erule division_of_tagged_division)
   2.100 -      using *
   2.101 -      apply auto
   2.102 -      done
   2.103 +      using cbp \<open>0 < e\<close> by (auto simp: zero_less_mult_iff)
   2.104    qed
   2.105    then show ?thesis
   2.106      by simp
   2.107 @@ -6850,7 +6844,6 @@
   2.108    shows   "((\<lambda>x::real. exp (-a*x)) has_integral exp (-a*c)/a) {c..}"
   2.109  proof -
   2.110    define f where "f = (\<lambda>k x. if x \<in> {c..real k} then exp (-a*x) else 0)"
   2.111 -
   2.112    {
   2.113      fix k :: nat assume k: "of_nat k \<ge> c"
   2.114      from k a
     3.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Thu Aug 31 20:19:55 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Aug 31 20:03:25 2017 +0100
     3.3 @@ -1919,89 +1919,71 @@
     3.4  
     3.5  lemma interval_bisection_step:
     3.6    fixes type :: "'a::euclidean_space"
     3.7 -  assumes "P {}"
     3.8 -    and "\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P (s \<union> t)"
     3.9 -    and "\<not> P (cbox a (b::'a))"
    3.10 +  assumes emp: "P {}"
    3.11 +    and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
    3.12 +    and non: "\<not> P (cbox a (b::'a))"
    3.13    obtains c d where "\<not> P (cbox c d)"
    3.14 -    and "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
    3.15 +    and "\<And>i. i \<in> Basis \<Longrightarrow> a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
    3.16  proof -
    3.17    have "cbox a b \<noteq> {}"
    3.18 -    using assms(1,3) by metis
    3.19 +    using emp non by metis
    3.20    then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
    3.21      by (force simp: mem_box)
    3.22 -  have UN_cases: "\<lbrakk>finite f;
    3.23 -           \<And>s. s\<in>f \<Longrightarrow> P s;
    3.24 -           \<And>s. s\<in>f \<Longrightarrow> \<exists>a b. s = cbox a b;
    3.25 -           \<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>f)" for f
    3.26 -  proof (induct f rule: finite_induct)
    3.27 -    case empty
    3.28 -    show ?case
    3.29 -      using assms(1) by auto
    3.30 +  have UN_cases: "\<lbrakk>finite \<F>;
    3.31 +           \<And>S. S\<in>\<F> \<Longrightarrow> P S;
    3.32 +           \<And>S. S\<in>\<F> \<Longrightarrow> \<exists>a b. S = cbox a b;
    3.33 +           \<And>S T. S\<in>\<F> \<Longrightarrow> T\<in>\<F> \<Longrightarrow> S \<noteq> T \<Longrightarrow> interior S \<inter> interior T = {}\<rbrakk> \<Longrightarrow> P (\<Union>\<F>)" for \<F>
    3.34 +  proof (induct \<F> rule: finite_induct)
    3.35 +    case empty show ?case
    3.36 +      using emp by auto
    3.37    next
    3.38      case (insert x f)
    3.39 -    show ?case
    3.40 -      unfolding Union_insert
    3.41 -      apply (rule assms(2)[rule_format])
    3.42 -      using Int_interior_Union_intervals [of f "interior x"]
    3.43 -      by (metis (no_types, lifting) insert insert_iff open_interior)
    3.44 +    then show ?case
    3.45 +      unfolding Union_insert by (metis Int_interior_Union_intervals Un insert_iff open_interior)
    3.46    qed
    3.47 -  let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or>
    3.48 -    (c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}"
    3.49 -  let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
    3.50 -  {
    3.51 -    presume "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d) \<Longrightarrow> False"
    3.52 -    then show thesis
    3.53 -      unfolding atomize_not not_all
    3.54 -      by (blast intro: that)
    3.55 -  }
    3.56 -  assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
    3.57 -  have "P (\<Union>?A)"
    3.58 +  let ?ab = "\<lambda>i. (a\<bullet>i + b\<bullet>i) / 2"
    3.59 +  let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = ?ab i) \<or>
    3.60 +    (c\<bullet>i = ?ab i) \<and> (d\<bullet>i = b\<bullet>i)}"
    3.61 +  have "P (\<Union>?A)" 
    3.62 +    if "\<And>c d.  \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i \<Longrightarrow> P (cbox c d)"
    3.63    proof (rule UN_cases)
    3.64 -    let ?B = "(\<lambda>s. cbox (\<Sum>i\<in>Basis. (if i \<in> s then a\<bullet>i else (a\<bullet>i + b\<bullet>i) / 2) *\<^sub>R i::'a)
    3.65 -      (\<Sum>i\<in>Basis. (if i \<in> s then (a\<bullet>i + b\<bullet>i) / 2 else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
    3.66 +    let ?B = "(\<lambda>S. cbox (\<Sum>i\<in>Basis. (if i \<in> S then a\<bullet>i else ?ab i) *\<^sub>R i::'a)
    3.67 +                        (\<Sum>i\<in>Basis. (if i \<in> S then ?ab i else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
    3.68      have "?A \<subseteq> ?B"
    3.69      proof
    3.70        fix x
    3.71        assume "x \<in> ?A"
    3.72        then obtain c d
    3.73          where x:  "x = cbox c d"
    3.74 -                  "\<And>i. i \<in> Basis \<Longrightarrow>
    3.75 -                        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
    3.76 -                        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast
    3.77 -      show "x \<in> ?B"
    3.78 -        unfolding image_iff x
    3.79 -        apply (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in bexI)
    3.80 -        apply (rule arg_cong2 [where f = cbox])
    3.81 -        using x(2) ab
    3.82 -        apply (auto simp add: euclidean_eq_iff[where 'a='a])
    3.83 -        by fastforce
    3.84 +          "\<And>i. i \<in> Basis \<Longrightarrow>
    3.85 +                        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i" 
    3.86 +        by blast
    3.87 +      have "c = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then a \<bullet> i else ?ab i) *\<^sub>R i)"
    3.88 +           "d = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then ?ab i else b \<bullet> i) *\<^sub>R i)"
    3.89 +        using x(2) ab by (fastforce simp add: euclidean_eq_iff[where 'a='a])+
    3.90 +      then show "x \<in> ?B"
    3.91 +        unfolding x by (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in image_eqI) auto
    3.92      qed
    3.93      then show "finite ?A"
    3.94        by (rule finite_subset) auto
    3.95    next
    3.96 -    fix s
    3.97 -    assume "s \<in> ?A"
    3.98 +    fix S
    3.99 +    assume "S \<in> ?A"
   3.100      then obtain c d
   3.101 -      where s: "s = cbox c d"
   3.102 -               "\<And>i. i \<in> Basis \<Longrightarrow>
   3.103 -                     c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
   3.104 -                     c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
   3.105 +      where s: "S = cbox c d"
   3.106 +               "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
   3.107        by blast
   3.108 -    show "P s"
   3.109 -      unfolding s
   3.110 -      apply (rule as[rule_format])
   3.111 -      using ab s(2) by force
   3.112 -    show "\<exists>a b. s = cbox a b"
   3.113 +    show "P S"
   3.114 +      unfolding s using ab s(2) by (fastforce intro!: that)
   3.115 +    show "\<exists>a b. S = cbox a b"
   3.116        unfolding s by auto
   3.117 -    fix t
   3.118 -    assume "t \<in> ?A"
   3.119 +    fix T
   3.120 +    assume "T \<in> ?A"
   3.121      then obtain e f where t:
   3.122 -      "t = cbox e f"
   3.123 -      "\<And>i. i \<in> Basis \<Longrightarrow>
   3.124 -        e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
   3.125 -        e \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> f \<bullet> i = b \<bullet> i"
   3.126 +      "T = cbox e f"
   3.127 +      "\<And>i. i \<in> Basis \<Longrightarrow> e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = ?ab i \<or> e \<bullet> i = ?ab i \<and> f \<bullet> i = b \<bullet> i"
   3.128        by blast
   3.129 -    assume "s \<noteq> t"
   3.130 +    assume "S \<noteq> T"
   3.131      then have "\<not> (c = e \<and> d = f)"
   3.132        unfolding s t by auto
   3.133      then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis"
   3.134 @@ -2011,24 +1993,15 @@
   3.135        using t(2)[OF i'] \<open>c \<bullet> i \<noteq> e \<bullet> i \<or> d \<bullet> i \<noteq> f \<bullet> i\<close> i' s(2) t(2) by fastforce
   3.136      have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}"
   3.137        by auto
   3.138 -    show "interior s \<inter> interior t = {}"
   3.139 +    show "interior S \<inter> interior T = {}"
   3.140        unfolding s t interior_cbox
   3.141      proof (rule *)
   3.142        fix x
   3.143        assume "x \<in> box c d" "x \<in> box e f"
   3.144        then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
   3.145 -        unfolding mem_box using i'
   3.146 -        by force+
   3.147 -      show False  using s(2)[OF i']
   3.148 -      proof safe
   3.149 -        assume as: "c \<bullet> i = a \<bullet> i" "d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2"
   3.150 -        show False
   3.151 -          using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps)
   3.152 -      next
   3.153 -        assume as: "c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" "d \<bullet> i = b \<bullet> i"
   3.154 -        show False
   3.155 -          using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps)
   3.156 -      qed
   3.157 +        unfolding mem_box using i'  by force+
   3.158 +      show False  using s(2)[OF i'] t(2)[OF i'] and i x  
   3.159 +        by auto
   3.160      qed
   3.161    qed
   3.162    also have "\<Union>?A = cbox a b"
   3.163 @@ -2037,48 +2010,30 @@
   3.164      assume "x \<in> \<Union>?A"
   3.165      then obtain c d where x:
   3.166        "x \<in> cbox c d"
   3.167 -      "\<And>i. i \<in> Basis \<Longrightarrow>
   3.168 -        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
   3.169 -        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
   3.170 +      "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
   3.171        by blast
   3.172 -    show "x\<in>cbox a b"
   3.173 -      unfolding mem_box
   3.174 -    proof safe
   3.175 -      fix i :: 'a
   3.176 -      assume i: "i \<in> Basis"
   3.177 -      then show "a \<bullet> i \<le> x \<bullet> i" "x \<bullet> i \<le> b \<bullet> i"
   3.178 -        using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto
   3.179 -    qed
   3.180 +    then show "x\<in>cbox a b"
   3.181 +      unfolding mem_box by force
   3.182    next
   3.183      fix x
   3.184      assume x: "x \<in> cbox a b"
   3.185 -    have "\<forall>i\<in>Basis.
   3.186 -      \<exists>c d. (c = a\<bullet>i \<and> d = (a\<bullet>i + b\<bullet>i) / 2 \<or> c = (a\<bullet>i + b\<bullet>i) / 2 \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
   3.187 +    then have "\<forall>i\<in>Basis. \<exists>c d. (c = a\<bullet>i \<and> d = ?ab i \<or> c = ?ab i \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
   3.188        (is "\<forall>i\<in>Basis. \<exists>c d. ?P i c d")
   3.189 -      unfolding mem_box
   3.190 -    proof
   3.191 -      fix i :: 'a
   3.192 -      assume i: "i \<in> Basis"
   3.193 -      have "?P i (a\<bullet>i) ((a \<bullet> i + b \<bullet> i) / 2) \<or> ?P i ((a \<bullet> i + b \<bullet> i) / 2) (b\<bullet>i)"
   3.194 -        using x[unfolded mem_box,THEN bspec, OF i] by auto
   3.195 -      then show "\<exists>c d. ?P i c d"
   3.196 -        by blast
   3.197 -    qed
   3.198 -    then obtain \<alpha> \<beta> where
   3.199 -     "\<forall>i\<in>Basis. (\<alpha> \<bullet> i = a \<bullet> i \<and> \<beta> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
   3.200 -         \<alpha> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> \<beta> \<bullet> i = b \<bullet> i) \<and> \<alpha> \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> \<beta> \<bullet> i"
   3.201 +      unfolding mem_box by (metis linear)
   3.202 +    then obtain \<alpha> \<beta> where "\<forall>i\<in>Basis. (\<alpha> \<bullet> i = a \<bullet> i \<and> \<beta> \<bullet> i = ?ab i \<or>
   3.203 +         \<alpha> \<bullet> i = ?ab i \<and> \<beta> \<bullet> i = b \<bullet> i) \<and> \<alpha> \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> \<beta> \<bullet> i"
   3.204        by (auto simp: choice_Basis_iff)
   3.205      then show "x\<in>\<Union>?A"
   3.206        by (force simp add: mem_box)
   3.207    qed
   3.208 -  finally show False
   3.209 -    using assms by auto
   3.210 +  finally show thesis
   3.211 +      by (metis (no_types, lifting) assms(3) that)
   3.212  qed
   3.213  
   3.214  lemma interval_bisection:
   3.215    fixes type :: "'a::euclidean_space"
   3.216    assumes "P {}"
   3.217 -    and "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))"
   3.218 +    and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
   3.219      and "\<not> P (cbox a (b::'a))"
   3.220    obtains x where "x \<in> cbox a b"
   3.221      and "\<forall>e>0. \<exists>c d. x \<in> cbox c d \<and> cbox c d \<subseteq> ball x e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
   3.222 @@ -2092,14 +2047,14 @@
   3.223        case True
   3.224        then show ?thesis by auto
   3.225      next
   3.226 -      case as: False
   3.227 +      case False
   3.228        obtain c d where "\<not> P (cbox c d)"
   3.229 -        "\<forall>i\<in>Basis.
   3.230 +        "\<And>i. i \<in> Basis \<Longrightarrow>
   3.231             fst x \<bullet> i \<le> c \<bullet> i \<and>
   3.232             c \<bullet> i \<le> d \<bullet> i \<and>
   3.233             d \<bullet> i \<le> snd x \<bullet> i \<and>
   3.234             2 * (d \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i"
   3.235 -        by (rule interval_bisection_step[of P, OF assms(1-2) as])
   3.236 +        by (blast intro: interval_bisection_step[of P, OF assms(1-2) False])
   3.237        then show ?thesis
   3.238          by (rule_tac x="(c,d)" in exI) auto
   3.239      qed
   3.240 @@ -2281,33 +2236,17 @@
   3.241  
   3.242  lemma tagged_division_finer:
   3.243    fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
   3.244 -  assumes "p tagged_division_of (cbox a b)"
   3.245 +  assumes ptag: "p tagged_division_of (cbox a b)"
   3.246      and "gauge d"
   3.247    obtains q where "q tagged_division_of (cbox a b)"
   3.248      and "d fine q"
   3.249      and "\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q"
   3.250  proof -
   3.251 -  let ?P = "\<lambda>p. p tagged_partial_division_of (cbox a b) \<longrightarrow> gauge d \<longrightarrow>
   3.252 -    (\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and>
   3.253 -      (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))"
   3.254 -  {
   3.255 -    have *: "finite p" "p tagged_partial_division_of (cbox a b)"
   3.256 -      using assms(1)
   3.257 -      unfolding tagged_division_of_def
   3.258 -      by auto
   3.259 -    presume "\<And>p. finite p \<Longrightarrow> ?P p"
   3.260 -    from this[rule_format,OF * assms(2)] 
   3.261 -    obtain q where q: "q tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}" "d fine q" "(\<forall>(x, k)\<in>p. k \<subseteq> d x \<longrightarrow> (x, k) \<in> q)"
   3.262 -      by auto
   3.263 -    with that[of q] show ?thesis
   3.264 -      using assms(1) by auto
   3.265 -  }
   3.266 -  fix p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
   3.267 -  assume as: "finite p"
   3.268 -  show "?P p"
   3.269 -    apply rule
   3.270 -    apply rule
   3.271 -    using as
   3.272 +  have p: "finite p" "p tagged_partial_division_of (cbox a b)"
   3.273 +    using ptag unfolding tagged_division_of_def by auto
   3.274 +  have "(\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and> (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))" 
   3.275 +    if "finite p" "p tagged_partial_division_of (cbox a b)" "gauge d" for p
   3.276 +    using that
   3.277    proof (induct p)
   3.278      case empty
   3.279      show ?case
   3.280 @@ -2325,7 +2264,7 @@
   3.281        unfolding xk by auto
   3.282      note p = tagged_partial_division_ofD[OF insert(4)]
   3.283      obtain u v where uv: "k = cbox u v"
   3.284 -      using p(4)[unfolded xk, OF insertI1] by blast
   3.285 +      using p(4) xk by blast
   3.286      have "finite {k. \<exists>x. (x, k) \<in> p}"
   3.287        apply (rule finite_subset[of _ "snd ` p"])
   3.288        using image_iff apply fastforce
   3.289 @@ -2363,6 +2302,9 @@
   3.290          done
   3.291      qed
   3.292    qed
   3.293 +  with p obtain q where q: "q tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}" "d fine q" "\<forall>(x, k)\<in>p. k \<subseteq> d x \<longrightarrow> (x, k) \<in> q"
   3.294 +    by (meson \<open>gauge d\<close>)
   3.295 +  with ptag that show ?thesis by auto
   3.296  qed
   3.297  
   3.298  subsubsection \<open>Covering lemma\<close>