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.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.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.48    from False c have "c > 0" by simp