tuned proofs;
authorwenzelm
Thu Jun 25 23:33:47 2015 +0200 (2015-06-25)
changeset 605807e741e22d7fc
parent 60579 915da29bf5d9
child 60581 d2fbc021a44d
tuned proofs;
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/GCD.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Product_Order.thy
src/HOL/Library/RBT_Set.thy
src/HOL/Library/While_Combinator.thy
src/HOL/List.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Nominal/Examples/Pattern.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Probability/Embed_Measure.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/ZF/Games.thy
src/HOL/ex/Tree23.thy
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 25 22:56:33 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 25 23:33:47 2015 +0200
     1.3 @@ -908,13 +908,13 @@
     1.4  subsection \<open>Miscellaneous lemmas about indexes, decrementation, substitution  etc ...\<close>
     1.5  
     1.6  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
     1.7 -proof (induct p arbitrary: n rule: poly.induct, auto)
     1.8 -  case (goal1 c n p n')
     1.9 +proof (induct p arbitrary: n rule: poly.induct, auto, goals)
    1.10 +  case prems: (1 c n p n')
    1.11    then have "n = Suc (n - 1)"
    1.12      by simp
    1.13    then have "isnpolyh p (Suc (n - 1))"
    1.14      using \<open>isnpolyh p n\<close> by simp
    1.15 -  with goal1(2) show ?case
    1.16 +  with prems(2) show ?case
    1.17      by simp
    1.18  qed
    1.19  
     2.1 --- a/src/HOL/GCD.thy	Thu Jun 25 22:56:33 2015 +0200
     2.2 +++ b/src/HOL/GCD.thy	Thu Jun 25 23:33:47 2015 +0200
     2.3 @@ -1451,17 +1451,19 @@
     2.4  
     2.5  subsection {* The complete divisibility lattice *}
     2.6  
     2.7 -interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
     2.8 -proof
     2.9 -  case goal3 thus ?case by(metis gcd_unique_nat)
    2.10 +interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
    2.11 +proof (default, goals)
    2.12 +  case 3
    2.13 +  thus ?case by(metis gcd_unique_nat)
    2.14  qed auto
    2.15  
    2.16 -interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
    2.17 -proof
    2.18 -  case goal3 thus ?case by(metis lcm_unique_nat)
    2.19 +interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
    2.20 +proof (default, goals)
    2.21 +  case 3
    2.22 +  thus ?case by(metis lcm_unique_nat)
    2.23  qed auto
    2.24  
    2.25 -interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm ..
    2.26 +interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
    2.27  
    2.28  text{* Lifting gcd and lcm to sets (Gcd/Lcm).
    2.29  Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
    2.30 @@ -1522,23 +1524,28 @@
    2.31  
    2.32  interpretation gcd_lcm_complete_lattice_nat:
    2.33    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
    2.34 -where
    2.35 -  "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
    2.36 +where "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
    2.37    and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
    2.38  proof -
    2.39    show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
    2.40 -  proof
    2.41 -    case goal1 thus ?case by (simp add: Gcd_nat_def)
    2.42 +  proof (default, goals)
    2.43 +    case 1
    2.44 +    thus ?case by (simp add: Gcd_nat_def)
    2.45    next
    2.46 -    case goal2 thus ?case by (simp add: Gcd_nat_def)
    2.47 +    case 2
    2.48 +    thus ?case by (simp add: Gcd_nat_def)
    2.49    next
    2.50 -    case goal5 show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
    2.51 +    case 5
    2.52 +    show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
    2.53    next
    2.54 -    case goal6 show ?case by (simp add: Lcm_nat_empty)
    2.55 +    case 6
    2.56 +    show ?case by (simp add: Lcm_nat_empty)
    2.57    next
    2.58 -    case goal3 thus ?case by simp
    2.59 +    case 3
    2.60 +    thus ?case by simp
    2.61    next
    2.62 -    case goal4 thus ?case by simp
    2.63 +    case 4
    2.64 +    thus ?case by simp
    2.65    qed
    2.66    then interpret gcd_lcm_complete_lattice_nat:
    2.67      complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
     3.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Jun 25 22:56:33 2015 +0200
     3.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Jun 25 23:33:47 2015 +0200
     3.3 @@ -333,11 +333,11 @@
     3.4  | "ereal r + -\<infinity> = - \<infinity>"
     3.5  | "-\<infinity> + ereal p = -(\<infinity>::ereal)"
     3.6  | "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
     3.7 -proof -
     3.8 -  case (goal1 P x)
     3.9 +proof goals
    3.10 +  case prems: (1 P x)
    3.11    then obtain a b where "x = (a, b)"
    3.12      by (cases x) auto
    3.13 -  with goal1 show P
    3.14 +  with prems show P
    3.15     by (cases rule: ereal2_cases[of a b]) auto
    3.16  qed auto
    3.17  termination by default (rule wf_empty)
    3.18 @@ -437,10 +437,10 @@
    3.19  | "ereal x    < \<infinity>           \<longleftrightarrow> True"
    3.20  | "        -\<infinity> < ereal r     \<longleftrightarrow> True"
    3.21  | "        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
    3.22 -proof -
    3.23 -  case (goal1 P x)
    3.24 +proof goals
    3.25 +  case prems: (1 P x)
    3.26    then obtain a b where "x = (a,b)" by (cases x) auto
    3.27 -  with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
    3.28 +  with prems show P by (cases rule: ereal2_cases[of a b]) auto
    3.29  qed simp_all
    3.30  termination by (relation "{}") simp
    3.31  
    3.32 @@ -860,11 +860,11 @@
    3.33  | "-(\<infinity>::ereal) * \<infinity> = -\<infinity>"
    3.34  | "(\<infinity>::ereal) * -\<infinity> = -\<infinity>"
    3.35  | "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
    3.36 -proof -
    3.37 -  case (goal1 P x)
    3.38 +proof goals
    3.39 +  case prems: (1 P x)
    3.40    then obtain a b where "x = (a, b)"
    3.41      by (cases x) auto
    3.42 -  with goal1 show P
    3.43 +  with prems show P
    3.44      by (cases rule: ereal2_cases[of a b]) auto
    3.45  qed simp_all
    3.46  termination by (relation "{}") simp
     4.1 --- a/src/HOL/Library/Product_Order.thy	Thu Jun 25 22:56:33 2015 +0200
     4.2 +++ b/src/HOL/Library/Product_Order.thy	Thu Jun 25 23:33:47 2015 +0200
     4.3 @@ -233,11 +233,13 @@
     4.4  
     4.5  instance prod ::
     4.6    (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
     4.7 -proof
     4.8 -  case goal1 thus ?case
     4.9 +proof (default, goals)
    4.10 +  case 1
    4.11 +  then show ?case
    4.12      by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
    4.13  next
    4.14 -  case goal2 thus ?case
    4.15 +  case 2
    4.16 +  then show ?case
    4.17      by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
    4.18  qed
    4.19  
     5.1 --- a/src/HOL/Library/RBT_Set.thy	Thu Jun 25 22:56:33 2015 +0200
     5.2 +++ b/src/HOL/Library/RBT_Set.thy	Thu Jun 25 23:33:47 2015 +0200
     5.3 @@ -294,27 +294,32 @@
     5.4  using assms 
     5.5  proof (induction t rule: rbt_min_opt_induct)
     5.6    case empty
     5.7 -    then show ?case by simp
     5.8 +  then show ?case by simp
     5.9  next
    5.10    case left_empty
    5.11 -    then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
    5.12 +  then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
    5.13  next
    5.14    case (left_non_empty c t1 k v t2 y)
    5.15 -    then have "y = k \<or> y \<in> set (RBT_Impl.keys t1) \<or> y \<in> set (RBT_Impl.keys t2)" by auto
    5.16 -    with left_non_empty show ?case 
    5.17 -    proof(elim disjE)
    5.18 -      case goal1 then show ?case 
    5.19 -        by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
    5.20 -    next
    5.21 -      case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch)
    5.22 -    next 
    5.23 -      case goal3 show ?case
    5.24 -      proof -
    5.25 -        from goal3 have "rbt_min_opt t1 \<le> k" by (simp add: left_le_key rbt_min_opt_in_set)
    5.26 -        moreover from goal3 have "k \<le> y" by (simp add: key_le_right)
    5.27 -        ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch)
    5.28 -      qed
    5.29 -    qed
    5.30 +  then consider "y = k" | "y \<in> set (RBT_Impl.keys t1)" | "y \<in> set (RBT_Impl.keys t2)"
    5.31 +    by auto
    5.32 +  then show ?case 
    5.33 +  proof cases
    5.34 +    case 1
    5.35 +    with left_non_empty show ?thesis
    5.36 +      by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
    5.37 +  next
    5.38 +    case 2
    5.39 +    with left_non_empty show ?thesis
    5.40 +      by (auto simp add: rbt_min_opt_Branch)
    5.41 +  next 
    5.42 +    case y: 3
    5.43 +    have "rbt_min_opt t1 \<le> k"
    5.44 +      using left_non_empty by (simp add: left_le_key rbt_min_opt_in_set)
    5.45 +    moreover have "k \<le> y"
    5.46 +      using left_non_empty y by (simp add: key_le_right)
    5.47 +    ultimately show ?thesis
    5.48 +      using left_non_empty y by (simp add: rbt_min_opt_Branch)
    5.49 +  qed
    5.50  qed
    5.51  
    5.52  lemma rbt_min_eq_rbt_min_opt:
    5.53 @@ -388,27 +393,32 @@
    5.54  using assms 
    5.55  proof (induction t rule: rbt_max_opt_induct)
    5.56    case empty
    5.57 -    then show ?case by simp
    5.58 +  then show ?case by simp
    5.59  next
    5.60    case right_empty
    5.61 -    then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
    5.62 +  then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
    5.63  next
    5.64    case (right_non_empty c t1 k v t2 y)
    5.65 -    then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto
    5.66 -    with right_non_empty show ?case 
    5.67 -    proof(elim disjE)
    5.68 -      case goal1 then show ?case 
    5.69 -        by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
    5.70 -    next
    5.71 -      case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch)
    5.72 -    next 
    5.73 -      case goal3 show ?case
    5.74 -      proof -
    5.75 -        from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set)
    5.76 -        moreover from goal3 have "y \<le> k" by (simp add: left_le_key)
    5.77 -        ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch)
    5.78 -      qed
    5.79 -    qed
    5.80 +  then consider "y = k" | "y \<in> set (RBT_Impl.keys t2)" | "y \<in> set (RBT_Impl.keys t1)"
    5.81 +    by auto
    5.82 +  then show ?case 
    5.83 +  proof cases
    5.84 +    case 1
    5.85 +    with right_non_empty show ?thesis
    5.86 +      by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
    5.87 +  next
    5.88 +    case 2
    5.89 +    with right_non_empty show ?thesis
    5.90 +      by (auto simp add: rbt_max_opt_Branch)
    5.91 +  next 
    5.92 +    case y: 3
    5.93 +    have "rbt_max_opt t2 \<ge> k"
    5.94 +      using right_non_empty by (simp add: key_le_right rbt_max_opt_in_set)
    5.95 +    moreover have "y \<le> k"
    5.96 +      using right_non_empty y by (simp add: left_le_key)
    5.97 +    ultimately show ?thesis
    5.98 +      using right_non_empty by (simp add: rbt_max_opt_Branch)
    5.99 +  qed
   5.100  qed
   5.101  
   5.102  lemma rbt_max_eq_rbt_max_opt:
     6.1 --- a/src/HOL/Library/While_Combinator.thy	Thu Jun 25 22:56:33 2015 +0200
     6.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu Jun 25 23:33:47 2015 +0200
     6.3 @@ -157,14 +157,15 @@
     6.4      note b = this(1) and body = this(2) and inv = this(3)
     6.5      hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
     6.6      ultimately show ?thesis unfolding Suc using b
     6.7 -    proof (intro Least_equality[symmetric])
     6.8 -      case goal1
     6.9 +    proof (intro Least_equality[symmetric], goals)
    6.10 +      case 1
    6.11        hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
    6.12          by (auto simp: BodyCommute inv b)
    6.13        have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b)
    6.14        with Test show ?case by (auto simp: TestCommute)
    6.15      next
    6.16 -      case goal2 thus ?case by (metis not_less_eq_eq)
    6.17 +      case 2
    6.18 +      thus ?case by (metis not_less_eq_eq)
    6.19      qed
    6.20    qed
    6.21    have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
     7.1 --- a/src/HOL/List.thy	Thu Jun 25 22:56:33 2015 +0200
     7.2 +++ b/src/HOL/List.thy	Thu Jun 25 23:33:47 2015 +0200
     7.3 @@ -2308,19 +2308,29 @@
     7.4    "\<lbrakk> \<And> i. \<lbrakk> i < n ; i < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) ; n < length xs \<Longrightarrow> \<not> P (xs ! n) \<rbrakk> \<Longrightarrow>
     7.5    takeWhile P xs = take n xs"
     7.6  proof (induct xs arbitrary: n)
     7.7 +  case Nil
     7.8 +  thus ?case by simp
     7.9 +next
    7.10    case (Cons x xs)
    7.11 -  thus ?case
    7.12 +  show ?case
    7.13    proof (cases n)
    7.14 -    case (Suc n') note this[simp]
    7.15 +    case 0
    7.16 +    with Cons show ?thesis by simp
    7.17 +  next
    7.18 +    case [simp]: (Suc n')
    7.19      have "P x" using Cons.prems(1)[of 0] by simp
    7.20      moreover have "takeWhile P xs = take n' xs"
    7.21      proof (rule Cons.hyps)
    7.22 -      case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
    7.23 -    next case goal2 thus ?case using Cons by auto
    7.24 +      fix i
    7.25 +      assume "i < n'" "i < length xs"
    7.26 +      thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
    7.27 +    next
    7.28 +      assume "n' < length xs"
    7.29 +      thus "\<not> P (xs ! n')" using Cons by auto
    7.30      qed
    7.31      ultimately show ?thesis by simp
    7.32 -   qed simp
    7.33 -qed simp
    7.34 +   qed
    7.35 +qed
    7.36  
    7.37  lemma nth_length_takeWhile:
    7.38    "length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
     8.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Jun 25 22:56:33 2015 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Jun 25 23:33:47 2015 +0200
     8.3 @@ -1337,22 +1337,25 @@
     8.4    obtains q where "\<forall>i<n. q i < p"
     8.5      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"
     8.6  proof -
     8.7 -  let ?rl = "reduced n\<circ>label"
     8.8 +  let ?rl = "reduced n \<circ> label"
     8.9    let ?A = "{s. ksimplex p n s \<and> ?rl ` s = {..n}}"
    8.10    have "odd (card ?A)"
    8.11      using assms by (intro kuhn_combinatorial[of p n label]) auto
    8.12    then have "?A \<noteq> {}"
    8.13 -    by (intro notI) simp
    8.14 +    by fastforce
    8.15    then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}"
    8.16      by (auto elim: ksimplex.cases)
    8.17    interpret kuhn_simplex p n b u s by fact
    8.18  
    8.19    show ?thesis
    8.20    proof (intro that[of b] allI impI)
    8.21 -    fix i assume "i < n" then show "b i < p"
    8.22 +    fix i
    8.23 +    assume "i < n"
    8.24 +    then show "b i < p"
    8.25        using base by auto
    8.26    next
    8.27 -    case goal2
    8.28 +    fix i
    8.29 +    assume "i < n"
    8.30      then have "i \<in> {.. n}" "Suc i \<in> {.. n}"
    8.31        by auto
    8.32      then obtain u v where u: "u \<in> s" "Suc i = ?rl u" and v: "v \<in> s" "i = ?rl v"
    8.33 @@ -1363,10 +1366,11 @@
    8.34          u(2)[symmetric] v(2)[symmetric] \<open>i < n\<close>
    8.35        by auto
    8.36      moreover
    8.37 -    { fix j assume "j < n"
    8.38 -      then have "b j \<le> u j" "u j \<le> b j + 1" "b j \<le> v j" "v j \<le> b j + 1"
    8.39 -        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 }
    8.40 -    ultimately show ?case
    8.41 +    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
    8.42 +      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>]
    8.43 +      by auto
    8.44 +    ultimately show "\<exists>r s. (\<forall>j<n. b j \<le> r j \<and> r j \<le> b j + 1) \<and>
    8.45 +        (\<forall>j<n. b j \<le> s j \<and> s j \<le> b j + 1) \<and> label r i \<noteq> label s i"
    8.46        by blast
    8.47    qed
    8.48  qed
    8.49 @@ -1392,23 +1396,20 @@
    8.50      apply rule
    8.51      apply rule
    8.52    proof -
    8.53 -    case goal1
    8.54 +    fix x x'
    8.55      let ?R = "\<lambda>y::nat.
    8.56 -      (P x \<and> Q xa \<and> x xa = 0 \<longrightarrow> y = 0) \<and>
    8.57 -      (P x \<and> Q xa \<and> x xa = 1 \<longrightarrow> y = 1) \<and>
    8.58 -      (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x xa \<le> (f x) xa) \<and>
    8.59 -      (P x \<and> Q xa \<and> y = 1 \<longrightarrow> (f x) xa \<le> x xa)"
    8.60 -    {
    8.61 -      assume "P x" and "Q xa"
    8.62 -      then have "0 \<le> f x xa \<and> f x xa \<le> 1"
    8.63 -        using assms(2)[rule_format,of "f x" xa]
    8.64 -        apply (drule_tac assms(1)[rule_format])
    8.65 -        apply auto
    8.66 -        done
    8.67 -    }
    8.68 +      (P x \<and> Q x' \<and> x x' = 0 \<longrightarrow> y = 0) \<and>
    8.69 +      (P x \<and> Q x' \<and> x x' = 1 \<longrightarrow> y = 1) \<and>
    8.70 +      (P x \<and> Q x' \<and> y = 0 \<longrightarrow> x x' \<le> (f x) x') \<and>
    8.71 +      (P x \<and> Q x' \<and> y = 1 \<longrightarrow> (f x) x' \<le> x x')"
    8.72 +    have "0 \<le> f x x' \<and> f x x' \<le> 1" if "P x" "Q x'"
    8.73 +      using assms(2)[rule_format,of "f x" x'] that
    8.74 +      apply (drule_tac assms(1)[rule_format])
    8.75 +      apply auto
    8.76 +      done
    8.77      then have "?R 0 \<or> ?R 1"
    8.78        by auto
    8.79 -    then show ?case
    8.80 +    then show "\<exists>y\<le>1. ?R y"
    8.81        by auto
    8.82    qed
    8.83  qed
    8.84 @@ -1988,17 +1989,17 @@
    8.85    assumes "e > 0"
    8.86    shows "\<not> (frontier (cball a e) retract_of (cball a e))"
    8.87  proof
    8.88 -  case goal1
    8.89 -  have *: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
    8.90 +  assume *: "frontier (cball a e) retract_of (cball a e)"
    8.91 +  have **: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
    8.92      using scaleR_left_distrib[of 1 1 a] by auto
    8.93    obtain x where x:
    8.94        "x \<in> {x. norm (a - x) = e}"
    8.95        "2 *\<^sub>R a - x = x"
    8.96 -    apply (rule retract_fixpoint_property[OF goal1, of "\<lambda>x. scaleR 2 a - x"])
    8.97 +    apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
    8.98      apply (blast intro: brouwer_ball[OF assms])
    8.99      apply (intro continuous_intros)
   8.100      unfolding frontier_cball subset_eq Ball_def image_iff dist_norm
   8.101 -    apply (auto simp add: * norm_minus_commute)
   8.102 +    apply (auto simp add: ** norm_minus_commute)
   8.103      done
   8.104    then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
   8.105      by (auto simp add: algebra_simps)
     9.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Thu Jun 25 22:56:33 2015 +0200
     9.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Thu Jun 25 23:33:47 2015 +0200
     9.3 @@ -62,20 +62,20 @@
     9.4    by (simp add: supp_def Collect_disj_eq del: disj_not1)
     9.5  
     9.6  instance pat :: pt_name
     9.7 -proof intro_classes
     9.8 -  case goal1
     9.9 +proof (default, goals)
    9.10 +  case (1 x)
    9.11    show ?case by (induct x) simp_all
    9.12  next
    9.13 -  case goal2
    9.14 +  case (2 _ _ x)
    9.15    show ?case by (induct x) (simp_all add: pt_name2)
    9.16  next
    9.17 -  case goal3
    9.18 +  case (3 _ _ x)
    9.19    then show ?case by (induct x) (simp_all add: pt_name3)
    9.20  qed
    9.21  
    9.22  instance pat :: fs_name
    9.23 -proof intro_classes
    9.24 -  case goal1
    9.25 +proof (default, goals)
    9.26 +  case (1 x)
    9.27    show ?case by (induct x) (simp_all add: fin_supp)
    9.28  qed
    9.29  
    10.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Jun 25 22:56:33 2015 +0200
    10.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Jun 25 23:33:47 2015 +0200
    10.3 @@ -2202,7 +2202,6 @@
    10.4    have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at)
    10.5    show ?thesis
    10.6    proof (rule equalityI)
    10.7 -    case goal1
    10.8      show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
    10.9        apply(auto simp add: perm_set_def)
   10.10        apply(rule_tac x="pi\<bullet>xb" in exI)
   10.11 @@ -2218,7 +2217,6 @@
   10.12        apply(rule pt_fun_app_eq[OF pt, OF at])
   10.13        done
   10.14    next
   10.15 -    case goal2
   10.16      show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
   10.17        apply(auto simp add: perm_set_def)
   10.18        apply(rule_tac x="(rev pi)\<bullet>x" in exI)
    11.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 22:56:33 2015 +0200
    11.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 23:33:47 2015 +0200
    11.3 @@ -1527,14 +1527,19 @@
    11.4  definition [simp]:
    11.5    "normalization_factor_int = (sgn :: int \<Rightarrow> int)"
    11.6  
    11.7 -instance proof
    11.8 -  case goal2 then show ?case by (auto simp add: abs_mult nat_mult_distrib)
    11.9 +instance
   11.10 +proof (default, goals)
   11.11 +  case 2
   11.12 +  then show ?case by (auto simp add: abs_mult nat_mult_distrib)
   11.13  next
   11.14 -  case goal3 then show ?case by (simp add: zsgn_def)
   11.15 +  case 3
   11.16 +  then show ?case by (simp add: zsgn_def)
   11.17  next
   11.18 -  case goal5 then show ?case by (auto simp: zsgn_def)
   11.19 +  case 5
   11.20 +  then show ?case by (auto simp: zsgn_def)
   11.21  next
   11.22 -  case goal6 then show ?case by (auto split: abs_split simp: zsgn_def)
   11.23 +  case 6
   11.24 +  then show ?case by (auto split: abs_split simp: zsgn_def)
   11.25  qed (auto simp: sgn_times split: abs_split)
   11.26  
   11.27  end
    12.1 --- a/src/HOL/Probability/Embed_Measure.thy	Thu Jun 25 22:56:33 2015 +0200
    12.2 +++ b/src/HOL/Probability/Embed_Measure.thy	Thu Jun 25 23:33:47 2015 +0200
    12.3 @@ -154,22 +154,22 @@
    12.4  lemma sigma_finite_embed_measure:
    12.5    assumes "sigma_finite_measure M" and inj: "inj f"
    12.6    shows "sigma_finite_measure (embed_measure M f)"
    12.7 -proof
    12.8 -  case goal1
    12.9 +proof -
   12.10    from assms(1) interpret sigma_finite_measure M .
   12.11    from sigma_finite_countable obtain A where
   12.12        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
   12.13 -  show ?case
   12.14 -  proof (intro exI[of _ "op ` f`A"] conjI allI)
   12.15 -    from A_props show "countable (op ` f`A)" by auto
   12.16 -    from inj and A_props show "op ` f`A \<subseteq> sets (embed_measure M f)" 
   12.17 -      by (auto simp: sets_embed_measure)
   12.18 -    from A_props and inj show "\<Union>(op ` f`A) = space (embed_measure M f)"
   12.19 -      by (auto simp: space_embed_measure intro!: imageI)
   12.20 -    from A_props and inj show "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
   12.21 -      by (intro ballI, subst emeasure_embed_measure)
   12.22 -         (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
   12.23 -  qed
   12.24 +  from A_props have "countable (op ` f`A)" by auto
   12.25 +  moreover
   12.26 +  from inj and A_props have "op ` f`A \<subseteq> sets (embed_measure M f)" 
   12.27 +    by (auto simp: sets_embed_measure)
   12.28 +  moreover
   12.29 +  from A_props and inj have "\<Union>(op ` f`A) = space (embed_measure M f)"
   12.30 +    by (auto simp: space_embed_measure intro!: imageI)
   12.31 +  moreover
   12.32 +  from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
   12.33 +    by (intro ballI, subst emeasure_embed_measure)
   12.34 +       (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
   12.35 +  ultimately show ?thesis by - (default, blast)
   12.36  qed
   12.37  
   12.38  lemma embed_measure_count_space':
    13.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Thu Jun 25 22:56:33 2015 +0200
    13.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Thu Jun 25 23:33:47 2015 +0200
    13.3 @@ -192,20 +192,22 @@
    13.4  lemma PiM_cong:
    13.5    assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
    13.6    shows "PiM I M = PiM J N"
    13.7 -unfolding PiM_def
    13.8 -proof (rule extend_measure_cong)
    13.9 -  case goal1 show ?case using assms
   13.10 +  unfolding PiM_def
   13.11 +proof (rule extend_measure_cong, goals)
   13.12 +  case 1
   13.13 +  show ?case using assms
   13.14      by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
   13.15  next
   13.16 -  case goal2
   13.17 +  case 2
   13.18    have "\<And>K. K \<subseteq> J \<Longrightarrow> (\<Pi> j\<in>K. sets (M j)) = (\<Pi> j\<in>K. sets (N j))"
   13.19      using assms by (intro Pi_cong_sets) auto
   13.20    thus ?case by (auto simp: assms)
   13.21  next
   13.22 -  case goal3 show ?case using assms 
   13.23 +  case 3
   13.24 +  show ?case using assms 
   13.25      by (intro ext) (auto simp: prod_emb_def dest: PiE_mem)
   13.26  next
   13.27 -  case (goal4 x)
   13.28 +  case (4 x)
   13.29    thus ?case using assms 
   13.30      by (auto intro!: setprod.cong split: split_if_asm)
   13.31  qed
    14.1 --- a/src/HOL/Probability/Information.thy	Thu Jun 25 22:56:33 2015 +0200
    14.2 +++ b/src/HOL/Probability/Information.thy	Thu Jun 25 23:33:47 2015 +0200
    14.3 @@ -1022,11 +1022,12 @@
    14.4      Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
    14.5      Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
    14.6    proof eventually_elim
    14.7 -    case (goal1 x)
    14.8 +    case (elim x)
    14.9      show ?case
   14.10      proof cases
   14.11        assume "Pxyz x \<noteq> 0"
   14.12 -      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"
   14.13 +      with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
   14.14 +        "0 < Pyz (snd x)" "0 < Pxyz x"
   14.15          by auto
   14.16        then show ?thesis
   14.17          using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
   14.18 @@ -1252,11 +1253,12 @@
   14.19      Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
   14.20      Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
   14.21    proof eventually_elim
   14.22 -    case (goal1 x)
   14.23 +    case (elim x)
   14.24      show ?case
   14.25      proof cases
   14.26        assume "Pxyz x \<noteq> 0"
   14.27 -      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"
   14.28 +      with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
   14.29 +        "0 < Pyz (snd x)" "0 < Pxyz x"
   14.30          by auto
   14.31        then show ?thesis
   14.32          using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
   14.33 @@ -1730,11 +1732,11 @@
   14.34      Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
   14.35      (is "AE x in _. ?f x = ?g x")
   14.36    proof eventually_elim
   14.37 -    case (goal1 x)
   14.38 +    case (elim x)
   14.39      show ?case
   14.40      proof cases
   14.41        assume "Pxy x \<noteq> 0"
   14.42 -      with goal1 have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
   14.43 +      with elim have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
   14.44          by auto
   14.45        then show ?thesis
   14.46          using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
    15.1 --- a/src/HOL/Probability/Measure_Space.thy	Thu Jun 25 22:56:33 2015 +0200
    15.2 +++ b/src/HOL/Probability/Measure_Space.thy	Thu Jun 25 23:33:47 2015 +0200
    15.3 @@ -1134,44 +1134,56 @@
    15.4  lemma (in sigma_finite_measure) sigma_finite_disjoint:
    15.5    obtains A :: "nat \<Rightarrow> 'a set"
    15.6    where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "disjoint_family A"
    15.7 -proof atomize_elim
    15.8 -  case goal1
    15.9 +proof -
   15.10    obtain A :: "nat \<Rightarrow> 'a set" where
   15.11      range: "range A \<subseteq> sets M" and
   15.12      space: "(\<Union>i. A i) = space M" and
   15.13      measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
   15.14      using sigma_finite by auto
   15.15 -  note range' = sets.range_disjointed_sets[OF range] range
   15.16 -  { fix i
   15.17 -    have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
   15.18 -      using range' disjointed_subset[of A i] by (auto intro!: emeasure_mono)
   15.19 -    then have "emeasure M (disjointed A i) \<noteq> \<infinity>"
   15.20 -      using measure[of i] by auto }
   15.21 -  with disjoint_family_disjointed UN_disjointed_eq[of A] space range'
   15.22 -  show ?case by (auto intro!: exI[of _ "disjointed A"])
   15.23 +  show thesis
   15.24 +  proof (rule that[of "disjointed A"])
   15.25 +    show "range (disjointed A) \<subseteq> sets M"
   15.26 +      by (rule sets.range_disjointed_sets[OF range])
   15.27 +    show "(\<Union>i. disjointed A i) = space M"
   15.28 +      and "disjoint_family (disjointed A)"
   15.29 +      using disjoint_family_disjointed UN_disjointed_eq[of A] space range
   15.30 +      by auto
   15.31 +    show "emeasure M (disjointed A i) \<noteq> \<infinity>" for i
   15.32 +    proof -
   15.33 +      have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
   15.34 +        using range disjointed_subset[of A i] by (auto intro!: emeasure_mono)
   15.35 +      then show ?thesis using measure[of i] by auto
   15.36 +    qed
   15.37 +  qed
   15.38  qed
   15.39  
   15.40  lemma (in sigma_finite_measure) sigma_finite_incseq:
   15.41    obtains A :: "nat \<Rightarrow> 'a set"
   15.42    where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "incseq A"
   15.43 -proof atomize_elim
   15.44 -  case goal1
   15.45 +proof -
   15.46    obtain F :: "nat \<Rightarrow> 'a set" where
   15.47      F: "range F \<subseteq> sets M" "(\<Union>i. F i) = space M" "\<And>i. emeasure M (F i) \<noteq> \<infinity>"
   15.48      using sigma_finite by auto
   15.49 -  then show ?case
   15.50 -  proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI)
   15.51 -    from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
   15.52 -    then show "(\<Union>n. \<Union> i\<le>n. F i) = space M"
   15.53 -      using F by fastforce
   15.54 -  next
   15.55 -    fix n
   15.56 -    have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))" using F
   15.57 -      by (auto intro!: emeasure_subadditive_finite)
   15.58 -    also have "\<dots> < \<infinity>"
   15.59 -      using F by (auto simp: setsum_Pinfty)
   15.60 -    finally show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" by simp
   15.61 -  qed (force simp: incseq_def)+
   15.62 +  show thesis
   15.63 +  proof (rule that[of "\<lambda>n. \<Union>i\<le>n. F i"])
   15.64 +    show "range (\<lambda>n. \<Union>i\<le>n. F i) \<subseteq> sets M"
   15.65 +      using F by (force simp: incseq_def)
   15.66 +    show "(\<Union>n. \<Union>i\<le>n. F i) = space M"
   15.67 +    proof -
   15.68 +      from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
   15.69 +      with F show ?thesis by fastforce
   15.70 +    qed
   15.71 +    show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" for n
   15.72 +    proof -
   15.73 +      have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))"
   15.74 +        using F by (auto intro!: emeasure_subadditive_finite)
   15.75 +      also have "\<dots> < \<infinity>"
   15.76 +        using F by (auto simp: setsum_Pinfty)
   15.77 +      finally show ?thesis by simp
   15.78 +    qed
   15.79 +    show "incseq (\<lambda>n. \<Union>i\<le>n. F i)"
   15.80 +      by (force simp: incseq_def)
   15.81 +  qed
   15.82  qed
   15.83  
   15.84  subsection {* Measure space induced by distribution of @{const measurable}-functions *}
    16.1 --- a/src/HOL/ZF/Games.thy	Thu Jun 25 22:56:33 2015 +0200
    16.2 +++ b/src/HOL/ZF/Games.thy	Thu Jun 25 23:33:47 2015 +0200
    16.3 @@ -418,22 +418,22 @@
    16.4  proof (induct x rule: wf_induct[OF wf_option_of]) 
    16.5    case (1 "g")  
    16.6    show ?case
    16.7 -  proof (auto)
    16.8 -    {case (goal1 y) 
    16.9 -      from goal1 have "(y, g) \<in> option_of" by (auto)
   16.10 +  proof (auto, goals)
   16.11 +    {case prems: (1 y) 
   16.12 +      from prems have "(y, g) \<in> option_of" by (auto)
   16.13        with 1 have "ge_game (y, y)" by auto
   16.14 -      with goal1 have "\<not> ge_game (g, y)" 
   16.15 +      with prems have "\<not> ge_game (g, y)" 
   16.16          by (subst ge_game_eq, auto)
   16.17 -      with goal1 show ?case by auto}
   16.18 +      with prems show ?case by auto}
   16.19      note right = this
   16.20 -    {case (goal2 y)
   16.21 -      from goal2 have "(y, g) \<in> option_of" by (auto)
   16.22 +    {case prems: (2 y)
   16.23 +      from prems have "(y, g) \<in> option_of" by (auto)
   16.24        with 1 have "ge_game (y, y)" by auto
   16.25 -      with goal2 have "\<not> ge_game (y, g)" 
   16.26 +      with prems have "\<not> ge_game (y, g)" 
   16.27          by (subst ge_game_eq, auto)
   16.28 -      with goal2 show ?case by auto}
   16.29 +      with prems show ?case by auto}
   16.30      note left = this
   16.31 -    {case goal3
   16.32 +    {case 3
   16.33        from left right show ?case
   16.34          by (subst ge_game_eq, auto)
   16.35      }
   16.36 @@ -462,8 +462,8 @@
   16.37      proof (induct a rule: induct_game)
   16.38        case (1 a)
   16.39        show ?case
   16.40 -      proof (rule allI | rule impI)+
   16.41 -        case (goal1 x y z)
   16.42 +      proof ((rule allI | rule impI)+, goals)
   16.43 +        case prems: (1 x y z)
   16.44          show ?case
   16.45          proof -
   16.46            { fix xr
   16.47 @@ -471,10 +471,10 @@
   16.48              assume a: "ge_game (z, xr)"
   16.49              have "ge_game (y, xr)"
   16.50                apply (rule 1[rule_format, where y="[y,z,xr]"])
   16.51 -              apply (auto intro: xr lprod_3_1 simp add: goal1 a)
   16.52 +              apply (auto intro: xr lprod_3_1 simp add: prems a)
   16.53                done
   16.54              moreover from xr have "\<not> ge_game (y, xr)"
   16.55 -              by (simp add: goal1(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
   16.56 +              by (simp add: prems(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
   16.57              ultimately have "False" by auto      
   16.58            }
   16.59            note xr = this
   16.60 @@ -483,10 +483,10 @@
   16.61              assume a: "ge_game (zl, x)"
   16.62              have "ge_game (zl, y)"
   16.63                apply (rule 1[rule_format, where y="[zl,x,y]"])
   16.64 -              apply (auto intro: zl lprod_3_2 simp add: goal1 a)
   16.65 +              apply (auto intro: zl lprod_3_2 simp add: prems a)
   16.66                done
   16.67              moreover from zl have "\<not> ge_game (zl, y)"
   16.68 -              by (simp add: goal1(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
   16.69 +              by (simp add: prems(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
   16.70              ultimately have "False" by auto
   16.71            }
   16.72            note zl = this
   16.73 @@ -542,21 +542,18 @@
   16.74  
   16.75  lemma plus_game_zero_right[simp]: "plus_game G zero_game = G"
   16.76  proof -
   16.77 -  { 
   16.78 -    fix G H
   16.79 -    have "H = zero_game \<longrightarrow> plus_game G H = G "
   16.80 -    proof (induct G H rule: plus_game.induct, rule impI)
   16.81 -      case (goal1 G H)
   16.82 -      note induct_hyp = this[simplified goal1, simplified] and this
   16.83 -      show ?case
   16.84 -        apply (simp only: plus_game.simps[where G=G and H=H])
   16.85 -        apply (simp add: game_ext_eq goal1)
   16.86 -        apply (auto simp add: 
   16.87 -          zimage_cong [where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
   16.88 -          induct_hyp)
   16.89 -        done
   16.90 -    qed
   16.91 -  }
   16.92 +  have "H = zero_game \<longrightarrow> plus_game G H = G " for G H
   16.93 +  proof (induct G H rule: plus_game.induct, rule impI, goals)
   16.94 +    case prems: (1 G H)
   16.95 +    note induct_hyp = this[simplified prems, simplified] and this
   16.96 +    show ?case
   16.97 +      apply (simp only: plus_game.simps[where G=G and H=H])
   16.98 +      apply (simp add: game_ext_eq prems)
   16.99 +      apply (auto simp add: 
  16.100 +        zimage_cong [where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
  16.101 +        induct_hyp)
  16.102 +      done
  16.103 +  qed
  16.104    then show ?thesis by auto
  16.105  qed
  16.106  
  16.107 @@ -585,36 +582,33 @@
  16.108    
  16.109  lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)"
  16.110  proof -
  16.111 -  { 
  16.112 -    fix a
  16.113 -    have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game F G) H = plus_game F (plus_game G H)"
  16.114 -    proof (induct a rule: induct_game, (rule impI | rule allI)+)
  16.115 -      case (goal1 x F G H)
  16.116 -      let ?L = "plus_game (plus_game F G) H"
  16.117 -      let ?R = "plus_game F (plus_game G H)"
  16.118 -      note options_plus = left_options_plus right_options_plus
  16.119 -      {
  16.120 -        fix opt
  16.121 -        note hyp = goal1(1)[simplified goal1(2), rule_format] 
  16.122 -        have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
  16.123 -          by (blast intro: hyp lprod_3_3)
  16.124 -        have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
  16.125 -          by (blast intro: hyp lprod_3_4)
  16.126 -        have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game F G) opt = plus_game F (plus_game G opt)" 
  16.127 -          by (blast intro: hyp lprod_3_5)
  16.128 -        note F and G and H
  16.129 -      }
  16.130 -      note induct_hyp = this
  16.131 -      have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
  16.132 -        by (auto simp add: 
  16.133 -          plus_game.simps[where G="plus_game F G" and H=H]
  16.134 -          plus_game.simps[where G="F" and H="plus_game G H"] 
  16.135 -          zet_ext_eq zunion zimage_iff options_plus
  16.136 -          induct_hyp left_imp_options right_imp_options)
  16.137 -      then show ?case
  16.138 -        by (simp add: game_ext_eq)
  16.139 -    qed
  16.140 -  }
  16.141 +  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
  16.142 +  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
  16.143 +    case prems: (1 x F G H)
  16.144 +    let ?L = "plus_game (plus_game F G) H"
  16.145 +    let ?R = "plus_game F (plus_game G H)"
  16.146 +    note options_plus = left_options_plus right_options_plus
  16.147 +    {
  16.148 +      fix opt
  16.149 +      note hyp = prems(1)[simplified prems(2), rule_format] 
  16.150 +      have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
  16.151 +        by (blast intro: hyp lprod_3_3)
  16.152 +      have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
  16.153 +        by (blast intro: hyp lprod_3_4)
  16.154 +      have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game F G) opt = plus_game F (plus_game G opt)" 
  16.155 +        by (blast intro: hyp lprod_3_5)
  16.156 +      note F and G and H
  16.157 +    }
  16.158 +    note induct_hyp = this
  16.159 +    have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
  16.160 +      by (auto simp add: 
  16.161 +        plus_game.simps[where G="plus_game F G" and H=H]
  16.162 +        plus_game.simps[where G="F" and H="plus_game G H"] 
  16.163 +        zet_ext_eq zunion zimage_iff options_plus
  16.164 +        induct_hyp left_imp_options right_imp_options)
  16.165 +    then show ?case
  16.166 +      by (simp add: game_ext_eq)
  16.167 +  qed
  16.168    then show ?thesis by auto
  16.169  qed
  16.170  
  16.171 @@ -632,58 +626,38 @@
  16.172  qed
  16.173  
  16.174  lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
  16.175 -proof (induct x rule: wf_induct[OF wf_option_of])
  16.176 -  case (goal1 x)
  16.177 -  { fix y
  16.178 -    assume "zin y (options x)"
  16.179 -    then have "eq_game (plus_game y (neg_game y)) zero_game"
  16.180 -      by (auto simp add: goal1)
  16.181 -  }
  16.182 -  note ihyp = this
  16.183 -  {
  16.184 -    fix y
  16.185 -    assume y: "zin y (right_options x)"
  16.186 -    have "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
  16.187 -      apply (subst ge_game.simps, simp)
  16.188 -      apply (rule exI[where x="plus_game y (neg_game y)"])
  16.189 -      apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
  16.190 -      apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: y)
  16.191 -      done
  16.192 -  }
  16.193 -  note case1 = this
  16.194 -  {
  16.195 -    fix y
  16.196 -    assume y: "zin y (left_options x)"
  16.197 -    have "\<not> (ge_game (zero_game, plus_game x (neg_game y)))"
  16.198 -      apply (subst ge_game.simps, simp)
  16.199 -      apply (rule exI[where x="plus_game y (neg_game y)"])
  16.200 -      apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
  16.201 -      apply (auto simp add: left_options_plus zunion zimage_iff intro: y)
  16.202 -      done
  16.203 -  }
  16.204 -  note case2 = this
  16.205 -  {
  16.206 -    fix y
  16.207 -    assume y: "zin y (left_options x)"
  16.208 -    have "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
  16.209 -      apply (subst ge_game.simps, simp)
  16.210 -      apply (rule exI[where x="plus_game y (neg_game y)"])
  16.211 -      apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
  16.212 -      apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: y)
  16.213 -      done
  16.214 -  }
  16.215 -  note case3 = this
  16.216 -  {
  16.217 -    fix y
  16.218 -    assume y: "zin y (right_options x)"
  16.219 -    have "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
  16.220 -      apply (subst ge_game.simps, simp)
  16.221 -      apply (rule exI[where x="plus_game y (neg_game y)"])
  16.222 -      apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
  16.223 -      apply (auto simp add: right_options_plus zunion zimage_iff intro: y)
  16.224 -      done
  16.225 -  }
  16.226 -  note case4 = this
  16.227 +proof (induct x rule: wf_induct[OF wf_option_of], goals)
  16.228 +  case prems: (1 x)
  16.229 +  then have ihyp: "eq_game (plus_game y (neg_game y)) zero_game" if "zin y (options x)" for y
  16.230 +    using that by (auto simp add: prems)
  16.231 +  have case1: "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
  16.232 +    if y: "zin y (right_options x)" for y
  16.233 +    apply (subst ge_game.simps, simp)
  16.234 +    apply (rule exI[where x="plus_game y (neg_game y)"])
  16.235 +    apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
  16.236 +    apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: y)
  16.237 +    done
  16.238 +  have case2: "\<not> (ge_game (zero_game, plus_game x (neg_game y)))"
  16.239 +    if y: "zin y (left_options x)" for y
  16.240 +    apply (subst ge_game.simps, simp)
  16.241 +    apply (rule exI[where x="plus_game y (neg_game y)"])
  16.242 +    apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
  16.243 +    apply (auto simp add: left_options_plus zunion zimage_iff intro: y)
  16.244 +    done
  16.245 +  have case3: "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
  16.246 +    if y: "zin y (left_options x)" for y
  16.247 +    apply (subst ge_game.simps, simp)
  16.248 +    apply (rule exI[where x="plus_game y (neg_game y)"])
  16.249 +    apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
  16.250 +    apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: y)
  16.251 +    done
  16.252 +  have case4: "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
  16.253 +    if y: "zin y (right_options x)" for y
  16.254 +    apply (subst ge_game.simps, simp)
  16.255 +    apply (rule exI[where x="plus_game y (neg_game y)"])
  16.256 +    apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
  16.257 +    apply (auto simp add: right_options_plus zunion zimage_iff intro: y)
  16.258 +    done
  16.259    show ?case
  16.260      apply (simp add: eq_game_def)
  16.261      apply (simp add: ge_game.simps[of "plus_game x (neg_game x)" "zero_game"])
  16.262 @@ -695,112 +669,109 @@
  16.263  
  16.264  lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
  16.265  proof -
  16.266 -  { fix a
  16.267 -    have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
  16.268 -    proof (induct a rule: induct_game, (rule impI | rule allI)+)
  16.269 -      case (goal1 a x y z)
  16.270 -      note induct_hyp = goal1(1)[rule_format, simplified goal1(2)]
  16.271 -      { 
  16.272 -        assume hyp: "ge_game(plus_game x y, plus_game x z)"
  16.273 -        have "ge_game (y, z)"
  16.274 -        proof -
  16.275 -          { fix yr
  16.276 -            assume yr: "zin yr (right_options y)"
  16.277 -            from hyp have "\<not> (ge_game (plus_game x z, plus_game x yr))"
  16.278 -              by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
  16.279 -                right_options_plus zunion zimage_iff intro: yr)
  16.280 -            then have "\<not> (ge_game (z, yr))"
  16.281 -              apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
  16.282 -              apply (simp_all add: yr lprod_3_6)
  16.283 -              done
  16.284 -          }
  16.285 -          note yr = this
  16.286 -          { fix zl
  16.287 -            assume zl: "zin zl (left_options z)"
  16.288 -            from hyp have "\<not> (ge_game (plus_game x zl, plus_game x y))"
  16.289 -              by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
  16.290 -                left_options_plus zunion zimage_iff intro: zl)
  16.291 -            then have "\<not> (ge_game (zl, y))"
  16.292 -              apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
  16.293 -              apply (simp_all add: goal1(2) zl lprod_3_7)
  16.294 -              done
  16.295 -          }     
  16.296 -          note zl = this
  16.297 -          show "ge_game (y, z)"
  16.298 -            apply (subst ge_game_eq)
  16.299 -            apply (auto simp add: yr zl)
  16.300 +  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
  16.301 +  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
  16.302 +    case prems: (1 a x y z)
  16.303 +    note induct_hyp = prems(1)[rule_format, simplified prems(2)]
  16.304 +    { 
  16.305 +      assume hyp: "ge_game(plus_game x y, plus_game x z)"
  16.306 +      have "ge_game (y, z)"
  16.307 +      proof -
  16.308 +        { fix yr
  16.309 +          assume yr: "zin yr (right_options y)"
  16.310 +          from hyp have "\<not> (ge_game (plus_game x z, plus_game x yr))"
  16.311 +            by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
  16.312 +              right_options_plus zunion zimage_iff intro: yr)
  16.313 +          then have "\<not> (ge_game (z, yr))"
  16.314 +            apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
  16.315 +            apply (simp_all add: yr lprod_3_6)
  16.316              done
  16.317 -        qed      
  16.318 -      }
  16.319 -      note right_imp_left = this
  16.320 -      {
  16.321 -        assume yz: "ge_game (y, z)"
  16.322 -        {
  16.323 -          fix x'
  16.324 -          assume x': "zin x' (right_options x)"
  16.325 -          assume hyp: "ge_game (plus_game x z, plus_game x' y)"
  16.326 -          then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
  16.327 -            by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"] 
  16.328 -              right_options_plus zunion zimage_iff intro: x')
  16.329 -          have t: "ge_game (plus_game x' y, plus_game x' z)"
  16.330 -            apply (subst induct_hyp[symmetric])
  16.331 -            apply (auto intro: lprod_3_3 x' yz)
  16.332 +        }
  16.333 +        note yr = this
  16.334 +        { fix zl
  16.335 +          assume zl: "zin zl (left_options z)"
  16.336 +          from hyp have "\<not> (ge_game (plus_game x zl, plus_game x y))"
  16.337 +            by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
  16.338 +              left_options_plus zunion zimage_iff intro: zl)
  16.339 +          then have "\<not> (ge_game (zl, y))"
  16.340 +            apply (subst prems(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
  16.341 +            apply (simp_all add: prems(2) zl lprod_3_7)
  16.342              done
  16.343 -          from n t have "False" by blast
  16.344 -        }    
  16.345 -        note case1 = this
  16.346 -        {
  16.347 -          fix x'
  16.348 -          assume x': "zin x' (left_options x)"
  16.349 -          assume hyp: "ge_game (plus_game x' z, plus_game x y)"
  16.350 -          then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
  16.351 -            by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"] 
  16.352 -              left_options_plus zunion zimage_iff intro: x')
  16.353 -          have t: "ge_game (plus_game x' y, plus_game x' z)"
  16.354 -            apply (subst induct_hyp[symmetric])
  16.355 -            apply (auto intro: lprod_3_3 x' yz)
  16.356 -            done
  16.357 -          from n t have "False" by blast
  16.358 -        }
  16.359 -        note case3 = this
  16.360 -        {
  16.361 -          fix y'
  16.362 -          assume y': "zin y' (right_options y)"
  16.363 -          assume hyp: "ge_game (plus_game x z, plus_game x y')"
  16.364 -          then have "ge_game(z, y')"
  16.365 -            apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
  16.366 -            apply (auto simp add: hyp lprod_3_6 y')
  16.367 -            done
  16.368 -          with yz have "ge_game (y, y')"
  16.369 -            by (blast intro: ge_game_trans)      
  16.370 -          with y' have "False" by (auto simp add: ge_game_leftright_refl)
  16.371 -        }
  16.372 -        note case2 = this
  16.373 -        {
  16.374 -          fix z'
  16.375 -          assume z': "zin z' (left_options z)"
  16.376 -          assume hyp: "ge_game (plus_game x z', plus_game x y)"
  16.377 -          then have "ge_game(z', y)"
  16.378 -            apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
  16.379 -            apply (auto simp add: hyp lprod_3_7 z')
  16.380 -            done    
  16.381 -          with yz have "ge_game (z', z)"
  16.382 -            by (blast intro: ge_game_trans)      
  16.383 -          with z' have "False" by (auto simp add: ge_game_leftright_refl)
  16.384 -        }
  16.385 -        note case4 = this   
  16.386 -        have "ge_game(plus_game x y, plus_game x z)"
  16.387 +        }     
  16.388 +        note zl = this
  16.389 +        show "ge_game (y, z)"
  16.390            apply (subst ge_game_eq)
  16.391 -          apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
  16.392 -          apply (auto intro: case1 case2 case3 case4)
  16.393 +          apply (auto simp add: yr zl)
  16.394            done
  16.395 +      qed      
  16.396 +    }
  16.397 +    note right_imp_left = this
  16.398 +    {
  16.399 +      assume yz: "ge_game (y, z)"
  16.400 +      {
  16.401 +        fix x'
  16.402 +        assume x': "zin x' (right_options x)"
  16.403 +        assume hyp: "ge_game (plus_game x z, plus_game x' y)"
  16.404 +        then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
  16.405 +          by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"] 
  16.406 +            right_options_plus zunion zimage_iff intro: x')
  16.407 +        have t: "ge_game (plus_game x' y, plus_game x' z)"
  16.408 +          apply (subst induct_hyp[symmetric])
  16.409 +          apply (auto intro: lprod_3_3 x' yz)
  16.410 +          done
  16.411 +        from n t have "False" by blast
  16.412 +      }    
  16.413 +      note case1 = this
  16.414 +      {
  16.415 +        fix x'
  16.416 +        assume x': "zin x' (left_options x)"
  16.417 +        assume hyp: "ge_game (plus_game x' z, plus_game x y)"
  16.418 +        then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
  16.419 +          by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"] 
  16.420 +            left_options_plus zunion zimage_iff intro: x')
  16.421 +        have t: "ge_game (plus_game x' y, plus_game x' z)"
  16.422 +          apply (subst induct_hyp[symmetric])
  16.423 +          apply (auto intro: lprod_3_3 x' yz)
  16.424 +          done
  16.425 +        from n t have "False" by blast
  16.426        }
  16.427 -      note left_imp_right = this
  16.428 -      show ?case by (auto intro: right_imp_left left_imp_right)
  16.429 -    qed
  16.430 -  }
  16.431 -  note a = this[of "[x, y, z]"]
  16.432 -  then show ?thesis by blast
  16.433 +      note case3 = this
  16.434 +      {
  16.435 +        fix y'
  16.436 +        assume y': "zin y' (right_options y)"
  16.437 +        assume hyp: "ge_game (plus_game x z, plus_game x y')"
  16.438 +        then have "ge_game(z, y')"
  16.439 +          apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
  16.440 +          apply (auto simp add: hyp lprod_3_6 y')
  16.441 +          done
  16.442 +        with yz have "ge_game (y, y')"
  16.443 +          by (blast intro: ge_game_trans)      
  16.444 +        with y' have "False" by (auto simp add: ge_game_leftright_refl)
  16.445 +      }
  16.446 +      note case2 = this
  16.447 +      {
  16.448 +        fix z'
  16.449 +        assume z': "zin z' (left_options z)"
  16.450 +        assume hyp: "ge_game (plus_game x z', plus_game x y)"
  16.451 +        then have "ge_game(z', y)"
  16.452 +          apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
  16.453 +          apply (auto simp add: hyp lprod_3_7 z')
  16.454 +          done    
  16.455 +        with yz have "ge_game (z', z)"
  16.456 +          by (blast intro: ge_game_trans)      
  16.457 +        with z' have "False" by (auto simp add: ge_game_leftright_refl)
  16.458 +      }
  16.459 +      note case4 = this   
  16.460 +      have "ge_game(plus_game x y, plus_game x z)"
  16.461 +        apply (subst ge_game_eq)
  16.462 +        apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
  16.463 +        apply (auto intro: case1 case2 case3 case4)
  16.464 +        done
  16.465 +    }
  16.466 +    note left_imp_right = this
  16.467 +    show ?case by (auto intro: right_imp_left left_imp_right)
  16.468 +  qed
  16.469 +  from this[of "[x, y, z]"] show ?thesis by blast
  16.470  qed
  16.471  
  16.472  lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game y x, plus_game z x)"
  16.473 @@ -808,34 +779,31 @@
  16.474  
  16.475  lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
  16.476  proof -
  16.477 -  { fix a
  16.478 -    have "\<forall> x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)"
  16.479 -    proof (induct a rule: induct_game, (rule impI | rule allI)+)
  16.480 -      case (goal1 a x y)
  16.481 -      note ihyp = goal1(1)[rule_format, simplified goal1(2)]
  16.482 -      { fix xl
  16.483 -        assume xl: "zin xl (left_options x)"
  16.484 -        have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)"
  16.485 -          apply (subst ihyp)
  16.486 -          apply (auto simp add: lprod_2_1 xl)
  16.487 -          done
  16.488 -      }
  16.489 -      note xl = this
  16.490 -      { fix yr
  16.491 -        assume yr: "zin yr (right_options y)"
  16.492 -        have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)"
  16.493 -          apply (subst ihyp)
  16.494 -          apply (auto simp add: lprod_2_2 yr)
  16.495 -          done
  16.496 -      }
  16.497 -      note yr = this
  16.498 -      show ?case
  16.499 -        by (auto simp add: ge_game_eq[of "neg_game x" "neg_game y"] ge_game_eq[of "y" "x"]
  16.500 -          right_options_neg left_options_neg zimage_iff  xl yr)
  16.501 -    qed
  16.502 -  }
  16.503 -  note a = this[of "[x,y]"]
  16.504 -  then show ?thesis by blast
  16.505 +  have "\<forall>x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)" for a
  16.506 +  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
  16.507 +    case prems: (1 a x y)
  16.508 +    note ihyp = prems(1)[rule_format, simplified prems(2)]
  16.509 +    { fix xl
  16.510 +      assume xl: "zin xl (left_options x)"
  16.511 +      have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)"
  16.512 +        apply (subst ihyp)
  16.513 +        apply (auto simp add: lprod_2_1 xl)
  16.514 +        done
  16.515 +    }
  16.516 +    note xl = this
  16.517 +    { fix yr
  16.518 +      assume yr: "zin yr (right_options y)"
  16.519 +      have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)"
  16.520 +        apply (subst ihyp)
  16.521 +        apply (auto simp add: lprod_2_2 yr)
  16.522 +        done
  16.523 +    }
  16.524 +    note yr = this
  16.525 +    show ?case
  16.526 +      by (auto simp add: ge_game_eq[of "neg_game x" "neg_game y"] ge_game_eq[of "y" "x"]
  16.527 +        right_options_neg left_options_neg zimage_iff  xl yr)
  16.528 +  qed
  16.529 +  from this[of "[x,y]"] show ?thesis by blast
  16.530  qed
  16.531  
  16.532  definition eq_game_rel :: "(game * game) set" where
  16.533 @@ -974,4 +942,3 @@
  16.534  qed
  16.535  
  16.536  end
  16.537 -
    17.1 --- a/src/HOL/ex/Tree23.thy	Thu Jun 25 22:56:33 2015 +0200
    17.2 +++ b/src/HOL/ex/Tree23.thy	Thu Jun 25 23:33:47 2015 +0200
    17.3 @@ -377,16 +377,26 @@
    17.4       done
    17.5    } note B = this
    17.6    show "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
    17.7 -  proof (induct k t arbitrary: n rule: del.induct)
    17.8 -    { case goal1 thus "dfull n (del (Some k) Empty)" by simp }
    17.9 -    { case goal2 thus "dfull n (del None (Branch2 Empty p Empty))" by simp }
   17.10 -    { case goal3 thus "dfull n (del None (Branch3 Empty p Empty q Empty))"
   17.11 -        by simp }
   17.12 -    { case goal4 thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
   17.13 -        by (simp split: ord.split) }
   17.14 -    { case goal5 thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
   17.15 -        by (simp split: ord.split) }
   17.16 -    { case goal26 thus ?case by simp }
   17.17 +  proof (induct k t arbitrary: n rule: del.induct, goals)
   17.18 +    case (1 k n)
   17.19 +    thus "dfull n (del (Some k) Empty)" by simp
   17.20 +  next
   17.21 +    case (2 p n)
   17.22 +    thus "dfull n (del None (Branch2 Empty p Empty))" by simp
   17.23 +  next
   17.24 +    case (3 p q n)
   17.25 +    thus "dfull n (del None (Branch3 Empty p Empty q Empty))" by simp
   17.26 +  next
   17.27 +    case (4 v p n)
   17.28 +    thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
   17.29 +      by (simp split: ord.split)
   17.30 +  next
   17.31 +    case (5 v p q n)
   17.32 +    thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
   17.33 +      by (simp split: ord.split)
   17.34 +  next
   17.35 +    case (26 n)
   17.36 +    thus ?case by simp
   17.37    qed (fact A | fact B)+
   17.38  qed
   17.39