author wenzelm Mon, 23 Jun 2008 15:26:47 +0200 changeset 27318 5cd16e4df9c2 parent 27317 7f4ee574f29c child 27319 6584901d694c
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]}