induct_tac: rule is inferred from types;

--- a/doc-src/TutorialI/Datatype/ABexpr.thy	Sun Jun 22 23:08:32 2008 +0200
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Mon Jun 23 15:26:47 2008 +0200
@@ -93,10 +93,9 @@
 
 lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
         evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
-apply(induct_tac a and b rule: aexp_bexp.induct);
+apply(induct_tac a and b);
 
-txt{*\noindent Unfortunately, induction needs to be told explicitly which induction rule to use (via @{text"rule:"}).
-The resulting 8 goals (one for each constructor) are proved in one fell swoop:
+txt{*\noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:
 *}
 
 apply simp_all;
@@ -108,7 +107,7 @@
 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
 where each variable $x@i$ is of type $\tau@i$. Induction is started by
 \begin{isabelle}
-\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$ @{text"rule:"} $\tau@1$@{text"_"}\dots@{text"_"}$\tau@n$@{text".induct)"}
+\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text ")"}
 \end{isabelle}
 
 \begin{exercise}
@@ -138,7 +137,7 @@
 
 lemma " evala (norma a) env = evala a env 
       \<and> (\<forall> t e. evala (normb b t e) env = evala (IF b t e) env)"
-apply (induct_tac a and b rule: aexp_bexp.induct)
+apply (induct_tac a and b)
 apply (simp_all)
 done
 
@@ -156,7 +155,7 @@
 
 lemma "normala (norma (a::'a aexp)) \<and>
        (\<forall> (t::'a aexp) e. (normala t \<and> normala e) \<longrightarrow> normala (normb b t e))"
-apply (induct_tac a and b rule: aexp_bexp.induct)
+apply (induct_tac a and b)
 apply (auto)
 done
 

--- a/doc-src/TutorialI/Datatype/Nested.thy	Sun Jun 22 23:08:32 2008 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Mon Jun 23 15:26:47 2008 +0200
@@ -67,7 +67,7 @@
 
 lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst  Var t  = (t ::('v,'f)term)  \<and>
                   substs Var ts = (ts::('v,'f)term list)";
-apply(induct_tac t and ts rule: term.induct, simp_all);
+apply(induct_tac t and ts, simp_all);
 done
 
 text{*\noindent
@@ -105,7 +105,7 @@
 (* Exercise 1: *)
 lemma "subst  ((subst f) \<circ> g) t  = subst  f (subst g t) \<and>
        substs ((subst f) \<circ> g) ts = substs f (substs g ts)"
-apply (induct_tac t and ts rule: term.induct)
+apply (induct_tac t and ts)
 apply (simp_all)
 done
 
@@ -126,7 +126,7 @@
 
 lemma "trev (trev t) = (t::('v,'f)term) \<and> 
        trevs (trevs ts) = (ts::('v,'f)term list)"
-apply (induct_tac t and ts rule: term.induct, simp_all)
+apply (induct_tac t and ts, simp_all)
 done
 (*>*)
 

--- a/doc-src/TutorialI/Types/Typedefs.thy	Sun Jun 22 23:08:32 2008 +0200
+++ b/doc-src/TutorialI/Types/Typedefs.thy	Mon Jun 23 15:26:47 2008 +0200
@@ -189,9 +189,9 @@
 
 lemma three_cases: "\<lbrakk> P A; P B; P C \<rbrakk> \<Longrightarrow> P x"
 
-txt{*\noindent Again this follows easily from a pre-proved general theorem:*}
+txt{*\noindent Again this follows easily using the induction principle stemming from the type definition:*}
 
-apply(induct_tac x rule: Abs_three_induct)
+apply(induct_tac x)
 
 txt{*
 @{subgoals[display,indent=0]}