author wenzelm Sun, 13 Sep 2015 16:50:12 +0200 changeset 61165 8020249565fb parent 61164 2a03ae772c60 child 61166 5976fe402824
tuned proofs;
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Sep 13 14:44:03 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Sep 13 16:50:12 2015 +0200
@@ -1191,8 +1191,9 @@
have lem1: "\<forall>e>0. \<exists>d>0. \<forall>z.
norm (z - y) < d \<longrightarrow> norm (g z - g y - g'(z - y)) \<le> e * norm (g z - g y)"
proof (rule, rule)
-    case goal1
-    have *: "e / C > 0" using \<open>e > 0\<close> C(1) by auto
+    fix e :: real
+    assume "e > 0"
+    with C(1) have *: "e / C > 0" by auto
obtain d0 where d0:
"0 < d0"
"\<forall>ya. norm (ya - g y) < d0 \<longrightarrow> norm (f ya - f (g y) - f' (ya - g y)) \<le> e / C * norm (ya - g y)"
@@ -1213,7 +1214,7 @@
using assms(6) by blast
obtain d where d: "0 < d" "d < d1" "d < d2"
using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
-    then show ?case
+    then show "\<exists>d>0. \<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
apply (rule_tac x=d in exI)
apply rule
defer
@@ -1257,14 +1258,13 @@
def B \<equiv> "C * 2"
have "B > 0"
unfolding B_def using C by auto
-  have lem2: "\<forall>z. norm(z - y) < d \<longrightarrow> norm (g z - g y) \<le> B * norm (z - y)"
-  proof (rule, rule)
-    case goal1
+  have lem2: "norm (g z - g y) \<le> B * norm (z - y)" if z: "norm(z - y) < d" for z
+  proof -
have "norm (g z - g y) \<le> norm(g' (z - y)) + norm ((g z - g y) - g'(z - y))"
by (rule norm_triangle_sub)
also have "\<dots> \<le> norm (g' (z - y)) + 1 / 2 * norm (g z - g y)"
-      using d and goal1
+      using d and z
apply auto
done
also have "\<dots> \<le> norm (z - y) * C + 1 / 2 * norm (g z - g y)"
@@ -1272,7 +1272,7 @@
using C
apply auto
done
-    finally show ?case
+    finally show "norm (g z - g y) \<le> B * norm (z - y)"
unfolding B_def
by (auto simp add: field_simps)
qed
@@ -1283,15 +1283,16 @@
apply rule
apply rule
proof -
-    case goal1
-    hence *: "e / B >0" by (metis \<open>0 < B\<close> divide_pos_pos)
+    fix e :: real
+    assume "e > 0"
+    then have *: "e / B > 0" by (metis \<open>B > 0\<close> divide_pos_pos)
obtain d' where d':
"0 < d'"
"\<forall>z. norm (z - y) < d' \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
using lem1 * by blast
obtain k where k: "0 < k" "k < d" "k < d'"
using real_lbound_gt_zero[OF d(1) d'(1)] by blast
-    show ?case
+    show "\<exists>d>0. \<forall>ya. norm (ya - y) < d \<longrightarrow> norm (g ya - g y - g' (ya - y)) \<le> e * norm (ya - y)"
apply (rule_tac x=k in exI)
apply auto
proof -
@@ -1301,7 +1302,7 @@
using d' k by auto
also have "\<dots> \<le> e * norm (z - y)"
unfolding times_divide_eq_left pos_divide_le_eq[OF \<open>B>0\<close>]
-        using lem2[THEN spec[where x=z]]
+        using lem2[of z]
using k as using \<open>e > 0\<close>
by (auto simp add: field_simps)
finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (z - y)"
@@ -1650,7 +1651,8 @@
apply rule
apply rule
proof -
-      case goal1
+      fix y
+      assume "0 < dist y (f x) \<and> dist y (f x) < d"
then have "g y \<in> g ` f ` (ball x e \<inter> s)"
using d(2)[unfolded subset_eq,THEN bspec[where x=y]]
by (auto simp add: dist_commute)
@@ -1667,13 +1669,12 @@
using interior_open[OF assms(1)] and \<open>x \<in> s\<close>
apply auto
done
-  moreover have "\<And>y. y \<in> interior (f ` s) \<Longrightarrow> f (g y) = y"
+  moreover have "f (g y) = y" if "y \<in> interior (f ` s)" for y
proof -
-    case goal1
-    then have "y \<in> f ` s"
+    from that have "y \<in> f ` s"
using interior_subset by auto
then obtain z where "z \<in> s" "y = f z" unfolding image_iff ..
-    then show ?case
+    then show ?thesis
using assms(4) by auto
qed
ultimately show ?thesis using assms
@@ -1882,11 +1883,13 @@
shows "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s.
norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
proof (rule, rule)
-  case goal1 have *: "2 * (1/2* e) = e" "1/2 * e >0"
-    using \<open>e > 0\<close> by auto
+  fix e :: real
+  assume "e > 0"
+  then have *: "2 * (1/2* e) = e" "1/2 * e >0"
+    by auto
obtain N where "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> 1 / 2 * e * norm h"
using assms(3) *(2) by blast
-  then show ?case
+  then show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
apply (rule_tac x=N in exI)
apply (rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *])
using assms \<open>e > 0\<close>
@@ -2060,9 +2063,10 @@
qed
show "\<forall>e>0. eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within s)"
proof (rule, rule)
-      case goal1
-      have *: "e / 3 > 0"
-        using goal1 by auto
+      fix e :: real
+      assume "e > 0"
+      then have *: "e / 3 > 0"
+        by auto
obtain N1 where N1: "\<forall>n\<ge>N1. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e / 3 * norm h"
using assms(3) * by blast
obtain N2 where
@@ -2073,7 +2077,7 @@
using assms(2)[unfolded has_derivative_within_alt2] and \<open>x \<in> s\<close> and * by fast
moreover have "eventually (\<lambda>y. y \<in> s) (at x within s)"
unfolding eventually_at by (fast intro: zero_less_one)
-      ultimately show ?case
+      ultimately show "\<forall>\<^sub>F y in at x within s. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
proof (rule eventually_elim2)
fix y
assume "y \<in> s"
@@ -2150,15 +2154,20 @@
using reals_Archimedean[OF \<open>e>0\<close>] ..
show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
apply (rule_tac x=N in exI)
-    proof rule+
-      case goal1
+      apply rule
+      apply rule
+      apply rule
+      apply rule
+    proof -
+      fix n x h
+      assume n: "N \<le> n" and x: "x \<in> s"
have *: "inverse (real (Suc n)) \<le> e"
apply (rule order_trans[OF _ N[THEN less_imp_le]])
-        using goal1(1)
+        using n
apply (auto simp add: field_simps)
done
-      show ?case
-        using f[rule_format,THEN conjunct2,OF goal1(2), of n, THEN spec[where x=h]]
+      show "norm (f' n x h - g' x h) \<le> e * norm h"
+        using f[rule_format,THEN conjunct2, OF x, of n, THEN spec[where x=h]]
apply (rule order_trans)
using N *
apply (cases "h = 0")
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 13 14:44:03 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 13 16:50:12 2015 +0200
@@ -175,9 +175,8 @@
qed
have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
unfolding subset_eq
-    apply rule
-  proof -
-    case goal1
+  proof (rule, goals)
+    case (1 x)
then obtain y :: "real^2" where y:
"y \<in> cbox (- 1) 1"
"x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x \$ 1)) w - (g \<circ> (\<lambda>x. x \$ 2)) w)) y"
@@ -198,8 +197,9 @@
apply -
apply rule
proof -
-      case goal1
-      then show ?case
+      fix i
+      assume "max \<bar>x \$ 1\<bar> \<bar>x \$ 2\<bar> = 1"
+      then show "(- 1) \$ i \<le> x \$ i \<and> x \$ i \<le> 1 \$ i"
apply (cases "i = 1")
defer
apply (drule 21)
@@ -834,9 +834,8 @@
z \<in> closed_segment (pathfinish g) (vector [pathfinish g \$ 1, a \$ 2 - 1])) \<or>
z \<in> closed_segment (vector [pathfinish g \$ 1, a \$ 2 - 1]) (vector [b \$ 1 + 1, a \$ 2 - 1])) \<or>
z \<in> closed_segment (vector [b \$ 1 + 1, a \$ 2 - 1]) (vector [b \$ 1 + 1, b \$ 2 + 3]) \<Longrightarrow> False"
-      apply (simp only: segment_vertical segment_horizontal vector_2)
-    proof -
-      case goal1 note as=this
+    proof (simp only: segment_vertical segment_horizontal vector_2, goals)
+      case as: 1
have "pathfinish f \<in> cbox a b"
using assms(3) pathfinish_in_path_image[of f] by auto
then have "1 + b \$ 1 \<le> pathfinish f \$ 1 \<Longrightarrow> False"
@@ -855,7 +854,7 @@
using as(2) using assms ab
by (auto simp add: field_simps)
ultimately have *: "z\$2 = a\$2 - 2"
-        using goal1(1)
+        using as(1)
by auto
have "z\$1 \<noteq> pathfinish g\$1"
using as(2)
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Sep 13 14:44:03 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Sep 13 16:50:12 2015 +0200
@@ -15,7 +15,7 @@
shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2 bdd_aboveI)

-lemma cInf_abs_ge:
+lemma cInf_abs_ge:
fixes S :: "real set"
shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
using cSup_abs_le [of "uminus ` S"]
@@ -248,156 +248,153 @@
have lem1: "\<And>x e s U. ball x e \<subseteq> s \<inter> interior U \<longleftrightarrow> ball x e \<subseteq> s \<inter> U"
using interior_subset
by auto (meson Topology_Euclidean_Space.open_ball contra_subsetD interior_maximal mem_ball)
-  have "\<And>f. finite f \<Longrightarrow> \<forall>t\<in>f. \<exists>a b. t = cbox a b \<Longrightarrow>
-    \<exists>x. x \<in> s \<inter> interior (\<Union>f) \<Longrightarrow> \<exists>t\<in>f. \<exists>x. \<exists>e>0. ball x e \<subseteq> s \<inter> t"
-  proof -
-    case goal1
-    then show ?case
-    proof (induct rule: finite_induct)
-      case empty
-      obtain x where "x \<in> s \<inter> interior (\<Union>{})"
-        using empty(2) ..
-      then have False
-        unfolding Union_empty interior_empty by auto
-      then show ?case by auto
+  have "\<exists>t\<in>f. \<exists>x. \<exists>e>0. ball x e \<subseteq> s \<inter> t"
+    if "finite f" and "\<forall>t\<in>f. \<exists>a b. t = cbox a b" and "\<exists>x. x \<in> s \<inter> interior (\<Union>f)" for f
+    using that
+  proof (induct rule: finite_induct)
+    case empty
+    obtain x where "x \<in> s \<inter> interior (\<Union>{})"
+      using empty(2) ..
+    then have False
+      unfolding Union_empty interior_empty by auto
+    then show ?case by auto
+  next
+    case (insert i f)
+    obtain x where x: "x \<in> s \<inter> interior (\<Union>insert i f)"
+      using insert(5) ..
+    then obtain e where e: "0 < e \<and> ball x e \<subseteq> s \<inter> interior (\<Union>insert i f)"
+      unfolding open_contains_ball_eq[OF open_Int[OF assms(2) open_interior], rule_format] ..
+    obtain a where "\<exists>b. i = cbox a b"
+      using insert(4)[rule_format,OF insertI1] ..
+    then obtain b where ab: "i = cbox a b" ..
+    show ?case
+    proof (cases "x \<in> i")
+      case False
+      then have "x \<in> UNIV - cbox a b"
+        unfolding ab by auto
+      then obtain d where "0 < d \<and> ball x d \<subseteq> UNIV - cbox a b"
+        unfolding open_contains_ball_eq[OF open_Diff[OF open_UNIV closed_cbox],rule_format] ..
+      then have "0 < d" "ball x (min d e) \<subseteq> UNIV - i"
+        unfolding ab ball_min_Int by auto
+      then have "ball x (min d e) \<subseteq> s \<inter> interior (\<Union>f)"
+        using e unfolding lem1 unfolding  ball_min_Int by auto
+      then have "x \<in> s \<inter> interior (\<Union>f)" using \<open>d>0\<close> e by auto
+      then have "\<exists>t\<in>f. \<exists>x e. 0 < e \<and> ball x e \<subseteq> s \<inter> t"
+        using insert.hyps(3) insert.prems(1) by blast
+      then show ?thesis by auto
next
-      case (insert i f)
-      obtain x where x: "x \<in> s \<inter> interior (\<Union>insert i f)"
-        using insert(5) ..
-      then obtain e where e: "0 < e \<and> ball x e \<subseteq> s \<inter> interior (\<Union>insert i f)"
-        unfolding open_contains_ball_eq[OF open_Int[OF assms(2) open_interior], rule_format] ..
-      obtain a where "\<exists>b. i = cbox a b"
-        using insert(4)[rule_format,OF insertI1] ..
-      then obtain b where ab: "i = cbox a b" ..
-      show ?case
-      proof (cases "x \<in> i")
+      case True show ?thesis
+      proof (cases "x\<in>box a b")
+        case True
+        then obtain d where "0 < d \<and> ball x d \<subseteq> box a b"
+          unfolding open_contains_ball_eq[OF open_box,rule_format] ..
+        then show ?thesis
+          apply (rule_tac x=i in bexI, rule_tac x=x in exI, rule_tac x="min d e" in exI)
+          unfolding ab
+          using box_subset_cbox[of a b] and e
+          apply fastforce+
+          done
+      next
case False
-        then have "x \<in> UNIV - cbox a b"
-          unfolding ab by auto
-        then obtain d where "0 < d \<and> ball x d \<subseteq> UNIV - cbox a b"
-          unfolding open_contains_ball_eq[OF open_Diff[OF open_UNIV closed_cbox],rule_format] ..
-        then have "0 < d" "ball x (min d e) \<subseteq> UNIV - i"
-          unfolding ab ball_min_Int by auto
-        then have "ball x (min d e) \<subseteq> s \<inter> interior (\<Union>f)"
-          using e unfolding lem1 unfolding  ball_min_Int by auto
-        then have "x \<in> s \<inter> interior (\<Union>f)" using \<open>d>0\<close> e by auto
-        then have "\<exists>t\<in>f. \<exists>x e. 0 < e \<and> ball x e \<subseteq> s \<inter> t"
-          using insert.hyps(3) insert.prems(1) by blast
-        then show ?thesis by auto
-      next
-        case True show ?thesis
-        proof (cases "x\<in>box a b")
-          case True
-          then obtain d where "0 < d \<and> ball x d \<subseteq> box a b"
-            unfolding open_contains_ball_eq[OF open_box,rule_format] ..
-          then show ?thesis
-            apply (rule_tac x=i in bexI, rule_tac x=x in exI, rule_tac x="min d e" in exI)
-            unfolding ab
-            using box_subset_cbox[of a b] and e
-            apply fastforce+
+        then obtain k where "x\<bullet>k \<le> a\<bullet>k \<or> x\<bullet>k \<ge> b\<bullet>k" and k: "k \<in> Basis"
+          unfolding mem_box by (auto simp add: not_less)
+        then have "x\<bullet>k = a\<bullet>k \<or> x\<bullet>k = b\<bullet>k"
+          using True unfolding ab and mem_box
+            apply (erule_tac x = k in ballE)
+            apply auto
done
-        next
-          case False
-          then obtain k where "x\<bullet>k \<le> a\<bullet>k \<or> x\<bullet>k \<ge> b\<bullet>k" and k: "k \<in> Basis"
-            unfolding mem_box by (auto simp add: not_less)
-          then have "x\<bullet>k = a\<bullet>k \<or> x\<bullet>k = b\<bullet>k"
-            using True unfolding ab and mem_box
-              apply (erule_tac x = k in ballE)
+        then have "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)"
+        proof (rule disjE)
+          let ?z = "x - (e/2) *\<^sub>R k"
+          assume as: "x\<bullet>k = a\<bullet>k"
+          have "ball ?z (e / 2) \<inter> i = {}"
+          proof (clarsimp simp only: all_not_in_conv [symmetric])
+            fix y
+            assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
+            then have "dist ?z y < e/2" by auto
+            then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
+              using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
+            then have "y\<bullet>k < a\<bullet>k"
+              using e k
+              by (auto simp add: field_simps abs_less_iff as inner_simps)
+            then have "y \<notin> i"
+              unfolding ab mem_box by (auto intro!: bexI[OF _ k])
+            then show False using yi by auto
+          qed
+          moreover
+          have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
+            apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
+          proof
+            fix y
+            assume as: "y \<in> ball ?z (e/2)"
+            have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R k)"
+              apply (rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R k"])
+              unfolding norm_scaleR norm_Basis[OF k]
apply auto
done
-          then have "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)"
-          proof (rule disjE)
-            let ?z = "x - (e/2) *\<^sub>R k"
-            assume as: "x\<bullet>k = a\<bullet>k"
-            have "ball ?z (e / 2) \<inter> i = {}"
-            proof (clarsimp simp only: all_not_in_conv [symmetric])
-              fix y
-              assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
-              then have "dist ?z y < e/2" by auto
-              then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
-                using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
-              then have "y\<bullet>k < a\<bullet>k"
-                using e k
-                by (auto simp add: field_simps abs_less_iff as inner_simps)
-              then have "y \<notin> i"
-                unfolding ab mem_box by (auto intro!: bexI[OF _ k])
-              then show False using yi by auto
-            qed
-            moreover
-            have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
-              apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
-            proof
-              fix y
-              assume as: "y \<in> ball ?z (e/2)"
-              have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R k)"
-                apply (rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R k"])
-                unfolding norm_scaleR norm_Basis[OF k]
-                apply auto
-                done
-              also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
-                apply (rule add_strict_left_mono)
-                using as e
-                apply (auto simp add: field_simps dist_norm)
-                done
-              finally show "y \<in> ball x e"
-                unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
-            qed
-            ultimately show ?thesis
-              apply (rule_tac x="?z" in exI)
-              unfolding Union_insert
-              apply auto
+            also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
+              apply (rule add_strict_left_mono)
+              using as e
+              apply (auto simp add: field_simps dist_norm)
done
-          next
-            let ?z = "x + (e/2) *\<^sub>R k"
-            assume as: "x\<bullet>k = b\<bullet>k"
-            have "ball ?z (e / 2) \<inter> i = {}"
-            proof (clarsimp simp only: all_not_in_conv [symmetric])
-              fix y
-              assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
-              then have "dist ?z y < e/2"
-                by auto
-              then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
-                using Basis_le_norm[OF k, of "?z - y"]
-                unfolding dist_norm by auto
-              then have "y\<bullet>k > b\<bullet>k"
-                using e k
-                by (auto simp add:field_simps inner_simps inner_Basis as)
-              then have "y \<notin> i"
-                unfolding ab mem_box by (auto intro!: bexI[OF _ k])
-              then show False using yi by auto
-            qed
-            moreover
-            have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
-              apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
-            proof
-              fix y
-              assume as: "y\<in> ball ?z (e/2)"
-              have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y + (e / 2) *\<^sub>R k)"
-                apply (rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R k"])
-                unfolding norm_scaleR
-                apply (auto simp: k)
-                done
-              also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
-                apply (rule add_strict_left_mono)
-                using as unfolding mem_ball dist_norm
-                using e apply (auto simp add: field_simps)
-                done
-              finally show "y \<in> ball x e"
-                unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
-            qed
-            ultimately show ?thesis
-              apply (rule_tac x="?z" in exI)
-              unfolding Union_insert
-              apply auto
+            finally show "y \<in> ball x e"
+              unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
+          qed
+          ultimately show ?thesis
+            apply (rule_tac x="?z" in exI)
+            unfolding Union_insert
+            apply auto
+            done
+        next
+          let ?z = "x + (e/2) *\<^sub>R k"
+          assume as: "x\<bullet>k = b\<bullet>k"
+          have "ball ?z (e / 2) \<inter> i = {}"
+          proof (clarsimp simp only: all_not_in_conv [symmetric])
+            fix y
+            assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
+            then have "dist ?z y < e/2"
+              by auto
+            then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
+              using Basis_le_norm[OF k, of "?z - y"]
+              unfolding dist_norm by auto
+            then have "y\<bullet>k > b\<bullet>k"
+              using e k
+              by (auto simp add:field_simps inner_simps inner_Basis as)
+            then have "y \<notin> i"
+              unfolding ab mem_box by (auto intro!: bexI[OF _ k])
+            then show False using yi by auto
+          qed
+          moreover
+          have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
+            apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
+          proof
+            fix y
+            assume as: "y\<in> ball ?z (e/2)"
+            have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y + (e / 2) *\<^sub>R k)"
+              apply (rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R k"])
+              unfolding norm_scaleR
+              apply (auto simp: k)
done
+            also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
+              apply (rule add_strict_left_mono)
+              using as unfolding mem_ball dist_norm
+              using e apply (auto simp add: field_simps)
+              done
+            finally show "y \<in> ball x e"
+              unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
qed
-          then obtain x where "ball x (e / 2) \<subseteq> s \<inter> \<Union>f" ..
-          then have "x \<in> s \<inter> interior (\<Union>f)"
-            unfolding lem1[where U="\<Union>f", symmetric]
-            using centre_in_ball e by auto
-          then show ?thesis
-            using insert.hyps(3) insert.prems(1) by blast
+          ultimately show ?thesis
+            apply (rule_tac x="?z" in exI)
+            unfolding Union_insert
+            apply auto
+            done
qed
+        then obtain x where "ball x (e / 2) \<subseteq> s \<inter> \<Union>f" ..
+        then have "x \<in> s \<inter> interior (\<Union>f)"
+          unfolding lem1[where U="\<Union>f", symmetric]
+          using centre_in_ball e by auto
+        then show ?thesis
+          using insert.hyps(3) insert.prems(1) by blast
qed
qed
qed
@@ -1097,15 +1094,16 @@
note p = division_ofD[OF assms(1)]
have div_cbox: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q"
proof
-    case goal1
+    fix k
+    assume kp: "k \<in> p"
obtain c d where k: "k = cbox c d"
-      using p(4)[OF goal1] by blast
+      using p(4)[OF kp] by blast
have *: "cbox c d \<subseteq> cbox a b" "cbox c d \<noteq> {}"
-      using p(2,3)[OF goal1, unfolded k] using assms(2)
+      using p(2,3)[OF kp, unfolded k] using assms(2)
by (blast intro: order.trans)+
obtain q where "q division_of cbox a b" "cbox c d \<in> q"
by (rule partial_division_extend_1[OF *])
-    then show ?case
+    then show "\<exists>q. q division_of cbox a b \<and> k \<in> q"
unfolding k by auto
qed
obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
@@ -1275,9 +1273,10 @@
assume as: "p \<noteq> {}" "interior (cbox a b) \<noteq> {}" "cbox a b \<noteq> {}"
have "\<forall>k\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
proof
-      case goal1
-      from assm(4)[OF this] obtain c d where "k = cbox c d" by blast
-      then show ?case
+      fix k
+      assume kp: "k \<in> p"
+      from assm(4)[OF kp] obtain c d where "k = cbox c d" by blast
+      then show "\<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
by (meson as(3) division_union_intervals_exists)
qed
from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
@@ -1910,7 +1909,8 @@
(\<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}"
have "?A \<subseteq> ?B"
proof
-      case goal1
+      fix x
+      assume "x \<in> ?A"
then obtain c d
where x:  "x = cbox c d"
"\<And>i. i \<in> Basis \<Longrightarrow>
@@ -2034,15 +2034,14 @@
proof -
have "\<forall>x. \<exists>y. \<not> P (cbox (fst x) (snd x)) \<longrightarrow> (\<not> P (cbox (fst y) (snd y)) \<and>
(\<forall>i\<in>Basis. fst x\<bullet>i \<le> fst y\<bullet>i \<and> fst y\<bullet>i \<le> snd y\<bullet>i \<and> snd y\<bullet>i \<le> snd x\<bullet>i \<and>
-       2 * (snd y\<bullet>i - fst y\<bullet>i) \<le> snd x\<bullet>i - fst x\<bullet>i))"
+       2 * (snd y\<bullet>i - fst y\<bullet>i) \<le> snd x\<bullet>i - fst x\<bullet>i))" (is "\<forall>x. ?P x")
proof
-    case goal1
-    show ?case
-    proof -
-      presume "\<not> P (cbox (fst x) (snd x)) \<Longrightarrow> ?thesis"
-      then show ?thesis by (cases "P (cbox (fst x) (snd x))") auto
+    show "?P x" for x
+    proof (cases "P (cbox (fst x) (snd x))")
+      case True
+      then show ?thesis by auto
next
-      assume as: "\<not> P (cbox (fst x) (snd x))"
+      case as: False
obtain c d where "\<not> P (cbox c d)"
"\<forall>i\<in>Basis.
fst x \<bullet> i \<le> c \<bullet> i \<and>
@@ -2080,9 +2079,8 @@
proof -
show "A 0 = a" "B 0 = b"
unfolding ab_def by auto
-    case goal3
note S = ab_def funpow.simps o_def id_apply
-    show ?case
+    show "?P n" for n
proof (induct n)
case 0
then show ?case
@@ -2103,12 +2101,12 @@
qed
note AB = this(1-2) conjunctD2[OF this(3),rule_format]

-  have interv: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. \<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e"
+  have interv: "\<exists>n. \<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e"
+    if e: "0 < e" for e
proof -
-    case goal1
obtain n where n: "(\<Sum>i\<in>Basis. b \<bullet> i - a \<bullet> i) / e < 2 ^ n"
using real_arch_pow2[of "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] ..
-    show ?case
+    show ?thesis
proof (rule exI [where x=n], clarify)
fix x y
assume xy: "x\<in>cbox (A n) (B n)" "y\<in>cbox (A n) (B n)"
@@ -2125,8 +2123,7 @@
also have "\<dots> \<le> setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis / 2^n"
unfolding setsum_divide_distrib
proof (rule setsum_mono)
-        case goal1
-        then show ?case
+        show "B n \<bullet> i - A n \<bullet> i \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ n" if i: "i \<in> Basis" for i
proof (induct n)
case 0
then show ?case
@@ -2134,14 +2131,14 @@
next
case (Suc n)
have "B (Suc n) \<bullet> i - A (Suc n) \<bullet> i \<le> (B n \<bullet> i - A n \<bullet> i) / 2"
-            using AB(4)[of i n] using goal1 by auto
+            using AB(4)[of i n] using i by auto
also have "\<dots> \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ Suc n"
-            using Suc by (auto simp add:field_simps)
+            using Suc by (auto simp add: field_simps)
finally show ?case .
qed
qed
also have "\<dots> < e"
-        using n using goal1 by (auto simp add:field_simps)
+        using n using e by (auto simp add: field_simps)
finally show "dist x y < e" .
qed
qed
@@ -2240,25 +2237,27 @@
shows "k1 = k2"
proof (rule ccontr)
let ?e = "norm (k1 - k2) / 2"
-  assume as:"k1 \<noteq> k2"
+  assume as: "k1 \<noteq> k2"
then have e: "?e > 0"
by auto
-  have lem: "\<And>f::'n \<Rightarrow> 'a.  \<And>a b k1 k2.
-    (f has_integral k1) (cbox a b) \<Longrightarrow> (f has_integral k2) (cbox a b) \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> False"
+  have lem: False
+    if f_k1: "(f has_integral k1) (cbox a b)"
+    and f_k2: "(f has_integral k2) (cbox a b)"
+    and "k1 \<noteq> k2"
+    for f :: "'n \<Rightarrow> 'a" and a b k1 k2
proof -
-    case goal1
let ?e = "norm (k1 - k2) / 2"
-    from goal1(3) have e: "?e > 0" by auto
+    from \<open>k1 \<noteq> k2\<close> have e: "?e > 0" by auto
obtain d1 where d1:
"gauge d1"
"\<And>p. p tagged_division_of cbox a b \<Longrightarrow>
d1 fine p \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k1) < norm (k1 - k2) / 2"
-      by (rule has_integralD[OF goal1(1) e]) blast
+      by (rule has_integralD[OF f_k1 e]) blast
obtain d2 where d2:
"gauge d2"
"\<And>p. p tagged_division_of cbox a b \<Longrightarrow>
d2 fine p \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k2) < norm (k1 - k2) / 2"
-      by (rule has_integralD[OF goal1(2) e]) blast
+      by (rule has_integralD[OF f_k2 e]) blast
obtain p where p:
"p tagged_division_of cbox a b"
"(\<lambda>x. d1 x \<inter> d2 x) fine p"
@@ -2336,26 +2335,26 @@
fix a b e
fix f :: "'n \<Rightarrow> 'a"
assume as: "\<forall>x\<in>cbox a b. f x = 0" "0 < (e::real)"
-    have "\<And>p. p tagged_division_of cbox a b \<Longrightarrow> (\<lambda>x. ball x 1) fine p \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
+    have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
+      if p: "p tagged_division_of cbox a b" for p
proof -
-      case goal1
have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) = 0"
proof (rule setsum.neutral, rule)
fix x
assume x: "x \<in> p"
have "f (fst x) = 0"
-          using tagged_division_ofD(2-3)[OF goal1(1), of "fst x" "snd x"] using as x by auto
+          using tagged_division_ofD(2-3)[OF p, of "fst x" "snd x"] using as x by auto
then show "(\<lambda>(x, k). content k *\<^sub>R f x) x = 0"
apply (subst surjective_pairing[of x])
unfolding split_conv
apply auto
done
qed
-      then show ?case
+      then show ?thesis
using as by auto
qed
then show "\<exists>d. gauge d \<and>
-                   (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e)"
+        (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e)"
by auto
qed
{
@@ -2392,19 +2391,20 @@
by blast
have lem: "\<And>(f :: 'n \<Rightarrow> 'a) y a b.
(f has_integral y) (cbox a b) \<Longrightarrow> ((h o f) has_integral h y) (cbox a b)"
-  unfolding has_integral
-  proof clarify
-    case goal1
+    unfolding has_integral
+  proof (clarify, goals)
+    case (1 f y a b e)
from pos_bounded
obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
by blast
-    have "e / B > 0" using goal1(2) B by simp
+    have "e / B > 0" using 1(2) B by simp
then obtain g
where g: "gauge g"
"\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e / B"
-        using goal1(1) by auto
-    { fix p
+        using 1(1) by auto
+    {
+      fix p
assume as: "p tagged_division_of (cbox a b)" "g fine p"
have hc: "\<And>x k. h ((\<lambda>(x, k). content k *\<^sub>R f x) x) = (\<lambda>(x, k). h (content k *\<^sub>R f x)) x"
by auto
@@ -2441,18 +2441,19 @@
using has_integral_altD[OF assms(1) as *] by blast
show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
(\<exists>z. ((\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
-    proof (rule_tac x=M in exI, clarsimp simp add: M)
-      case goal1
+    proof (rule_tac x=M in exI, clarsimp simp add: M, goals)
+      case (1 a b)
obtain z where z:
"((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b)"
"norm (z - y) < e / B"
-        using M(2)[OF goal1(1)] by blast
+        using M(2)[OF 1(1)] by blast
have *: "(\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> s then f x else 0)"
using zero by auto
show ?case
apply (rule_tac x="h z" in exI)
-        apply (simp add: "*" lem z(1))
-        by (metis B diff le_less_trans pos_less_divide_eq z(2))
+        apply (simp add: * lem z(1))
+        apply (metis B diff le_less_trans pos_less_divide_eq z(2))
+        done
qed
qed
qed
@@ -2475,7 +2476,7 @@
fixes c :: "'a :: real_normed_algebra"
shows "(f has_integral y) i \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) i"
using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def)
-
+
lemma has_integral_cmul: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
unfolding o_def[symmetric]
by (metis has_integral_linear bounded_linear_scaleR_right)
@@ -2502,51 +2503,47 @@
and "(g has_integral l) s"
shows "((\<lambda>x. f x + g x) has_integral (k + l)) s"
proof -
-  have lem:"\<And>(f:: 'n \<Rightarrow> 'a) g a b k l.
-    (f has_integral k) (cbox a b) \<Longrightarrow>
-    (g has_integral l) (cbox a b) \<Longrightarrow>
-    ((\<lambda>x. f x + g x) has_integral (k + l)) (cbox a b)"
-  proof -
-    case goal1
-    show ?case
-      unfolding has_integral
-    proof clarify
-      fix e :: real
-      assume e: "e > 0"
-      then have *: "e/2 > 0"
+  have lem: "((\<lambda>x. f x + g x) has_integral (k + l)) (cbox a b)"
+    if f_k: "(f has_integral k) (cbox a b)"
+    and g_l: "(g has_integral l) (cbox a b)"
+    for f :: "'n \<Rightarrow> 'a" and g a b k l
+    unfolding has_integral
+  proof clarify
+    fix e :: real
+    assume e: "e > 0"
+    then have *: "e / 2 > 0"
+      by auto
+    obtain d1 where d1:
+      "gauge d1"
+      "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d1 fine p \<Longrightarrow>
+        norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) < e / 2"
+      using has_integralD[OF f_k *] by blast
+    obtain d2 where d2:
+      "gauge d2"
+      "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d2 fine p \<Longrightarrow>
+        norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l) < e / 2"
+      using has_integralD[OF g_l *] by blast
+    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
+              norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e)"
+    proof (rule exI [where x="\<lambda>x. (d1 x) \<inter> (d2 x)"], clarsimp simp add: gauge_inter[OF d1(1) d2(1)])
+      fix p
+      assume as: "p tagged_division_of (cbox a b)" "(\<lambda>x. d1 x \<inter> d2 x) fine p"
+      have *: "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) =
+        (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
+        unfolding scaleR_right_distrib setsum.distrib[of "\<lambda>(x,k). content k *\<^sub>R f x" "\<lambda>(x,k). content k *\<^sub>R g x" p,symmetric]
+        by (rule setsum.cong) auto
+      from as have fine: "d1 fine p" "d2 fine p"
+        unfolding fine_inter by auto
+      have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) =
+            norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
+        unfolding * by (auto simp add: algebra_simps)
+      also have "\<dots> < e/2 + e/2"
+        apply (rule le_less_trans[OF norm_triangle_ineq])
+        using as d1 d2 fine
+        apply (blast intro: add_strict_mono)
+        done
+      finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e"
by auto
-      obtain d1 where d1:
-        "gauge d1"
-        "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d1 fine p \<Longrightarrow>
-          norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) < e / 2"
-        using has_integralD[OF goal1(1) *] by blast
-      obtain d2 where d2:
-        "gauge d2"
-        "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d2 fine p \<Longrightarrow>
-          norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l) < e / 2"
-        using has_integralD[OF goal1(2) *] by blast
-      show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
-                norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e)"
-      proof (rule exI [where x="\<lambda>x. (d1 x) \<inter> (d2 x)"], clarsimp simp add: gauge_inter[OF d1(1) d2(1)])
-        fix p
-        assume as: "p tagged_division_of (cbox a b)" "(\<lambda>x. d1 x \<inter> d2 x) fine p"
-        have *: "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) =
-          (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
-          unfolding scaleR_right_distrib setsum.distrib[of "\<lambda>(x,k). content k *\<^sub>R f x" "\<lambda>(x,k). content k *\<^sub>R g x" p,symmetric]
-          by (rule setsum.cong) auto
-        from as have fine: "d1 fine p" "d2 fine p"
-          unfolding fine_inter by auto
-        have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) =
-              norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
-          unfolding * by (auto simp add: algebra_simps)
-        also have "\<dots> < e/2 + e/2"
-          apply (rule le_less_trans[OF norm_triangle_ineq])
-          using as d1 d2 fine
-          apply (blast intro: add_strict_mono)
-          done
-        finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e"
-          by auto
-      qed
qed
qed
{
@@ -2556,9 +2553,9 @@
}
assume as: "\<not> (\<exists>a b. s = cbox a b)"
then show ?thesis
-  proof (subst has_integral_alt, clarsimp)
-    case goal1
-    then have *: "e/2 > 0"
+  proof (subst has_integral_alt, clarsimp, goals)
+    case (1 e)
+    then have *: "e / 2 > 0"
by auto
from has_integral_altD[OF assms(1) as *]
obtain B1 where B1:
@@ -2812,8 +2809,8 @@
assume ?l
then guess y unfolding integrable_on_def has_integral .. note y=this
show "\<forall>e>0. \<exists>d. ?P e d"
-  proof clarify
-    case goal1
+  proof (clarify, goals)
+    case (1 e)
then have "e/2 > 0" by auto
then guess d
apply -
@@ -2847,8 +2844,8 @@
have dp: "\<And>i n. i\<le>n \<Longrightarrow> d i fine p n"
using p(2) unfolding fine_inters by auto
have "Cauchy (\<lambda>n. setsum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))"
-  proof (rule CauchyI)
-    case goal1
+  proof (rule CauchyI, goals)
+    case (1 e)
then guess N unfolding real_arch_inv[of e] .. note N=this
show ?case
apply (rule_tac x=N in exI)
@@ -3107,8 +3104,8 @@
and fj: "(f has_integral j) (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
and k: "k \<in> Basis"
shows "(f has_integral (i + j)) (cbox a b)"
-proof (unfold has_integral, rule, rule)
-  case goal1
+proof (unfold has_integral, rule, rule, goals)
+  case (1 e)
then have e: "e/2 > 0"
by auto
obtain d1
@@ -3176,12 +3173,11 @@
have lem1: "\<And>f P Q. (\<forall>x k. (x, k) \<in> {(x, f k) | x k. P x k} \<longrightarrow> Q x k) \<longleftrightarrow>
(\<forall>x k. P x k \<longrightarrow> Q x (f k))"
by auto
-    have fin_finite: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
+    have fin_finite: "finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}" if "finite s" for f s P
proof -
-      case goal1
-      then have "finite ((\<lambda>(x, k). (x, f k)) ` s)"
+      from that have "finite ((\<lambda>(x, k). (x, f k)) ` s)"
by auto
-      then show ?case
+      then show ?thesis
by (rule rev_finite_subset) auto
qed
{ fix g :: "'a set \<Rightarrow> 'a set"
@@ -3848,16 +3844,18 @@

lemma iterate_image:
assumes "monoidal opp"
-      and "inj_on f s"
-    shows "iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
-proof -
-  have *: "\<And>s. finite s \<Longrightarrow>  \<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<longrightarrow> x = y \<Longrightarrow>
-    iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
-  proof -
-    case goal1
-    then show ?case
-      apply (induct s)
-      using assms(1) by auto
+    and "inj_on f s"
+  shows "iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
+proof -
+  have *: "iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
+    if "finite s" "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<longrightarrow> x = y" for s
+    using that
+  proof (induct s)
+    case empty
+    then show ?case by simp
+  next
+    case insert
+    with assms(1) show ?case by auto
qed
show ?thesis
apply (cases "finite (support opp g (f ` s))")
@@ -4333,14 +4331,17 @@
and "\<forall>x\<in>s. (f x)\<bullet>k \<le> (g x)\<bullet>k"
shows "i\<bullet>k \<le> j\<bullet>k"
proof -
-  have lem: "\<And>a b i j::'b. \<And>g f::'a \<Rightarrow> 'b. (f has_integral i) (cbox a b) \<Longrightarrow>
-    (g has_integral j) (cbox a b) \<Longrightarrow> \<forall>x\<in>cbox a b. (f x)\<bullet>k \<le> (g x)\<bullet>k \<Longrightarrow> i\<bullet>k \<le> j\<bullet>k"
+  have lem: "i\<bullet>k \<le> j\<bullet>k"
+    if f_i: "(f has_integral i) (cbox a b)"
+    and g_j: "(g has_integral j) (cbox a b)"
+    and le: "\<forall>x\<in>cbox a b. (f x)\<bullet>k \<le> (g x)\<bullet>k"
+    for a b i and j :: 'b and f g :: "'a \<Rightarrow> 'b"
proof (rule ccontr)
-    case goal1
+    assume "\<not> ?thesis"
then have *: "0 < (i\<bullet>k - j\<bullet>k) / 3"
by auto
-    guess d1 using goal1(1)[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d1=this[rule_format]
-    guess d2 using goal1(2)[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d2=this[rule_format]
+    guess d1 using f_i[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d1=this[rule_format]
+    guess d2 using g_j[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d2=this[rule_format]
obtain p where p: "p tagged_division_of cbox a b" "d1 fine p" "d2 fine p"
using fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] unfolding fine_inter
by metis
@@ -4351,7 +4352,7 @@
by blast+
then show False
unfolding inner_simps
-      using rsum_component_le[OF p(1) goal1(3)]
+      using rsum_component_le[OF p(1) le]
by (simp add: abs_real_def split: split_if_asm)
qed
show ?thesis
@@ -4747,9 +4748,10 @@
assumes k: "k \<in> Basis"
shows "negligible {x. x\<bullet>k = c}"
unfolding negligible_def has_integral
-proof clarify
-  case goal1
-  from content_doublesplit[OF this k,of a b c] guess d . note d=this
+proof (clarify, goals)
+  case (1 a b e)
+  from this and k obtain d where d: "0 < d" "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
+    by (rule content_doublesplit)
let ?i = "indicator {x::'a. x\<bullet>k = c} :: 'a\<Rightarrow>real"
show ?case
apply (rule_tac x="\<lambda>x. ball x d" in exI)
@@ -4821,9 +4823,8 @@
apply (auto simp add:interval_doublesplit[OF k])
done
also have "\<dots> < e"
-        apply (subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]])
-      proof -
-        case goal1
+      proof (subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]], goals)
+        case (1 u v)
have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
unfolding interval_doublesplit[OF k]
apply (rule content_subset)
@@ -4831,7 +4832,7 @@
apply auto
done
then show ?case
-          unfolding goal1
+          unfolding 1
unfolding interval_doublesplit[OF k]
by (blast intro: antisym)
next
@@ -5111,8 +5112,8 @@
assume assm: "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
show "(f has_integral 0) (cbox a b)"
unfolding has_integral
-  proof safe
-    case goal1
+  proof (safe, goals)
+    case (1 e)
then have "\<And>n. e / 2 / ((real n+1) * (2 ^ n)) > 0"
apply -
apply (rule divide_pos_pos)
@@ -5135,7 +5136,7 @@
presume "p \<noteq> {} \<Longrightarrow> ?goal"
then show ?goal
apply (cases "p = {}")
-          using goal1
+          using 1
apply auto
done
}
@@ -5159,21 +5160,16 @@
apply (drule tagged_division_ofD(4)[OF q(1)])
apply (auto intro: mult_nonneg_nonneg)
done
-      have **: "\<And>f g s t. finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow>
-        (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> setsum f s \<le> setsum g t"
-      proof -
-        case goal1
-        then show ?case
-          apply -
-          apply (rule setsum_le_included[of s t g snd f])
-          prefer 4
-          apply safe
-          apply (erule_tac x=x in ballE)
-          apply (erule exE)
-          apply (rule_tac x="(xa,x)" in bexI)
-          apply auto
-          done
-      qed
+      have **: "finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow>
+        (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> setsum f s \<le> setsum g t" for f g s t
+        apply (rule setsum_le_included[of s t g snd f])
+        prefer 4
+        apply safe
+        apply (erule_tac x=x in ballE)
+        apply (erule exE)
+        apply (rule_tac x="(xa,x)" in bexI)
+        apply auto
+        done
have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) \<le> setsum (\<lambda>i. (real i + 1) *
norm (setsum (\<lambda>(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {..N+1}"
unfolding real_norm_def setsum_right_distrib abs_of_nonneg[OF *] diff_0_right
@@ -5244,12 +5240,11 @@
done
qed (insert as, auto)
also have "\<dots> \<le> setsum (\<lambda>i. e / 2 / 2 ^ i) {..N+1}"
-        apply (rule setsum_mono)
-      proof -
-        case goal1
+      proof (rule setsum_mono, goals)
+        case (1 i)
then show ?case
apply (subst mult.commute, subst pos_le_divide_eq[symmetric])
-          using d(2)[rule_format,of "q i" i]
+          using d(2)[rule_format, of "q i" i]
using q[rule_format]
apply (auto simp add: field_simps)
done
@@ -5259,7 +5254,7 @@
apply (rule mult_strict_left_mono)
unfolding power_inverse [symmetric] lessThan_Suc_atMost[symmetric]
apply (subst geometric_sum)
-        using goal1
+        using 1
apply auto
done
finally show "?goal" by auto
@@ -5352,8 +5347,8 @@
and "t \<subseteq> s"
shows "negligible t"
unfolding negligible_def
-proof safe
-  case goal1
+proof (safe, goals)
+  case (1 a b)
show ?case
using assms(1)[unfolded negligible_def,rule_format,of a b]
apply -
@@ -5381,8 +5376,8 @@
and "negligible t"
shows "negligible (s \<union> t)"
unfolding negligible_def
-proof safe
-  case goal1
+proof (safe, goals)
+  case (1 a b)
note assm = assms[unfolded negligible_def,rule_format,of a b]
then show ?case
apply (subst has_integral_spike_eq[OF assms(2)])
@@ -5557,20 +5552,18 @@
by auto

lemma operative_approximable:
-  fixes f::"'b::euclidean_space \<Rightarrow> 'a::banach"
+  fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
assumes "0 \<le> e"
shows "operative op \<and> (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)"
unfolding operative_def neutral_and
proof safe
fix a b :: 'b
-  {
-    assume "content (cbox a b) = 0"
-    then show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
-      apply (rule_tac x=f in exI)
-      using assms
-      apply (auto intro!:integrable_on_null)
-      done
-  }
+  show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+    if "content (cbox a b) = 0"
+    apply (rule_tac x=f in exI)
+    using assms that
+    apply (auto intro!: integrable_on_null)
+    done
{
fix c g
fix k :: 'b
@@ -5590,8 +5583,9 @@
let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
apply (rule_tac x="?g" in exI)
-  proof safe
-    case goal1
+    apply safe
+  proof goals
+    case (1 x)
then show ?case
apply -
apply (cases "x\<bullet>k=c")
@@ -5600,7 +5594,7 @@
apply auto
done
next
-    case goal2
+    case 2
presume "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
and "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
then guess h1 h2 unfolding integrable_on_def by auto
@@ -6437,8 +6431,8 @@
let ?I = "\<lambda>a b. integral {a .. b} f"
show "\<exists>d>0. \<forall>y\<in>{a .. b}. norm (y - x) < d \<longrightarrow>
norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \<le> e * norm (y - x)"
-  proof (rule, rule, rule d, safe)
-    case goal1
+  proof (rule, rule, rule d, safe, goals)
+    case (1 y)
show ?case
proof (cases "y < x")
case False
@@ -6446,7 +6440,7 @@
apply (rule integrable_subinterval_real,rule integrable_continuous_real)
apply (rule assms)
unfolding not_less
-        using assms(2) goal1
+        using assms(2) 1
apply auto
done
then have *: "?I a y - ?I a x = ?I x y"
@@ -6455,7 +6449,7 @@
apply (rule integral_combine)
using False
unfolding not_less
-        using assms(2) goal1
+        using assms(2) 1
apply auto
done
have **: "norm (y - x) = content {x .. y}"
@@ -6472,7 +6466,7 @@
apply (rule assms)+
proof -
show "{x .. y} \<subseteq> {a .. b}"
-          using goal1 assms(2) by auto
+          using 1 assms(2) by auto
have *: "y - x = norm (y - x)"
using False by auto
show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {x .. y}"
@@ -6484,7 +6478,7 @@
apply (rule less_imp_le)
apply (rule d(2)[unfolded dist_norm])
using assms(2)
-          using goal1
+          using 1
apply auto
done
qed (insert e, auto)
@@ -6495,14 +6489,14 @@
unfolding box_real
apply (rule assms)+
unfolding not_less
-        using assms(2) goal1
+        using assms(2) 1
apply auto
done
then have *: "?I a x - ?I a y = ?I y x"
unfolding algebra_simps
apply (subst eq_commute)
apply (rule integral_combine)
-        using True using assms(2) goal1
+        using True using assms(2) 1
apply auto
done
have **: "norm (y - x) = content {y .. x}"
@@ -6528,7 +6522,7 @@
apply (rule assms)+
proof -
show "{y .. x} \<subseteq> {a .. b}"
-          using goal1 assms(2) by auto
+          using 1 assms(2) by auto
have *: "x - y = norm (y - x)"
using True by auto
show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {y .. x}"
@@ -6541,7 +6535,7 @@
apply (rule less_imp_le)
apply (rule d(2)[unfolded dist_norm])
using assms(2)
-          using goal1
+          using 1
apply auto
done
qed (insert e, auto)
@@ -6570,17 +6564,18 @@
from antiderivative_continuous[OF assms] guess g . note g=this
show ?thesis
apply (rule that[of g])
-  proof safe
-    case goal1
+    apply safe
+  proof goals
+    case (1 u v)
have "\<forall>x\<in>cbox u v. (g has_vector_derivative f x) (at x within cbox u v)"
apply rule
apply (rule has_vector_derivative_within_subset)
apply (rule g[rule_format])
-      using goal1(1-2)
+      using 1(1-2)
apply auto
done
then show ?case
-      using fundamental_theorem_of_calculus[OF goal1(3),of "g" "f"] by auto
+      using fundamental_theorem_of_calculus[OF 1(3), of g f] by auto
qed
qed

@@ -6598,18 +6593,16 @@
and "(f has_integral i) (cbox a b)"
shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` cbox a b)"
proof -
-  {
-    presume *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
-    show ?thesis
-      apply cases
-      defer
-      apply (rule *)
-      apply assumption
-    proof -
-      case goal1
-      then show ?thesis
-        unfolding goal1 assms(8)[unfolded goal1 has_integral_empty_eq] by auto qed
-  }
+  show ?thesis when *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
+    apply cases
+    defer
+    apply (rule *)
+    apply assumption
+  proof goals
+    case 1
+    then show ?thesis
+      unfolding 1 assms(8)[unfolded 1 has_integral_empty_eq] by auto
+  qed
assume "cbox a b \<noteq> {}"
from assms(6)[rule_format,of a b] guess w z by (elim exE) note wz=this
have inj: "inj g" "inj h"
@@ -6809,7 +6802,7 @@
using assms
apply (safe intro!: interval_image_affinity_interval content_image_affinity_cbox)
apply (rule zero_less_power)
-  unfolding scaleR_right_distrib
+  unfolding scaleR_right_distrib
apply auto
done

@@ -7102,10 +7095,9 @@
by (rule norm_triangle_ineq4)
also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8"
-        case goal1
have "\<bar>c - a\<bar> \<le> \<bar>l\<bar>"
using as' by auto
-        then show ?case
+        then show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8"
apply -
apply (rule order_trans[OF _ l(2)])
unfolding norm_scaleR
@@ -7113,8 +7105,7 @@
apply auto
done
next
-        case goal2
-        show ?case
+        show "norm (f c - f a) \<le> e * (b - a) / 8"
apply (rule less_imp_le)
apply (cases "a = c")
defer
@@ -7165,10 +7156,9 @@
by (rule norm_triangle_ineq4)
also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8"
-        case goal1
have "\<bar>c - b\<bar> \<le> \<bar>l\<bar>"
using as' by auto
-        then show ?case
+        then show "norm ((b - c) *\<^sub>R f' b) \<le> e * (b - a) / 8"
apply -
apply (rule order_trans[OF _ l(2)])
unfolding norm_scaleR
@@ -7176,8 +7166,7 @@
apply auto
done
next
-        case goal2
-        show ?case
+        show "norm (f b - f c) \<le> e * (b - a) / 8"
apply (rule less_imp_le)
apply (cases "b = c")
defer
@@ -7196,21 +7185,20 @@
let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))"
show "?P e"
apply (rule_tac x="?d" in exI)
-  proof safe
-    case goal1
+  proof (safe, goals)
+    case 1
show ?case
apply (rule gauge_ball_dependent)
using ab db(1) da(1) d(1)
apply auto
done
next
-    case goal2
-    note as=this
+    case as: (2 p)
let ?A = "{t. fst t \<in> {a, b}}"
-    note p = tagged_division_ofD[OF goal2(1)]
+    note p = tagged_division_ofD[OF as(1)]
have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"
-      using goal2 by auto
-    note * = additive_tagged_division_1'[OF assms(1) goal2(1), symmetric]
+      using as by auto
+    note * = additive_tagged_division_1'[OF assms(1) as(1), symmetric]
have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2"
by arith
show ?case
@@ -7219,8 +7207,8 @@
apply (subst(2) pA)
apply (subst pA)
unfolding setsum.union_disjoint[OF pA(2-)]
-    proof (rule norm_triangle_le, rule **)
-      case goal1
+    proof (rule norm_triangle_le, rule **, goals)
+      case 1
show ?case
apply (rule order_trans)
apply (rule setsum_norm_le)
@@ -7231,17 +7219,17 @@
apply (unfold not_le o_def split_conv fst_conv)
proof (rule ccontr)
fix x k
-        assume as: "(x, k) \<in> p"
+        assume xk: "(x, k) \<in> p"
"e * (Sup k -  Inf k) / 2 <
norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))"
from p(4)[OF this(1)] guess u v by (elim exE) note k=this
then have "u \<le> v" and uv: "{u, v} \<subseteq> cbox u v"
-          using p(2)[OF as(1)] by auto
-        note result = as(2)[unfolded k box_real interval_bounds_real[OF this(1)] content_real[OF this(1)]]
+          using p(2)[OF xk(1)] by auto
+        note result = xk(2)[unfolded k box_real interval_bounds_real[OF this(1)] content_real[OF this(1)]]

assume as': "x \<noteq> a" "x \<noteq> b"
then have "x \<in> box a b"
-          using p(2-3)[OF as(1)] by (auto simp: mem_box)
+          using p(2-3)[OF xk(1)] by (auto simp: mem_box)
note  * = d(2)[OF this]
have "norm ((v - u) *\<^sub>R f' (x) - (f (v) - f (u))) =
norm ((f (u) - f (x) - (u - x) *\<^sub>R f' (x)) - (f (v) - f (x) - (v - x) *\<^sub>R f' (x)))"
@@ -7253,7 +7241,7 @@
apply (rule norm_triangle_le_sub)
apply (rule_tac[!] *)
-          using fineD[OF goal2(2) as(1)] as'
+          using fineD[OF as(2) xk(1)] as'
unfolding k subset_eq
apply -
apply (erule_tac x=u in ballE)
@@ -7262,7 +7250,7 @@
apply (auto simp:dist_real_def)
done
also have "\<dots> \<le> e / 2 * norm (v - u)"
-          using p(2)[OF as(1)]
+          using p(2)[OF xk(1)]
unfolding k
by (auto simp add: field_simps)
finally have "e * (v - u) / 2 < e * (v - u) / 2"
@@ -7276,7 +7264,7 @@
next
have *: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2) / 2 \<Longrightarrow> x - s1 \<le> s2 / 2"
by auto
-      case goal2
+      case 2
show ?case
apply (rule *)
apply (rule setsum_nonneg)
@@ -7307,7 +7295,7 @@
defer
apply rule
unfolding split_paired_all split_conv o_def
-        proof -
+        proof goals
fix x k
assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> {t. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
then have xk: "(x, k) \<in> p" "content k = 0"
@@ -7325,18 +7313,24 @@
have *: "p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0} =
{t. t\<in>p \<and> fst t = a \<and> content(snd t) \<noteq> 0} \<union> {t. t\<in>p \<and> fst t = b \<and> content(snd t) \<noteq> 0}"
by blast
-          have **: "\<And>s f. \<And>e::real. (\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> x = y) \<Longrightarrow>
-            (\<forall>x. x \<in> s \<longrightarrow> norm (f x) \<le> e) \<Longrightarrow> e > 0 \<Longrightarrow> norm (setsum f s) \<le> e"
-          proof (case_tac "s = {}")
-            case goal2
+          have **: "norm (setsum f s) \<le> e"
+            if "\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> x = y"
+            and "\<forall>x. x \<in> s \<longrightarrow> norm (f x) \<le> e"
+            and "e > 0"
+            for s f and e :: real
+          proof (cases "s = {}")
+            case True
+            with that show ?thesis by auto
+          next
+            case False
then obtain x where "x \<in> s"
by auto
then have *: "s = {x}"
-              using goal2(1) by auto
-            then show ?case
-              using \<open>x \<in> s\<close> goal2(2) by auto
-          qed auto
-          case goal2
+              using that(1) by auto
+            then show ?thesis
+              using \<open>x \<in> s\<close> that(2) by auto
+          qed
+          case 2
show ?case
apply (subst *)
apply (subst setsum.union_disjoint)
@@ -7346,48 +7340,46 @@
apply (rule_tac[1-2] **)
proof -
let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
-            have pa: "\<And>k. (a, k) \<in> p \<Longrightarrow> \<exists>v. k = cbox a v \<and> a \<le> v"
+            have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
proof -
-              case goal1
-              guess u v using p(4)[OF goal1] by (elim exE) note uv=this
+              guess u v using p(4)[OF that] by (elim exE) note uv=this
have *: "u \<le> v"
-                using p(2)[OF goal1] unfolding uv by auto
+                using p(2)[OF that] unfolding uv by auto
have u: "u = a"
proof (rule ccontr)
have "u \<in> cbox u v"
-                  using p(2-3)[OF goal1(1)] unfolding uv by auto
+                  using p(2-3)[OF that(1)] unfolding uv by auto
have "u \<ge> a"
-                  using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto
+                  using p(2-3)[OF that(1)] unfolding uv subset_eq by auto
moreover assume "\<not> ?thesis"
ultimately have "u > a" by auto
then show False
-                  using p(2)[OF goal1(1)] unfolding uv by (auto simp add:)
+                  using p(2)[OF that(1)] unfolding uv by (auto simp add:)
qed
-              then show ?case
+              then show ?thesis
apply (rule_tac x=v in exI)
unfolding uv
using *
apply auto
done
qed
-            have pb: "\<And>k. (b, k) \<in> p \<Longrightarrow> \<exists>v. k = cbox v b \<and> b \<ge> v"
+            have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
proof -
-              case goal1
-              guess u v using p(4)[OF goal1] by (elim exE) note uv=this
+              guess u v using p(4)[OF that] by (elim exE) note uv=this
have *: "u \<le> v"
-                using p(2)[OF goal1] unfolding uv by auto
-              have u: "v =  b"
+                using p(2)[OF that] unfolding uv by auto
+              have u: "v = b"
proof (rule ccontr)
have "u \<in> cbox u v"
-                  using p(2-3)[OF goal1(1)] unfolding uv by auto
+                  using p(2-3)[OF that(1)] unfolding uv by auto
have "v \<le> b"
-                  using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto
+                  using p(2-3)[OF that(1)] unfolding uv subset_eq by auto
moreover assume "\<not> ?thesis"
ultimately have "v < b" by auto
then show False
-                  using p(2)[OF goal1(1)] unfolding uv by (auto simp add:)
+                  using p(2)[OF that(1)] unfolding uv by (auto simp add:)
qed
-              then show ?case
+              then show ?thesis
apply (rule_tac x=u in exI)
unfolding uv
using *
@@ -7458,15 +7450,15 @@
apply rule
unfolding mem_Collect_eq
unfolding split_paired_all fst_conv snd_conv
-            proof safe
-              case goal1
-              guess v using pa[OF goal1(1)] .. note v = conjunctD2[OF this]
+            proof (safe, goals)
+              case 1
+              guess v using pa[OF 1(1)] .. note v = conjunctD2[OF this]
have "?a \<in> {?a..v}"
using v(2) by auto
then have "v \<le> ?b"
-                using p(3)[OF goal1(1)] unfolding subset_eq v by auto
+                using p(3)[OF 1(1)] unfolding subset_eq v by auto
moreover have "{?a..v} \<subseteq> ball ?a da"
-                using fineD[OF as(2) goal1(1)]
+                using fineD[OF as(2) 1(1)]
apply -
apply (subst(asm) if_P)
apply (rule refl)
@@ -7479,7 +7471,7 @@
unfolding v interval_bounds_real[OF v(2)] box_real
apply -
apply(rule da(2)[of "v"])
-                using goal1 fineD[OF as(2) goal1(1)]
+                using 1 fineD[OF as(2) 1(1)]
unfolding v content_eq_0
apply auto
done
@@ -7490,14 +7482,15 @@
apply rule
unfolding mem_Collect_eq
unfolding split_paired_all fst_conv snd_conv
-            proof safe
-              case goal1 guess v using pb[OF goal1(1)] .. note v = conjunctD2[OF this]
+            proof (safe, goals)
+              case 1
+              guess v using pb[OF 1(1)] .. note v = conjunctD2[OF this]
have "?b \<in> {v.. ?b}"
using v(2) by auto
-              then have "v \<ge> ?a" using p(3)[OF goal1(1)]
+              then have "v \<ge> ?a" using p(3)[OF 1(1)]
unfolding subset_eq v by auto
moreover have "{v..?b} \<subseteq> ball ?b db"
-                using fineD[OF as(2) goal1(1)]
+                using fineD[OF as(2) 1(1)]
apply -
apply (subst(asm) if_P, rule refl)
unfolding subset_eq
@@ -7511,7 +7504,7 @@
unfolding interval_bounds_real[OF v(2)] box_real
apply -
apply(rule db(2)[of "v"])
-                using goal1 fineD[OF as(2) goal1(1)]
+                using 1 fineD[OF as(2) 1(1)]
unfolding v content_eq_0
apply auto
done
@@ -7705,8 +7698,8 @@
from fine_division_exists_real[OF this, of a t] guess p . note p=this
note p'=tagged_division_ofD[OF this(1)]
have pt: "\<forall>(x,k)\<in>p. x \<le> t"
-    proof safe
-      case goal1
+    proof (safe, goals)
+      case 1
from p'(2,3)[OF this] show ?case
by auto
qed
@@ -7760,8 +7753,8 @@
have **: "\<And>x F. F \<union> {x} = insert x F"
by auto
have "(c, cbox t c) \<notin> p"
-      proof safe
-        case goal1
+      proof (safe, goals)
+        case 1
from p'(2-3)[OF this] have "c \<in> cbox a t"
by auto
then show False using \<open>t < c\<close>
@@ -7862,8 +7855,8 @@
apply cases
apply (rule *)
apply assumption
-    proof -
-      case goal1
+    proof goals
+      case 1
then have "cbox a b = {x}"
using as(1)
apply -
@@ -8001,12 +7994,11 @@
using assms(4,7)
apply auto
done
-  have *: "\<And>t xa. (1 - t) *\<^sub>R c + t *\<^sub>R x = (1 - xa) *\<^sub>R c + xa *\<^sub>R x \<Longrightarrow> t = xa"
+  have *: "t = xa" if "(1 - t) *\<^sub>R c + t *\<^sub>R x = (1 - xa) *\<^sub>R c + xa *\<^sub>R x" for t xa
proof -
-    case goal1
-    then have "(t - xa) *\<^sub>R x = (t - xa) *\<^sub>R c"
+    from that have "(t - xa) *\<^sub>R x = (t - xa) *\<^sub>R c"
unfolding scaleR_simps by (auto simp add: algebra_simps)
-    then show ?case
+    then show ?thesis
using \<open>x \<noteq> c\<close> by auto
qed
have as2: "finite {t. ((1 - t) *\<^sub>R c + t *\<^sub>R x) \<in> k}"
@@ -8151,14 +8143,14 @@
apply cases
apply (rule *)
apply assumption
-    proof -
-      case goal1
+    proof goals
+      case 1
then have *: "box c d = {}"
by (metis bot.extremum_uniqueI box_subset_cbox)
show ?thesis
using assms(1)
unfolding *
-        using goal1
+        using 1
by auto
qed
}
@@ -8187,13 +8179,14 @@
have iterate:"iterate (lifted op +) (p - {cbox c d})
(\<lambda>i. if g integrable_on i then Some (integral i g) else None) = Some 0"
proof (rule *)
-    case goal1
+    fix x
+    assume x: "x \<in> p - {cbox c d}"
then have "x \<in> p"
by auto
note div = division_ofD(2-5)[OF p(1) this]
from div(3) guess u v by (elim exE) note uv=this
have "interior x \<inter> interior (cbox c d) = {}"
-      using div(4)[OF p(2)] goal1 by auto
+      using div(4)[OF p(2)] x by auto
then have "(g has_integral 0) x"
unfolding uv
apply -
@@ -8201,7 +8194,7 @@
unfolding g_def interior_cbox
apply auto
done
-    then show ?case
+    then show "(if g integrable_on x then Some (integral x g) else None) = Some 0"
by auto
qed

@@ -8345,19 +8338,20 @@
apply (drule B(2))
unfolding mem_box
proof
-      case goal1
-      then show ?case
-        using Basis_le_norm[OF \<open>i\<in>Basis\<close>, of x]
+      fix x i
+      show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm x \<le> B" and "i \<in> Basis"
+        using that and Basis_le_norm[OF \<open>i\<in>Basis\<close>, of x]
unfolding c_def d_def
by (auto simp add: field_simps setsum_negf)
qed
have "ball 0 C \<subseteq> cbox c d"
-      apply safe
+      apply (rule subsetI)
unfolding mem_box mem_ball dist_norm
-    proof
-      case goal1
-      then show ?case
-        using Basis_le_norm[OF \<open>i\<in>Basis\<close>, of x]
+    proof (rule, goals)
+      fix x i :: 'n
+      assume x: "norm (0 - x) < C" and i: "i \<in> Basis"
+      show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
+        using Basis_le_norm[OF i, of x] and x i
unfolding c_def d_def
by (auto simp: setsum_negf)
qed
@@ -8380,18 +8374,20 @@
apply (drule B(2))
unfolding mem_box
proof
-        case goal1
-        then show ?case
+        fix x i :: 'n
+        assume "norm x \<le> B" and "i \<in> Basis"
+        then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
using Basis_le_norm[of i x]
unfolding c_def d_def
by (auto simp add: field_simps setsum_negf)
qed
have "ball 0 C \<subseteq> cbox c d"
-        apply safe
+        apply (rule subsetI)
unfolding mem_box mem_ball dist_norm
proof
-        case goal1
-        then show ?case
+        fix x i :: 'n
+        assume "norm (0 - x) < C" and "i \<in> Basis"
+        then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
using Basis_le_norm[of i x]
unfolding c_def d_def
by (auto simp: setsum_negf)
@@ -8521,8 +8517,8 @@
show ?l
unfolding negligible_def
proof safe
-    case goal1
-    show ?case
+    fix a b
+    show "(indicator s has_integral 0) (cbox a b)"
apply (rule has_integral_negligible[OF \<open>?r\<close>[rule_format,of a b]])
unfolding indicator_def
apply auto
@@ -8662,8 +8658,8 @@
show ?l
apply (subst has_integral')
apply safe
-  proof -
-    case goal1
+  proof goals
+    case (1 e)
from \<open>?r\<close>[THEN conjunct2,rule_format,OF this] guess B .. note B=conjunctD2[OF this]
show ?case
apply rule
@@ -8688,10 +8684,10 @@
show "?f integrable_on cbox a b"
proof (rule integrable_subinterval[of _ ?a ?b])
have "ball 0 B \<subseteq> cbox ?a ?b"
-        apply safe
+        apply (rule subsetI)
unfolding mem_ball mem_box dist_norm
-      proof
-        case goal1
+      proof (rule, goals)
+        case (1 x i)
then show ?case using Basis_le_norm[of i x]
by (auto simp add:field_simps)
qed
@@ -8716,8 +8712,8 @@
apply rule
apply (rule B)
apply safe
-    proof -
-      case goal1
+    proof goals
+      case 1
from B(2)[OF this] guess z .. note z=conjunctD2[OF this]
from integral_unique[OF this(1)] show ?case
using z(2) by auto
@@ -8743,8 +8739,8 @@
show ?r
apply safe
apply (rule y)
-  proof -
-    case goal1
+  proof goals
+    case (1 e)
then have "e/2 > 0"
by auto
from y(2)[OF this] guess B .. note B=conjunctD2[OF this,rule_format]
@@ -8753,11 +8749,11 @@
apply rule
apply (rule B)
apply safe
-    proof -
-      case goal1
+    proof goals
+      case (1 a b c d)
show ?case
apply (rule norm_triangle_half_l)
-        using B(2)[OF goal1(1)] B(2)[OF goal1(2)]
+        using B(2)[OF 1(1)] B(2)[OF 1(2)]
apply auto
done
qed
@@ -8767,18 +8763,18 @@
note as = conjunctD2[OF this,rule_format]
let ?cube = "\<lambda>n. cbox (\<Sum>i\<in>Basis. - real n *\<^sub>R i::'n) (\<Sum>i\<in>Basis. real n *\<^sub>R i)"
have "Cauchy (\<lambda>n. integral (?cube n) (\<lambda>x. if x \<in> s then f x else 0))"
-  proof (unfold Cauchy_def, safe)
-    case goal1
+  proof (unfold Cauchy_def, safe, goals)
+    case (1 e)
from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format]
from real_arch_simple[of B] guess N .. note N = this
{
fix n
assume n: "n \<ge> N"
have "ball 0 B \<subseteq> ?cube n"
-        apply safe
+        apply (rule subsetI)
unfolding mem_ball mem_box dist_norm
-      proof
-        case goal1
+      proof (rule, goals)
+        case (1 x i)
then show ?case
using Basis_le_norm[of i x] \<open>i\<in>Basis\<close>
using n N
@@ -8801,8 +8797,8 @@
apply (rule_tac x=i in exI)
apply safe
apply (rule as(1)[unfolded integrable_on_def])
-  proof -
-    case goal1
+  proof goals
+    case (1 e)
then have *: "e/2 > 0" by auto
from i[OF this] guess N .. note N =this[rule_format]
from as(2)[OF *] guess B .. note B=conjunctD2[OF this,rule_format]
@@ -8834,8 +8830,8 @@
using x
unfolding mem_box mem_ball dist_norm
apply -
-        proof
-          case goal1
+        proof (rule, goals)
+          case (1 i)
then show ?case
using Basis_le_norm[of i x] \<open>i \<in> Basis\<close>
using n
@@ -8874,8 +8870,8 @@
assumes "\<forall>e>0. \<exists>g  h i j. (g has_integral i) (cbox a b) \<and> (h has_integral j) (cbox a b) \<and>
norm (i - j) < e \<and> (\<forall>x\<in>cbox a b. (g x) \<le> f x \<and> f x \<le> h x)"
shows "f integrable_on cbox a b"
-proof (subst integrable_cauchy, safe)
-  case goal1
+proof (subst integrable_cauchy, safe, goals)
+  case (1 e)
then have e: "e/3 > 0"
by auto
note assms[rule_format,OF this]
@@ -8886,13 +8882,13 @@
apply (rule_tac x="\<lambda>x. d1 x \<inter> d2 x" in exI)
apply (rule conjI gauge_inter d1 d2)+
unfolding fine_inter
-  proof safe
+  proof (safe, goals)
have **: "\<And>i j g1 g2 h1 h2 f1 f2. g1 - h2 \<le> f1 - f2 \<Longrightarrow> f1 - f2 \<le> h1 - g2 \<Longrightarrow>
abs (i - j) < e / 3 \<Longrightarrow> abs (g2 - i) < e / 3 \<Longrightarrow>  abs (g1 - i) < e / 3 \<Longrightarrow>
abs (h2 - j) < e / 3 \<Longrightarrow> abs (h1 - j) < e / 3 \<Longrightarrow> abs (f1 - f2) < e"
using \<open>e > 0\<close> by arith
-    case goal1
-    note tagged_division_ofD(2-4) note * = this[OF goal1(1)] this[OF goal1(4)]
+    case (1 p1 p2)
+    note tagged_division_ofD(2-4) note * = this[OF 1(1)] this[OF 1(4)]

have "(\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R g x) \<ge> 0"
and "0 \<le> (\<Sum>(x, k)\<in>p2. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)"
@@ -8937,10 +8933,10 @@
defer
unfolding real_norm_def[symmetric]
apply (rule obt(3))
-      apply (rule d1(2)[OF conjI[OF goal1(4,5)]])
-      apply (rule d1(2)[OF conjI[OF goal1(1,2)]])
-      apply (rule d2(2)[OF conjI[OF goal1(4,6)]])
-      apply (rule d2(2)[OF conjI[OF goal1(1,3)]])
+      apply (rule d1(2)[OF conjI[OF 1(4,5)]])
+      apply (rule d1(2)[OF conjI[OF 1(1,2)]])
+      apply (rule d2(2)[OF conjI[OF 1(4,6)]])
+      apply (rule d2(2)[OF conjI[OF 1(1,3)]])
apply auto
done
qed
@@ -8953,8 +8949,8 @@
shows "f integrable_on s"
proof -
have "\<And>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on cbox a b"
-  proof (rule integrable_straddle_interval, safe)
-    case goal1
+  proof (rule integrable_straddle_interval, safe, goals)
+    case (1 a b e)
then have *: "e/4 > 0"
by auto
from assms[rule_format,OF this] guess g h i j by (elim exE conjE) note obt=this
@@ -8972,16 +8968,16 @@
apply safe
unfolding mem_ball mem_box dist_norm
apply (rule_tac[!] ballI)
-    proof -
-      case goal1
+    proof goals
+      case (1 x i)
then show ?case using Basis_le_norm[of i x]
unfolding c_def d_def by auto
next
-      case goal2
+      case (2 x i)
then show ?case using Basis_le_norm[of i x]
unfolding c_def d_def by auto
qed
-    have **:" \<And>ch cg ag ah::real. norm (ah - ag) \<le> norm (ch - cg) \<Longrightarrow> norm (cg - i) < e / 4 \<Longrightarrow>
+    have **: "\<And>ch cg ag ah::real. norm (ah - ag) \<le> norm (ch - cg) \<Longrightarrow> norm (cg - i) < e / 4 \<Longrightarrow>
norm (ch - j) < e / 4 \<Longrightarrow> norm (ag - ah) < e"
using obt(3)
unfolding real_norm_def
@@ -9031,8 +9027,8 @@
unfolding integrable_alt[of f]
apply safe
apply (rule interv)
-  proof -
-    case goal1
+  proof goals
+    case (1 e)
then have *: "e/3 > 0"
by auto
from assms[rule_format,OF this] guess g h i j by (elim exE conjE) note obt=this
@@ -9129,15 +9125,21 @@
done
note assms(2)[unfolded *]
note has_integral_setsum[OF assms(1) this]
-  then show ?thesis unfolding * apply-apply(rule has_integral_spike[OF **]) defer apply assumption
-  proof safe
-    case goal1
+  then show ?thesis
+    unfolding *
+    apply -
+    apply (rule has_integral_spike[OF **])
+    defer
+    apply assumption
+    apply safe
+  proof goals
+    case (1 x)
then show ?case
proof (cases "x \<in> \<Union>t")
case True
then guess s unfolding Union_iff .. note s=this
then have *: "\<forall>b\<in>t. x \<in> b \<longleftrightarrow> b = s"
-        using goal1(3) by blast
+        using 1(3) by blast
show ?thesis
unfolding if_P[OF True]
apply (rule trans)
@@ -9172,10 +9174,10 @@
apply rule
apply rule
apply rule
-  proof -
-    case goal1
+  proof goals
+    case (1 s s')
from d(4)[OF this(1)] d(4)[OF this(2)] guess a c b d by (elim exE) note obt=this
-    from d(5)[OF goal1] show ?case
+    from d(5)[OF 1] show ?case
unfolding obt interior_cbox
apply -
apply (rule negligible_subset[of "(cbox a b-box a b) \<union> (cbox c d-box c d)"])
@@ -9206,8 +9208,8 @@
apply (rule has_integral_combine_division[OF assms(2)])
apply safe
unfolding has_integral_integral[symmetric]
-proof -
-  case goal1
+proof goals
+  case (1 k)
from division_ofD(2,4)[OF assms(2) this]
show ?case
apply safe
@@ -9245,8 +9247,9 @@
and "i \<subseteq> s"
shows "f integrable_on i"
apply (rule integrable_combine_division assms)+
-proof safe
-  case goal1
+  apply safe
+proof goals
+  case 1
note division_ofD(2,4)[OF assms(1) this]
then show ?case
apply safe
@@ -9306,8 +9309,9 @@
and "p tagged_division_of (cbox a b)"
shows "(f has_integral (setsum (\<lambda>(x,k). integral k f) p)) (cbox a b)"
apply (rule has_integral_combine_tagged_division[OF assms(2)])
-proof safe
-  case goal1
+  apply safe
+proof goals
+  case 1
note tagged_division_ofD(3-4)[OF assms(2) this]
then show ?case
using integrable_subinterval[OF assms(1)] by blast
@@ -9354,8 +9358,9 @@

have "\<forall>i\<in>r. \<exists>p. p tagged_division_of i \<and> d fine p \<and>
norm (setsum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
-  proof safe
-    case goal1
+    apply safe
+  proof goals
+    case (1 i)
then have i: "i \<in> q"
unfolding r_def by auto
from q'(4)[OF this] guess u v by (elim exE) note uv=this
@@ -9392,14 +9397,13 @@
done
note * = tagged_partial_division_of_union_self[OF p(1)]
have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r"
-    proof (rule tagged_division_union[OF * tagged_division_unions])
-      show "finite r"
-        by fact
-      case goal2
+      using r
+    proof (rule tagged_division_union[OF * tagged_division_unions], goals)
+      case 1
then show ?case
using qq by auto
next
-      case goal3
+      case 2
then show ?case
apply rule
apply rule
@@ -9409,7 +9413,7 @@
apply auto
done
next
-      case goal4
+      case 3
then show ?case
apply (rule inter_interior_unions_intervals)
apply fact
@@ -9514,22 +9518,24 @@
using as(3) unfolding as by auto
qed

-  have *: "\<And>ir ip i cr cp. norm ((cp + cr) - i) < e \<Longrightarrow> norm(cr - ir) < k \<Longrightarrow>
-    ip + ir = i \<Longrightarrow> norm (cp - ip) \<le> e + k"
+  have *: "norm (cp - ip) \<le> e + k"
+    if "norm ((cp + cr) - i) < e"
+    and "norm (cr - ir) < k"
+    and "ip + ir = i"
+    for ir ip i cr cp
proof -
-    case goal1
-    then show ?case
+    from that show ?thesis
using norm_triangle_le[of "cp + cr - i" "- (cr - ir)"]
-      unfolding goal1(3)[symmetric] norm_minus_cancel
+      unfolding that(3)[symmetric] norm_minus_cancel
by (auto simp add: algebra_simps)
qed

have "?x =  norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))"
unfolding split_def setsum_subtractf ..
also have "\<dots> \<le> e + k"
-    apply (rule *[OF **, where ir="setsum (\<lambda>k. integral k f) r"])
-  proof -
-    case goal2
+    apply (rule *[OF **, where ir2="setsum (\<lambda>k. integral k f) r"])
+  proof goals
+    case 2
have *: "(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)"
apply (subst setsum.reindex_nontrivial)
apply fact
@@ -9554,7 +9560,7 @@
using ** q'(1) p'(1) setsum.union_disjoint [of "snd ` p" "q - snd ` p" "\<lambda>k. integral k f", symmetric]
by simp
next
-    case goal1
+    case 1
have *: "k * real (card r) / (1 + real (card r)) < k"
using k by (auto simp add: field_simps)
show ?case
@@ -9614,8 +9620,8 @@
show thesis
apply (rule that)
apply (rule d)
-  proof safe
-    case goal1
+  proof (safe, goals)
+    case (1 p)
note * = henstock_lemma_part2[OF assms(1) * d this]
show ?case
apply (rule le_less_trans[OF *])
@@ -9727,18 +9733,18 @@
by auto
next
case False
-  have fg: "\<forall>x\<in>cbox a b. \<forall> k. (f k x) \<bullet> 1 \<le> (g x) \<bullet> 1"
+  have fg: "\<forall>x\<in>cbox a b. \<forall>k. (f k x) \<bullet> 1 \<le> (g x) \<bullet> 1"
proof safe
-    case goal1
-    note assms(3)[rule_format,OF this]
-    note * = Lim_component_ge[OF this trivial_limit_sequentially]
-    show ?case
+    fix x k
+    assume x: "x \<in> cbox a b"
+    note * = Lim_component_ge[OF assms(3)[rule_format, OF x] trivial_limit_sequentially]
+    show "f k x \<bullet> 1 \<le> g x \<bullet> 1"
apply (rule *)
unfolding eventually_sequentially
apply (rule_tac x=k in exI)
apply -
apply (rule transitive_stepwise_le)
-      using assms(2)[rule_format,OF goal1]
+      using assms(2)[rule_format, OF x]
apply auto
done
qed
@@ -9770,9 +9776,8 @@

have "(g has_integral i) (cbox a b)"
unfolding has_integral
-  proof safe
-    case goal1
-    note e=this
+  proof (safe, goals)
+    case e: (1 e)
then have "\<forall>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral (cbox a b) (f k)) < e / 2 ^ (k + 2)))"
apply -
@@ -9784,36 +9789,32 @@

have "\<exists>r. \<forall>k\<ge>r. 0 \<le> i\<bullet>1 - (integral (cbox a b) (f k)) \<and> i\<bullet>1 - (integral (cbox a b) (f k)) < e / 4"
proof -
-      case goal1
have "e/4 > 0"
using e by auto
from LIMSEQ_D [OF i this] guess r ..
-      then show ?case
+      then show ?thesis
apply (rule_tac x=r in exI)
apply rule
apply (erule_tac x=k in allE)
-      proof -
-        case goal1
-        then show ?case
-          using i'[of k] by auto
-      qed
+        subgoal for k using i'[of k] by auto
+        done
qed
then guess r .. note r=conjunctD2[OF this[rule_format]]

have "\<forall>x\<in>cbox a b. \<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x)\<bullet>1 - (f k x)\<bullet>1 \<and>
(g x)\<bullet>1 - (f k x)\<bullet>1 < e / (4 * content(cbox a b))"
-    proof
-      case goal1
+    proof (rule, goals)
+      case (1 x)
have "e / (4 * content (cbox a b)) > 0"
using \<open>e>0\<close> False content_pos_le[of a b] by auto
-      from assms(3)[rule_format, OF goal1, THEN LIMSEQ_D, OF this]
+      from assms(3)[rule_format, OF 1, THEN LIMSEQ_D, OF this]
guess n .. note n=this
then show ?case
apply (rule_tac x="n + r" in exI)
apply safe
apply (erule_tac[2-3] x=k in allE)
unfolding dist_real_def
-        using fg[rule_format,OF goal1]
+        using fg[rule_format,OF 1]
apply (auto simp add: field_simps)
done
qed
@@ -9834,8 +9835,8 @@
then guess s .. note s=this
have *: "\<forall>a b c d. norm(a - b) \<le> e / 4 \<and> norm(b - c) < e / 2 \<and>
norm (c - d) < e / 4 \<longrightarrow> norm (a - d) < e"
-      proof safe
-        case goal1
+      proof (safe, goals)
+        case (1 a b c d)
then show ?case
using norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
norm_triangle_lt[of "a - b + (b - c)" "c - d" e]
@@ -9845,8 +9846,8 @@
show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e"
apply (rule *[rule_format,where
b="\<Sum>(x, k)\<in>p. content k *\<^sub>R f (m x) x" and c="\<Sum>(x, k)\<in>p. integral k (f (m x))"])
-      proof safe
-        case goal1
+      proof (safe, goals)
+        case 1
show ?case
apply (rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content (cbox a b)))"])
unfolding setsum_subtractf[symmetric]
@@ -9872,7 +9873,7 @@
qed (insert False, auto)

next
-        case goal2
+        case 2
show ?case
apply (rule le_less_trans[of _ "norm (\<Sum>j = 0..s.
\<Sum>(x, k)\<in>{xk\<in>p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))"])
@@ -9927,7 +9928,7 @@
qed
qed (insert s, auto)
next
-        case goal3
+        case 3
note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)]
have *: "\<And>sr sx ss ks kr::real. kr = sr \<longrightarrow> ks = ss \<longrightarrow>
ks \<le> i \<and> sr \<le> sx \<and> sx \<le> ss \<and> 0 \<le> i\<bullet>1 - kr\<bullet>1 \<and> i\<bullet>1 - kr\<bullet>1 < e/4 \<longrightarrow> abs (sx - i) < e/4"
@@ -9994,42 +9995,43 @@
and "bounded {integral s (f k)| k. True}"
shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
proof -
-  have lem: "\<And>f::nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real.
-    \<And>g s. \<forall>k.\<forall>x\<in>s. 0 \<le> f k x \<Longrightarrow> \<forall>k. (f k) integrable_on s \<Longrightarrow>
-      \<forall>k. \<forall>x\<in>s. f k x \<le> f (Suc k) x \<Longrightarrow> \<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially \<Longrightarrow>
-    bounded {integral s (f k)| k. True} \<Longrightarrow>
-    g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+  have lem: "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+    if "\<forall>k. \<forall>x\<in>s. 0 \<le> f k x"
+    and "\<forall>k. (f k) integrable_on s"
+    and "\<forall>k. \<forall>x\<in>s. f k x \<le> f (Suc k) x"
+    and "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially"
+    and "bounded {integral s (f k)| k. True}"
+    for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g s
proof -
-    case goal1
-    note assms=this[rule_format]
+    note assms=that[rule_format]
have "\<forall>x\<in>s. \<forall>k. (f k x)\<bullet>1 \<le> (g x)\<bullet>1"
apply safe
apply (rule Lim_component_ge)
-      apply (rule goal1(4)[rule_format])
+      apply (rule that(4)[rule_format])
apply assumption
apply (rule trivial_limit_sequentially)
unfolding eventually_sequentially
apply (rule_tac x=k in exI)
apply (rule transitive_stepwise_le)
-      using goal1(3)
+      using that(3)
apply auto
done
note fg=this[rule_format]

have "\<exists>i. ((\<lambda>k. integral s (f k)) ---> i) sequentially"
apply (rule bounded_increasing_convergent)
-      apply (rule goal1(5))
+      apply (rule that(5))
apply rule
apply (rule integral_le)
-      apply (rule goal1(2)[rule_format])+
-      using goal1(3)
+      apply (rule that(2)[rule_format])+
+      using that(3)
apply auto
done
then guess i .. note i=this
have "\<And>k. \<forall>x\<in>s. \<forall>n\<ge>k. f k x \<le> f n x"
apply rule
apply (rule transitive_stepwise_le)
-      using goal1(3)
+      using that(3)
apply auto
done
then have i': "\<forall>k. (integral s (f k))\<bullet>1 \<le> i\<bullet>1"
@@ -10043,7 +10045,7 @@
apply safe
apply (rule integral_component_le)
apply simp
-      apply (rule goal1(2)[rule_format])+
+      apply (rule that(2)[rule_format])+
apply auto
done

@@ -10060,25 +10062,25 @@
have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on cbox a b \<and>
((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> s then f k x else 0)) --->
integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0)) sequentially"
-    proof (rule monotone_convergence_interval, safe)
-      case goal1
+    proof (rule monotone_convergence_interval, safe, goals)
+      case 1
show ?case by (rule int)
next
-      case goal2
+      case (2 _ _ _ x)
then show ?case
apply (cases "x \<in> s")
using assms(3)
apply auto
done
next
-      case goal3
+      case (3 _ _ x)
then show ?case
apply (cases "x \<in> s")
using assms(4)
apply auto
done
next
-      case goal4
+      case (4 a b)
note * = integral_nonneg
have "\<And>k. norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f k x else 0)) \<le> norm (integral s (f k))"
unfolding real_norm_def
@@ -10089,7 +10091,7 @@
apply (drule assms(1))
prefer 3
apply (subst abs_of_nonneg)
-        apply (rule *[OF assms(2) goal1(1)[THEN spec]])
+        apply (rule *[OF assms(2) that(1)[THEN spec]])
apply (subst integral_restrict_univ[symmetric,OF int])
unfolding ifif
unfolding integral_restrict_univ[OF int']
@@ -10115,8 +10117,8 @@
unfolding has_integral_alt'
apply safe
apply (rule g(1))
-    proof -
-      case goal1
+    proof goals
+      case (1 e)
then have "e/4>0"
by auto
from LIMSEQ_D [OF i this] guess N .. note N=this
@@ -10153,8 +10155,8 @@
apply (rule integral_le[OF int int])
defer
apply (rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]])
-        proof safe
-          case goal2
+        proof (safe, goals)
+          case (2 x)
have "\<And>m. x \<in> s \<Longrightarrow> \<forall>n\<ge>m. (f m x)\<bullet>1 \<le> (f n x)\<bullet>1"
apply (rule transitive_stepwise_le)
using assms(3)
@@ -10163,7 +10165,7 @@
then show ?case
by auto
next
-          case goal1
+          case 1
show ?case
apply (subst integral_restrict_univ[symmetric,OF int])
unfolding ifif integral_restrict_univ[OF int']
@@ -10174,7 +10176,7 @@
qed
qed
qed
-    then show ?case
+    then show ?thesis
apply safe
defer
apply (drule integral_unique)
@@ -10198,23 +10200,23 @@
integral s (\<lambda>x. g x - f 0 x)) sequentially"
apply (rule lem)
apply safe
-  proof -
-    case goal1
+  proof goals
+    case (1 k x)
then show ?case
using *[of x 0 "Suc k"] by auto
next
-    case goal2
+    case (2 k)
then show ?case
apply (rule integrable_sub)
using assms(1)
apply auto
done
next
-    case goal3
+    case (3 k x)
then show ?case
using *[of x "Suc k" "Suc (Suc k)"] by auto
next
-    case goal4
+    case (4 x)
then show ?case
apply -
apply (rule tendsto_diff)
@@ -10222,7 +10224,7 @@
apply auto
done
next
-    case goal5
+    case 5
then show ?case
using assms(4)
unfolding bounded_iff
@@ -10352,43 +10354,44 @@
and "\<forall>x\<in>s. norm (f x) \<le> g x"
shows "norm (integral s f) \<le> integral s g"
proof -
-  have *: "\<And>x y. (\<forall>e::real. 0 < e \<longrightarrow> x < y + e) \<longrightarrow> x \<le> y"
-    apply safe
+  have *: "\<And>x y. (\<forall>e::real. 0 < e \<longrightarrow> x < y + e) \<Longrightarrow> x \<le> y"
apply (rule ccontr)
apply (erule_tac x="x - y" in allE)
apply auto
done
-  have "\<And>e sg dsa dia ig.
-    norm sg \<le> dsa \<longrightarrow> abs (dsa - dia) < e / 2 \<longrightarrow> norm (sg - ig) < e / 2 \<longrightarrow> norm ig < dia + e"
-  proof safe
-    case goal1
-    show ?case
-      apply (rule le_less_trans[OF norm_triangle_sub[of ig sg]])
-      apply (subst real_sum_of_halves[of e,symmetric])
-      apply (rule add_le_less_mono)
-      defer
-      apply (subst norm_minus_commute)
-      apply (rule goal1)
-      apply (rule order_trans[OF goal1(1)])
-      using goal1(2)
-      apply arith
-      done
-  qed
-  note norm=this[rule_format]
-  have lem: "\<And>f::'n \<Rightarrow> 'a. \<And>g a b. f integrable_on cbox a b \<Longrightarrow> g integrable_on cbox a b \<Longrightarrow>
-    \<forall>x\<in>cbox a b. norm (f x) \<le> g x \<Longrightarrow> norm (integral(cbox a b) f) \<le> integral (cbox a b) g"
+  have norm: "norm ig < dia + e"
+    if "norm sg \<le> dsa"
+    and "abs (dsa - dia) < e / 2"
+    and "norm (sg - ig) < e / 2"
+    for e dsa dia and sg ig :: 'a
+    apply (rule le_less_trans[OF norm_triangle_sub[of ig sg]])
+    apply (subst real_sum_of_halves[of e,symmetric])
+    apply (rule add_le_less_mono)
+    defer
+    apply (subst norm_minus_commute)
+    apply (rule that(3))
+    apply (rule order_trans[OF that(1)])
+    using that(2)
+    apply arith
+    done
+  have lem: "norm (integral(cbox a b) f) \<le> integral (cbox a b) g"
+    if "f integrable_on cbox a b"
+    and "g integrable_on cbox a b"
+    and "\<forall>x\<in>cbox a b. norm (f x) \<le> g x"
+    for f :: "'n \<Rightarrow> 'a" and g a b
proof (rule *[rule_format])
-    case goal1
+    fix e :: real
+    assume "e > 0"
then have *: "e/2 > 0"
by auto
-    from integrable_integral[OF goal1(1),unfolded has_integral[of f],rule_format,OF *]
+    from integrable_integral[OF that(1),unfolded has_integral[of f],rule_format,OF *]
guess d1 .. note d1 = conjunctD2[OF this,rule_format]
-    from integrable_integral[OF goal1(2),unfolded has_integral[of g],rule_format,OF *]
+    from integrable_integral[OF that(2),unfolded has_integral[of g],rule_format,OF *]
guess d2 .. note d2 = conjunctD2[OF this,rule_format]
note gauge_inter[OF d1(1) d2(1)]
from fine_division_exists[OF this, of a b] guess p . note p=this
-    show ?case
+    show "norm (integral (cbox a b) f) < integral (cbox a b) g + e"
apply (rule norm)
defer
apply (rule d2(2)[OF conjI[OF p(1)],unfolded real_norm_def])
@@ -10405,7 +10408,7 @@
unfolding uv norm_scaleR
unfolding abs_of_nonneg[OF content_pos_le] real_scaleR_def
apply (rule mult_left_mono)
-        using goal1(3) as
+        using that(3) as
apply auto
done
qed (insert p[unfolded fine_inter], auto)
@@ -10534,9 +10537,10 @@
assumes "f absolutely_integrable_on UNIV"
obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
apply (rule that[of "integral UNIV (\<lambda>x. norm (f x))"])
-proof safe
-  case goal1
-  note d = division_ofD[OF this(2)]
+  apply safe
+proof goals
+  case (1 d)
+  note d = division_ofD[OF 1(2)]
have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. integral i (\<lambda>x. norm (f x)))"
apply (rule setsum_mono,rule absolutely_integrable_le)
apply (drule d(4))
@@ -10545,14 +10549,14 @@
apply auto
done
also have "\<dots> \<le> integral (\<Union>d) (\<lambda>x. norm (f x))"
-    apply (subst integral_combine_division_topdown[OF _ goal1(2)])
-    using integrable_on_subdivision[OF goal1(2)]
+    apply (subst integral_combine_division_topdown[OF _ 1(2)])
+    using integrable_on_subdivision[OF 1(2)]
using assms
apply auto
done
also have "\<dots> \<le> integral UNIV (\<lambda>x. norm (f x))"
apply (rule integral_subset_le)
-    using integrable_on_subdivision[OF goal1(2)]
+    using integrable_on_subdivision[OF 1(2)]
using assms
apply auto
done
@@ -10586,8 +10590,9 @@
show ?thesis
apply (rule absolutely_integrable_onI [OF f has_integral_integrable])
apply (subst has_integral[of _ ?S])
-  proof safe
-    case goal1
+    apply safe
+  proof goals
+    case (1 e)
then have "?S - e / 2 < ?S" by simp
then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
unfolding less_cSUP_iff[OF D] by auto
@@ -10595,7 +10600,7 @@

have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
proof
-      case goal1
+      fix x
have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
apply (rule separate_point_closed)
apply (rule closed_Union)
@@ -10603,13 +10608,13 @@
using d'(4)
apply auto
done
-      then show ?case
+      then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
by force
qed
from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]

have "e/2 > 0"
-      using goal1 by auto
+      using 1 by auto
from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format]
let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
show ?case
@@ -10720,23 +10725,23 @@
by (force intro!: helplemma)

have p'alt: "p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}}"
-      proof safe
-        case goal2
+      proof (safe, goals)
+        case (2 _ _ x i l)
have "x \<in> i"
-          using fineD[OF p(3) goal2(1)] k(2)[OF goal2(2), of x] goal2(4-)
+          using fineD[OF p(3) 2(1)] k(2)[OF 2(2), of x] 2(4-)
by auto
then have "(x, i \<inter> l) \<in> p'"
unfolding p'_def
-          using goal2
+          using 2
apply safe
apply (rule_tac x=x in exI)
apply (rule_tac x="i \<inter> l" in exI)
apply safe
-          using goal2
+          using 2
apply auto
done
then show ?case
-          using goal2(3) by auto
+          using 2(3) by auto
next
fix x k
assume "(x, k) \<in> p'"
@@ -10768,18 +10773,18 @@
apply (rule *[rule_format,OF **])
apply safe
apply(rule d(2))
-      proof -
-        case goal1 show ?case
+      proof goals
+        case 1
+        show ?case
by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
next
-        case goal2
+        case 2
have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
(\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}"
by auto
have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
-        proof (rule setsum_mono)
-          case goal1
-          note k=this
+        proof (rule setsum_mono, goals)
+          case k: (1 k)
from d'(4)[OF this] guess u v by (elim exE) note uv=this
def d' \<equiv> "{cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
note uvab = d'(2)[OF k[unfolded uv]]
@@ -10804,13 +10809,13 @@
apply fact
unfolding d'_def uv
apply blast
-          proof
-            case goal1
+          proof (rule, goals)
+            case (1 i)
then have "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
by auto
from this[unfolded mem_Collect_eq] guess l .. note l=this
then have "cbox u v \<inter> l = {}"
-              using goal1 by auto
+              using 1 by auto
then show ?case
using l by auto
qed
@@ -10819,18 +10824,18 @@
apply (rule setsum.reindex_nontrivial [unfolded o_def])
apply (rule finite_imageI)
apply (rule p')
-          proof -
-            case goal1
+          proof goals
+            case (1 l y)
have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
apply (subst(2) interior_inter)
apply (rule Int_greatest)
defer
-              apply (subst goal1(4))
+              apply (subst 1(4))
apply auto
done
then have *: "interior (k \<inter> l) = {}"
-              using snd_p(5)[OF goal1(1-3)] by auto
-            from d'(4)[OF k] snd_p(4)[OF goal1(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
+              using snd_p(5)[OF 1(1-3)] by auto
+            from d'(4)[OF k] snd_p(4)[OF 1(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
show ?case
using *
unfolding uv inter_interval content_eq_0_interior[symmetric]
@@ -10895,10 +10900,9 @@
apply fact
apply (rule finite_imageI[OF p'(1)])
apply safe
-        proof -
-          case goal2
-          have "ia \<inter> b = {}"
-            using goal2
+        proof goals
+          case (2 i ia l a b)
+          then have "ia \<inter> b = {}"
unfolding p'alt image_iff Bex_def not_ex
apply (erule_tac x="(a, ia \<inter> b)" in allE)
apply auto
@@ -10906,7 +10910,7 @@
then show ?case
by auto
next
-          case goal1
+          case (1 x a b)
then show ?case
unfolding p'_def
apply safe
@@ -10920,7 +10924,7 @@
qed
finally show ?case .
next
-        case goal3
+        case 3
let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
have Sigma_alt: "\<And>s t. s \<times> t = {(i, j) |i j. i \<in> s \<and> j \<in> t}"
by auto
@@ -11007,19 +11011,19 @@
unfolding simple_image
apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
apply (rule d')
-          proof -
-            case goal1
+          proof goals
+            case (1 k y)
from d'(4)[OF this(1)] d'(4)[OF this(2)]
guess u1 v1 u2 v2 by (elim exE) note uv=this
have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
apply (subst interior_inter)
-              using d'(5)[OF goal1(1-3)]
+              using d'(5)[OF 1(1-3)]
apply auto
done
also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
by auto
also have "\<dots> = interior (k \<inter> cbox u v)"
-              unfolding goal1(4) by auto
+              unfolding 1(4) by auto
finally show ?case
unfolding uv inter_interval content_eq_0_interior ..
qed
@@ -11031,15 +11035,15 @@
apply blast
apply safe
apply (rule_tac x=k in exI)
-          proof -
-            case goal1
+          proof goals
+            case (1 i k)
from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
have "interior (k \<inter> cbox u v) \<noteq> {}"
-              using goal1(2)
+              using 1(2)
unfolding ab inter_interval content_eq_0_interior
by auto
then show ?case
-              using goal1(1)
+              using 1(1)
using interior_subset[of "k \<inter> cbox u v"]
by auto
qed
@@ -11081,19 +11085,19 @@
show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
apply (subst has_integral_alt')
apply safe
-  proof -
-    case goal1
+  proof goals
+    case (1 a b)
show ?case
using f_int[of a b] by auto
next
-    case goal2
+    case (2 e)
have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
proof (rule ccontr)
assume "\<not> ?thesis"
then have "?S \<le> ?S - e"
by (intro cSUP_least[OF D(1)]) auto
then show False
-        using goal2 by auto
+        using 2 by auto
qed
then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
"SUPREMUM {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
@@ -11120,8 +11124,8 @@
apply (rule *[rule_format])
apply safe
apply (rule d(2))
-      proof -
-        case goal1
+      proof goals
+        case 1
have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
apply (rule setsum_mono)
apply (rule absolutely_integrable_le)
@@ -11138,14 +11142,13 @@
done
also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
proof -
-          case goal1
have "\<Union>d \<subseteq> cbox a b"
apply rule
apply (drule K(2)[rule_format])
apply (rule ab[unfolded subset_eq,rule_format])
apply (auto simp add: dist_norm)
done
-          then show ?case
+          then show ?thesis
apply -
apply (subst if_P)
apply rule
@@ -11247,10 +11250,11 @@
apply (rule bounded_variation_absolutely_integrable[of _ "B1+B2"])
prefer 3
-  proof safe
-    case goal1
+    apply safe
+  proof goals
+    case (1 d)
have "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k \<and> g integrable_on k"
-      apply (drule division_ofD(4)[OF goal1])
+      apply (drule division_ofD(4)[OF 1])
apply safe
apply (rule_tac[!] integrable_on_subcbox[of _ UNIV])
using assms
@@ -11267,7 +11271,7 @@
apply auto
done
also have "\<dots> \<le> B1 + B2"
-      using B(1)[OF goal1] B(2)[OF goal1] by auto
+      using B(1)[OF 1] B(2)[OF 1] by auto
finally show ?case .
qed (insert assms, auto)
qed
@@ -11305,14 +11309,15 @@
show "(h \<circ> f) absolutely_integrable_on UNIV"
apply (rule bounded_variation_absolutely_integrable[of _ "B * b"])
apply (rule integrable_linear[OF _ assms(2)])
-  proof safe
-    case goal2
+    apply safe
+  proof goals
+    case (2 d)
have "(\<Sum>k\<in>d. norm (integral k (h \<circ> f))) \<le> setsum (\<lambda>k. norm(integral k f)) d * b"
unfolding setsum_left_distrib
apply (rule setsum_mono)
-    proof -
-      case goal1
-      from division_ofD(4)[OF goal2 this]
+    proof goals
+      case (1 k)
+      from division_ofD(4)[OF 2 this]
guess u v by (elim exE) note uv=this
have *: "f integrable_on k"
unfolding uv
@@ -11328,7 +11333,7 @@
qed
also have "\<dots> \<le> B * b"
apply (rule mult_right_mono)
-      using B goal2 b
+      using B 2 b
apply auto
done
finally show ?case .
@@ -11450,8 +11455,8 @@
show "f absolutely_integrable_on UNIV"
apply (rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"])
apply safe
-  proof -
-    case goal1
+  proof goals
+    case (1 d)
note d=this and d'=division_ofD[OF this]
have "(\<Sum>k\<in>d. norm (integral k f)) \<le>
(\<Sum>k\<in>d. setsum (op \<bullet> (integral k (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m))) Basis)"
@@ -11481,8 +11486,8 @@
also have "\<dots> \<le> setsum (op \<bullet> (integral UNIV (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m))) Basis"
apply (subst setsum.commute)
apply (rule setsum_mono)
-    proof -
-      case goal1
+    proof goals
+      case (1 j)
have *: "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) integrable_on \<Union>d"
using integrable_on_subdivision[OF d assms(2)] by auto
have "(\<Sum>i\<in>d. integral i (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) \<bullet> j) =
@@ -11535,9 +11540,10 @@
assume assms: "\<forall>x. norm (f x) \<le> g x" "f integrable_on UNIV" "g integrable_on UNIV"
show "f absolutely_integrable_on UNIV"
apply (rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"])
-  proof safe
-    case goal1
-    note d=this and d'=division_ofD[OF this]
+    apply safe
+  proof goals
+    case d: (1 d)
+    note d'=division_ofD[OF d]
have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>k\<in>d. integral k g)"
apply (rule setsum_mono)
apply (rule integral_norm_bound_integral)
@@ -11725,9 +11731,8 @@
by (rule cInf_superset_mono) auto
let ?S = "{f j x| j. m \<le> j}"
show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> Inf ?S) sequentially"
-    proof (rule LIMSEQ_I)
-      case goal1
-      note r = this
+    proof (rule LIMSEQ_I, goals)
+      case r: (1 r)

have "\<exists>y\<in>?S. y < Inf ?S + r"
by (subst cInf_less_iff[symmetric]) (auto simp: \<open>x\<in>s\<close> r)
@@ -11736,8 +11741,9 @@

show ?case
apply (rule_tac x=N in exI)
-      proof safe
-        case goal1
+        apply safe
+      proof goals
+        case (1 n)
have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - Inf ?S) < r"
by arith
show ?case
@@ -11745,7 +11751,7 @@
apply (rule *[rule_format, OF N(1)])
apply (rule cInf_superset_mono, auto simp: \<open>x\<in>s\<close>) []
apply (rule cInf_lower)
-            using N goal1
+            using N 1
apply auto []
apply simp
done
@@ -11796,8 +11802,8 @@
by (rule cSup_subset_mono) auto
let ?S = "{f j x| j. m \<le> j}"
show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> Sup ?S) sequentially"
-    proof (rule LIMSEQ_I)
-      case goal1 note r=this
+    proof (rule LIMSEQ_I, goals)
+      case r: (1 r)
have "\<exists>y\<in>?S. Sup ?S - r < y"
by (subst less_cSup_iff[symmetric]) (auto simp: r \<open>x\<in>s\<close>)
then obtain N where N: "Sup ?S - r < f N x" "m \<le> N"
@@ -11805,8 +11811,9 @@

show ?case
apply (rule_tac x=N in exI)
-      proof safe
-        case goal1
+        apply safe
+      proof goals
+        case (1 n)
have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - Sup ?S) < r"
by arith
show ?case
@@ -11814,7 +11821,7 @@
apply (rule *[rule_format, OF N(1)])
apply (rule cSup_subset_mono, auto simp: \<open>x\<in>s\<close>) []
apply (subst cSup_upper)
-          using N goal1
+          using N 1
apply auto
done
qed
@@ -11849,20 +11856,21 @@
by (intro cInf_superset_mono) (auto simp: \<open>x\<in>s\<close>)

show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
-    proof (rule LIMSEQ_I)
-      case goal1
+    proof (rule LIMSEQ_I, goals)
+      case r: (1 r)
then have "0<r/2"
by auto
from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N = this
show ?case
-        apply (rule_tac x=N in exI,safe)
+        apply (rule_tac x=N in exI)
+        apply safe
unfolding real_norm_def
apply (rule le_less_trans[of _ "r/2"])
apply (rule cInf_asclose)
apply safe
defer
apply (rule less_imp_le)
-        using N goal1
+        using N r
apply auto
done
qed
@@ -11896,8 +11904,8 @@
show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
by (rule cSup_subset_mono) (auto simp: \<open>x\<in>s\<close>)
show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
-    proof (rule LIMSEQ_I)
-      case goal1
+    proof (rule LIMSEQ_I, goals)
+      case r: (1 r)
then have "0<r/2"
by auto
from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N=this
@@ -11909,7 +11917,7 @@
apply safe
defer
apply (rule less_imp_le)
-        using N goal1
+        using N r
apply auto
done
qed
@@ -11918,10 +11926,10 @@

show "g integrable_on s" by fact
show "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
-  proof (rule LIMSEQ_I)
-    case goal1
-    from LIMSEQ_D [OF inc2(2) goal1] guess N1 .. note N1=this[unfolded real_norm_def]
-    from LIMSEQ_D [OF dec2(2) goal1] guess N2 .. note N2=this[unfolded real_norm_def]
+  proof (rule LIMSEQ_I, goals)
+    case r: (1 r)
+    from LIMSEQ_D [OF inc2(2) r] guess N1 .. note N1=this[unfolded real_norm_def]
+    from LIMSEQ_D [OF dec2(2) r] guess N2 .. note N2=this[unfolded real_norm_def]
show ?case
proof (rule_tac x="N1+N2" in exI, safe)
fix n