--- 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}%
--- 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
--- 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|)}%
--- 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.%
--- 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
--- 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}%
--- 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}:%
--- 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
--- 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}%
--- 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
--- 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}%
--- 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}
--- 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<n$. In Isabelle, this is the theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}:
\begin{isabelle}%
\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
@@ -149,11 +128,7 @@
\isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-From the above axiom\footnote{In general, the use of axioms is strongly
-discouraged, because of the danger of inconsistencies. The above axiom does
-not introduce an inconsistency because, for example, the identity function
-satisfies it.}
-for \isa{f} it follows that \isa{n\ {\isasymle}\ f\ n}, which can
+The axiom for \isa{f} implies \isa{n\ {\isasymle}\ f\ n}, which can
be proved by induction on \isa{f\ n}. Following the recipe outlined
above, we have to phrase the proposition as follows to allow induction:%
\end{isamarkuptext}%
@@ -189,14 +164,23 @@
\isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-It is not surprising if you find the last step puzzling.
+If you find the last step puzzling, here are the
+two other lemmas used above:
+\begin{isabelle}
+\isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
+\rulename{Suc_leI}\isanewline
+\isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}
+\rulename{le_less_trans}
+\end{isabelle}
+%
The proof goes like this (writing \isa{j} instead of \isa{nat}).
Since \isa{i\ {\isacharequal}\ Suc\ j} it suffices to show
-\isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (by \isa{Suc{\isacharunderscore}leI}: \isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}). This is
+\hbox{\isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}},
+by \isa{Suc{\isacharunderscore}leI}\@. This is
proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}
-(1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} (by the induction hypothesis).
-Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by transitivity
-(\isa{le{\isacharunderscore}less{\isacharunderscore}trans}: \isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}).
+(1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} by the induction hypothesis.
+Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by the transitivity
+rule \isa{le{\isacharunderscore}less{\isacharunderscore}trans}.
Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j}
which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by
\isa{le{\isacharunderscore}less{\isacharunderscore}trans}).
@@ -204,7 +188,7 @@
This last step shows both the power and the danger of automatic proofs: they
will usually not tell you how the proof goes, because it can be very hard to
translate the internal proof into a human-readable format. Therefore
-\S\ref{sec:part2?} introduces a language for writing readable yet concise
+Chapter~\ref{sec:part2?} introduces a language for writing readable
proofs.
We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr}:%
@@ -212,16 +196,22 @@
\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%
\begin{isamarkuptext}%
\noindent
-The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. Again,
-we could have included this derivation in the original statement of the lemma:%
+The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}.
+We could have included this derivation in the original statement of the lemma:%
\end{isamarkuptext}%
\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
\begin{isamarkuptext}%
-\begin{exercise}
-From the above axiom and lemma for \isa{f} show that \isa{f} is the
-identity.
-\end{exercise}
+\begin{warn}
+We discourage the use of axioms because of the danger of
+inconsistencies. Axiom \isa{f{\isacharunderscore}ax} does
+not introduce an inconsistency because, for example, the identity function
+satisfies it. Axioms can be useful in exploratory developments, say when
+you assume some well-known theorems so that you can quickly demonstrate some
+point about methodology. If your example turns into a substantial proof
+development, you should replace the axioms by proofs.
+\end{warn}
+\bigskip
In general, \isa{induct{\isacharunderscore}tac} can be applied with any rule $r$
whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
format is
@@ -240,10 +230,15 @@
which case the application is
\begin{quote}
\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{and} \dots\ \isa{and} $z@1 \dots z@m$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
-\end{quote}%
+\end{quote}
+
+\begin{exercise}
+From the axiom and lemma for \isa{f}, show that \isa{f} is the
+identity function.
+\end{exercise}%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Derivation of new induction schemas%
+\isamarkupsubsection{Derivation of New Induction Schemas%
}
%
\begin{isamarkuptext}%
@@ -266,7 +261,8 @@
\isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}less{\isacharunderscore}SucE{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
+The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction
+mentioned above:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
\end{isabelle}
@@ -283,9 +279,9 @@
\begin{isamarkuptext}%
Finally we should remind the reader that HOL already provides the mother of
all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For
-example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and derived) as
+example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is
a special case of \isa{wf{\isacharunderscore}induct} where \isa{r} is \isa{{\isacharless}} on
-\isa{nat}. The details can be found in the HOL library.%
+\isa{nat}. The details can be found in theory \isa{Wellfounded_Recursion}.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Fri Jan 12 16:07:20 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{Itrev}%
%
-\isamarkupsection{Induction heuristics%
+\isamarkupsection{Induction Heuristics%
}
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Fri Jan 12 16:07:20 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{case{\isacharunderscore}exprs}%
%
-\isamarkupsubsection{Case expressions%
+\isamarkupsubsection{Case Expressions%
}
%
\begin{isamarkuptext}%
@@ -49,7 +49,7 @@
indicate their scope%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Structural induction and case distinction%
+\isamarkupsubsection{Structural Induction and Case Distinction%
}
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 12 16:07:20 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{simp}%
%
-\isamarkupsubsubsection{Simplification rules%
+\isamarkupsubsubsection{Simplification Rules%
}
%
\begin{isamarkuptext}%
@@ -40,7 +40,7 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{The simplification method%
+\isamarkupsubsubsection{The Simplification Method%
}
%
\begin{isamarkuptext}%
@@ -57,7 +57,7 @@
Note that \isa{simp} fails if nothing changes.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Adding and deleting simplification rules%
+\isamarkupsubsubsection{Adding and Deleting Simplification Rules%
}
%
\begin{isamarkuptext}%
@@ -126,7 +126,7 @@
other arguments.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Rewriting with definitions%
+\isamarkupsubsubsection{Rewriting with Definitions%
}
%
\begin{isamarkuptext}%
@@ -175,7 +175,7 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Simplifying let-expressions%
+\isamarkupsubsubsection{Simplifying Let-Expressions%
}
%
\begin{isamarkuptext}%
@@ -195,7 +195,7 @@
default:%
\end{isamarkuptext}%
\isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
-\isamarkupsubsubsection{Conditional equations%
+\isamarkupsubsubsection{Conditional Equations%
}
%
\begin{isamarkuptext}%
@@ -223,7 +223,7 @@
assumption of the subgoal.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Automatic case splits%
+\isamarkupsubsubsection{Automatic Case Splits%
}
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Misc/document/types.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/types.tex Fri Jan 12 16:07:20 2001 +0100
@@ -13,7 +13,7 @@
\end{isamarkuptext}%
\isacommand{consts}\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
\ \ \ \ \ \ \ xor\ \ {\isacharcolon}{\isacharcolon}\ gate%
-\isamarkupsubsection{Constant definitions%
+\isamarkupsubsection{Constant Definitions%
}
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Fri Jan 12 16:07:20 2001 +0100
@@ -11,8 +11,9 @@
and closed with the observation that the associated schema for the definition
of primitive recursive functions leads to overly verbose definitions. Moreover,
if you have worked exercise~\ref{ex:trev-trev} you will have noticed that
-you needed to reprove many lemmas reminiscent of similar lemmas about
-\isa{rev}. We will now show you how \isacommand{recdef} can simplify
+you needed to declare essentially the same function as \isa{rev}
+and prove many standard properties of list reverse all over again.
+We will now show you how \isacommand{recdef} can simplify
definitions and proofs about nested recursive datatypes. As an example we
choose exercise~\ref{ex:trev-trev}:%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Fri Jan 12 16:07:20 2001 +0100
@@ -5,7 +5,7 @@
\begin{isamarkuptext}%
\noindent
Although the definition of \isa{trev} is quite natural, we will have
-overcome a minor difficulty in convincing Isabelle of is termination.
+to overcome a minor difficulty in convincing Isabelle of its termination.
It is precisely this difficulty that is the \textit{raison d'\^etre} of
this subsection.
@@ -27,12 +27,13 @@
where \isa{set} returns the set of elements of a list
and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary
function automatically defined by Isabelle
-(when \isa{term} was defined). First we have to understand why the
+(while processing the declaration of \isa{term}). First we have to understand why the
recursive call of \isa{trev} underneath \isa{map} leads to the above
condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map}
-will apply \isa{trev} only to elements of \isa{ts}. Thus the above
+will apply \isa{trev} only to elements of \isa{ts}. Thus the
condition expresses that the size of the argument \isa{t\ {\isasymin}\ set\ ts} of any
-recursive call of \isa{trev} is strictly less than \isa{size\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}. We will now prove the termination condition and
+recursive call of \isa{trev} is strictly less than \isa{size\ {\isacharparenleft}App\ f\ ts{\isacharparenright}},
+which equals \isa{Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}. We will now prove the termination condition and
continue with our definition. Below we return to the question of how
\isacommand{recdef} ``knows'' about \isa{map}.%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Fri Jan 12 16:07:20 2001 +0100
@@ -11,10 +11,10 @@
\begin{isamarkuptext}%
\noindent
By making this theorem a simplification rule, \isacommand{recdef}
-applies it automatically and the above definition of \isa{trev}
+applies it automatically and the definition of \isa{trev}
succeeds now. As a reward for our effort, we can now prove the desired
-lemma directly. The key is the fact that we no longer need the verbose
-induction schema for type \isa{term} but the simpler one arising from
+lemma directly. We no longer need the verbose
+induction schema for type \isa{term} and can use the simpler one arising from
\isa{trev}:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
@@ -31,7 +31,7 @@
\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-If the proof of the induction step mystifies you, we recommend to go through
+If the proof of the induction step mystifies you, we recommend that you go through
the chain of simplification steps in detail; you will probably need the help of
\isa{trace{\isacharunderscore}simp}. Theorem \isa{map{\isacharunderscore}cong} is discussed below.
%\begin{quote}
@@ -44,9 +44,9 @@
%{term[display]"App f ts"}
%\end{quote}
-The above definition of \isa{trev} is superior to the one in
-\S\ref{sec:nested-datatype} because it brings \isa{rev} into play, about
-which already know a lot, in particular \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.
+The definition of \isa{trev} above is superior to the one in
+\S\ref{sec:nested-datatype} because it uses \isa{rev}
+and lets us use existing facts such as \hbox{\isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}}.
Thus this proof is a good example of an important principle:
\begin{quote}
\emph{Chose your definitions carefully\\
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Fri Jan 12 16:07:20 2001 +0100
@@ -20,8 +20,8 @@
\begin{isabelle}%
\ \ \ \ \ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
\end{isabelle}
-is provded automatically because it is already present as a lemma in the
-arithmetic library. Thus the recursion equation becomes a simplification
+is proved automatically because it is already present as a lemma in
+HOL\@. Thus the recursion equation becomes a simplification
rule. Of course the equation is nonterminating if we are allowed to unfold
the recursive call inside the \isa{else} branch, which is why programming
languages and our simplifier don't do that. Unfortunately the simplifier does
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 12 16:07:20 2001 +0100
@@ -104,7 +104,7 @@
the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
-\section{An introductory proof}
+\section{An Introductory Proof}
\label{sec:intro-proof}
Assuming you have input the declarations and definitions of \texttt{ToyList}
@@ -210,7 +210,7 @@
In order to simplify this subgoal further, a lemma suggests itself.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{First lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}%
+\isamarkupsubsubsection{First Lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}%
}
%
\begin{isamarkuptext}%
@@ -245,7 +245,7 @@
embarking on the proof of a lemma usually remains implicit.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}%
+\isamarkupsubsubsection{Second Lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}%
}
%
\begin{isamarkuptext}%
@@ -300,7 +300,7 @@
and the missing lemma is associativity of \isa{{\isacharat}}.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Third lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}%
+\isamarkupsubsubsection{Third Lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}%
}
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Types/document/Axioms.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Fri Jan 12 16:07:20 2001 +0100
@@ -12,7 +12,7 @@
our above ordering relations.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Partial orders%
+\isamarkupsubsubsection{Partial Orders%
}
%
\begin{isamarkuptext}%
@@ -30,7 +30,7 @@
requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected.
Note that behind the scenes, Isabelle has restricted the axioms to class
\isa{parord}. For example, this is what \isa{refl} really looks like:
-\isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
+\isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isasymColon}parord{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
We have not made \isa{less{\isacharunderscore}le} a global definition because it would
fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}}.
@@ -88,14 +88,14 @@
\isacommand{by}\ simp%
\begin{isamarkuptext}%
\noindent
-The effect is not stunning but demonstrates the principle. It also shows
+The effect is not stunning, but it demonstrates the principle. It also shows
that tools like the simplifier can deal with generic rules as well. Moreover,
it should be clear that the main advantage of the axiomatic method is that
theorems can be proved in the abstract and one does not need to repeat the
proof for each instance.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Linear orders%
+\isamarkupsubsubsection{Linear Orders%
}
%
\begin{isamarkuptext}%
@@ -122,7 +122,7 @@
paragraph.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Strict orders%
+\isamarkupsubsubsection{Strict Orders%
}
%
\begin{isamarkuptext}%
@@ -150,7 +150,7 @@
complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Multiple inheritance and sorts%
+\isamarkupsubsubsection{Multiple Inheritance and Sorts%
}
%
\begin{isamarkuptext}%
@@ -184,7 +184,7 @@
& & \isa{wellord}
\end{array}
\]
-\caption{Subclass diagramm}
+\caption{Subclass Diagram}
\label{fig:subclass}
\end{figure}
--- a/doc-src/TutorialI/Types/document/Numbers.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Fri Jan 12 16:07:20 2001 +0100
@@ -9,16 +9,23 @@
\begin{isamarkuptext}%
numeric literals; default simprules; can re-orient%
\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequote}\isanewline
-\isacommand{oops}%
-\begin{isamarkuptext}%
-proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{0}}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isacommand{oops}\isanewline
\isanewline
-goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
-{\isacharparenleft}{\isacharhash}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m\isanewline
-\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m
-
-
+\isacommand{consts}\ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{recdef}\ h\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline
+{\isachardoublequote}h\ i\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isacharequal}\ {\isacharhash}{\isadigit{3}}\ then\ {\isacharhash}{\isadigit{2}}\ else\ i{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptext}%
+\isa{h\ {\isacharhash}{\isadigit{3}}\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}}
+\isa{h\ i\ {\isacharequal}\ i}%
+\end{isamarkuptext}%
+%
+\begin{isamarkuptext}%
\begin{isabelle}%
{\isacharhash}{\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}%
\end{isabelle}
@@ -56,24 +63,20 @@
these form add_ac; similarly there is mult_ac%
\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}i\ {\isacharplus}\ j{\isacharasterisk}l{\isacharasterisk}k\ {\isacharplus}\ m{\isacharasterisk}n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n{\isacharasterisk}m\ {\isacharplus}\ i\ {\isacharplus}\ k{\isacharasterisk}j{\isacharasterisk}l{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ add{\isacharunderscore}ac\ mult{\isacharunderscore}ac{\isacharparenright}\isanewline
-\isacommand{oops}%
-\begin{isamarkuptext}%
-proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{0}}\isanewline
-\isanewline
-goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
-Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}\isanewline
-\ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}
-
-proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
-\isanewline
-goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
-Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}i\ {\isacharplus}\ j{\isacharasterisk}l{\isacharasterisk}k\ {\isacharplus}\ m{\isacharasterisk}n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n{\isacharasterisk}m\ {\isacharplus}\ i\ {\isacharplus}\ k{\isacharasterisk}j{\isacharasterisk}l{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ add{\isacharunderscore}ac\ mult{\isacharunderscore}ac{\isacharparenright}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ f\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}%
-\end{isamarkuptext}%
-%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isacommand{oops}%
\begin{isamarkuptext}%
\begin{isabelle}%
{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ k\ {\isasymle}\ l{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isasymle}\ j\ {\isacharasterisk}\ l%
@@ -231,7 +234,8 @@
\end{isabelle}
\rulename{abs_mult}%
\end{isamarkuptext}%
-%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}abs\ x\ {\isacharless}\ a{\isacharsemicolon}\ abs\ y\ {\isacharless}\ b{\isasymrbrakk}\ {\isasymLongrightarrow}\ abs\ x\ {\isacharplus}\ abs\ y\ {\isacharless}\ {\isacharparenleft}a\ {\isacharplus}\ b\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{by}\ arith%
\begin{isamarkuptext}%
REALS
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Fri Jan 12 16:07:20 2001 +0100
@@ -8,7 +8,7 @@
constant may have multiple definitions at non-overlapping types.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{An initial example%
+\isamarkupsubsubsection{An Initial Example%
}
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Types/document/Overloading1.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex Fri Jan 12 16:07:20 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{Overloading{\isadigit{1}}}%
%
-\isamarkupsubsubsection{Controlled overloading with type classes%
+\isamarkupsubsubsection{Controlled Overloading with Type Classes%
}
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Fri Jan 12 16:07:20 2001 +0100
@@ -19,7 +19,7 @@
The infix function \isa{{\isacharbang}} yields the nth element of a list.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Predefined overloading%
+\isamarkupsubsubsection{Predefined Overloading%
}
%
\begin{isamarkuptext}%
@@ -47,7 +47,7 @@
\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} &
\isa{LEAST}$~x.~P$
\end{tabular}
-\caption{Overloaded constants in HOL}
+\caption{Overloaded Constants in HOL}
\label{tab:overloading}
\end{center}
\end{table}
--- a/doc-src/TutorialI/Types/document/Pairs.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Fri Jan 12 16:07:20 2001 +0100
@@ -15,27 +15,28 @@
problem: pattern matching with tuples.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Pattern matching with tuples%
+\isamarkupsubsection{Pattern Matching with Tuples%
}
%
\begin{isamarkuptext}%
-It is possible to use (nested) tuples as patterns in $\lambda$-abstractions,
+Tuples may be used as patterns in $\lambda$-abstractions,
for example \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}x{\isacharplus}y{\isacharplus}z} and \isa{{\isasymlambda}{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isacharcomma}z{\isacharparenright}{\isachardot}x{\isacharplus}y{\isacharplus}z}. In fact,
-tuple patterns can be used in most variable binding constructs. Here are
+tuple patterns can be used in most variable binding constructs,
+and they can be nested. Here are
some typical examples:
\begin{quote}
\isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\
\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}\\
\isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}A{\isachardot}\ x{\isacharequal}y}\\
-\isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}}\\
+\isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}\ x{\isacharequal}z{\isacharbraceright}}\\
\isa{{\isasymUnion}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A{\isachardot}\ {\isacharbraceleft}x\ {\isacharplus}\ y{\isacharbraceright}}
\end{quote}%
\end{isamarkuptext}%
%
\begin{isamarkuptext}%
-The intuitive meaning of this notations should be pretty obvious.
+The intuitive meanings of these expressions should be obvious.
Unfortunately, we need to know in more detail what the notation really stands
-for once we have to reason about it. The fact of the matter is that abstraction
+for once we have to reason about it. Abstraction
over pairs and tuples is merely a convenient shorthand for a more complex
internal representation. Thus the internal and external form of a term may
differ, which can affect proofs. If you want to avoid this complication,
@@ -55,7 +56,7 @@
understand how to reason about such constructs.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Theorem proving%
+\isamarkupsubsection{Theorem Proving%
}
%
\begin{isamarkuptext}%
@@ -65,7 +66,7 @@
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}split{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptext}%
This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the
-proof, as in the above lemma. But if it doesn't, you end up with exactly what
+proof, as it does above. But if it doesn't, you end up with exactly what
we are trying to avoid: nests of \isa{fst} and \isa{snd}. Thus this
approach is neither elegant nor very practical in large examples, although it
can be effective in small ones.
--- a/doc-src/TutorialI/Types/document/Typedef.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Typedef.tex Fri Jan 12 16:07:20 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{Typedef}%
%
-\isamarkupsection{Introducing new types%
+\isamarkupsection{Introducing New Types%
}
%
\begin{isamarkuptext}%
@@ -10,8 +10,8 @@
By now we have seen a number of ways for introducing new types, for example
type synonyms, recursive datatypes and records. For most applications, this
repertoire should be quite sufficient. Very occasionally you may feel the
-need for a more advanced type. If you cannot avoid that type, and you are
-quite certain that it is not definable by any of the standard means,
+need for a more advanced type. If you cannot do without that type, and you are
+certain that it is not definable by any of the standard means,
then read on.
\begin{warn}
Types in HOL must be non-empty; otherwise the quantifier rules would be
@@ -19,7 +19,7 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Declaring new types%
+\isamarkupsubsection{Declaring New Types%
}
%
\begin{isamarkuptext}%
@@ -54,11 +54,11 @@
However, we strongly discourage this approach, except at explorative stages
of your development. It is extremely easy to write down contradictory sets of
axioms, in which case you will be able to prove everything but it will mean
-nothing. In the above case it also turns out that the axiomatic approach is
+nothing. Here the axiomatic approach is
unnecessary: a one-element type called \isa{unit} is already defined in HOL.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Defining new types%
+\isamarkupsubsection{Defining New Types%
}
%
\begin{isamarkuptext}%
@@ -131,16 +131,16 @@
\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} &~~ (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse})
\end{tabular}
\end{center}
-
-From the above example it should be clear what \isacommand{typedef} does
-in general: simply replace the name \isa{three} and the set
-\isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}} by the respective arguments.
+%
+From this example it should be clear what \isacommand{typedef} does
+in general given a name (here \isa{three}) and a set
+(here \isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}).
Our next step is to define the basic functions expected on the new type.
Although this depends on the type at hand, the following strategy works well:
\begin{itemize}
-\item define a small kernel of basic functions such that all further
-functions you anticipate can be defined on top of that kernel.
+\item define a small kernel of basic functions that can express all other
+functions you anticipate.
\item define the kernel in terms of corresponding functions on the
representing type using \isa{Abs} and \isa{Rep} to convert between the
two levels.
@@ -170,9 +170,13 @@
\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x{\isacharequal}y{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-We prove both directions separately. From \isa{Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y}
-we derive \isa{Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}} (via
-\isa{arg{\isacharunderscore}cong}: \isa{{\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isacharquery}f\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}f\ {\isacharquery}y}), and thus the required \isa{x\ {\isacharequal}\ y} by simplification with \isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse}. The other direction
+We prove each direction separately. From \isa{Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y}
+we use \isa{arg{\isacharunderscore}cong} to apply \isa{Rep{\isacharunderscore}three} to both sides,
+deriving \begin{isabelle}%
+Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}%
+\end{isabelle}
+Thus we get the required \isa{x\ {\isacharequal}\ y} by simplification with \isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse}.
+The other direction
is trivial by simplification:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}rule\ iffI{\isacharparenright}\isanewline
@@ -226,7 +230,7 @@
\noindent
This substitution step worked nicely because there was just a single
occurrence of a term of type \isa{three}, namely \isa{x}.
-When we now apply the above lemma, \isa{Q} becomes \isa{{\isasymlambda}n{\isachardot}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ n{\isacharparenright}} because \isa{Rep{\isacharunderscore}three\ x} is the only term of type \isa{nat}:%
+When we now apply the lemma, \isa{Q} becomes \isa{{\isasymlambda}n{\isachardot}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ n{\isacharparenright}} because \isa{Rep{\isacharunderscore}three\ x} is the only term of type \isa{nat}:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}rule\ cases{\isacharunderscore}lemma{\isacharparenright}%
\begin{isamarkuptxt}%
@@ -259,7 +263,7 @@
example to demonstrate \isacommand{typedef} because its simplicity makes the
key concepts particularly easy to grasp. If you would like to see a
nontrivial example that cannot be defined more directly, we recommend the
-definition of \emph{finite multisets} in the HOL library.
+definition of \emph{finite multisets} in the HOL Library.
Let us conclude by summarizing the above procedure for defining a new type.
Given some abstract axiomatic description $P$ of a type $ty$ in terms of a