src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

 theory Henstock_Kurzweil_Integration
 imports
   Lebesgue_Measure Tagged_Division
 begin
 
-(* BEGIN MOVE *)
-lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)"
-  by (simp add: norm_minus_eqI)
-
+(* try instead structured proofs below *)
 lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
   \<Longrightarrow> norm(y - x) \<le> e"
   using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
   by (simp add: add_diff_add)
 

         using fine by (simp add: fine_def Ball_def)
       { fix x1 x2
         assume xuvwz: "x1 \<in> cbox u v" "x2 \<in> cbox w z"
         then have x: "x1 \<in> cbox a b" "x2 \<in> cbox c d"
           using uwvz_sub by auto
-        have "norm (x1 - t1, x2 - t2) < k"
+        have "norm (x1 - t1, x2 - t2) = norm (t1 - x1, t2 - x2)"
+          by (simp add: norm_Pair norm_minus_commute)
+        also have "norm (t1 - x1, t2 - x2) < k"
           using xuvwz ls uwvz_sub unfolding ball_def
-          by (force simp add: cbox_Pair_eq dist_norm norm_minus2)
-        then have "norm (f (x1,x2) - f (t1,t2)) \<le> e / content ?CBOX / 2"
+          by (force simp add: cbox_Pair_eq dist_norm )
+        finally have "norm (f (x1,x2) - f (t1,t2)) \<le> e / content ?CBOX / 2"
           using nf [OF t x]  by simp
       } note nf' = this
       have f_int_uwvz: "f integrable_on cbox (u,w) (v,z)"
         using f_int_acbd uwvz_sub integrable_on_subcbox by blast
       have f_int_uv: "\<And>x. x \<in> cbox u v \<Longrightarrow> (\<lambda>y. f (x,y)) integrable_on cbox w z"

         using False a by (intro abs_of_nonneg) (simp_all add: field_simps)
       also have "\<dots> \<le> exp (- a * c) / a" using a by simp
       finally show ?thesis .
     qed (insert a, simp_all add: integral_f)
     thus "bounded {integral {c..} (f k) |k. True}"
-      by (intro bounded_realI[of _ "exp (-a*c)/a"]) auto
+      by (intro boundedI[of _ "exp (-a*c)/a"]) auto
   qed (auto simp: f_def)
 
   from eventually_gt_at_top[of "nat \<lceil>c\<rceil>"] have "eventually (\<lambda>k. of_nat k > c) sequentially"
     by eventually_elim linarith
   hence "eventually (\<lambda>k. exp (-a*c)/a - exp (-a * of_nat k)/a = integral {c..} (f k)) sequentially"

         by (auto simp: F_def divide_simps simp del: of_nat_Suc intro!: powr_mono2)
       hence "F k = abs (F k)" by simp
       finally have "abs (F k) \<le>  c powr (a + 1) / (a + 1)" .
     }
     thus "bounded {integral {0..c} (f k) |k. True}"
-      by (intro bounded_realI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f)
+      by (intro boundedI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f)
   qed
 
   from False c have "c > 0" by simp
   from order_tendstoD(2)[OF LIMSEQ_inverse_real_of_nat this]
     have "eventually (\<lambda>k. c powr (a + 1) / (a + 1) - inverse (real (Suc k)) powr (a+1) / (a+1) =