renamed method "goals" to "goal_cases" to emphasize its meaning;
authorwenzelm
Sun Sep 13 20:20:16 2015 +0200 (2015-09-13)
changeset 611665976fe402824
parent 61165 8020249565fb
child 61167 34f782641caa
renamed method "goals" to "goal_cases" to emphasize its meaning;
NEWS
src/Doc/Isar_Ref/Proof.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Library/Cardinality.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Product_Order.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Multivariate_Analysis/Fashoda.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Nominal/Examples/Pattern.thy
src/HOL/Number_Theory/Eratosthenes.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/ZF/Games.thy
src/HOL/ex/Tree23.thy
src/Pure/Isar/method.ML
     1.1 --- a/NEWS	Sun Sep 13 16:50:12 2015 +0200
     1.2 +++ b/NEWS	Sun Sep 13 20:20:16 2015 +0200
     1.3 @@ -116,13 +116,13 @@
     1.4  sequences. Further explanations and examples are given in the isar-ref
     1.5  manual.
     1.6  
     1.7 -* Proof method "goals" turns the current subgoals into cases within the
     1.8 -context; the conclusion is bound to variable ?case in each case.
     1.9 -For example:
    1.10 +* Proof method "goal_cases" turns the current subgoals into cases within
    1.11 +the context; the conclusion is bound to variable ?case in each case. For
    1.12 +example:
    1.13  
    1.14  lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
    1.15    and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
    1.16 -proof goals
    1.17 +proof goal_cases
    1.18    case (1 x)
    1.19    then show ?case using \<open>A x\<close> \<open>B x\<close> sorry
    1.20  next
    1.21 @@ -132,7 +132,7 @@
    1.22  
    1.23  lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
    1.24    and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
    1.25 -proof goals
    1.26 +proof goal_cases
    1.27    case prems: 1
    1.28    then show ?case using prems sorry
    1.29  next
     2.1 --- a/src/Doc/Isar_Ref/Proof.thy	Sun Sep 13 16:50:12 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Sun Sep 13 20:20:16 2015 +0200
     2.3 @@ -832,7 +832,7 @@
     2.4    \begin{matharray}{rcl}
     2.5      @{command_def "print_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\[0.5ex]
     2.6      @{method_def "-"} & : & @{text method} \\
     2.7 -    @{method_def "goals"} & : & @{text method} \\
     2.8 +    @{method_def "goal_cases"} & : & @{text method} \\
     2.9      @{method_def "fact"} & : & @{text method} \\
    2.10      @{method_def "assumption"} & : & @{text method} \\
    2.11      @{method_def "this"} & : & @{text method} \\
    2.12 @@ -847,7 +847,7 @@
    2.13    \end{matharray}
    2.14  
    2.15    @{rail \<open>
    2.16 -    @@{method goals} (@{syntax name}*)
    2.17 +    @@{method goal_cases} (@{syntax name}*)
    2.18      ;
    2.19      @@{method fact} @{syntax thmrefs}?
    2.20      ;
    2.21 @@ -886,7 +886,7 @@
    2.22    method; thus a plain \emph{do-nothing} proof step would be ``@{command
    2.23    "proof"}~@{text "-"}'' rather than @{command "proof"} alone.
    2.24  
    2.25 -  \item @{method "goals"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} turns the current subgoals
    2.26 +  \item @{method "goal_cases"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} turns the current subgoals
    2.27    into cases within the context (see also \secref{sec:cases-induct}). The
    2.28    specified case names are used if present; otherwise cases are numbered
    2.29    starting from 1.
     3.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Sep 13 16:50:12 2015 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Sep 13 20:20:16 2015 +0200
     3.3 @@ -578,7 +578,7 @@
     3.4  begin
     3.5  
     3.6  sublocale dlo: unbounded_dense_linorder
     3.7 -proof (unfold_locales, goals)
     3.8 +proof (unfold_locales, goal_cases)
     3.9    case (1 x y)
    3.10    then show ?case
    3.11      using between_less [of x y] by auto
     4.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Sep 13 16:50:12 2015 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Sep 13 20:20:16 2015 +0200
     4.3 @@ -891,7 +891,7 @@
     4.4  subsection \<open>Miscellaneous lemmas about indexes, decrementation, substitution  etc ...\<close>
     4.5  
     4.6  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
     4.7 -proof (induct p arbitrary: n rule: poly.induct, auto, goals)
     4.8 +proof (induct p arbitrary: n rule: poly.induct, auto, goal_cases)
     4.9    case prems: (1 c n p n')
    4.10    then have "n = Suc (n - 1)"
    4.11      by simp
     5.1 --- a/src/HOL/Library/Cardinality.thy	Sun Sep 13 16:50:12 2015 +0200
     5.2 +++ b/src/HOL/Library/Cardinality.thy	Sun Sep 13 20:20:16 2015 +0200
     5.3 @@ -479,7 +479,7 @@
     5.4    and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs"
     5.5    and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
     5.6    and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
     5.7 -proof goals
     5.8 +proof goal_cases
     5.9    {
    5.10      case 1
    5.11      show ?case (is "?lhs \<longleftrightarrow> ?rhs")
     6.1 --- a/src/HOL/Library/Extended_Real.thy	Sun Sep 13 16:50:12 2015 +0200
     6.2 +++ b/src/HOL/Library/Extended_Real.thy	Sun Sep 13 20:20:16 2015 +0200
     6.3 @@ -333,7 +333,7 @@
     6.4  | "ereal r + -\<infinity> = - \<infinity>"
     6.5  | "-\<infinity> + ereal p = -(\<infinity>::ereal)"
     6.6  | "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
     6.7 -proof goals
     6.8 +proof goal_cases
     6.9    case prems: (1 P x)
    6.10    then obtain a b where "x = (a, b)"
    6.11      by (cases x) auto
    6.12 @@ -437,7 +437,7 @@
    6.13  | "ereal x    < \<infinity>           \<longleftrightarrow> True"
    6.14  | "        -\<infinity> < ereal r     \<longleftrightarrow> True"
    6.15  | "        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
    6.16 -proof goals
    6.17 +proof goal_cases
    6.18    case prems: (1 P x)
    6.19    then obtain a b where "x = (a,b)" by (cases x) auto
    6.20    with prems show P by (cases rule: ereal2_cases[of a b]) auto
    6.21 @@ -860,7 +860,7 @@
    6.22  | "-(\<infinity>::ereal) * \<infinity> = -\<infinity>"
    6.23  | "(\<infinity>::ereal) * -\<infinity> = -\<infinity>"
    6.24  | "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
    6.25 -proof goals
    6.26 +proof goal_cases
    6.27    case prems: (1 P x)
    6.28    then obtain a b where "x = (a, b)"
    6.29      by (cases x) auto
     7.1 --- a/src/HOL/Library/Product_Order.thy	Sun Sep 13 16:50:12 2015 +0200
     7.2 +++ b/src/HOL/Library/Product_Order.thy	Sun Sep 13 20:20:16 2015 +0200
     7.3 @@ -233,7 +233,7 @@
     7.4  (* Contribution: Alessandro Coglio *)
     7.5  
     7.6  instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
     7.7 -proof (standard, goals)
     7.8 +proof (standard, goal_cases)
     7.9    case 1
    7.10    then show ?case
    7.11      by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
     8.1 --- a/src/HOL/Library/While_Combinator.thy	Sun Sep 13 16:50:12 2015 +0200
     8.2 +++ b/src/HOL/Library/While_Combinator.thy	Sun Sep 13 20:20:16 2015 +0200
     8.3 @@ -157,7 +157,7 @@
     8.4      note b = this(1) and body = this(2) and inv = this(3)
     8.5      hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
     8.6      ultimately show ?thesis unfolding Suc using b
     8.7 -    proof (intro Least_equality[symmetric], goals)
     8.8 +    proof (intro Least_equality[symmetric], goal_cases)
     8.9        case 1
    8.10        hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
    8.11          by (auto simp: BodyCommute inv b)
     9.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 13 16:50:12 2015 +0200
     9.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 13 20:20:16 2015 +0200
     9.3 @@ -175,7 +175,7 @@
     9.4    qed
     9.5    have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
     9.6      unfolding subset_eq
     9.7 -  proof (rule, goals)
     9.8 +  proof (rule, goal_cases)
     9.9      case (1 x)
    9.10      then obtain y :: "real^2" where y:
    9.11          "y \<in> cbox (- 1) 1"
    9.12 @@ -834,7 +834,7 @@
    9.13        z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
    9.14        z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
    9.15        z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
    9.16 -    proof (simp only: segment_vertical segment_horizontal vector_2, goals)
    9.17 +    proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
    9.18        case as: 1
    9.19        have "pathfinish f \<in> cbox a b"
    9.20          using assms(3) pathfinish_in_path_image[of f] by auto 
    10.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Sep 13 16:50:12 2015 +0200
    10.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Sep 13 20:20:16 2015 +0200
    10.3 @@ -2392,7 +2392,7 @@
    10.4    have lem: "\<And>(f :: 'n \<Rightarrow> 'a) y a b.
    10.5      (f has_integral y) (cbox a b) \<Longrightarrow> ((h o f) has_integral h y) (cbox a b)"
    10.6      unfolding has_integral
    10.7 -  proof (clarify, goals)
    10.8 +  proof (clarify, goal_cases)
    10.9      case (1 f y a b e)
   10.10      from pos_bounded
   10.11      obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
   10.12 @@ -2441,7 +2441,7 @@
   10.13        using has_integral_altD[OF assms(1) as *] by blast
   10.14      show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
   10.15        (\<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)"
   10.16 -    proof (rule_tac x=M in exI, clarsimp simp add: M, goals)
   10.17 +    proof (rule_tac x=M in exI, clarsimp simp add: M, goal_cases)
   10.18        case (1 a b)
   10.19        obtain z where z:
   10.20          "((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b)"
   10.21 @@ -2553,7 +2553,7 @@
   10.22    }
   10.23    assume as: "\<not> (\<exists>a b. s = cbox a b)"
   10.24    then show ?thesis
   10.25 -  proof (subst has_integral_alt, clarsimp, goals)
   10.26 +  proof (subst has_integral_alt, clarsimp, goal_cases)
   10.27      case (1 e)
   10.28      then have *: "e / 2 > 0"
   10.29        by auto
   10.30 @@ -2809,7 +2809,7 @@
   10.31    assume ?l
   10.32    then guess y unfolding integrable_on_def has_integral .. note y=this
   10.33    show "\<forall>e>0. \<exists>d. ?P e d"
   10.34 -  proof (clarify, goals)
   10.35 +  proof (clarify, goal_cases)
   10.36      case (1 e)
   10.37      then have "e/2 > 0" by auto
   10.38      then guess d
   10.39 @@ -2844,7 +2844,7 @@
   10.40    have dp: "\<And>i n. i\<le>n \<Longrightarrow> d i fine p n"
   10.41      using p(2) unfolding fine_inters by auto
   10.42    have "Cauchy (\<lambda>n. setsum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))"
   10.43 -  proof (rule CauchyI, goals)
   10.44 +  proof (rule CauchyI, goal_cases)
   10.45      case (1 e)
   10.46      then guess N unfolding real_arch_inv[of e] .. note N=this
   10.47      show ?case
   10.48 @@ -3104,7 +3104,7 @@
   10.49        and fj: "(f has_integral j) (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
   10.50        and k: "k \<in> Basis"
   10.51    shows "(f has_integral (i + j)) (cbox a b)"
   10.52 -proof (unfold has_integral, rule, rule, goals)
   10.53 +proof (unfold has_integral, rule, rule, goal_cases)
   10.54    case (1 e)
   10.55    then have e: "e/2 > 0"
   10.56      by auto
   10.57 @@ -4748,7 +4748,7 @@
   10.58    assumes k: "k \<in> Basis"
   10.59    shows "negligible {x. x\<bullet>k = c}"
   10.60    unfolding negligible_def has_integral
   10.61 -proof (clarify, goals)
   10.62 +proof (clarify, goal_cases)
   10.63    case (1 a b e)
   10.64    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"
   10.65      by (rule content_doublesplit)
   10.66 @@ -4823,7 +4823,7 @@
   10.67          apply (auto simp add:interval_doublesplit[OF k])
   10.68          done
   10.69        also have "\<dots> < e"
   10.70 -      proof (subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]], goals)
   10.71 +      proof (subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases)
   10.72          case (1 u v)
   10.73          have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
   10.74            unfolding interval_doublesplit[OF k]
   10.75 @@ -5112,7 +5112,7 @@
   10.76    assume assm: "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
   10.77    show "(f has_integral 0) (cbox a b)"
   10.78      unfolding has_integral
   10.79 -  proof (safe, goals)
   10.80 +  proof (safe, goal_cases)
   10.81      case (1 e)
   10.82      then have "\<And>n. e / 2 / ((real n+1) * (2 ^ n)) > 0"
   10.83        apply -
   10.84 @@ -5240,7 +5240,7 @@
   10.85            done
   10.86        qed (insert as, auto)
   10.87        also have "\<dots> \<le> setsum (\<lambda>i. e / 2 / 2 ^ i) {..N+1}"
   10.88 -      proof (rule setsum_mono, goals)
   10.89 +      proof (rule setsum_mono, goal_cases)
   10.90          case (1 i)
   10.91          then show ?case
   10.92            apply (subst mult.commute, subst pos_le_divide_eq[symmetric])
   10.93 @@ -5347,7 +5347,7 @@
   10.94      and "t \<subseteq> s"
   10.95    shows "negligible t"
   10.96    unfolding negligible_def
   10.97 -proof (safe, goals)
   10.98 +proof (safe, goal_cases)
   10.99    case (1 a b)
  10.100    show ?case
  10.101      using assms(1)[unfolded negligible_def,rule_format,of a b]
  10.102 @@ -5376,7 +5376,7 @@
  10.103      and "negligible t"
  10.104    shows "negligible (s \<union> t)"
  10.105    unfolding negligible_def
  10.106 -proof (safe, goals)
  10.107 +proof (safe, goal_cases)
  10.108    case (1 a b)
  10.109    note assm = assms[unfolded negligible_def,rule_format,of a b]
  10.110    then show ?case
  10.111 @@ -5584,7 +5584,7 @@
  10.112    show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
  10.113      apply (rule_tac x="?g" in exI)
  10.114      apply safe
  10.115 -  proof goals
  10.116 +  proof goal_cases
  10.117      case (1 x)
  10.118      then show ?case
  10.119        apply -
  10.120 @@ -6074,7 +6074,7 @@
  10.121      "f b = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
  10.122    and taylor_integrable:
  10.123      "i integrable_on {a .. b}"
  10.124 -proof goals
  10.125 +proof goal_cases
  10.126    case 1
  10.127    interpret bounded_bilinear "scaleR::real\<Rightarrow>'a\<Rightarrow>'a"
  10.128      by (rule bounded_bilinear_scaleR)
  10.129 @@ -6431,7 +6431,7 @@
  10.130    let ?I = "\<lambda>a b. integral {a .. b} f"
  10.131    show "\<exists>d>0. \<forall>y\<in>{a .. b}. norm (y - x) < d \<longrightarrow>
  10.132      norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \<le> e * norm (y - x)"
  10.133 -  proof (rule, rule, rule d, safe, goals)
  10.134 +  proof (rule, rule, rule d, safe, goal_cases)
  10.135      case (1 y)
  10.136      show ?case
  10.137      proof (cases "y < x")
  10.138 @@ -6565,7 +6565,7 @@
  10.139    show ?thesis
  10.140      apply (rule that[of g])
  10.141      apply safe
  10.142 -  proof goals
  10.143 +  proof goal_cases
  10.144      case (1 u v)
  10.145      have "\<forall>x\<in>cbox u v. (g has_vector_derivative f x) (at x within cbox u v)"
  10.146        apply rule
  10.147 @@ -6598,7 +6598,7 @@
  10.148      defer
  10.149      apply (rule *)
  10.150      apply assumption
  10.151 -  proof goals
  10.152 +  proof goal_cases
  10.153      case 1
  10.154      then show ?thesis
  10.155        unfolding 1 assms(8)[unfolded 1 has_integral_empty_eq] by auto
  10.156 @@ -7185,7 +7185,7 @@
  10.157    let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))"
  10.158    show "?P e"
  10.159      apply (rule_tac x="?d" in exI)
  10.160 -  proof (safe, goals)
  10.161 +  proof (safe, goal_cases)
  10.162      case 1
  10.163      show ?case
  10.164        apply (rule gauge_ball_dependent)
  10.165 @@ -7207,7 +7207,7 @@
  10.166        apply (subst(2) pA)
  10.167        apply (subst pA)
  10.168        unfolding setsum.union_disjoint[OF pA(2-)]
  10.169 -    proof (rule norm_triangle_le, rule **, goals)
  10.170 +    proof (rule norm_triangle_le, rule **, goal_cases)
  10.171        case 1
  10.172        show ?case
  10.173          apply (rule order_trans)
  10.174 @@ -7295,7 +7295,7 @@
  10.175            defer
  10.176            apply rule
  10.177            unfolding split_paired_all split_conv o_def
  10.178 -        proof goals
  10.179 +        proof goal_cases
  10.180            fix x k
  10.181            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}"
  10.182            then have xk: "(x, k) \<in> p" "content k = 0"
  10.183 @@ -7450,7 +7450,7 @@
  10.184                apply rule
  10.185                unfolding mem_Collect_eq
  10.186                unfolding split_paired_all fst_conv snd_conv
  10.187 -            proof (safe, goals)
  10.188 +            proof (safe, goal_cases)
  10.189                case 1
  10.190                guess v using pa[OF 1(1)] .. note v = conjunctD2[OF this]
  10.191                have "?a \<in> {?a..v}"
  10.192 @@ -7482,7 +7482,7 @@
  10.193                apply rule
  10.194                unfolding mem_Collect_eq
  10.195                unfolding split_paired_all fst_conv snd_conv
  10.196 -            proof (safe, goals)
  10.197 +            proof (safe, goal_cases)
  10.198                case 1
  10.199                guess v using pb[OF 1(1)] .. note v = conjunctD2[OF this]
  10.200                have "?b \<in> {v.. ?b}"
  10.201 @@ -7698,7 +7698,7 @@
  10.202      from fine_division_exists_real[OF this, of a t] guess p . note p=this
  10.203      note p'=tagged_division_ofD[OF this(1)]
  10.204      have pt: "\<forall>(x,k)\<in>p. x \<le> t"
  10.205 -    proof (safe, goals)
  10.206 +    proof (safe, goal_cases)
  10.207        case 1
  10.208        from p'(2,3)[OF this] show ?case
  10.209          by auto
  10.210 @@ -7753,7 +7753,7 @@
  10.211        have **: "\<And>x F. F \<union> {x} = insert x F"
  10.212          by auto
  10.213        have "(c, cbox t c) \<notin> p"
  10.214 -      proof (safe, goals)
  10.215 +      proof (safe, goal_cases)
  10.216          case 1
  10.217          from p'(2-3)[OF this] have "c \<in> cbox a t"
  10.218            by auto
  10.219 @@ -7855,7 +7855,7 @@
  10.220        apply cases
  10.221        apply (rule *)
  10.222        apply assumption
  10.223 -    proof goals
  10.224 +    proof goal_cases
  10.225        case 1
  10.226        then have "cbox a b = {x}"
  10.227          using as(1)
  10.228 @@ -8143,7 +8143,7 @@
  10.229        apply cases
  10.230        apply (rule *)
  10.231        apply assumption
  10.232 -    proof goals
  10.233 +    proof goal_cases
  10.234        case 1
  10.235        then have *: "box c d = {}"
  10.236          by (metis bot.extremum_uniqueI box_subset_cbox)
  10.237 @@ -8347,7 +8347,7 @@
  10.238      have "ball 0 C \<subseteq> cbox c d"
  10.239        apply (rule subsetI)
  10.240        unfolding mem_box mem_ball dist_norm
  10.241 -    proof (rule, goals)
  10.242 +    proof (rule, goal_cases)
  10.243        fix x i :: 'n
  10.244        assume x: "norm (0 - x) < C" and i: "i \<in> Basis"
  10.245        show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
  10.246 @@ -8658,7 +8658,7 @@
  10.247    show ?l
  10.248      apply (subst has_integral')
  10.249      apply safe
  10.250 -  proof goals
  10.251 +  proof goal_cases
  10.252      case (1 e)
  10.253      from \<open>?r\<close>[THEN conjunct2,rule_format,OF this] guess B .. note B=conjunctD2[OF this]
  10.254      show ?case
  10.255 @@ -8686,7 +8686,7 @@
  10.256        have "ball 0 B \<subseteq> cbox ?a ?b"
  10.257          apply (rule subsetI)
  10.258          unfolding mem_ball mem_box dist_norm
  10.259 -      proof (rule, goals)
  10.260 +      proof (rule, goal_cases)
  10.261          case (1 x i)
  10.262          then show ?case using Basis_le_norm[of i x]
  10.263            by (auto simp add:field_simps)
  10.264 @@ -8712,7 +8712,7 @@
  10.265        apply rule
  10.266        apply (rule B)
  10.267        apply safe
  10.268 -    proof goals
  10.269 +    proof goal_cases
  10.270        case 1
  10.271        from B(2)[OF this] guess z .. note z=conjunctD2[OF this]
  10.272        from integral_unique[OF this(1)] show ?case
  10.273 @@ -8739,7 +8739,7 @@
  10.274    show ?r
  10.275      apply safe
  10.276      apply (rule y)
  10.277 -  proof goals
  10.278 +  proof goal_cases
  10.279      case (1 e)
  10.280      then have "e/2 > 0"
  10.281        by auto
  10.282 @@ -8749,7 +8749,7 @@
  10.283        apply rule
  10.284        apply (rule B)
  10.285        apply safe
  10.286 -    proof goals
  10.287 +    proof goal_cases
  10.288        case (1 a b c d)
  10.289        show ?case
  10.290          apply (rule norm_triangle_half_l)
  10.291 @@ -8763,7 +8763,7 @@
  10.292    note as = conjunctD2[OF this,rule_format]
  10.293    let ?cube = "\<lambda>n. cbox (\<Sum>i\<in>Basis. - real n *\<^sub>R i::'n) (\<Sum>i\<in>Basis. real n *\<^sub>R i)"
  10.294    have "Cauchy (\<lambda>n. integral (?cube n) (\<lambda>x. if x \<in> s then f x else 0))"
  10.295 -  proof (unfold Cauchy_def, safe, goals)
  10.296 +  proof (unfold Cauchy_def, safe, goal_cases)
  10.297      case (1 e)
  10.298      from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format]
  10.299      from real_arch_simple[of B] guess N .. note N = this
  10.300 @@ -8773,7 +8773,7 @@
  10.301        have "ball 0 B \<subseteq> ?cube n"
  10.302          apply (rule subsetI)
  10.303          unfolding mem_ball mem_box dist_norm
  10.304 -      proof (rule, goals)
  10.305 +      proof (rule, goal_cases)
  10.306          case (1 x i)
  10.307          then show ?case
  10.308            using Basis_le_norm[of i x] \<open>i\<in>Basis\<close>
  10.309 @@ -8797,7 +8797,7 @@
  10.310      apply (rule_tac x=i in exI)
  10.311      apply safe
  10.312      apply (rule as(1)[unfolded integrable_on_def])
  10.313 -  proof goals
  10.314 +  proof goal_cases
  10.315      case (1 e)
  10.316      then have *: "e/2 > 0" by auto
  10.317      from i[OF this] guess N .. note N =this[rule_format]
  10.318 @@ -8830,7 +8830,7 @@
  10.319            using x
  10.320            unfolding mem_box mem_ball dist_norm
  10.321            apply -
  10.322 -        proof (rule, goals)
  10.323 +        proof (rule, goal_cases)
  10.324            case (1 i)
  10.325            then show ?case
  10.326              using Basis_le_norm[of i x] \<open>i \<in> Basis\<close>
  10.327 @@ -8870,7 +8870,7 @@
  10.328    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>
  10.329      norm (i - j) < e \<and> (\<forall>x\<in>cbox a b. (g x) \<le> f x \<and> f x \<le> h x)"
  10.330    shows "f integrable_on cbox a b"
  10.331 -proof (subst integrable_cauchy, safe, goals)
  10.332 +proof (subst integrable_cauchy, safe, goal_cases)
  10.333    case (1 e)
  10.334    then have e: "e/3 > 0"
  10.335      by auto
  10.336 @@ -8882,7 +8882,7 @@
  10.337      apply (rule_tac x="\<lambda>x. d1 x \<inter> d2 x" in exI)
  10.338      apply (rule conjI gauge_inter d1 d2)+
  10.339      unfolding fine_inter
  10.340 -  proof (safe, goals)
  10.341 +  proof (safe, goal_cases)
  10.342      have **: "\<And>i j g1 g2 h1 h2 f1 f2. g1 - h2 \<le> f1 - f2 \<Longrightarrow> f1 - f2 \<le> h1 - g2 \<Longrightarrow>
  10.343        abs (i - j) < e / 3 \<Longrightarrow> abs (g2 - i) < e / 3 \<Longrightarrow>  abs (g1 - i) < e / 3 \<Longrightarrow>
  10.344        abs (h2 - j) < e / 3 \<Longrightarrow> abs (h1 - j) < e / 3 \<Longrightarrow> abs (f1 - f2) < e"
  10.345 @@ -8949,7 +8949,7 @@
  10.346    shows "f integrable_on s"
  10.347  proof -
  10.348    have "\<And>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on cbox a b"
  10.349 -  proof (rule integrable_straddle_interval, safe, goals)
  10.350 +  proof (rule integrable_straddle_interval, safe, goal_cases)
  10.351      case (1 a b e)
  10.352      then have *: "e/4 > 0"
  10.353        by auto
  10.354 @@ -8968,7 +8968,7 @@
  10.355        apply safe
  10.356        unfolding mem_ball mem_box dist_norm
  10.357        apply (rule_tac[!] ballI)
  10.358 -    proof goals
  10.359 +    proof goal_cases
  10.360        case (1 x i)
  10.361        then show ?case using Basis_le_norm[of i x]
  10.362          unfolding c_def d_def by auto
  10.363 @@ -9027,7 +9027,7 @@
  10.364      unfolding integrable_alt[of f]
  10.365      apply safe
  10.366      apply (rule interv)
  10.367 -  proof goals
  10.368 +  proof goal_cases
  10.369      case (1 e)
  10.370      then have *: "e/3 > 0"
  10.371        by auto
  10.372 @@ -9132,7 +9132,7 @@
  10.373      defer
  10.374      apply assumption
  10.375      apply safe
  10.376 -  proof goals
  10.377 +  proof goal_cases
  10.378      case (1 x)
  10.379      then show ?case
  10.380      proof (cases "x \<in> \<Union>t")
  10.381 @@ -9174,7 +9174,7 @@
  10.382      apply rule
  10.383      apply rule
  10.384      apply rule
  10.385 -  proof goals
  10.386 +  proof goal_cases
  10.387      case (1 s s')
  10.388      from d(4)[OF this(1)] d(4)[OF this(2)] guess a c b d by (elim exE) note obt=this
  10.389      from d(5)[OF 1] show ?case
  10.390 @@ -9208,7 +9208,7 @@
  10.391    apply (rule has_integral_combine_division[OF assms(2)])
  10.392    apply safe
  10.393    unfolding has_integral_integral[symmetric]
  10.394 -proof goals
  10.395 +proof goal_cases
  10.396    case (1 k)
  10.397    from division_ofD(2,4)[OF assms(2) this]
  10.398    show ?case
  10.399 @@ -9248,7 +9248,7 @@
  10.400    shows "f integrable_on i"
  10.401    apply (rule integrable_combine_division assms)+
  10.402    apply safe
  10.403 -proof goals
  10.404 +proof goal_cases
  10.405    case 1
  10.406    note division_ofD(2,4)[OF assms(1) this]
  10.407    then show ?case
  10.408 @@ -9310,7 +9310,7 @@
  10.409    shows "(f has_integral (setsum (\<lambda>(x,k). integral k f) p)) (cbox a b)"
  10.410    apply (rule has_integral_combine_tagged_division[OF assms(2)])
  10.411    apply safe
  10.412 -proof goals
  10.413 +proof goal_cases
  10.414    case 1
  10.415    note tagged_division_ofD(3-4)[OF assms(2) this]
  10.416    then show ?case
  10.417 @@ -9359,7 +9359,7 @@
  10.418    have "\<forall>i\<in>r. \<exists>p. p tagged_division_of i \<and> d fine p \<and>
  10.419      norm (setsum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
  10.420      apply safe
  10.421 -  proof goals
  10.422 +  proof goal_cases
  10.423      case (1 i)
  10.424      then have i: "i \<in> q"
  10.425        unfolding r_def by auto
  10.426 @@ -9398,7 +9398,7 @@
  10.427      note * = tagged_partial_division_of_union_self[OF p(1)]
  10.428      have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r"
  10.429        using r
  10.430 -    proof (rule tagged_division_union[OF * tagged_division_unions], goals)
  10.431 +    proof (rule tagged_division_union[OF * tagged_division_unions], goal_cases)
  10.432        case 1
  10.433        then show ?case
  10.434          using qq by auto
  10.435 @@ -9534,7 +9534,7 @@
  10.436      unfolding split_def setsum_subtractf ..
  10.437    also have "\<dots> \<le> e + k"
  10.438      apply (rule *[OF **, where ir2="setsum (\<lambda>k. integral k f) r"])
  10.439 -  proof goals
  10.440 +  proof goal_cases
  10.441      case 2
  10.442      have *: "(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)"
  10.443        apply (subst setsum.reindex_nontrivial)
  10.444 @@ -9620,7 +9620,7 @@
  10.445    show thesis
  10.446      apply (rule that)
  10.447      apply (rule d)
  10.448 -  proof (safe, goals)
  10.449 +  proof (safe, goal_cases)
  10.450      case (1 p)
  10.451      note * = henstock_lemma_part2[OF assms(1) * d this]
  10.452      show ?case
  10.453 @@ -9776,7 +9776,7 @@
  10.454  
  10.455    have "(g has_integral i) (cbox a b)"
  10.456      unfolding has_integral
  10.457 -  proof (safe, goals)
  10.458 +  proof (safe, goal_cases)
  10.459      case e: (1 e)
  10.460      then have "\<forall>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
  10.461        norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral (cbox a b) (f k)) < e / 2 ^ (k + 2)))"
  10.462 @@ -9803,7 +9803,7 @@
  10.463  
  10.464      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>
  10.465        (g x)\<bullet>1 - (f k x)\<bullet>1 < e / (4 * content(cbox a b))"
  10.466 -    proof (rule, goals)
  10.467 +    proof (rule, goal_cases)
  10.468        case (1 x)
  10.469        have "e / (4 * content (cbox a b)) > 0"
  10.470          using \<open>e>0\<close> False content_pos_le[of a b] by auto
  10.471 @@ -9835,7 +9835,7 @@
  10.472        then guess s .. note s=this
  10.473        have *: "\<forall>a b c d. norm(a - b) \<le> e / 4 \<and> norm(b - c) < e / 2 \<and>
  10.474          norm (c - d) < e / 4 \<longrightarrow> norm (a - d) < e"
  10.475 -      proof (safe, goals)
  10.476 +      proof (safe, goal_cases)
  10.477          case (1 a b c d)
  10.478          then show ?case
  10.479            using norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
  10.480 @@ -9846,7 +9846,7 @@
  10.481        show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e"
  10.482          apply (rule *[rule_format,where
  10.483            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))"])
  10.484 -      proof (safe, goals)
  10.485 +      proof (safe, goal_cases)
  10.486          case 1
  10.487          show ?case
  10.488            apply (rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content (cbox a b)))"])
  10.489 @@ -10062,7 +10062,7 @@
  10.490      have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on cbox a b \<and>
  10.491        ((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> s then f k x else 0)) --->
  10.492        integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0)) sequentially"
  10.493 -    proof (rule monotone_convergence_interval, safe, goals)
  10.494 +    proof (rule monotone_convergence_interval, safe, goal_cases)
  10.495        case 1
  10.496        show ?case by (rule int)
  10.497      next
  10.498 @@ -10117,7 +10117,7 @@
  10.499        unfolding has_integral_alt'
  10.500        apply safe
  10.501        apply (rule g(1))
  10.502 -    proof goals
  10.503 +    proof goal_cases
  10.504        case (1 e)
  10.505        then have "e/4>0"
  10.506          by auto
  10.507 @@ -10155,7 +10155,7 @@
  10.508            apply (rule integral_le[OF int int])
  10.509            defer
  10.510            apply (rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]])
  10.511 -        proof (safe, goals)
  10.512 +        proof (safe, goal_cases)
  10.513            case (2 x)
  10.514            have "\<And>m. x \<in> s \<Longrightarrow> \<forall>n\<ge>m. (f m x)\<bullet>1 \<le> (f n x)\<bullet>1"
  10.515              apply (rule transitive_stepwise_le)
  10.516 @@ -10200,7 +10200,7 @@
  10.517      integral s (\<lambda>x. g x - f 0 x)) sequentially"
  10.518      apply (rule lem)
  10.519      apply safe
  10.520 -  proof goals
  10.521 +  proof goal_cases
  10.522      case (1 k x)
  10.523      then show ?case
  10.524        using *[of x 0 "Suc k"] by auto
  10.525 @@ -10538,7 +10538,7 @@
  10.526    obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
  10.527    apply (rule that[of "integral UNIV (\<lambda>x. norm (f x))"])
  10.528    apply safe
  10.529 -proof goals
  10.530 +proof goal_cases
  10.531    case (1 d)
  10.532    note d = division_ofD[OF 1(2)]
  10.533    have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. integral i (\<lambda>x. norm (f x)))"
  10.534 @@ -10591,7 +10591,7 @@
  10.535      apply (rule absolutely_integrable_onI [OF f has_integral_integrable])
  10.536      apply (subst has_integral[of _ ?S])
  10.537      apply safe
  10.538 -  proof goals
  10.539 +  proof goal_cases
  10.540      case (1 e)
  10.541      then have "?S - e / 2 < ?S" by simp
  10.542      then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
  10.543 @@ -10725,7 +10725,7 @@
  10.544          by (force intro!: helplemma)
  10.545  
  10.546        have p'alt: "p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}}"
  10.547 -      proof (safe, goals)
  10.548 +      proof (safe, goal_cases)
  10.549          case (2 _ _ x i l)
  10.550          have "x \<in> i"
  10.551            using fineD[OF p(3) 2(1)] k(2)[OF 2(2), of x] 2(4-)
  10.552 @@ -10773,7 +10773,7 @@
  10.553          apply (rule *[rule_format,OF **])
  10.554          apply safe
  10.555          apply(rule d(2))
  10.556 -      proof goals
  10.557 +      proof goal_cases
  10.558          case 1
  10.559          show ?case
  10.560            by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
  10.561 @@ -10783,7 +10783,7 @@
  10.562            (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}"
  10.563            by auto
  10.564          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))"
  10.565 -        proof (rule setsum_mono, goals)
  10.566 +        proof (rule setsum_mono, goal_cases)
  10.567            case k: (1 k)
  10.568            from d'(4)[OF this] guess u v by (elim exE) note uv=this
  10.569            def d' \<equiv> "{cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
  10.570 @@ -10809,7 +10809,7 @@
  10.571              apply fact
  10.572              unfolding d'_def uv
  10.573              apply blast
  10.574 -          proof (rule, goals)
  10.575 +          proof (rule, goal_cases)
  10.576              case (1 i)
  10.577              then have "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
  10.578                by auto
  10.579 @@ -10824,7 +10824,7 @@
  10.580              apply (rule setsum.reindex_nontrivial [unfolded o_def])
  10.581              apply (rule finite_imageI)
  10.582              apply (rule p')
  10.583 -          proof goals
  10.584 +          proof goal_cases
  10.585              case (1 l y)
  10.586              have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
  10.587                apply (subst(2) interior_inter)
  10.588 @@ -10900,7 +10900,7 @@
  10.589            apply fact
  10.590            apply (rule finite_imageI[OF p'(1)])
  10.591            apply safe
  10.592 -        proof goals
  10.593 +        proof goal_cases
  10.594            case (2 i ia l a b)
  10.595            then have "ia \<inter> b = {}"
  10.596              unfolding p'alt image_iff Bex_def not_ex
  10.597 @@ -11011,7 +11011,7 @@
  10.598              unfolding simple_image
  10.599              apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
  10.600              apply (rule d')
  10.601 -          proof goals
  10.602 +          proof goal_cases
  10.603              case (1 k y)
  10.604              from d'(4)[OF this(1)] d'(4)[OF this(2)]
  10.605              guess u1 v1 u2 v2 by (elim exE) note uv=this
  10.606 @@ -11035,7 +11035,7 @@
  10.607              apply blast
  10.608              apply safe
  10.609              apply (rule_tac x=k in exI)
  10.610 -          proof goals
  10.611 +          proof goal_cases
  10.612              case (1 i k)
  10.613              from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
  10.614              have "interior (k \<inter> cbox u v) \<noteq> {}"
  10.615 @@ -11085,7 +11085,7 @@
  10.616    show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
  10.617      apply (subst has_integral_alt')
  10.618      apply safe
  10.619 -  proof goals
  10.620 +  proof goal_cases
  10.621      case (1 a b)
  10.622      show ?case
  10.623        using f_int[of a b] by auto
  10.624 @@ -11124,7 +11124,7 @@
  10.625          apply (rule *[rule_format])
  10.626          apply safe
  10.627          apply (rule d(2))
  10.628 -      proof goals
  10.629 +      proof goal_cases
  10.630          case 1
  10.631          have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
  10.632            apply (rule setsum_mono)
  10.633 @@ -11251,7 +11251,7 @@
  10.634      apply (rule integrable_add)
  10.635      prefer 3
  10.636      apply safe
  10.637 -  proof goals
  10.638 +  proof goal_cases
  10.639      case (1 d)
  10.640      have "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k \<and> g integrable_on k"
  10.641        apply (drule division_ofD(4)[OF 1])
  10.642 @@ -11310,12 +11310,12 @@
  10.643      apply (rule bounded_variation_absolutely_integrable[of _ "B * b"])
  10.644      apply (rule integrable_linear[OF _ assms(2)])
  10.645      apply safe
  10.646 -  proof goals
  10.647 +  proof goal_cases
  10.648      case (2 d)
  10.649      have "(\<Sum>k\<in>d. norm (integral k (h \<circ> f))) \<le> setsum (\<lambda>k. norm(integral k f)) d * b"
  10.650        unfolding setsum_left_distrib
  10.651        apply (rule setsum_mono)
  10.652 -    proof goals
  10.653 +    proof goal_cases
  10.654        case (1 k)
  10.655        from division_ofD(4)[OF 2 this]
  10.656        guess u v by (elim exE) note uv=this
  10.657 @@ -11455,7 +11455,7 @@
  10.658    show "f absolutely_integrable_on UNIV"
  10.659      apply (rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"])
  10.660      apply safe
  10.661 -  proof goals
  10.662 +  proof goal_cases
  10.663      case (1 d)
  10.664      note d=this and d'=division_ofD[OF this]
  10.665      have "(\<Sum>k\<in>d. norm (integral k f)) \<le>
  10.666 @@ -11486,7 +11486,7 @@
  10.667      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"
  10.668        apply (subst setsum.commute)
  10.669        apply (rule setsum_mono)
  10.670 -    proof goals
  10.671 +    proof goal_cases
  10.672        case (1 j)
  10.673        have *: "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) integrable_on \<Union>d"
  10.674          using integrable_on_subdivision[OF d assms(2)] by auto
  10.675 @@ -11541,7 +11541,7 @@
  10.676    show "f absolutely_integrable_on UNIV"
  10.677      apply (rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"])
  10.678      apply safe
  10.679 -  proof goals
  10.680 +  proof goal_cases
  10.681      case d: (1 d)
  10.682      note d'=division_ofD[OF d]
  10.683      have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>k\<in>d. integral k g)"
  10.684 @@ -11731,7 +11731,7 @@
  10.685        by (rule cInf_superset_mono) auto
  10.686      let ?S = "{f j x| j. m \<le> j}"
  10.687      show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> Inf ?S) sequentially"
  10.688 -    proof (rule LIMSEQ_I, goals)
  10.689 +    proof (rule LIMSEQ_I, goal_cases)
  10.690        case r: (1 r)
  10.691  
  10.692        have "\<exists>y\<in>?S. y < Inf ?S + r"
  10.693 @@ -11742,7 +11742,7 @@
  10.694        show ?case
  10.695          apply (rule_tac x=N in exI)
  10.696          apply safe
  10.697 -      proof goals
  10.698 +      proof goal_cases
  10.699          case (1 n)
  10.700          have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - Inf ?S) < r"
  10.701            by arith
  10.702 @@ -11802,7 +11802,7 @@
  10.703        by (rule cSup_subset_mono) auto
  10.704      let ?S = "{f j x| j. m \<le> j}"
  10.705      show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> Sup ?S) sequentially"
  10.706 -    proof (rule LIMSEQ_I, goals)
  10.707 +    proof (rule LIMSEQ_I, goal_cases)
  10.708        case r: (1 r)
  10.709        have "\<exists>y\<in>?S. Sup ?S - r < y"
  10.710          by (subst less_cSup_iff[symmetric]) (auto simp: r \<open>x\<in>s\<close>)
  10.711 @@ -11812,7 +11812,7 @@
  10.712        show ?case
  10.713          apply (rule_tac x=N in exI)
  10.714          apply safe
  10.715 -      proof goals
  10.716 +      proof goal_cases
  10.717          case (1 n)
  10.718          have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - Sup ?S) < r"
  10.719            by arith
  10.720 @@ -11856,7 +11856,7 @@
  10.721        by (intro cInf_superset_mono) (auto simp: \<open>x\<in>s\<close>)
  10.722  
  10.723      show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
  10.724 -    proof (rule LIMSEQ_I, goals)
  10.725 +    proof (rule LIMSEQ_I, goal_cases)
  10.726        case r: (1 r)
  10.727        then have "0<r/2"
  10.728          by auto
  10.729 @@ -11904,7 +11904,7 @@
  10.730      show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
  10.731        by (rule cSup_subset_mono) (auto simp: \<open>x\<in>s\<close>)
  10.732      show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
  10.733 -    proof (rule LIMSEQ_I, goals)
  10.734 +    proof (rule LIMSEQ_I, goal_cases)
  10.735        case r: (1 r)
  10.736        then have "0<r/2"
  10.737          by auto
  10.738 @@ -11926,7 +11926,7 @@
  10.739  
  10.740    show "g integrable_on s" by fact
  10.741    show "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
  10.742 -  proof (rule LIMSEQ_I, goals)
  10.743 +  proof (rule LIMSEQ_I, goal_cases)
  10.744      case r: (1 r)
  10.745      from LIMSEQ_D [OF inc2(2) r] guess N1 .. note N1=this[unfolded real_norm_def]
  10.746      from LIMSEQ_D [OF dec2(2) r] guess N2 .. note N2=this[unfolded real_norm_def]
    11.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Sun Sep 13 16:50:12 2015 +0200
    11.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Sun Sep 13 20:20:16 2015 +0200
    11.3 @@ -62,7 +62,7 @@
    11.4    by (simp add: supp_def Collect_disj_eq del: disj_not1)
    11.5  
    11.6  instance pat :: pt_name
    11.7 -proof (default, goals)
    11.8 +proof (default, goal_cases)
    11.9    case (1 x)
   11.10    show ?case by (induct x) simp_all
   11.11  next
   11.12 @@ -74,7 +74,7 @@
   11.13  qed
   11.14  
   11.15  instance pat :: fs_name
   11.16 -proof (default, goals)
   11.17 +proof (default, goal_cases)
   11.18    case (1 x)
   11.19    show ?case by (induct x) (simp_all add: fin_supp)
   11.20  qed
    12.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Sun Sep 13 16:50:12 2015 +0200
    12.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Sun Sep 13 20:20:16 2015 +0200
    12.3 @@ -122,7 +122,7 @@
    12.4    "mark_out_aux n m [] = []"
    12.5    "mark_out_aux n 0 (b # bs) = False # mark_out_aux n n bs"
    12.6    "mark_out_aux n (Suc m) (b # bs) = b # mark_out_aux n m bs"
    12.7 -proof goals
    12.8 +proof goal_cases
    12.9    case 1
   12.10    show ?case
   12.11      by (simp add: mark_out_aux_def)
    13.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Sun Sep 13 16:50:12 2015 +0200
    13.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Sun Sep 13 20:20:16 2015 +0200
    13.3 @@ -193,7 +193,7 @@
    13.4    assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
    13.5    shows "PiM I M = PiM J N"
    13.6    unfolding PiM_def
    13.7 -proof (rule extend_measure_cong, goals)
    13.8 +proof (rule extend_measure_cong, goal_cases)
    13.9    case 1
   13.10    show ?case using assms
   13.11      by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
    14.1 --- a/src/HOL/Probability/Measure_Space.thy	Sun Sep 13 16:50:12 2015 +0200
    14.2 +++ b/src/HOL/Probability/Measure_Space.thy	Sun Sep 13 20:20:16 2015 +0200
    14.3 @@ -2078,7 +2078,7 @@
    14.4    "less_measure M N \<longleftrightarrow> (M \<le> N \<and> \<not> N \<le> M)"
    14.5  
    14.6  instance
    14.7 -proof (standard, goals)
    14.8 +proof (standard, goal_cases)
    14.9    case 1 then show ?case
   14.10      unfolding less_measure_def ..
   14.11  next
    15.1 --- a/src/HOL/ZF/Games.thy	Sun Sep 13 16:50:12 2015 +0200
    15.2 +++ b/src/HOL/ZF/Games.thy	Sun Sep 13 20:20:16 2015 +0200
    15.3 @@ -418,7 +418,7 @@
    15.4  proof (induct x rule: wf_induct[OF wf_option_of]) 
    15.5    case (1 "g")  
    15.6    show ?case
    15.7 -  proof (auto, goals)
    15.8 +  proof (auto, goal_cases)
    15.9      {case prems: (1 y) 
   15.10        from prems have "(y, g) \<in> option_of" by (auto)
   15.11        with 1 have "ge_game (y, y)" by auto
   15.12 @@ -462,7 +462,7 @@
   15.13      proof (induct a rule: induct_game)
   15.14        case (1 a)
   15.15        show ?case
   15.16 -      proof ((rule allI | rule impI)+, goals)
   15.17 +      proof ((rule allI | rule impI)+, goal_cases)
   15.18          case prems: (1 x y z)
   15.19          show ?case
   15.20          proof -
   15.21 @@ -543,7 +543,7 @@
   15.22  lemma plus_game_zero_right[simp]: "plus_game G zero_game = G"
   15.23  proof -
   15.24    have "H = zero_game \<longrightarrow> plus_game G H = G " for G H
   15.25 -  proof (induct G H rule: plus_game.induct, rule impI, goals)
   15.26 +  proof (induct G H rule: plus_game.induct, rule impI, goal_cases)
   15.27      case prems: (1 G H)
   15.28      note induct_hyp = this[simplified prems, simplified] and this
   15.29      show ?case
   15.30 @@ -583,7 +583,7 @@
   15.31  lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)"
   15.32  proof -
   15.33    have "\<forall>F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game F G) H = plus_game F (plus_game G H)" for a
   15.34 -  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
   15.35 +  proof (induct a rule: induct_game, (rule impI | rule allI)+, goal_cases)
   15.36      case prems: (1 x F G H)
   15.37      let ?L = "plus_game (plus_game F G) H"
   15.38      let ?R = "plus_game F (plus_game G H)"
   15.39 @@ -626,7 +626,7 @@
   15.40  qed
   15.41  
   15.42  lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
   15.43 -proof (induct x rule: wf_induct[OF wf_option_of], goals)
   15.44 +proof (induct x rule: wf_induct[OF wf_option_of], goal_cases)
   15.45    case prems: (1 x)
   15.46    then have ihyp: "eq_game (plus_game y (neg_game y)) zero_game" if "zin y (options x)" for y
   15.47      using that by (auto simp add: prems)
   15.48 @@ -670,7 +670,7 @@
   15.49  lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
   15.50  proof -
   15.51    have "\<forall>x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game (plus_game x y, plus_game x z)" for a
   15.52 -  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
   15.53 +  proof (induct a rule: induct_game, (rule impI | rule allI)+, goal_cases)
   15.54      case prems: (1 a x y z)
   15.55      note induct_hyp = prems(1)[rule_format, simplified prems(2)]
   15.56      { 
   15.57 @@ -780,7 +780,7 @@
   15.58  lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
   15.59  proof -
   15.60    have "\<forall>x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)" for a
   15.61 -  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
   15.62 +  proof (induct a rule: induct_game, (rule impI | rule allI)+, goal_cases)
   15.63      case prems: (1 a x y)
   15.64      note ihyp = prems(1)[rule_format, simplified prems(2)]
   15.65      { fix xl
    16.1 --- a/src/HOL/ex/Tree23.thy	Sun Sep 13 16:50:12 2015 +0200
    16.2 +++ b/src/HOL/ex/Tree23.thy	Sun Sep 13 20:20:16 2015 +0200
    16.3 @@ -377,7 +377,7 @@
    16.4       done
    16.5    } note B = this
    16.6    show "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
    16.7 -  proof (induct k t arbitrary: n rule: del.induct, goals)
    16.8 +  proof (induct k t arbitrary: n rule: del.induct, goal_cases)
    16.9      case (1 k n)
   16.10      thus "dfull n (del (Some k) Empty)" by simp
   16.11    next
    17.1 --- a/src/Pure/Isar/method.ML	Sun Sep 13 16:50:12 2015 +0200
    17.2 +++ b/src/Pure/Isar/method.ML	Sun Sep 13 20:20:16 2015 +0200
    17.3 @@ -17,7 +17,7 @@
    17.4    val SIMPLE_METHOD: tactic -> method
    17.5    val SIMPLE_METHOD': (int -> tactic) -> method
    17.6    val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
    17.7 -  val goals_tac: Proof.context -> string list -> cases_tactic
    17.8 +  val goal_cases_tac: Proof.context -> string list -> cases_tactic
    17.9    val cheating: Proof.context -> bool -> method
   17.10    val intro: Proof.context -> thm list -> method
   17.11    val elim: Proof.context -> thm list -> method
   17.12 @@ -130,7 +130,7 @@
   17.13  
   17.14  (* goals as cases *)
   17.15  
   17.16 -fun goals_tac ctxt case_names st =
   17.17 +fun goal_cases_tac ctxt case_names st =
   17.18    let
   17.19      val cases =
   17.20        (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names)
   17.21 @@ -693,7 +693,7 @@
   17.22      "succeed after delay (in seconds)" #>
   17.23    setup @{binding "-"} (Scan.succeed (K insert_facts))
   17.24      "insert current facts, nothing else" #>
   17.25 -  setup @{binding goals} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
   17.26 +  setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
   17.27      METHOD_CASES (fn facts => fn st =>
   17.28        let
   17.29          val _ =
   17.30 @@ -705,7 +705,7 @@
   17.31                  (* FIXME Seq.Error *)
   17.32                  error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
   17.33                    Position.here (Position.set_range (Token.range_of bad))));
   17.34 -      in goals_tac ctxt (map Token.content_of names) st end)))
   17.35 +      in goal_cases_tac ctxt (map Token.content_of names) st end)))
   17.36      "bind cases for goals" #>
   17.37    setup @{binding insert} (Attrib.thms >> (K o insert))
   17.38      "insert theorems, ignoring facts" #>