# HG changeset patch # User paulson # Date 979312040 -3600 # Node ID b254d5ad6dd4f5f49222dc85f68d6b644fa6e74f # Parent 6417de2029b089dfb98bf8230d1bcd6952356e43 auto update diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Advanced/document/Partial.tex --- a/doc-src/TutorialI/Advanced/document/Partial.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Fri Jan 12 16:07:20 2001 +0100 @@ -34,7 +34,7 @@ matching.% \end{isamarkuptext}% % -\isamarkupsubsubsection{Guarded recursion% +\isamarkupsubsubsection{Guarded Recursion% } % \begin{isamarkuptext}% @@ -61,8 +61,8 @@ \noindent Of course we could also have defined \isa{divi\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}} to be some specific number, for example 0. The latter option is chosen for the predefined \isa{div} function, which -simplifies proofs at the expense of moving further away from the -standard mathematical divison function. +simplifies proofs at the expense of deviating from the +standard mathematical division function. As a more substantial example we consider the problem of searching a graph. For simplicity our graph is given by a function (\isa{f}) of @@ -135,13 +135,13 @@ \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}find{\isachardot}induct{\isacharparenright}\isanewline \isacommand{apply}\ simp\isanewline \isacommand{done}% -\isamarkupsubsubsection{The {\tt\slshape while} combinator% +\isamarkupsubsubsection{The {\tt\slshape while} Combinator% } % \begin{isamarkuptext}% If the recursive function happens to be tail recursive, its definition becomes a triviality if based on the predefined \isaindexbold{while} -combinator. The latter lives in the library theory +combinator. The latter lives in the Library theory \isa{While_Combinator}, which is not part of \isa{Main} but needs to be included explicitly among the ancestor theories. @@ -179,18 +179,18 @@ \ \ \ \ \ {\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}% \end{isabelle} \isa{P} needs to be true of the initial state \isa{s} and invariant under \isa{c} -(premises 1 and 2).The post-condition \isa{Q} must become true when -leaving the loop (premise 3). And each loop iteration must descend -along a well-founded relation \isa{r} (premises 4 and 5). +(premises 1 and~2). The post-condition \isa{Q} must become true when +leaving the loop (premise~3). And each loop iteration must descend +along a well-founded relation \isa{r} (premises 4 and~5). Let us now prove that \isa{find{\isadigit{2}}} does indeed find a fixed point. Instead of induction we apply the above while rule, suitably instantiated. Only the final premise of \isa{while{\isacharunderscore}rule} is left unproved by \isa{auto} but falls to \isa{simp}:% \end{isamarkuptext}% -\isacommand{lemma}\ lem{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharsemicolon}\ x{\isacharprime}\ {\isacharequal}\ f\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}y\ y{\isacharprime}{\isachardot}\isanewline -\ \ \ while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}y{\isacharprime}{\isacharparenright}\ {\isasymand}\isanewline -\ \ \ y{\isacharprime}\ {\isacharequal}\ y\ {\isasymand}\ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline +\isacommand{lemma}\ lem{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharsemicolon}\ x{\isacharprime}\ {\isacharequal}\ f\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \isanewline +\ \ \ {\isasymexists}y{\isachardot}\ while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}y{\isacharparenright}\ {\isasymand}\isanewline +\ \ \ \ \ \ \ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ P\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ f\ x{\isachardoublequote}\ \isakeyword{and}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ {\isacharequal}\ {\isachardoublequote}inv{\isacharunderscore}image\ {\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ fst{\isachardoublequote}\ \isakeyword{in}\ while{\isacharunderscore}rule{\isacharparenright}\isanewline \isacommand{apply}\ auto\isanewline @@ -214,8 +214,8 @@ program. This is in stark contrast to guarded recursion as introduced above which requires an explicit test \isa{x\ {\isasymin}\ dom\ f} in the function body. Unless \isa{dom} is trivial, this leads to a -definition which is either not at all executable or prohibitively -expensive. Thus, if you are aiming for an efficiently executable definition +definition that is impossible to execute (or prohibitively slow). +Thus, if you are aiming for an efficiently executable definition of a partial function, you are likely to need \isa{while}.% \end{isamarkuptext}% \end{isabellebody}% diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Advanced/document/WFrec.tex --- a/doc-src/TutorialI/Advanced/document/WFrec.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Fri Jan 12 16:07:20 2001 +0100 @@ -30,11 +30,11 @@ left-hand side of an equation and $r$ the argument of some recursive call on the corresponding right-hand side, induces a well-founded relation. For a systematic account of termination proofs via well-founded relations see, for -example, \cite{Baader-Nipkow}. +example, Baader and Nipkow~\cite{Baader-Nipkow}. Each \isacommand{recdef} definition should be accompanied (after the name of the function) by a well-founded relation on the argument type of the -function. The HOL library formalizes some of the most important +function. HOL formalizes some of the most important constructions of well-founded relations (see \S\ref{sec:Well-founded}). For example, \isa{measure\ f} is always well-founded, and the lexicographic product of two well-founded relations is again well-founded, which we relied @@ -50,7 +50,7 @@ {\isachardoublequote}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}% \begin{isamarkuptext}% Lexicographic products of measure functions already go a long -way. Furthermore you may embed some type in an +way. Furthermore, you may embed a type in an existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you will never have to prove well-foundedness of any relation composed solely of these building blocks. But of course the proof of diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Advanced/document/simp.tex --- a/doc-src/TutorialI/Advanced/document/simp.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/Advanced/document/simp.tex Fri Jan 12 16:07:20 2001 +0100 @@ -13,10 +13,10 @@ situation.% \end{isamarkuptext}% % -\isamarkupsubsection{Advanced features% +\isamarkupsubsection{Advanced Features% } % -\isamarkupsubsubsection{Congruence rules% +\isamarkupsubsubsection{Congruence Rules% } % \begin{isamarkuptext}% @@ -58,7 +58,7 @@ congruence rule for \isa{if}. Analogous rules control the evaluaton of \isa{case} expressions. -You can delare your own congruence rules with the attribute \isa{cong}, +You can declare your own congruence rules with the attribute \isa{cong}, either globally, in the usual manner, \begin{quote} \isacommand{declare} \textit{theorem-name} \isa{{\isacharbrackleft}cong{\isacharbrackright}} @@ -74,11 +74,12 @@ \begin{isabelle}% \ \ \ \ \ {\isasymlbrakk}P\ {\isacharequal}\ P{\isacharprime}{\isacharsemicolon}\ P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymand}\ Q{\isacharprime}{\isacharparenright}% \end{isabelle} -is occasionally useful but not a default rule; you have to use it explicitly. +\par\noindent +is occasionally useful but is not a default rule; you have to declare it explicitly. \end{warn}% \end{isamarkuptext}% % -\isamarkupsubsubsection{Permutative rewrite rules% +\isamarkupsubsubsection{Permutative Rewrite Rules% } % \begin{isamarkuptext}% @@ -120,11 +121,11 @@ f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \] Note that ordered rewriting for \isa{{\isacharplus}} and \isa{{\isacharasterisk}} on numbers is rarely -necessary because the builtin arithmetic capabilities often take care of -this.% +necessary because the built-in arithmetic prover often succeeds without +such hints.% \end{isamarkuptext}% % -\isamarkupsubsection{How it works% +\isamarkupsubsection{How It Works% } % \begin{isamarkuptext}% @@ -134,7 +135,7 @@ proved (again by simplification). Below we explain some special features of the rewriting process.% \end{isamarkuptext}% % -\isamarkupsubsubsection{Higher-order patterns% +\isamarkupsubsubsection{Higher-Order Patterns% } % \begin{isamarkuptext}% @@ -158,7 +159,7 @@ If the left-hand side is not a higher-order pattern, not all is lost and the simplifier will still try to apply the rule, but only if it -matches ``directly'', i.e.\ without much $\lambda$-calculus hocus +matches \emph{directly}, i.e.\ without much $\lambda$-calculus hocus pocus. For example, \isa{{\isacharquery}f\ {\isacharquery}x\ {\isasymin}\ range\ {\isacharquery}f\ {\isacharequal}\ True} rewrites \isa{g\ a\ {\isasymin}\ range\ g} to \isa{True}, but will fail to match \isa{g{\isacharparenleft}h\ b{\isacharparenright}\ {\isasymin}\ range{\isacharparenleft}{\isasymlambda}x{\isachardot}\ g{\isacharparenleft}h\ x{\isacharparenright}{\isacharparenright}}. However, you can @@ -166,25 +167,25 @@ is not a pattern) by adding new variables and conditions: \isa{{\isacharquery}y\ {\isacharequal}\ {\isacharquery}f\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}y\ {\isasymin}\ range\ {\isacharquery}f\ {\isacharequal}\ True} is fine as a conditional rewrite rule since conditions can be arbitrary terms. However, this trick is not a panacea because the newly -introduced conditions may be hard to prove, which has to take place +introduced conditions may be hard to prove, as they must be before the rule can actually be applied. -There is basically no restriction on the form of the right-hand +There is no restriction on the form of the right-hand sides. They may not contain extraneous term or type variables, though.% \end{isamarkuptext}% % -\isamarkupsubsubsection{The preprocessor% +\isamarkupsubsubsection{The Preprocessor% } % \begin{isamarkuptext}% \label{sec:simp-preprocessor} -When some theorem is declared a simplification rule, it need not be a +When a theorem is declared a simplification rule, it need not be a conditional equation already. The simplifier will turn it into a set of -conditional equations automatically. For example, given \isa{f\ x\ {\isacharequal}\ g\ x\ {\isasymand}\ h\ x\ {\isacharequal}\ k\ x} the simplifier will turn this into the two separate -simplifiction rules \isa{f\ x\ {\isacharequal}\ g\ x} and \isa{h\ x\ {\isacharequal}\ k\ x}. In +conditional equations automatically. For example, \isa{f\ x\ {\isacharequal}\ g\ x\ {\isasymand}\ h\ x\ {\isacharequal}\ k\ x} becomes the two separate +simplification rules \isa{f\ x\ {\isacharequal}\ g\ x} and \isa{h\ x\ {\isacharequal}\ k\ x}. In general, the input theorem is converted as follows: \begin{eqnarray} -\neg P &\mapsto& P = False \nonumber\\ +\neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\ P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\ P \land Q &\mapsto& P,\ Q \nonumber\\ \forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\ @@ -193,11 +194,12 @@ P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber \end{eqnarray} Once this conversion process is finished, all remaining non-equations -$P$ are turned into trivial equations $P = True$. -For example, the formula \begin{center}\isa{{\isacharparenleft}p\ {\isasymlongrightarrow}\ q\ {\isasymand}\ r{\isacharparenright}\ {\isasymand}\ s}\end{center} +$P$ are turned into trivial equations $P =\isa{True}$. +For example, the formula +\begin{center}\isa{{\isacharparenleft}p\ {\isasymlongrightarrow}\ t\ {\isacharequal}\ u\ {\isasymand}\ {\isasymnot}\ r{\isacharparenright}\ {\isasymand}\ s}\end{center} is converted into the three rules \begin{center} -\isa{p\ {\isasymLongrightarrow}\ q\ {\isacharequal}\ True},\quad \isa{p\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ True},\quad \isa{s\ {\isacharequal}\ True}. +\isa{p\ {\isasymLongrightarrow}\ t\ {\isacharequal}\ u},\quad \isa{p\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ False},\quad \isa{s\ {\isacharequal}\ True}. \end{center} \index{simplification rule|)} \index{simplification|)}% diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 12 16:07:20 2001 +0100 @@ -319,10 +319,10 @@ Let us close this section with a few words about the executability of our model checkers. It is clear that if all sets are finite, they can be represented as lists and the usual set operations are easily implemented. Only \isa{lfp} requires a little thought. -\REMARK{you had `in the library' but I assume you meant it was a -built in lemma. Do we give its name?} -Fortunately, Isabelle/HOL provides a theorem stating that -in the case of finite sets and a monotone \isa{F}, +Fortunately, the HOL Library% +\footnote{See theory \isa{While_Combinator_Example}.} +provides a theorem stating that +in the case of finite sets and a monotone function~\isa{F}, the value of \isa{lfp\ F} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until a fixed point is reached. It is actually possible to generate executable functional programs from HOL definitions, but that is beyond the scope of the tutorial.% diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/CTL/document/CTLind.tex --- a/doc-src/TutorialI/CTL/document/CTLind.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Fri Jan 12 16:07:20 2001 +0100 @@ -2,7 +2,7 @@ \begin{isabellebody}% \def\isabellecontext{CTLind}% % -\isamarkupsubsection{CTL revisited% +\isamarkupsubsection{CTL Revisited% } % \begin{isamarkuptext}% @@ -55,9 +55,8 @@ starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate the \isa{{\isasymforall}f{\isasymin}Paths\ t} in the induction hypothesis by the path starting with \isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term -expresses. That fact that this is a path starting with \isa{t} and that -the instantiated induction hypothesis implies the conclusion is shown by -simplification. +expresses. Simplification shows that this is a path starting with \isa{t} +and that the instantiated induction hypothesis implies the conclusion. Now we come to the key lemma. It says that if \isa{t} can be reached by a finite \isa{A}-avoiding path from \isa{s}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, @@ -67,10 +66,11 @@ \ \ {\isachardoublequote}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ t\ {\isasymin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent -The trick is not to induct on \isa{t\ {\isasymin}\ Avoid\ s\ A}, as already the base -case would be a problem, but to proceed by well-founded induction \isa{t}. Hence \isa{t\ {\isasymin}\ Avoid\ s\ A} needs to be brought into the conclusion as +The trick is not to induct on \isa{t\ {\isasymin}\ Avoid\ s\ A}, as even the base +case would be a problem, but to proceed by well-founded induction on~\isa{t}. Hence\hbox{ \isa{t\ {\isasymin}\ Avoid\ s\ A}} must be brought into the conclusion as well, which the directive \isa{rule{\isacharunderscore}format} undoes at the end (see below). -But induction with respect to which well-founded relation? The restriction +But induction with respect to which well-founded relation? The +one we want is the restriction of \isa{M} to \isa{Avoid\ s\ A}: \begin{isabelle}% \ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}% @@ -85,7 +85,19 @@ \ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}% \begin{isamarkuptxt}% \noindent -Now can assume additionally (induction hypothesis) that if \isa{t\ {\isasymnotin}\ A} +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ x\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}y{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline +\ \ \ \ wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\isanewline +\ \ \ \ \ \ \ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}% +\end{isabelle} +\REMARK{I put in this proof state but I wonder if readers will be able to +follow this proof. You could prove that your relation is WF in a +lemma beforehand, maybe omitting that proof.} +Now the induction hypothesis states that if \isa{t\ {\isasymnotin}\ A} then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. To prove the actual goal we unfold \isa{lfp} once. Now we have to prove that \isa{t} is in \isa{A} or all successors of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. If \isa{t} is not in \isa{A}, the second @@ -99,15 +111,14 @@ \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}% \begin{isamarkuptxt}% Having proved the main goal we return to the proof obligation that the above -relation is indeed well-founded. This is proved by contraposition: we assume -the relation is not well-founded. Thus there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem +relation is indeed well-founded. This is proved by contradiction: if +the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem \isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}: \begin{isabelle}% \ \ \ \ \ wf\ r\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ {\isacharparenleft}{\isasymexists}f{\isachardot}\ {\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharcomma}\ f\ i{\isacharparenright}\ {\isasymin}\ r{\isacharparenright}{\isacharparenright}% \end{isabelle} From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite -\isa{A}-avoiding path starting in \isa{s} follows, just as required for -the contraposition.% +\isa{A}-avoiding path starting in \isa{s} follows, contradiction.% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/CodeGen/document/CodeGen.tex --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Fri Jan 12 16:07:20 2001 +0100 @@ -2,7 +2,7 @@ \begin{isabellebody}% \def\isabellecontext{CodeGen}% % -\isamarkupsection{Case study: compiling expressions% +\isamarkupsection{Case Study: Compiling Expressions% } % \begin{isamarkuptext}% diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Fri Jan 12 16:07:20 2001 +0100 @@ -2,7 +2,7 @@ \begin{isabellebody}% \def\isabellecontext{Ifexpr}% % -\isamarkupsubsection{Case study: boolean expressions% +\isamarkupsubsection{Case Study: Boolean Expressions% } % \begin{isamarkuptext}% @@ -12,7 +12,7 @@ the constructs introduced above.% \end{isamarkuptext}% % -\isamarkupsubsubsection{How can we model boolean expressions?% +\isamarkupsubsubsection{How Can We Model Boolean Expressions?% } % \begin{isamarkuptext}% @@ -30,7 +30,7 @@ For example, the formula $P@0 \land \neg P@1$ is represented by the term \isa{And\ {\isacharparenleft}Var\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}}. -\subsubsection{What is the value of a boolean expression?} +\subsubsection{What is the Value of a Boolean Expression?} The value of a boolean expression depends on the value of its variables. Hence the function \isa{value} takes an additional parameter, an @@ -45,7 +45,7 @@ {\isachardoublequote}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent -\subsubsection{If-expressions} +\subsubsection{If-Expressions} An alternative and often more efficient (because in a certain sense canonical) representation are so-called \emph{If-expressions} built up @@ -64,8 +64,9 @@ {\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% -\subsubsection{Transformation into and of If-expressions} +\subsubsection{Transformation Into and of If-Expressions} +\REMARK{is this the title you wanted?} The type \isa{boolex} is close to the customary representation of logical formulae, whereas \isa{ifex} is designed for efficiency. It is easy to translate from \isa{boolex} into \isa{ifex}:% diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Fri Jan 12 16:07:20 2001 +0100 @@ -2,7 +2,7 @@ \begin{isabellebody}% \def\isabellecontext{AB}% % -\isamarkupsection{Case study: A context free grammar% +\isamarkupsection{Case Study: A Context Free Grammar% } % \begin{isamarkuptext}% @@ -11,19 +11,19 @@ which represent sets of strings. For example, the production $A \to B c$ is short for \[ w \in B \Longrightarrow wc \in A \] -This section demonstrates this idea with a standard example -\cite[p.\ 81]{HopcroftUllman}, a grammar for generating all words with an -equal number of $a$'s and $b$'s: +This section demonstrates this idea with an example +due to Hopcroft and Ullman, a grammar for generating all words with an +equal number of $a$'s and~$b$'s: \begin{eqnarray} S &\to& \epsilon \mid b A \mid a B \nonumber\\ A &\to& a S \mid b A A \nonumber\\ B &\to& b S \mid a B B \nonumber \end{eqnarray} -At the end we say a few words about the relationship of the formalization -and the text in the book~\cite[p.\ 81]{HopcroftUllman}. +At the end we say a few words about the relationship between +the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version. We start by fixing the alphabet, which consists only of \isa{a}'s -and \isa{b}'s:% +and~\isa{b}'s:% \end{isamarkuptext}% \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b% \begin{isamarkuptext}% @@ -31,21 +31,20 @@ For convenience we include the following easy lemmas as simplification rules:% \end{isamarkuptext}% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}x\ {\isasymnoteq}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline -\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}% +\isacommand{by}\ {\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharcomma}\ auto{\isacharparenright}% \begin{isamarkuptext}% \noindent Words over this alphabet are of type \isa{alfa\ list}, and -the three nonterminals are declare as sets of such words:% +the three nonterminals are declared as sets of such words:% \end{isamarkuptext}% \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline \ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}% \begin{isamarkuptext}% \noindent -The above productions are recast as a \emph{simultaneous} inductive +The productions above are recast as a \emph{mutual} inductive definition\index{inductive definition!simultaneous} -of \isa{S}, \isa{A} and \isa{B}:% +of \isa{S}, \isa{A} and~\isa{B}:% \end{isamarkuptext}% \isacommand{inductive}\ S\ A\ B\isanewline \isakeyword{intros}\isanewline @@ -60,8 +59,8 @@ \ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}% \begin{isamarkuptext}% \noindent -First we show that all words in \isa{S} contain the same number of \isa{a}'s and \isa{b}'s. Since the definition of \isa{S} is by simultaneous -induction, so is this proof: we show at the same time that all words in +First we show that all words in \isa{S} contain the same number of \isa{a}'s and \isa{b}'s. Since the definition of \isa{S} is by mutual +induction, so is the proof: we show at the same time that all words in \isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.% \end{isamarkuptext}% \isacommand{lemma}\ correctness{\isacharcolon}\isanewline @@ -71,24 +70,23 @@ \begin{isamarkuptxt}% \noindent These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x} -holds. Remember that on lists \isa{size} and \isa{size} are synonymous. +holds. Remember that on lists \isa{size} and \isa{length} are synonymous. The proof itself is by rule induction and afterwards automatic:% \end{isamarkuptxt}% -\isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}% +\isacommand{by}\ {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharcomma}\ auto{\isacharparenright}% \begin{isamarkuptext}% \noindent This may seem surprising at first, and is indeed an indication of the power of inductive definitions. But it is also quite straightforward. For example, consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$ -contain one more $a$ than $b$'s, then $bvw$ must again contain one more $a$ -than $b$'s. +contain one more $a$ than~$b$'s, then $bvw$ must again contain one more $a$ +than~$b$'s. As usual, the correctness of syntactic descriptions is easy, but completeness is hard: does \isa{S} contain \emph{all} words with an equal number of \isa{a}'s and \isa{b}'s? It turns out that this proof requires the -following little lemma: every string with two more \isa{a}'s than \isa{b}'s can be cut somehwere such that each half has one more \isa{a} than +following lemma: every string with two more \isa{a}'s than \isa{b}'s can be cut somewhere such that each half has one more \isa{a} than \isa{b}. This is best seen by imagining counting the difference between the number of \isa{a}'s and \isa{b}'s starting at the left end of the word. We start with 0 and end (at the right end) with 2. Since each move to the @@ -117,9 +115,9 @@ \noindent The lemma is a bit hard to read because of the coercion function \isa{{\isachardoublequote}int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns -a natural number, but \isa{{\isacharminus}} on \isa{nat} will do the wrong thing. +a natural number, but subtraction on type~\isa{nat} will do the wrong thing. Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of -length \isa{i} of \isa{xs}; below we als need \isa{drop\ i\ xs}, which +length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which is what remains after that prefix has been dropped from \isa{xs}. The proof is by induction on \isa{w}, with a trivial base case, and a not @@ -130,15 +128,15 @@ \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}% \begin{isamarkuptext}% -Finally we come to the above mentioned lemma about cutting a word with two -more elements of one sort than of the other sort into two halves:% +Finally we come to the above mentioned lemma about cutting in half a word with two +more elements of one sort than of the other sort:% \end{isamarkuptext}% \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline \ {\isachardoublequote}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline \ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent -This is proved by force with the help of the intermediate value theorem, +This is proved by \isa{force} with the help of the intermediate value theorem, instantiated appropriately and with its first premise disposed of by lemma \isa{step{\isadigit{1}}}:% \end{isamarkuptxt}% @@ -148,7 +146,7 @@ \noindent Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}. -The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:% +An easy lemma deals with the suffix \isa{drop\ i\ w}:% \end{isamarkuptext}% \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline @@ -158,8 +156,11 @@ \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}% \begin{isamarkuptext}% \noindent -Lemma \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}, \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs}, -which is generally useful, needs to be disabled for once. +In the proof, we have had to disable a normally useful lemma: +\begin{isabelle} +\isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs} +\rulename{append_take_drop_id} +\end{isabelle} To dispose of trivial cases automatically, the rules of the inductive definition are declared simplification rules:% @@ -170,8 +171,8 @@ This could have been done earlier but was not necessary so far. The completeness theorem tells us that if a word has the same number of -\isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly and -simultaneously for \isa{A} and \isa{B}:% +\isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly +for \isa{A} and \isa{B}:% \end{isamarkuptext}% \isacommand{theorem}\ completeness{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline @@ -201,7 +202,9 @@ \noindent Simplification disposes of the base case and leaves only two step cases to be proved: -if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \isa{length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}} then +if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \begin{isabelle}% +\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}% +\end{isabelle} then \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}. We only consider the first case in detail. @@ -216,9 +219,13 @@ \begin{isamarkuptxt}% \noindent This yields an index \isa{i\ {\isasymle}\ length\ v} such that -\isa{length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}}. +\begin{isabelle}% +\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}% +\end{isabelle} With the help of \isa{part{\isadigit{1}}} it follows that -\isa{length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}}.% +\begin{isabelle}% +\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}% +\end{isabelle}% \end{isamarkuptxt}% \ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline \ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}% @@ -242,7 +249,7 @@ Note that the variables \isa{n{\isadigit{1}}} and \isa{t} referred to in the substitution step above come from the derived theorem \isa{subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}}. -The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved completely analogously:% +The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved analogously:% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline @@ -255,9 +262,9 @@ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}% \begin{isamarkuptext}% -We conclude this section with a comparison of the above proof and the one -in the textbook \cite[p.\ 81]{HopcroftUllman}. For a start, the texbook -grammar, for no good reason, excludes the empty word, which complicates +We conclude this section with a comparison of our proof with +Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the texbook +grammar, for no good reason, excludes the empty word. That complicates matters just a little bit because we now have 8 instead of our 7 productions. More importantly, the proof itself is different: rather than separating the diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Inductive/document/Advanced.tex --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Fri Jan 12 16:07:20 2001 +0100 @@ -17,24 +17,17 @@ \isanewline \isacommand{lemma}\ gterms{\isacharunderscore}mono{\isacharcolon}\ {\isachardoublequote}F{\isasymsubseteq}G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G{\isachardoublequote}\isanewline \isacommand{apply}\ clarify\isanewline -\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isanewline +\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline +\ \ \ \ \ \ \ {\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ t\ {\isasymin}\ gterms\ G{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G% +\end{isabelle}% +\end{isamarkuptxt}% \isacommand{apply}\ blast\isanewline \isacommand{done}% \begin{isamarkuptext}% -The situation after induction - -proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{2}}\isanewline -\isanewline -goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline -F\ {\isasymsubseteq}\ G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G\isanewline -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline -\ \ \ \ \ \ \ {\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ t\ {\isasymin}\ gterms\ G{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline -\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G% -\end{isamarkuptext}% -% -\begin{isamarkuptext}% -We completely forgot about "rule inversion". - \begin{isabelle}% \ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% \end{isabelle} @@ -71,25 +64,20 @@ \end{isamarkuptext}% \isacommand{lemma}\ gterms{\isacharunderscore}IntI\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline \ \ \ \ \ {\isachardoublequote}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequote}\isanewline -\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isanewline +\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline +\ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline +\ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}% +\end{isabelle}% +\end{isamarkuptxt}% \isacommand{apply}\ blast\isanewline \isacommand{done}% \begin{isamarkuptext}% -Subgoal after induction. How would we cope without rule inversion? - -pr(latex xsymbols symbols) - -proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline -\isanewline -goal\ {\isacharparenleft}lemma\ gterms{\isacharunderscore}IntI{\isacharparenright}{\isacharcolon}\isanewline -t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}\isanewline -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline -\ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline -\ \ \ \ \ \ \ \ \ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline -\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}% -\end{isamarkuptext}% -% -\begin{isamarkuptext}% \begin{isabelle}% \ \ \ \ \ mono\ f\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymsubseteq}\ f\ A\ {\isasyminter}\ f\ B% \end{isabelle} @@ -126,50 +114,59 @@ \isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline \isanewline \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline -\isacommand{apply}\ clarify\isanewline -\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isanewline -\isacommand{apply}\ auto\isanewline -\isacommand{done}% -\begin{isamarkuptext}% -The situation after clarify (note the induction hypothesis!) - -pr(latex xsymbols symbols) - -proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{2}}\isanewline -\isanewline -goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline -well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\isanewline +\isacommand{apply}\ clarify% +\begin{isamarkuptxt}% +The situation after clarify +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymLongrightarrow}\isanewline +\ \ \ \ \ \ \ \ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% +\end{isabelle}% +\end{isamarkuptxt}% +\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}% +\begin{isamarkuptxt}% +note the induction hypothesis! +\begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline \ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline -\ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\isanewline +\ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% -\end{isamarkuptext}% +\end{isabelle}% +\end{isamarkuptxt}% +\isacommand{apply}\ auto\isanewline +\isacommand{done}\isanewline +\isanewline +\isanewline +\isanewline \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline -\isacommand{apply}\ clarify\isanewline -\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isanewline +\isacommand{apply}\ clarify% +\begin{isamarkuptxt}% +The situation after clarify +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymLongrightarrow}\isanewline +\ \ \ \ \ \ \ \ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% +\end{isabelle}% +\end{isamarkuptxt}% +\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}% +\begin{isamarkuptxt}% +note the induction hypothesis! +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline +\ \ \ \ \ \ \ {\isasymlbrakk}args\isanewline +\ \ \ \ \ \ \ \ {\isasymin}\ lists\isanewline +\ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ {\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% +\end{isabelle}% +\end{isamarkuptxt}% \isacommand{apply}\ auto\isanewline \isacommand{done}% \begin{isamarkuptext}% \begin{isabelle}% \ \ \ \ \ lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B% -\end{isabelle} -\rulename{lists_Int_eq} - -The situation after clarify (note the strange induction hypothesis!) - -pr(latex xsymbols symbols) - -proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{2}}\isanewline -\isanewline -goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline -well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\isanewline -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline -\ \ \ \ \ \ \ {\isasymlbrakk}args\isanewline -\ \ \ \ \ \ \ \ {\isasymin}\ lists\isanewline -\ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\ {\isacharbraceleft}u{\isachardot}\ u\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline -\ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline -\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% +\end{isabelle}% \end{isamarkuptext}% % \begin{isamarkuptext}% diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Inductive/document/Even.tex --- a/doc-src/TutorialI/Inductive/document/Even.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Fri Jan 12 16:07:20 2001 +0100 @@ -2,28 +2,16 @@ \begin{isabellebody}% \def\isabellecontext{Even}% \isanewline -\isacommand{theory}\ Even\ {\isacharequal}\ Main{\isacharcolon}% -\begin{isamarkuptext}% -We begin with a simple example: the set of even numbers. Obviously this -concept can be expressed already using the divides relation (dvd). We shall -prove below that the two formulations coincide. - -First, we declare the constant \isa{even} to be a set of natural numbers. -Then, an inductive declaration gives it the desired properties.% -\end{isamarkuptext}% +\isacommand{theory}\ Even\ {\isacharequal}\ Main{\isacharcolon}\isanewline +\isanewline +\isanewline \isacommand{consts}\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline \isacommand{inductive}\ even\isanewline \isakeyword{intros}\isanewline zero{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequote}\isanewline step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}% \begin{isamarkuptext}% -An inductive definition consists of introduction rules. The first one -above states that 0 is even; the second states that if $n$ is even, so is -$n+2$. Given this declaration, Isabelle generates a fixed point definition -for \isa{even} and proves many theorems about it. These theorems include the -introduction rules specified in the declaration, an elimination rule for case -analysis and an induction rule. We can refer to these theorems by -automatically-generated names: +An inductive definition consists of introduction rules. \begin{isabelle}% \ \ \ \ \ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even% @@ -36,126 +24,96 @@ \rulename{even.induct} Attributes can be given to the introduction rules. Here both rules are -specified as \isa{intro!}, which will cause them to be applied aggressively. -Obviously, regarding 0 as even is always safe. The second rule is also safe -because $n+2$ is even if and only if $n$ is even. We prove this equivalence -later.% -\end{isamarkuptext}% -% -\begin{isamarkuptext}% -Our first lemma states that numbers of the form $2\times k$ are even. -Introduction rules are used to show that given values belong to the inductive -set. Often, as here, the proof involves some other sort of induction.% +specified as \isa{intro!} + +Our first lemma states that numbers of the form $2\times k$ are even.% \end{isamarkuptext}% \isacommand{lemma}\ two{\isacharunderscore}times{\isacharunderscore}even{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharhash}{\isadigit{2}}{\isacharasterisk}k\ {\isasymin}\ even{\isachardoublequote}\isanewline -\isacommand{apply}\ {\isacharparenleft}induct\ {\isachardoublequote}k{\isachardoublequote}{\isacharparenright}\isanewline +\isacommand{apply}\ {\isacharparenleft}induct\ {\isachardoublequote}k{\isachardoublequote}{\isacharparenright}% +\begin{isamarkuptxt}% +The first step is induction on the natural number \isa{k}, which leaves +two subgoals: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ even% +\end{isabelle} +Here \isa{auto} simplifies both subgoals so that they match the introduction +rules, which then are applied automatically.% +\end{isamarkuptxt}% \ \isacommand{apply}\ auto\isanewline \isacommand{done}% \begin{isamarkuptext}% -The first step is induction on the natural number \isa{k}, which leaves -two subgoals: - -pr(latex xsymbols symbols); -proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline -\isanewline -goal\ {\isacharparenleft}lemma\ two{\isacharunderscore}times{\isacharunderscore}even{\isacharparenright}{\isacharcolon}\isanewline -{\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\isanewline -\ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ even - -Here \isa{auto} simplifies both subgoals so that they match the introduction -rules, which then are applied automatically.% -\end{isamarkuptext}% -% -\begin{isamarkuptext}% Our goal is to prove the equivalence between the traditional definition of even (using the divides relation) and our inductive definition. Half of this equivalence is trivial using the lemma just proved, whose \isa{intro!} attribute ensures it will be applied automatically.% \end{isamarkuptext}% \isacommand{lemma}\ dvd{\isacharunderscore}imp{\isacharunderscore}even{\isacharcolon}\ {\isachardoublequote}{\isacharhash}{\isadigit{2}}\ dvd\ n\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline -\isacommand{apply}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}\isanewline -\isacommand{done}% +\isacommand{by}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptext}% our first rule induction!% \end{isamarkuptext}% \isacommand{lemma}\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n{\isachardoublequote}\isanewline -\isacommand{apply}\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}\isanewline -\ \isacommand{apply}\ simp\isanewline -\isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}\isanewline -\isacommand{apply}\ clarify\isanewline -\isacommand{apply}\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}Suc\ k{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline -\isacommand{apply}\ simp\isanewline -\isacommand{done}% -\begin{isamarkuptext}% -proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline -\isanewline -goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline -n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline +\isacommand{apply}\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% +\begin{isamarkuptxt}% +\begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isacharhash}{\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright} - -proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{3}}\isanewline -\isanewline -goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline -n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k - -proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{4}}\isanewline -\isanewline -goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}{\isacharcolon}\isanewline -n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isacharhash}{\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% +\end{isabelle}% +\end{isamarkuptxt}% +\isacommand{apply}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k% +\end{isabelle}% +\end{isamarkuptxt}% +\isacommand{apply}\ clarify% +\begin{isamarkuptxt}% +\begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ ka% -\end{isamarkuptext}% -% +\end{isabelle}% +\end{isamarkuptxt}% +\isacommand{apply}\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}Suc\ k{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharcomma}\ simp{\isacharparenright}\isanewline +\isacommand{done}% \begin{isamarkuptext}% no iff-attribute because we don't always want to use it% \end{isamarkuptext}% \isacommand{theorem}\ even{\isacharunderscore}iff{\isacharunderscore}dvd{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}n\ {\isasymin}\ even{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}\ dvd\ n{\isacharparenright}{\isachardoublequote}\isanewline -\isacommand{apply}\ {\isacharparenleft}blast\ intro{\isacharcolon}\ dvd{\isacharunderscore}imp{\isacharunderscore}even\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}\isanewline -\isacommand{done}% +\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharcolon}\ dvd{\isacharunderscore}imp{\isacharunderscore}even\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}% \begin{isamarkuptext}% this result ISN'T inductive...% \end{isamarkuptext}% \isacommand{lemma}\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharcolon}\ {\isachardoublequote}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline -\isacommand{apply}\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}\isanewline -\isacommand{oops}% -\begin{isamarkuptext}% -proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline -\isanewline -goal\ {\isacharparenleft}lemma\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharparenright}{\isacharcolon}\isanewline -Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even\isanewline +\isacommand{apply}\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% +\begin{isamarkuptxt}% +\begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ even\isanewline \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even% -\end{isamarkuptext}% -% +\end{isabelle}% +\end{isamarkuptxt}% +\isacommand{oops}% \begin{isamarkuptext}% ...so we need an inductive lemma...% \end{isamarkuptext}% \isacommand{lemma}\ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n{\isacharminus}{\isacharhash}{\isadigit{2}}\ {\isasymin}\ even{\isachardoublequote}\isanewline -\isacommand{apply}\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}\isanewline +\isacommand{apply}\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even% +\end{isabelle}% +\end{isamarkuptxt}% \isacommand{apply}\ auto\isanewline \isacommand{done}% \begin{isamarkuptext}% -proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline -\isanewline -goal\ {\isacharparenleft}lemma\ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharparenright}{\isacharcolon}\isanewline -n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even\isanewline -\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even% -\end{isamarkuptext}% -% -\begin{isamarkuptext}% ...and prove it in a separate step% \end{isamarkuptext}% \isacommand{lemma}\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharcolon}\ {\isachardoublequote}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline -\isacommand{apply}\ {\isacharparenleft}drule\ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharparenright}\isanewline -\isacommand{apply}\ simp\isanewline -\isacommand{done}\isanewline +\isacommand{by}\ {\isacharparenleft}drule\ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharcomma}\ simp{\isacharparenright}\isanewline +\isanewline \isanewline \isacommand{lemma}\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymin}\ even{\isacharparenright}{\isachardoublequote}\isanewline -\isacommand{apply}\ {\isacharparenleft}blast\ dest{\isacharcolon}\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharparenright}\isanewline -\isacommand{done}\isanewline +\isacommand{by}\ {\isacharparenleft}blast\ dest{\isacharcolon}\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharparenright}\isanewline \isanewline \isacommand{end}\isanewline \isanewline diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Inductive/document/Mutual.tex --- a/doc-src/TutorialI/Inductive/document/Mutual.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Fri Jan 12 16:07:20 2001 +0100 @@ -2,7 +2,7 @@ \begin{isabellebody}% \def\isabellecontext{Mutual}% % -\isamarkupsubsection{Mutually inductive definitions% +\isamarkupsubsection{Mutually Inductive Definitions% } % \begin{isamarkuptext}% diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Inductive/document/Star.tex --- a/doc-src/TutorialI/Inductive/document/Star.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Fri Jan 12 16:07:20 2001 +0100 @@ -2,14 +2,16 @@ \begin{isabellebody}% \def\isabellecontext{Star}% % -\isamarkupsection{The reflexive transitive closure% +\isamarkupsection{The Reflexive Transitive Closure% } % \begin{isamarkuptext}% \label{sec:rtc} -Many inductive definitions define proper relations rather than merely set -like \isa{even}. A perfect example is the -reflexive transitive closure of a relation. This concept was already +An inductive definition may accept parameters, so it can express +functions that yield sets. +Relations too can be defined inductively, since they are just sets of pairs. +A perfect example is the function that maps a relation to its +reflexive transitive closure. This concept was already introduced in \S\ref{sec:Relations}, where the operator \isa{{\isacharcircum}{\isacharasterisk}} was defined as a least fixed point because inductive definitions were not yet available. But now they are:% @@ -32,9 +34,9 @@ The above definition of the concept of reflexive transitive closure may be sufficiently intuitive but it is certainly not the only possible one: -for a start, it does not even mention transitivity explicitly. +for a start, it does not even mention transitivity. The rest of this section is devoted to proving that it is equivalent to -the ``standard'' definition. We start with a simple lemma:% +the standard definition. We start with a simple lemma:% \end{isamarkuptext}% \isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharcolon}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline \isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}% @@ -45,7 +47,7 @@ danger of killing the automatic tactics because \isa{r{\isacharasterisk}} occurs only in the conclusion and not in the premise. Thus some proofs that would otherwise need \isa{rtc{\isacharunderscore}step} can now be found automatically. The proof also -shows that \isa{blast} is quite able to handle \isa{rtc{\isacharunderscore}step}. But +shows that \isa{blast} is able to handle \isa{rtc{\isacharunderscore}step}. But some of the other automatic tactics are more sensitive, and even \isa{blast} can be lead astray in the presence of large numbers of rules. To prove transitivity, we need rule induction, i.e.\ theorem @@ -149,8 +151,9 @@ So why did we start with the first definition? Because it is simpler. It contains only two rules, and the single step rule is simpler than transitivity. As a consequence, \isa{rtc{\isachardot}induct} is simpler than -\isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough, we should -certainly pick the simplest induction schema available for any concept. +\isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough +anyway, we should +certainly pick the simplest induction schema available. Hence \isa{rtc} is the definition of choice. \begin{exercise}\label{ex:converse-rtc-step} diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Fri Jan 12 16:05:12 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Fri Jan 12 16:07:20 2001 +0100 @@ -12,21 +12,22 @@ with an extended example of induction (\S\ref{sec:CTL-revisited}).% \end{isamarkuptext}% % -\isamarkupsubsection{Massaging the proposition% +\isamarkupsubsection{Massaging the Proposition% } % \begin{isamarkuptext}% \label{sec:ind-var-in-prems} -So far we have assumed that the theorem we want to prove is already in a form -that is amenable to induction, but this is not always the case:% +Often we have assumed that the theorem we want to prove is already in a form +that is amenable to induction, but sometimes it isn't. +Here is an example. +Since \isa{hd} and \isa{last} return the first and last element of a +non-empty list, this lemma looks easy to prove:% \end{isamarkuptext}% \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}% \begin{isamarkuptxt}% \noindent -(where \isa{hd} and \isa{last} return the first and last element of a -non-empty list) -produces the warning +But induction produces the warning \begin{quote}\tt Induction variable occurs also among premises! \end{quote} @@ -34,74 +35,52 @@ \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}% \end{isabelle} -which, after simplification, becomes +After simplification, it becomes \begin{isabelle} \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ [] \end{isabelle} We cannot prove this equality because we do not know what \isa{hd} and \isa{last} return when applied to \isa{{\isacharbrackleft}{\isacharbrackright}}. -The point is that we have violated the above warning. Because the induction -formula is only the conclusion, the occurrence of \isa{xs} in the premises is -not modified by induction. Thus the case that should have been trivial +We should not have ignored the warning. Because the induction +formula is only the conclusion, induction does not affect the occurrence of \isa{xs} in the premises. +Thus the case that should have been trivial becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar heuristic applies to rule inductions; see \S\ref{sec:rtc}.} \begin{quote} \emph{Pull all occurrences of the induction variable into the conclusion using \isa{{\isasymlongrightarrow}}.} \end{quote} -This means we should prove% +Thus we should state the lemma as an ordinary +implication~(\isa{{\isasymlongrightarrow}}), letting +\isa{rule{\isacharunderscore}format} (\S\ref{sec:forward}) convert the +result to the usual \isa{{\isasymLongrightarrow}} form:% \end{isamarkuptxt}% -\isacommand{lemma}\ hd{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}% +\isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}% \begin{isamarkuptxt}% \noindent -This time, induction leaves us with the following base case +This time, induction leaves us with a trivial base case: \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}% \end{isabelle} -which is trivial, and \isa{auto} finishes the whole proof. - -If \isa{hd{\isacharunderscore}rev} is meant to be a simplification rule, you are -done. But if you really need the \isa{{\isasymLongrightarrow}}-version of -\isa{hd{\isacharunderscore}rev}, for example because you want to apply it as an -introduction rule, you need to derive it separately, by combining it with -modus ponens:% +And \isa{auto} completes the proof.% \end{isamarkuptxt}% -\isacommand{lemmas}\ hd{\isacharunderscore}revI\ {\isacharequal}\ hd{\isacharunderscore}rev{\isacharbrackleft}THEN\ mp{\isacharbrackright}% +% \begin{isamarkuptext}% -\noindent -which yields the lemma we originally set out to prove. - -In case there are multiple premises $A@1$, \dots, $A@n$ containing the +If there are multiple premises $A@1$, \dots, $A@n$ containing the induction variable, you should turn the conclusion $C$ into \[ A@1 \longrightarrow \cdots A@n \longrightarrow C \] (see the remark?? in \S\ref{??}). Additionally, you may also have to universally quantify some other variables, -which can yield a fairly complex conclusion. +which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format} +can remove any number of occurrences of \isa{{\isasymforall}} and +\isa{{\isasymlongrightarrow}}. + Here is a simple example (which is proved by \isa{blast}):% \end{isamarkuptext}% -\isacommand{lemma}\ simple{\isacharcolon}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymand}\ A\ y{\isachardoublequote}% -\begin{isamarkuptext}% -\noindent -You can get the desired lemma by explicit -application of modus ponens and \isa{spec}:% -\end{isamarkuptext}% -\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}THEN\ spec{\isacharcomma}\ THEN\ mp{\isacharcomma}\ THEN\ mp{\isacharbrackright}% +\isacommand{lemma}\ simple{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymand}\ A\ y{\isachardoublequote}% \begin{isamarkuptext}% -\noindent -or the wholesale stripping of \isa{{\isasymforall}} and -\isa{{\isasymlongrightarrow}} in the conclusion via \isa{rule{\isacharunderscore}format}% -\end{isamarkuptext}% -\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}% -\begin{isamarkuptext}% -\noindent -yielding \isa{{\isasymlbrakk}A\ y{\isacharsemicolon}\ B\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}. -You can go one step further and include these derivations already in the -statement of your original lemma, thus avoiding the intermediate step:% -\end{isamarkuptext}% -\isacommand{lemma}\ myrule{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymand}\ A\ y{\isachardoublequote}% -\begin{isamarkuptext}% -\bigskip +\medskip A second reason why your proposition may not be amenable to induction is that you want to induct on a whole term, rather than an individual variable. In @@ -124,21 +103,21 @@ the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above.% \end{isamarkuptext}% % -\isamarkupsubsection{Beyond structural and recursion induction% +\isamarkupsubsection{Beyond Structural and Recursion Induction% } % \begin{isamarkuptext}% \label{sec:complete-ind} -So far, inductive proofs where by structural induction for +So far, inductive proofs were by structural induction for primitive recursive functions and recursion induction for total recursive functions. But sometimes structural induction is awkward and there is no -recursive function in sight either that could furnish a more appropriate -induction schema. In such cases some existing standard induction schema can +recursive function that could furnish a more appropriate +induction schema. In such cases a general-purpose induction schema can be helpful. We show how to apply such induction schemas by an example. Structural induction on \isa{nat} is -usually known as ``mathematical induction''. There is also ``complete -induction'', where you must prove $P(n)$ under the assumption that $P(m)$ +usually known as mathematical induction. There is also \emph{complete} +induction, where you must prove $P(n)$ under the assumption that $P(m)$ holds for all $m