merged
authornipkow
Wed Sep 21 00:12:36 2011 +0200 (2011-09-21)
changeset 45016a5d43ffc95eb
parent 45013 05031b71a89a
parent 45015 fdac1e9880eb
child 45017 07a0638c351a
merged
NEWS
     1.1 --- a/NEWS	Tue Sep 20 22:11:22 2011 +0200
     1.2 +++ b/NEWS	Wed Sep 21 00:12:36 2011 +0200
     1.3 @@ -76,6 +76,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New proof method "induction" that gives induction hypotheses the name IH,
     1.8 +thus distinguishing them from further hypotheses that come from rule
     1.9 +induction.  The latter are still called "hyps".  Method "induction" is a thin
    1.10 +wrapper around "induct" and follows the same syntax.
    1.11 +
    1.12  * Class bot and top require underlying partial order rather than
    1.13  preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
    1.14  
     2.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Tue Sep 20 22:11:22 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Wed Sep 21 00:12:36 2011 +0200
     2.3 @@ -1259,10 +1259,12 @@
     2.4    \begin{matharray}{rcl}
     2.5      @{method_def cases} & : & @{text method} \\
     2.6      @{method_def induct} & : & @{text method} \\
     2.7 +    @{method_def induction} & : & @{text method} \\
     2.8      @{method_def coinduct} & : & @{text method} \\
     2.9    \end{matharray}
    2.10  
    2.11 -  The @{method cases}, @{method induct}, and @{method coinduct}
    2.12 +  The @{method cases}, @{method induct}, @{method induction},
    2.13 +  and @{method coinduct}
    2.14    methods provide a uniform interface to common proof techniques over
    2.15    datatypes, inductive predicates (or sets), recursive functions etc.
    2.16    The corresponding rules may be specified and instantiated in a
    2.17 @@ -1277,11 +1279,15 @@
    2.18    and parameters separately).  This avoids cumbersome encoding of
    2.19    ``strengthened'' inductive statements within the object-logic.
    2.20  
    2.21 +  Method @{method induction} differs from @{method induct} only in
    2.22 +  the names of the facts in the local context invoked by the @{command "case"}
    2.23 +  command.
    2.24 +
    2.25    @{rail "
    2.26      @@{method cases} ('(' 'no_simp' ')')? \\
    2.27        (@{syntax insts} * @'and') rule?
    2.28      ;
    2.29 -    @@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
    2.30 +    (@@{method induct} | @@{method induction}) ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
    2.31      ;
    2.32      @@{method coinduct} @{syntax insts} taking rule?
    2.33      ;
    2.34 @@ -1325,8 +1331,9 @@
    2.35    "(no_simp)"} option can be used to disable pre-simplification of
    2.36    cases (see the description of @{method induct} below for details).
    2.37  
    2.38 -  \item @{method induct}~@{text "insts R"} is analogous to the
    2.39 -  @{method cases} method, but refers to induction rules, which are
    2.40 +  \item @{method induct}~@{text "insts R"} and
    2.41 +  @{method induction}~@{text "insts R"} are analogous to the
    2.42 +  @{method cases} method, but refer to induction rules, which are
    2.43    determined as follows:
    2.44  
    2.45    \medskip
    2.46 @@ -1437,13 +1444,20 @@
    2.47    and definitions effectively participate in the inductive rephrasing
    2.48    of the original statement.
    2.49  
    2.50 -  In induction proofs, local assumptions introduced by cases are split
    2.51 +  In @{method induct} proofs, local assumptions introduced by cases are split
    2.52    into two different kinds: @{text hyps} stemming from the rule and
    2.53    @{text prems} from the goal statement.  This is reflected in the
    2.54    extracted cases accordingly, so invoking ``@{command "case"}~@{text
    2.55    c}'' will provide separate facts @{text c.hyps} and @{text c.prems},
    2.56    as well as fact @{text c} to hold the all-inclusive list.
    2.57  
    2.58 +  In @{method induction} proofs, local assumptions introduced by cases are
    2.59 +  split into three different kinds: @{text IH}, the induction hypotheses,
    2.60 +  @{text hyps}, the remaining hypotheses stemming from the rule, and
    2.61 +  @{text prems}, the assumptions from the goal statement. The names are
    2.62 +  @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above.
    2.63 +
    2.64 +
    2.65    \medskip Facts presented to either method are consumed according to
    2.66    the number of ``major premises'' of the rule involved, which is
    2.67    usually 0 for plain cases and induction rules of datatypes etc.\ and
     3.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Tue Sep 20 22:11:22 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Wed Sep 21 00:12:36 2011 +0200
     3.3 @@ -1700,10 +1700,12 @@
     3.4  \begin{matharray}{rcl}
     3.5      \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isa{method} \\
     3.6      \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isa{method} \\
     3.7 +    \indexdef{}{method}{induction}\hypertarget{method.induction}{\hyperlink{method.induction}{\mbox{\isa{induction}}}} & : & \isa{method} \\
     3.8      \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{method} \\
     3.9    \end{matharray}
    3.10  
    3.11 -  The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
    3.12 +  The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, \hyperlink{method.induction}{\mbox{\isa{induction}}},
    3.13 +  and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
    3.14    methods provide a uniform interface to common proof techniques over
    3.15    datatypes, inductive predicates (or sets), recursive functions etc.
    3.16    The corresponding rules may be specified and instantiated in a
    3.17 @@ -1718,6 +1720,10 @@
    3.18    and parameters separately).  This avoids cumbersome encoding of
    3.19    ``strengthened'' inductive statements within the object-logic.
    3.20  
    3.21 +  Method \hyperlink{method.induction}{\mbox{\isa{induction}}} differs from \hyperlink{method.induct}{\mbox{\isa{induct}}} only in
    3.22 +  the names of the facts in the local context invoked by the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}
    3.23 +  command.
    3.24 +
    3.25    \begin{railoutput}
    3.26  \rail@begin{6}{}
    3.27  \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
    3.28 @@ -1742,7 +1748,11 @@
    3.29  \rail@endbar
    3.30  \rail@end
    3.31  \rail@begin{6}{}
    3.32 +\rail@bar
    3.33  \rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]
    3.34 +\rail@nextbar{1}
    3.35 +\rail@term{\hyperlink{method.induction}{\mbox{\isa{induction}}}}[]
    3.36 +\rail@endbar
    3.37  \rail@bar
    3.38  \rail@nextbar{1}
    3.39  \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
    3.40 @@ -1872,8 +1882,9 @@
    3.41    last premise (it is usually the same for all cases).  The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option can be used to disable pre-simplification of
    3.42    cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
    3.43  
    3.44 -  \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} is analogous to the
    3.45 -  \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
    3.46 +  \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} and
    3.47 +  \hyperlink{method.induction}{\mbox{\isa{induction}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} are analogous to the
    3.48 +  \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refer to induction rules, which are
    3.49    determined as follows:
    3.50  
    3.51    \medskip
    3.52 @@ -1979,12 +1990,19 @@
    3.53    and definitions effectively participate in the inductive rephrasing
    3.54    of the original statement.
    3.55  
    3.56 -  In induction proofs, local assumptions introduced by cases are split
    3.57 +  In \hyperlink{method.induct}{\mbox{\isa{induct}}} proofs, local assumptions introduced by cases are split
    3.58    into two different kinds: \isa{hyps} stemming from the rule and
    3.59    \isa{prems} from the goal statement.  This is reflected in the
    3.60    extracted cases accordingly, so invoking ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' will provide separate facts \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems},
    3.61    as well as fact \isa{c} to hold the all-inclusive list.
    3.62  
    3.63 +  In \hyperlink{method.induction}{\mbox{\isa{induction}}} proofs, local assumptions introduced by cases are
    3.64 +  split into three different kinds: \isa{IH}, the induction hypotheses,
    3.65 +  \isa{hyps}, the remaining hypotheses stemming from the rule, and
    3.66 +  \isa{prems}, the assumptions from the goal statement. The names are
    3.67 +  \isa{c{\isaliteral{2E}{\isachardot}}IH}, \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems}, as above.
    3.68 +
    3.69 +
    3.70    \medskip Facts presented to either method are consumed according to
    3.71    the number of ``major premises'' of the rule involved, which is
    3.72    usually 0 for plain cases and induction rules of datatypes etc.\ and
     4.1 --- a/src/HOL/HOL.thy	Tue Sep 20 22:11:22 2011 +0200
     4.2 +++ b/src/HOL/HOL.thy	Wed Sep 21 00:12:36 2011 +0200
     4.3 @@ -26,6 +26,7 @@
     4.4    ("Tools/simpdata.ML")
     4.5    "~~/src/Tools/atomize_elim.ML"
     4.6    "~~/src/Tools/induct.ML"
     4.7 +  ("~~/src/Tools/induction.ML")
     4.8    ("~~/src/Tools/induct_tacs.ML")
     4.9    ("Tools/recfun_codegen.ML")
    4.10    ("Tools/cnf_funcs.ML")
    4.11 @@ -1490,8 +1491,10 @@
    4.12  )
    4.13  *}
    4.14  
    4.15 +use "~~/src/Tools/induction.ML"
    4.16 +
    4.17  setup {*
    4.18 -  Induct.setup #>
    4.19 +  Induct.setup #> Induction.setup #>
    4.20    Context.theory_map (Induct.map_simpset (fn ss => ss
    4.21      setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
    4.22        map (Simplifier.rewrite_rule (map Thm.symmetric
     5.1 --- a/src/HOL/IMP/AExp.thy	Tue Sep 20 22:11:22 2011 +0200
     5.2 +++ b/src/HOL/IMP/AExp.thy	Wed Sep 21 00:12:36 2011 +0200
     5.3 @@ -62,7 +62,7 @@
     5.4  
     5.5  theorem aval_asimp_const[simp]:
     5.6    "aval (asimp_const a) s = aval a s"
     5.7 -apply(induct a)
     5.8 +apply(induction a)
     5.9  apply (auto split: aexp.split)
    5.10  done
    5.11  
    5.12 @@ -77,7 +77,7 @@
    5.13  
    5.14  lemma aval_plus[simp]:
    5.15    "aval (plus a1 a2) s = aval a1 s + aval a2 s"
    5.16 -apply(induct a1 a2 rule: plus.induct)
    5.17 +apply(induction a1 a2 rule: plus.induct)
    5.18  apply simp_all (* just for a change from auto *)
    5.19  done
    5.20  
    5.21 @@ -94,7 +94,7 @@
    5.22  
    5.23  theorem aval_asimp[simp]:
    5.24    "aval (asimp a) s = aval a s"
    5.25 -apply(induct a)
    5.26 +apply(induction a)
    5.27  apply simp_all
    5.28  done
    5.29  
     6.1 --- a/src/HOL/IMP/ASM.thy	Tue Sep 20 22:11:22 2011 +0200
     6.2 +++ b/src/HOL/IMP/ASM.thy	Wed Sep 21 00:12:36 2011 +0200
     6.3 @@ -29,7 +29,7 @@
     6.4  
     6.5  lemma aexec_append[simp]:
     6.6    "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
     6.7 -apply(induct is1 arbitrary: stk)
     6.8 +apply(induction is1 arbitrary: stk)
     6.9  apply (auto)
    6.10  done
    6.11  
    6.12 @@ -44,7 +44,7 @@
    6.13  value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
    6.14  
    6.15  theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
    6.16 -apply(induct a arbitrary: stk)
    6.17 +apply(induction a arbitrary: stk)
    6.18  apply (auto)
    6.19  done
    6.20  
     7.1 --- a/src/HOL/IMP/AbsInt0.thy	Tue Sep 20 22:11:22 2011 +0200
     7.2 +++ b/src/HOL/IMP/AbsInt0.thy	Wed Sep 21 00:12:36 2011 +0200
     7.3 @@ -38,7 +38,7 @@
     7.4  "AI (WHILE b DO c) S = pfp (AI c) S"
     7.5  
     7.6  lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
     7.7 -proof(induct c arbitrary: s t S0)
     7.8 +proof(induction c arbitrary: s t S0)
     7.9    case SKIP thus ?case by fastforce
    7.10  next
    7.11    case Assign thus ?case
    7.12 @@ -52,10 +52,10 @@
    7.13    case (While b c)
    7.14    let ?P = "pfp (AI c) S0"
    7.15    { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
    7.16 -    proof(induct "WHILE b DO c" s t rule: big_step_induct)
    7.17 +    proof(induction "WHILE b DO c" s t rule: big_step_induct)
    7.18        case WhileFalse thus ?case by simp
    7.19      next
    7.20 -      case WhileTrue thus ?case using While.hyps pfp astate_in_rep_le by metis
    7.21 +      case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
    7.22      qed
    7.23    }
    7.24    with astate_in_rep_le[OF `s <: S0` above]
     8.1 --- a/src/HOL/IMP/AbsInt0_fun.thy	Tue Sep 20 22:11:22 2011 +0200
     8.2 +++ b/src/HOL/IMP/AbsInt0_fun.thy	Wed Sep 21 00:12:36 2011 +0200
     8.3 @@ -36,7 +36,7 @@
     8.4  "iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
     8.5  
     8.6  lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
     8.7 -apply (induct n arbitrary: x)
     8.8 +apply (induction n arbitrary: x)
     8.9   apply (simp)
    8.10  apply (simp)
    8.11  done
    8.12 @@ -52,7 +52,7 @@
    8.13  point does @{const iter} yield? *}
    8.14  
    8.15  lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
    8.16 -apply(induct n arbitrary: x)
    8.17 +apply(induction n arbitrary: x)
    8.18   apply simp
    8.19  apply (auto)
    8.20   apply(metis funpow.simps(1) id_def)
    8.21 @@ -69,7 +69,7 @@
    8.22      using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
    8.23    moreover
    8.24    { fix n have "(f^^n) x0 \<sqsubseteq> p"
    8.25 -    proof(induct n)
    8.26 +    proof(induction n)
    8.27        case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
    8.28      next
    8.29        case (Suc n) thus ?case
    8.30 @@ -155,7 +155,7 @@
    8.31  "AI (WHILE b DO c) S = pfp (AI c) S"
    8.32  
    8.33  lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
    8.34 -proof(induct c arbitrary: s t S0)
    8.35 +proof(induction c arbitrary: s t S0)
    8.36    case SKIP thus ?case by fastforce
    8.37  next
    8.38    case Assign thus ?case by (auto simp: aval'_sound)
    8.39 @@ -167,10 +167,10 @@
    8.40    case (While b c)
    8.41    let ?P = "pfp (AI c) S0"
    8.42    { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
    8.43 -    proof(induct "WHILE b DO c" s t rule: big_step_induct)
    8.44 +    proof(induction "WHILE b DO c" s t rule: big_step_induct)
    8.45        case WhileFalse thus ?case by simp
    8.46      next
    8.47 -      case WhileTrue thus ?case by(metis While.hyps pfp fun_in_rep_le)
    8.48 +      case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
    8.49      qed
    8.50    }
    8.51    with fun_in_rep_le[OF `s <: S0` above]
     9.1 --- a/src/HOL/IMP/AbsInt1.thy	Tue Sep 20 22:11:22 2011 +0200
     9.2 +++ b/src/HOL/IMP/AbsInt1.thy	Wed Sep 21 00:12:36 2011 +0200
     9.3 @@ -141,7 +141,7 @@
     9.4     in afilter e1 res1 (afilter e2 res2 S))"
     9.5  
     9.6  lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
     9.7 -proof(induct e arbitrary: a S)
     9.8 +proof(induction e arbitrary: a S)
     9.9    case N thus ?case by simp
    9.10  next
    9.11    case (V x)
    9.12 @@ -158,7 +158,7 @@
    9.13  qed
    9.14  
    9.15  lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
    9.16 -proof(induct b arbitrary: S bv)
    9.17 +proof(induction b arbitrary: S bv)
    9.18    case B thus ?case by simp
    9.19  next
    9.20    case (Not b) thus ?case by simp
    9.21 @@ -181,7 +181,7 @@
    9.22    bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)"
    9.23  
    9.24  lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
    9.25 -proof(induct c arbitrary: s t S)
    9.26 +proof(induction c arbitrary: s t S)
    9.27    case SKIP thus ?case by fastforce
    9.28  next
    9.29    case Assign thus ?case
    9.30 @@ -196,12 +196,12 @@
    9.31    { fix s t
    9.32      have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
    9.33            t <:: bfilter b False ?P"
    9.34 -    proof(induct "WHILE b DO c" s t rule: big_step_induct)
    9.35 +    proof(induction "WHILE b DO c" s t rule: big_step_induct)
    9.36        case WhileFalse thus ?case by(metis bfilter_sound)
    9.37      next
    9.38        case WhileTrue show ?case
    9.39          by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
    9.40 -           rule While.hyps[OF WhileTrue(2)],
    9.41 +           rule While.IH[OF WhileTrue(2)],
    9.42             rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
    9.43      qed
    9.44    }
    10.1 --- a/src/HOL/IMP/AbsInt2.thy	Tue Sep 20 22:11:22 2011 +0200
    10.2 +++ b/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 00:12:36 2011 +0200
    10.3 @@ -24,7 +24,7 @@
    10.4    (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
    10.5  
    10.6  lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
    10.7 -apply (induct n arbitrary: x)
    10.8 +apply (induction n arbitrary: x)
    10.9   apply (simp)
   10.10  apply (simp add: Let_def)
   10.11  done
   10.12 @@ -35,7 +35,7 @@
   10.13    (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
   10.14  
   10.15  lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
   10.16 -apply (induct n arbitrary: x)
   10.17 +apply (induction n arbitrary: x)
   10.18   apply (simp)
   10.19  apply (simp add: Let_def)
   10.20  done
    11.1 --- a/src/HOL/IMP/BExp.thy	Tue Sep 20 22:11:22 2011 +0200
    11.2 +++ b/src/HOL/IMP/BExp.thy	Wed Sep 21 00:12:36 2011 +0200
    11.3 @@ -23,7 +23,7 @@
    11.4  "less a1 a2 = Less a1 a2"
    11.5  
    11.6  lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
    11.7 -apply(induct a1 a2 rule: less.induct)
    11.8 +apply(induction a1 a2 rule: less.induct)
    11.9  apply simp_all
   11.10  done
   11.11  
   11.12 @@ -35,7 +35,7 @@
   11.13  "and b1 b2 = And b1 b2"
   11.14  
   11.15  lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
   11.16 -apply(induct b1 b2 rule: and.induct)
   11.17 +apply(induction b1 b2 rule: and.induct)
   11.18  apply simp_all
   11.19  done
   11.20  
   11.21 @@ -45,7 +45,7 @@
   11.22  "not b = Not b"
   11.23  
   11.24  lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
   11.25 -apply(induct b rule: not.induct)
   11.26 +apply(induction b rule: not.induct)
   11.27  apply simp_all
   11.28  done
   11.29  
   11.30 @@ -62,7 +62,7 @@
   11.31  value "bsimp (And (Less (N 1) (N 0)) (B True))"
   11.32  
   11.33  theorem "bval (bsimp b) s = bval b s"
   11.34 -apply(induct b)
   11.35 +apply(induction b)
   11.36  apply simp_all
   11.37  done
   11.38  
    12.1 --- a/src/HOL/IMP/Big_Step.thy	Tue Sep 20 22:11:22 2011 +0200
    12.2 +++ b/src/HOL/IMP/Big_Step.thy	Wed Sep 21 00:12:36 2011 +0200
    12.3 @@ -215,7 +215,7 @@
    12.4  
    12.5  text {* This proof is automatic. *}
    12.6  theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
    12.7 -apply (induct arbitrary: u rule: big_step.induct)
    12.8 +apply (induction arbitrary: u rule: big_step.induct)
    12.9  apply blast+
   12.10  done
   12.11  
   12.12 @@ -225,7 +225,7 @@
   12.13  *}
   12.14  theorem
   12.15    "(c,s) \<Rightarrow> t  \<Longrightarrow>  (c,s) \<Rightarrow> t'  \<Longrightarrow>  t' = t"
   12.16 -proof (induct arbitrary: t' rule: big_step.induct)
   12.17 +proof (induction arbitrary: t' rule: big_step.induct)
   12.18    -- "the only interesting case, @{text WhileTrue}:"
   12.19    fix b c s s1 t t'
   12.20    -- "The assumptions of the rule:"
    13.1 --- a/src/HOL/IMP/Comp_Rev.thy	Tue Sep 20 22:11:22 2011 +0200
    13.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Wed Sep 21 00:12:36 2011 +0200
    13.3 @@ -196,13 +196,13 @@
    13.4    "0 \<le> i \<Longrightarrow>
    13.5    succs (bcomp b c i) n \<subseteq> {n .. n + isize (bcomp b c i)}
    13.6                             \<union> {n + i + isize (bcomp b c i)}" 
    13.7 -proof (induct b arbitrary: c i n)
    13.8 +proof (induction b arbitrary: c i n)
    13.9    case (And b1 b2)
   13.10    from And.prems
   13.11    show ?case 
   13.12      by (cases c)
   13.13 -       (auto dest: And.hyps(1) [THEN subsetD, rotated] 
   13.14 -                   And.hyps(2) [THEN subsetD, rotated])
   13.15 +       (auto dest: And.IH(1) [THEN subsetD, rotated] 
   13.16 +                   And.IH(2) [THEN subsetD, rotated])
   13.17  qed auto
   13.18  
   13.19  lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]
   13.20 @@ -219,7 +219,7 @@
   13.21  
   13.22  lemma ccomp_succs:
   13.23    "succs (ccomp c) n \<subseteq> {n..n + isize (ccomp c)}"
   13.24 -proof (induct c arbitrary: n)
   13.25 +proof (induction c arbitrary: n)
   13.26    case SKIP thus ?case by simp
   13.27  next
   13.28    case Assign thus ?case by simp
   13.29 @@ -227,16 +227,16 @@
   13.30    case (Semi c1 c2)
   13.31    from Semi.prems
   13.32    show ?case 
   13.33 -    by (fastforce dest: Semi.hyps [THEN subsetD])
   13.34 +    by (fastforce dest: Semi.IH [THEN subsetD])
   13.35  next
   13.36    case (If b c1 c2)
   13.37    from If.prems
   13.38    show ?case
   13.39 -    by (auto dest!: If.hyps [THEN subsetD] simp: isuccs_def succs_Cons)
   13.40 +    by (auto dest!: If.IH [THEN subsetD] simp: isuccs_def succs_Cons)
   13.41  next
   13.42    case (While b c)
   13.43    from While.prems
   13.44 -  show ?case by (auto dest!: While.hyps [THEN subsetD])
   13.45 +  show ?case by (auto dest!: While.IH [THEN subsetD])
   13.46  qed
   13.47  
   13.48  lemma ccomp_exits:
   13.49 @@ -264,7 +264,7 @@
   13.50                     i' \<in> exits c \<and> 
   13.51                     P @ c @ P' \<turnstile> (isize P + i', s'') \<rightarrow>^m (j, s') \<and>
   13.52                     n = k + m" 
   13.53 -using assms proof (induct n arbitrary: i j s)
   13.54 +using assms proof (induction n arbitrary: i j s)
   13.55    case 0
   13.56    thus ?case by simp
   13.57  next
   13.58 @@ -289,7 +289,7 @@
   13.59    { assume "j0 \<in> {0 ..< isize c}"
   13.60      with j0 j rest c
   13.61      have ?case
   13.62 -      by (fastforce dest!: Suc.hyps intro!: exec_Suc)
   13.63 +      by (fastforce dest!: Suc.IH intro!: exec_Suc)
   13.64    } moreover {
   13.65      assume "j0 \<notin> {0 ..< isize c}"
   13.66      moreover
   13.67 @@ -338,7 +338,7 @@
   13.68    assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"
   13.69            "isize P \<le> i" "exits P' \<subseteq> {0..}"
   13.70    shows "P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')"
   13.71 -using assms proof (induct k arbitrary: i s stk)
   13.72 +using assms proof (induction k arbitrary: i s stk)
   13.73    case 0 thus ?case by simp
   13.74  next
   13.75    case (Suc k)
   13.76 @@ -357,7 +357,7 @@
   13.77    have "isize P \<le> i'" by (auto simp: exits_def)
   13.78    from rest this `exits P' \<subseteq> {0..}`     
   13.79    have "P' \<turnstile> (i' - isize P, s'', stk'') \<rightarrow>^k (n - isize P, s', stk')"
   13.80 -    by (rule Suc.hyps)
   13.81 +    by (rule Suc.IH)
   13.82    finally
   13.83    show ?case .
   13.84  qed
   13.85 @@ -411,7 +411,7 @@
   13.86  lemma acomp_exec_n [dest!]:
   13.87    "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (isize (acomp a),s',stk') \<Longrightarrow> 
   13.88    s' = s \<and> stk' = aval a s#stk"
   13.89 -proof (induct a arbitrary: n s' stk stk')
   13.90 +proof (induction a arbitrary: n s' stk stk')
   13.91    case (Plus a1 a2)
   13.92    let ?sz = "isize (acomp a1) + (isize (acomp a2) + 1)"
   13.93    from Plus.prems
   13.94 @@ -424,7 +424,7 @@
   13.95         "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
   13.96      by (auto dest!: exec_n_split_full)
   13.97  
   13.98 -  thus ?case by (fastforce dest: Plus.hyps simp: exec_n_simps)
   13.99 +  thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps)
  13.100  qed (auto simp: exec_n_simps)
  13.101  
  13.102  lemma bcomp_split:
  13.103 @@ -442,13 +442,13 @@
  13.104            "isize (bcomp b c j) \<le> i" "0 \<le> j"
  13.105    shows "i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
  13.106           s' = s \<and> stk' = stk"
  13.107 -using assms proof (induct b arbitrary: c j i n s' stk')
  13.108 +using assms proof (induction b arbitrary: c j i n s' stk')
  13.109    case B thus ?case 
  13.110      by (simp split: split_if_asm add: exec_n_simps)
  13.111  next
  13.112    case (Not b) 
  13.113    from Not.prems show ?case
  13.114 -    by (fastforce dest!: Not.hyps) 
  13.115 +    by (fastforce dest!: Not.IH) 
  13.116  next
  13.117    case (And b1 b2)
  13.118    
  13.119 @@ -466,10 +466,10 @@
  13.120      by (auto dest!: bcomp_split dest: exec_n_drop_left)
  13.121    from b1 j
  13.122    have "i' = isize ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk"
  13.123 -    by (auto dest!: And.hyps)
  13.124 +    by (auto dest!: And.IH)
  13.125    with b2 j
  13.126    show ?case 
  13.127 -    by (fastforce dest!: And.hyps simp: exec_n_end split: split_if_asm)
  13.128 +    by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm)
  13.129  next
  13.130    case Less
  13.131    thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *) 
  13.132 @@ -484,7 +484,7 @@
  13.133  lemma ccomp_exec_n:
  13.134    "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk')
  13.135    \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
  13.136 -proof (induct c arbitrary: s t stk stk' n)
  13.137 +proof (induction c arbitrary: s t stk stk' n)
  13.138    case SKIP
  13.139    thus ?case by auto
  13.140  next
  13.141 @@ -496,7 +496,7 @@
  13.142    thus ?case by (fastforce dest!: exec_n_split_full)
  13.143  next
  13.144    case (If b c1 c2)
  13.145 -  note If.hyps [dest!]
  13.146 +  note If.IH [dest!]
  13.147  
  13.148    let ?if = "IF b THEN c1 ELSE c2"
  13.149    let ?cs = "ccomp ?if"
  13.150 @@ -538,7 +538,7 @@
  13.151  
  13.152    from While.prems
  13.153    show ?case
  13.154 -  proof (induct n arbitrary: s rule: nat_less_induct)
  13.155 +  proof (induction n arbitrary: s rule: nat_less_induct)
  13.156      case (1 n)
  13.157      
  13.158      { assume "\<not> bval b s"
  13.159 @@ -568,7 +568,7 @@
  13.160            "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (isize (ccomp ?c0), t, stk')"
  13.161            "m < n"
  13.162            by (auto simp: exec_n_step [where k=k])
  13.163 -        with "1.hyps"
  13.164 +        with "1.IH"
  13.165          show ?case by blast
  13.166        next
  13.167          assume "ccomp c \<noteq> []"
  13.168 @@ -581,14 +581,14 @@
  13.169            by (auto dest: exec_n_split [where i=0, simplified])
  13.170          from c
  13.171          have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk"
  13.172 -          by (auto dest!: While.hyps)
  13.173 +          by (auto dest!: While.IH)
  13.174          moreover
  13.175          from rest m k stk
  13.176          obtain k' where
  13.177            "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (isize ?cs, t, stk')"
  13.178            "k' < n"
  13.179            by (auto simp: exec_n_step [where k=m])
  13.180 -        with "1.hyps"
  13.181 +        with "1.IH"
  13.182          have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast
  13.183          ultimately
  13.184          show ?case using b by blast
    14.1 --- a/src/HOL/IMP/Compiler.thy	Tue Sep 20 22:11:22 2011 +0200
    14.2 +++ b/src/HOL/IMP/Compiler.thy	Wed Sep 21 00:12:36 2011 +0200
    14.3 @@ -222,7 +222,7 @@
    14.4    "0 \<le> n \<Longrightarrow>
    14.5    bcomp b c n \<turnstile>
    14.6   (0,s,stk)  \<rightarrow>*  (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
    14.7 -proof(induct b arbitrary: c n m)
    14.8 +proof(induction b arbitrary: c n m)
    14.9    case Not
   14.10    from Not(1)[where c="~c"] Not(2) show ?case by fastforce
   14.11  next
   14.12 @@ -256,17 +256,17 @@
   14.13  
   14.14  lemma ccomp_bigstep:
   14.15    "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
   14.16 -proof(induct arbitrary: stk rule: big_step_induct)
   14.17 +proof(induction arbitrary: stk rule: big_step_induct)
   14.18    case (Assign x a s)
   14.19    show ?case by (fastforce simp:fun_upd_def cong: if_cong)
   14.20  next
   14.21    case (Semi c1 s1 s2 c2 s3)
   14.22    let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
   14.23    have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
   14.24 -    using Semi.hyps(2) by fastforce
   14.25 +    using Semi.IH(1) by fastforce
   14.26    moreover
   14.27    have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
   14.28 -    using Semi.hyps(4) by fastforce
   14.29 +    using Semi.IH(2) by fastforce
   14.30    ultimately show ?case by simp (blast intro: exec_trans)
   14.31  next
   14.32    case (WhileTrue b s1 c s2 s3)
   14.33 @@ -274,12 +274,12 @@
   14.34    let ?cb = "bcomp b False (isize ?cc + 1)"
   14.35    let ?cw = "ccomp(WHILE b DO c)"
   14.36    have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
   14.37 -    using WhileTrue(1,3) by fastforce
   14.38 +    using WhileTrue.IH(1) WhileTrue.hyps(1) by fastforce
   14.39    moreover
   14.40    have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
   14.41      by fastforce
   14.42    moreover
   14.43 -  have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue(5))
   14.44 +  have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue.IH(2))
   14.45    ultimately show ?case by(blast intro: exec_trans)
   14.46  qed fastforce+
   14.47  
    15.1 --- a/src/HOL/IMP/Def_Ass_Sound_Big.thy	Tue Sep 20 22:11:22 2011 +0200
    15.2 +++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy	Wed Sep 21 00:12:36 2011 +0200
    15.3 @@ -12,7 +12,7 @@
    15.4  theorem Sound:
    15.5    "\<lbrakk> (c,Some s) \<Rightarrow> s';  D A c A';  A \<subseteq> dom s \<rbrakk>
    15.6    \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
    15.7 -proof (induct c "Some s" s' arbitrary: s A A' rule:big_step_induct)
    15.8 +proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct)
    15.9    case AssignNone thus ?case
   15.10      by auto (metis aval_Some option.simps(3) subset_trans)
   15.11  next
    16.1 --- a/src/HOL/IMP/Def_Ass_Sound_Small.thy	Tue Sep 20 22:11:22 2011 +0200
    16.2 +++ b/src/HOL/IMP/Def_Ass_Sound_Small.thy	Wed Sep 21 00:12:36 2011 +0200
    16.3 @@ -7,7 +7,7 @@
    16.4  
    16.5  theorem progress:
    16.6    "D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"
    16.7 -proof (induct c arbitrary: s A')
    16.8 +proof (induction c arbitrary: s A')
    16.9    case Assign thus ?case by auto (metis aval_Some small_step.Assign)
   16.10  next
   16.11    case (If b c1 c2)
   16.12 @@ -17,13 +17,13 @@
   16.13  qed (fastforce intro: small_step.intros)+
   16.14  
   16.15  lemma D_mono:  "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
   16.16 -proof (induct c arbitrary: A A' M)
   16.17 +proof (induction c arbitrary: A A' M)
   16.18    case Semi thus ?case by auto (metis D.intros(3))
   16.19  next
   16.20    case (If b c1 c2)
   16.21    then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
   16.22      by auto
   16.23 -  with If.hyps `A \<subseteq> A'` obtain M1' M2'
   16.24 +  with If.IH `A \<subseteq> A'` obtain M1' M2'
   16.25      where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
   16.26    hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
   16.27      using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastforce intro: D.intros)+
   16.28 @@ -34,7 +34,7 @@
   16.29  
   16.30  theorem D_preservation:
   16.31    "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
   16.32 -proof (induct arbitrary: A rule: small_step_induct)
   16.33 +proof (induction arbitrary: A rule: small_step_induct)
   16.34    case (While b c s)
   16.35    then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
   16.36    moreover
   16.37 @@ -49,7 +49,7 @@
   16.38  theorem D_sound:
   16.39    "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' \<Longrightarrow> c' \<noteq> SKIP
   16.40     \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
   16.41 -apply(induct arbitrary: A' rule:star_induct)
   16.42 +apply(induction arbitrary: A' rule:star_induct)
   16.43  apply (metis progress)
   16.44  by (metis D_preservation)
   16.45  
    17.1 --- a/src/HOL/IMP/Denotation.thy	Tue Sep 20 22:11:22 2011 +0200
    17.2 +++ b/src/HOL/IMP/Denotation.thy	Wed Sep 21 00:12:36 2011 +0200
    17.3 @@ -32,7 +32,7 @@
    17.4  text{* Equivalence of denotational and big-step semantics: *}
    17.5  
    17.6  lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
    17.7 -apply (induct rule: big_step_induct)
    17.8 +apply (induction rule: big_step_induct)
    17.9  apply auto
   17.10  (* while *)
   17.11  apply (unfold Gamma_def)
   17.12 @@ -43,7 +43,7 @@
   17.13  done
   17.14  
   17.15  lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
   17.16 -apply (induct c arbitrary: s t)
   17.17 +apply (induction c arbitrary: s t)
   17.18  apply auto 
   17.19  apply blast
   17.20  (* while *)
    18.1 --- a/src/HOL/IMP/Fold.thy	Tue Sep 20 22:11:22 2011 +0200
    18.2 +++ b/src/HOL/IMP/Fold.thy	Wed Sep 21 00:12:36 2011 +0200
    18.3 @@ -81,7 +81,7 @@
    18.4  
    18.5  lemma defs_restrict:
    18.6    "defs c t |` (- lnames c) = t |` (- lnames c)"
    18.7 -proof (induct c arbitrary: t)
    18.8 +proof (induction c arbitrary: t)
    18.9    case (Semi c1 c2)
   18.10    hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
   18.11      by simp
   18.12 @@ -114,7 +114,7 @@
   18.13  
   18.14  lemma big_step_pres_approx:
   18.15    "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'"
   18.16 -proof (induct arbitrary: t rule: big_step_induct)
   18.17 +proof (induction arbitrary: t rule: big_step_induct)
   18.18    case Skip thus ?case by simp
   18.19  next
   18.20    case Assign
   18.21 @@ -122,8 +122,8 @@
   18.22      by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
   18.23  next
   18.24    case (Semi c1 s1 s2 c2 s3)
   18.25 -  have "approx (defs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
   18.26 -  hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi(4))
   18.27 +  have "approx (defs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
   18.28 +  hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi.IH(2))
   18.29    thus ?case by simp
   18.30  next
   18.31    case (IfTrue b s c1 s')
   18.32 @@ -151,7 +151,7 @@
   18.33  
   18.34  lemma big_step_pres_approx_restrict:
   18.35    "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
   18.36 -proof (induct arbitrary: t rule: big_step_induct)
   18.37 +proof (induction arbitrary: t rule: big_step_induct)
   18.38    case Assign
   18.39    thus ?case by (clarsimp simp: approx_def)
   18.40  next
   18.41 @@ -190,7 +190,7 @@
   18.42  
   18.43  lemma approx_eq:
   18.44    "approx t \<Turnstile> c \<sim> fold c t"
   18.45 -proof (induct c arbitrary: t)
   18.46 +proof (induction c arbitrary: t)
   18.47    case SKIP show ?case by simp
   18.48  next
   18.49    case Assign
   18.50 @@ -292,7 +292,7 @@
   18.51  
   18.52  lemma bdefs_restrict:
   18.53    "bdefs c t |` (- lnames c) = t |` (- lnames c)"
   18.54 -proof (induct c arbitrary: t)
   18.55 +proof (induction c arbitrary: t)
   18.56    case (Semi c1 c2)
   18.57    hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
   18.58      by simp
   18.59 @@ -327,7 +327,7 @@
   18.60  
   18.61  lemma big_step_pres_approx_b:
   18.62    "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'" 
   18.63 -proof (induct arbitrary: t rule: big_step_induct)
   18.64 +proof (induction arbitrary: t rule: big_step_induct)
   18.65    case Skip thus ?case by simp
   18.66  next
   18.67    case Assign
   18.68 @@ -335,8 +335,8 @@
   18.69      by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
   18.70  next
   18.71    case (Semi c1 s1 s2 c2 s3)
   18.72 -  have "approx (bdefs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
   18.73 -  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi(4))
   18.74 +  have "approx (bdefs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
   18.75 +  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi.IH(2))
   18.76    thus ?case by simp
   18.77  next
   18.78    case (IfTrue b s c1 s')
   18.79 @@ -371,7 +371,7 @@
   18.80  
   18.81  lemma bfold_equiv: 
   18.82    "approx t \<Turnstile> c \<sim> bfold c t"
   18.83 -proof (induct c arbitrary: t)
   18.84 +proof (induction c arbitrary: t)
   18.85    case SKIP show ?case by simp
   18.86  next
   18.87    case Assign
    19.1 --- a/src/HOL/IMP/HoareT.thy	Tue Sep 20 22:11:22 2011 +0200
    19.2 +++ b/src/HOL/IMP/HoareT.thy	Wed Sep 21 00:12:36 2011 +0200
    19.3 @@ -88,7 +88,7 @@
    19.4    proof
    19.5      fix s
    19.6      show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)"
    19.7 -    proof(induct "f s" arbitrary: s rule: less_induct)
    19.8 +    proof(induction "f s" arbitrary: s rule: less_induct)
    19.9        case (less n)
   19.10        thus ?case by (metis While(2) WhileFalse WhileTrue)
   19.11      qed
   19.12 @@ -137,7 +137,7 @@
   19.13  text{* The relation is in fact a function: *}
   19.14  
   19.15  lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
   19.16 -proof(induct arbitrary: n' rule:Its.induct)
   19.17 +proof(induction arbitrary: n' rule:Its.induct)
   19.18  (* new release:
   19.19    case Its_0 thus ?case by(metis Its.cases)
   19.20  next
   19.21 @@ -160,7 +160,7 @@
   19.22  text{* For all terminating loops, @{const Its} yields a result: *}
   19.23  
   19.24  lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
   19.25 -proof(induct "WHILE b DO c" s t rule: big_step_induct)
   19.26 +proof(induction "WHILE b DO c" s t rule: big_step_induct)
   19.27    case WhileFalse thus ?case by (metis Its_0)
   19.28  next
   19.29    case WhileTrue thus ?case by (metis Its_Suc)
   19.30 @@ -179,7 +179,7 @@
   19.31  by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality)
   19.32  
   19.33  lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
   19.34 -proof (induct c arbitrary: Q)
   19.35 +proof (induction c arbitrary: Q)
   19.36    case SKIP show ?case by simp (blast intro:hoaret.Skip)
   19.37  next
   19.38    case Assign show ?case by simp (blast intro:hoaret.Assign)
    20.1 --- a/src/HOL/IMP/Hoare_Examples.thy	Tue Sep 20 22:11:22 2011 +0200
    20.2 +++ b/src/HOL/IMP/Hoare_Examples.thy	Wed Sep 21 00:12:36 2011 +0200
    20.3 @@ -25,7 +25,7 @@
    20.4    
    20.5  lemma while_sum:
    20.6    "(w n, s) \<Rightarrow> t \<Longrightarrow> t ''x'' = s ''x'' + \<Sum> {s ''y'' + 1 .. n}"
    20.7 -apply(induct "w n" s t rule: big_step_induct)
    20.8 +apply(induction "w n" s t rule: big_step_induct)
    20.9  apply(auto simp add: setsum_head_plus_1)
   20.10  done
   20.11  
    21.1 --- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Sep 20 22:11:22 2011 +0200
    21.2 +++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Wed Sep 21 00:12:36 2011 +0200
    21.3 @@ -9,11 +9,11 @@
    21.4  "\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t  \<longrightarrow>  P s \<longrightarrow>  Q t)"
    21.5  
    21.6  lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
    21.7 -proof(induct rule: hoare.induct)
    21.8 +proof(induction rule: hoare.induct)
    21.9    case (While P b c)
   21.10    { fix s t
   21.11      have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s \<longrightarrow> P t \<and> \<not> bval b t"
   21.12 -    proof(induct "WHILE b DO c" s t rule: big_step_induct)
   21.13 +    proof(induction "WHILE b DO c" s t rule: big_step_induct)
   21.14        case WhileFalse thus ?case by blast
   21.15      next
   21.16        case WhileTrue thus ?case
   21.17 @@ -59,7 +59,7 @@
   21.18  subsection "Completeness"
   21.19  
   21.20  lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
   21.21 -proof(induct c arbitrary: Q)
   21.22 +proof(induction c arbitrary: Q)
   21.23    case Semi thus ?case by(auto intro: Semi)
   21.24  next
   21.25    case (If b c1 c2)
    22.1 --- a/src/HOL/IMP/Live.thy	Tue Sep 20 22:11:22 2011 +0200
    22.2 +++ b/src/HOL/IMP/Live.thy	Wed Sep 21 00:12:36 2011 +0200
    22.3 @@ -44,17 +44,17 @@
    22.4  theorem L_sound:
    22.5    "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
    22.6    \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
    22.7 -proof (induct arbitrary: X t rule: big_step_induct)
    22.8 +proof (induction arbitrary: X t rule: big_step_induct)
    22.9    case Skip then show ?case by auto
   22.10  next
   22.11    case Assign then show ?case
   22.12      by (auto simp: ball_Un)
   22.13  next
   22.14    case (Semi c1 s1 s2 c2 s3 X t1)
   22.15 -  from Semi(2,5) obtain t2 where
   22.16 +  from Semi.IH(1) Semi.prems obtain t2 where
   22.17      t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
   22.18      by simp blast
   22.19 -  from Semi(4)[OF s2t2] obtain t3 where
   22.20 +  from Semi.IH(2)[OF s2t2] obtain t3 where
   22.21      t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
   22.22      by auto
   22.23    show ?case using t12 t23 s3t3 by auto
   22.24 @@ -83,9 +83,9 @@
   22.25      by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   22.26    have "s1 = t1 on L c (L ?w X)" using  L_While_subset WhileTrue.prems
   22.27      by (blast)
   22.28 -  from WhileTrue(3)[OF this] obtain t2 where
   22.29 +  from WhileTrue.IH(1)[OF this] obtain t2 where
   22.30      "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
   22.31 -  from WhileTrue(5)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
   22.32 +  from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
   22.33      by auto
   22.34    with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
   22.35  qed
   22.36 @@ -108,17 +108,17 @@
   22.37  theorem bury_sound:
   22.38    "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
   22.39    \<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X"
   22.40 -proof (induct arbitrary: X t rule: big_step_induct)
   22.41 +proof (induction arbitrary: X t rule: big_step_induct)
   22.42    case Skip then show ?case by auto
   22.43  next
   22.44    case Assign then show ?case
   22.45      by (auto simp: ball_Un)
   22.46  next
   22.47    case (Semi c1 s1 s2 c2 s3 X t1)
   22.48 -  from Semi(2,5) obtain t2 where
   22.49 +  from Semi.IH(1) Semi.prems obtain t2 where
   22.50      t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
   22.51      by simp blast
   22.52 -  from Semi(4)[OF s2t2] obtain t3 where
   22.53 +  from Semi.IH(2)[OF s2t2] obtain t3 where
   22.54      t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
   22.55      by auto
   22.56    show ?case using t12 t23 s3t3 by auto
   22.57 @@ -147,9 +147,9 @@
   22.58      by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   22.59    have "s1 = t1 on L c (L ?w X)"
   22.60      using L_While_subset WhileTrue.prems by blast
   22.61 -  from WhileTrue(3)[OF this] obtain t2 where
   22.62 +  from WhileTrue.IH(1)[OF this] obtain t2 where
   22.63      "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
   22.64 -  from WhileTrue(5)[OF this(2)] obtain t3
   22.65 +  from WhileTrue.IH(2)[OF this(2)] obtain t3
   22.66      where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
   22.67      by auto
   22.68    with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
   22.69 @@ -184,7 +184,7 @@
   22.70  theorem bury_sound2:
   22.71    "(bury c X,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
   22.72    \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
   22.73 -proof (induct "bury c X" s s' arbitrary: c X t rule: big_step_induct)
   22.74 +proof (induction "bury c X" s s' arbitrary: c X t rule: big_step_induct)
   22.75    case Skip then show ?case by auto
   22.76  next
   22.77    case Assign then show ?case
   22.78 @@ -193,9 +193,10 @@
   22.79    case (Semi bc1 s1 s2 bc2 s3 c X t1)
   22.80    then obtain c1 c2 where c: "c = c1;c2"
   22.81      and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
   22.82 -  from Semi(2)[OF bc1, of t1] Semi.prems c obtain t2 where
   22.83 +  note IH = Semi.hyps(2,4)
   22.84 +  from IH(1)[OF bc1, of t1] Semi.prems c obtain t2 where
   22.85      t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
   22.86 -  from Semi(4)[OF bc2 s2t2] obtain t3 where
   22.87 +  from IH(2)[OF bc2 s2t2] obtain t3 where
   22.88      t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
   22.89      by auto
   22.90    show ?case using c t12 t23 s3t3 by auto
   22.91 @@ -205,7 +206,8 @@
   22.92      and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
   22.93    have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
   22.94    from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
   22.95 -  from IfTrue(3)[OF bc1 `s = t on L c1 X`] obtain t' where
   22.96 +  note IH = IfTrue.hyps(3)
   22.97 +  from IH[OF bc1 `s = t on L c1 X`] obtain t' where
   22.98      "(c1, t) \<Rightarrow> t'" "s' =t' on X" by auto
   22.99    thus ?case using c `bval b t` by auto
  22.100  next
  22.101 @@ -214,7 +216,8 @@
  22.102      and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
  22.103    have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
  22.104    from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
  22.105 -  from IfFalse(3)[OF bc2 `s = t on L c2 X`] obtain t' where
  22.106 +  note IH = IfFalse.hyps(3)
  22.107 +  from IH[OF bc2 `s = t on L c2 X`] obtain t' where
  22.108      "(c2, t) \<Rightarrow> t'" "s' =t' on X" by auto
  22.109    thus ?case using c `~bval b t` by auto
  22.110  next
  22.111 @@ -228,11 +231,12 @@
  22.112    let ?w = "WHILE b DO c'"
  22.113    from `bval b s1` WhileTrue.prems c have "bval b t1"
  22.114      by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
  22.115 +  note IH = WhileTrue.hyps(3,5)
  22.116    have "s1 = t1 on L c' (L ?w X)"
  22.117      using L_While_subset WhileTrue.prems c by blast
  22.118 -  with WhileTrue(3)[OF bc', of t1] obtain t2 where
  22.119 +  with IH(1)[OF bc', of t1] obtain t2 where
  22.120      "(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
  22.121 -  from WhileTrue(5)[OF WhileTrue(6), of t2] c this(2) obtain t3
  22.122 +  from IH(2)[OF WhileTrue.hyps(6), of t2] c this(2) obtain t3
  22.123      where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
  22.124      by auto
  22.125    with `bval b t1` `(c', t1) \<Rightarrow> t2` c show ?case by auto
    23.1 --- a/src/HOL/IMP/Poly_Types.thy	Tue Sep 20 22:11:22 2011 +0200
    23.2 +++ b/src/HOL/IMP/Poly_Types.thy	Wed Sep 21 00:12:36 2011 +0200
    23.3 @@ -45,12 +45,12 @@
    23.4  subsection{* Typing is Preserved by Substitution *}
    23.5  
    23.6  lemma subst_atyping: "E \<turnstile>p a : t \<Longrightarrow> tsubst S \<circ> E \<turnstile>p a : tsubst S t"
    23.7 -apply(induct rule: atyping.induct)
    23.8 +apply(induction rule: atyping.induct)
    23.9  apply(auto intro: atyping.intros)
   23.10  done
   23.11  
   23.12  lemma subst_btyping: "E \<turnstile>p (b::bexp) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p b"
   23.13 -apply(induct rule: btyping.induct)
   23.14 +apply(induction rule: btyping.induct)
   23.15  apply(auto intro: btyping.intros)
   23.16  apply(drule subst_atyping[where S=S])
   23.17  apply(drule subst_atyping[where S=S])
   23.18 @@ -58,7 +58,7 @@
   23.19  done
   23.20  
   23.21  lemma subst_ctyping: "E \<turnstile>p (c::com) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p c"
   23.22 -apply(induct rule: ctyping.induct)
   23.23 +apply(induction rule: ctyping.induct)
   23.24  apply(auto intro: ctyping.intros)
   23.25  apply(drule subst_atyping[where S=S])
   23.26  apply(simp add: o_def ctyping.intros)
    24.1 --- a/src/HOL/IMP/Sec_Typing.thy	Tue Sep 20 22:11:22 2011 +0200
    24.2 +++ b/src/HOL/IMP/Sec_Typing.thy	Wed Sep 21 00:12:36 2011 +0200
    24.3 @@ -30,7 +30,7 @@
    24.4  text{* An important property: anti-monotonicity. *}
    24.5  
    24.6  lemma anti_mono: "\<lbrakk> l \<turnstile> c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c"
    24.7 -apply(induct arbitrary: l' rule: sec_type.induct)
    24.8 +apply(induction arbitrary: l' rule: sec_type.induct)
    24.9  apply (metis sec_type.intros(1))
   24.10  apply (metis le_trans sec_type.intros(2))
   24.11  apply (metis sec_type.intros(3))
   24.12 @@ -39,7 +39,7 @@
   24.13  done
   24.14  
   24.15  lemma confinement: "\<lbrakk> (c,s) \<Rightarrow> t;  l \<turnstile> c \<rbrakk> \<Longrightarrow> s = t (< l)"
   24.16 -proof(induct rule: big_step_induct)
   24.17 +proof(induction rule: big_step_induct)
   24.18    case Skip thus ?case by simp
   24.19  next
   24.20    case Assign thus ?case by auto
   24.21 @@ -49,12 +49,12 @@
   24.22    case (IfTrue b s c1)
   24.23    hence "max (sec_bexp b) l \<turnstile> c1" by auto
   24.24    hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
   24.25 -  thus ?case using IfTrue.hyps by metis
   24.26 +  thus ?case using IfTrue.IH by metis
   24.27  next
   24.28    case (IfFalse b s c2)
   24.29    hence "max (sec_bexp b) l \<turnstile> c2" by auto
   24.30    hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
   24.31 -  thus ?case using IfFalse.hyps by metis
   24.32 +  thus ?case using IfFalse.IH by metis
   24.33  next
   24.34    case WhileFalse thus ?case by auto
   24.35  next
   24.36 @@ -68,7 +68,7 @@
   24.37  theorem noninterference:
   24.38    "\<lbrakk> (c,s) \<Rightarrow> s'; (c,t) \<Rightarrow> t';  0 \<turnstile> c;  s = t (\<le> l) \<rbrakk>
   24.39     \<Longrightarrow> s' = t' (\<le> l)"
   24.40 -proof(induct arbitrary: t t' rule: big_step_induct)
   24.41 +proof(induction arbitrary: t t' rule: big_step_induct)
   24.42    case Skip thus ?case by auto
   24.43  next
   24.44    case (Assign x a s)
   24.45 @@ -94,7 +94,7 @@
   24.46      assume "sec_bexp b \<le> l"
   24.47      hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
   24.48      hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
   24.49 -    with IfTrue.hyps(3) IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1`  anti_mono
   24.50 +    with IfTrue.IH IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1`  anti_mono
   24.51      show ?thesis by auto
   24.52    next
   24.53      assume "\<not> sec_bexp b \<le> l"
   24.54 @@ -115,7 +115,7 @@
   24.55      assume "sec_bexp b \<le> l"
   24.56      hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
   24.57      hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
   24.58 -    with IfFalse.hyps(3) IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
   24.59 +    with IfFalse.IH IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
   24.60      show ?thesis by auto
   24.61    next
   24.62      assume "\<not> sec_bexp b \<le> l"
   24.63 @@ -157,14 +157,14 @@
   24.64        using `bval b s1` by(simp add: bval_eq_if_eq_le)
   24.65      then obtain t2 where "(c,t1) \<Rightarrow> t2" "(?w,t2) \<Rightarrow> t3"
   24.66        using `(?w,t1) \<Rightarrow> t3` by auto
   24.67 -    from WhileTrue.hyps(5)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
   24.68 -      WhileTrue.hyps(3)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
   24.69 +    from WhileTrue.IH(2)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
   24.70 +      WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
   24.71          `s1 = t1 (\<le> l)`]]
   24.72      show ?thesis by simp
   24.73    next
   24.74      assume "\<not> sec_bexp b \<le> l"
   24.75      have 1: "sec_bexp b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
   24.76 -    from confinement[OF big_step.WhileTrue[OF WhileTrue(1,2,4)] 1] `\<not> sec_bexp b \<le> l`
   24.77 +    from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec_bexp b \<le> l`
   24.78      have "s1 = s3 (\<le> l)" by auto
   24.79      moreover
   24.80      from confinement[OF WhileTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
   24.81 @@ -196,7 +196,7 @@
   24.82    "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
   24.83  
   24.84  lemma sec_type_sec_type': "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
   24.85 -apply(induct rule: sec_type.induct)
   24.86 +apply(induction rule: sec_type.induct)
   24.87  apply (metis Skip')
   24.88  apply (metis Assign')
   24.89  apply (metis Semi')
   24.90 @@ -205,7 +205,7 @@
   24.91  
   24.92  
   24.93  lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
   24.94 -apply(induct rule: sec_type'.induct)
   24.95 +apply(induction rule: sec_type'.induct)
   24.96  apply (metis Skip)
   24.97  apply (metis Assign)
   24.98  apply (metis Semi)
   24.99 @@ -230,7 +230,7 @@
  24.100  
  24.101  
  24.102  lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"
  24.103 -apply(induct rule: sec_type2.induct)
  24.104 +apply(induction rule: sec_type2.induct)
  24.105  apply (metis Skip')
  24.106  apply (metis Assign' eq_imp_le)
  24.107  apply (metis Semi' anti_mono' min_max.inf.commute min_max.inf_le2)
  24.108 @@ -238,7 +238,7 @@
  24.109  by (metis While')
  24.110  
  24.111  lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
  24.112 -apply(induct rule: sec_type'.induct)
  24.113 +apply(induction rule: sec_type'.induct)
  24.114  apply (metis Skip2 le_refl)
  24.115  apply (metis Assign2)
  24.116  apply (metis Semi2 min_max.inf_greatest)
    25.1 --- a/src/HOL/IMP/Sec_TypingT.thy	Tue Sep 20 22:11:22 2011 +0200
    25.2 +++ b/src/HOL/IMP/Sec_TypingT.thy	Wed Sep 21 00:12:36 2011 +0200
    25.3 @@ -23,7 +23,7 @@
    25.4  
    25.5  
    25.6  lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c"
    25.7 -apply(induct arbitrary: l' rule: sec_type.induct)
    25.8 +apply(induction arbitrary: l' rule: sec_type.induct)
    25.9  apply (metis sec_type.intros(1))
   25.10  apply (metis le_trans sec_type.intros(2))
   25.11  apply (metis sec_type.intros(3))
   25.12 @@ -32,7 +32,7 @@
   25.13  
   25.14  
   25.15  lemma confinement: "(c,s) \<Rightarrow> t \<Longrightarrow> l \<turnstile> c \<Longrightarrow> s = t (< l)"
   25.16 -proof(induct rule: big_step_induct)
   25.17 +proof(induction rule: big_step_induct)
   25.18    case Skip thus ?case by simp
   25.19  next
   25.20    case Assign thus ?case by auto
   25.21 @@ -42,12 +42,12 @@
   25.22    case (IfTrue b s c1)
   25.23    hence "max (sec_bexp b) l \<turnstile> c1" by auto
   25.24    hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
   25.25 -  thus ?case using IfTrue.hyps by metis
   25.26 +  thus ?case using IfTrue.IH by metis
   25.27  next
   25.28    case (IfFalse b s c2)
   25.29    hence "max (sec_bexp b) l \<turnstile> c2" by auto
   25.30    hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
   25.31 -  thus ?case using IfFalse.hyps by metis
   25.32 +  thus ?case using IfFalse.IH by metis
   25.33  next
   25.34    case WhileFalse thus ?case by auto
   25.35  next
   25.36 @@ -57,7 +57,7 @@
   25.37  qed
   25.38  
   25.39  lemma termi_if_non0: "l \<turnstile> c \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists> t. (c,s) \<Rightarrow> t"
   25.40 -apply(induct arbitrary: s rule: sec_type.induct)
   25.41 +apply(induction arbitrary: s rule: sec_type.induct)
   25.42  apply (metis big_step.Skip)
   25.43  apply (metis big_step.Assign)
   25.44  apply (metis big_step.Semi)
   25.45 @@ -67,7 +67,7 @@
   25.46  
   25.47  theorem noninterference: "(c,s) \<Rightarrow> s' \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow>  s = t (\<le> l)
   25.48    \<Longrightarrow> \<exists> t'. (c,t) \<Rightarrow> t' \<and> s' = t' (\<le> l)"
   25.49 -proof(induct arbitrary: t rule: big_step_induct)
   25.50 +proof(induction arbitrary: t rule: big_step_induct)
   25.51    case Skip thus ?case by auto
   25.52  next
   25.53    case (Assign x a s)
   25.54 @@ -152,9 +152,9 @@
   25.55    let ?w = "WHILE b DO c"
   25.56    from `0 \<turnstile> ?w` have [simp]: "sec_bexp b = 0" by auto
   25.57    have "0 \<turnstile> c" using WhileTrue.prems(1) by auto
   25.58 -  from WhileTrue(3)[OF this WhileTrue.prems(2)]
   25.59 +  from WhileTrue.IH(1)[OF this WhileTrue.prems(2)]
   25.60    obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast
   25.61 -  from WhileTrue(5)[OF `0 \<turnstile> ?w` this(2)]
   25.62 +  from WhileTrue.IH(2)[OF `0 \<turnstile> ?w` this(2)]
   25.63    obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast
   25.64    from `bval b s` have "bval b t"
   25.65      using bval_eq_if_eq_le[OF `s = t (\<le>l)`] by auto
   25.66 @@ -185,7 +185,7 @@
   25.67    "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
   25.68  
   25.69  lemma "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
   25.70 -apply(induct rule: sec_type.induct)
   25.71 +apply(induction rule: sec_type.induct)
   25.72  apply (metis Skip')
   25.73  apply (metis Assign')
   25.74  apply (metis Semi')
   25.75 @@ -194,7 +194,7 @@
   25.76  
   25.77  
   25.78  lemma "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
   25.79 -apply(induct rule: sec_type'.induct)
   25.80 +apply(induction rule: sec_type'.induct)
   25.81  apply (metis Skip)
   25.82  apply (metis Assign)
   25.83  apply (metis Semi)
    26.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Tue Sep 20 22:11:22 2011 +0200
    26.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Wed Sep 21 00:12:36 2011 +0200
    26.3 @@ -83,10 +83,9 @@
    26.4           P s \<Longrightarrow> 
    26.5           d = WHILE b DO c \<Longrightarrow> 
    26.6           (WHILE b' DO c', s) \<Rightarrow> s'"  
    26.7 -proof (induct rule: big_step_induct)
    26.8 +proof (induction rule: big_step_induct)
    26.9    case (WhileTrue b s1 c s2 s3)
   26.10 -  note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
   26.11 -  
   26.12 +  note IH = WhileTrue.IH(2) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
   26.13    from WhileTrue.prems
   26.14    have "P \<Turnstile> b <\<sim>> b'" by simp
   26.15    with `bval b s1` `P s1`
    27.1 --- a/src/HOL/IMP/Small_Step.thy	Tue Sep 20 22:11:22 2011 +0200
    27.2 +++ b/src/HOL/IMP/Small_Step.thy	Wed Sep 21 00:12:36 2011 +0200
    27.3 @@ -71,7 +71,7 @@
    27.4  text{* A simple property: *}
    27.5  lemma deterministic:
    27.6    "cs \<rightarrow> cs' \<Longrightarrow> cs \<rightarrow> cs'' \<Longrightarrow> cs'' = cs'"
    27.7 -apply(induct arbitrary: cs'' rule: small_step.induct)
    27.8 +apply(induction arbitrary: cs'' rule: small_step.induct)
    27.9  apply blast+
   27.10  done
   27.11  
   27.12 @@ -79,7 +79,7 @@
   27.13  subsection "Equivalence with big-step semantics"
   27.14  
   27.15  lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
   27.16 -proof(induct rule: star_induct)
   27.17 +proof(induction rule: star_induct)
   27.18    case refl thus ?case by simp
   27.19  next
   27.20    case step
   27.21 @@ -98,7 +98,7 @@
   27.22  
   27.23  lemma big_to_small:
   27.24    "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
   27.25 -proof (induct rule: big_step.induct)
   27.26 +proof (induction rule: big_step.induct)
   27.27    fix s show "(SKIP,s) \<rightarrow>* (SKIP,s)" by simp
   27.28  next
   27.29    fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto
   27.30 @@ -140,7 +140,7 @@
   27.31  
   27.32  text{* Each case of the induction can be proved automatically: *}
   27.33  lemma  "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
   27.34 -proof (induct rule: big_step.induct)
   27.35 +proof (induction rule: big_step.induct)
   27.36    case Skip show ?case by blast
   27.37  next
   27.38    case Assign show ?case by blast
   27.39 @@ -161,13 +161,13 @@
   27.40  
   27.41  lemma small1_big_continue:
   27.42    "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
   27.43 -apply (induct arbitrary: t rule: small_step.induct)
   27.44 +apply (induction arbitrary: t rule: small_step.induct)
   27.45  apply auto
   27.46  done
   27.47  
   27.48  lemma small_big_continue:
   27.49    "cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
   27.50 -apply (induct rule: star.induct)
   27.51 +apply (induction rule: star.induct)
   27.52  apply (auto intro: small1_big_continue)
   27.53  done
   27.54  
   27.55 @@ -188,7 +188,7 @@
   27.56  
   27.57  lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP"
   27.58  apply(simp add: final_def)
   27.59 -apply(induct c)
   27.60 +apply(induction c)
   27.61  apply blast+
   27.62  done
   27.63  
    28.1 --- a/src/HOL/IMP/Star.thy	Tue Sep 20 22:11:22 2011 +0200
    28.2 +++ b/src/HOL/IMP/Star.thy	Wed Sep 21 00:12:36 2011 +0200
    28.3 @@ -9,7 +9,7 @@
    28.4  
    28.5  lemma star_trans:
    28.6    "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
    28.7 -proof(induct rule: star.induct)
    28.8 +proof(induction rule: star.induct)
    28.9    case refl thus ?case .
   28.10  next
   28.11    case step thus ?case by (metis star.step)
    29.1 --- a/src/HOL/IMP/Types.thy	Tue Sep 20 22:11:22 2011 +0200
    29.2 +++ b/src/HOL/IMP/Types.thy	Wed Sep 21 00:12:36 2011 +0200
    29.3 @@ -119,28 +119,28 @@
    29.4  
    29.5  lemma apreservation:
    29.6    "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>"
    29.7 -apply(induct arbitrary: v rule: atyping.induct)
    29.8 +apply(induction arbitrary: v rule: atyping.induct)
    29.9  apply (fastforce simp: styping_def)+
   29.10  done
   29.11  
   29.12  lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
   29.13 -proof(induct rule: atyping.induct)
   29.14 +proof(induction rule: atyping.induct)
   29.15    case (Plus_ty \<Gamma> a1 t a2)
   29.16    then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast
   29.17    show ?case
   29.18    proof (cases v1)
   29.19      case Iv
   29.20 -    with Plus_ty(1,3,5) v show ?thesis
   29.21 +    with Plus_ty v show ?thesis
   29.22        by(fastforce intro: taval.intros(4) dest!: apreservation)
   29.23    next
   29.24      case Rv
   29.25 -    with Plus_ty(1,3,5) v show ?thesis
   29.26 +    with Plus_ty v show ?thesis
   29.27        by(fastforce intro: taval.intros(5) dest!: apreservation)
   29.28    qed
   29.29  qed (auto intro: taval.intros)
   29.30  
   29.31  lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v"
   29.32 -proof(induct rule: btyping.induct)
   29.33 +proof(induction rule: btyping.induct)
   29.34    case (Less_ty \<Gamma> a1 t a2)
   29.35    then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2"
   29.36      by (metis aprogress)
   29.37 @@ -158,7 +158,7 @@
   29.38  
   29.39  theorem progress:
   29.40    "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
   29.41 -proof(induct rule: ctyping.induct)
   29.42 +proof(induction rule: ctyping.induct)
   29.43    case Skip_ty thus ?case by simp
   29.44  next
   29.45    case Assign_ty 
   29.46 @@ -182,7 +182,7 @@
   29.47  
   29.48  theorem styping_preservation:
   29.49    "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'"
   29.50 -proof(induct rule: small_step_induct)
   29.51 +proof(induction rule: small_step_induct)
   29.52    case Assign thus ?case
   29.53      by (auto simp: styping_def) (metis Assign(1,3) apreservation)
   29.54  qed auto
   29.55 @@ -197,7 +197,7 @@
   29.56  theorem type_sound:
   29.57    "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP
   29.58     \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
   29.59 -apply(induct rule:star_induct)
   29.60 +apply(induction rule:star_induct)
   29.61  apply (metis progress)
   29.62  by (metis styping_preservation ctyping_preservation)
   29.63  
    30.1 --- a/src/HOL/IMP/VC.thy	Tue Sep 20 22:11:22 2011 +0200
    30.2 +++ b/src/HOL/IMP/VC.thy	Wed Sep 21 00:12:36 2011 +0200
    30.3 @@ -49,14 +49,14 @@
    30.4  subsection "Soundness"
    30.5  
    30.6  lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} astrip c {Q}"
    30.7 -proof(induct c arbitrary: Q)
    30.8 +proof(induction c arbitrary: Q)
    30.9    case (Awhile b I c)
   30.10    show ?case
   30.11    proof(simp, rule While')
   30.12      from `\<forall>s. vc (Awhile b I c) Q s`
   30.13      have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
   30.14           pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all
   30.15 -    have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.hyps[OF vc])
   30.16 +    have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.IH[OF vc])
   30.17      with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} astrip c {I}"
   30.18        by(rule strengthen_pre)
   30.19      show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
   30.20 @@ -72,20 +72,20 @@
   30.21  
   30.22  lemma pre_mono:
   30.23    "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
   30.24 -proof (induct c arbitrary: P P' s)
   30.25 +proof (induction c arbitrary: P P' s)
   30.26    case Asemi thus ?case by simp metis
   30.27  qed simp_all
   30.28  
   30.29  lemma vc_mono:
   30.30    "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
   30.31 -proof(induct c arbitrary: P P')
   30.32 +proof(induction c arbitrary: P P')
   30.33    case Asemi thus ?case by simp (metis pre_mono)
   30.34  qed simp_all
   30.35  
   30.36  lemma vc_complete:
   30.37   "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. astrip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)"
   30.38    (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")
   30.39 -proof (induct rule: hoare.induct)
   30.40 +proof (induction rule: hoare.induct)
   30.41    case Skip
   30.42    show ?case (is "\<exists>ac. ?C ac")
   30.43    proof show "?C Askip" by simp qed
   30.44 @@ -95,8 +95,8 @@
   30.45    proof show "?C(Aassign x a)" by simp qed
   30.46  next
   30.47    case (Semi P c1 Q c2 R)
   30.48 -  from Semi.hyps obtain ac1 where ih1: "?G P c1 Q ac1" by blast
   30.49 -  from Semi.hyps obtain ac2 where ih2: "?G Q c2 R ac2" by blast
   30.50 +  from Semi.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
   30.51 +  from Semi.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
   30.52    show ?case (is "\<exists>ac. ?C ac")
   30.53    proof
   30.54      show "?C(Asemi ac1 ac2)"
   30.55 @@ -104,9 +104,9 @@
   30.56    qed
   30.57  next
   30.58    case (If P b c1 Q c2)
   30.59 -  from If.hyps obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
   30.60 +  from If.IH obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
   30.61      by blast
   30.62 -  from If.hyps obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
   30.63 +  from If.IH obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
   30.64      by blast
   30.65    show ?case (is "\<exists>ac. ?C ac")
   30.66    proof
   30.67 @@ -114,7 +114,7 @@
   30.68    qed
   30.69  next
   30.70    case (While P b c)
   30.71 -  from While.hyps obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
   30.72 +  from While.IH obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
   30.73    show ?case (is "\<exists>ac. ?C ac")
   30.74    proof show "?C(Awhile b P ac)" using ih by simp qed
   30.75  next
    31.1 --- a/src/HOL/IMP/Vars.thy	Tue Sep 20 22:11:22 2011 +0200
    31.2 +++ b/src/HOL/IMP/Vars.thy	Wed Sep 21 00:12:36 2011 +0200
    31.3 @@ -59,13 +59,13 @@
    31.4  
    31.5  lemma aval_eq_if_eq_on_vars[simp]:
    31.6    "s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
    31.7 -apply(induct a)
    31.8 +apply(induction a)
    31.9  apply simp_all
   31.10  done
   31.11  
   31.12  lemma bval_eq_if_eq_on_vars:
   31.13    "s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
   31.14 -proof(induct b)
   31.15 +proof(induction b)
   31.16    case (Less a1 a2)
   31.17    hence "aval a1 s\<^isub>1 = aval a1 s\<^isub>2" and "aval a2 s\<^isub>1 = aval a2 s\<^isub>2" by simp_all
   31.18    thus ?case by simp
    32.1 --- a/src/HOL/IsaMakefile	Tue Sep 20 22:11:22 2011 +0200
    32.2 +++ b/src/HOL/IsaMakefile	Wed Sep 21 00:12:36 2011 +0200
    32.3 @@ -145,6 +145,7 @@
    32.4    $(SRC)/Tools/eqsubst.ML \
    32.5    $(SRC)/Tools/induct.ML \
    32.6    $(SRC)/Tools/induct_tacs.ML \
    32.7 +  $(SRC)/Tools/induction.ML \
    32.8    $(SRC)/Tools/intuitionistic.ML \
    32.9    $(SRC)/Tools/misc_legacy.ML \
   32.10    $(SRC)/Tools/nbe.ML \
    33.1 --- a/src/Tools/induct.ML	Tue Sep 20 22:11:22 2011 +0200
    33.2 +++ b/src/Tools/induct.ML	Wed Sep 21 00:12:36 2011 +0200
    33.3 @@ -74,11 +74,21 @@
    33.4    val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
    33.5      thm list -> int -> cases_tactic
    33.6    val get_inductT: Proof.context -> term option list list -> thm list list
    33.7 +  type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
    33.8 +  val gen_induct_tac: (theory -> case_data * thm -> case_data * thm) ->
    33.9 +    Proof.context -> bool -> (binding option * (term * bool)) option list list ->
   33.10 +    (string * typ) list list -> term option list -> thm list option ->
   33.11 +    thm list -> int -> cases_tactic
   33.12    val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
   33.13      (string * typ) list list -> term option list -> thm list option ->
   33.14      thm list -> int -> cases_tactic
   33.15    val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
   33.16      thm list -> int -> cases_tactic
   33.17 +  val gen_induct_setup: binding ->
   33.18 +   (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
   33.19 +    (string * typ) list list -> term option list -> thm list option ->
   33.20 +    thm list -> int -> cases_tactic) ->
   33.21 +   theory -> theory
   33.22    val setup: theory -> theory
   33.23  end;
   33.24  
   33.25 @@ -721,7 +731,9 @@
   33.26  fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   33.27    | get_inductP _ _ = [];
   33.28  
   33.29 -fun induct_tac ctxt simp def_insts arbitrary taking opt_rule facts =
   33.30 +type case_data = (((string * string list) * string list) list * int)
   33.31 +
   33.32 +fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
   33.33    let
   33.34      val thy = Proof_Context.theory_of ctxt;
   33.35  
   33.36 @@ -734,6 +746,7 @@
   33.37            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
   33.38          |> maps (prep_inst ctxt align_right (atomize_term thy))
   33.39          |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
   33.40 +      |> mod_cases thy
   33.41        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
   33.42  
   33.43      val ruleq =
   33.44 @@ -791,7 +804,7 @@
   33.45         THEN_ALL_NEW rulify_tac)
   33.46    end;
   33.47  
   33.48 -
   33.49 +val induct_tac = gen_induct_tac (K I);
   33.50  
   33.51  (** coinduct method **)
   33.52  
   33.53 @@ -910,16 +923,18 @@
   33.54            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
   33.55      "case analysis on types or predicates/sets";
   33.56  
   33.57 -val induct_setup =
   33.58 -  Method.setup @{binding induct}
   33.59 +fun gen_induct_setup binding itac =
   33.60 +  Method.setup binding
   33.61      (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
   33.62        (arbitrary -- taking -- Scan.option induct_rule)) >>
   33.63        (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
   33.64          RAW_METHOD_CASES (fn facts =>
   33.65            Seq.DETERM
   33.66 -            (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
   33.67 +            (HEADGOAL (itac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
   33.68      "induction on types or predicates/sets";
   33.69  
   33.70 +val induct_setup = gen_induct_setup @{binding induct} induct_tac;
   33.71 +
   33.72  val coinduct_setup =
   33.73    Method.setup @{binding coinduct}
   33.74      (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
    34.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    34.2 +++ b/src/Tools/induction.ML	Wed Sep 21 00:12:36 2011 +0200
    34.3 @@ -0,0 +1,43 @@
    34.4 +signature INDUCTION =
    34.5 +sig
    34.6 +  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    34.7 +    (string * typ) list list -> term option list -> thm list option ->
    34.8 +    thm list -> int -> cases_tactic
    34.9 +  val setup: theory -> theory
   34.10 +end
   34.11 +
   34.12 +structure Induction: INDUCTION =
   34.13 +struct
   34.14 +
   34.15 +val ind_hypsN = "IH";
   34.16 +
   34.17 +fun preds_of t =
   34.18 + (case strip_comb t of
   34.19 +    (p as Var _, _) => [p]
   34.20 +  | (p as Free _, _) => [p]
   34.21 +  | (_, ts) => flat(map preds_of ts))
   34.22 +
   34.23 +fun name_hyps thy (arg as ((cases,consumes),th)) =
   34.24 +  if not(forall (null o #2 o #1) cases) then arg
   34.25 +  else
   34.26 +    let
   34.27 +      val (prems, concl) = Logic.strip_horn (prop_of th);
   34.28 +      val prems' = drop consumes prems;
   34.29 +      val ps = preds_of concl;
   34.30 +
   34.31 +      fun hname_of t =
   34.32 +        if exists_subterm (member (op =) ps) t
   34.33 +        then ind_hypsN else Rule_Cases.case_hypsN
   34.34 +
   34.35 +      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
   34.36 +      val n = Int.min (length hnamess, length cases) 
   34.37 +      val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
   34.38 +        (take n cases ~~ take n hnamess)
   34.39 +    in ((cases',consumes),th) end
   34.40 +
   34.41 +val induction_tac = Induct.gen_induct_tac name_hyps
   34.42 +
   34.43 +val setup = Induct.gen_induct_setup @{binding induction} induction_tac
   34.44 +
   34.45 +end
   34.46 +