--- a/doc-src/Intro/advanced.tex Thu Mar 17 17:48:37 1994 +0100
+++ b/doc-src/Intro/advanced.tex Sat Mar 19 03:01:25 1994 +0100
@@ -1,17 +1,8 @@
%% $Id$
-\part{Advanced methods}
+\part{Advanced Methods}
Before continuing, it might be wise to try some of your own examples in
Isabelle, reinforcing your knowledge of the basic functions.
-This paper is merely an introduction to Isabelle. Two other documents
-exist:
-\begin{itemize}
- \item {\em The Isabelle Reference Manual\/} contains information about
-most of the facilities of Isabelle, apart from particular object-logics.
- \item {\em Isabelle's Object-Logics\/} describes the various logics
-distributed with Isabelle. It also explains how to define new logics in
-Isabelle.
-\end{itemize}
Look through {\em Isabelle's Object-Logics\/} and try proving some simple
theorems. You probably should begin with first-order logic ({\tt FOL}
or~{\tt LK}). Try working some of the examples provided, and others from
@@ -225,11 +216,13 @@
\subsubsection{Deriving the elimination rule}
-Let us derive $(\neg E)$. The proof follows that of~{\tt conjE}
+Let us derive the rule $(\neg E)$. The proof follows that of~{\tt conjE}
(\S\ref{deriving-example}), with an additional step to unfold negation in
the major premise. Although the {\tt goalw} command is best for this, let
-us try~\ttindex{goal}. As usual, we bind the premises to \ML\ identifiers.
-We then apply \ttindex{FalseE}, which stands for~$(\bot E)$:
+us try~\ttindex{goal} and examine another way of unfolding definitions.
+
+As usual, we bind the premises to \ML\ identifiers. We then apply
+\ttindex{FalseE}, which stands for~$(\bot E)$:
\begin{ttbox}
val [major,minor] = goal FOL.thy "[| ~P; P |] ==> R";
{\out Level 0}
@@ -242,7 +235,10 @@
{\out Level 1}
{\out R}
{\out 1. False}
-\ttbreak
+\end{ttbox}
+Everything follows from falsity. And we can prove falsity using the
+premises and Modus Ponens:
+\begin{ttbox}
by (resolve_tac [mp] 1);
{\out Level 2}
{\out R}
@@ -261,7 +257,8 @@
{\out R}
{\out 1. P}
\end{ttbox}
-Now {\tt?P1} has changed to~{\tt P}; we need only use the minor premise:
+The subgoal {\tt?P1} has been instantiate to~{\tt P}, which we can prove
+using the minor premise:
\begin{ttbox}
by (resolve_tac [minor] 1);
{\out Level 4}
@@ -273,9 +270,9 @@
\indexbold{*notE}
\medskip
-Again, there is a simpler way of conducting this proof. The
-\ttindex{goalw} command unfolds definitions in the premises as well
-as the conclusion:
+Again, there is a simpler way of conducting this proof. Recall that
+the \ttindex{goalw} command unfolds definitions the conclusion; it also
+unfolds definitions in the premises:
\begin{ttbox}
val [major,minor] = goalw FOL.thy [not_def]
"[| ~P; P |] ==> R";
@@ -285,7 +282,8 @@
Observe the difference in {\tt major}; the premises are now {\bf unfolded}
and we need not call~\ttindex{rewrite_rule}. Incidentally, the four calls
to \ttindex{resolve_tac} above can be collapsed to one, with the help
-of~\ttindex{RS}\@:
+of~\ttindex{RS}; this is a typical example of forward reasoning from a
+complex premise.
\begin{ttbox}
minor RS (major RS mp RS FalseE);
{\out val it = "?P [P, ~P]" : thm}
@@ -295,11 +293,12 @@
{\out No subgoals!}
\end{ttbox}
-
-\medskip Finally, here is a trick that is sometimes useful. If the goal
+\goodbreak\medskip
+Finally, here is a trick that is sometimes useful. If the goal
has an outermost meta-quantifier, then \ttindex{goal} and \ttindex{goalw}
-do not return the rule's premises in the list of theorems. Instead, the
-premises become assumptions in subgoal~1:
+do not return the rule's premises in the list of theorems; instead, the
+premises become assumptions in subgoal~1.
+%%%It does not matter which variables are quantified over.
\begin{ttbox}
goalw FOL.thy [not_def] "!!P R. [| ~P; P |] ==> R";
{\out Level 0}
@@ -338,7 +337,7 @@
for deriving the introduction rule~$(\neg I)$.
-\section{Defining theories}
+\section{Defining theories}\label{sec:defining-theories}
\index{theories!defining|(}
Isabelle makes no distinction between simple extensions of a logic --- like
defining a type~$bool$ with constants~$true$ and~$false$ --- and defining
@@ -362,8 +361,7 @@
associated concrete syntax. The translations section specifies rewrite
rules on abstract syntax trees, for defining notations and abbreviations.
The {\ML} section contains code to perform arbitrary syntactic
-transformations. The main declaration forms are discussed below; see {\em
- Isabelle's Object-Logics} for full details and examples.
+transformations. The main declaration forms are discussed below.
All the declaration parts can be omitted. In the simplest case, $T$ is
just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one
@@ -396,7 +394,7 @@
bindings to the old rule may persist. Isabelle ensures that the old and
new versions of~$T$ are not involved in the same proof. Attempting to
combine different versions of~$T$ yields the fatal error
-\begin{ttbox}
+\begin{ttbox}
Attempt to merge different versions of theory: \(T\)
\end{ttbox}
@@ -424,13 +422,20 @@
\(id@n\) "\(rule@n\)"
\end{ttbox}
where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,
-$rule@n$ are expressions of type~$prop$. {\bf Definitions} are rules of
-the form $t\equiv u$. Each rule {\em must\/} be enclosed in quotation marks.
+$rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be
+enclosed in quotation marks.
+
+{\bf Definitions} are rules of the form $t\equiv u$. Normally definitions
+should be conservative, serving only as abbreviations. As of this writing,
+Isabelle does not provide a separate declaration part for definitions; it
+is your responsibility to ensure that your definitions are conservative.
+However, Isabelle's rewriting primitives will reject $t\equiv u$ unless all
+variables free in~$u$ are also free in~$t$.
\index{examples!of theories}
This theory extends first-order logic with two constants {\em nand} and
-{\em xor}, and two rules defining them:
-\begin{ttbox}
+{\em xor}, and declares rules to define them:
+\begin{ttbox}
Gate = FOL +
consts nand,xor :: "[o,o] => o"
rules nand_def "nand(P,Q) == ~(P & Q)"
@@ -440,21 +445,28 @@
\subsection{Declaring type constructors}
-\indexbold{type constructors!declaring}\indexbold{arities!declaring}
+\indexbold{types!declaring}\indexbold{arities!declaring}
+%
Types are composed of type variables and {\bf type constructors}. Each
-type constructor has a fixed number of argument places. For example,
-$list$ is a 1-place type constructor and $nat$ is a 0-place type
-constructor.
-
-The {\bf type declaration part} has the form
+type constructor takes a fixed number of arguments. They are declared
+with an \ML-like syntax. If $list$ takes one type argument, $tree$ takes
+two arguments and $nat$ takes no arguments, then these type constructors
+can be declared by
\begin{ttbox}
-types \(id@1\) \(k@1\)
- \vdots
- \(id@n\) \(k@n\)
+types 'a list
+ ('a,'b) tree
+ nat
\end{ttbox}
-where $id@1$, \ldots, $id@n$ are identifiers and $k@1$, \ldots, $k@n$ are
-natural numbers. It declares each $id@i$ as a type constructor with $k@i$
-argument places.
+
+The {\bf type declaration part} has the general form
+\begin{ttbox}
+types \(tids@1\) \(id@1\)
+ \vdots
+ \(tids@1\) \(id@n\)
+\end{ttbox}
+where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$
+are type argument lists as shown in the example above. It declares each
+$id@i$ as a type constructor with the specified number of argument places.
The {\bf arity declaration part} has the form
\begin{ttbox}
@@ -465,28 +477,26 @@
where $tycon@1$, \ldots, $tycon@n$ are identifiers and $arity@1$, \ldots,
$arity@n$ are arities. Arity declarations add arities to existing
types; they complement type declarations.
-
In the simplest case, for an 0-place type constructor, an arity is simply
the type's class. Let us declare a type~$bool$ of class $term$, with
-constants $tt$ and~$ff$:\footnote{In first-order logic, booleans are
-distinct from formulae, which have type $o::logic$.}
+constants $tt$ and~$ff$. (In first-order logic, booleans are
+distinct from formulae, which have type $o::logic$.)
\index{examples!of theories}
-\begin{ttbox}
+\begin{ttbox}
Bool = FOL +
-types bool 0
+types bool
arities bool :: term
consts tt,ff :: "bool"
end
\end{ttbox}
-In the general case, type constructors take arguments. Each type
-constructor has an {\bf arity} with respect to
-classes~(\S\ref{polymorphic}). A $k$-place type constructor may have
-arities of the form $(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts
-and $c$ is a class. Each sort specifies a type argument; it has the form
-$\{c@1,\ldots,c@m\}$, where $c@1$, \dots,~$c@m$ are classes. Mostly we
-deal with singleton sorts, and may abbreviate them by dropping the braces.
-The arity declaration $list{::}(term)term$ is short for
-$list{::}(\{term\})term$.
+Type constructors can take arguments. Each type constructor has an {\bf
+ arity} with respect to classes~(\S\ref{polymorphic}). A $k$-place type
+constructor may have arities of the form $(s@1,\ldots,s@k)c$, where
+$s@1,\ldots,s@n$ are sorts and $c$ is a class. Each sort specifies a type
+argument; it has the form $\{c@1,\ldots,c@m\}$, where $c@1$, \dots,~$c@m$
+are classes. Mostly we deal with singleton sorts, and may abbreviate them
+by dropping the braces. The arity $(term)term$ is short for
+$(\{term\})term$.
A type constructor may be overloaded (subject to certain conditions) by
appearing in several arity declarations. For instance, the built-in type
@@ -494,20 +504,19 @@
logic, it is declared also to have arity $(term,term)term$.
Theory {\tt List} declares the 1-place type constructor $list$, gives
-it arity $list{::}(term)term$, and declares constants $Nil$ and $Cons$ with
+it arity $(term)term$, and declares constants $Nil$ and $Cons$ with
polymorphic types:
\index{examples!of theories}
-\begin{ttbox}
+\begin{ttbox}
List = FOL +
-types list 1
+types 'a list
arities list :: (term)term
consts Nil :: "'a list"
Cons :: "['a, 'a list] => 'a list"
end
\end{ttbox}
-Multiple type and arity declarations may be abbreviated to a single line:
+Multiple arity declarations may be abbreviated to a single line:
\begin{ttbox}
-types \(id@1\), \ldots, \(id@n\) \(k\)
arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)
\end{ttbox}
@@ -520,7 +529,7 @@
\subsection{Infixes and Mixfixes}
\indexbold{infix operators}\index{examples!of theories}
The constant declaration part of the theory
-\begin{ttbox}
+\begin{ttbox}
Gate2 = FOL +
consts "~&" :: "[o,o] => o" (infixl 35)
"#" :: "[o,o] => o" (infixl 30)
@@ -540,19 +549,19 @@
\indexbold{mixfix operators}
{\bf Mixfix} operators may have arbitrary context-free syntaxes. For example
-\begin{ttbox}
- If :: "[o,o,o] => o" ("if _ then _ else _")
+\begin{ttbox}
+ If :: "[o,o,o] => o" ("if _ then _ else _")
\end{ttbox}
-declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax
-$if~P~then~Q~else~R$ instead of $If(P,Q,R)$. Underscores denote argument
-positions. Pretty-printing information can be specified in order to
-improve the layout of formulae with mixfix operations. For details, see
-{\em Isabelle's Object-Logics}.
+declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
+ if~$P$ then~$Q$ else~$R$} instead of {\tt If($P$,$Q$,$R$)}. Underscores
+denote argument positions. Pretty-printing information can be specified in
+order to improve the layout of formulae with mixfix operations. For
+details, see {\em Isabelle's Object-Logics}.
Mixfix declarations can be annotated with precedences, just like
infixes. The example above is just a shorthand for
-\begin{ttbox}
- If :: "[o,o,o] => o" ("if _ then _ else _" [0,0,0] 1000)
+\begin{ttbox}
+ If :: "[o,o,o] => o" ("if _ then _ else _" [0,0,0] 1000)
\end{ttbox}
The numeric components determine precedences. The list of integers
defines, for each argument position, the minimal precedence an expression
@@ -561,15 +570,15 @@
acceptable because precedences are non-negative, and conditionals may
appear everywhere because 1000 is the highest precedence. On the other
hand,
-\begin{ttbox}
- If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99)
+\begin{ttbox}
+ If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99)
\end{ttbox}
-defines concrete syntax for a
-conditional whose first argument cannot have the form $if~P~then~Q~else~R$
-because it must have a precedence of at least~100. Since expressions put in
-parentheses have maximal precedence, we may of course write
-\begin{quote}
-\it if (if P then Q else R) then S else T
+defines concrete syntax for a conditional whose first argument cannot have
+the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a precedence
+of at least~100. Since expressions put in parentheses have maximal
+precedence, we may of course write
+\begin{quote}\tt
+if (if $P$ then $Q$ else $R$) then $S$ else $T$
\end{quote}
Conditional expressions can also be written using the constant {\tt If}.
@@ -580,7 +589,7 @@
\index{examples!of theories}
\begin{ttbox}
Prod = FOL +
-types "*" 2 (infixl 20)
+types ('a,'b) "*" (infixl 20)
arities "*" :: (term,term)term
consts fst :: "'a * 'b => 'a"
snd :: "'a * 'b => 'b"
@@ -637,9 +646,10 @@
\index{examples!of theories}
\begin{ttbox}
BoolNat = Arith +
-types bool,nat 0
+types bool,nat
arities bool,nat :: arith
consts Suc :: "nat=>nat"
+\ttbreak
rules add0 "0 + n = n::nat"
addS "Suc(m)+n = Suc(m+n)"
nat1 "1 = Suc(0)"
@@ -653,7 +663,7 @@
either type. The type constraints in the axioms are vital. Without
constraints, the $x$ in $1+x = x$ would have type $\alpha{::}arith$
and the axiom would hold for any type of class $arith$. This would
-collapse $nat$:
+collapse $nat$ to a trivial type:
\[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \]
The class $arith$ as defined above is more specific than necessary. Many
types come with a binary operation and identity~(0). On lists,
@@ -670,10 +680,10 @@
\subsection{Extending first-order logic with the natural numbers}
\index{examples!of theories}
-The early part of this paper defines a first-order logic, including a
-type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$. Let us
-introduce the Peano axioms for mathematical induction and the freeness of
-$0$ and~$Suc$:
+Section\ts\ref{sec:logical-syntax} has formalized a first-order logic,
+including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
+Let us introduce the Peano axioms for mathematical induction and the
+freeness of $0$ and~$Suc$:
\[ \vcenter{\infer[(induct)*]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
\qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}
\]
@@ -730,7 +740,7 @@
the 0-place type constructor $nat$ and the constants $rec$ and~$Suc$:
\begin{ttbox}
Nat = FOL +
-types nat 0
+types nat
arities nat :: term
consts "0" :: "nat" ("0")
Suc :: "nat=>nat"
@@ -753,31 +763,31 @@
File {\tt FOL/ex/nat.ML} contains proofs involving this theory of the
natural numbers. As a trivial example, let us derive recursion equations
for \verb$+$. Here is the zero case:
-\begin{ttbox}
+\begin{ttbox}
goalw Nat.thy [add_def] "0+n = n";
{\out Level 0}
{\out 0 + n = n}
-{\out 1. rec(0,n,%x y. Suc(y)) = n}
+{\out 1. rec(0,n,\%x y. Suc(y)) = n}
\ttbreak
by (resolve_tac [rec_0] 1);
{\out Level 1}
{\out 0 + n = n}
{\out No subgoals!}
val add_0 = result();
-\end{ttbox}
+\end{ttbox}
And here is the successor case:
-\begin{ttbox}
+\begin{ttbox}
goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
{\out Level 0}
{\out Suc(m) + n = Suc(m + n)}
-{\out 1. rec(Suc(m),n,%x y. Suc(y)) = Suc(rec(m,n,%x y. Suc(y)))}
+{\out 1. rec(Suc(m),n,\%x y. Suc(y)) = Suc(rec(m,n,\%x y. Suc(y)))}
\ttbreak
by (resolve_tac [rec_Suc] 1);
{\out Level 1}
{\out Suc(m) + n = Suc(m + n)}
{\out No subgoals!}
val add_Suc = result();
-\end{ttbox}
+\end{ttbox}
The induction rule raises some complications, which are discussed next.
\index{theories!defining|)}
@@ -820,7 +830,7 @@
Let us prove that no natural number~$k$ equals its own successor. To
use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good
instantiation for~$\Var{P}$.
-\begin{ttbox}
+\begin{ttbox}
goal Nat.thy "~ (Suc(k) = k)";
{\out Level 0}
{\out ~Suc(k) = k}
@@ -831,13 +841,13 @@
{\out ~Suc(k) = k}
{\out 1. ~Suc(0) = 0}
{\out 2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
-\end{ttbox}
+\end{ttbox}
We should check that Isabelle has correctly applied induction. Subgoal~1
is the base case, with $k$ replaced by~0. Subgoal~2 is the inductive step,
with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.
The rest of the proof demonstrates~\ttindex{notI}, \ttindex{notE} and the
other rules of~\ttindex{Nat.thy}. The base case holds by~\ttindex{Suc_neq_0}:
-\begin{ttbox}
+\begin{ttbox}
by (resolve_tac [notI] 1);
{\out Level 2}
{\out ~Suc(k) = k}
@@ -848,10 +858,11 @@
{\out Level 3}
{\out ~Suc(k) = k}
{\out 1. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
-\end{ttbox}
+\end{ttbox}
The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
-Using the negation rule, we assume $Suc(Suc(x)) = Suc(x)$ and prove $Suc(x)=x$:
-\begin{ttbox}
+Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
+$Suc(Suc(x)) = Suc(x)$:
+\begin{ttbox}
by (resolve_tac [notI] 1);
{\out Level 4}
{\out ~Suc(k) = k}
@@ -866,7 +877,7 @@
{\out Level 6}
{\out ~Suc(k) = k}
{\out No subgoals!}
-\end{ttbox}
+\end{ttbox}
\subsection{An example of ambiguity in {\tt resolve_tac}}
@@ -875,7 +886,7 @@
not actually needed. Almost by chance, \ttindex{resolve_tac} finds the right
instantiation for~$(induct)$ to yield the desired next state. With more
complex formulae, our luck fails.
-\begin{ttbox}
+\begin{ttbox}
goal Nat.thy "(k+m)+n = k+(m+n)";
{\out Level 0}
{\out k + m + n = k + (m + n)}
@@ -886,59 +897,63 @@
{\out k + m + n = k + (m + n)}
{\out 1. k + m + n = 0}
{\out 2. !!x. k + m + n = x ==> k + m + n = Suc(x)}
-\end{ttbox}
-This proof requires induction on~$k$. But the 0 in subgoal~1 indicates
-that induction has been applied to the term~$k+(m+n)$. The
-\ttindex{back} command causes backtracking to an alternative
-outcome of the tactic.
-\begin{ttbox}
+\end{ttbox}
+This proof requires induction on~$k$. The occurrence of~0 in subgoal~1
+indicates that induction has been applied to the term~$k+(m+n)$; this
+application is sound but will not lead to a proof here. Fortunately,
+Isabelle can (lazily!) generate all the valid applications of induction.
+The \ttindex{back} command causes backtracking to an alternative outcome of
+the tactic.
+\begin{ttbox}
back();
{\out Level 1}
{\out k + m + n = k + (m + n)}
{\out 1. k + m + n = k + 0}
{\out 2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)}
-\end{ttbox}
-Now induction has been applied to~$m+n$. Let us call \ttindex{back}
-again.
-\begin{ttbox}
+\end{ttbox}
+Now induction has been applied to~$m+n$. This is equally useless. Let us
+call \ttindex{back} again.
+\begin{ttbox}
back();
{\out Level 1}
{\out k + m + n = k + (m + n)}
{\out 1. k + m + 0 = k + (m + 0)}
-{\out 2. !!x. k + m + x = k + (m + x) ==> k + m + Suc(x) = k + (m + Suc(x))}
-\end{ttbox}
+{\out 2. !!x. k + m + x = k + (m + x) ==>}
+{\out k + m + Suc(x) = k + (m + Suc(x))}
+\end{ttbox}
Now induction has been applied to~$n$. What is the next alternative?
-\begin{ttbox}
+\begin{ttbox}
back();
{\out Level 1}
{\out k + m + n = k + (m + n)}
{\out 1. k + m + n = k + (m + 0)}
{\out 2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))}
-\end{ttbox}
+\end{ttbox}
Inspecting subgoal~1 reveals that induction has been applied to just the
second occurrence of~$n$. This perfectly legitimate induction is useless
here. The main goal admits fourteen different applications of induction.
The number is exponential in the size of the formula.
\subsection{Proving that addition is associative}
-\index{associativity of addition}
-\index{examples!of rewriting}
-Let us do the proof properly, using~\ttindex{res_inst_tac}. At the same
-time, we shall have a glimpse at Isabelle's rewriting tactics, which are
-described in the {\em Reference Manual}.
+Let us invoke the induction rule properly properly,
+using~\ttindex{res_inst_tac}. At the same time, we shall have a glimpse at
+Isabelle's rewriting tactics, which are described in the {\em Reference
+ Manual}.
-\index{rewriting!object-level}
+\index{rewriting!object-level}\index{examples!of rewriting}
+
Isabelle's rewriting tactics repeatedly applies equations to a subgoal,
simplifying or proving it. For efficiency, the rewriting rules must be
-packaged into a \bfindex{simplification set}. Let us include the equations
+packaged into a \bfindex{simplification set}, or {\bf simpset}. We take
+the standard simpset for first-order logic and insert the equations
for~{\tt add} proved in the previous section, namely $0+n=n$ and ${\tt
- Suc}(m)+n={\tt Suc}(m+n)$:
-\begin{ttbox}
+ Suc}(m)+n={\tt Suc}(m+n)$:
+\begin{ttbox}
val add_ss = FOL_ss addrews [add_0, add_Suc];
-\end{ttbox}
+\end{ttbox}
We state the goal for associativity of addition, and
use \ttindex{res_inst_tac} to invoke induction on~$k$:
-\begin{ttbox}
+\begin{ttbox}
goal Nat.thy "(k+m)+n = k+(m+n)";
{\out Level 0}
{\out k + m + n = k + (m + n)}
@@ -948,34 +963,36 @@
{\out Level 1}
{\out k + m + n = k + (m + n)}
{\out 1. 0 + m + n = 0 + (m + n)}
-{\out 2. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)}
-\end{ttbox}
+{\out 2. !!x. x + m + n = x + (m + n) ==>}
+{\out Suc(x) + m + n = Suc(x) + (m + n)}
+\end{ttbox}
The base case holds easily; both sides reduce to $m+n$. The
tactic~\ttindex{simp_tac} rewrites with respect to the given simplification
set, applying the rewrite rules for~{\tt +}:
-\begin{ttbox}
+\begin{ttbox}
by (simp_tac add_ss 1);
{\out Level 2}
{\out k + m + n = k + (m + n)}
-{\out 1. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)}
-\end{ttbox}
+{\out 1. !!x. x + m + n = x + (m + n) ==>}
+{\out Suc(x) + m + n = Suc(x) + (m + n)}
+\end{ttbox}
The inductive step requires rewriting by the equations for~{\tt add}
together the induction hypothesis, which is also an equation. The
tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any
useful assumptions:
-\begin{ttbox}
+\begin{ttbox}
by (asm_simp_tac add_ss 1);
{\out Level 3}
{\out k + m + n = k + (m + n)}
{\out No subgoals!}
-\end{ttbox}
+\end{ttbox}
-\section{A {\sc Prolog} interpreter}
+\section{A Prolog interpreter}
\index{Prolog interpreter|bold}
-To demonstrate the power of tacticals, let us construct a {\sc Prolog}
+To demonstrate the power of tacticals, let us construct a Prolog
interpreter and execute programs involving lists.\footnote{To run these
-examples, see the file {\tt FOL/ex/prolog.ML}.} The {\sc Prolog} program
+examples, see the file {\tt FOL/ex/prolog.ML}.} The Prolog program
consists of a theory. We declare a type constructor for lists, with an
arity declaration to say that $(\tau)list$ is of class~$term$
provided~$\tau$ is:
@@ -984,7 +1001,7 @@
\end{eqnarray*}
We declare four constants: the empty list~$Nil$; the infix list
constructor~{:}; the list concatenation predicate~$app$; the list reverse
-predicate~$rev$. (In {\sc Prolog}, functions on lists are expressed as
+predicate~$rev$. (In Prolog, functions on lists are expressed as
predicates.)
\begin{eqnarray*}
Nil & :: & \alpha list \\
@@ -992,7 +1009,7 @@
app & :: & [\alpha list,\alpha list,\alpha list] \To o \\
rev & :: & [\alpha list,\alpha list] \To o
\end{eqnarray*}
-The predicate $app$ should satisfy the {\sc Prolog}-style rules
+The predicate $app$ should satisfy the Prolog-style rules
\[ {app(Nil,ys,ys)} \qquad
{app(xs,ys,zs) \over app(x:xs, ys, x:zs)} \]
We define the naive version of $rev$, which calls~$app$:
@@ -1020,7 +1037,7 @@
end
\end{ttbox}
\subsection{Simple executions}
-Repeated application of the rules solves {\sc Prolog} goals. Let us
+Repeated application of the rules solves Prolog goals. Let us
append the lists $[a,b,c]$ and~$[d,e]$. As the rules are applied, the
answer builds up in~{\tt ?x}.
\begin{ttbox}
@@ -1052,7 +1069,7 @@
{\out No subgoals!}
\end{ttbox}
-{\sc Prolog} can run functions backwards. Which list can be appended
+Prolog can run functions backwards. Which list can be appended
with $[c,d]$ to produce $[a,b,c,d]$?
Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$:
\begin{ttbox}
@@ -1068,11 +1085,11 @@
\end{ttbox}
-\subsection{Backtracking}
-\index{backtracking}
+\subsection{Backtracking}\index{backtracking}
+Prolog backtracking can handle questions that have multiple solutions.
Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$?
-Using \ttindex{REPEAT} to apply the rules, we quickly find the solution
-$x=[]$ and $y=[a,b,c,d]$:
+Using \ttindex{REPEAT} to apply the rules, we quickly find the first
+solution, namely $x=[]$ and $y=[a,b,c,d]$:
\begin{ttbox}
goal Prolog.thy "app(?x, ?y, a:b:c:d:Nil)";
{\out Level 0}
@@ -1084,8 +1101,8 @@
{\out app(Nil, a : b : c : d : Nil, a : b : c : d : Nil)}
{\out No subgoals!}
\end{ttbox}
-The \ttindex{back} command returns the tactic's next outcome,
-$x=[a]$ and $y=[b,c,d]$:
+Isabelle can lazily generate all the possibilities. The \ttindex{back}
+command returns the tactic's next outcome, namely $x=[a]$ and $y=[b,c,d]$:
\begin{ttbox}
back();
{\out Level 1}
@@ -1121,7 +1138,9 @@
goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
{\out Level 0}
{\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)}
-{\out 1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)}
+{\out 1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
+{\out ?w)}
+\ttbreak
val rules = [appNil,appCons,revNil,revCons];
\ttbreak
by (REPEAT (resolve_tac rules 1));
@@ -1168,8 +1187,8 @@
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1)
(resolve_tac rules 1);
\end{ttbox}
-Since {\sc Prolog} uses depth-first search, this tactic is a (slow!) {\sc
-Prolog} interpreter. We return to the start of the proof (using
+Since Prolog uses depth-first search, this tactic is a (slow!)
+Prolog interpreter. We return to the start of the proof (using
\ttindex{choplev}), and apply {\tt prolog_tac}:
\begin{ttbox}
choplev 0;
@@ -1194,6 +1213,6 @@
{\out rev(a : b : c : d : Nil, d : c : b : a : Nil)}
{\out No subgoals!}
\end{ttbox}
-Although Isabelle is much slower than a {\sc Prolog} system, Isabelle
+Although Isabelle is much slower than a Prolog system, Isabelle
tactics can exploit logic programming techniques.