# HG changeset patch
# User wenzelm
# Date 1435268027 -7200
# Node ID 7e741e22d7fc54f94c12a912be51cecf8bbf4ba9
# Parent  915da29bf5d9beba80eb98609dd2cf49d14e5e3c
tuned proofs;

diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -908,13 +908,13 @@
 subsection \<open>Miscellaneous lemmas about indexes, decrementation, substitution  etc ...\<close>
 
 lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
-proof (induct p arbitrary: n rule: poly.induct, auto)
-  case (goal1 c n p n')
+proof (induct p arbitrary: n rule: poly.induct, auto, goals)
+  case prems: (1 c n p n')
   then have "n = Suc (n - 1)"
     by simp
   then have "isnpolyh p (Suc (n - 1))"
     using \<open>isnpolyh p n\<close> by simp
-  with goal1(2) show ?case
+  with prems(2) show ?case
     by simp
 qed
 
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/GCD.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -1451,17 +1451,19 @@
 
 subsection {* The complete divisibility lattice *}
 
-interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
-proof
-  case goal3 thus ?case by(metis gcd_unique_nat)
+interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
+proof (default, goals)
+  case 3
+  thus ?case by(metis gcd_unique_nat)
 qed auto
 
-interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
-proof
-  case goal3 thus ?case by(metis lcm_unique_nat)
+interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
+proof (default, goals)
+  case 3
+  thus ?case by(metis lcm_unique_nat)
 qed auto
 
-interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm ..
+interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
 
 text{* Lifting gcd and lcm to sets (Gcd/Lcm).
 Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
@@ -1522,23 +1524,28 @@
 
 interpretation gcd_lcm_complete_lattice_nat:
   complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
-where
-  "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
+where "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
   and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
 proof -
   show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
-  proof
-    case goal1 thus ?case by (simp add: Gcd_nat_def)
+  proof (default, goals)
+    case 1
+    thus ?case by (simp add: Gcd_nat_def)
   next
-    case goal2 thus ?case by (simp add: Gcd_nat_def)
+    case 2
+    thus ?case by (simp add: Gcd_nat_def)
   next
-    case goal5 show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
+    case 5
+    show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
   next
-    case goal6 show ?case by (simp add: Lcm_nat_empty)
+    case 6
+    show ?case by (simp add: Lcm_nat_empty)
   next
-    case goal3 thus ?case by simp
+    case 3
+    thus ?case by simp
   next
-    case goal4 thus ?case by simp
+    case 4
+    thus ?case by simp
   qed
   then interpret gcd_lcm_complete_lattice_nat:
     complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -333,11 +333,11 @@
 | "ereal r + -\<infinity> = - \<infinity>"
 | "-\<infinity> + ereal p = -(\<infinity>::ereal)"
 | "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
-proof -
-  case (goal1 P x)
+proof goals
+  case prems: (1 P x)
   then obtain a b where "x = (a, b)"
     by (cases x) auto
-  with goal1 show P
+  with prems show P
    by (cases rule: ereal2_cases[of a b]) auto
 qed auto
 termination by default (rule wf_empty)
@@ -437,10 +437,10 @@
 | "ereal x    < \<infinity>           \<longleftrightarrow> True"
 | "        -\<infinity> < ereal r     \<longleftrightarrow> True"
 | "        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
-proof -
-  case (goal1 P x)
+proof goals
+  case prems: (1 P x)
   then obtain a b where "x = (a,b)" by (cases x) auto
-  with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
+  with prems show P by (cases rule: ereal2_cases[of a b]) auto
 qed simp_all
 termination by (relation "{}") simp
 
@@ -860,11 +860,11 @@
 | "-(\<infinity>::ereal) * \<infinity> = -\<infinity>"
 | "(\<infinity>::ereal) * -\<infinity> = -\<infinity>"
 | "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
-proof -
-  case (goal1 P x)
+proof goals
+  case prems: (1 P x)
   then obtain a b where "x = (a, b)"
     by (cases x) auto
-  with goal1 show P
+  with prems show P
     by (cases rule: ereal2_cases[of a b]) auto
 qed simp_all
 termination by (relation "{}") simp
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Library/Product_Order.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -233,11 +233,13 @@
 
 instance prod ::
   (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
-proof
-  case goal1 thus ?case
+proof (default, goals)
+  case 1
+  then show ?case
     by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
 next
-  case goal2 thus ?case
+  case 2
+  then show ?case
     by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
 qed
 
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -294,27 +294,32 @@
 using assms 
 proof (induction t rule: rbt_min_opt_induct)
   case empty
-    then show ?case by simp
+  then show ?case by simp
 next
   case left_empty
-    then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
+  then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
 next
   case (left_non_empty c t1 k v t2 y)
-    then have "y = k \<or> y \<in> set (RBT_Impl.keys t1) \<or> y \<in> set (RBT_Impl.keys t2)" by auto
-    with left_non_empty show ?case 
-    proof(elim disjE)
-      case goal1 then show ?case 
-        by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
-    next
-      case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch)
-    next 
-      case goal3 show ?case
-      proof -
-        from goal3 have "rbt_min_opt t1 \<le> k" by (simp add: left_le_key rbt_min_opt_in_set)
-        moreover from goal3 have "k \<le> y" by (simp add: key_le_right)
-        ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch)
-      qed
-    qed
+  then consider "y = k" | "y \<in> set (RBT_Impl.keys t1)" | "y \<in> set (RBT_Impl.keys t2)"
+    by auto
+  then show ?case 
+  proof cases
+    case 1
+    with left_non_empty show ?thesis
+      by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
+  next
+    case 2
+    with left_non_empty show ?thesis
+      by (auto simp add: rbt_min_opt_Branch)
+  next 
+    case y: 3
+    have "rbt_min_opt t1 \<le> k"
+      using left_non_empty by (simp add: left_le_key rbt_min_opt_in_set)
+    moreover have "k \<le> y"
+      using left_non_empty y by (simp add: key_le_right)
+    ultimately show ?thesis
+      using left_non_empty y by (simp add: rbt_min_opt_Branch)
+  qed
 qed
 
 lemma rbt_min_eq_rbt_min_opt:
@@ -388,27 +393,32 @@
 using assms 
 proof (induction t rule: rbt_max_opt_induct)
   case empty
-    then show ?case by simp
+  then show ?case by simp
 next
   case right_empty
-    then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
+  then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
 next
   case (right_non_empty c t1 k v t2 y)
-    then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto
-    with right_non_empty show ?case 
-    proof(elim disjE)
-      case goal1 then show ?case 
-        by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
-    next
-      case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch)
-    next 
-      case goal3 show ?case
-      proof -
-        from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set)
-        moreover from goal3 have "y \<le> k" by (simp add: left_le_key)
-        ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch)
-      qed
-    qed
+  then consider "y = k" | "y \<in> set (RBT_Impl.keys t2)" | "y \<in> set (RBT_Impl.keys t1)"
+    by auto
+  then show ?case 
+  proof cases
+    case 1
+    with right_non_empty show ?thesis
+      by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
+  next
+    case 2
+    with right_non_empty show ?thesis
+      by (auto simp add: rbt_max_opt_Branch)
+  next 
+    case y: 3
+    have "rbt_max_opt t2 \<ge> k"
+      using right_non_empty by (simp add: key_le_right rbt_max_opt_in_set)
+    moreover have "y \<le> k"
+      using right_non_empty y by (simp add: left_le_key)
+    ultimately show ?thesis
+      using right_non_empty by (simp add: rbt_max_opt_Branch)
+  qed
 qed
 
 lemma rbt_max_eq_rbt_max_opt:
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -157,14 +157,15 @@
     note b = this(1) and body = this(2) and inv = this(3)
     hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
     ultimately show ?thesis unfolding Suc using b
-    proof (intro Least_equality[symmetric])
-      case goal1
+    proof (intro Least_equality[symmetric], goals)
+      case 1
       hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
         by (auto simp: BodyCommute inv b)
       have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b)
       with Test show ?case by (auto simp: TestCommute)
     next
-      case goal2 thus ?case by (metis not_less_eq_eq)
+      case 2
+      thus ?case by (metis not_less_eq_eq)
     qed
   qed
   have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/List.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -2308,19 +2308,29 @@
   "\<lbrakk> \<And> i. \<lbrakk> i < n ; i < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) ; n < length xs \<Longrightarrow> \<not> P (xs ! n) \<rbrakk> \<Longrightarrow>
   takeWhile P xs = take n xs"
 proof (induct xs arbitrary: n)
+  case Nil
+  thus ?case by simp
+next
   case (Cons x xs)
-  thus ?case
+  show ?case
   proof (cases n)
-    case (Suc n') note this[simp]
+    case 0
+    with Cons show ?thesis by simp
+  next
+    case [simp]: (Suc n')
     have "P x" using Cons.prems(1)[of 0] by simp
     moreover have "takeWhile P xs = take n' xs"
     proof (rule Cons.hyps)
-      case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
-    next case goal2 thus ?case using Cons by auto
+      fix i
+      assume "i < n'" "i < length xs"
+      thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
+    next
+      assume "n' < length xs"
+      thus "\<not> P (xs ! n')" using Cons by auto
     qed
     ultimately show ?thesis by simp
-   qed simp
-qed simp
+   qed
+qed
 
 lemma nth_length_takeWhile:
   "length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -1337,22 +1337,25 @@
   obtains q where "\<forall>i<n. q i < p"
     and "\<forall>i<n. \<exists>r s. (\<forall>j<n. q j \<le> r j \<and> r j \<le> q j + 1) \<and> (\<forall>j<n. q j \<le> s j \<and> s j \<le> q j + 1) \<and> label r i \<noteq> label s i"
 proof -
-  let ?rl = "reduced n\<circ>label"
+  let ?rl = "reduced n \<circ> label"
   let ?A = "{s. ksimplex p n s \<and> ?rl ` s = {..n}}"
   have "odd (card ?A)"
     using assms by (intro kuhn_combinatorial[of p n label]) auto
   then have "?A \<noteq> {}"
-    by (intro notI) simp
+    by fastforce
   then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}"
     by (auto elim: ksimplex.cases)
   interpret kuhn_simplex p n b u s by fact
 
   show ?thesis
   proof (intro that[of b] allI impI)
-    fix i assume "i < n" then show "b i < p"
+    fix i
+    assume "i < n"
+    then show "b i < p"
       using base by auto
   next
-    case goal2
+    fix i
+    assume "i < n"
     then have "i \<in> {.. n}" "Suc i \<in> {.. n}"
       by auto
     then obtain u v where u: "u \<in> s" "Suc i = ?rl u" and v: "v \<in> s" "i = ?rl v"
@@ -1363,10 +1366,11 @@
         u(2)[symmetric] v(2)[symmetric] \<open>i < n\<close>
       by auto
     moreover
-    { fix j assume "j < n"
-      then have "b j \<le> u j" "u j \<le> b j + 1" "b j \<le> v j" "v j \<le> b j + 1"
-        using base_le[OF \<open>u\<in>s\<close>] le_Suc_base[OF \<open>u\<in>s\<close>] base_le[OF \<open>v\<in>s\<close>] le_Suc_base[OF \<open>v\<in>s\<close>] by auto }
-    ultimately show ?case
+    have "b j \<le> u j" "u j \<le> b j + 1" "b j \<le> v j" "v j \<le> b j + 1" if "j < n" for j
+      using that base_le[OF \<open>u\<in>s\<close>] le_Suc_base[OF \<open>u\<in>s\<close>] base_le[OF \<open>v\<in>s\<close>] le_Suc_base[OF \<open>v\<in>s\<close>]
+      by auto
+    ultimately show "\<exists>r s. (\<forall>j<n. b j \<le> r j \<and> r j \<le> b j + 1) \<and>
+        (\<forall>j<n. b j \<le> s j \<and> s j \<le> b j + 1) \<and> label r i \<noteq> label s i"
       by blast
   qed
 qed
@@ -1392,23 +1396,20 @@
     apply rule
     apply rule
   proof -
-    case goal1
+    fix x x'
     let ?R = "\<lambda>y::nat.
-      (P x \<and> Q xa \<and> x xa = 0 \<longrightarrow> y = 0) \<and>
-      (P x \<and> Q xa \<and> x xa = 1 \<longrightarrow> y = 1) \<and>
-      (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x xa \<le> (f x) xa) \<and>
-      (P x \<and> Q xa \<and> y = 1 \<longrightarrow> (f x) xa \<le> x xa)"
-    {
-      assume "P x" and "Q xa"
-      then have "0 \<le> f x xa \<and> f x xa \<le> 1"
-        using assms(2)[rule_format,of "f x" xa]
-        apply (drule_tac assms(1)[rule_format])
-        apply auto
-        done
-    }
+      (P x \<and> Q x' \<and> x x' = 0 \<longrightarrow> y = 0) \<and>
+      (P x \<and> Q x' \<and> x x' = 1 \<longrightarrow> y = 1) \<and>
+      (P x \<and> Q x' \<and> y = 0 \<longrightarrow> x x' \<le> (f x) x') \<and>
+      (P x \<and> Q x' \<and> y = 1 \<longrightarrow> (f x) x' \<le> x x')"
+    have "0 \<le> f x x' \<and> f x x' \<le> 1" if "P x" "Q x'"
+      using assms(2)[rule_format,of "f x" x'] that
+      apply (drule_tac assms(1)[rule_format])
+      apply auto
+      done
     then have "?R 0 \<or> ?R 1"
       by auto
-    then show ?case
+    then show "\<exists>y\<le>1. ?R y"
       by auto
   qed
 qed
@@ -1988,17 +1989,17 @@
   assumes "e > 0"
   shows "\<not> (frontier (cball a e) retract_of (cball a e))"
 proof
-  case goal1
-  have *: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
+  assume *: "frontier (cball a e) retract_of (cball a e)"
+  have **: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
     using scaleR_left_distrib[of 1 1 a] by auto
   obtain x where x:
       "x \<in> {x. norm (a - x) = e}"
       "2 *\<^sub>R a - x = x"
-    apply (rule retract_fixpoint_property[OF goal1, of "\<lambda>x. scaleR 2 a - x"])
+    apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
     apply (blast intro: brouwer_ball[OF assms])
     apply (intro continuous_intros)
     unfolding frontier_cball subset_eq Ball_def image_iff dist_norm
-    apply (auto simp add: * norm_minus_commute)
+    apply (auto simp add: ** norm_minus_commute)
     done
   then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
     by (auto simp add: algebra_simps)
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -62,20 +62,20 @@
   by (simp add: supp_def Collect_disj_eq del: disj_not1)
 
 instance pat :: pt_name
-proof intro_classes
-  case goal1
+proof (default, goals)
+  case (1 x)
   show ?case by (induct x) simp_all
 next
-  case goal2
+  case (2 _ _ x)
   show ?case by (induct x) (simp_all add: pt_name2)
 next
-  case goal3
+  case (3 _ _ x)
   then show ?case by (induct x) (simp_all add: pt_name3)
 qed
 
 instance pat :: fs_name
-proof intro_classes
-  case goal1
+proof (default, goals)
+  case (1 x)
   show ?case by (induct x) (simp_all add: fin_supp)
 qed
 
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -2202,7 +2202,6 @@
   have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at)
   show ?thesis
   proof (rule equalityI)
-    case goal1
     show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
       apply(auto simp add: perm_set_def)
       apply(rule_tac x="pi\<bullet>xb" in exI)
@@ -2218,7 +2217,6 @@
       apply(rule pt_fun_app_eq[OF pt, OF at])
       done
   next
-    case goal2
     show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
       apply(auto simp add: perm_set_def)
       apply(rule_tac x="(rev pi)\<bullet>x" in exI)
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -1527,14 +1527,19 @@
 definition [simp]:
   "normalization_factor_int = (sgn :: int \<Rightarrow> int)"
 
-instance proof
-  case goal2 then show ?case by (auto simp add: abs_mult nat_mult_distrib)
+instance
+proof (default, goals)
+  case 2
+  then show ?case by (auto simp add: abs_mult nat_mult_distrib)
 next
-  case goal3 then show ?case by (simp add: zsgn_def)
+  case 3
+  then show ?case by (simp add: zsgn_def)
 next
-  case goal5 then show ?case by (auto simp: zsgn_def)
+  case 5
+  then show ?case by (auto simp: zsgn_def)
 next
-  case goal6 then show ?case by (auto split: abs_split simp: zsgn_def)
+  case 6
+  then show ?case by (auto split: abs_split simp: zsgn_def)
 qed (auto simp: sgn_times split: abs_split)
 
 end
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Probability/Embed_Measure.thy
--- a/src/HOL/Probability/Embed_Measure.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Probability/Embed_Measure.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -154,22 +154,22 @@
 lemma sigma_finite_embed_measure:
   assumes "sigma_finite_measure M" and inj: "inj f"
   shows "sigma_finite_measure (embed_measure M f)"
-proof
-  case goal1
+proof -
   from assms(1) interpret sigma_finite_measure M .
   from sigma_finite_countable obtain A where
       A_props: "countable A" "A \<subseteq> sets M" "\<Union>A = space M" "\<And>X. X\<in>A \<Longrightarrow> emeasure M X \<noteq> \<infinity>" by blast
-  show ?case
-  proof (intro exI[of _ "op ` f`A"] conjI allI)
-    from A_props show "countable (op ` f`A)" by auto
-    from inj and A_props show "op ` f`A \<subseteq> sets (embed_measure M f)" 
-      by (auto simp: sets_embed_measure)
-    from A_props and inj show "\<Union>(op ` f`A) = space (embed_measure M f)"
-      by (auto simp: space_embed_measure intro!: imageI)
-    from A_props and inj show "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
-      by (intro ballI, subst emeasure_embed_measure)
-         (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
-  qed
+  from A_props have "countable (op ` f`A)" by auto
+  moreover
+  from inj and A_props have "op ` f`A \<subseteq> sets (embed_measure M f)" 
+    by (auto simp: sets_embed_measure)
+  moreover
+  from A_props and inj have "\<Union>(op ` f`A) = space (embed_measure M f)"
+    by (auto simp: space_embed_measure intro!: imageI)
+  moreover
+  from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
+    by (intro ballI, subst emeasure_embed_measure)
+       (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
+  ultimately show ?thesis by - (default, blast)
 qed
 
 lemma embed_measure_count_space':
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -192,20 +192,22 @@
 lemma PiM_cong:
   assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
   shows "PiM I M = PiM J N"
-unfolding PiM_def
-proof (rule extend_measure_cong)
-  case goal1 show ?case using assms
+  unfolding PiM_def
+proof (rule extend_measure_cong, goals)
+  case 1
+  show ?case using assms
     by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
 next
-  case goal2
+  case 2
   have "\<And>K. K \<subseteq> J \<Longrightarrow> (\<Pi> j\<in>K. sets (M j)) = (\<Pi> j\<in>K. sets (N j))"
     using assms by (intro Pi_cong_sets) auto
   thus ?case by (auto simp: assms)
 next
-  case goal3 show ?case using assms 
+  case 3
+  show ?case using assms 
     by (intro ext) (auto simp: prod_emb_def dest: PiE_mem)
 next
-  case (goal4 x)
+  case (4 x)
   thus ?case using assms 
     by (auto intro!: setprod.cong split: split_if_asm)
 qed
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Probability/Information.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -1022,11 +1022,12 @@
     Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
     Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
   proof eventually_elim
-    case (goal1 x)
+    case (elim x)
     show ?case
     proof cases
       assume "Pxyz x \<noteq> 0"
-      with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
+      with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
+        "0 < Pyz (snd x)" "0 < Pxyz x"
         by auto
       then show ?thesis
         using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
@@ -1252,11 +1253,12 @@
     Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
     Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
   proof eventually_elim
-    case (goal1 x)
+    case (elim x)
     show ?case
     proof cases
       assume "Pxyz x \<noteq> 0"
-      with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
+      with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
+        "0 < Pyz (snd x)" "0 < Pxyz x"
         by auto
       then show ?thesis
         using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
@@ -1730,11 +1732,11 @@
     Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
     (is "AE x in _. ?f x = ?g x")
   proof eventually_elim
-    case (goal1 x)
+    case (elim x)
     show ?case
     proof cases
       assume "Pxy x \<noteq> 0"
-      with goal1 have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
+      with elim have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
         by auto
       then show ?thesis
         using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -1134,44 +1134,56 @@
 lemma (in sigma_finite_measure) sigma_finite_disjoint:
   obtains A :: "nat \<Rightarrow> 'a set"
   where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "disjoint_family A"
-proof atomize_elim
-  case goal1
+proof -
   obtain A :: "nat \<Rightarrow> 'a set" where
     range: "range A \<subseteq> sets M" and
     space: "(\<Union>i. A i) = space M" and
     measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
     using sigma_finite by auto
-  note range' = sets.range_disjointed_sets[OF range] range
-  { fix i
-    have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
-      using range' disjointed_subset[of A i] by (auto intro!: emeasure_mono)
-    then have "emeasure M (disjointed A i) \<noteq> \<infinity>"
-      using measure[of i] by auto }
-  with disjoint_family_disjointed UN_disjointed_eq[of A] space range'
-  show ?case by (auto intro!: exI[of _ "disjointed A"])
+  show thesis
+  proof (rule that[of "disjointed A"])
+    show "range (disjointed A) \<subseteq> sets M"
+      by (rule sets.range_disjointed_sets[OF range])
+    show "(\<Union>i. disjointed A i) = space M"
+      and "disjoint_family (disjointed A)"
+      using disjoint_family_disjointed UN_disjointed_eq[of A] space range
+      by auto
+    show "emeasure M (disjointed A i) \<noteq> \<infinity>" for i
+    proof -
+      have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
+        using range disjointed_subset[of A i] by (auto intro!: emeasure_mono)
+      then show ?thesis using measure[of i] by auto
+    qed
+  qed
 qed
 
 lemma (in sigma_finite_measure) sigma_finite_incseq:
   obtains A :: "nat \<Rightarrow> 'a set"
   where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "incseq A"
-proof atomize_elim
-  case goal1
+proof -
   obtain F :: "nat \<Rightarrow> 'a set" where
     F: "range F \<subseteq> sets M" "(\<Union>i. F i) = space M" "\<And>i. emeasure M (F i) \<noteq> \<infinity>"
     using sigma_finite by auto
-  then show ?case
-  proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI)
-    from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
-    then show "(\<Union>n. \<Union> i\<le>n. F i) = space M"
-      using F by fastforce
-  next
-    fix n
-    have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))" using F
-      by (auto intro!: emeasure_subadditive_finite)
-    also have "\<dots> < \<infinity>"
-      using F by (auto simp: setsum_Pinfty)
-    finally show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" by simp
-  qed (force simp: incseq_def)+
+  show thesis
+  proof (rule that[of "\<lambda>n. \<Union>i\<le>n. F i"])
+    show "range (\<lambda>n. \<Union>i\<le>n. F i) \<subseteq> sets M"
+      using F by (force simp: incseq_def)
+    show "(\<Union>n. \<Union>i\<le>n. F i) = space M"
+    proof -
+      from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
+      with F show ?thesis by fastforce
+    qed
+    show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" for n
+    proof -
+      have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))"
+        using F by (auto intro!: emeasure_subadditive_finite)
+      also have "\<dots> < \<infinity>"
+        using F by (auto simp: setsum_Pinfty)
+      finally show ?thesis by simp
+    qed
+    show "incseq (\<lambda>n. \<Union>i\<le>n. F i)"
+      by (force simp: incseq_def)
+  qed
 qed
 
 subsection {* Measure space induced by distribution of @{const measurable}-functions *}
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/ZF/Games.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -418,22 +418,22 @@
 proof (induct x rule: wf_induct[OF wf_option_of]) 
   case (1 "g")  
   show ?case
-  proof (auto)
-    {case (goal1 y) 
-      from goal1 have "(y, g) \<in> option_of" by (auto)
+  proof (auto, goals)
+    {case prems: (1 y) 
+      from prems have "(y, g) \<in> option_of" by (auto)
       with 1 have "ge_game (y, y)" by auto
-      with goal1 have "\<not> ge_game (g, y)" 
+      with prems have "\<not> ge_game (g, y)" 
         by (subst ge_game_eq, auto)
-      with goal1 show ?case by auto}
+      with prems show ?case by auto}
     note right = this
-    {case (goal2 y)
-      from goal2 have "(y, g) \<in> option_of" by (auto)
+    {case prems: (2 y)
+      from prems have "(y, g) \<in> option_of" by (auto)
       with 1 have "ge_game (y, y)" by auto
-      with goal2 have "\<not> ge_game (y, g)" 
+      with prems have "\<not> ge_game (y, g)" 
         by (subst ge_game_eq, auto)
-      with goal2 show ?case by auto}
+      with prems show ?case by auto}
     note left = this
-    {case goal3
+    {case 3
       from left right show ?case
         by (subst ge_game_eq, auto)
     }
@@ -462,8 +462,8 @@
     proof (induct a rule: induct_game)
       case (1 a)
       show ?case
-      proof (rule allI | rule impI)+
-        case (goal1 x y z)
+      proof ((rule allI | rule impI)+, goals)
+        case prems: (1 x y z)
         show ?case
         proof -
           { fix xr
@@ -471,10 +471,10 @@
             assume a: "ge_game (z, xr)"
             have "ge_game (y, xr)"
               apply (rule 1[rule_format, where y="[y,z,xr]"])
-              apply (auto intro: xr lprod_3_1 simp add: goal1 a)
+              apply (auto intro: xr lprod_3_1 simp add: prems a)
               done
             moreover from xr have "\<not> ge_game (y, xr)"
-              by (simp add: goal1(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
+              by (simp add: prems(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
             ultimately have "False" by auto      
           }
           note xr = this
@@ -483,10 +483,10 @@
             assume a: "ge_game (zl, x)"
             have "ge_game (zl, y)"
               apply (rule 1[rule_format, where y="[zl,x,y]"])
-              apply (auto intro: zl lprod_3_2 simp add: goal1 a)
+              apply (auto intro: zl lprod_3_2 simp add: prems a)
               done
             moreover from zl have "\<not> ge_game (zl, y)"
-              by (simp add: goal1(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
+              by (simp add: prems(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
             ultimately have "False" by auto
           }
           note zl = this
@@ -542,21 +542,18 @@
 
 lemma plus_game_zero_right[simp]: "plus_game G zero_game = G"
 proof -
-  { 
-    fix G H
-    have "H = zero_game \<longrightarrow> plus_game G H = G "
-    proof (induct G H rule: plus_game.induct, rule impI)
-      case (goal1 G H)
-      note induct_hyp = this[simplified goal1, simplified] and this
-      show ?case
-        apply (simp only: plus_game.simps[where G=G and H=H])
-        apply (simp add: game_ext_eq goal1)
-        apply (auto simp add: 
-          zimage_cong [where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
-          induct_hyp)
-        done
-    qed
-  }
+  have "H = zero_game \<longrightarrow> plus_game G H = G " for G H
+  proof (induct G H rule: plus_game.induct, rule impI, goals)
+    case prems: (1 G H)
+    note induct_hyp = this[simplified prems, simplified] and this
+    show ?case
+      apply (simp only: plus_game.simps[where G=G and H=H])
+      apply (simp add: game_ext_eq prems)
+      apply (auto simp add: 
+        zimage_cong [where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
+        induct_hyp)
+      done
+  qed
   then show ?thesis by auto
 qed
 
@@ -585,36 +582,33 @@
   
 lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)"
 proof -
-  { 
-    fix a
-    have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game F G) H = plus_game F (plus_game G H)"
-    proof (induct a rule: induct_game, (rule impI | rule allI)+)
-      case (goal1 x F G H)
-      let ?L = "plus_game (plus_game F G) H"
-      let ?R = "plus_game F (plus_game G H)"
-      note options_plus = left_options_plus right_options_plus
-      {
-        fix opt
-        note hyp = goal1(1)[simplified goal1(2), rule_format] 
-        have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
-          by (blast intro: hyp lprod_3_3)
-        have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
-          by (blast intro: hyp lprod_3_4)
-        have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game F G) opt = plus_game F (plus_game G opt)" 
-          by (blast intro: hyp lprod_3_5)
-        note F and G and H
-      }
-      note induct_hyp = this
-      have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
-        by (auto simp add: 
-          plus_game.simps[where G="plus_game F G" and H=H]
-          plus_game.simps[where G="F" and H="plus_game G H"] 
-          zet_ext_eq zunion zimage_iff options_plus
-          induct_hyp left_imp_options right_imp_options)
-      then show ?case
-        by (simp add: game_ext_eq)
-    qed
-  }
+  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
+  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
+    case prems: (1 x F G H)
+    let ?L = "plus_game (plus_game F G) H"
+    let ?R = "plus_game F (plus_game G H)"
+    note options_plus = left_options_plus right_options_plus
+    {
+      fix opt
+      note hyp = prems(1)[simplified prems(2), rule_format] 
+      have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
+        by (blast intro: hyp lprod_3_3)
+      have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
+        by (blast intro: hyp lprod_3_4)
+      have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game F G) opt = plus_game F (plus_game G opt)" 
+        by (blast intro: hyp lprod_3_5)
+      note F and G and H
+    }
+    note induct_hyp = this
+    have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
+      by (auto simp add: 
+        plus_game.simps[where G="plus_game F G" and H=H]
+        plus_game.simps[where G="F" and H="plus_game G H"] 
+        zet_ext_eq zunion zimage_iff options_plus
+        induct_hyp left_imp_options right_imp_options)
+    then show ?case
+      by (simp add: game_ext_eq)
+  qed
   then show ?thesis by auto
 qed
 
@@ -632,58 +626,38 @@
 qed
 
 lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
-proof (induct x rule: wf_induct[OF wf_option_of])
-  case (goal1 x)
-  { fix y
-    assume "zin y (options x)"
-    then have "eq_game (plus_game y (neg_game y)) zero_game"
-      by (auto simp add: goal1)
-  }
-  note ihyp = this
-  {
-    fix y
-    assume y: "zin y (right_options x)"
-    have "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
-      apply (subst ge_game.simps, simp)
-      apply (rule exI[where x="plus_game y (neg_game y)"])
-      apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
-      apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: y)
-      done
-  }
-  note case1 = this
-  {
-    fix y
-    assume y: "zin y (left_options x)"
-    have "\<not> (ge_game (zero_game, plus_game x (neg_game y)))"
-      apply (subst ge_game.simps, simp)
-      apply (rule exI[where x="plus_game y (neg_game y)"])
-      apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
-      apply (auto simp add: left_options_plus zunion zimage_iff intro: y)
-      done
-  }
-  note case2 = this
-  {
-    fix y
-    assume y: "zin y (left_options x)"
-    have "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
-      apply (subst ge_game.simps, simp)
-      apply (rule exI[where x="plus_game y (neg_game y)"])
-      apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
-      apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: y)
-      done
-  }
-  note case3 = this
-  {
-    fix y
-    assume y: "zin y (right_options x)"
-    have "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
-      apply (subst ge_game.simps, simp)
-      apply (rule exI[where x="plus_game y (neg_game y)"])
-      apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
-      apply (auto simp add: right_options_plus zunion zimage_iff intro: y)
-      done
-  }
-  note case4 = this
+proof (induct x rule: wf_induct[OF wf_option_of], goals)
+  case prems: (1 x)
+  then have ihyp: "eq_game (plus_game y (neg_game y)) zero_game" if "zin y (options x)" for y
+    using that by (auto simp add: prems)
+  have case1: "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
+    if y: "zin y (right_options x)" for y
+    apply (subst ge_game.simps, simp)
+    apply (rule exI[where x="plus_game y (neg_game y)"])
+    apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
+    apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: y)
+    done
+  have case2: "\<not> (ge_game (zero_game, plus_game x (neg_game y)))"
+    if y: "zin y (left_options x)" for y
+    apply (subst ge_game.simps, simp)
+    apply (rule exI[where x="plus_game y (neg_game y)"])
+    apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
+    apply (auto simp add: left_options_plus zunion zimage_iff intro: y)
+    done
+  have case3: "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
+    if y: "zin y (left_options x)" for y
+    apply (subst ge_game.simps, simp)
+    apply (rule exI[where x="plus_game y (neg_game y)"])
+    apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
+    apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: y)
+    done
+  have case4: "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
+    if y: "zin y (right_options x)" for y
+    apply (subst ge_game.simps, simp)
+    apply (rule exI[where x="plus_game y (neg_game y)"])
+    apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
+    apply (auto simp add: right_options_plus zunion zimage_iff intro: y)
+    done
   show ?case
     apply (simp add: eq_game_def)
     apply (simp add: ge_game.simps[of "plus_game x (neg_game x)" "zero_game"])
@@ -695,112 +669,109 @@
 
 lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
 proof -
-  { fix a
-    have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
-    proof (induct a rule: induct_game, (rule impI | rule allI)+)
-      case (goal1 a x y z)
-      note induct_hyp = goal1(1)[rule_format, simplified goal1(2)]
-      { 
-        assume hyp: "ge_game(plus_game x y, plus_game x z)"
-        have "ge_game (y, z)"
-        proof -
-          { fix yr
-            assume yr: "zin yr (right_options y)"
-            from hyp have "\<not> (ge_game (plus_game x z, plus_game x yr))"
-              by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
-                right_options_plus zunion zimage_iff intro: yr)
-            then have "\<not> (ge_game (z, yr))"
-              apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
-              apply (simp_all add: yr lprod_3_6)
-              done
-          }
-          note yr = this
-          { fix zl
-            assume zl: "zin zl (left_options z)"
-            from hyp have "\<not> (ge_game (plus_game x zl, plus_game x y))"
-              by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
-                left_options_plus zunion zimage_iff intro: zl)
-            then have "\<not> (ge_game (zl, y))"
-              apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
-              apply (simp_all add: goal1(2) zl lprod_3_7)
-              done
-          }     
-          note zl = this
-          show "ge_game (y, z)"
-            apply (subst ge_game_eq)
-            apply (auto simp add: yr zl)
+  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
+  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
+    case prems: (1 a x y z)
+    note induct_hyp = prems(1)[rule_format, simplified prems(2)]
+    { 
+      assume hyp: "ge_game(plus_game x y, plus_game x z)"
+      have "ge_game (y, z)"
+      proof -
+        { fix yr
+          assume yr: "zin yr (right_options y)"
+          from hyp have "\<not> (ge_game (plus_game x z, plus_game x yr))"
+            by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
+              right_options_plus zunion zimage_iff intro: yr)
+          then have "\<not> (ge_game (z, yr))"
+            apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
+            apply (simp_all add: yr lprod_3_6)
             done
-        qed      
-      }
-      note right_imp_left = this
-      {
-        assume yz: "ge_game (y, z)"
-        {
-          fix x'
-          assume x': "zin x' (right_options x)"
-          assume hyp: "ge_game (plus_game x z, plus_game x' y)"
-          then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
-            by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"] 
-              right_options_plus zunion zimage_iff intro: x')
-          have t: "ge_game (plus_game x' y, plus_game x' z)"
-            apply (subst induct_hyp[symmetric])
-            apply (auto intro: lprod_3_3 x' yz)
+        }
+        note yr = this
+        { fix zl
+          assume zl: "zin zl (left_options z)"
+          from hyp have "\<not> (ge_game (plus_game x zl, plus_game x y))"
+            by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
+              left_options_plus zunion zimage_iff intro: zl)
+          then have "\<not> (ge_game (zl, y))"
+            apply (subst prems(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
+            apply (simp_all add: prems(2) zl lprod_3_7)
             done
-          from n t have "False" by blast
-        }    
-        note case1 = this
-        {
-          fix x'
-          assume x': "zin x' (left_options x)"
-          assume hyp: "ge_game (plus_game x' z, plus_game x y)"
-          then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
-            by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"] 
-              left_options_plus zunion zimage_iff intro: x')
-          have t: "ge_game (plus_game x' y, plus_game x' z)"
-            apply (subst induct_hyp[symmetric])
-            apply (auto intro: lprod_3_3 x' yz)
-            done
-          from n t have "False" by blast
-        }
-        note case3 = this
-        {
-          fix y'
-          assume y': "zin y' (right_options y)"
-          assume hyp: "ge_game (plus_game x z, plus_game x y')"
-          then have "ge_game(z, y')"
-            apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
-            apply (auto simp add: hyp lprod_3_6 y')
-            done
-          with yz have "ge_game (y, y')"
-            by (blast intro: ge_game_trans)      
-          with y' have "False" by (auto simp add: ge_game_leftright_refl)
-        }
-        note case2 = this
-        {
-          fix z'
-          assume z': "zin z' (left_options z)"
-          assume hyp: "ge_game (plus_game x z', plus_game x y)"
-          then have "ge_game(z', y)"
-            apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
-            apply (auto simp add: hyp lprod_3_7 z')
-            done    
-          with yz have "ge_game (z', z)"
-            by (blast intro: ge_game_trans)      
-          with z' have "False" by (auto simp add: ge_game_leftright_refl)
-        }
-        note case4 = this   
-        have "ge_game(plus_game x y, plus_game x z)"
+        }     
+        note zl = this
+        show "ge_game (y, z)"
           apply (subst ge_game_eq)
-          apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
-          apply (auto intro: case1 case2 case3 case4)
+          apply (auto simp add: yr zl)
           done
+      qed      
+    }
+    note right_imp_left = this
+    {
+      assume yz: "ge_game (y, z)"
+      {
+        fix x'
+        assume x': "zin x' (right_options x)"
+        assume hyp: "ge_game (plus_game x z, plus_game x' y)"
+        then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
+          by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"] 
+            right_options_plus zunion zimage_iff intro: x')
+        have t: "ge_game (plus_game x' y, plus_game x' z)"
+          apply (subst induct_hyp[symmetric])
+          apply (auto intro: lprod_3_3 x' yz)
+          done
+        from n t have "False" by blast
+      }    
+      note case1 = this
+      {
+        fix x'
+        assume x': "zin x' (left_options x)"
+        assume hyp: "ge_game (plus_game x' z, plus_game x y)"
+        then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
+          by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"] 
+            left_options_plus zunion zimage_iff intro: x')
+        have t: "ge_game (plus_game x' y, plus_game x' z)"
+          apply (subst induct_hyp[symmetric])
+          apply (auto intro: lprod_3_3 x' yz)
+          done
+        from n t have "False" by blast
       }
-      note left_imp_right = this
-      show ?case by (auto intro: right_imp_left left_imp_right)
-    qed
-  }
-  note a = this[of "[x, y, z]"]
-  then show ?thesis by blast
+      note case3 = this
+      {
+        fix y'
+        assume y': "zin y' (right_options y)"
+        assume hyp: "ge_game (plus_game x z, plus_game x y')"
+        then have "ge_game(z, y')"
+          apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
+          apply (auto simp add: hyp lprod_3_6 y')
+          done
+        with yz have "ge_game (y, y')"
+          by (blast intro: ge_game_trans)      
+        with y' have "False" by (auto simp add: ge_game_leftright_refl)
+      }
+      note case2 = this
+      {
+        fix z'
+        assume z': "zin z' (left_options z)"
+        assume hyp: "ge_game (plus_game x z', plus_game x y)"
+        then have "ge_game(z', y)"
+          apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
+          apply (auto simp add: hyp lprod_3_7 z')
+          done    
+        with yz have "ge_game (z', z)"
+          by (blast intro: ge_game_trans)      
+        with z' have "False" by (auto simp add: ge_game_leftright_refl)
+      }
+      note case4 = this   
+      have "ge_game(plus_game x y, plus_game x z)"
+        apply (subst ge_game_eq)
+        apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
+        apply (auto intro: case1 case2 case3 case4)
+        done
+    }
+    note left_imp_right = this
+    show ?case by (auto intro: right_imp_left left_imp_right)
+  qed
+  from this[of "[x, y, z]"] show ?thesis by blast
 qed
 
 lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game y x, plus_game z x)"
@@ -808,34 +779,31 @@
 
 lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
 proof -
-  { fix a
-    have "\<forall> x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)"
-    proof (induct a rule: induct_game, (rule impI | rule allI)+)
-      case (goal1 a x y)
-      note ihyp = goal1(1)[rule_format, simplified goal1(2)]
-      { fix xl
-        assume xl: "zin xl (left_options x)"
-        have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)"
-          apply (subst ihyp)
-          apply (auto simp add: lprod_2_1 xl)
-          done
-      }
-      note xl = this
-      { fix yr
-        assume yr: "zin yr (right_options y)"
-        have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)"
-          apply (subst ihyp)
-          apply (auto simp add: lprod_2_2 yr)
-          done
-      }
-      note yr = this
-      show ?case
-        by (auto simp add: ge_game_eq[of "neg_game x" "neg_game y"] ge_game_eq[of "y" "x"]
-          right_options_neg left_options_neg zimage_iff  xl yr)
-    qed
-  }
-  note a = this[of "[x,y]"]
-  then show ?thesis by blast
+  have "\<forall>x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)" for a
+  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
+    case prems: (1 a x y)
+    note ihyp = prems(1)[rule_format, simplified prems(2)]
+    { fix xl
+      assume xl: "zin xl (left_options x)"
+      have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)"
+        apply (subst ihyp)
+        apply (auto simp add: lprod_2_1 xl)
+        done
+    }
+    note xl = this
+    { fix yr
+      assume yr: "zin yr (right_options y)"
+      have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)"
+        apply (subst ihyp)
+        apply (auto simp add: lprod_2_2 yr)
+        done
+    }
+    note yr = this
+    show ?case
+      by (auto simp add: ge_game_eq[of "neg_game x" "neg_game y"] ge_game_eq[of "y" "x"]
+        right_options_neg left_options_neg zimage_iff  xl yr)
+  qed
+  from this[of "[x,y]"] show ?thesis by blast
 qed
 
 definition eq_game_rel :: "(game * game) set" where
@@ -974,4 +942,3 @@
 qed
 
 end
-
diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/ex/Tree23.thy
--- a/src/HOL/ex/Tree23.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/ex/Tree23.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -377,16 +377,26 @@
      done
   } note B = this
   show "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
-  proof (induct k t arbitrary: n rule: del.induct)
-    { case goal1 thus "dfull n (del (Some k) Empty)" by simp }
-    { case goal2 thus "dfull n (del None (Branch2 Empty p Empty))" by simp }
-    { case goal3 thus "dfull n (del None (Branch3 Empty p Empty q Empty))"
-        by simp }
-    { case goal4 thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
-        by (simp split: ord.split) }
-    { case goal5 thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
-        by (simp split: ord.split) }
-    { case goal26 thus ?case by simp }
+  proof (induct k t arbitrary: n rule: del.induct, goals)
+    case (1 k n)
+    thus "dfull n (del (Some k) Empty)" by simp
+  next
+    case (2 p n)
+    thus "dfull n (del None (Branch2 Empty p Empty))" by simp
+  next
+    case (3 p q n)
+    thus "dfull n (del None (Branch3 Empty p Empty q Empty))" by simp
+  next
+    case (4 v p n)
+    thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
+      by (simp split: ord.split)
+  next
+    case (5 v p q n)
+    thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
+      by (simp split: ord.split)
+  next
+    case (26 n)
+    thus ?case by simp
   qed (fact A | fact B)+
 qed