doc-src/TutorialI/Misc/AdvancedInd.thy

 
 lemmas myrule = simple[THEN spec, THEN mp, THEN mp];
 
 text{*\noindent
 or the wholesale stripping of @{text"\<forall>"} and
-@{text"\<longrightarrow>"} in the conclusion via @{text"rulify"} 
-*};
-
-lemmas myrule = simple[rulify];
+@{text"\<longrightarrow>"} in the conclusion via @{text"rulified"} 
+*};
+
+lemmas myrule = simple[rulified];
 
 text{*\noindent
 yielding @{thm"myrule"[no_vars]}.
 You can go one step further and include these derivations already in the
 statement of your original lemma, thus avoiding the intermediate step:
 *};
 
-lemma myrule[rulify]:  "\\<forall>y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma myrule[rulified]:  "\\<forall>y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y";
 (*<*)
 by blast;
 (*>*)
 
 text{*

 be helpful. We show how to apply such induction schemas by an example.
 
 Structural induction on @{typ"nat"} is
 usually known as ``mathematical induction''. There is also ``complete
 induction'', where you must prove $P(n)$ under the assumption that $P(m)$
-holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]less_induct}:
-@{thm[display]"less_induct"[no_vars]}
+holds for all $m<n$. In Isabelle, this is the theorem @{thm [source] nat_less_induct}:
+@{thm[display] nat_less_induct [no_vars]}
 Here is an example of its application.
 *};
 
 consts f :: "nat => nat";
 axioms f_ax: "f(f(n)) < f(Suc(n))";

 *};
 
 lemma f_incr_lem: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
 
 txt{*\noindent
-To perform induction on @{term"k"} using @{thm[source]less_induct}, we use the same
+To perform induction on @{term"k"} using @{thm [source] nat_less_induct}, we use the same
 general induction method as for recursion induction (see
 \S\ref{sec:recdef-induction}):
 *};
 
-apply(induct_tac k rule:less_induct);
+apply(induct_tac k rule: nat_less_induct);
 (*<*)
 apply(rule allI);
 apply(case_tac i);
  apply(simp);
 (*>*)

 \ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i});\ \mbox{i}\ =\ Suc\ \mbox{nat}{\isasymrbrakk}\isanewline
 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
 \end{isabelle}
 *};
 
-by(blast intro!: f_ax Suc_leI intro:le_less_trans);
+by(blast intro!: f_ax Suc_leI intro: le_less_trans);
 
 text{*\noindent
 It is not surprising if you find the last step puzzling.
 The proof goes like this (writing @{term"j"} instead of @{typ"nat"}).
 Since @{prop"i = Suc j"} it suffices to show

 proofs.
 
 We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}:
 *};
 
-lemmas f_incr = f_incr_lem[rulify, OF refl];
+lemmas f_incr = f_incr_lem[rulified, OF refl];
 
 text{*\noindent
 The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. Again,
 we could have included this derivation in the original statement of the lemma:
 *};
 
-lemma f_incr[rulify, OF refl]: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
+lemma f_incr[rulified, OF refl]: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
 (*<*)oops;(*>*)
 
 text{*
 \begin{exercise}
 From the above axiom and lemma for @{term"f"} show that @{term"f"} is the

 subsection{*Derivation of new induction schemas*};
 
 text{*\label{sec:derive-ind}
 Induction schemas are ordinary theorems and you can derive new ones
 whenever you wish.  This section shows you how to, using the example
-of @{thm[source]less_induct}. Assume we only have structural induction
+of @{thm [source] nat_less_induct}. Assume we only have structural induction
 available for @{typ"nat"} and want to derive complete induction. This
 requires us to generalize the statement first:
 *};
 
 lemma induct_lem: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) \\<Longrightarrow> \\<forall>m<n. P m";

 text{*\noindent
 The elimination rule @{thm[source]less_SucE} expresses the case distinction:
 @{thm[display]"less_SucE"[no_vars]}
 
 Now it is straightforward to derive the original version of
-@{thm[source]less_induct} by manipulting the conclusion of the above lemma:
+@{thm [source] nat_less_induct} by manipulting the conclusion of the above lemma:
 instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and
 remove the trivial condition @{prop"n < Sc n"}. Fortunately, this
 happens automatically when we add the lemma as a new premise to the
 desired goal:
 *};
 
-theorem less_induct: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) \\<Longrightarrow> P n";
+theorem nat_less_induct: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) \\<Longrightarrow> P n";
 by(insert induct_lem, blast);
 
 text{*\noindent
 Finally we should mention that HOL already provides the mother of all
 inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):
 @{thm[display]"wf_induct"[no_vars]}
 where @{term"wf r"} means that the relation @{term"r"} is wellfounded.
-For example @{thm[source]less_induct} is the special case where @{term"r"} is
+For example @{thm [source] nat_less_induct} is the special case where @{term"r"} is
 @{text"<"} on @{typ"nat"}. For details see the library.
 *};
 
 (*<*)
 end