merged
authorwenzelm
Thu Jun 25 23:51:54 2015 +0200 (2015-06-25)
changeset 60582d694f217ee41
parent 60572 718b1ba06429
parent 60581 d2fbc021a44d
child 60583 a645a0e6d790
merged
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/Admin/isatest/settings/at64-poly	Thu Jun 25 15:01:43 2015 +0200
     1.2 +++ b/Admin/isatest/settings/at64-poly	Thu Jun 25 23:51:54 2015 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  ML_PLATFORM="$ISABELLE_PLATFORM64"
     1.6  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
     1.7 -ML_OPTIONS="--minheap 2000 --maxheap 8000 --gcthreads 1"
     1.8 +ML_OPTIONS="--minheap 4000 --maxheap 16000 --gcthreads 1"
     1.9  
    1.10  ISABELLE_HOME_USER=~/isabelle-at64-poly
    1.11  
     2.1 --- a/NEWS	Thu Jun 25 15:01:43 2015 +0200
     2.2 +++ b/NEWS	Thu Jun 25 23:51:54 2015 +0200
     2.3 @@ -77,6 +77,13 @@
     2.4  INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
     2.5  and always put attributes in front.
     2.6  
     2.7 +* Proof method "goals" turns the current subgoals into cases within the
     2.8 +context; the conclusion is bound to variable ?case in each case.
     2.9 +
    2.10 +* The undocumented feature of implicit cases goal1, goal2, goal3, etc.
    2.11 +is marked as legacy, and will be removed eventually. Note that proof
    2.12 +method "goals" achieves a similar effect within regular Isar.
    2.13 +
    2.14  * Nesting of Isar goal structure has been clarified: the context after
    2.15  the initial backwards refinement is retained for the whole proof, within
    2.16  all its context sections (as indicated via 'next'). This is e.g.
     3.1 --- a/src/Doc/Isar_Ref/Proof.thy	Thu Jun 25 15:01:43 2015 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Thu Jun 25 23:51:54 2015 +0200
     3.3 @@ -818,6 +818,7 @@
     3.4    \begin{matharray}{rcl}
     3.5      @{command_def "print_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\[0.5ex]
     3.6      @{method_def "-"} & : & @{text method} \\
     3.7 +    @{method_def "goals"} & : & @{text method} \\
     3.8      @{method_def "fact"} & : & @{text method} \\
     3.9      @{method_def "assumption"} & : & @{text method} \\
    3.10      @{method_def "this"} & : & @{text method} \\
    3.11 @@ -832,6 +833,8 @@
    3.12    \end{matharray}
    3.13  
    3.14    @{rail \<open>
    3.15 +    @@{method goals} (@{syntax name}*)
    3.16 +    ;
    3.17      @@{method fact} @{syntax thmrefs}?
    3.18      ;
    3.19      @@{method (Pure) rule} @{syntax thmrefs}?
    3.20 @@ -861,12 +864,23 @@
    3.21    rule declarations of the classical reasoner
    3.22    (\secref{sec:classical}).
    3.23  
    3.24 -  \item ``@{method "-"}'' (minus) does nothing but insert the forward
    3.25 -  chaining facts as premises into the goal.  Note that command
    3.26 -  @{command_ref "proof"} without any method actually performs a single
    3.27 -  reduction step using the @{method_ref (Pure) rule} method; thus a plain
    3.28 -  \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
    3.29 -  "-"}'' rather than @{command "proof"} alone.
    3.30 +  \item ``@{method "-"}'' (minus) inserts the forward chaining facts as
    3.31 +  premises into the goal, and nothing else.
    3.32 +
    3.33 +  Note that command @{command_ref "proof"} without any method actually
    3.34 +  performs a single reduction step using the @{method_ref (Pure) rule}
    3.35 +  method; thus a plain \emph{do-nothing} proof step would be ``@{command
    3.36 +  "proof"}~@{text "-"}'' rather than @{command "proof"} alone.
    3.37 +
    3.38 +  \item @{method "goals"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} is like ``@{method "-"}'', but
    3.39 +  the current subgoals are turned into cases within the context (see also
    3.40 +  \secref{sec:cases-induct}). The specified case names are used if present;
    3.41 +  otherwise cases are numbered starting from 1.
    3.42 +
    3.43 +  Invoking cases in the subsequent proof body via the @{command_ref case}
    3.44 +  command will @{command fix} goal parameters, @{command assume} goal
    3.45 +  premises, and @{command let} variable @{variable_ref ?case} refer to the
    3.46 +  conclusion.
    3.47  
    3.48    \item @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from
    3.49    @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from the current proof context)
     4.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 25 15:01:43 2015 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 25 23:51:54 2015 +0200
     4.3 @@ -908,13 +908,13 @@
     4.4  subsection \<open>Miscellaneous lemmas about indexes, decrementation, substitution  etc ...\<close>
     4.5  
     4.6  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
     4.7 -proof (induct p arbitrary: n rule: poly.induct, auto)
     4.8 -  case (goal1 c n p n')
     4.9 +proof (induct p arbitrary: n rule: poly.induct, auto, goals)
    4.10 +  case prems: (1 c n p n')
    4.11    then have "n = Suc (n - 1)"
    4.12      by simp
    4.13    then have "isnpolyh p (Suc (n - 1))"
    4.14      using \<open>isnpolyh p n\<close> by simp
    4.15 -  with goal1(2) show ?case
    4.16 +  with prems(2) show ?case
    4.17      by simp
    4.18  qed
    4.19  
     5.1 --- a/src/HOL/GCD.thy	Thu Jun 25 15:01:43 2015 +0200
     5.2 +++ b/src/HOL/GCD.thy	Thu Jun 25 23:51:54 2015 +0200
     5.3 @@ -1451,17 +1451,19 @@
     5.4  
     5.5  subsection {* The complete divisibility lattice *}
     5.6  
     5.7 -interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
     5.8 -proof
     5.9 -  case goal3 thus ?case by(metis gcd_unique_nat)
    5.10 +interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
    5.11 +proof (default, goals)
    5.12 +  case 3
    5.13 +  thus ?case by(metis gcd_unique_nat)
    5.14  qed auto
    5.15  
    5.16 -interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
    5.17 -proof
    5.18 -  case goal3 thus ?case by(metis lcm_unique_nat)
    5.19 +interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
    5.20 +proof (default, goals)
    5.21 +  case 3
    5.22 +  thus ?case by(metis lcm_unique_nat)
    5.23  qed auto
    5.24  
    5.25 -interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm ..
    5.26 +interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
    5.27  
    5.28  text{* Lifting gcd and lcm to sets (Gcd/Lcm).
    5.29  Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
    5.30 @@ -1522,23 +1524,28 @@
    5.31  
    5.32  interpretation gcd_lcm_complete_lattice_nat:
    5.33    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
    5.34 -where
    5.35 -  "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
    5.36 +where "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
    5.37    and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
    5.38  proof -
    5.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)"
    5.40 -  proof
    5.41 -    case goal1 thus ?case by (simp add: Gcd_nat_def)
    5.42 +  proof (default, goals)
    5.43 +    case 1
    5.44 +    thus ?case by (simp add: Gcd_nat_def)
    5.45    next
    5.46 -    case goal2 thus ?case by (simp add: Gcd_nat_def)
    5.47 +    case 2
    5.48 +    thus ?case by (simp add: Gcd_nat_def)
    5.49    next
    5.50 -    case goal5 show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
    5.51 +    case 5
    5.52 +    show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
    5.53    next
    5.54 -    case goal6 show ?case by (simp add: Lcm_nat_empty)
    5.55 +    case 6
    5.56 +    show ?case by (simp add: Lcm_nat_empty)
    5.57    next
    5.58 -    case goal3 thus ?case by simp
    5.59 +    case 3
    5.60 +    thus ?case by simp
    5.61    next
    5.62 -    case goal4 thus ?case by simp
    5.63 +    case 4
    5.64 +    thus ?case by simp
    5.65    qed
    5.66    then interpret gcd_lcm_complete_lattice_nat:
    5.67      complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
     6.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Jun 25 15:01:43 2015 +0200
     6.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Jun 25 23:51:54 2015 +0200
     6.3 @@ -333,11 +333,11 @@
     6.4  | "ereal r + -\<infinity> = - \<infinity>"
     6.5  | "-\<infinity> + ereal p = -(\<infinity>::ereal)"
     6.6  | "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
     6.7 -proof -
     6.8 -  case (goal1 P x)
     6.9 +proof goals
    6.10 +  case prems: (1 P x)
    6.11    then obtain a b where "x = (a, b)"
    6.12      by (cases x) auto
    6.13 -  with goal1 show P
    6.14 +  with prems show P
    6.15     by (cases rule: ereal2_cases[of a b]) auto
    6.16  qed auto
    6.17  termination by default (rule wf_empty)
    6.18 @@ -437,10 +437,10 @@
    6.19  | "ereal x    < \<infinity>           \<longleftrightarrow> True"
    6.20  | "        -\<infinity> < ereal r     \<longleftrightarrow> True"
    6.21  | "        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
    6.22 -proof -
    6.23 -  case (goal1 P x)
    6.24 +proof goals
    6.25 +  case prems: (1 P x)
    6.26    then obtain a b where "x = (a,b)" by (cases x) auto
    6.27 -  with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
    6.28 +  with prems show P by (cases rule: ereal2_cases[of a b]) auto
    6.29  qed simp_all
    6.30  termination by (relation "{}") simp
    6.31  
    6.32 @@ -860,11 +860,11 @@
    6.33  | "-(\<infinity>::ereal) * \<infinity> = -\<infinity>"
    6.34  | "(\<infinity>::ereal) * -\<infinity> = -\<infinity>"
    6.35  | "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
    6.36 -proof -
    6.37 -  case (goal1 P x)
    6.38 +proof goals
    6.39 +  case prems: (1 P x)
    6.40    then obtain a b where "x = (a, b)"
    6.41      by (cases x) auto
    6.42 -  with goal1 show P
    6.43 +  with prems show P
    6.44      by (cases rule: ereal2_cases[of a b]) auto
    6.45  qed simp_all
    6.46  termination by (relation "{}") simp
     7.1 --- a/src/HOL/Library/Product_Order.thy	Thu Jun 25 15:01:43 2015 +0200
     7.2 +++ b/src/HOL/Library/Product_Order.thy	Thu Jun 25 23:51:54 2015 +0200
     7.3 @@ -233,11 +233,13 @@
     7.4  
     7.5  instance prod ::
     7.6    (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
     7.7 -proof
     7.8 -  case goal1 thus ?case
     7.9 +proof (default, goals)
    7.10 +  case 1
    7.11 +  then show ?case
    7.12      by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
    7.13  next
    7.14 -  case goal2 thus ?case
    7.15 +  case 2
    7.16 +  then show ?case
    7.17      by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
    7.18  qed
    7.19  
     8.1 --- a/src/HOL/Library/RBT_Set.thy	Thu Jun 25 15:01:43 2015 +0200
     8.2 +++ b/src/HOL/Library/RBT_Set.thy	Thu Jun 25 23:51:54 2015 +0200
     8.3 @@ -294,27 +294,32 @@
     8.4  using assms 
     8.5  proof (induction t rule: rbt_min_opt_induct)
     8.6    case empty
     8.7 -    then show ?case by simp
     8.8 +  then show ?case by simp
     8.9  next
    8.10    case left_empty
    8.11 -    then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
    8.12 +  then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
    8.13  next
    8.14    case (left_non_empty c t1 k v t2 y)
    8.15 -    then have "y = k \<or> y \<in> set (RBT_Impl.keys t1) \<or> y \<in> set (RBT_Impl.keys t2)" by auto
    8.16 -    with left_non_empty show ?case 
    8.17 -    proof(elim disjE)
    8.18 -      case goal1 then show ?case 
    8.19 -        by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
    8.20 -    next
    8.21 -      case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch)
    8.22 -    next 
    8.23 -      case goal3 show ?case
    8.24 -      proof -
    8.25 -        from goal3 have "rbt_min_opt t1 \<le> k" by (simp add: left_le_key rbt_min_opt_in_set)
    8.26 -        moreover from goal3 have "k \<le> y" by (simp add: key_le_right)
    8.27 -        ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch)
    8.28 -      qed
    8.29 -    qed
    8.30 +  then consider "y = k" | "y \<in> set (RBT_Impl.keys t1)" | "y \<in> set (RBT_Impl.keys t2)"
    8.31 +    by auto
    8.32 +  then show ?case 
    8.33 +  proof cases
    8.34 +    case 1
    8.35 +    with left_non_empty show ?thesis
    8.36 +      by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
    8.37 +  next
    8.38 +    case 2
    8.39 +    with left_non_empty show ?thesis
    8.40 +      by (auto simp add: rbt_min_opt_Branch)
    8.41 +  next 
    8.42 +    case y: 3
    8.43 +    have "rbt_min_opt t1 \<le> k"
    8.44 +      using left_non_empty by (simp add: left_le_key rbt_min_opt_in_set)
    8.45 +    moreover have "k \<le> y"
    8.46 +      using left_non_empty y by (simp add: key_le_right)
    8.47 +    ultimately show ?thesis
    8.48 +      using left_non_empty y by (simp add: rbt_min_opt_Branch)
    8.49 +  qed
    8.50  qed
    8.51  
    8.52  lemma rbt_min_eq_rbt_min_opt:
    8.53 @@ -388,27 +393,32 @@
    8.54  using assms 
    8.55  proof (induction t rule: rbt_max_opt_induct)
    8.56    case empty
    8.57 -    then show ?case by simp
    8.58 +  then show ?case by simp
    8.59  next
    8.60    case right_empty
    8.61 -    then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
    8.62 +  then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
    8.63  next
    8.64    case (right_non_empty c t1 k v t2 y)
    8.65 -    then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto
    8.66 -    with right_non_empty show ?case 
    8.67 -    proof(elim disjE)
    8.68 -      case goal1 then show ?case 
    8.69 -        by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
    8.70 -    next
    8.71 -      case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch)
    8.72 -    next 
    8.73 -      case goal3 show ?case
    8.74 -      proof -
    8.75 -        from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set)
    8.76 -        moreover from goal3 have "y \<le> k" by (simp add: left_le_key)
    8.77 -        ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch)
    8.78 -      qed
    8.79 -    qed
    8.80 +  then consider "y = k" | "y \<in> set (RBT_Impl.keys t2)" | "y \<in> set (RBT_Impl.keys t1)"
    8.81 +    by auto
    8.82 +  then show ?case 
    8.83 +  proof cases
    8.84 +    case 1
    8.85 +    with right_non_empty show ?thesis
    8.86 +      by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
    8.87 +  next
    8.88 +    case 2
    8.89 +    with right_non_empty show ?thesis
    8.90 +      by (auto simp add: rbt_max_opt_Branch)
    8.91 +  next 
    8.92 +    case y: 3
    8.93 +    have "rbt_max_opt t2 \<ge> k"
    8.94 +      using right_non_empty by (simp add: key_le_right rbt_max_opt_in_set)
    8.95 +    moreover have "y \<le> k"
    8.96 +      using right_non_empty y by (simp add: left_le_key)
    8.97 +    ultimately show ?thesis
    8.98 +      using right_non_empty by (simp add: rbt_max_opt_Branch)
    8.99 +  qed
   8.100  qed
   8.101  
   8.102  lemma rbt_max_eq_rbt_max_opt:
     9.1 --- a/src/HOL/Library/While_Combinator.thy	Thu Jun 25 15:01:43 2015 +0200
     9.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu Jun 25 23:51:54 2015 +0200
     9.3 @@ -157,14 +157,15 @@
     9.4      note b = this(1) and body = this(2) and inv = this(3)
     9.5      hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
     9.6      ultimately show ?thesis unfolding Suc using b
     9.7 -    proof (intro Least_equality[symmetric])
     9.8 -      case goal1
     9.9 +    proof (intro Least_equality[symmetric], goals)
    9.10 +      case 1
    9.11        hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
    9.12          by (auto simp: BodyCommute inv b)
    9.13        have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b)
    9.14        with Test show ?case by (auto simp: TestCommute)
    9.15      next
    9.16 -      case goal2 thus ?case by (metis not_less_eq_eq)
    9.17 +      case 2
    9.18 +      thus ?case by (metis not_less_eq_eq)
    9.19      qed
    9.20    qed
    9.21    have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
    10.1 --- a/src/HOL/List.thy	Thu Jun 25 15:01:43 2015 +0200
    10.2 +++ b/src/HOL/List.thy	Thu Jun 25 23:51:54 2015 +0200
    10.3 @@ -2308,19 +2308,29 @@
    10.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>
    10.5    takeWhile P xs = take n xs"
    10.6  proof (induct xs arbitrary: n)
    10.7 +  case Nil
    10.8 +  thus ?case by simp
    10.9 +next
   10.10    case (Cons x xs)
   10.11 -  thus ?case
   10.12 +  show ?case
   10.13    proof (cases n)
   10.14 -    case (Suc n') note this[simp]
   10.15 +    case 0
   10.16 +    with Cons show ?thesis by simp
   10.17 +  next
   10.18 +    case [simp]: (Suc n')
   10.19      have "P x" using Cons.prems(1)[of 0] by simp
   10.20      moreover have "takeWhile P xs = take n' xs"
   10.21      proof (rule Cons.hyps)
   10.22 -      case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
   10.23 -    next case goal2 thus ?case using Cons by auto
   10.24 +      fix i
   10.25 +      assume "i < n'" "i < length xs"
   10.26 +      thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
   10.27 +    next
   10.28 +      assume "n' < length xs"
   10.29 +      thus "\<not> P (xs ! n')" using Cons by auto
   10.30      qed
   10.31      ultimately show ?thesis by simp
   10.32 -   qed simp
   10.33 -qed simp
   10.34 +   qed
   10.35 +qed
   10.36  
   10.37  lemma nth_length_takeWhile:
   10.38    "length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
    11.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Jun 25 15:01:43 2015 +0200
    11.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Jun 25 23:51:54 2015 +0200
    11.3 @@ -1337,22 +1337,25 @@
    11.4    obtains q where "\<forall>i<n. q i < p"
    11.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"
    11.6  proof -
    11.7 -  let ?rl = "reduced n\<circ>label"
    11.8 +  let ?rl = "reduced n \<circ> label"
    11.9    let ?A = "{s. ksimplex p n s \<and> ?rl ` s = {..n}}"
   11.10    have "odd (card ?A)"
   11.11      using assms by (intro kuhn_combinatorial[of p n label]) auto
   11.12    then have "?A \<noteq> {}"
   11.13 -    by (intro notI) simp
   11.14 +    by fastforce
   11.15    then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}"
   11.16      by (auto elim: ksimplex.cases)
   11.17    interpret kuhn_simplex p n b u s by fact
   11.18  
   11.19    show ?thesis
   11.20    proof (intro that[of b] allI impI)
   11.21 -    fix i assume "i < n" then show "b i < p"
   11.22 +    fix i
   11.23 +    assume "i < n"
   11.24 +    then show "b i < p"
   11.25        using base by auto
   11.26    next
   11.27 -    case goal2
   11.28 +    fix i
   11.29 +    assume "i < n"
   11.30      then have "i \<in> {.. n}" "Suc i \<in> {.. n}"
   11.31        by auto
   11.32      then obtain u v where u: "u \<in> s" "Suc i = ?rl u" and v: "v \<in> s" "i = ?rl v"
   11.33 @@ -1363,10 +1366,11 @@
   11.34          u(2)[symmetric] v(2)[symmetric] \<open>i < n\<close>
   11.35        by auto
   11.36      moreover
   11.37 -    { fix j assume "j < n"
   11.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"
   11.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 }
   11.40 -    ultimately show ?case
   11.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
   11.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>]
   11.43 +      by auto
   11.44 +    ultimately show "\<exists>r s. (\<forall>j<n. b j \<le> r j \<and> r j \<le> b j + 1) \<and>
   11.45 +        (\<forall>j<n. b j \<le> s j \<and> s j \<le> b j + 1) \<and> label r i \<noteq> label s i"
   11.46        by blast
   11.47    qed
   11.48  qed
   11.49 @@ -1392,23 +1396,20 @@
   11.50      apply rule
   11.51      apply rule
   11.52    proof -
   11.53 -    case goal1
   11.54 +    fix x x'
   11.55      let ?R = "\<lambda>y::nat.
   11.56 -      (P x \<and> Q xa \<and> x xa = 0 \<longrightarrow> y = 0) \<and>
   11.57 -      (P x \<and> Q xa \<and> x xa = 1 \<longrightarrow> y = 1) \<and>
   11.58 -      (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x xa \<le> (f x) xa) \<and>
   11.59 -      (P x \<and> Q xa \<and> y = 1 \<longrightarrow> (f x) xa \<le> x xa)"
   11.60 -    {
   11.61 -      assume "P x" and "Q xa"
   11.62 -      then have "0 \<le> f x xa \<and> f x xa \<le> 1"
   11.63 -        using assms(2)[rule_format,of "f x" xa]
   11.64 -        apply (drule_tac assms(1)[rule_format])
   11.65 -        apply auto
   11.66 -        done
   11.67 -    }
   11.68 +      (P x \<and> Q x' \<and> x x' = 0 \<longrightarrow> y = 0) \<and>
   11.69 +      (P x \<and> Q x' \<and> x x' = 1 \<longrightarrow> y = 1) \<and>
   11.70 +      (P x \<and> Q x' \<and> y = 0 \<longrightarrow> x x' \<le> (f x) x') \<and>
   11.71 +      (P x \<and> Q x' \<and> y = 1 \<longrightarrow> (f x) x' \<le> x x')"
   11.72 +    have "0 \<le> f x x' \<and> f x x' \<le> 1" if "P x" "Q x'"
   11.73 +      using assms(2)[rule_format,of "f x" x'] that
   11.74 +      apply (drule_tac assms(1)[rule_format])
   11.75 +      apply auto
   11.76 +      done
   11.77      then have "?R 0 \<or> ?R 1"
   11.78        by auto
   11.79 -    then show ?case
   11.80 +    then show "\<exists>y\<le>1. ?R y"
   11.81        by auto
   11.82    qed
   11.83  qed
   11.84 @@ -1988,17 +1989,17 @@
   11.85    assumes "e > 0"
   11.86    shows "\<not> (frontier (cball a e) retract_of (cball a e))"
   11.87  proof
   11.88 -  case goal1
   11.89 -  have *: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
   11.90 +  assume *: "frontier (cball a e) retract_of (cball a e)"
   11.91 +  have **: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
   11.92      using scaleR_left_distrib[of 1 1 a] by auto
   11.93    obtain x where x:
   11.94        "x \<in> {x. norm (a - x) = e}"
   11.95        "2 *\<^sub>R a - x = x"
   11.96 -    apply (rule retract_fixpoint_property[OF goal1, of "\<lambda>x. scaleR 2 a - x"])
   11.97 +    apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
   11.98      apply (blast intro: brouwer_ball[OF assms])
   11.99      apply (intro continuous_intros)
  11.100      unfolding frontier_cball subset_eq Ball_def image_iff dist_norm
  11.101 -    apply (auto simp add: * norm_minus_commute)
  11.102 +    apply (auto simp add: ** norm_minus_commute)
  11.103      done
  11.104    then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
  11.105      by (auto simp add: algebra_simps)
    12.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Thu Jun 25 15:01:43 2015 +0200
    12.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Thu Jun 25 23:51:54 2015 +0200
    12.3 @@ -62,20 +62,20 @@
    12.4    by (simp add: supp_def Collect_disj_eq del: disj_not1)
    12.5  
    12.6  instance pat :: pt_name
    12.7 -proof intro_classes
    12.8 -  case goal1
    12.9 +proof (default, goals)
   12.10 +  case (1 x)
   12.11    show ?case by (induct x) simp_all
   12.12  next
   12.13 -  case goal2
   12.14 +  case (2 _ _ x)
   12.15    show ?case by (induct x) (simp_all add: pt_name2)
   12.16  next
   12.17 -  case goal3
   12.18 +  case (3 _ _ x)
   12.19    then show ?case by (induct x) (simp_all add: pt_name3)
   12.20  qed
   12.21  
   12.22  instance pat :: fs_name
   12.23 -proof intro_classes
   12.24 -  case goal1
   12.25 +proof (default, goals)
   12.26 +  case (1 x)
   12.27    show ?case by (induct x) (simp_all add: fin_supp)
   12.28  qed
   12.29  
    13.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Jun 25 15:01:43 2015 +0200
    13.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Jun 25 23:51:54 2015 +0200
    13.3 @@ -2202,7 +2202,6 @@
    13.4    have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at)
    13.5    show ?thesis
    13.6    proof (rule equalityI)
    13.7 -    case goal1
    13.8      show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
    13.9        apply(auto simp add: perm_set_def)
   13.10        apply(rule_tac x="pi\<bullet>xb" in exI)
   13.11 @@ -2218,7 +2217,6 @@
   13.12        apply(rule pt_fun_app_eq[OF pt, OF at])
   13.13        done
   13.14    next
   13.15 -    case goal2
   13.16      show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
   13.17        apply(auto simp add: perm_set_def)
   13.18        apply(rule_tac x="(rev pi)\<bullet>x" in exI)
    14.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 15:01:43 2015 +0200
    14.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 23:51:54 2015 +0200
    14.3 @@ -1584,14 +1584,19 @@
    14.4  definition [simp]:
    14.5    "normalization_factor_int = (sgn :: int \<Rightarrow> int)"
    14.6  
    14.7 -instance proof
    14.8 -  case goal2 then show ?case by (auto simp add: abs_mult nat_mult_distrib)
    14.9 +instance
   14.10 +proof (default, goals)
   14.11 +  case 2
   14.12 +  then show ?case by (auto simp add: abs_mult nat_mult_distrib)
   14.13  next
   14.14 -  case goal3 then show ?case by (simp add: zsgn_def)
   14.15 +  case 3
   14.16 +  then show ?case by (simp add: zsgn_def)
   14.17  next
   14.18 -  case goal5 then show ?case by (auto simp: zsgn_def)
   14.19 +  case 5
   14.20 +  then show ?case by (auto simp: zsgn_def)
   14.21  next
   14.22 -  case goal6 then show ?case by (auto split: abs_split simp: zsgn_def)
   14.23 +  case 6
   14.24 +  then show ?case by (auto split: abs_split simp: zsgn_def)
   14.25  qed (auto simp: sgn_times split: abs_split)
   14.26  
   14.27  end
    15.1 --- a/src/HOL/Probability/Embed_Measure.thy	Thu Jun 25 15:01:43 2015 +0200
    15.2 +++ b/src/HOL/Probability/Embed_Measure.thy	Thu Jun 25 23:51:54 2015 +0200
    15.3 @@ -154,22 +154,22 @@
    15.4  lemma sigma_finite_embed_measure:
    15.5    assumes "sigma_finite_measure M" and inj: "inj f"
    15.6    shows "sigma_finite_measure (embed_measure M f)"
    15.7 -proof
    15.8 -  case goal1
    15.9 +proof -
   15.10    from assms(1) interpret sigma_finite_measure M .
   15.11    from sigma_finite_countable obtain A where
   15.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
   15.13 -  show ?case
   15.14 -  proof (intro exI[of _ "op ` f`A"] conjI allI)
   15.15 -    from A_props show "countable (op ` f`A)" by auto
   15.16 -    from inj and A_props show "op ` f`A \<subseteq> sets (embed_measure M f)" 
   15.17 -      by (auto simp: sets_embed_measure)
   15.18 -    from A_props and inj show "\<Union>(op ` f`A) = space (embed_measure M f)"
   15.19 -      by (auto simp: space_embed_measure intro!: imageI)
   15.20 -    from A_props and inj show "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
   15.21 -      by (intro ballI, subst emeasure_embed_measure)
   15.22 -         (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
   15.23 -  qed
   15.24 +  from A_props have "countable (op ` f`A)" by auto
   15.25 +  moreover
   15.26 +  from inj and A_props have "op ` f`A \<subseteq> sets (embed_measure M f)" 
   15.27 +    by (auto simp: sets_embed_measure)
   15.28 +  moreover
   15.29 +  from A_props and inj have "\<Union>(op ` f`A) = space (embed_measure M f)"
   15.30 +    by (auto simp: space_embed_measure intro!: imageI)
   15.31 +  moreover
   15.32 +  from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
   15.33 +    by (intro ballI, subst emeasure_embed_measure)
   15.34 +       (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
   15.35 +  ultimately show ?thesis by - (default, blast)
   15.36  qed
   15.37  
   15.38  lemma embed_measure_count_space':
    16.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Thu Jun 25 15:01:43 2015 +0200
    16.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Thu Jun 25 23:51:54 2015 +0200
    16.3 @@ -192,20 +192,22 @@
    16.4  lemma PiM_cong:
    16.5    assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
    16.6    shows "PiM I M = PiM J N"
    16.7 -unfolding PiM_def
    16.8 -proof (rule extend_measure_cong)
    16.9 -  case goal1 show ?case using assms
   16.10 +  unfolding PiM_def
   16.11 +proof (rule extend_measure_cong, goals)
   16.12 +  case 1
   16.13 +  show ?case using assms
   16.14      by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
   16.15  next
   16.16 -  case goal2
   16.17 +  case 2
   16.18    have "\<And>K. K \<subseteq> J \<Longrightarrow> (\<Pi> j\<in>K. sets (M j)) = (\<Pi> j\<in>K. sets (N j))"
   16.19      using assms by (intro Pi_cong_sets) auto
   16.20    thus ?case by (auto simp: assms)
   16.21  next
   16.22 -  case goal3 show ?case using assms 
   16.23 +  case 3
   16.24 +  show ?case using assms 
   16.25      by (intro ext) (auto simp: prod_emb_def dest: PiE_mem)
   16.26  next
   16.27 -  case (goal4 x)
   16.28 +  case (4 x)
   16.29    thus ?case using assms 
   16.30      by (auto intro!: setprod.cong split: split_if_asm)
   16.31  qed
    17.1 --- a/src/HOL/Probability/Information.thy	Thu Jun 25 15:01:43 2015 +0200
    17.2 +++ b/src/HOL/Probability/Information.thy	Thu Jun 25 23:51:54 2015 +0200
    17.3 @@ -1022,11 +1022,12 @@
    17.4      Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
    17.5      Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
    17.6    proof eventually_elim
    17.7 -    case (goal1 x)
    17.8 +    case (elim x)
    17.9      show ?case
   17.10      proof cases
   17.11        assume "Pxyz x \<noteq> 0"
   17.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"
   17.13 +      with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
   17.14 +        "0 < Pyz (snd x)" "0 < Pxyz x"
   17.15          by auto
   17.16        then show ?thesis
   17.17          using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
   17.18 @@ -1252,11 +1253,12 @@
   17.19      Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
   17.20      Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
   17.21    proof eventually_elim
   17.22 -    case (goal1 x)
   17.23 +    case (elim x)
   17.24      show ?case
   17.25      proof cases
   17.26        assume "Pxyz x \<noteq> 0"
   17.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"
   17.28 +      with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
   17.29 +        "0 < Pyz (snd x)" "0 < Pxyz x"
   17.30          by auto
   17.31        then show ?thesis
   17.32          using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
   17.33 @@ -1730,11 +1732,11 @@
   17.34      Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
   17.35      (is "AE x in _. ?f x = ?g x")
   17.36    proof eventually_elim
   17.37 -    case (goal1 x)
   17.38 +    case (elim x)
   17.39      show ?case
   17.40      proof cases
   17.41        assume "Pxy x \<noteq> 0"
   17.42 -      with goal1 have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
   17.43 +      with elim have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
   17.44          by auto
   17.45        then show ?thesis
   17.46          using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
    18.1 --- a/src/HOL/Probability/Measure_Space.thy	Thu Jun 25 15:01:43 2015 +0200
    18.2 +++ b/src/HOL/Probability/Measure_Space.thy	Thu Jun 25 23:51:54 2015 +0200
    18.3 @@ -1134,44 +1134,56 @@
    18.4  lemma (in sigma_finite_measure) sigma_finite_disjoint:
    18.5    obtains A :: "nat \<Rightarrow> 'a set"
    18.6    where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "disjoint_family A"
    18.7 -proof atomize_elim
    18.8 -  case goal1
    18.9 +proof -
   18.10    obtain A :: "nat \<Rightarrow> 'a set" where
   18.11      range: "range A \<subseteq> sets M" and
   18.12      space: "(\<Union>i. A i) = space M" and
   18.13      measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
   18.14      using sigma_finite by auto
   18.15 -  note range' = sets.range_disjointed_sets[OF range] range
   18.16 -  { fix i
   18.17 -    have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
   18.18 -      using range' disjointed_subset[of A i] by (auto intro!: emeasure_mono)
   18.19 -    then have "emeasure M (disjointed A i) \<noteq> \<infinity>"
   18.20 -      using measure[of i] by auto }
   18.21 -  with disjoint_family_disjointed UN_disjointed_eq[of A] space range'
   18.22 -  show ?case by (auto intro!: exI[of _ "disjointed A"])
   18.23 +  show thesis
   18.24 +  proof (rule that[of "disjointed A"])
   18.25 +    show "range (disjointed A) \<subseteq> sets M"
   18.26 +      by (rule sets.range_disjointed_sets[OF range])
   18.27 +    show "(\<Union>i. disjointed A i) = space M"
   18.28 +      and "disjoint_family (disjointed A)"
   18.29 +      using disjoint_family_disjointed UN_disjointed_eq[of A] space range
   18.30 +      by auto
   18.31 +    show "emeasure M (disjointed A i) \<noteq> \<infinity>" for i
   18.32 +    proof -
   18.33 +      have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
   18.34 +        using range disjointed_subset[of A i] by (auto intro!: emeasure_mono)
   18.35 +      then show ?thesis using measure[of i] by auto
   18.36 +    qed
   18.37 +  qed
   18.38  qed
   18.39  
   18.40  lemma (in sigma_finite_measure) sigma_finite_incseq:
   18.41    obtains A :: "nat \<Rightarrow> 'a set"
   18.42    where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "incseq A"
   18.43 -proof atomize_elim
   18.44 -  case goal1
   18.45 +proof -
   18.46    obtain F :: "nat \<Rightarrow> 'a set" where
   18.47      F: "range F \<subseteq> sets M" "(\<Union>i. F i) = space M" "\<And>i. emeasure M (F i) \<noteq> \<infinity>"
   18.48      using sigma_finite by auto
   18.49 -  then show ?case
   18.50 -  proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI)
   18.51 -    from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
   18.52 -    then show "(\<Union>n. \<Union> i\<le>n. F i) = space M"
   18.53 -      using F by fastforce
   18.54 -  next
   18.55 -    fix n
   18.56 -    have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))" using F
   18.57 -      by (auto intro!: emeasure_subadditive_finite)
   18.58 -    also have "\<dots> < \<infinity>"
   18.59 -      using F by (auto simp: setsum_Pinfty)
   18.60 -    finally show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" by simp
   18.61 -  qed (force simp: incseq_def)+
   18.62 +  show thesis
   18.63 +  proof (rule that[of "\<lambda>n. \<Union>i\<le>n. F i"])
   18.64 +    show "range (\<lambda>n. \<Union>i\<le>n. F i) \<subseteq> sets M"
   18.65 +      using F by (force simp: incseq_def)
   18.66 +    show "(\<Union>n. \<Union>i\<le>n. F i) = space M"
   18.67 +    proof -
   18.68 +      from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
   18.69 +      with F show ?thesis by fastforce
   18.70 +    qed
   18.71 +    show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" for n
   18.72 +    proof -
   18.73 +      have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))"
   18.74 +        using F by (auto intro!: emeasure_subadditive_finite)
   18.75 +      also have "\<dots> < \<infinity>"
   18.76 +        using F by (auto simp: setsum_Pinfty)
   18.77 +      finally show ?thesis by simp
   18.78 +    qed
   18.79 +    show "incseq (\<lambda>n. \<Union>i\<le>n. F i)"
   18.80 +      by (force simp: incseq_def)
   18.81 +  qed
   18.82  qed
   18.83  
   18.84  subsection {* Measure space induced by distribution of @{const measurable}-functions *}
    19.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 25 15:01:43 2015 +0200
    19.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 25 23:51:54 2015 +0200
    19.3 @@ -1649,7 +1649,7 @@
    19.4      val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
    19.5      val lthy'' = lthy'
    19.6        |> fold Variable.auto_fixes cases_rules
    19.7 -      |> Proof_Context.update_cases true case_env
    19.8 +      |> Proof_Context.update_cases case_env
    19.9      fun after_qed thms goal_ctxt =
   19.10        let
   19.11          val global_thms = Proof_Context.export goal_ctxt
    20.1 --- a/src/HOL/ZF/Games.thy	Thu Jun 25 15:01:43 2015 +0200
    20.2 +++ b/src/HOL/ZF/Games.thy	Thu Jun 25 23:51:54 2015 +0200
    20.3 @@ -418,22 +418,22 @@
    20.4  proof (induct x rule: wf_induct[OF wf_option_of]) 
    20.5    case (1 "g")  
    20.6    show ?case
    20.7 -  proof (auto)
    20.8 -    {case (goal1 y) 
    20.9 -      from goal1 have "(y, g) \<in> option_of" by (auto)
   20.10 +  proof (auto, goals)
   20.11 +    {case prems: (1 y) 
   20.12 +      from prems have "(y, g) \<in> option_of" by (auto)
   20.13        with 1 have "ge_game (y, y)" by auto
   20.14 -      with goal1 have "\<not> ge_game (g, y)" 
   20.15 +      with prems have "\<not> ge_game (g, y)" 
   20.16          by (subst ge_game_eq, auto)
   20.17 -      with goal1 show ?case by auto}
   20.18 +      with prems show ?case by auto}
   20.19      note right = this
   20.20 -    {case (goal2 y)
   20.21 -      from goal2 have "(y, g) \<in> option_of" by (auto)
   20.22 +    {case prems: (2 y)
   20.23 +      from prems have "(y, g) \<in> option_of" by (auto)
   20.24        with 1 have "ge_game (y, y)" by auto
   20.25 -      with goal2 have "\<not> ge_game (y, g)" 
   20.26 +      with prems have "\<not> ge_game (y, g)" 
   20.27          by (subst ge_game_eq, auto)
   20.28 -      with goal2 show ?case by auto}
   20.29 +      with prems show ?case by auto}
   20.30      note left = this
   20.31 -    {case goal3
   20.32 +    {case 3
   20.33        from left right show ?case
   20.34          by (subst ge_game_eq, auto)
   20.35      }
   20.36 @@ -462,8 +462,8 @@
   20.37      proof (induct a rule: induct_game)
   20.38        case (1 a)
   20.39        show ?case
   20.40 -      proof (rule allI | rule impI)+
   20.41 -        case (goal1 x y z)
   20.42 +      proof ((rule allI | rule impI)+, goals)
   20.43 +        case prems: (1 x y z)
   20.44          show ?case
   20.45          proof -
   20.46            { fix xr
   20.47 @@ -471,10 +471,10 @@
   20.48              assume a: "ge_game (z, xr)"
   20.49              have "ge_game (y, xr)"
   20.50                apply (rule 1[rule_format, where y="[y,z,xr]"])
   20.51 -              apply (auto intro: xr lprod_3_1 simp add: goal1 a)
   20.52 +              apply (auto intro: xr lprod_3_1 simp add: prems a)
   20.53                done
   20.54              moreover from xr have "\<not> ge_game (y, xr)"
   20.55 -              by (simp add: goal1(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
   20.56 +              by (simp add: prems(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
   20.57              ultimately have "False" by auto      
   20.58            }
   20.59            note xr = this
   20.60 @@ -483,10 +483,10 @@
   20.61              assume a: "ge_game (zl, x)"
   20.62              have "ge_game (zl, y)"
   20.63                apply (rule 1[rule_format, where y="[zl,x,y]"])
   20.64 -              apply (auto intro: zl lprod_3_2 simp add: goal1 a)
   20.65 +              apply (auto intro: zl lprod_3_2 simp add: prems a)
   20.66                done
   20.67              moreover from zl have "\<not> ge_game (zl, y)"
   20.68 -              by (simp add: goal1(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
   20.69 +              by (simp add: prems(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
   20.70              ultimately have "False" by auto
   20.71            }
   20.72            note zl = this
   20.73 @@ -542,21 +542,18 @@
   20.74  
   20.75  lemma plus_game_zero_right[simp]: "plus_game G zero_game = G"
   20.76  proof -
   20.77 -  { 
   20.78 -    fix G H
   20.79 -    have "H = zero_game \<longrightarrow> plus_game G H = G "
   20.80 -    proof (induct G H rule: plus_game.induct, rule impI)
   20.81 -      case (goal1 G H)
   20.82 -      note induct_hyp = this[simplified goal1, simplified] and this
   20.83 -      show ?case
   20.84 -        apply (simp only: plus_game.simps[where G=G and H=H])
   20.85 -        apply (simp add: game_ext_eq goal1)
   20.86 -        apply (auto simp add: 
   20.87 -          zimage_cong [where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
   20.88 -          induct_hyp)
   20.89 -        done
   20.90 -    qed
   20.91 -  }
   20.92 +  have "H = zero_game \<longrightarrow> plus_game G H = G " for G H
   20.93 +  proof (induct G H rule: plus_game.induct, rule impI, goals)
   20.94 +    case prems: (1 G H)
   20.95 +    note induct_hyp = this[simplified prems, simplified] and this
   20.96 +    show ?case
   20.97 +      apply (simp only: plus_game.simps[where G=G and H=H])
   20.98 +      apply (simp add: game_ext_eq prems)
   20.99 +      apply (auto simp add: 
  20.100 +        zimage_cong [where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
  20.101 +        induct_hyp)
  20.102 +      done
  20.103 +  qed
  20.104    then show ?thesis by auto
  20.105  qed
  20.106  
  20.107 @@ -585,36 +582,33 @@
  20.108    
  20.109  lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)"
  20.110  proof -
  20.111 -  { 
  20.112 -    fix a
  20.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)"
  20.114 -    proof (induct a rule: induct_game, (rule impI | rule allI)+)
  20.115 -      case (goal1 x F G H)
  20.116 -      let ?L = "plus_game (plus_game F G) H"
  20.117 -      let ?R = "plus_game F (plus_game G H)"
  20.118 -      note options_plus = left_options_plus right_options_plus
  20.119 -      {
  20.120 -        fix opt
  20.121 -        note hyp = goal1(1)[simplified goal1(2), rule_format] 
  20.122 -        have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
  20.123 -          by (blast intro: hyp lprod_3_3)
  20.124 -        have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
  20.125 -          by (blast intro: hyp lprod_3_4)
  20.126 -        have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game F G) opt = plus_game F (plus_game G opt)" 
  20.127 -          by (blast intro: hyp lprod_3_5)
  20.128 -        note F and G and H
  20.129 -      }
  20.130 -      note induct_hyp = this
  20.131 -      have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
  20.132 -        by (auto simp add: 
  20.133 -          plus_game.simps[where G="plus_game F G" and H=H]
  20.134 -          plus_game.simps[where G="F" and H="plus_game G H"] 
  20.135 -          zet_ext_eq zunion zimage_iff options_plus
  20.136 -          induct_hyp left_imp_options right_imp_options)
  20.137 -      then show ?case
  20.138 -        by (simp add: game_ext_eq)
  20.139 -    qed
  20.140 -  }
  20.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
  20.142 +  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
  20.143 +    case prems: (1 x F G H)
  20.144 +    let ?L = "plus_game (plus_game F G) H"
  20.145 +    let ?R = "plus_game F (plus_game G H)"
  20.146 +    note options_plus = left_options_plus right_options_plus
  20.147 +    {
  20.148 +      fix opt
  20.149 +      note hyp = prems(1)[simplified prems(2), rule_format] 
  20.150 +      have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
  20.151 +        by (blast intro: hyp lprod_3_3)
  20.152 +      have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
  20.153 +        by (blast intro: hyp lprod_3_4)
  20.154 +      have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game F G) opt = plus_game F (plus_game G opt)" 
  20.155 +        by (blast intro: hyp lprod_3_5)
  20.156 +      note F and G and H
  20.157 +    }
  20.158 +    note induct_hyp = this
  20.159 +    have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
  20.160 +      by (auto simp add: 
  20.161 +        plus_game.simps[where G="plus_game F G" and H=H]
  20.162 +        plus_game.simps[where G="F" and H="plus_game G H"] 
  20.163 +        zet_ext_eq zunion zimage_iff options_plus
  20.164 +        induct_hyp left_imp_options right_imp_options)
  20.165 +    then show ?case
  20.166 +      by (simp add: game_ext_eq)
  20.167 +  qed
  20.168    then show ?thesis by auto
  20.169  qed
  20.170  
  20.171 @@ -632,58 +626,38 @@
  20.172  qed
  20.173  
  20.174  lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
  20.175 -proof (induct x rule: wf_induct[OF wf_option_of])
  20.176 -  case (goal1 x)
  20.177 -  { fix y
  20.178 -    assume "zin y (options x)"
  20.179 -    then have "eq_game (plus_game y (neg_game y)) zero_game"
  20.180 -      by (auto simp add: goal1)
  20.181 -  }
  20.182 -  note ihyp = this
  20.183 -  {
  20.184 -    fix y
  20.185 -    assume y: "zin y (right_options x)"
  20.186 -    have "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
  20.187 -      apply (subst ge_game.simps, simp)
  20.188 -      apply (rule exI[where x="plus_game y (neg_game y)"])
  20.189 -      apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
  20.190 -      apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: y)
  20.191 -      done
  20.192 -  }
  20.193 -  note case1 = this
  20.194 -  {
  20.195 -    fix y
  20.196 -    assume y: "zin y (left_options x)"
  20.197 -    have "\<not> (ge_game (zero_game, plus_game x (neg_game y)))"
  20.198 -      apply (subst ge_game.simps, simp)
  20.199 -      apply (rule exI[where x="plus_game y (neg_game y)"])
  20.200 -      apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
  20.201 -      apply (auto simp add: left_options_plus zunion zimage_iff intro: y)
  20.202 -      done
  20.203 -  }
  20.204 -  note case2 = this
  20.205 -  {
  20.206 -    fix y
  20.207 -    assume y: "zin y (left_options x)"
  20.208 -    have "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
  20.209 -      apply (subst ge_game.simps, simp)
  20.210 -      apply (rule exI[where x="plus_game y (neg_game y)"])
  20.211 -      apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
  20.212 -      apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: y)
  20.213 -      done
  20.214 -  }
  20.215 -  note case3 = this
  20.216 -  {
  20.217 -    fix y
  20.218 -    assume y: "zin y (right_options x)"
  20.219 -    have "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
  20.220 -      apply (subst ge_game.simps, simp)
  20.221 -      apply (rule exI[where x="plus_game y (neg_game y)"])
  20.222 -      apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
  20.223 -      apply (auto simp add: right_options_plus zunion zimage_iff intro: y)
  20.224 -      done
  20.225 -  }
  20.226 -  note case4 = this
  20.227 +proof (induct x rule: wf_induct[OF wf_option_of], goals)
  20.228 +  case prems: (1 x)
  20.229 +  then have ihyp: "eq_game (plus_game y (neg_game y)) zero_game" if "zin y (options x)" for y
  20.230 +    using that by (auto simp add: prems)
  20.231 +  have case1: "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
  20.232 +    if y: "zin y (right_options x)" for y
  20.233 +    apply (subst ge_game.simps, simp)
  20.234 +    apply (rule exI[where x="plus_game y (neg_game y)"])
  20.235 +    apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
  20.236 +    apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: y)
  20.237 +    done
  20.238 +  have case2: "\<not> (ge_game (zero_game, plus_game x (neg_game y)))"
  20.239 +    if y: "zin y (left_options x)" for y
  20.240 +    apply (subst ge_game.simps, simp)
  20.241 +    apply (rule exI[where x="plus_game y (neg_game y)"])
  20.242 +    apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
  20.243 +    apply (auto simp add: left_options_plus zunion zimage_iff intro: y)
  20.244 +    done
  20.245 +  have case3: "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
  20.246 +    if y: "zin y (left_options x)" for y
  20.247 +    apply (subst ge_game.simps, simp)
  20.248 +    apply (rule exI[where x="plus_game y (neg_game y)"])
  20.249 +    apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
  20.250 +    apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: y)
  20.251 +    done
  20.252 +  have case4: "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
  20.253 +    if y: "zin y (right_options x)" for y
  20.254 +    apply (subst ge_game.simps, simp)
  20.255 +    apply (rule exI[where x="plus_game y (neg_game y)"])
  20.256 +    apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
  20.257 +    apply (auto simp add: right_options_plus zunion zimage_iff intro: y)
  20.258 +    done
  20.259    show ?case
  20.260      apply (simp add: eq_game_def)
  20.261      apply (simp add: ge_game.simps[of "plus_game x (neg_game x)" "zero_game"])
  20.262 @@ -695,112 +669,109 @@
  20.263  
  20.264  lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
  20.265  proof -
  20.266 -  { fix a
  20.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)"
  20.268 -    proof (induct a rule: induct_game, (rule impI | rule allI)+)
  20.269 -      case (goal1 a x y z)
  20.270 -      note induct_hyp = goal1(1)[rule_format, simplified goal1(2)]
  20.271 -      { 
  20.272 -        assume hyp: "ge_game(plus_game x y, plus_game x z)"
  20.273 -        have "ge_game (y, z)"
  20.274 -        proof -
  20.275 -          { fix yr
  20.276 -            assume yr: "zin yr (right_options y)"
  20.277 -            from hyp have "\<not> (ge_game (plus_game x z, plus_game x yr))"
  20.278 -              by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
  20.279 -                right_options_plus zunion zimage_iff intro: yr)
  20.280 -            then have "\<not> (ge_game (z, yr))"
  20.281 -              apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
  20.282 -              apply (simp_all add: yr lprod_3_6)
  20.283 -              done
  20.284 -          }
  20.285 -          note yr = this
  20.286 -          { fix zl
  20.287 -            assume zl: "zin zl (left_options z)"
  20.288 -            from hyp have "\<not> (ge_game (plus_game x zl, plus_game x y))"
  20.289 -              by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
  20.290 -                left_options_plus zunion zimage_iff intro: zl)
  20.291 -            then have "\<not> (ge_game (zl, y))"
  20.292 -              apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
  20.293 -              apply (simp_all add: goal1(2) zl lprod_3_7)
  20.294 -              done
  20.295 -          }     
  20.296 -          note zl = this
  20.297 -          show "ge_game (y, z)"
  20.298 -            apply (subst ge_game_eq)
  20.299 -            apply (auto simp add: yr zl)
  20.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
  20.301 +  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
  20.302 +    case prems: (1 a x y z)
  20.303 +    note induct_hyp = prems(1)[rule_format, simplified prems(2)]
  20.304 +    { 
  20.305 +      assume hyp: "ge_game(plus_game x y, plus_game x z)"
  20.306 +      have "ge_game (y, z)"
  20.307 +      proof -
  20.308 +        { fix yr
  20.309 +          assume yr: "zin yr (right_options y)"
  20.310 +          from hyp have "\<not> (ge_game (plus_game x z, plus_game x yr))"
  20.311 +            by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
  20.312 +              right_options_plus zunion zimage_iff intro: yr)
  20.313 +          then have "\<not> (ge_game (z, yr))"
  20.314 +            apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
  20.315 +            apply (simp_all add: yr lprod_3_6)
  20.316              done
  20.317 -        qed      
  20.318 -      }
  20.319 -      note right_imp_left = this
  20.320 -      {
  20.321 -        assume yz: "ge_game (y, z)"
  20.322 -        {
  20.323 -          fix x'
  20.324 -          assume x': "zin x' (right_options x)"
  20.325 -          assume hyp: "ge_game (plus_game x z, plus_game x' y)"
  20.326 -          then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
  20.327 -            by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"] 
  20.328 -              right_options_plus zunion zimage_iff intro: x')
  20.329 -          have t: "ge_game (plus_game x' y, plus_game x' z)"
  20.330 -            apply (subst induct_hyp[symmetric])
  20.331 -            apply (auto intro: lprod_3_3 x' yz)
  20.332 +        }
  20.333 +        note yr = this
  20.334 +        { fix zl
  20.335 +          assume zl: "zin zl (left_options z)"
  20.336 +          from hyp have "\<not> (ge_game (plus_game x zl, plus_game x y))"
  20.337 +            by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
  20.338 +              left_options_plus zunion zimage_iff intro: zl)
  20.339 +          then have "\<not> (ge_game (zl, y))"
  20.340 +            apply (subst prems(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
  20.341 +            apply (simp_all add: prems(2) zl lprod_3_7)
  20.342              done
  20.343 -          from n t have "False" by blast
  20.344 -        }    
  20.345 -        note case1 = this
  20.346 -        {
  20.347 -          fix x'
  20.348 -          assume x': "zin x' (left_options x)"
  20.349 -          assume hyp: "ge_game (plus_game x' z, plus_game x y)"
  20.350 -          then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
  20.351 -            by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"] 
  20.352 -              left_options_plus zunion zimage_iff intro: x')
  20.353 -          have t: "ge_game (plus_game x' y, plus_game x' z)"
  20.354 -            apply (subst induct_hyp[symmetric])
  20.355 -            apply (auto intro: lprod_3_3 x' yz)
  20.356 -            done
  20.357 -          from n t have "False" by blast
  20.358 -        }
  20.359 -        note case3 = this
  20.360 -        {
  20.361 -          fix y'
  20.362 -          assume y': "zin y' (right_options y)"
  20.363 -          assume hyp: "ge_game (plus_game x z, plus_game x y')"
  20.364 -          then have "ge_game(z, y')"
  20.365 -            apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
  20.366 -            apply (auto simp add: hyp lprod_3_6 y')
  20.367 -            done
  20.368 -          with yz have "ge_game (y, y')"
  20.369 -            by (blast intro: ge_game_trans)      
  20.370 -          with y' have "False" by (auto simp add: ge_game_leftright_refl)
  20.371 -        }
  20.372 -        note case2 = this
  20.373 -        {
  20.374 -          fix z'
  20.375 -          assume z': "zin z' (left_options z)"
  20.376 -          assume hyp: "ge_game (plus_game x z', plus_game x y)"
  20.377 -          then have "ge_game(z', y)"
  20.378 -            apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
  20.379 -            apply (auto simp add: hyp lprod_3_7 z')
  20.380 -            done    
  20.381 -          with yz have "ge_game (z', z)"
  20.382 -            by (blast intro: ge_game_trans)      
  20.383 -          with z' have "False" by (auto simp add: ge_game_leftright_refl)
  20.384 -        }
  20.385 -        note case4 = this   
  20.386 -        have "ge_game(plus_game x y, plus_game x z)"
  20.387 +        }     
  20.388 +        note zl = this
  20.389 +        show "ge_game (y, z)"
  20.390            apply (subst ge_game_eq)
  20.391 -          apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
  20.392 -          apply (auto intro: case1 case2 case3 case4)
  20.393 +          apply (auto simp add: yr zl)
  20.394            done
  20.395 +      qed      
  20.396 +    }
  20.397 +    note right_imp_left = this
  20.398 +    {
  20.399 +      assume yz: "ge_game (y, z)"
  20.400 +      {
  20.401 +        fix x'
  20.402 +        assume x': "zin x' (right_options x)"
  20.403 +        assume hyp: "ge_game (plus_game x z, plus_game x' y)"
  20.404 +        then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
  20.405 +          by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"] 
  20.406 +            right_options_plus zunion zimage_iff intro: x')
  20.407 +        have t: "ge_game (plus_game x' y, plus_game x' z)"
  20.408 +          apply (subst induct_hyp[symmetric])
  20.409 +          apply (auto intro: lprod_3_3 x' yz)
  20.410 +          done
  20.411 +        from n t have "False" by blast
  20.412 +      }    
  20.413 +      note case1 = this
  20.414 +      {
  20.415 +        fix x'
  20.416 +        assume x': "zin x' (left_options x)"
  20.417 +        assume hyp: "ge_game (plus_game x' z, plus_game x y)"
  20.418 +        then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
  20.419 +          by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"] 
  20.420 +            left_options_plus zunion zimage_iff intro: x')
  20.421 +        have t: "ge_game (plus_game x' y, plus_game x' z)"
  20.422 +          apply (subst induct_hyp[symmetric])
  20.423 +          apply (auto intro: lprod_3_3 x' yz)
  20.424 +          done
  20.425 +        from n t have "False" by blast
  20.426        }
  20.427 -      note left_imp_right = this
  20.428 -      show ?case by (auto intro: right_imp_left left_imp_right)
  20.429 -    qed
  20.430 -  }
  20.431 -  note a = this[of "[x, y, z]"]
  20.432 -  then show ?thesis by blast
  20.433 +      note case3 = this
  20.434 +      {
  20.435 +        fix y'
  20.436 +        assume y': "zin y' (right_options y)"
  20.437 +        assume hyp: "ge_game (plus_game x z, plus_game x y')"
  20.438 +        then have "ge_game(z, y')"
  20.439 +          apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
  20.440 +          apply (auto simp add: hyp lprod_3_6 y')
  20.441 +          done
  20.442 +        with yz have "ge_game (y, y')"
  20.443 +          by (blast intro: ge_game_trans)      
  20.444 +        with y' have "False" by (auto simp add: ge_game_leftright_refl)
  20.445 +      }
  20.446 +      note case2 = this
  20.447 +      {
  20.448 +        fix z'
  20.449 +        assume z': "zin z' (left_options z)"
  20.450 +        assume hyp: "ge_game (plus_game x z', plus_game x y)"
  20.451 +        then have "ge_game(z', y)"
  20.452 +          apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
  20.453 +          apply (auto simp add: hyp lprod_3_7 z')
  20.454 +          done    
  20.455 +        with yz have "ge_game (z', z)"
  20.456 +          by (blast intro: ge_game_trans)      
  20.457 +        with z' have "False" by (auto simp add: ge_game_leftright_refl)
  20.458 +      }
  20.459 +      note case4 = this   
  20.460 +      have "ge_game(plus_game x y, plus_game x z)"
  20.461 +        apply (subst ge_game_eq)
  20.462 +        apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
  20.463 +        apply (auto intro: case1 case2 case3 case4)
  20.464 +        done
  20.465 +    }
  20.466 +    note left_imp_right = this
  20.467 +    show ?case by (auto intro: right_imp_left left_imp_right)
  20.468 +  qed
  20.469 +  from this[of "[x, y, z]"] show ?thesis by blast
  20.470  qed
  20.471  
  20.472  lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game y x, plus_game z x)"
  20.473 @@ -808,34 +779,31 @@
  20.474  
  20.475  lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
  20.476  proof -
  20.477 -  { fix a
  20.478 -    have "\<forall> x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)"
  20.479 -    proof (induct a rule: induct_game, (rule impI | rule allI)+)
  20.480 -      case (goal1 a x y)
  20.481 -      note ihyp = goal1(1)[rule_format, simplified goal1(2)]
  20.482 -      { fix xl
  20.483 -        assume xl: "zin xl (left_options x)"
  20.484 -        have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)"
  20.485 -          apply (subst ihyp)
  20.486 -          apply (auto simp add: lprod_2_1 xl)
  20.487 -          done
  20.488 -      }
  20.489 -      note xl = this
  20.490 -      { fix yr
  20.491 -        assume yr: "zin yr (right_options y)"
  20.492 -        have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)"
  20.493 -          apply (subst ihyp)
  20.494 -          apply (auto simp add: lprod_2_2 yr)
  20.495 -          done
  20.496 -      }
  20.497 -      note yr = this
  20.498 -      show ?case
  20.499 -        by (auto simp add: ge_game_eq[of "neg_game x" "neg_game y"] ge_game_eq[of "y" "x"]
  20.500 -          right_options_neg left_options_neg zimage_iff  xl yr)
  20.501 -    qed
  20.502 -  }
  20.503 -  note a = this[of "[x,y]"]
  20.504 -  then show ?thesis by blast
  20.505 +  have "\<forall>x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)" for a
  20.506 +  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
  20.507 +    case prems: (1 a x y)
  20.508 +    note ihyp = prems(1)[rule_format, simplified prems(2)]
  20.509 +    { fix xl
  20.510 +      assume xl: "zin xl (left_options x)"
  20.511 +      have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)"
  20.512 +        apply (subst ihyp)
  20.513 +        apply (auto simp add: lprod_2_1 xl)
  20.514 +        done
  20.515 +    }
  20.516 +    note xl = this
  20.517 +    { fix yr
  20.518 +      assume yr: "zin yr (right_options y)"
  20.519 +      have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)"
  20.520 +        apply (subst ihyp)
  20.521 +        apply (auto simp add: lprod_2_2 yr)
  20.522 +        done
  20.523 +    }
  20.524 +    note yr = this
  20.525 +    show ?case
  20.526 +      by (auto simp add: ge_game_eq[of "neg_game x" "neg_game y"] ge_game_eq[of "y" "x"]
  20.527 +        right_options_neg left_options_neg zimage_iff  xl yr)
  20.528 +  qed
  20.529 +  from this[of "[x,y]"] show ?thesis by blast
  20.530  qed
  20.531  
  20.532  definition eq_game_rel :: "(game * game) set" where
  20.533 @@ -974,4 +942,3 @@
  20.534  qed
  20.535  
  20.536  end
  20.537 -
    21.1 --- a/src/HOL/ex/Tree23.thy	Thu Jun 25 15:01:43 2015 +0200
    21.2 +++ b/src/HOL/ex/Tree23.thy	Thu Jun 25 23:51:54 2015 +0200
    21.3 @@ -377,16 +377,26 @@
    21.4       done
    21.5    } note B = this
    21.6    show "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
    21.7 -  proof (induct k t arbitrary: n rule: del.induct)
    21.8 -    { case goal1 thus "dfull n (del (Some k) Empty)" by simp }
    21.9 -    { case goal2 thus "dfull n (del None (Branch2 Empty p Empty))" by simp }
   21.10 -    { case goal3 thus "dfull n (del None (Branch3 Empty p Empty q Empty))"
   21.11 -        by simp }
   21.12 -    { case goal4 thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
   21.13 -        by (simp split: ord.split) }
   21.14 -    { case goal5 thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
   21.15 -        by (simp split: ord.split) }
   21.16 -    { case goal26 thus ?case by simp }
   21.17 +  proof (induct k t arbitrary: n rule: del.induct, goals)
   21.18 +    case (1 k n)
   21.19 +    thus "dfull n (del (Some k) Empty)" by simp
   21.20 +  next
   21.21 +    case (2 p n)
   21.22 +    thus "dfull n (del None (Branch2 Empty p Empty))" by simp
   21.23 +  next
   21.24 +    case (3 p q n)
   21.25 +    thus "dfull n (del None (Branch3 Empty p Empty q Empty))" by simp
   21.26 +  next
   21.27 +    case (4 v p n)
   21.28 +    thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
   21.29 +      by (simp split: ord.split)
   21.30 +  next
   21.31 +    case (5 v p q n)
   21.32 +    thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
   21.33 +      by (simp split: ord.split)
   21.34 +  next
   21.35 +    case (26 n)
   21.36 +    thus ?case by simp
   21.37    qed (fact A | fact B)+
   21.38  qed
   21.39  
    22.1 --- a/src/Pure/Isar/args.ML	Thu Jun 25 15:01:43 2015 +0200
    22.2 +++ b/src/Pure/Isar/args.ML	Thu Jun 25 23:51:54 2015 +0200
    22.3 @@ -21,14 +21,15 @@
    22.4    val bracks: 'a parser -> 'a parser
    22.5    val mode: string -> bool parser
    22.6    val maybe: 'a parser -> 'a option parser
    22.7 +  val name_token: Token.T parser
    22.8 +  val name_inner_syntax: string parser
    22.9 +  val name_input: Input.source parser
   22.10 +  val name: string parser
   22.11    val cartouche_inner_syntax: string parser
   22.12    val cartouche_input: Input.source parser
   22.13    val text_token: Token.T parser
   22.14    val text_input: Input.source parser
   22.15    val text: string parser
   22.16 -  val name_inner_syntax: string parser
   22.17 -  val name_input: Input.source parser
   22.18 -  val name: string parser
   22.19    val binding: binding parser
   22.20    val alt_name: string parser
   22.21    val symbol: string parser
   22.22 @@ -92,8 +93,6 @@
   22.23        else Scan.fail
   22.24      end);
   22.25  
   22.26 -val named = ident || string;
   22.27 -
   22.28  val add = $$$ "add";
   22.29  val del = $$$ "del";
   22.30  val colon = $$$ ":";
   22.31 @@ -107,18 +106,19 @@
   22.32  fun mode s = Scan.optional (parens ($$$ s) >> K true) false;
   22.33  fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
   22.34  
   22.35 +val name_token = ident || string;
   22.36 +val name_inner_syntax = name_token >> Token.inner_syntax_of;
   22.37 +val name_input = name_token >> Token.input_of;
   22.38 +val name = name_token >> Token.content_of;
   22.39 +
   22.40  val cartouche = Parse.token Parse.cartouche;
   22.41  val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
   22.42  val cartouche_input = cartouche >> Token.input_of;
   22.43  
   22.44 -val text_token = named || Parse.token (Parse.verbatim || Parse.cartouche);
   22.45 +val text_token = name_token || Parse.token (Parse.verbatim || Parse.cartouche);
   22.46  val text_input = text_token >> Token.input_of;
   22.47  val text = text_token >> Token.content_of;
   22.48  
   22.49 -val name_inner_syntax = named >> Token.inner_syntax_of;
   22.50 -val name_input = named >> Token.input_of;
   22.51 -
   22.52 -val name = named >> Token.content_of;
   22.53  val binding = Parse.position name >> Binding.make;
   22.54  val alt_name = alt_string >> Token.content_of;
   22.55  val symbol = symbolic >> Token.content_of;
   22.56 @@ -144,19 +144,22 @@
   22.57  val internal_attribute = value (fn Token.Attribute att => att);
   22.58  val internal_declaration = value (fn Token.Declaration decl => decl);
   22.59  
   22.60 -fun named_source read = internal_source || named >> evaluate Token.Source read;
   22.61 +fun named_source read = internal_source || name_token >> evaluate Token.Source read;
   22.62  
   22.63 -fun named_typ read = internal_typ || named >> evaluate Token.Typ (read o Token.inner_syntax_of);
   22.64 -fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
   22.65 +fun named_typ read =
   22.66 +  internal_typ || name_token >> evaluate Token.Typ (read o Token.inner_syntax_of);
   22.67 +
   22.68 +fun named_term read =
   22.69 +  internal_term || name_token >> evaluate Token.Term (read o Token.inner_syntax_of);
   22.70  
   22.71  fun named_fact get =
   22.72    internal_fact ||
   22.73 -  named >> evaluate Token.Fact (get o Token.content_of) >> #2 ||
   22.74 +  name_token >> evaluate Token.Fact (get o Token.content_of) >> #2 ||
   22.75    alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of) >> #2;
   22.76  
   22.77  fun named_attribute att =
   22.78    internal_attribute ||
   22.79 -  named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
   22.80 +  name_token >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
   22.81  
   22.82  fun text_declaration read =
   22.83    internal_declaration || text_token >> evaluate Token.Declaration (read o Token.input_of);
   22.84 @@ -203,7 +206,7 @@
   22.85  fun attribs check =
   22.86    let
   22.87      fun intern tok = check (Token.content_of tok, Token.pos_of tok);
   22.88 -    val attrib_name = internal_name >> #1 || (symbolic || named) >> evaluate Token.name0 intern;
   22.89 +    val attrib_name = internal_name >> #1 || (symbolic || name_token) >> evaluate Token.name0 intern;
   22.90      val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry Token.src;
   22.91    in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
   22.92  
    23.1 --- a/src/Pure/Isar/method.ML	Thu Jun 25 15:01:43 2015 +0200
    23.2 +++ b/src/Pure/Isar/method.ML	Thu Jun 25 23:51:54 2015 +0200
    23.3 @@ -17,6 +17,7 @@
    23.4    val SIMPLE_METHOD: tactic -> method
    23.5    val SIMPLE_METHOD': (int -> tactic) -> method
    23.6    val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
    23.7 +  val goals_tac: Proof.context -> string list -> cases_tactic
    23.8    val cheating: Proof.context -> bool -> method
    23.9    val intro: Proof.context -> thm list -> method
   23.10    val elim: Proof.context -> thm list -> method
   23.11 @@ -126,6 +127,17 @@
   23.12  end;
   23.13  
   23.14  
   23.15 +(* goals as cases *)
   23.16 +
   23.17 +fun goals_tac ctxt case_names st =
   23.18 +  let
   23.19 +    val cases =
   23.20 +      (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names)
   23.21 +      |> map (rpair [] o rpair [])
   23.22 +      |> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st));
   23.23 +  in Seq.single (cases, st) end;
   23.24 +
   23.25 +
   23.26  (* cheating *)
   23.27  
   23.28  fun cheating ctxt int = METHOD (fn _ => fn st =>
   23.29 @@ -676,9 +688,21 @@
   23.30    setup @{binding sleep} (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s)))
   23.31      "succeed after delay (in seconds)" #>
   23.32    setup @{binding "-"} (Scan.succeed (K insert_facts))
   23.33 -    "do nothing (insert current facts only)" #>
   23.34 +    "insert current facts, nothing else" #>
   23.35 +  setup @{binding goals} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
   23.36 +    METHOD_CASES (fn facts =>
   23.37 +      Seq.THEN (ALLGOALS (insert_tac facts), fn st =>
   23.38 +        let
   23.39 +          val _ =
   23.40 +            (case drop (Thm.nprems_of st) names of
   23.41 +              [] => ()
   23.42 +            | bad => (* FIXME Seq.Error *)
   23.43 +                error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
   23.44 +                  Position.here (Position.set_range (Token.range_of bad))));
   23.45 +        in goals_tac ctxt (map Token.content_of names) st end))))
   23.46 +    "insert facts and bind cases for goals" #>
   23.47    setup @{binding insert} (Attrib.thms >> (K o insert))
   23.48 -    "insert theorems, ignoring facts (improper)" #>
   23.49 +    "insert theorems, ignoring facts" #>
   23.50    setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
   23.51      "repeatedly apply introduction rules" #>
   23.52    setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))
    24.1 --- a/src/Pure/Isar/proof.ML	Thu Jun 25 15:01:43 2015 +0200
    24.2 +++ b/src/Pure/Isar/proof.ML	Thu Jun 25 23:51:54 2015 +0200
    24.3 @@ -422,8 +422,8 @@
    24.4      |> Seq.map (fn (meth_cases, goal') =>
    24.5        state
    24.6        |> map_goal
    24.7 -          (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases ctxt goal') #>
    24.8 -           Proof_Context.update_cases true meth_cases)
    24.9 +          (Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal') #>
   24.10 +           Proof_Context.update_cases meth_cases)
   24.11            (K (statement, using, goal', before_qed, after_qed)) I));
   24.12  
   24.13  in
    25.1 --- a/src/Pure/Isar/proof_context.ML	Thu Jun 25 15:01:43 2015 +0200
    25.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Jun 25 23:51:54 2015 +0200
    25.3 @@ -139,8 +139,8 @@
    25.4    val add_assms_cmd: Assumption.export ->
    25.5      (Thm.binding * (string * string list) list) list ->
    25.6      Proof.context -> (string * thm list) list * Proof.context
    25.7 -  val dest_cases: Proof.context -> (string * (Rule_Cases.T * bool)) list
    25.8 -  val update_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
    25.9 +  val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   25.10 +  val update_cases_legacy: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   25.11    val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
   25.12    val check_case: Proof.context -> bool ->
   25.13      string * Position.T -> binding option list -> Rule_Cases.T
   25.14 @@ -203,7 +203,7 @@
   25.15  
   25.16  (** Isar proof context information **)
   25.17  
   25.18 -type cases = ((Rule_Cases.T * bool) * int) Name_Space.table;
   25.19 +type cases = ((Rule_Cases.T * {legacy: bool}) * int) Name_Space.table;
   25.20  val empty_cases: cases = Name_Space.empty_table Markup.caseN;
   25.21  
   25.22  datatype data =
   25.23 @@ -213,7 +213,7 @@
   25.24      tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
   25.25      consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
   25.26      facts: Facts.T,              (*local facts, based on initial global facts*)
   25.27 -    cases: cases};               (*named case contexts: case, is_proper, running index*)
   25.28 +    cases: cases};               (*named case contexts: case, legacy, running index*)
   25.29  
   25.30  fun make_data (mode, syntax, tsig, consts, facts, cases) =
   25.31    Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
   25.32 @@ -1202,26 +1202,30 @@
   25.33  fun update_case _ _ ("", _) res = res
   25.34    | update_case _ _ (name, NONE) (cases, index) =
   25.35        (Name_Space.del_table name cases, index)
   25.36 -  | update_case context is_proper (name, SOME c) (cases, index) =
   25.37 +  | update_case context legacy (name, SOME c) (cases, index) =
   25.38        let
   25.39 -        val binding = Binding.name name |> not is_proper ? Binding.concealed;
   25.40 -        val (_, cases') = Name_Space.define context false (binding, ((c, is_proper), index)) cases;
   25.41 +        val binding = Binding.name name |> legacy ? Binding.concealed;
   25.42 +        val (_, cases') = cases
   25.43 +          |> Name_Space.define context false (binding, ((c, {legacy = legacy}), index));
   25.44          val index' = index + 1;
   25.45        in (cases', index') end;
   25.46  
   25.47 +fun update_cases' legacy args ctxt =
   25.48 +  let
   25.49 +    val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
   25.50 +    val cases = cases_of ctxt;
   25.51 +    val index = Name_Space.fold_table (fn _ => Integer.add 1) cases 0;
   25.52 +    val (cases', _) = fold (update_case context legacy) args (cases, index);
   25.53 +  in map_cases (K cases') ctxt end;
   25.54 +
   25.55  fun fix (b, T) ctxt =
   25.56    let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
   25.57    in (Free (x, T), ctxt') end;
   25.58  
   25.59  in
   25.60  
   25.61 -fun update_cases is_proper args ctxt =
   25.62 -  let
   25.63 -    val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
   25.64 -    val cases = cases_of ctxt;
   25.65 -    val index = Name_Space.fold_table (fn _ => Integer.add 1) cases 0;
   25.66 -    val (cases', _) = fold (update_case context is_proper) args (cases, index);
   25.67 -  in map_cases (K cases') ctxt end;
   25.68 +val update_cases = update_cases' false;
   25.69 +val update_cases_legacy = update_cases' true;
   25.70  
   25.71  fun case_result c ctxt =
   25.72    let
   25.73 @@ -1231,7 +1235,7 @@
   25.74    in
   25.75      ctxt'
   25.76      |> fold (cert_maybe_bind_term o drop_schematic) binds
   25.77 -    |> update_cases true (map (apsnd SOME) cases)
   25.78 +    |> update_cases (map (apsnd SOME) cases)
   25.79      |> pair (assumes, (binds, cases))
   25.80    end;
   25.81  
   25.82 @@ -1239,9 +1243,13 @@
   25.83  
   25.84  fun check_case ctxt internal (name, pos) fxs =
   25.85    let
   25.86 -    val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, is_proper), _)) =
   25.87 +    val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, {legacy}), _)) =
   25.88        Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
   25.89 -    val _ = if is_proper then () else Context_Position.report ctxt pos Markup.improper;
   25.90 +    val _ =
   25.91 +      if legacy then
   25.92 +        legacy_feature ("Bad case " ^ quote name ^ Position.here pos ^
   25.93 +          " -- use proof method \"goals\" instead")
   25.94 +      else ();
   25.95  
   25.96      val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) fxs;
   25.97      fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
   25.98 @@ -1357,8 +1365,8 @@
   25.99  
  25.100  fun pretty_cases ctxt =
  25.101    let
  25.102 -    fun mk_case (_, (_, false)) = NONE
  25.103 -      | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, true)) =
  25.104 +    fun mk_case (_, (_, {legacy = true})) = NONE
  25.105 +      | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, {legacy = false})) =
  25.106            SOME (name, (fixes, case_result c ctxt));
  25.107      val cases = dest_cases ctxt |> map_filter mk_case;
  25.108    in
    26.1 --- a/src/Pure/Isar/rule_cases.ML	Thu Jun 25 15:01:43 2015 +0200
    26.2 +++ b/src/Pure/Isar/rule_cases.ML	Thu Jun 25 23:51:54 2015 +0200
    26.3 @@ -27,10 +27,9 @@
    26.4      cases: (string * T) list}
    26.5    val case_hypsN: string
    26.6    val strip_params: term -> (string * typ) list
    26.7 -  val make_common: Proof.context -> term ->
    26.8 -    ((string * string list) * string list) list -> cases
    26.9 -  val make_nested: Proof.context -> term -> term ->
   26.10 -    ((string * string list) * string list) list -> cases
   26.11 +  type info = ((string * string list) * string list) list
   26.12 +  val make_common: Proof.context -> term -> info -> cases
   26.13 +  val make_nested: Proof.context -> term -> term -> info -> cases
   26.14    val apply: term list -> T -> T
   26.15    val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm ->
   26.16      (('a * (int * thm list)) * thm) Seq.seq
   26.17 @@ -51,7 +50,7 @@
   26.18    val cases_open: attribute
   26.19    val internalize_params: thm -> thm
   26.20    val save: thm -> thm -> thm
   26.21 -  val get: thm -> ((string * string list) * string list) list * int
   26.22 +  val get: thm -> info * int
   26.23    val rename_params: string list list -> thm -> thm
   26.24    val params: string list list -> attribute
   26.25    val mutual_rule: Proof.context -> thm list -> (int list * thm) option
   26.26 @@ -77,6 +76,8 @@
   26.27  
   26.28  val strip_params = map (apfst (perhaps (try Name.dest_skolem))) o Logic.strip_params;
   26.29  
   26.30 +type info = ((string * string list) * string list) list;
   26.31 +
   26.32  local
   26.33  
   26.34  fun app us t = Term.betapplys (t, us);
   26.35 @@ -221,13 +222,13 @@
   26.36  
   26.37  in
   26.38  
   26.39 -fun consume ctxt defs facts ((xx, n), th) =
   26.40 +fun consume ctxt defs facts ((a, n), th) =
   26.41    let val m = Int.min (length facts, n) in
   26.42      th
   26.43      |> unfold_prems ctxt n defs
   26.44      |> unfold_prems_concls ctxt defs
   26.45      |> Drule.multi_resolve (SOME ctxt) (take m facts)
   26.46 -    |> Seq.map (pair (xx, (n - m, drop m facts)))
   26.47 +    |> Seq.map (pair (a, (n - m, drop m facts)))
   26.48    end;
   26.49  
   26.50  end;
   26.51 @@ -424,8 +425,8 @@
   26.52        (case lookup_cases_hyp_names th of
   26.53          NONE => replicate (length cases) []
   26.54        | SOME names => names);
   26.55 -    fun regroup ((name,concls),hyps) = ((name,hyps),concls)
   26.56 -  in (map regroup (cases ~~ cases_hyps), n) end;
   26.57 +    fun regroup (name, concls) hyps = ((name, hyps), concls);
   26.58 +  in (map2 regroup cases cases_hyps, n) end;
   26.59  
   26.60  
   26.61  (* params *)
    27.1 --- a/src/Tools/induct.ML	Thu Jun 25 15:01:43 2015 +0200
    27.2 +++ b/src/Tools/induct.ML	Thu Jun 25 23:51:54 2015 +0200
    27.3 @@ -74,8 +74,7 @@
    27.4    val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
    27.5      thm list -> int -> cases_tactic
    27.6    val get_inductT: Proof.context -> term option list list -> thm list list
    27.7 -  type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
    27.8 -  val gen_induct_tac: (case_data * thm -> case_data * thm) ->
    27.9 +  val gen_induct_tac: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
   27.10      Proof.context -> bool -> (binding option * (term * bool)) option list list ->
   27.11      (string * typ) list list -> term option list -> thm list option ->
   27.12      thm list -> int -> cases_tactic
   27.13 @@ -127,15 +126,15 @@
   27.14      fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
   27.15        | conv1 k ctxt =
   27.16            Conv.rewr_conv @{thm swap_params} then_conv
   27.17 -          Conv.forall_conv (conv1 (k - 1) o snd) ctxt
   27.18 +          Conv.forall_conv (conv1 (k - 1) o snd) ctxt;
   27.19      fun conv2 0 ctxt = conv1 j ctxt
   27.20 -      | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt
   27.21 +      | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt;
   27.22    in conv2 i ctxt end;
   27.23  
   27.24  fun swap_prems_conv 0 = Conv.all_conv
   27.25    | swap_prems_conv i =
   27.26        Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
   27.27 -      Conv.rewr_conv Drule.swap_prems_eq
   27.28 +      Conv.rewr_conv Drule.swap_prems_eq;
   27.29  
   27.30  fun find_eq ctxt t =
   27.31    let
   27.32 @@ -622,7 +621,9 @@
   27.33              val xs = rename_params (Logic.strip_params A);
   27.34              val xs' =
   27.35                (case filter (fn x' => x' = x) xs of
   27.36 -                [] => xs | [_] => xs | _ => index 1 xs);
   27.37 +                [] => xs
   27.38 +              | [_] => xs
   27.39 +              | _ => index 1 xs);
   27.40            in Logic.list_rename_params xs' A end;
   27.41          fun rename_prop prop =
   27.42            let val (As, C) = Logic.strip_horn prop
   27.43 @@ -733,8 +734,6 @@
   27.44  fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   27.45    | get_inductP _ _ = [];
   27.46  
   27.47 -type case_data = (((string * string list) * string list) list * int);
   27.48 -
   27.49  fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
   27.50    SUBGOAL_CASES (fn (_, i) =>
   27.51      let
   27.52 @@ -778,7 +777,7 @@
   27.53                  val adefs = nth_list atomized_defs (j - 1);
   27.54                  val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
   27.55                  val xs = nth_list arbitrary (j - 1);
   27.56 -                val k = nth concls (j - 1) + more_consumes
   27.57 +                val k = nth concls (j - 1) + more_consumes;
   27.58                in
   27.59                  Method.insert_tac (more_facts @ adefs) THEN'
   27.60                    (if simp then