src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 65036 ab7e11730ad8
parent 64911 f0e07600de47
child 65204 d23eded35a33
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Feb 19 11:58:51 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Feb 21 15:04:01 2017 +0000
     1.3 @@ -9,10 +9,7 @@
     1.4    Lebesgue_Measure Tagged_Division
     1.5  begin
     1.6  
     1.7 -(* BEGIN MOVE *)
     1.8 -lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)"
     1.9 -  by (simp add: norm_minus_eqI)
    1.10 -
    1.11 +(* try instead structured proofs below *)
    1.12  lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
    1.13    \<Longrightarrow> norm(y - x) \<le> e"
    1.14    using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
    1.15 @@ -7696,10 +7693,12 @@
    1.16          assume xuvwz: "x1 \<in> cbox u v" "x2 \<in> cbox w z"
    1.17          then have x: "x1 \<in> cbox a b" "x2 \<in> cbox c d"
    1.18            using uwvz_sub by auto
    1.19 -        have "norm (x1 - t1, x2 - t2) < k"
    1.20 +        have "norm (x1 - t1, x2 - t2) = norm (t1 - x1, t2 - x2)"
    1.21 +          by (simp add: norm_Pair norm_minus_commute)
    1.22 +        also have "norm (t1 - x1, t2 - x2) < k"
    1.23            using xuvwz ls uwvz_sub unfolding ball_def
    1.24 -          by (force simp add: cbox_Pair_eq dist_norm norm_minus2)
    1.25 -        then have "norm (f (x1,x2) - f (t1,t2)) \<le> e / content ?CBOX / 2"
    1.26 +          by (force simp add: cbox_Pair_eq dist_norm )
    1.27 +        finally have "norm (f (x1,x2) - f (t1,t2)) \<le> e / content ?CBOX / 2"
    1.28            using nf [OF t x]  by simp
    1.29        } note nf' = this
    1.30        have f_int_uwvz: "f integrable_on cbox (u,w) (v,z)"
    1.31 @@ -7852,7 +7851,7 @@
    1.32        finally show ?thesis .
    1.33      qed (insert a, simp_all add: integral_f)
    1.34      thus "bounded {integral {c..} (f k) |k. True}"
    1.35 -      by (intro bounded_realI[of _ "exp (-a*c)/a"]) auto
    1.36 +      by (intro boundedI[of _ "exp (-a*c)/a"]) auto
    1.37    qed (auto simp: f_def)
    1.38  
    1.39    from eventually_gt_at_top[of "nat \<lceil>c\<rceil>"] have "eventually (\<lambda>k. of_nat k > c) sequentially"
    1.40 @@ -7945,7 +7944,7 @@
    1.41        finally have "abs (F k) \<le>  c powr (a + 1) / (a + 1)" .
    1.42      }
    1.43      thus "bounded {integral {0..c} (f k) |k. True}"
    1.44 -      by (intro bounded_realI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f)
    1.45 +      by (intro boundedI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f)
    1.46    qed
    1.47  
    1.48    from False c have "c > 0" by simp