more elimination of "guess", etc.
authorpaulson <lp15@cam.ac.uk>
Thu Aug 24 17:15:53 2017 +0100 (21 months ago)
changeset 665037685861f337d
parent 66498 97fc319d6089
child 66504 04b3a4548323
more elimination of "guess", etc.
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Linear_Algebra.thy
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 24 12:45:46 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 24 17:15:53 2017 +0100
     1.3 @@ -4228,33 +4228,28 @@
     1.4    obtains d where "0 < d"
     1.5      and "\<forall>t. c \<le> t \<and> t < c + d \<longrightarrow> norm (integral {a..c} f - integral {a..t} f) < e"
     1.6  proof -
     1.7 -  have *: "(\<lambda>x. f (- x)) integrable_on {-b .. -a}" "- b < - c" "- c \<le> - a"
     1.8 +  have intm: "(\<lambda>x. f (- x)) integrable_on {-b .. -a}" "- b < - c" "- c \<le> - a"
     1.9      using assms by auto
    1.10 -  from indefinite_integral_continuous_left[OF * \<open>e>0\<close>] guess d . note d = this
    1.11 +  from indefinite_integral_continuous_left[OF intm \<open>e>0\<close>]
    1.12 +  obtain d where "0 < d"
    1.13 +    and d: "\<And>t. \<lbrakk>- c - d < t; t \<le> -c\<rbrakk> 
    1.14 +             \<Longrightarrow> norm (integral {- b..- c} (\<lambda>x. f (-x)) - integral {- b..t} (\<lambda>x. f (-x))) < e"
    1.15 +    by metis
    1.16    let ?d = "min d (b - c)" 
    1.17    show ?thesis
    1.18 -    apply (rule that[of "?d"])
    1.19 -    apply safe
    1.20 -  proof -
    1.21 +  proof (intro that[of "?d"] allI impI)
    1.22      show "0 < ?d"
    1.23 -      using d(1) assms(3) by auto
    1.24 +      using \<open>0 < d\<close> \<open>c < b\<close> by auto
    1.25      fix t :: real
    1.26 -    assume as: "c \<le> t" "t < c + ?d"
    1.27 +    assume t: "c \<le> t \<and> t < c + ?d"
    1.28      have *: "integral {a..c} f = integral {a..b} f - integral {c..b} f"
    1.29 -      "integral {a..t} f = integral {a..b} f - integral {t..b} f"
    1.30 +            "integral {a..t} f = integral {a..b} f - integral {t..b} f"
    1.31        apply (simp_all only: algebra_simps)
    1.32 -      apply (rule_tac[!] integral_combine)
    1.33 -      using assms as
    1.34 -      apply auto
    1.35 -      done
    1.36 -    have "(- c) - d < (- t) \<and> - t \<le> - c"
    1.37 -      using as by auto note d(2)[rule_format,OF this]
    1.38 -    then show "norm (integral {a..c} f - integral {a..t} f) < e"
    1.39 -      unfolding *
    1.40 -      unfolding integral_reflect
    1.41 -      apply (subst norm_minus_commute)
    1.42 -      apply (auto simp add: algebra_simps)
    1.43 -      done
    1.44 +      using assms t by (auto simp: integral_combine)
    1.45 +    have "(- c) - d < (- t)" "- t \<le> - c"
    1.46 +      using t by auto 
    1.47 +    from d[OF this] show "norm (integral {a..c} f - integral {a..t} f) < e"
    1.48 +      by (auto simp add: algebra_simps norm_minus_commute *)
    1.49    qed
    1.50  qed
    1.51  
    1.52 @@ -4484,8 +4479,8 @@
    1.53  
    1.54  lemma has_integral_restrict_open_subinterval:
    1.55    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
    1.56 -  assumes "(f has_integral i) (cbox c d)"
    1.57 -    and "cbox c d \<subseteq> cbox a b"
    1.58 +  assumes intf: "(f has_integral i) (cbox c d)"
    1.59 +    and cb: "cbox c d \<subseteq> cbox a b"
    1.60    shows "((\<lambda>x. if x \<in> box c d then f x else 0) has_integral i) (cbox a b)"
    1.61  proof -
    1.62    define g where [abs_def]: "g x = (if x \<in>box c d then f x else 0)" for x
    1.63 @@ -4507,7 +4502,8 @@
    1.64      qed
    1.65    }
    1.66    assume "cbox c d \<noteq> {}"
    1.67 -  from partial_division_extend_1 [OF assms(2) this] guess p . note p=this
    1.68 +  then obtain p where p: "p division_of cbox a b" "cbox c d \<in> p"
    1.69 +    using cb partial_division_extend_1 by blast
    1.70    interpret operative "lift_option plus" "Some (0 :: 'b)"
    1.71      "\<lambda>i. if g integrable_on i then Some (integral i g) else None"
    1.72      by (fact operative_integralI)
    1.73 @@ -4536,16 +4532,13 @@
    1.74      then have "x \<in> p"
    1.75        by auto
    1.76      note div = division_ofD(2-5)[OF p(1) this]
    1.77 -    from div(3) guess u v by (elim exE) note uv=this
    1.78 +    then obtain u v where uv: "x = cbox u v" by blast
    1.79      have "interior x \<inter> interior (cbox c d) = {}"
    1.80        using div(4)[OF p(2)] x by auto
    1.81      then have "(g has_integral 0) x"
    1.82        unfolding uv
    1.83 -      apply -
    1.84 -      apply (rule has_integral_spike_interior[where f="\<lambda>x. 0"])
    1.85 -      unfolding g_def interior_cbox
    1.86 -      apply auto
    1.87 -      done
    1.88 +      using has_integral_spike_interior[where f="\<lambda>x. 0"]
    1.89 +      by (metis (no_types, lifting) disjoint_iff_not_equal g_def has_integral_0_eq interior_cbox)
    1.90      then show "(if g integrable_on x then Some (integral x g) else None) = Some 0"
    1.91        by auto
    1.92    qed
    1.93 @@ -4650,11 +4643,13 @@
    1.94        done
    1.95    }
    1.96    assume "\<exists>a b. s = cbox a b"
    1.97 -  then guess a b by (elim exE) note s=this
    1.98 -  from bounded_cbox[of a b, unfolded bounded_pos] guess B ..
    1.99 -  note B = conjunctD2[OF this,rule_format] show ?thesis
   1.100 -    apply safe
   1.101 -  proof -
   1.102 +  then obtain a b where s: "s = cbox a b"
   1.103 +    by blast
   1.104 +  from bounded_cbox[of a b, unfolded bounded_pos] 
   1.105 +  obtain B where " 0 < B" and B: "\<And>x. x \<in> cbox a b \<Longrightarrow> norm x \<le> B"
   1.106 +    by blast
   1.107 +  show ?thesis
   1.108 +  proof safe
   1.109      fix e :: real
   1.110      assume ?l and "e > 0"
   1.111      show "?r e"
   1.112 @@ -4671,12 +4666,12 @@
   1.113          apply (rule has_integral_restrict_closed_subinterval)
   1.114          apply (rule \<open>?l\<close>[unfolded s])
   1.115          apply safe
   1.116 -        apply (drule B(2)[rule_format])
   1.117 +        apply (drule B[rule_format])
   1.118          unfolding subset_eq
   1.119          apply (erule_tac x=x in ballE)
   1.120          apply (auto simp add: dist_norm)
   1.121          done
   1.122 -    qed (insert B \<open>e>0\<close>, auto)
   1.123 +    qed (insert \<open>B>0\<close> \<open>e>0\<close>, auto)
   1.124    next
   1.125      assume as: "\<forall>e>0. ?r e"
   1.126      from this[rule_format,OF zero_less_one] guess C..note C=conjunctD2[OF this,rule_format]
   1.127 @@ -4684,7 +4679,7 @@
   1.128      define d :: 'n where "d = (\<Sum>i\<in>Basis. max B C *\<^sub>R i)"
   1.129      have c_d: "cbox a b \<subseteq> cbox c d"
   1.130        apply safe
   1.131 -      apply (drule B(2))
   1.132 +      apply (drule B)
   1.133        unfolding mem_box
   1.134      proof
   1.135        fix x i
   1.136 @@ -4720,7 +4715,7 @@
   1.137        define d :: 'n where "d = (\<Sum>i\<in>Basis. max B C *\<^sub>R i)"
   1.138        have c_d: "cbox a b \<subseteq> cbox c d"
   1.139          apply safe
   1.140 -        apply (drule B(2))
   1.141 +        apply (drule B)
   1.142          unfolding mem_box
   1.143        proof
   1.144          fix x i :: 'n
   1.145 @@ -5029,75 +5024,55 @@
   1.146  
   1.147  lemma has_integral_alt':
   1.148    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   1.149 -  shows "(f has_integral i) s \<longleftrightarrow> (\<forall>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on cbox a b) \<and>
   1.150 -    (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
   1.151 -      norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0) - i) < e)"
   1.152 +  shows "(f has_integral i) s \<longleftrightarrow> 
   1.153 +          (\<forall>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on cbox a b) \<and>
   1.154 +          (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
   1.155 +            norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0) - i) < e)"
   1.156    (is "?l = ?r")
   1.157  proof
   1.158 -  assume ?r
   1.159 +  assume rhs: ?r
   1.160    show ?l
   1.161 -    apply (subst has_integral')
   1.162 -    apply safe
   1.163 -  proof goal_cases
   1.164 -    case (1 e)
   1.165 -    from \<open>?r\<close>[THEN conjunct2,rule_format,OF this] guess B..note B=conjunctD2[OF this]
   1.166 -    show ?case
   1.167 -      apply rule
   1.168 -      apply rule
   1.169 -      apply (rule B)
   1.170 -      apply safe
   1.171 -      apply (rule_tac x="integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0)" in exI)
   1.172 -      apply (drule B(2)[rule_format])
   1.173 -      using integrable_integral[OF \<open>?r\<close>[THEN conjunct1,rule_format]]
   1.174 -      apply auto
   1.175 -      done
   1.176 +  proof (subst has_integral', intro allI impI)
   1.177 +    fix e::real
   1.178 +    assume "e > 0"
   1.179 +    from rhs[THEN conjunct2,rule_format,OF this] 
   1.180 +    show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
   1.181 +                   (\<exists>z. ((\<lambda>x. if x \<in> s then f x else 0) has_integral z)
   1.182 +                         (cbox a b) \<and> norm (z - i) < e)"
   1.183 +      apply (rule ex_forward)
   1.184 +      using rhs by blast
   1.185    qed
   1.186  next
   1.187 -  assume ?l note as = this[unfolded has_integral'[of f],rule_format]
   1.188 +  let ?\<Phi> = "\<lambda>e a b. \<exists>z. ((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b) \<and> norm (z - i) < e"
   1.189 +  assume ?l 
   1.190 +  then have lhs: "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow> ?\<Phi> e a b" if "e > 0" for e
   1.191 +    using that has_integral'[of f] by auto
   1.192    let ?f = "\<lambda>x. if x \<in> s then f x else 0"
   1.193    show ?r
   1.194 -  proof safe
   1.195 +  proof (intro conjI allI impI)
   1.196      fix a b :: 'n
   1.197 -    from as[OF zero_less_one] guess B..note B=conjunctD2[OF this,rule_format]
   1.198 +    from lhs[OF zero_less_one]
   1.199 +    obtain B where "0 < B" and B: "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow> ?\<Phi> 1 a b"
   1.200 +      by blast
   1.201      let ?a = "\<Sum>i\<in>Basis. min (a\<bullet>i) (-B) *\<^sub>R i::'n"
   1.202      let ?b = "\<Sum>i\<in>Basis. max (b\<bullet>i) B *\<^sub>R i::'n"
   1.203      show "?f integrable_on cbox a b"
   1.204      proof (rule integrable_subinterval[of _ ?a ?b])
   1.205 -      have "ball 0 B \<subseteq> cbox ?a ?b"
   1.206 -        apply (rule subsetI)
   1.207 -        unfolding mem_ball mem_box dist_norm
   1.208 -      proof (rule, goal_cases)
   1.209 -        case (1 x i)
   1.210 -        then show ?case using Basis_le_norm[of i x]
   1.211 -          by (auto simp add:field_simps)
   1.212 -      qed
   1.213 -      from B(2)[OF this] guess z..note conjunct1[OF this]
   1.214 +      have "?a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> ?b \<bullet> i" if "norm (0 - x) < B" "i \<in> Basis" for x i
   1.215 +        using Basis_le_norm[of i x] that by (auto simp add:field_simps)
   1.216 +      then have "ball 0 B \<subseteq> cbox ?a ?b"
   1.217 +        by (auto simp: mem_box dist_norm)
   1.218        then show "?f integrable_on cbox ?a ?b"
   1.219 -        unfolding integrable_on_def by auto
   1.220 +        unfolding integrable_on_def using B by blast
   1.221        show "cbox a b \<subseteq> cbox ?a ?b"
   1.222 -        apply safe
   1.223 -        unfolding mem_box
   1.224 -        apply rule
   1.225 -        apply (erule_tac x=i in ballE)
   1.226 -        apply auto
   1.227 -        done
   1.228 +        by (force simp: mem_box)
   1.229      qed
   1.230 -
   1.231 +  
   1.232      fix e :: real
   1.233      assume "e > 0"
   1.234 -    from as[OF this] guess B..note B=conjunctD2[OF this,rule_format]
   1.235 -    show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
   1.236 +    with lhs show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
   1.237        norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
   1.238 -      apply rule
   1.239 -      apply rule
   1.240 -      apply (rule B)
   1.241 -      apply safe
   1.242 -    proof goal_cases
   1.243 -      case 1
   1.244 -      from B(2)[OF this] guess z..note z=conjunctD2[OF this]
   1.245 -      from integral_unique[OF this(1)] show ?case
   1.246 -        using z(2) by auto
   1.247 -    qed
   1.248 +      by (metis (no_types, lifting) has_integral_integrable_integral)
   1.249    qed
   1.250  qed
   1.251  
   1.252 @@ -5695,8 +5670,7 @@
   1.253      and p: "p tagged_partial_division_of (cbox a b)" "d fine p"
   1.254    shows "norm (sum (\<lambda>(x,K). content K *\<^sub>R f x - integral K f) p) \<le> e"
   1.255    (is "?x \<le> e")
   1.256 -proof -
   1.257 -  { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" then show ?thesis by (blast intro: field_le_epsilon) }
   1.258 +proof (rule field_le_epsilon)
   1.259    fix k :: real
   1.260    assume k: "k > 0"
   1.261    note p' = tagged_partial_division_ofD[OF p(1)]
   1.262 @@ -6365,7 +6339,7 @@
   1.263      and le_g: "\<forall>x\<in>S. norm (f x) \<le> g x"
   1.264    shows "norm (integral S f) \<le> integral S g"
   1.265  proof -
   1.266 -  have norm: "norm \<eta> < y + e"
   1.267 +  have norm: "norm \<eta> \<le> y + e"
   1.268      if "norm \<zeta> \<le> x" and "\<bar>x - y\<bar> < e/2" and "norm (\<zeta> - \<eta>) < e/2"
   1.269      for e x y and \<zeta> \<eta> :: 'a
   1.270    proof -
   1.271 @@ -6374,14 +6348,14 @@
   1.272      moreover have "x \<le> y + e/2"
   1.273        using that(2) by linarith
   1.274      ultimately show ?thesis
   1.275 -      using that(1) le_less_trans[OF norm_triangle_sub[of \<eta> \<zeta>]] by auto
   1.276 +      using that(1) le_less_trans[OF norm_triangle_sub[of \<eta> \<zeta>]] by (auto simp: less_imp_le)
   1.277    qed
   1.278    have lem: "norm (integral(cbox a b) f) \<le> integral (cbox a b) g"
   1.279      if f: "f integrable_on cbox a b"
   1.280      and g: "g integrable_on cbox a b"
   1.281      and nle: "\<And>x. x \<in> cbox a b \<Longrightarrow> norm (f x) \<le> g x"
   1.282      for f :: "'n \<Rightarrow> 'a" and g a b
   1.283 -  proof (rule eps_leI)
   1.284 +  proof (rule field_le_epsilon)
   1.285      fix e :: real
   1.286      assume "e > 0"
   1.287      then have e: "e/2 > 0"
   1.288 @@ -6404,7 +6378,7 @@
   1.289        by metis
   1.290      have "\<gamma> fine \<D>" "\<delta> fine \<D>"
   1.291        using fine_Int p(2) by blast+
   1.292 -    show "norm (integral (cbox a b) f) < integral (cbox a b) g + e"
   1.293 +    show "norm (integral (cbox a b) f) \<le> integral (cbox a b) g + e"
   1.294      proof (rule norm)
   1.295        have "norm (content K *\<^sub>R f x) \<le> content K *\<^sub>R g x" if  "(x, K) \<in> \<D>" for x K
   1.296        proof-
   1.297 @@ -6426,7 +6400,7 @@
   1.298      qed
   1.299    qed
   1.300    show ?thesis
   1.301 -  proof (rule eps_leI)
   1.302 +  proof (rule field_le_epsilon)
   1.303      fix e :: real
   1.304      assume "e > 0"
   1.305      then have e: "e/2 > 0"
   1.306 @@ -6453,7 +6427,7 @@
   1.307        using ab by auto
   1.308      with Bg obtain w where int_gw: "(?g has_integral w) (cbox a b)" and w: "norm (w - integral S g) < e/2"
   1.309        by meson
   1.310 -    show "norm (integral S f) < integral S g + e"
   1.311 +    show "norm (integral S f) \<le> integral S g + e"
   1.312      proof (rule norm)
   1.313        show "norm (integral (cbox a b) ?f) \<le> integral (cbox a b) ?g"
   1.314          by (simp add: le_g lem[OF f g, of a b])
     2.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Aug 24 12:45:46 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Aug 24 17:15:53 2017 +0100
     2.3 @@ -1457,10 +1457,6 @@
     2.4    shows "abs (x - x') < e"
     2.5    using assms by linarith
     2.6  
     2.7 -lemma eps_leI: 
     2.8 -  assumes "(\<And>e::'a::linordered_idom. 0 < e \<Longrightarrow> x < y + e)" shows "x \<le> y"
     2.9 -  by (metis add_diff_eq assms diff_diff_add diff_gt_0_iff_gt linorder_not_less order_less_irrefl)
    2.10 -
    2.11  lemma sum_clauses:
    2.12    shows "sum f {} = 0"
    2.13      and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"