Initial revision
authorlcp
Wed Nov 10 05:06:55 1993 +0100 (1993-11-10)
changeset 105216d6ed87399
parent 104 d8205bb279a7
child 106 7a5d207e6151
Initial revision
doc-src/Intro/advanced.tex
doc-src/Intro/arith.thy
doc-src/Intro/bool.thy
doc-src/Intro/bool_nat.thy
doc-src/Intro/deriv.txt
doc-src/Intro/foundations.tex
doc-src/Intro/gate.thy
doc-src/Intro/gate2.thy
doc-src/Intro/getting.tex
doc-src/Intro/intro.bbl
doc-src/Intro/intro.ind
doc-src/Intro/intro.tex
doc-src/Intro/intro.toc
doc-src/Intro/list.thy
doc-src/Intro/prod.thy
doc-src/Intro/quant.txt
doc-src/Intro/theorems-out.txt
doc-src/Intro/theorems.txt
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Intro/advanced.tex	Wed Nov 10 05:06:55 1993 +0100
     1.3 @@ -0,0 +1,1199 @@
     1.4 +%% $Id$
     1.5 +\part{Advanced methods}
     1.6 +Before continuing, it might be wise to try some of your own examples in
     1.7 +Isabelle, reinforcing your knowledge of the basic functions.
     1.8 +This paper is merely an introduction to Isabelle.  Two other documents
     1.9 +exist:
    1.10 +\begin{itemize}
    1.11 +  \item {\em The Isabelle Reference Manual\/} contains information about
    1.12 +most of the facilities of Isabelle, apart from particular object-logics.
    1.13 +
    1.14 +  \item {\em Isabelle's Object-Logics\/} describes the various logics
    1.15 +distributed with Isabelle.  It also explains how to define new logics in
    1.16 +Isabelle.
    1.17 +\end{itemize}
    1.18 +Look through {\em Isabelle's Object-Logics\/} and try proving some simple
    1.19 +theorems.  You probably should begin with first-order logic ({\tt FOL}
    1.20 +or~{\tt LK}).  Try working some of the examples provided, and others from
    1.21 +the literature.  Set theory~({\tt ZF}) and Constructive Type Theory~({\tt
    1.22 +  CTT}) form a richer world for mathematical reasoning and, again, many
    1.23 +examples are in the literature.  Higher-order logic~({\tt HOL}) is
    1.24 +Isabelle's most sophisticated logic, because its types and functions are
    1.25 +identified with those of the meta-logic; this may cause difficulties for
    1.26 +beginners.
    1.27 +
    1.28 +Choose a logic that you already understand.  Isabelle is a proof
    1.29 +tool, not a teaching tool; if you do not know how to do a particular proof
    1.30 +on paper, then you certainly will not be able to do it on the machine.
    1.31 +Even experienced users plan large proofs on paper.
    1.32 +
    1.33 +We have covered only the bare essentials of Isabelle, but enough to perform
    1.34 +substantial proofs.  By occasionally dipping into the {\em Reference
    1.35 +Manual}, you can learn additional tactics, subgoal commands and tacticals.
    1.36 +Isabelle's simplifier and classical theorem prover are
    1.37 +difficult to learn, and can be ignored at first.
    1.38 +
    1.39 +
    1.40 +\section{Deriving rules in Isabelle}
    1.41 +\index{rules!derived}
    1.42 +A mathematical development goes through a progression of stages.  Each
    1.43 +stage defines some concepts and derives rules about them.  We shall see how
    1.44 +to derive rules, perhaps involving definitions, using Isabelle.  The
    1.45 +following section will explain how to declare types, constants, axioms and
    1.46 +definitions.
    1.47 +
    1.48 +
    1.49 +\subsection{Deriving a rule using tactics} \label{deriving-example}
    1.50 +\index{examples!of deriving rules}
    1.51 +The subgoal module supports the derivation of rules.  The \ttindex{goal}
    1.52 +command, when supplied a goal of the form $\List{\theta@1; \ldots;
    1.53 +\theta@k} \Imp \phi$, creates $\phi\Imp\phi$ as the initial proof state and
    1.54 +returns a list consisting of the theorems 
    1.55 +${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.  These assumptions are
    1.56 +also recorded internally, allowing \ttindex{result} to discharge them in the
    1.57 +original order.
    1.58 +
    1.59 +Let us derive $\conj$ elimination~(\S\ref{deriving}) using Isabelle.
    1.60 +Until now, calling \ttindex{goal} has returned an empty list, which we have
    1.61 +thrown away.  In this example, the list contains the two premises of the
    1.62 +rule.  We bind them to the \ML\ identifiers {\tt major} and {\tt
    1.63 +minor}:\footnote{Some ML compilers will print a message such as {\em
    1.64 +binding not exhaustive}.  This warns that {\tt goal} must return a
    1.65 +2-element list.  Otherwise, the pattern-match will fail; ML will
    1.66 +raise exception \ttindex{Match}.}
    1.67 +\begin{ttbox}
    1.68 +val [major,minor] = goal FOL.thy
    1.69 +    "[| P&Q;  [| P; Q |] ==> R |] ==> R";
    1.70 +{\out Level 0}
    1.71 +{\out R}
    1.72 +{\out  1. R}
    1.73 +{\out val major = "P & Q  [P & Q]" : thm}
    1.74 +{\out val minor = "[| P; Q |] ==> R  [[| P; Q |] ==> R]" : thm}
    1.75 +\end{ttbox}
    1.76 +Look at the minor premise, recalling that meta-level assumptions are
    1.77 +shown in brackets.  Using {\tt minor}, we reduce $R$ to the subgoals
    1.78 +$P$ and~$Q$:
    1.79 +\begin{ttbox}
    1.80 +by (resolve_tac [minor] 1);
    1.81 +{\out Level 1}
    1.82 +{\out R}
    1.83 +{\out  1. P}
    1.84 +{\out  2. Q}
    1.85 +\end{ttbox}
    1.86 +Deviating from~\S\ref{deriving}, we apply $({\conj}E1)$ forwards from the
    1.87 +assumption $P\conj Q$ to obtain the theorem~$P\;[P\conj Q]$.
    1.88 +\begin{ttbox}
    1.89 +major RS conjunct1;
    1.90 +{\out val it = "P  [P & Q]" : thm}
    1.91 +\ttbreak
    1.92 +by (resolve_tac [major RS conjunct1] 1);
    1.93 +{\out Level 2}
    1.94 +{\out R}
    1.95 +{\out  1. Q}
    1.96 +\end{ttbox}
    1.97 +Similarly, we solve the subgoal involving~$Q$.
    1.98 +\begin{ttbox}
    1.99 +major RS conjunct2;
   1.100 +{\out val it = "Q  [P & Q]" : thm}
   1.101 +by (resolve_tac [major RS conjunct2] 1);
   1.102 +{\out Level 3}
   1.103 +{\out R}
   1.104 +{\out No subgoals!}
   1.105 +\end{ttbox}
   1.106 +Calling \ttindex{topthm} returns the current proof state as a theorem.
   1.107 +Note that it contains assumptions.  Calling \ttindex{result} discharges the
   1.108 +assumptions --- both occurrences of $P\conj Q$ are discharged as one ---
   1.109 +and makes the variables schematic.
   1.110 +\begin{ttbox}
   1.111 +topthm();
   1.112 +{\out val it = "R  [P & Q, P & Q, [| P; Q |] ==> R]" : thm}
   1.113 +val conjE = result();
   1.114 +{\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm}
   1.115 +\end{ttbox}
   1.116 +
   1.117 +
   1.118 +\subsection{Definitions and derived rules} \label{definitions}
   1.119 +\index{rules!derived}
   1.120 +\index{Isabelle!definitions in}
   1.121 +\index{definitions!reasoning about|bold}
   1.122 +Definitions are expressed as meta-level equalities.  Let us define negation
   1.123 +and the if-and-only-if connective:
   1.124 +\begin{eqnarray*}
   1.125 +  \neg \Var{P}          & \equiv & \Var{P}\imp\bot \\
   1.126 +  \Var{P}\bimp \Var{Q}  & \equiv & 
   1.127 +                (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
   1.128 +\end{eqnarray*}
   1.129 +\index{rewriting!meta-level|bold}
   1.130 +\index{unfolding|bold}\index{folding|bold}
   1.131 +Isabelle permits {\bf meta-level rewriting} using definitions such as
   1.132 +these.  {\bf Unfolding} replaces every instance
   1.133 +of $\neg \Var{P}$ by the corresponding instance of $\Var{P}\imp\bot$.  For
   1.134 +example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to
   1.135 +\[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot.  \]
   1.136 +{\bf Folding} a definition replaces occurrences of the right-hand side by
   1.137 +the left.  The occurrences need not be free in the entire formula.
   1.138 +
   1.139 +\begin{warn}
   1.140 +Isabelle does not distinguish sensible definitions, like $1\equiv Suc(0)$, from
   1.141 +equations like $1\equiv Suc(1)$.  However, meta-rewriting fails for
   1.142 +equations like ${f(\Var{x})\equiv g(\Var{x},\Var{y})}$: all variables on
   1.143 +the right-hand side must also be present on the left.
   1.144 +\index{rewriting!meta-level}
   1.145 +\end{warn}
   1.146 +
   1.147 +When you define new concepts, you should derive rules asserting their
   1.148 +abstract properties, and then forget their definitions.  This supports
   1.149 +modularity: if you later change the definitions, without affecting their
   1.150 +abstract properties, then most of your proofs will carry through without
   1.151 +change.  Indiscriminate unfolding makes a subgoal grow exponentially,
   1.152 +becoming unreadable.
   1.153 +
   1.154 +Taking this point of view, Isabelle does not unfold definitions
   1.155 +automatically during proofs.  Rewriting must be explicit and selective.
   1.156 +Isabelle provides tactics and meta-rules for rewriting, and a version of
   1.157 +the {\tt goal} command that unfolds the conclusion and premises of the rule
   1.158 +being derived.
   1.159 +
   1.160 +For example, the intuitionistic definition of negation given above may seem
   1.161 +peculiar.  Using Isabelle, we shall derive pleasanter negation rules:
   1.162 +\[  \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}}   \qquad
   1.163 +    \infer[({\neg}E)]{Q}{\neg P & P}  \]
   1.164 +This requires proving the following formulae:
   1.165 +$$ (P\Imp\bot)    \Imp \neg P   \eqno(\neg I)$$
   1.166 +$$ \List{\neg P; P} \Imp Q.       \eqno(\neg E)$$
   1.167 +
   1.168 +
   1.169 +\subsubsection{Deriving the introduction rule}
   1.170 +To derive $(\neg I)$, we may call \ttindex{goal} with the appropriate
   1.171 +formula.  Again, {\tt goal} returns a list consisting of the rule's
   1.172 +premises.  We bind this list, which contains the one element $P\Imp\bot$,
   1.173 +to the \ML\ identifier {\tt prems}.
   1.174 +\begin{ttbox}
   1.175 +val prems = goal FOL.thy "(P ==> False) ==> ~P";
   1.176 +{\out Level 0}
   1.177 +{\out ~P}
   1.178 +{\out  1. ~P}
   1.179 +{\out val prems = ["P ==> False  [P ==> False]"] : thm list}
   1.180 +\end{ttbox}
   1.181 +Calling \ttindex{rewrite_goals_tac} with \ttindex{not_def}, which is the
   1.182 +definition of negation, unfolds that definition in the subgoals.  It leaves
   1.183 +the main goal alone.
   1.184 +\begin{ttbox}
   1.185 +not_def;
   1.186 +{\out val it = "~?P == ?P --> False" : thm}
   1.187 +by (rewrite_goals_tac [not_def]);
   1.188 +{\out Level 1}
   1.189 +{\out ~P}
   1.190 +{\out  1. P --> False}
   1.191 +\end{ttbox}
   1.192 +Using \ttindex{impI} and the premise, we reduce subgoal~1 to a triviality:
   1.193 +\begin{ttbox}
   1.194 +by (resolve_tac [impI] 1);
   1.195 +{\out Level 2}
   1.196 +{\out ~P}
   1.197 +{\out  1. P ==> False}
   1.198 +\ttbreak
   1.199 +by (resolve_tac prems 1);
   1.200 +{\out Level 3}
   1.201 +{\out ~P}
   1.202 +{\out  1. P ==> P}
   1.203 +\end{ttbox}
   1.204 +The rest of the proof is routine.
   1.205 +\begin{ttbox}
   1.206 +by (assume_tac 1);
   1.207 +{\out Level 4}
   1.208 +{\out ~P}
   1.209 +{\out No subgoals!}
   1.210 +val notI = result();
   1.211 +{\out val notI = "(?P ==> False) ==> ~?P" : thm}
   1.212 +\end{ttbox}
   1.213 +\indexbold{*notI}
   1.214 +
   1.215 +\medskip
   1.216 +There is a simpler way of conducting this proof.  The \ttindex{goalw}
   1.217 +command starts a backward proof, as does \ttindex{goal}, but it also
   1.218 +unfolds definitions:
   1.219 +\begin{ttbox}
   1.220 +val prems = goalw FOL.thy [not_def]
   1.221 +    "(P ==> False) ==> ~P";
   1.222 +{\out Level 0}
   1.223 +{\out ~P}
   1.224 +{\out  1. P --> False}
   1.225 +{\out val prems = ["P ==> False  [P ==> False]"] : thm list}
   1.226 +\end{ttbox}
   1.227 +The proof continues as above, but without calling \ttindex{rewrite_goals_tac}.
   1.228 +
   1.229 +
   1.230 +\subsubsection{Deriving the elimination rule}
   1.231 +Let us derive $(\neg E)$.  The proof follows that of~{\tt conjE}
   1.232 +(\S\ref{deriving-example}), with an additional step to unfold negation in
   1.233 +the major premise.  Although the {\tt goalw} command is best for this, let
   1.234 +us try~\ttindex{goal}.  As usual, we bind the premises to \ML\ identifiers.
   1.235 +We then apply \ttindex{FalseE}, which stands for~$(\bot E)$:
   1.236 +\begin{ttbox}
   1.237 +val [major,minor] = goal FOL.thy "[| ~P;  P |] ==> R";
   1.238 +{\out Level 0}
   1.239 +{\out R}
   1.240 +{\out  1. R}
   1.241 +{\out val major = "~ P  [~ P]" : thm}
   1.242 +{\out val minor = "P  [P]" : thm}
   1.243 +\ttbreak
   1.244 +by (resolve_tac [FalseE] 1);
   1.245 +{\out Level 1}
   1.246 +{\out R}
   1.247 +{\out  1. False}
   1.248 +\ttbreak
   1.249 +by (resolve_tac [mp] 1);
   1.250 +{\out Level 2}
   1.251 +{\out R}
   1.252 +{\out  1. ?P1 --> False}
   1.253 +{\out  2. ?P1}
   1.254 +\end{ttbox}
   1.255 +For subgoal~1, we transform the major premise from~$\neg P$
   1.256 +to~${P\imp\bot}$.  The function \ttindex{rewrite_rule}, given a list of
   1.257 +definitions, unfolds them in a theorem.  Rewriting does {\bf not}
   1.258 +affect the theorem's hypothesis, which remains~$\neg P$:
   1.259 +\begin{ttbox}
   1.260 +rewrite_rule [not_def] major;
   1.261 +{\out val it = "P --> False  [~P]" : thm}
   1.262 +by (resolve_tac [it] 1);
   1.263 +{\out Level 3}
   1.264 +{\out R}
   1.265 +{\out  1. P}
   1.266 +\end{ttbox}
   1.267 +Now {\tt?P1} has changed to~{\tt P}; we need only use the minor premise:
   1.268 +\begin{ttbox}
   1.269 +by (resolve_tac [minor] 1);
   1.270 +{\out Level 4}
   1.271 +{\out R}
   1.272 +{\out No subgoals!}
   1.273 +val notE = result();
   1.274 +{\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
   1.275 +\end{ttbox}
   1.276 +\indexbold{*notE}
   1.277 +
   1.278 +\medskip
   1.279 +Again, there is a simpler way of conducting this proof.  The
   1.280 +\ttindex{goalw} command starts unfolds definitions in the premises, as well
   1.281 +as the conclusion:
   1.282 +\begin{ttbox}
   1.283 +val [major,minor] = goalw FOL.thy [not_def]
   1.284 +    "[| ~P;  P |] ==> R";
   1.285 +{\out val major = "P --> False  [~ P]" : thm}
   1.286 +{\out val minor = "P  [P]" : thm}
   1.287 +\end{ttbox}
   1.288 +Observe the difference in {\tt major}; the premises are now {\bf unfolded}
   1.289 +and we need not call~\ttindex{rewrite_rule}.  Incidentally, the four calls
   1.290 +to \ttindex{resolve_tac} above can be collapsed to one, with the help
   1.291 +of~\ttindex{RS}\@:
   1.292 +\begin{ttbox}
   1.293 +minor RS (major RS mp RS FalseE);
   1.294 +{\out val it = "?P  [P, ~P]" : thm}
   1.295 +by (resolve_tac [it] 1);
   1.296 +{\out Level 1}
   1.297 +{\out R}
   1.298 +{\out No subgoals!}
   1.299 +\end{ttbox}
   1.300 +
   1.301 +
   1.302 +\medskip Finally, here is a trick that is sometimes useful.  If the goal
   1.303 +has an outermost meta-quantifier, then \ttindex{goal} and \ttindex{goalw}
   1.304 +do not return the rule's premises in the list of theorems.  Instead, the
   1.305 +premises become assumptions in subgoal~1:
   1.306 +\begin{ttbox}
   1.307 +goalw FOL.thy [not_def] "!!P R. [| ~P;  P |] ==> R";
   1.308 +{\out Level 0}
   1.309 +{\out !!P R. [| ~ P; P |] ==> R}
   1.310 +{\out  1. !!P R. [| P --> False; P |] ==> R}
   1.311 +val it = [] : thm list
   1.312 +\end{ttbox}
   1.313 +The proof continues as before.  But instead of referring to \ML\
   1.314 +identifiers, we refer to assumptions using \ttindex{eresolve_tac} or
   1.315 +\ttindex{assume_tac}: 
   1.316 +\begin{ttbox}
   1.317 +by (resolve_tac [FalseE] 1);
   1.318 +{\out Level 1}
   1.319 +{\out !!P R. [| ~ P; P |] ==> R}
   1.320 +{\out  1. !!P R. [| P --> False; P |] ==> False}
   1.321 +\ttbreak
   1.322 +by (eresolve_tac [mp] 1);
   1.323 +{\out Level 2}
   1.324 +{\out !!P R. [| ~ P; P |] ==> R}
   1.325 +{\out  1. !!P R. P ==> P}
   1.326 +\ttbreak
   1.327 +by (assume_tac 1);
   1.328 +{\out Level 3}
   1.329 +{\out !!P R. [| ~ P; P |] ==> R}
   1.330 +{\out No subgoals!}
   1.331 +\end{ttbox}
   1.332 +Calling \ttindex{result} strips the meta-quantifiers, so the resulting
   1.333 +theorem is the same as before.
   1.334 +\begin{ttbox}
   1.335 +val notE = result();
   1.336 +{\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
   1.337 +\end{ttbox}
   1.338 +Do not use the {\tt!!}\ trick if the premises contain meta-level
   1.339 +connectives, because \ttindex{eresolve_tac} and \ttindex{assume_tac} would
   1.340 +not be able to handle the resulting assumptions.  The trick is not suitable
   1.341 +for deriving the introduction rule~$(\neg I)$.
   1.342 +
   1.343 +
   1.344 +\section{Defining theories}
   1.345 +\index{theories!defining|(}
   1.346 +Isabelle makes no distinction between simple extensions of a logic --- like
   1.347 +defining a type~$bool$ with constants~$true$ and~$false$ --- and defining
   1.348 +an entire logic.  A theory definition has the form
   1.349 +\begin{ttbox}
   1.350 +\(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
   1.351 +classes      {\it class declarations}
   1.352 +default      {\it sort}
   1.353 +types        {\it type declarations}
   1.354 +arities      {\it arity declarations}
   1.355 +consts       {\it constant declarations}
   1.356 +rules        {\it rule declarations}
   1.357 +translations {\it translation declarations}
   1.358 +end
   1.359 +ML           {\it ML code}
   1.360 +\end{ttbox}
   1.361 +This declares the theory $T$ to extend the existing theories
   1.362 +$S@1$,~\ldots,~$S@n$.  It may declare new classes, types, arities
   1.363 +(overloadings of existing types), constants and rules; it can specify the
   1.364 +default sort for type variables.  A constant declaration can specify an
   1.365 +associated concrete syntax.  The translations section specifies rewrite
   1.366 +rules on abstract syntax trees, for defining notations and abbreviations.
   1.367 +The {\ML} section contains code to perform arbitrary syntactic
   1.368 +transformations.  The main declaration forms are discussed below; see {\em
   1.369 +  Isabelle's Object-Logics} for full details and examples.
   1.370 +
   1.371 +All the declaration parts can be omitted.  In the simplest case, $T$ is
   1.372 +just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
   1.373 +or more other theories, inheriting their types, constants, syntax, etc.
   1.374 +The theory \ttindexbold{Pure} contains nothing but Isabelle's meta-logic.
   1.375 +
   1.376 +Each theory definition must reside in a separate file, whose name is
   1.377 +determined as follows: the theory name, say {\tt ListFn}, is converted to
   1.378 +lower case and {\tt.thy} is appended, yielding the filename {\tt
   1.379 +  listfn.thy}.  Isabelle uses this convention to locate the file containing
   1.380 +a given theory; \ttindexbold{use_thy} automatically loads a theory's
   1.381 +parents before loading the theory itself.
   1.382 +
   1.383 +Calling \ttindexbold{use_thy}~{\tt"}{\it tf\/}{\tt"} reads a theory from
   1.384 +the file {\it tf}{\tt.thy}, writes the corresponding {\ML} code to the file
   1.385 +{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file.  This declares the
   1.386 +{\ML} structure~$T$, which contains a component {\tt thy} denoting the new
   1.387 +theory, a component for each rule, and everything declared in {\it ML
   1.388 +  code}.
   1.389 +
   1.390 +Errors may arise during the translation to {\ML} (say, a misspelled keyword)
   1.391 +or during creation of the new theory (say, a type error in a rule).  But if
   1.392 +all goes well, {\tt use_thy} will finally read the file {\it tf}{\tt.ML}, if
   1.393 +it exists.  This file typically begins with the {\ML} declaration {\tt
   1.394 +open}~$T$ and contains proofs that refer to the components of~$T$.
   1.395 +Theories can be defined directly by issuing {\ML} declarations to Isabelle,
   1.396 +but the calling sequences are extremely cumbersome.
   1.397 +
   1.398 +If theory~$T$ is later redeclared in order to delete an incorrect rule,
   1.399 +bindings to the old rule may persist.  Isabelle ensures that the old and
   1.400 +new versions of~$T$ are not involved in the same proof.  Attempting to
   1.401 +combine different versions of~$T$ yields the fatal error
   1.402 +\begin{ttbox} 
   1.403 +Attempt to merge different versions of theory: \(T\)
   1.404 +\end{ttbox}
   1.405 +
   1.406 +\subsection{Declaring constants and rules}
   1.407 +\indexbold{constants!declaring}\indexbold{rules!declaring}
   1.408 +Most theories simply declare constants and some rules.  The {\bf constant
   1.409 +declaration part} has the form
   1.410 +\begin{ttbox}
   1.411 +consts  \(c@1\) :: "\(\tau@1\)"
   1.412 +        \vdots
   1.413 +        \(c@n\) :: "\(\tau@n\)"
   1.414 +\end{ttbox}
   1.415 +where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are
   1.416 +types.  Each type {\em must\/} be enclosed in quotation marks.  Each
   1.417 +constant must be enclosed in quotation marks unless it is a valid
   1.418 +identifier.  To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$,
   1.419 +the $n$ declarations may be abbreviated to a single line:
   1.420 +\begin{ttbox}
   1.421 +        \(c@1\), \ldots, \(c@n\) :: "\(\tau\)"
   1.422 +\end{ttbox}
   1.423 +The {\bf rule declaration part} has the form
   1.424 +\begin{ttbox}
   1.425 +rules   \(id@1\) "\(rule@1\)"
   1.426 +        \vdots
   1.427 +        \(id@n\) "\(rule@n\)"
   1.428 +\end{ttbox}
   1.429 +where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,
   1.430 +$rule@n$ are expressions of type~$prop$.  {\bf Definitions} are rules of
   1.431 +the form $t\equiv u$.  Each rule {\em must\/} be enclosed in quotation marks.
   1.432 +
   1.433 +\index{examples!of theories}
   1.434 +This theory extends first-order logic with two constants {\em nand} and
   1.435 +{\em xor}, and two rules defining them:
   1.436 +\begin{ttbox} 
   1.437 +Gate = FOL +
   1.438 +consts  nand,xor :: "[o,o] => o"
   1.439 +rules   nand_def "nand(P,Q) == ~(P & Q)"
   1.440 +        xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
   1.441 +end
   1.442 +\end{ttbox}
   1.443 +
   1.444 +
   1.445 +\subsection{Declaring type constructors}
   1.446 +\indexbold{type constructors!declaring}\indexbold{arities!declaring}
   1.447 +Types are composed of type variables and {\bf type constructors}.  Each
   1.448 +type constructor has a fixed number of argument places.  For example,
   1.449 +$list$ is a 1-place type constructor and $nat$ is a 0-place type
   1.450 +constructor.
   1.451 +
   1.452 +The {\bf type declaration part} has the form
   1.453 +\begin{ttbox}
   1.454 +types   \(id@1\) \(k@1\)
   1.455 +        \vdots
   1.456 +        \(id@n\) \(k@n\)
   1.457 +\end{ttbox}
   1.458 +where $id@1$, \ldots, $id@n$ are identifiers and $k@1$, \ldots, $k@n$ are
   1.459 +natural numbers.  It declares each $id@i$ as a type constructor with $k@i$
   1.460 +argument places.
   1.461 +
   1.462 +The {\bf arity declaration part} has the form
   1.463 +\begin{ttbox}
   1.464 +arities \(tycon@1\) :: \(arity@1\)
   1.465 +        \vdots
   1.466 +        \(tycon@n\) :: \(arity@n\)
   1.467 +\end{ttbox}
   1.468 +where $tycon@1$, \ldots, $tycon@n$ are identifiers and $arity@1$, \ldots,
   1.469 +$arity@n$ are arities.  Arity declarations add arities to existing
   1.470 +types; they complement type declarations.
   1.471 +
   1.472 +In the simplest case, for an 0-place type constructor, an arity is simply
   1.473 +the type's class.  Let us declare a type~$bool$ of class $term$, with
   1.474 +constants $tt$ and~$ff$:\footnote{In first-order logic, booleans are
   1.475 +distinct from formulae, which have type $o::logic$.}
   1.476 +\index{examples!of theories}
   1.477 +\begin{ttbox} 
   1.478 +Bool = FOL +
   1.479 +types   bool 0
   1.480 +arities bool    :: term
   1.481 +consts  tt,ff   :: "bool"
   1.482 +end
   1.483 +\end{ttbox}
   1.484 +In the general case, type constructors take arguments.  Each type
   1.485 +constructor has an {\bf arity} with respect to
   1.486 +classes~(\S\ref{polymorphic}).  A $k$-place type constructor may have
   1.487 +arities of the form $(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts
   1.488 +and $c$ is a class.  Each sort specifies a type argument; it has the form
   1.489 +$\{c@1,\ldots,c@m\}$, where $c@1$, \dots,~$c@m$ are classes.  Mostly we
   1.490 +deal with singleton sorts, and may abbreviate them by dropping the braces.
   1.491 +The arity declaration $list{::}(term)term$ is short for
   1.492 +$list{::}(\{term\})term$.
   1.493 +
   1.494 +A type constructor may be overloaded (subject to certain conditions) by
   1.495 +appearing in several arity declarations.  For instance, the built-in type
   1.496 +constructor~$\To$ has the arity $(logic,logic)logic$; in higher-order
   1.497 +logic, it is declared also to have arity $(term,term)term$.
   1.498 +
   1.499 +Theory {\tt List} declares the 1-place type constructor $list$, gives
   1.500 +it arity $list{::}(term)term$, and declares constants $Nil$ and $Cons$ with
   1.501 +polymorphic types:
   1.502 +\index{examples!of theories}
   1.503 +\begin{ttbox} 
   1.504 +List = FOL +
   1.505 +types   list 1
   1.506 +arities list    :: (term)term
   1.507 +consts  Nil     :: "'a list"
   1.508 +        Cons    :: "['a, 'a list] => 'a list" 
   1.509 +end
   1.510 +\end{ttbox}
   1.511 +Multiple type and arity declarations may be abbreviated to a single line:
   1.512 +\begin{ttbox}
   1.513 +types   \(id@1\), \ldots, \(id@n\) \(k\)
   1.514 +arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)
   1.515 +\end{ttbox}
   1.516 +
   1.517 +\begin{warn}
   1.518 +Arity declarations resemble constant declarations, but there are {\it no\/}
   1.519 +quotation marks!  Types and rules must be quoted because the theory
   1.520 +translator passes them verbatim to the {\ML} output file.
   1.521 +\end{warn}
   1.522 +
   1.523 +\subsection{Infixes and Mixfixes}
   1.524 +\indexbold{infix operators}\index{examples!of theories}
   1.525 +The constant declaration part of the theory
   1.526 +\begin{ttbox} 
   1.527 +Gate2 = FOL +
   1.528 +consts  "~&"     :: "[o,o] => o"         (infixl 35)
   1.529 +        "#"      :: "[o,o] => o"         (infixl 30)
   1.530 +rules   nand_def "P ~& Q == ~(P & Q)"    
   1.531 +        xor_def  "P # Q  == P & ~Q | ~P & Q"
   1.532 +end
   1.533 +\end{ttbox}
   1.534 +declares two left-associating infix operators: $\nand$ of precedence~35 and
   1.535 +$\xor$ of precedence~30.  Hence $P \xor Q \xor R$ is parsed as $(P\xor
   1.536 +Q) \xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$.  Note the
   1.537 +quotation marks in \verb|"~&"| and \verb|"#"|.
   1.538 +
   1.539 +The constants \hbox{\verb|op ~&|} and \hbox{\verb|op #|} are declared
   1.540 +automatically, just as in \ML.  Hence you may write propositions like
   1.541 +\verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda
   1.542 +Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical.
   1.543 +
   1.544 +\indexbold{mixfix operators}
   1.545 +{\bf Mixfix} operators may have arbitrary context-free syntaxes.  For example
   1.546 +\begin{ttbox} 
   1.547 +    If :: "[o,o,o] => o"       ("if _ then _ else _")
   1.548 +\end{ttbox}
   1.549 +declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax
   1.550 +$if~P~then~Q~else~R$ instead of $If(P,Q,R)$.  Underscores denote argument
   1.551 +positions.  Pretty-printing information can be specified in order to
   1.552 +improve the layout of formulae with mixfix operations.  For details, see
   1.553 +{\em Isabelle's Object-Logics}.
   1.554 +
   1.555 +Mixfix declarations can be annotated with precedences, just like
   1.556 +infixes.  The example above is just a shorthand for
   1.557 +\begin{ttbox} 
   1.558 +    If :: "[o,o,o] => o"       ("if _ then _ else _" [0,0,0] 1000)
   1.559 +\end{ttbox}
   1.560 +The numeric components determine precedences.  The list of integers
   1.561 +defines, for each argument position, the minimal precedence an expression
   1.562 +at that position must have.  The final integer is the precedence of the
   1.563 +construct itself.  In the example above, any argument expression is
   1.564 +acceptable because precedences are non-negative, and conditionals may
   1.565 +appear everywhere because 1000 is the highest precedence.  On the other
   1.566 +hand,
   1.567 +\begin{ttbox} 
   1.568 +    If :: "[o,o,o] => o"       ("if _ then _ else _" [100,0,0] 99)
   1.569 +\end{ttbox}
   1.570 +defines a conditional whose first argument cannot be a conditional because it
   1.571 +must have a precedence of at least 100.  Precedences only apply to
   1.572 +mixfix syntax: we may write $If(If(P,Q,R),S,T)$.
   1.573 +
   1.574 +Binary type constructors, like products and sums, may also be declared as
   1.575 +infixes.  The type declaration below introduces a type constructor~$*$ with
   1.576 +infix notation $\alpha*\beta$, together with the mixfix notation
   1.577 +${<}\_,\_{>}$ for pairs.  
   1.578 +\index{examples!of theories}
   1.579 +\begin{ttbox}
   1.580 +Prod = FOL +
   1.581 +types   "*" 2                                 (infixl 20)
   1.582 +arities "*"     :: (term,term)term
   1.583 +consts  fst     :: "'a * 'b => 'a"
   1.584 +        snd     :: "'a * 'b => 'b"
   1.585 +        Pair    :: "['a,'b] => 'a * 'b"       ("(1<_,/_>)")
   1.586 +rules   fst     "fst(<a,b>) = a"
   1.587 +        snd     "snd(<a,b>) = b"
   1.588 +end
   1.589 +\end{ttbox}
   1.590 +
   1.591 +\begin{warn}
   1.592 +The name of the type constructor is~{\tt *} and not {\tt op~*}, as it would
   1.593 +be in the case of an infix constant.  Only infix type constructors can have
   1.594 +symbolic names like~{\tt *}.  There is no general mixfix syntax for types.
   1.595 +\end{warn}
   1.596 +
   1.597 +
   1.598 +\subsection{Overloading}
   1.599 +\index{overloading}\index{examples!of theories}
   1.600 +The {\bf class declaration part} has the form
   1.601 +\begin{ttbox}
   1.602 +classes \(id@1\) < \(c@1\)
   1.603 +        \vdots
   1.604 +        \(id@n\) < \(c@n\)
   1.605 +\end{ttbox}
   1.606 +where $id@1$, \ldots, $id@n$ are identifiers and $c@1$, \ldots, $c@n$ are
   1.607 +existing classes.  It declares each $id@i$ as a new class, a subclass
   1.608 +of~$c@i$.  In the general case, an identifier may be declared to be a
   1.609 +subclass of $k$ existing classes:
   1.610 +\begin{ttbox}
   1.611 +        \(id\) < \(c@1\), \ldots, \(c@k\)
   1.612 +\end{ttbox}
   1.613 +Type classes allow constants to be overloaded~(\S\ref{polymorphic}).  As an
   1.614 +example, we define the class $arith$ of ``arithmetic'' types with the
   1.615 +constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 :: \alpha$, for
   1.616 +$\alpha{::}arith$.  We introduce $arith$ as a subclass of $term$ and add
   1.617 +the three polymorphic constants of this class.
   1.618 +\index{examples!of theories}
   1.619 +\begin{ttbox}
   1.620 +Arith = FOL +
   1.621 +classes arith < term
   1.622 +consts  "0"     :: "'a::arith"                  ("0")
   1.623 +        "1"     :: "'a::arith"                  ("1")
   1.624 +        "+"     :: "['a::arith,'a] => 'a"       (infixl 60)
   1.625 +end
   1.626 +\end{ttbox}
   1.627 +No rules are declared for these constants: we merely introduce their
   1.628 +names without specifying properties.  On the other hand, classes
   1.629 +with rules make it possible to prove {\bf generic} theorems.  Such
   1.630 +theorems hold for all instances, all types in that class.
   1.631 +
   1.632 +We can now obtain distinct versions of the constants of $arith$ by
   1.633 +declaring certain types to be of class $arith$.  For example, let us
   1.634 +declare the 0-place type constructors $bool$ and $nat$:
   1.635 +\index{examples!of theories}
   1.636 +\begin{ttbox}
   1.637 +BoolNat = Arith +
   1.638 +types   bool,nat    0
   1.639 +arities bool,nat    :: arith
   1.640 +consts  Suc         :: "nat=>nat"
   1.641 +rules   add0        "0 + n = n::nat"
   1.642 +        addS        "Suc(m)+n = Suc(m+n)"
   1.643 +        nat1        "1 = Suc(0)"
   1.644 +        or0l        "0 + x = x::bool"
   1.645 +        or0r        "x + 0 = x::bool"
   1.646 +        or1l        "1 + x = 1::bool"
   1.647 +        or1r        "x + 1 = 1::bool"
   1.648 +end
   1.649 +\end{ttbox}
   1.650 +Because $nat$ and $bool$ have class $arith$, we can use $0$, $1$ and $+$ at
   1.651 +either type.  The type constraints in the axioms are vital.  Without
   1.652 +constraints, the $x$ in $1+x = x$ would have type $\alpha{::}arith$
   1.653 +and the axiom would hold for any type of class $arith$.  This would
   1.654 +collapse $nat$:
   1.655 +\[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \]
   1.656 +The class $arith$ as defined above is more specific than necessary.  Many
   1.657 +types come with a binary operation and identity~(0).  On lists,
   1.658 +$+$ could be concatenation and 0 the empty list --- but what is 1?  Hence it
   1.659 +may be better to define $+$ and 0 on $arith$ and introduce a separate
   1.660 +class, say $k$, containing~1.  Should $k$ be a subclass of $term$ or of
   1.661 +$arith$?  This depends on the structure of your theories; the design of an
   1.662 +appropriate class hierarchy may require some experimentation.
   1.663 +
   1.664 +We will now work through a small example of formalized mathematics
   1.665 +demonstrating many of the theory extension features.
   1.666 +
   1.667 +
   1.668 +\subsection{Extending first-order logic with the natural numbers}
   1.669 +\index{examples!of theories}
   1.670 +
   1.671 +The early part of this paper defines a first-order logic, including a
   1.672 +type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.  Let us
   1.673 +introduce the Peano axioms for mathematical induction and the freeness of
   1.674 +$0$ and~$Suc$:
   1.675 +\[ \vcenter{\infer[(induct)*]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
   1.676 + \qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}
   1.677 +\]
   1.678 +\[ \infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad
   1.679 +   \infer[(Suc\_neq\_0)]{R}{Suc(m)=0}
   1.680 +\]
   1.681 +Mathematical induction asserts that $P(n)$ is true, for any $n::nat$,
   1.682 +provided $P(0)$ holds and that $P(x)$ implies $P(Suc(x))$ for all~$x$.
   1.683 +Some authors express the induction step as $\forall x. P(x)\imp P(Suc(x))$.
   1.684 +To avoid making induction require the presence of other connectives, we
   1.685 +formalize mathematical induction as
   1.686 +$$ \List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n). \eqno(induct) $$
   1.687 +
   1.688 +\noindent
   1.689 +Similarly, to avoid expressing the other rules using~$\forall$, $\imp$
   1.690 +and~$\neg$, we take advantage of the meta-logic;\footnote
   1.691 +{On the other hand, the axioms $Suc(m)=Suc(n) \bimp m=n$
   1.692 +and $\neg(Suc(m)=0)$ are logically equivalent to those given, and work
   1.693 +better with Isabelle's simplifier.} 
   1.694 +$(Suc\_neq\_0)$ is
   1.695 +an elimination rule for $Suc(m)=0$:
   1.696 +$$ Suc(m)=Suc(n) \Imp m=n  \eqno(Suc\_inject) $$
   1.697 +$$ Suc(m)=0      \Imp R    \eqno(Suc\_neq\_0) $$
   1.698 +
   1.699 +\noindent
   1.700 +We shall also define a primitive recursion operator, $rec$.  Traditionally,
   1.701 +primitive recursion takes a natural number~$a$ and a 2-place function~$f$,
   1.702 +and obeys the equations
   1.703 +\begin{eqnarray*}
   1.704 +  rec(0,a,f)            & = & a \\
   1.705 +  rec(Suc(m),a,f)       & = & f(m, rec(m,a,f))
   1.706 +\end{eqnarray*}
   1.707 +Addition, defined by $m+n \equiv rec(m,n,\lambda x\,y.Suc(y))$,
   1.708 +should satisfy
   1.709 +\begin{eqnarray*}
   1.710 +  0+n      & = & n \\
   1.711 +  Suc(m)+n & = & Suc(m+n)
   1.712 +\end{eqnarray*}
   1.713 +This appears to pose difficulties: first-order logic has no functions.
   1.714 +Following the previous examples, we take advantage of the meta-logic, which
   1.715 +does have functions.  We also generalise primitive recursion to be
   1.716 +polymorphic over any type of class~$term$, and declare the addition
   1.717 +function:
   1.718 +\begin{eqnarray*}
   1.719 +  rec   & :: & [nat, \alpha{::}term, [nat,\alpha]\To\alpha] \To\alpha \\
   1.720 +  +     & :: & [nat,nat]\To nat 
   1.721 +\end{eqnarray*}
   1.722 +
   1.723 +
   1.724 +\subsection{Declaring the theory to Isabelle}
   1.725 +\index{examples!of theories}
   1.726 +Let us create the theory \ttindexbold{Nat} starting from theory~\verb$FOL$,
   1.727 +which contains only classical logic with no natural numbers.  We declare
   1.728 +the 0-place type constructor $nat$ and the constants $rec$ and~$Suc$:
   1.729 +\begin{ttbox}
   1.730 +Nat = FOL +
   1.731 +types   nat 0
   1.732 +arities nat         :: term
   1.733 +consts  "0"         :: "nat"    ("0")
   1.734 +        Suc         :: "nat=>nat"
   1.735 +        rec         :: "[nat, 'a, [nat,'a]=>'a] => 'a"
   1.736 +        "+"         :: "[nat, nat] => nat"              (infixl 60)
   1.737 +rules   induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
   1.738 +        Suc_inject  "Suc(m)=Suc(n) ==> m=n"
   1.739 +        Suc_neq_0   "Suc(m)=0      ==> R"
   1.740 +        rec_0       "rec(0,a,f) = a"
   1.741 +        rec_Suc     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
   1.742 +        add_def     "m+n == rec(m, n, %x y. Suc(y))"
   1.743 +end
   1.744 +\end{ttbox}
   1.745 +In axiom {\tt add_def}, recall that \verb|%| stands for~$\lambda$.
   1.746 +Opening the \ML\ structure {\tt Nat} permits reference to the axioms by \ML\
   1.747 +identifiers; we may write {\tt induct} instead of {\tt Nat.induct}.
   1.748 +\begin{ttbox}
   1.749 +open Nat;
   1.750 +\end{ttbox}
   1.751 +File {\tt FOL/ex/nat.ML} contains proofs involving this theory of the
   1.752 +natural numbers.  As a trivial example, let us derive recursion equations
   1.753 +for \verb$+$.  Here is the zero case:
   1.754 +\begin{ttbox} 
   1.755 +goalw Nat.thy [add_def] "0+n = n";
   1.756 +{\out Level 0}
   1.757 +{\out 0 + n = n}
   1.758 +{\out  1. rec(0,n,%x y. Suc(y)) = n}
   1.759 +\ttbreak
   1.760 +by (resolve_tac [rec_0] 1);
   1.761 +{\out Level 1}
   1.762 +{\out 0 + n = n}
   1.763 +{\out No subgoals!}
   1.764 +val add_0 = result();
   1.765 +\end{ttbox} 
   1.766 +And here is the successor case:
   1.767 +\begin{ttbox} 
   1.768 +goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
   1.769 +{\out Level 0}
   1.770 +{\out Suc(m) + n = Suc(m + n)}
   1.771 +{\out  1. rec(Suc(m),n,%x y. Suc(y)) = Suc(rec(m,n,%x y. Suc(y)))}
   1.772 +\ttbreak
   1.773 +by (resolve_tac [rec_Suc] 1);
   1.774 +{\out Level 1}
   1.775 +{\out Suc(m) + n = Suc(m + n)}
   1.776 +{\out No subgoals!}
   1.777 +val add_Suc = result();
   1.778 +\end{ttbox} 
   1.779 +The induction rule raises some complications, which are discussed next.
   1.780 +\index{theories!defining|)}
   1.781 +
   1.782 +
   1.783 +\section{Refinement with explicit instantiation}
   1.784 +\index{refinement!with instantiation|bold}
   1.785 +\index{instantiation!explicit|bold}
   1.786 +In order to employ mathematical induction, we need to refine a subgoal by
   1.787 +the rule~$(induct)$.  The conclusion of this rule is $\Var{P}(\Var{n})$,
   1.788 +which is highly ambiguous in higher-order unification.  It matches every
   1.789 +way that a formula can be regarded as depending on a subterm of type~$nat$.
   1.790 +To get round this problem, we could make the induction rule conclude
   1.791 +$\forall n.\Var{P}(n)$ --- but putting a subgoal into this form requires
   1.792 +refinement by~$(\forall E)$, which is equally hard!
   1.793 +
   1.794 +The tactic {\tt res_inst_tac}, like {\tt resolve_tac}, refines a subgoal by
   1.795 +a rule.  But it also accepts explicit instantiations for the rule's
   1.796 +schematic variables.  
   1.797 +\begin{description}
   1.798 +\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
   1.799 +instantiates the rule {\it thm} with the instantiations {\it insts}, and
   1.800 +then performs resolution on subgoal~$i$.
   1.801 +
   1.802 +\item[\ttindexbold{eres_inst_tac}] 
   1.803 +and \ttindexbold{dres_inst_tac} are similar, but perform elim-resolution
   1.804 +and destruct-resolution, respectively.
   1.805 +\end{description}
   1.806 +The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,
   1.807 +where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule ---
   1.808 +with {\bf no} leading question marks!! --- and $e@1$, \ldots, $e@n$ are
   1.809 +expressions giving their instantiations.  The expressions are type-checked
   1.810 +in the context of a particular subgoal: free variables receive the same
   1.811 +types as they have in the subgoal, and parameters may appear.  Type
   1.812 +variable instantiations may appear in~{\it insts}, but they are seldom
   1.813 +required: {\tt res_inst_tac} instantiates type variables automatically
   1.814 +whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$.
   1.815 +
   1.816 +\subsection{A simple proof by induction}
   1.817 +\index{proof!by induction}\index{examples!of induction}
   1.818 +Let us prove that no natural number~$k$ equals its own successor.  To
   1.819 +use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good
   1.820 +instantiation for~$\Var{P}$.
   1.821 +\begin{ttbox} 
   1.822 +goal Nat.thy "~ (Suc(k) = k)";
   1.823 +{\out Level 0}
   1.824 +{\out ~Suc(k) = k}
   1.825 +{\out  1. ~Suc(k) = k}
   1.826 +\ttbreak
   1.827 +by (res_inst_tac [("n","k")] induct 1);
   1.828 +{\out Level 1}
   1.829 +{\out ~Suc(k) = k}
   1.830 +{\out  1. ~Suc(0) = 0}
   1.831 +{\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
   1.832 +\end{ttbox} 
   1.833 +We should check that Isabelle has correctly applied induction.  Subgoal~1
   1.834 +is the base case, with $k$ replaced by~0.  Subgoal~2 is the inductive step,
   1.835 +with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.
   1.836 +The rest of the proof demonstrates~\ttindex{notI}, \ttindex{notE} and the
   1.837 +other rules of~\ttindex{Nat.thy}.  The base case holds by~\ttindex{Suc_neq_0}:
   1.838 +\begin{ttbox} 
   1.839 +by (resolve_tac [notI] 1);
   1.840 +{\out Level 2}
   1.841 +{\out ~Suc(k) = k}
   1.842 +{\out  1. Suc(0) = 0 ==> False}
   1.843 +{\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
   1.844 +\ttbreak
   1.845 +by (eresolve_tac [Suc_neq_0] 1);
   1.846 +{\out Level 3}
   1.847 +{\out ~Suc(k) = k}
   1.848 +{\out  1. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
   1.849 +\end{ttbox} 
   1.850 +The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
   1.851 +Using the negation rule, we assume $Suc(Suc(x)) = Suc(x)$ and prove $Suc(x)=x$:
   1.852 +\begin{ttbox} 
   1.853 +by (resolve_tac [notI] 1);
   1.854 +{\out Level 4}
   1.855 +{\out ~Suc(k) = k}
   1.856 +{\out  1. !!x. [| ~Suc(x) = x; Suc(Suc(x)) = Suc(x) |] ==> False}
   1.857 +\ttbreak
   1.858 +by (eresolve_tac [notE] 1);
   1.859 +{\out Level 5}
   1.860 +{\out ~Suc(k) = k}
   1.861 +{\out  1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
   1.862 +\ttbreak
   1.863 +by (eresolve_tac [Suc_inject] 1);
   1.864 +{\out Level 6}
   1.865 +{\out ~Suc(k) = k}
   1.866 +{\out No subgoals!}
   1.867 +\end{ttbox} 
   1.868 +
   1.869 +
   1.870 +\subsection{An example of ambiguity in {\tt resolve_tac}}
   1.871 +\index{examples!of induction}\index{unification!higher-order}
   1.872 +If you try the example above, you may observe that {\tt res_inst_tac} is
   1.873 +not actually needed.  Almost by chance, \ttindex{resolve_tac} finds the right
   1.874 +instantiation for~$(induct)$ to yield the desired next state.  With more
   1.875 +complex formulae, our luck fails.  
   1.876 +\begin{ttbox} 
   1.877 +goal Nat.thy "(k+m)+n = k+(m+n)";
   1.878 +{\out Level 0}
   1.879 +{\out k + m + n = k + (m + n)}
   1.880 +{\out  1. k + m + n = k + (m + n)}
   1.881 +\ttbreak
   1.882 +by (resolve_tac [induct] 1);
   1.883 +{\out Level 1}
   1.884 +{\out k + m + n = k + (m + n)}
   1.885 +{\out  1. k + m + n = 0}
   1.886 +{\out  2. !!x. k + m + n = x ==> k + m + n = Suc(x)}
   1.887 +\end{ttbox} 
   1.888 +This proof requires induction on~$k$.  But the 0 in subgoal~1 indicates
   1.889 +that induction has been applied to the term~$k+(m+n)$.  The
   1.890 +\ttindex{back} command causes backtracking to an alternative
   1.891 +outcome of the tactic.  
   1.892 +\begin{ttbox} 
   1.893 +back();
   1.894 +{\out Level 1}
   1.895 +{\out k + m + n = k + (m + n)}
   1.896 +{\out  1. k + m + n = k + 0}
   1.897 +{\out  2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)}
   1.898 +\end{ttbox} 
   1.899 +Now induction has been applied to~$m+n$.  Let us call \ttindex{back}
   1.900 +again.
   1.901 +\begin{ttbox} 
   1.902 +back();
   1.903 +{\out Level 1}
   1.904 +{\out k + m + n = k + (m + n)}
   1.905 +{\out  1. k + m + 0 = k + (m + 0)}
   1.906 +{\out  2. !!x. k + m + x = k + (m + x) ==> k + m + Suc(x) = k + (m + Suc(x))}
   1.907 +\end{ttbox} 
   1.908 +Now induction has been applied to~$n$.  What is the next alternative?
   1.909 +\begin{ttbox} 
   1.910 +back();
   1.911 +{\out Level 1}
   1.912 +{\out k + m + n = k + (m + n)}
   1.913 +{\out  1. k + m + n = k + (m + 0)}
   1.914 +{\out  2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))}
   1.915 +\end{ttbox} 
   1.916 +Inspecting subgoal~1 reveals that induction has been applied to just the
   1.917 +second occurrence of~$n$.  This perfectly legitimate induction is useless
   1.918 +here.  The main goal admits fourteen different applications of induction.
   1.919 +The number is exponential in the size of the formula.
   1.920 +
   1.921 +\subsection{Proving that addition is associative}
   1.922 +\index{associativity of addition}
   1.923 +\index{examples!of rewriting}
   1.924 +Let us do the proof properly, using~\ttindex{res_inst_tac}.  At the same
   1.925 +time, we shall have a glimpse at Isabelle's rewriting tactics, which are
   1.926 +described in the {\em Reference Manual}.
   1.927 +
   1.928 +\index{rewriting!object-level} 
   1.929 +Isabelle's rewriting tactics repeatedly applies equations to a subgoal,
   1.930 +simplifying or proving it.  For efficiency, the rewriting rules must be
   1.931 +packaged into a \bfindex{simplification set}.  Let us include the equations
   1.932 +for~{\tt add} proved in the previous section, namely $0+n=n$ and ${\tt
   1.933 +  Suc}(m)+n={\tt Suc}(m+n)$: 
   1.934 +\begin{ttbox} 
   1.935 +val add_ss = FOL_ss addrews [add_0, add_Suc];
   1.936 +\end{ttbox} 
   1.937 +We state the goal for associativity of addition, and
   1.938 +use \ttindex{res_inst_tac} to invoke induction on~$k$:
   1.939 +\begin{ttbox} 
   1.940 +goal Nat.thy "(k+m)+n = k+(m+n)";
   1.941 +{\out Level 0}
   1.942 +{\out k + m + n = k + (m + n)}
   1.943 +{\out  1. k + m + n = k + (m + n)}
   1.944 +\ttbreak
   1.945 +by (res_inst_tac [("n","k")] induct 1);
   1.946 +{\out Level 1}
   1.947 +{\out k + m + n = k + (m + n)}
   1.948 +{\out  1. 0 + m + n = 0 + (m + n)}
   1.949 +{\out  2. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)}
   1.950 +\end{ttbox} 
   1.951 +The base case holds easily; both sides reduce to $m+n$.  The
   1.952 +tactic~\ttindex{simp_tac} rewrites with respect to the given simplification
   1.953 +set, applying the rewrite rules for~{\tt +}:
   1.954 +\begin{ttbox} 
   1.955 +by (simp_tac add_ss 1);
   1.956 +{\out Level 2}
   1.957 +{\out k + m + n = k + (m + n)}
   1.958 +{\out  1. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)}
   1.959 +\end{ttbox} 
   1.960 +The inductive step requires rewriting by the equations for~{\tt add}
   1.961 +together the induction hypothesis, which is also an equation.  The
   1.962 +tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any
   1.963 +useful assumptions:
   1.964 +\begin{ttbox} 
   1.965 +by (asm_simp_tac add_ss 1);
   1.966 +{\out Level 3}
   1.967 +{\out k + m + n = k + (m + n)}
   1.968 +{\out No subgoals!}
   1.969 +\end{ttbox} 
   1.970 +
   1.971 +
   1.972 +\section{A {\sc Prolog} interpreter}
   1.973 +\index{Prolog interpreter|bold}
   1.974 +To demonstrate the power of tacticals, let us construct a {\sc Prolog}
   1.975 +interpreter and execute programs involving lists.\footnote{To run these
   1.976 +examples, see the file {\tt FOL/ex/prolog.ML}.} The {\sc Prolog} program
   1.977 +consists of a theory.  We declare a type constructor for lists, with an
   1.978 +arity declaration to say that $(\tau)list$ is of class~$term$
   1.979 +provided~$\tau$ is:
   1.980 +\begin{eqnarray*}
   1.981 +  list  & :: & (term)term
   1.982 +\end{eqnarray*}
   1.983 +We declare four constants: the empty list~$Nil$; the infix list
   1.984 +constructor~{:}; the list concatenation predicate~$app$; the list reverse
   1.985 +predicate~$rev$.  (In {\sc Prolog}, functions on lists are expressed as
   1.986 +predicates.)
   1.987 +\begin{eqnarray*}
   1.988 +    Nil         & :: & \alpha list \\
   1.989 +    {:}         & :: & [\alpha,\alpha list] \To \alpha list \\
   1.990 +    app & :: & [\alpha list,\alpha list,\alpha list] \To o \\
   1.991 +    rev & :: & [\alpha list,\alpha list] \To o 
   1.992 +\end{eqnarray*}
   1.993 +The predicate $app$ should satisfy the {\sc Prolog}-style rules
   1.994 +\[ {app(Nil,ys,ys)} \qquad
   1.995 +   {app(xs,ys,zs) \over app(x:xs, ys, x:zs)} \]
   1.996 +We define the naive version of $rev$, which calls~$app$:
   1.997 +\[ {rev(Nil,Nil)} \qquad
   1.998 +   {rev(xs,ys)\quad  app(ys, x:Nil, zs) \over
   1.999 +    rev(x:xs, zs)} 
  1.1000 +\]
  1.1001 +
  1.1002 +\index{examples!of theories}
  1.1003 +Theory \ttindex{Prolog} extends first-order logic in order to make use
  1.1004 +of the class~$term$ and the type~$o$.  The interpreter does not use the
  1.1005 +rules of~\ttindex{FOL}.
  1.1006 +\begin{ttbox}
  1.1007 +Prolog = FOL +
  1.1008 +types   list 1
  1.1009 +arities list    :: (term)term
  1.1010 +consts  Nil     :: "'a list"
  1.1011 +        ":"     :: "['a, 'a list]=> 'a list"            (infixr 60)
  1.1012 +        app     :: "['a list, 'a list, 'a list] => o"
  1.1013 +        rev     :: "['a list, 'a list] => o"
  1.1014 +rules   appNil  "app(Nil,ys,ys)"
  1.1015 +        appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
  1.1016 +        revNil  "rev(Nil,Nil)"
  1.1017 +        revCons "[| rev(xs,ys); app(ys,x:Nil,zs) |] ==> rev(x:xs,zs)"
  1.1018 +end
  1.1019 +\end{ttbox}
  1.1020 +\subsection{Simple executions}
  1.1021 +Repeated application of the rules solves {\sc Prolog} goals.  Let us
  1.1022 +append the lists $[a,b,c]$ and~$[d,e]$.  As the rules are applied, the
  1.1023 +answer builds up in~{\tt ?x}.
  1.1024 +\begin{ttbox}
  1.1025 +goal Prolog.thy "app(a:b:c:Nil, d:e:Nil, ?x)";
  1.1026 +{\out Level 0}
  1.1027 +{\out app(a : b : c : Nil, d : e : Nil, ?x)}
  1.1028 +{\out  1. app(a : b : c : Nil, d : e : Nil, ?x)}
  1.1029 +\ttbreak
  1.1030 +by (resolve_tac [appNil,appCons] 1);
  1.1031 +{\out Level 1}
  1.1032 +{\out app(a : b : c : Nil, d : e : Nil, a : ?zs1)}
  1.1033 +{\out  1. app(b : c : Nil, d : e : Nil, ?zs1)}
  1.1034 +\ttbreak
  1.1035 +by (resolve_tac [appNil,appCons] 1);
  1.1036 +{\out Level 2}
  1.1037 +{\out app(a : b : c : Nil, d : e : Nil, a : b : ?zs2)}
  1.1038 +{\out  1. app(c : Nil, d : e : Nil, ?zs2)}
  1.1039 +\end{ttbox}
  1.1040 +At this point, the first two elements of the result are~$a$ and~$b$.
  1.1041 +\begin{ttbox}
  1.1042 +by (resolve_tac [appNil,appCons] 1);
  1.1043 +{\out Level 3}
  1.1044 +{\out app(a : b : c : Nil, d : e : Nil, a : b : c : ?zs3)}
  1.1045 +{\out  1. app(Nil, d : e : Nil, ?zs3)}
  1.1046 +\ttbreak
  1.1047 +by (resolve_tac [appNil,appCons] 1);
  1.1048 +{\out Level 4}
  1.1049 +{\out app(a : b : c : Nil, d : e : Nil, a : b : c : d : e : Nil)}
  1.1050 +{\out No subgoals!}
  1.1051 +\end{ttbox}
  1.1052 +
  1.1053 +{\sc Prolog} can run functions backwards.  Which list can be appended
  1.1054 +with $[c,d]$ to produce $[a,b,c,d]$?
  1.1055 +Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$:
  1.1056 +\begin{ttbox}
  1.1057 +goal Prolog.thy "app(?x, c:d:Nil, a:b:c:d:Nil)";
  1.1058 +{\out Level 0}
  1.1059 +{\out app(?x, c : d : Nil, a : b : c : d : Nil)}
  1.1060 +{\out  1. app(?x, c : d : Nil, a : b : c : d : Nil)}
  1.1061 +\ttbreak
  1.1062 +by (REPEAT (resolve_tac [appNil,appCons] 1));
  1.1063 +{\out Level 1}
  1.1064 +{\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
  1.1065 +{\out No subgoals!}
  1.1066 +\end{ttbox}
  1.1067 +
  1.1068 +
  1.1069 +\subsection{Backtracking}
  1.1070 +\index{backtracking}
  1.1071 +Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$?
  1.1072 +Using \ttindex{REPEAT} to apply the rules, we quickly find the solution
  1.1073 +$x=[]$ and $y=[a,b,c,d]$:
  1.1074 +\begin{ttbox}
  1.1075 +goal Prolog.thy "app(?x, ?y, a:b:c:d:Nil)";
  1.1076 +{\out Level 0}
  1.1077 +{\out app(?x, ?y, a : b : c : d : Nil)}
  1.1078 +{\out  1. app(?x, ?y, a : b : c : d : Nil)}
  1.1079 +\ttbreak
  1.1080 +by (REPEAT (resolve_tac [appNil,appCons] 1));
  1.1081 +{\out Level 1}
  1.1082 +{\out app(Nil, a : b : c : d : Nil, a : b : c : d : Nil)}
  1.1083 +{\out No subgoals!}
  1.1084 +\end{ttbox}
  1.1085 +The \ttindex{back} command returns the tactic's next outcome,
  1.1086 +$x=[a]$ and $y=[b,c,d]$:
  1.1087 +\begin{ttbox}
  1.1088 +back();
  1.1089 +{\out Level 1}
  1.1090 +{\out app(a : Nil, b : c : d : Nil, a : b : c : d : Nil)}
  1.1091 +{\out No subgoals!}
  1.1092 +\end{ttbox}
  1.1093 +The other solutions are generated similarly.
  1.1094 +\begin{ttbox}
  1.1095 +back();
  1.1096 +{\out Level 1}
  1.1097 +{\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
  1.1098 +{\out No subgoals!}
  1.1099 +\ttbreak
  1.1100 +back();
  1.1101 +{\out Level 1}
  1.1102 +{\out app(a : b : c : Nil, d : Nil, a : b : c : d : Nil)}
  1.1103 +{\out No subgoals!}
  1.1104 +\ttbreak
  1.1105 +back();
  1.1106 +{\out Level 1}
  1.1107 +{\out app(a : b : c : d : Nil, Nil, a : b : c : d : Nil)}
  1.1108 +{\out No subgoals!}
  1.1109 +\end{ttbox}
  1.1110 +
  1.1111 +
  1.1112 +\subsection{Depth-first search}
  1.1113 +\index{search!depth-first}
  1.1114 +Now let us try $rev$, reversing a list.
  1.1115 +Bundle the rules together as the \ML{} identifier {\tt rules}.  Naive
  1.1116 +reverse requires 120 inferences for this 14-element list, but the tactic
  1.1117 +terminates in a few seconds.
  1.1118 +\begin{ttbox}
  1.1119 +goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
  1.1120 +{\out Level 0}
  1.1121 +{\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)}
  1.1122 +{\out  1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)}
  1.1123 +val rules = [appNil,appCons,revNil,revCons];
  1.1124 +\ttbreak
  1.1125 +by (REPEAT (resolve_tac rules 1));
  1.1126 +{\out Level 1}
  1.1127 +{\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
  1.1128 +{\out     n : m : l : k : j : i : h : g : f : e : d : c : b : a : Nil)}
  1.1129 +{\out No subgoals!}
  1.1130 +\end{ttbox}
  1.1131 +We may execute $rev$ backwards.  This, too, should reverse a list.  What
  1.1132 +is the reverse of $[a,b,c]$?
  1.1133 +\begin{ttbox}
  1.1134 +goal Prolog.thy "rev(?x, a:b:c:Nil)";
  1.1135 +{\out Level 0}
  1.1136 +{\out rev(?x, a : b : c : Nil)}
  1.1137 +{\out  1. rev(?x, a : b : c : Nil)}
  1.1138 +\ttbreak
  1.1139 +by (REPEAT (resolve_tac rules 1));
  1.1140 +{\out Level 1}
  1.1141 +{\out rev(?x1 : Nil, a : b : c : Nil)}
  1.1142 +{\out  1. app(Nil, ?x1 : Nil, a : b : c : Nil)}
  1.1143 +\end{ttbox}
  1.1144 +The tactic has failed to find a solution!  It reached a dead end at
  1.1145 +subgoal~1: there is no~$\Var{x1}$ such that [] appended with~$[\Var{x1}]$
  1.1146 +equals~$[a,b,c]$.  Backtracking explores other outcomes.
  1.1147 +\begin{ttbox}
  1.1148 +back();
  1.1149 +{\out Level 1}
  1.1150 +{\out rev(?x1 : a : Nil, a : b : c : Nil)}
  1.1151 +{\out  1. app(Nil, ?x1 : Nil, b : c : Nil)}
  1.1152 +\end{ttbox}
  1.1153 +This too is a dead end, but the next outcome is successful.
  1.1154 +\begin{ttbox}
  1.1155 +back();
  1.1156 +{\out Level 1}
  1.1157 +{\out rev(c : b : a : Nil, a : b : c : Nil)}
  1.1158 +{\out No subgoals!}
  1.1159 +\end{ttbox}
  1.1160 +\ttindex{REPEAT} stops when it cannot continue, regardless of which state
  1.1161 +is reached.  The tactical \ttindex{DEPTH_FIRST} searches for a satisfactory
  1.1162 +state, as specified by an \ML{} predicate.  Below,
  1.1163 +\ttindex{has_fewer_prems} specifies that the proof state should have no
  1.1164 +subgoals.  
  1.1165 +\begin{ttbox}
  1.1166 +val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) 
  1.1167 +                             (resolve_tac rules 1);
  1.1168 +\end{ttbox}
  1.1169 +Since {\sc Prolog} uses depth-first search, this tactic is a (slow!) {\sc
  1.1170 +Prolog} interpreter.  We return to the start of the proof (using
  1.1171 +\ttindex{choplev}), and apply {\tt prolog_tac}:
  1.1172 +\begin{ttbox}
  1.1173 +choplev 0;
  1.1174 +{\out Level 0}
  1.1175 +{\out rev(?x, a : b : c : Nil)}
  1.1176 +{\out  1. rev(?x, a : b : c : Nil)}
  1.1177 +\ttbreak
  1.1178 +by (DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1));
  1.1179 +{\out Level 1}
  1.1180 +{\out rev(c : b : a : Nil, a : b : c : Nil)}
  1.1181 +{\out No subgoals!}
  1.1182 +\end{ttbox}
  1.1183 +Let us try {\tt prolog_tac} on one more example, containing four unknowns:
  1.1184 +\begin{ttbox}
  1.1185 +goal Prolog.thy "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
  1.1186 +{\out Level 0}
  1.1187 +{\out rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
  1.1188 +{\out  1. rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
  1.1189 +\ttbreak
  1.1190 +by prolog_tac;
  1.1191 +{\out Level 1}
  1.1192 +{\out rev(a : b : c : d : Nil, d : c : b : a : Nil)}
  1.1193 +{\out No subgoals!}
  1.1194 +\end{ttbox}
  1.1195 +Although Isabelle is much slower than a {\sc Prolog} system, many
  1.1196 +Isabelle tactics exploit logic programming techniques.  For instance, the
  1.1197 +simplification tactics prove subgoals of the form $t=\Var{x}$, rewriting~$t$
  1.1198 +and placing the normalised result in~$\Var{x}$.
  1.1199 +% Local Variables: 
  1.1200 +% mode: latex
  1.1201 +% TeX-master: t
  1.1202 +% End: 
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/Intro/arith.thy	Wed Nov 10 05:06:55 1993 +0100
     2.3 @@ -0,0 +1,6 @@
     2.4 +Arith = FOL +
     2.5 +classes arith < term
     2.6 +consts  "0"     :: "'a::arith"                  ("0")
     2.7 +        "1"     :: "'a::arith"                  ("1")
     2.8 +        "+"     :: "['a::arith,'a] => 'a"       (infixl 60)
     2.9 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/Intro/bool.thy	Wed Nov 10 05:06:55 1993 +0100
     3.3 @@ -0,0 +1,5 @@
     3.4 +Bool = FOL +
     3.5 +types 	bool 0
     3.6 +arities bool 	:: term
     3.7 +consts tt,ff	:: "bool"
     3.8 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/Intro/bool_nat.thy	Wed Nov 10 05:06:55 1993 +0100
     4.3 @@ -0,0 +1,12 @@
     4.4 +BoolNat = Arith +
     4.5 +types   bool,nat    0
     4.6 +arities bool,nat    :: arith
     4.7 +consts  Suc         :: "nat=>nat"
     4.8 +rules   add0        "0 + n = n::nat"
     4.9 +        addS        "Suc(m)+n = Suc(m+n)"
    4.10 +        nat1        "1 = Suc(0)"
    4.11 +        or0l        "0 + x = x::bool"
    4.12 +        or0r        "x + 0 = x::bool"
    4.13 +        or1l        "1 + x = 1::bool"
    4.14 +        or1r        "x + 1 = 1::bool"
    4.15 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/Intro/deriv.txt	Wed Nov 10 05:06:55 1993 +0100
     5.3 @@ -0,0 +1,210 @@
     5.4 +(* Deriving an inference rule *)
     5.5 +
     5.6 +Pretty.setmargin 72;  (*existing macros just allow this margin*)
     5.7 +print_depth 0;
     5.8 +
     5.9 +
    5.10 +val [major,minor] = goal Int_Rule.thy
    5.11 +    "[| P&Q;  [| P; Q |] ==> R |] ==> R";
    5.12 +prth minor;
    5.13 +by (resolve_tac [minor] 1);
    5.14 +prth major;
    5.15 +prth (major RS conjunct1);
    5.16 +by (resolve_tac [major RS conjunct1] 1);
    5.17 +prth (major RS conjunct2);
    5.18 +by (resolve_tac [major RS conjunct2] 1);
    5.19 +prth (topthm());
    5.20 +val conjE = prth(result());
    5.21 +
    5.22 +
    5.23 +- val [major,minor] = goal Int_Rule.thy
    5.24 +=     "[| P&Q;  [| P; Q |] ==> R |] ==> R";
    5.25 +Level 0
    5.26 +R
    5.27 + 1. R
    5.28 +val major = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
    5.29 +val minor = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
    5.30 +- prth minor;
    5.31 +[| P; Q |] ==> R  [[| P; Q |] ==> R]
    5.32 +- by (resolve_tac [minor] 1);
    5.33 +Level 1
    5.34 +R
    5.35 + 1. P
    5.36 + 2. Q
    5.37 +- prth major;
    5.38 +P & Q  [P & Q]
    5.39 +- prth (major RS conjunct1);
    5.40 +P  [P & Q]
    5.41 +- by (resolve_tac [major RS conjunct1] 1);
    5.42 +Level 2
    5.43 +R
    5.44 + 1. Q
    5.45 +- prth (major RS conjunct2);
    5.46 +Q  [P & Q]
    5.47 +- by (resolve_tac [major RS conjunct2] 1);
    5.48 +Level 3
    5.49 +R
    5.50 +No subgoals!
    5.51 +- prth (topthm());
    5.52 +R  [P & Q, P & Q, [| P; Q |] ==> R]
    5.53 +- val conjE = prth(result());
    5.54 +[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R
    5.55 +val conjE = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
    5.56 +
    5.57 +
    5.58 +(*** Derived rules involving definitions ***)
    5.59 +
    5.60 +(** notI **)
    5.61 +
    5.62 +val prems = goal Int_Rule.thy "(P ==> False) ==> ~P";
    5.63 +prth not_def;
    5.64 +by (rewrite_goals_tac [not_def]);
    5.65 +by (resolve_tac [impI] 1);
    5.66 +by (resolve_tac prems 1);
    5.67 +by (assume_tac 1);
    5.68 +val notI = prth(result());
    5.69 +
    5.70 +val prems = goalw Int_Rule.thy [not_def]
    5.71 +    "(P ==> False) ==> ~P";
    5.72 +
    5.73 +
    5.74 +- prth not_def;
    5.75 +~?P == ?P --> False
    5.76 +- val prems = goal Int_Rule.thy "(P ==> False) ==> ~P";
    5.77 +Level 0
    5.78 +~P
    5.79 + 1. ~P
    5.80 +- by (rewrite_goals_tac [not_def]);
    5.81 +Level 1
    5.82 +~P
    5.83 + 1. P --> False
    5.84 +- by (resolve_tac [impI] 1);
    5.85 +Level 2
    5.86 +~P
    5.87 + 1. P ==> False
    5.88 +- by (resolve_tac prems 1);
    5.89 +Level 3
    5.90 +~P
    5.91 + 1. P ==> P
    5.92 +- by (assume_tac 1);
    5.93 +Level 4
    5.94 +~P
    5.95 +No subgoals!
    5.96 +- val notI = prth(result());
    5.97 +(?P ==> False) ==> ~?P
    5.98 +val notI = # : thm
    5.99 +
   5.100 +- val prems = goalw Int_Rule.thy [not_def]
   5.101 +=     "(P ==> False) ==> ~P";
   5.102 +Level 0
   5.103 +~P
   5.104 + 1. P --> False
   5.105 +
   5.106 +
   5.107 +(** notE **)
   5.108 +
   5.109 +val [major,minor] = goal Int_Rule.thy "[| ~P;  P |] ==> R";
   5.110 +by (resolve_tac [FalseE] 1);
   5.111 +by (resolve_tac [mp] 1);
   5.112 +prth (rewrite_rule [not_def] major);
   5.113 +by (resolve_tac [it] 1);
   5.114 +by (resolve_tac [minor] 1);
   5.115 +val notE = prth(result());
   5.116 +
   5.117 +val [major,minor] = goalw Int_Rule.thy [not_def]
   5.118 +    "[| ~P;  P |] ==> R";
   5.119 +prth (minor RS (major RS mp RS FalseE));
   5.120 +by (resolve_tac [it] 1);
   5.121 +
   5.122 +
   5.123 +val prems = goalw Int_Rule.thy [not_def]
   5.124 +    "[| ~P;  P |] ==> R";
   5.125 +prths prems;
   5.126 +by (resolve_tac [FalseE] 1);
   5.127 +by (resolve_tac [mp] 1);
   5.128 +by (resolve_tac prems 1);
   5.129 +by (resolve_tac prems 1);
   5.130 +val notE = prth(result());
   5.131 +
   5.132 +
   5.133 +- val [major,minor] = goal Int_Rule.thy "[| ~P;  P |] ==> R";
   5.134 +Level 0
   5.135 +R
   5.136 + 1. R
   5.137 +val major = # : thm
   5.138 +val minor = # : thm
   5.139 +- by (resolve_tac [FalseE] 1);
   5.140 +Level 1
   5.141 +R
   5.142 + 1. False
   5.143 +- by (resolve_tac [mp] 1);
   5.144 +Level 2
   5.145 +R
   5.146 + 1. ?P1 --> False
   5.147 + 2. ?P1
   5.148 +- prth (rewrite_rule [not_def] major);
   5.149 +P --> False  [~P]
   5.150 +- by (resolve_tac [it] 1);
   5.151 +Level 3
   5.152 +R
   5.153 + 1. P
   5.154 +- by (resolve_tac [minor] 1);
   5.155 +Level 4
   5.156 +R
   5.157 +No subgoals!
   5.158 +- val notE = prth(result());
   5.159 +[| ~?P; ?P |] ==> ?R
   5.160 +val notE = # : thm
   5.161 +- val [major,minor] = goalw Int_Rule.thy [not_def]
   5.162 +=     "[| ~P;  P |] ==> R";
   5.163 +Level 0
   5.164 +R
   5.165 + 1. R
   5.166 +val major = # : thm
   5.167 +val minor = # : thm
   5.168 +- prth (minor RS (major RS mp RS FalseE));
   5.169 +?P  [P, ~P]
   5.170 +- by (resolve_tac [it] 1);
   5.171 +Level 1
   5.172 +R
   5.173 +No subgoals!
   5.174 +
   5.175 +
   5.176 +
   5.177 +
   5.178 +- goal Int_Rule.thy "[| ~P;  P |] ==> R";
   5.179 +Level 0
   5.180 +R
   5.181 + 1. R
   5.182 +- prths (map (rewrite_rule [not_def]) it);
   5.183 +P --> False  [~P]
   5.184 +
   5.185 +P  [P]
   5.186 +
   5.187 +- val prems = goalw Int_Rule.thy [not_def]
   5.188 +=     "[| ~P;  P |] ==> R";
   5.189 +Level 0
   5.190 +R
   5.191 + 1. R
   5.192 +val prems = # : thm list
   5.193 +- prths prems;
   5.194 +P --> False  [~P]
   5.195 +
   5.196 +P  [P]
   5.197 +
   5.198 +- by (resolve_tac [mp RS FalseE] 1);
   5.199 +Level 1
   5.200 +R
   5.201 + 1. ?P1 --> False
   5.202 + 2. ?P1
   5.203 +- by (resolve_tac prems 1);
   5.204 +Level 2
   5.205 +R
   5.206 + 1. P
   5.207 +- by (resolve_tac prems 1);
   5.208 +Level 3
   5.209 +R
   5.210 +No subgoals!
   5.211 +- val notE = prth(result());
   5.212 +[| ~?P; ?P |] ==> ?R
   5.213 +val notE = # : thm
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-src/Intro/foundations.tex	Wed Nov 10 05:06:55 1993 +0100
     6.3 @@ -0,0 +1,1123 @@
     6.4 +%% $Id$
     6.5 +\part{Foundations} 
     6.6 +This Part presents Isabelle's logical foundations in detail:
     6.7 +representing logical syntax in the typed $\lambda$-calculus; expressing
     6.8 +inference rules in Isabelle's meta-logic; combining rules by resolution.
     6.9 +Readers wishing to use Isabelle immediately may prefer to skip straight to
    6.10 +Part~II, using this Part (via the index) for reference only.
    6.11 +
    6.12 +\begin{figure} 
    6.13 +\begin{eqnarray*}
    6.14 +  \neg P   & \hbox{abbreviates} & P\imp\bot \\
    6.15 +  P\bimp Q & \hbox{abbreviates} & (P\imp Q) \conj (Q\imp P)
    6.16 +\end{eqnarray*}
    6.17 +\vskip 4ex
    6.18 +
    6.19 +\(\begin{array}{c@{\qquad\qquad}c}
    6.20 +  \infer[({\conj}I)]{P\conj Q}{P & Q}  &
    6.21 +  \infer[({\conj}E1)]{P}{P\conj Q} \qquad 
    6.22 +  \infer[({\conj}E2)]{Q}{P\conj Q} \\[4ex]
    6.23 +
    6.24 +  \infer[({\disj}I1)]{P\disj Q}{P} \qquad 
    6.25 +  \infer[({\disj}I2)]{P\disj Q}{Q} &
    6.26 +  \infer[({\disj}E)]{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}}\\[4ex]
    6.27 +
    6.28 +  \infer[({\imp}I)]{P\imp Q}{\infer*{Q}{[P]}} &
    6.29 +  \infer[({\imp}E)]{Q}{P\imp Q & P}  \\[4ex]
    6.30 +
    6.31 +  &
    6.32 +  \infer[({\bot}E)]{P}{\bot}\\[4ex]
    6.33 +
    6.34 +  \infer[({\forall}I)*]{\forall x.P}{P} &
    6.35 +  \infer[({\forall}E)]{P[t/x]}{\forall x.P} \\[3ex]
    6.36 +
    6.37 +  \infer[({\exists}I)]{\exists x.P}{P[t/x]} &
    6.38 +  \infer[({\exists}E)*]{Q}{{\exists x.P} & \infer*{Q}{[P]} } \\[3ex]
    6.39 +
    6.40 +  {t=t} \,(refl)   &  \vcenter{\infer[(subst)]{P[u/x]}{t=u & P[t/x]}} 
    6.41 +\end{array} \)
    6.42 +
    6.43 +\bigskip\bigskip
    6.44 +*{\em Eigenvariable conditions\/}:
    6.45 +
    6.46 +$\forall I$: provided $x$ is not free in the assumptions
    6.47 +
    6.48 +$\exists E$: provided $x$ is not free in $Q$ or any assumption except $P$
    6.49 +\caption{Intuitionistic first-order logic} \label{fol-fig}
    6.50 +\end{figure}
    6.51 +
    6.52 +\section{Formalizing logical syntax in Isabelle}
    6.53 +\index{Isabelle!formalizing syntax|bold}
    6.54 +Figure~\ref{fol-fig} presents intuitionistic first-order logic,
    6.55 +including equality and the natural numbers.  Let us see how to formalize
    6.56 +this logic in Isabelle, illustrating the main features of Isabelle's
    6.57 +polymorphic meta-logic.
    6.58 +
    6.59 +Isabelle represents syntax using the typed $\lambda$-calculus.  We declare
    6.60 +a type for each syntactic category of the logic.  We declare a constant for
    6.61 +each symbol of the logic, giving each $n$-ary operation an $n$-argument
    6.62 +curried function type.  Most importantly, $\lambda$-abstraction represents
    6.63 +variable binding in quantifiers.
    6.64 +
    6.65 +\index{$\To$|bold}\index{types}
    6.66 +Isabelle has \ML-style type constructors such as~$(\alpha)list$, where
    6.67 +$(bool)list$ is the type of lists of booleans.  Function types have the
    6.68 +form $\sigma\To\tau$, where $\sigma$ and $\tau$ are types.  Functions
    6.69 +taking $n$~arguments require curried function types; we may abbreviate
    6.70 +\[  \sigma@1\To (\cdots \sigma@n\To \tau\cdots)  \quad \hbox{as} \quad
    6.71 +   [\sigma@1, \ldots, \sigma@n] \To \tau. $$ 
    6.72 + 
    6.73 +The syntax for terms is summarised below.  Note that function application is
    6.74 +written $t(u)$ rather than the usual $t\,u$.
    6.75 +\[ 
    6.76 +\begin{array}{ll}
    6.77 +  t :: \sigma   & \hbox{type constraint, on a term or variable} \\
    6.78 +  \lambda x.t   & \hbox{abstraction} \\
    6.79 +  \lambda x@1\ldots x@n.t
    6.80 +        & \hbox{curried abstraction, $\lambda x@1. \ldots \lambda x@n.t$} \\
    6.81 +  t(u)          & \hbox{application} \\
    6.82 +  t (u@1, \ldots, u@n) & \hbox{curried application, $t(u@1)\ldots(u@n)$} 
    6.83 +\end{array}
    6.84 +\]
    6.85 +
    6.86 +
    6.87 +\subsection{Simple types and constants}
    6.88 +\index{types!simple|bold}
    6.89 +The syntactic categories of our logic (Figure~\ref{fol-fig}) are 
    6.90 +{\bf formulae} and {\bf terms}.  Formulae denote truth
    6.91 +values, so (following logical tradition) we call their type~$o$.  Terms can
    6.92 +be constructed using~0 and~$Suc$, requiring a type~$nat$ of natural
    6.93 +numbers.  Later, we shall see how to admit terms of other types.
    6.94 +
    6.95 +After declaring the types~$o$ and~$nat$, we may declare constants for the
    6.96 +symbols of our logic.  Since $\bot$ denotes a truth value (falsity) and 0
    6.97 +denotes a number, we put \begin{eqnarray*}
    6.98 +  \bot  & :: & o \\
    6.99 +  0     & :: & nat.
   6.100 +\end{eqnarray*}
   6.101 +If a symbol requires operands, the corresponding constant must have a
   6.102 +function type.  In our logic, the successor function
   6.103 +($Suc$) is from natural numbers to natural numbers, negation ($\neg$) is a
   6.104 +function from truth values to truth values, and the binary connectives are
   6.105 +curried functions taking two truth values as arguments: 
   6.106 +\begin{eqnarray*}
   6.107 +  Suc    & :: & nat\To nat  \\
   6.108 +  {\neg} & :: & o\To o      \\
   6.109 +  \conj,\disj,\imp,\bimp  & :: & [o,o]\To o 
   6.110 +\end{eqnarray*}
   6.111 +
   6.112 +Isabelle allows us to declare the binary connectives as infixes, with
   6.113 +appropriate precedences, so that we write $P\conj Q\disj R$ instead of
   6.114 +$\disj(\conj(P,Q), R)$.
   6.115 +
   6.116 +
   6.117 +\subsection{Polymorphic types and constants} \label{polymorphic}
   6.118 +\index{types!polymorphic|bold}
   6.119 +Which type should we assign to the equality symbol?  If we tried
   6.120 +$[nat,nat]\To o$, then equality would be restricted to the natural
   6.121 +numbers; we would have to declare different equality symbols for each
   6.122 +type.  Isabelle's type system is polymorphic, so we could declare
   6.123 +\begin{eqnarray*}
   6.124 +  {=}  & :: & [\alpha,\alpha]\To o.
   6.125 +\end{eqnarray*}
   6.126 +But this is also wrong.  The declaration is too polymorphic; $\alpha$
   6.127 +ranges over all types, including~$o$ and $nat\To nat$.  Thus, it admits
   6.128 +$\bot=\neg(\bot)$ and $Suc=Suc$ as formulae, which is acceptable in
   6.129 +higher-order logic but not in first-order logic.
   6.130 +
   6.131 +Isabelle's \bfindex{classes} control polymorphism.  Each type variable
   6.132 +belongs to a class, which denotes a set of types.  Classes are partially
   6.133 +ordered by the subclass relation, which is essentially the subset relation
   6.134 +on the sets of types.  They closely resemble the classes of the functional
   6.135 +language Haskell~\cite{haskell-tutorial,haskell-report}.  Nipkow and
   6.136 +Prehofer discuss type inference for type classes~\cite{nipkow-prehofer}.
   6.137 +
   6.138 +Isabelle provides the built-in class $logic$, which consists of the logical
   6.139 +types: the ones we want to reason about.  Let us declare a class $term$, to
   6.140 +consist of all legal types of terms in our logic.  The subclass structure
   6.141 +is now $term\le logic$.
   6.142 +
   6.143 +We declare $nat$ to be in class $term$.  Type variables of class~$term$
   6.144 +should resemble Standard~\ML's equality type variables, which range over
   6.145 +those types that possess an equality test.  Thus, we declare the equality
   6.146 +constant by
   6.147 +\begin{eqnarray*}
   6.148 +  {=}  & :: & [\alpha{::}term,\alpha]\To o 
   6.149 +\end{eqnarray*}
   6.150 +We give function types and~$o$ the class $logic$ rather than~$term$, since
   6.151 +they are not legal types for terms.  We may introduce new types of class
   6.152 +$term$ --- for instance, type $string$ or $real$ --- at any time.  We can
   6.153 +even declare type constructors such as $(\alpha)list$, and state that type
   6.154 +$(\sigma)list$ belongs to class~$term$ provided $\sigma$ does;  equality
   6.155 +applies to lists of natural numbers but not to lists of formulae.  We may
   6.156 +summarize this paragraph by a set of {\bf arity declarations} for type
   6.157 +constructors: 
   6.158 +\index{$\To$|bold}\index{arities!declaring}
   6.159 +\begin{eqnarray*}
   6.160 +  o     & :: & logic \\
   6.161 +  {\To} & :: & (logic,logic)logic \\
   6.162 +  nat, string, real     & :: & term \\
   6.163 +  list  & :: & (term)term
   6.164 +\end{eqnarray*}
   6.165 +Higher-order logic, where equality does apply to truth values and
   6.166 +functions, would require different arity declarations, namely ${o::term}$
   6.167 +and ${{\To}::(term,term)term}$.  The class system can also handle
   6.168 +overloading.\index{overloading|bold} We could declare $arith$ to be the
   6.169 +subclass of $term$ consisting of the `arithmetic' types, such as~$nat$.
   6.170 +Then we could declare the operators
   6.171 +\begin{eqnarray*}
   6.172 +  {+},{-},{\times},{/}  & :: & [\alpha{::}arith,\alpha]\To \alpha
   6.173 +\end{eqnarray*}
   6.174 +If we declare new types $real$ and $complex$ of class $arith$, then we
   6.175 +effectively have three sets of operators:
   6.176 +\begin{eqnarray*}
   6.177 +  {+},{-},{\times},{/}  & :: & [nat,nat]\To nat \\
   6.178 +  {+},{-},{\times},{/}  & :: & [real,real]\To real \\
   6.179 +  {+},{-},{\times},{/}  & :: & [complex,complex]\To complex 
   6.180 +\end{eqnarray*}
   6.181 +Isabelle will regard these as distinct constants, each of which can be defined
   6.182 +separately.  We could even introduce the type $(\alpha)vector$, make
   6.183 +$(\sigma)vector$ belong to $arith$ provided $\sigma$ is in $arith$, and define
   6.184 +\begin{eqnarray*}
   6.185 +  {+}  & :: & [(\sigma)vector,(\sigma)vector]\To (\sigma)vector 
   6.186 +\end{eqnarray*}
   6.187 +in terms of ${+} :: [\sigma,\sigma]\To \sigma$.
   6.188 +
   6.189 +Although we have pretended so far that a type variable belongs to only one
   6.190 +class --- Isabelle's concrete syntax helps to uphold this illusion --- it
   6.191 +may in fact belong to any finite number of classes.  For example suppose
   6.192 +that we had declared yet another class $ord \le term$, the class of all
   6.193 +`ordered' types, and a constant
   6.194 +\begin{eqnarray*}
   6.195 +  {\le}  & :: & [\alpha{::}ord,\alpha]\To o.
   6.196 +\end{eqnarray*}
   6.197 +In this context the variable $x$ in $x \le (x+x)$ will be assigned type
   6.198 +$\alpha{::}\{arith,ord\}$, i.e.\ $\alpha$ belongs to both $arith$ and $ord$.
   6.199 +Semantically the set $\{arith,ord\}$ should be understood
   6.200 +as the intersection of the sets of types represented by $arith$ and $ord$.
   6.201 +Such intersections of classes are called \bfindex{sorts}.  The empty
   6.202 +intersection of classes, $\{\}$, contains all types and is thus the
   6.203 +{\bf universal sort}.
   6.204 +
   6.205 +The type checker handles overloading, assigning each term a unique type.  For
   6.206 +this to be possible, the class and type declarations must satisfy certain
   6.207 +technical constraints~\cite{nipkow-prehofer}.
   6.208 +
   6.209 +\subsection{Higher types and quantifiers}
   6.210 +\index{types!higher|bold}
   6.211 +Quantifiers are regarded as operations upon functions.  Ignoring polymorphism
   6.212 +for the moment, consider the formula $\forall x. P(x)$, where $x$ ranges
   6.213 +over type~$nat$.  This is true if $P(x)$ is true for all~$x$.  Abstracting
   6.214 +$P(x)$ into a function, this is the same as saying that $\lambda x.P(x)$
   6.215 +returns true for all arguments.  Thus, the universal quantifier can be
   6.216 +represented by a constant
   6.217 +\begin{eqnarray*}
   6.218 +  \forall  & :: & (nat\To o) \To o,
   6.219 +\end{eqnarray*}
   6.220 +which is essentially an infinitary truth table.  The representation of $\forall
   6.221 +x. P(x)$ is $\forall(\lambda x. P(x))$.  
   6.222 +
   6.223 +The existential quantifier is treated
   6.224 +in the same way.  Other binding operators are also easily handled; for
   6.225 +instance, the summation operator $\Sigma@{k=i}^j f(k)$ can be represented as
   6.226 +$\Sigma(i,j,\lambda k.f(k))$, where
   6.227 +\begin{eqnarray*}
   6.228 +  \Sigma  & :: & [nat,nat, nat\To nat] \To nat.
   6.229 +\end{eqnarray*}
   6.230 +Quantifiers may be polymorphic.  We may define $\forall$ and~$\exists$ over
   6.231 +all legal types of terms, not just the natural numbers, and
   6.232 +allow summations over all arithmetic types:
   6.233 +\begin{eqnarray*}
   6.234 +   \forall,\exists      & :: & (\alpha{::}term\To o) \To o \\
   6.235 +   \Sigma               & :: & [nat,nat, nat\To \alpha{::}arith] \To \alpha
   6.236 +\end{eqnarray*}
   6.237 +Observe that the index variables still have type $nat$, while the values
   6.238 +being summed may belong to any arithmetic type.
   6.239 +
   6.240 +
   6.241 +\section{Formalizing logical rules in Isabelle}
   6.242 +\index{meta-logic|bold}
   6.243 +\index{Isabelle!formalizing rules|bold}
   6.244 +\index{$\Imp$|bold}\index{$\Forall$|bold}\index{$\equiv$|bold}
   6.245 +\index{implication!meta-level|bold}
   6.246 +\index{quantifiers!meta-level|bold}
   6.247 +\index{equality!meta-level|bold}
   6.248 +Object-logics are formalized by extending Isabelle's meta-logic, which is
   6.249 +intuitionistic higher-order logic.  The meta-level connectives are {\bf
   6.250 +implication}, the {\bf universal quantifier}, and {\bf equality}.
   6.251 +\begin{itemize}
   6.252 +  \item The implication \(\phi\Imp \psi\) means `\(\phi\) implies
   6.253 +\(\psi\)', and expresses logical {\bf entailment}.  
   6.254 +
   6.255 +  \item The quantification \(\Forall x.\phi\) means `\(\phi\) is true for
   6.256 +all $x$', and expresses {\bf generality} in rules and axiom schemes. 
   6.257 +
   6.258 +\item The equality \(a\equiv b\) means `$a$ equals $b$', for expressing
   6.259 +  \bfindex{definitions} (see~\S\ref{definitions}).  Equalities left over
   6.260 +  from the unification process, so called \bfindex{flex-flex equations},
   6.261 +  are written $a\qeq b$.  The two equality symbols have the same logical
   6.262 +  meaning. 
   6.263 +
   6.264 +\end{itemize}
   6.265 +The syntax of the meta-logic is formalized in precisely in the same manner
   6.266 +as object-logics, using the typed $\lambda$-calculus.  Analogous to
   6.267 +type~$o$ above, there is a built-in type $prop$ of meta-level truth values.
   6.268 +Meta-level formulae will have this type.  Type $prop$ belongs to
   6.269 +class~$logic$; also, $\sigma\To\tau$ belongs to $logic$ provided $\sigma$
   6.270 +and $\tau$ do.  Here are the types of the built-in connectives:
   6.271 +\begin{eqnarray*}
   6.272 +  \Imp     & :: & [prop,prop]\To prop \\
   6.273 +  \Forall  & :: & (\alpha{::}logic\To prop) \To prop \\
   6.274 +  {\equiv} & :: & [\alpha{::}\{\},\alpha]\To prop \\
   6.275 +  \qeq & :: & [\alpha{::}\{\},\alpha]\To prop c
   6.276 +\end{eqnarray*}
   6.277 +The restricted polymorphism in $\Forall$ excludes certain types, those used
   6.278 +just for parsing. 
   6.279 +
   6.280 +In our formalization of first-order logic, we declared a type~$o$ of
   6.281 +object-level truth values, rather than using~$prop$ for this purpose.  If
   6.282 +we declared the object-level connectives to have types such as
   6.283 +${\neg}::prop\To prop$, then these connectives would be applicable to
   6.284 +meta-level formulae.  Keeping $prop$ and $o$ as separate types maintains
   6.285 +the distinction between the meta-level and the object-level.  To formalize
   6.286 +the inference rules, we shall need to relate the two levels; accordingly,
   6.287 +we declare the constant
   6.288 +\index{Trueprop@{$Trueprop$}}
   6.289 +\begin{eqnarray*}
   6.290 +  Trueprop & :: & o\To prop.
   6.291 +\end{eqnarray*}
   6.292 +We may regard $Trueprop$ as a meta-level predicate, reading $Trueprop(P)$ as
   6.293 +`$P$ is true at the object-level.'  Put another way, $Trueprop$ is a coercion
   6.294 +from $o$ to $prop$.
   6.295 +
   6.296 +
   6.297 +\subsection{Expressing propositional rules}
   6.298 +\index{rules!propositional|bold}
   6.299 +We shall illustrate the use of the meta-logic by formalizing the rules of
   6.300 +Figure~\ref{fol-fig}.  Each object-level rule is expressed as a meta-level
   6.301 +axiom. 
   6.302 +
   6.303 +One of the simplest rules is $(\conj E1)$.  Making
   6.304 +everything explicit, its formalization in the meta-logic is
   6.305 +$$ \Forall P\;Q. Trueprop(P\conj Q) \Imp Trueprop(P).   \eqno(\conj E1) $$
   6.306 +This may look formidable, but it has an obvious reading: for all object-level
   6.307 +truth values $P$ and~$Q$, if $P\conj Q$ is true then so is~$P$.  The
   6.308 +reading is correct because the meta-logic has simple models, where
   6.309 +types denote sets and $\Forall$ really means `for all.'
   6.310 +
   6.311 +\index{Trueprop@{$Trueprop$}}
   6.312 +Isabelle adopts notational conventions to ease the writing of rules.  We may
   6.313 +hide the occurrences of $Trueprop$ by making it an implicit coercion.
   6.314 +Outer universal quantifiers may be dropped.  Finally, the nested implication
   6.315 +\[  \phi@1\Imp(\cdots \phi@n\Imp\psi\cdots) \]
   6.316 +may be abbreviated as $\List{\phi@1; \ldots; \phi@n} \Imp \psi$, which
   6.317 +formalizes a rule of $n$~premises.
   6.318 +
   6.319 +Using these conventions, the conjunction rules become the following axioms.
   6.320 +These fully specify the properties of~$\conj$:
   6.321 +$$ \List{P; Q} \Imp P\conj Q                 \eqno(\conj I) $$
   6.322 +$$ P\conj Q \Imp P  \qquad  P\conj Q \Imp Q  \eqno(\conj E1,2) $$
   6.323 +
   6.324 +\noindent
   6.325 +Next, consider the disjunction rules.  The discharge of assumption in
   6.326 +$(\disj E)$ is expressed  using $\Imp$:
   6.327 +$$ P \Imp P\disj Q  \qquad  Q \Imp P\disj Q  \eqno(\disj I1,2) $$
   6.328 +$$ \List{P\disj Q; P\Imp R; Q\Imp R} \Imp R  \eqno(\disj E) $$
   6.329 +
   6.330 +\noindent
   6.331 +To understand this treatment of assumptions\index{assumptions} in natural
   6.332 +deduction, look at implication.  The rule $({\imp}I)$ is the classic
   6.333 +example of natural deduction: to prove that $P\imp Q$ is true, assume $P$
   6.334 +is true and show that $Q$ must then be true.  More concisely, if $P$
   6.335 +implies $Q$ (at the meta-level), then $P\imp Q$ is true (at the
   6.336 +object-level).  Showing the coercion explicitly, this is formalized as
   6.337 +\[ (Trueprop(P)\Imp Trueprop(Q)) \Imp Trueprop(P\imp Q). \]
   6.338 +The rule $({\imp}E)$ is straightforward; hiding $Trueprop$, the axioms to
   6.339 +specify $\imp$ are 
   6.340 +$$ (P \Imp Q)  \Imp  P\imp Q   \eqno({\imp}I) $$
   6.341 +$$ \List{P\imp Q; P}  \Imp Q.  \eqno({\imp}E) $$
   6.342 +
   6.343 +\noindent
   6.344 +Finally, the intuitionistic contradiction rule is formalized as the axiom
   6.345 +$$ \bot \Imp P.   \eqno(\bot E) $$
   6.346 +
   6.347 +\begin{warn}
   6.348 +Earlier versions of Isabelle, and certain
   6.349 +papers~\cite{paulson89,paulson700}, use $\List{P}$ to mean $Trueprop(P)$.
   6.350 +\index{Trueprop@{$Trueprop$}}
   6.351 +\end{warn}
   6.352 +
   6.353 +\subsection{Quantifier rules and substitution}
   6.354 +\index{rules!quantifier|bold}\index{substitution|bold}
   6.355 +\index{variables!bound}
   6.356 +Isabelle expresses variable binding using $\lambda$-abstraction; for instance,
   6.357 +$\forall x.P$ is formalized as $\forall(\lambda x.P)$.  Recall that $F(t)$
   6.358 +is Isabelle's syntax for application of the function~$F$ to the argument~$t$;
   6.359 +it is not a meta-notation for substitution.  On the other hand, a substitution
   6.360 +will take place if $F$ has the form $\lambda x.P$;  Isabelle transforms
   6.361 +$(\lambda x.P)(t)$ to~$P[t/x]$ by $\beta$-conversion.  Thus, we can express
   6.362 +inference rules that involve substitution for bound variables.
   6.363 +
   6.364 +\index{parameters|bold}\index{eigenvariables|see{parameters}}
   6.365 +A logic may attach provisos to certain of its rules, especially quantifier
   6.366 +rules.  We cannot hope to formalize arbitrary provisos.  Fortunately, those
   6.367 +typical of quantifier rules always have the same form, namely `$x$ not free in
   6.368 +\ldots {\it (some set of formulae)},' where $x$ is a variable (called a {\bf
   6.369 +parameter} or {\bf eigenvariable}) in some premise.  Isabelle treats
   6.370 +provisos using~$\Forall$, its inbuilt notion of `for all'.
   6.371 +
   6.372 +\index{$\Forall$}
   6.373 +The purpose of the proviso `$x$ not free in \ldots' is
   6.374 +to ensure that the premise may not make assumptions about the value of~$x$,
   6.375 +and therefore holds for all~$x$.  We formalize $(\forall I)$ by
   6.376 +\[ \left(\Forall x. Trueprop(P(x))\right) \Imp Trueprop(\forall x.P(x)). \]
   6.377 +This means, `if $P(x)$ is true for all~$x$, then $\forall x.P(x)$ is true.'
   6.378 +The $\forall E$ rule exploits $\beta$-conversion.  Hiding $Trueprop$, the
   6.379 +$\forall$ axioms are
   6.380 +$$ \left(\Forall x. P(x)\right)  \Imp  \forall x.P(x)   \eqno(\forall I) $$
   6.381 +$$ \forall x.P(x)  \Imp P(t).  \eqno(\forall E)$$
   6.382 +
   6.383 +\noindent
   6.384 +We have defined the object-level universal quantifier~($\forall$)
   6.385 +using~$\Forall$.  But we do not require meta-level counterparts of all the
   6.386 +connectives of the object-logic!  Consider the existential quantifier: 
   6.387 +$$ P(t)  \Imp  \exists x.P(x)  \eqno(\exists I)$$
   6.388 +$$ \List{\exists x.P(x);\; \Forall x. P(x)\Imp Q} \Imp Q  \eqno(\exists E) $$
   6.389 +Let us verify $(\exists E)$ semantically.  Suppose that the premises
   6.390 +hold; since $\exists x.P(x)$ is true, we may choose $a$ such that $P(a)$ is
   6.391 +true.  Instantiating $\Forall x. P(x)\Imp Q$ with $a$ yields $P(a)\Imp Q$, and
   6.392 +we obtain the desired conclusion, $Q$.
   6.393 +
   6.394 +The treatment of substitution deserves mention.  The rule
   6.395 +\[ \infer{P[u/t]}{t=u & P} \]
   6.396 +would be hard to formalize in Isabelle.  It calls for replacing~$t$ by $u$
   6.397 +throughout~$P$, which cannot be expressed using $\beta$-conversion.  Our
   6.398 +rule~$(subst)$ uses the occurrences of~$x$ in~$P$ as a template for
   6.399 +substitution, inferring $P[u/x]$ from~$P[t/x]$.  When we formalize this as
   6.400 +an axiom, the template becomes a function variable:
   6.401 +$$ \List{t=u; P(t)} \Imp P(u).  \eqno(subst)$$
   6.402 +
   6.403 +
   6.404 +\subsection{Signatures and theories}
   6.405 +\index{signatures|bold}\index{theories|bold}
   6.406 +A {\bf signature} contains the information necessary for type checking,
   6.407 +parsing and pretty printing.  It specifies classes and their
   6.408 +relationships; types, with their arities, and constants, with
   6.409 +their types.  It also contains syntax rules, specified using mixfix
   6.410 +declarations.
   6.411 +
   6.412 +Two signatures can be merged provided their specifications are compatible ---
   6.413 +they must not, for example, assign different types to the same constant.
   6.414 +Under similar conditions, a signature can be extended.  Signatures are
   6.415 +managed internally by Isabelle; users seldom encounter them.
   6.416 +
   6.417 +A {\bf theory} consists of a signature plus a collection of axioms.  The
   6.418 +{\bf pure} theory contains only the meta-logic.  Theories can be combined
   6.419 +provided their signatures are compatible.  A theory definition extends an
   6.420 +existing theory with further signature specifications --- classes, types,
   6.421 +constants and mixfix declarations --- plus a list of axioms, expressed as
   6.422 +strings to be parsed.  A theory can formalize a small piece of mathematics,
   6.423 +such as lists and their operations, or an entire logic.  A mathematical
   6.424 +development typically involves many theories in a hierarchy.  For example,
   6.425 +the pure theory could be extended to form a theory for
   6.426 +Figure~\ref{fol-fig}; this could be extended in two separate ways to form a
   6.427 +theory for natural numbers and a theory for lists; the union of these two
   6.428 +could be extended into a theory defining the length of a list:
   6.429 +\[ \bf
   6.430 +\begin{array}{c@{}c@{}c@{}c@{}c}
   6.431 +     {}   &     {} & \hbox{Length} &  {}   &     {}   \\
   6.432 +     {}   &     {}   &  \uparrow &     {}   &     {}   \\
   6.433 +     {}   &     {} &\hbox{Nat}+\hbox{List}&  {}   &     {}   \\
   6.434 +     {}   & \nearrow &     {}    & \nwarrow &     {}   \\
   6.435 + \hbox{Nat} &   {}   &     {}    &     {}   & \hbox{List} \\
   6.436 +     {}   & \nwarrow &     {}    & \nearrow &     {}   \\
   6.437 +     {}   &     {}   &\hbox{FOL} &     {}   &     {}   \\
   6.438 +     {}   &     {}   &  \uparrow &     {}   &     {}   \\
   6.439 +     {}   &     {}   &\hbox{Pure}&     {}  &     {}
   6.440 +\end{array}
   6.441 +\]
   6.442 +Each Isabelle proof typically works within a single theory, which is
   6.443 +associated with the proof state.  However, many different theories may
   6.444 +coexist at the same time, and you may work in each of these during a single
   6.445 +session.  
   6.446 +
   6.447 +
   6.448 +\section{Proof construction in Isabelle}
   6.449 +\index{Isabelle!proof construction in|bold}
   6.450 +There is a one-to-one correspondence between meta-level proofs and
   6.451 +object-level proofs~\cite{paulson89}.  To each use of a meta-level axiom,
   6.452 +such as $(\forall I)$, there is a use of the corresponding object-level
   6.453 +rule.  Object-level assumptions and parameters have meta-level
   6.454 +counterparts.  The meta-level formalization is {\bf faithful}, admitting no
   6.455 +incorrect object-level inferences, and {\bf adequate}, admitting all
   6.456 +correct object-level inferences.  These properties must be demonstrated
   6.457 +separately for each object-logic.
   6.458 +
   6.459 +The meta-logic is defined by a collection of inference rules, including
   6.460 +equational rules for the $\lambda$-calculus, and logical rules.  The rules
   6.461 +for~$\Imp$ and~$\Forall$ resemble those for~$\imp$ and~$\forall$ in
   6.462 +Figure~\ref{fol-fig}.  Proofs performed using the primitive meta-rules
   6.463 +would be lengthy; Isabelle proofs normally use certain derived rules.
   6.464 +{\bf Resolution}, in particular, is convenient for backward proof.
   6.465 +
   6.466 +Unification is central to theorem proving.  It supports quantifier
   6.467 +reasoning by allowing certain `unknown' terms to be instantiated later,
   6.468 +possibly in stages.  When proving that the time required to sort $n$
   6.469 +integers is proportional to~$n^2$, we need not state the constant of
   6.470 +proportionality; when proving that a hardware adder will deliver the sum of
   6.471 +its inputs, we need not state how many clock ticks will be required.  Such
   6.472 +quantities often emerge from the proof.
   6.473 +
   6.474 +\index{variables!schematic|see{unknowns}}
   6.475 +Isabelle provides {\bf schematic variables}, or \bfindex{unknowns}, for
   6.476 +unification.  Logically, unknowns are free variables.  Pragmatically, they
   6.477 +may be instantiated during a proof, while ordinary variables remain fixed.
   6.478 +Unknowns are written with a ?\ prefix and are frequently subscripted:
   6.479 +$\Var{a}$, $\Var{a@1}$, $\Var{a@2}$, \ldots, $\Var{P}$, $\Var{P@1}$, \ldots.
   6.480 +
   6.481 +Recall that an inference rule of the form
   6.482 +\[ \infer{\phi}{\phi@1 & \ldots & \phi@n} \]
   6.483 +is formalized in Isabelle's meta-logic as the axiom
   6.484 +$\List{\phi@1; \ldots; \phi@n} \Imp \phi$.
   6.485 +Such axioms resemble {\sc Prolog}'s Horn clauses, and can be combined by
   6.486 +resolution --- Isabelle's principal proof method.  Resolution yields both
   6.487 +forward and backward proof.  Backward proof works by unifying a goal with
   6.488 +the conclusion of a rule, whose premises become new subgoals.  Forward proof
   6.489 +works by unifying theorems with the premises of a rule, deriving a new theorem.
   6.490 +
   6.491 +Isabelle axioms will require an extended notion of resolution, because
   6.492 +they differ from Horn clauses in two major respects:
   6.493 +\begin{itemize}
   6.494 +  \item They are written in the typed $\lambda$-calculus, and therefore must be
   6.495 +resolved using higher-order unification.
   6.496 +
   6.497 +  \item Horn clauses are composed of atomic formulae.  Any formula of the form
   6.498 +$Trueprop(\cdots)$ is atomic, but axioms such as ${\imp}I$ and $\forall I$
   6.499 +contain non-atomic formulae.
   6.500 +\index{Trueprop@{$Trueprop$}}
   6.501 +\end{itemize}
   6.502 +Isabelle should not be confused with classical resolution theorem provers
   6.503 +such as Otter~\cite{wos-bledsoe}.  At the meta-level, Isabelle proves
   6.504 +theorems in their positive form, not by refutation.  However, an
   6.505 +object-logic that includes a contradiction rule may employ a refutation
   6.506 +proof procedure.
   6.507 +
   6.508 +
   6.509 +\subsection{Higher-order unification}
   6.510 +\index{unification!higher-order|bold}
   6.511 +Unification is equation solving.  The solution of $f(\Var{x},c) \qeq
   6.512 +f(d,\Var{y})$ is $\Var{x}\equiv d$ and $\Var{y}\equiv c$.  {\bf
   6.513 +Higher-order unification} is equation solving for typed $\lambda$-terms.
   6.514 +To handle $\beta$-conversion, it must reduce $(\lambda x.t)u$ to $t[u/x]$.
   6.515 +That is easy --- in the typed $\lambda$-calculus, all reduction sequences
   6.516 +terminate at a normal form.  But it must guess the unknown
   6.517 +function~$\Var{f}$ in order to solve the equation
   6.518 +\begin{equation} \label{hou-eqn}
   6.519 + \Var{f}(t) \qeq g(u@1,\ldots,u@k).
   6.520 +\end{equation}
   6.521 +Huet's~\cite{huet75} search procedure solves equations by imitation and
   6.522 +projection.  {\bf Imitation}\index{imitation|bold} makes~$\Var{f}$ apply
   6.523 +leading symbol (if a constant) of the right-hand side.  To solve
   6.524 +equation~(\ref{hou-eqn}), it guesses
   6.525 +\[ \Var{f} \equiv \lambda x. g(\Var{h@1}(x),\ldots,\Var{h@k}(x)), \]
   6.526 +where $\Var{h@1}$, \ldots, $\Var{h@k}$ are new unknowns.  Assuming there are no
   6.527 +other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the
   6.528 +set of equations
   6.529 +\[ \Var{h@1}(t)\qeq u@1 \quad\ldots\quad \Var{h@k}(t)\qeq u@k. \]
   6.530 +If the procedure solves these equations, instantiating $\Var{h@1}$, \ldots,
   6.531 +$\Var{h@k}$, then it yields an instantiation for~$\Var{f}$.
   6.532 +
   6.533 +\index{projection|bold}
   6.534 +{\bf Projection} makes $\Var{f}$ apply one of its arguments.  To solve
   6.535 +equation~(\ref{hou-eqn}), if $t$ expects~$m$ arguments and delivers a
   6.536 +result of suitable type, it guesses
   6.537 +\[ \Var{f} \equiv \lambda x. x(\Var{h@1}(x),\ldots,\Var{h@m}(x)), \]
   6.538 +where $\Var{h@1}$, \ldots, $\Var{h@m}$ are new unknowns.  Assuming there are no
   6.539 +other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the 
   6.540 +equation 
   6.541 +\[ t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k). $$ 
   6.542 +
   6.543 +\begin{warn}
   6.544 +Huet's unification procedure is complete.  Isabelle's polymorphic version,
   6.545 +which solves for type unknowns as well as for term unknowns, is incomplete.
   6.546 +The problem is that projection requires type information.  In
   6.547 +equation~(\ref{hou-eqn}), if the type of~$t$ is unknown, then projections
   6.548 +are possible for all~$m\geq0$, and the types of the $\Var{h@i}$ will be
   6.549 +similarly unconstrained.  Therefore, Isabelle never attempts such
   6.550 +projections, and may fail to find unifiers where a type unknown turns out
   6.551 +to be a function type.
   6.552 +\end{warn}
   6.553 +
   6.554 +\index{unknowns!of function type|bold}
   6.555 +Given $\Var{f}(t@1,\ldots,t@n)\qeq u$, Huet's procedure could make up to
   6.556 +$n+1$ guesses.  The search tree and set of unifiers may be infinite.  But
   6.557 +higher-order unification can work effectively, provided you are careful
   6.558 +with {\bf function unknowns}:
   6.559 +\begin{itemize}
   6.560 +  \item Equations with no function unknowns are solved using first-order
   6.561 +unification, extended to treat bound variables.  For example, $\lambda x.x
   6.562 +\qeq \lambda x.\Var{y}$ has no solution because $\Var{y}\equiv x$ would
   6.563 +capture the free variable~$x$.
   6.564 +
   6.565 +  \item An occurrence of the term $\Var{f}(x,y,z)$, where the arguments are
   6.566 +distinct bound variables, causes no difficulties.  Its projections can only
   6.567 +match the corresponding variables.
   6.568 +
   6.569 +  \item Even an equation such as $\Var{f}(a)\qeq a+a$ is all right.  It has
   6.570 +four solutions, but Isabelle evaluates them lazily, trying projection before
   6.571 +imitation. The first solution is usually the one desired:
   6.572 +\[ \Var{f}\equiv \lambda x. x+x \quad
   6.573 +   \Var{f}\equiv \lambda x. a+x \quad
   6.574 +   \Var{f}\equiv \lambda x. x+a \quad
   6.575 +   \Var{f}\equiv \lambda x. a+a \]
   6.576 +  \item  Equations such as $\Var{f}(\Var{x},\Var{y})\qeq t$ and
   6.577 +$\Var{f}(\Var{g}(x))\qeq t$ admit vast numbers of unifiers, and must be
   6.578 +avoided. 
   6.579 +\end{itemize}
   6.580 +In problematic cases, you may have to instantiate some unknowns before
   6.581 +invoking unification. 
   6.582 +
   6.583 +
   6.584 +\subsection{Joining rules by resolution} \label{joining}
   6.585 +\index{resolution|bold}
   6.586 +Let $\List{\psi@1; \ldots; \psi@m} \Imp \psi$ and $\List{\phi@1; \ldots;
   6.587 +\phi@n} \Imp \phi$ be two Isabelle theorems, representing object-level rules. 
   6.588 +Choosing some~$i$ from~1 to~$n$, suppose that $\psi$ and $\phi@i$ have a
   6.589 +higher-order unifier.  Writing $Xs$ for the application of substitution~$s$ to
   6.590 +expression~$X$, this means there is some~$s$ such that $\psi s\equiv \phi@i s$.
   6.591 +By resolution, we may conclude
   6.592 +\[ (\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m;
   6.593 +          \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.
   6.594 +\]
   6.595 +The substitution~$s$ may instantiate unknowns in both rules.  In short,
   6.596 +resolution is the following rule:
   6.597 +\[ \infer[(\psi s\equiv \phi@i s)]
   6.598 +         {(\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m;
   6.599 +          \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s}
   6.600 +         {\List{\psi@1; \ldots; \psi@m} \Imp \psi & &
   6.601 +          \List{\phi@1; \ldots; \phi@n} \Imp \phi}
   6.602 +\]
   6.603 +It operates at the meta-level, on Isabelle theorems, and is justified by
   6.604 +the properties of $\Imp$ and~$\Forall$.  It takes the number~$i$ (for
   6.605 +$1\leq i\leq n$) as a parameter and may yield infinitely many conclusions,
   6.606 +one for each unifier of $\psi$ with $\phi@i$.  Isabelle returns these
   6.607 +conclusions as a sequence (lazy list).
   6.608 +
   6.609 +Resolution expects the rules to have no outer quantifiers~($\Forall$).  It
   6.610 +may rename or instantiate any schematic variables, but leaves free
   6.611 +variables unchanged.  When constructing a theory, Isabelle puts the rules
   6.612 +into a standard form containing no free variables; for instance, $({\imp}E)$
   6.613 +becomes
   6.614 +\[ \List{\Var{P}\imp \Var{Q}; \Var{P}}  \Imp \Var{Q}. 
   6.615 +\]
   6.616 +When resolving two rules, the unknowns in the first rule are renamed, by
   6.617 +subscripting, to make them distinct from the unknowns in the second rule.  To
   6.618 +resolve $({\imp}E)$ with itself, the first copy of the rule would become
   6.619 +\[ \List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}}  \Imp \Var{Q@1}. \]
   6.620 +Resolving this with $({\imp}E)$ in the first premise, unifying $\Var{Q@1}$ with
   6.621 +$\Var{P}\imp \Var{Q}$, is the meta-level inference
   6.622 +\[ \infer{\List{\Var{P@1}\imp (\Var{P}\imp \Var{Q}); \Var{P@1}; \Var{P}} 
   6.623 +           \Imp\Var{Q}.}
   6.624 +         {\List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}}  \Imp \Var{Q@1} & &
   6.625 +          \List{\Var{P}\imp \Var{Q}; \Var{P}}  \Imp \Var{Q}}
   6.626 +\]
   6.627 +Renaming the unknowns in the resolvent, we have derived the
   6.628 +object-level rule
   6.629 +\[ \infer{Q.}{R\imp (P\imp Q)  &  R  &  P}  \]
   6.630 +\index{rules!derived}
   6.631 +Joining rules in this fashion is a simple way of proving theorems.  The
   6.632 +derived rules are conservative extensions of the object-logic, and may permit
   6.633 +simpler proofs.  Let us consider another example.  Suppose we have the axiom
   6.634 +$$ \forall x\,y. Suc(x)=Suc(y)\imp x=y. \eqno (inject) $$
   6.635 +
   6.636 +\noindent 
   6.637 +The standard form of $(\forall E)$ is
   6.638 +$\forall x.\Var{P}(x)  \Imp \Var{P}(\Var{t})$.
   6.639 +Resolving $(inject)$ with $(\forall E)$ replaces $\Var{P}$ by
   6.640 +$\lambda x. \forall y. Suc(x)=Suc(y)\imp x=y$ and leaves $\Var{t}$
   6.641 +unchanged, yielding  
   6.642 +\[ \forall y. Suc(\Var{t})=Suc(y)\imp \Var{t}=y. \]
   6.643 +Resolving this with $(\forall E)$ puts a subscript on~$\Var{t}$
   6.644 +and yields
   6.645 +\[ Suc(\Var{t@1})=Suc(\Var{t})\imp \Var{t@1}=\Var{t}. \]
   6.646 +Resolving this with $({\imp}E)$ increases the subscripts and yields
   6.647 +\[ Suc(\Var{t@2})=Suc(\Var{t@1})\Imp \Var{t@2}=\Var{t@1}. 
   6.648 +\]
   6.649 +We have derived the rule
   6.650 +\[ \infer{m=n,}{Suc(m)=Suc(n)} \]
   6.651 +which goes directly from $Suc(m)=Suc(n)$ to $m=n$.  It is handy for simplifying
   6.652 +an equation like $Suc(Suc(Suc(m)))=Suc(Suc(Suc(0)))$.  
   6.653 +
   6.654 +
   6.655 +\subsection{Lifting a rule into a context}
   6.656 +The rules $({\imp}I)$ and $(\forall I)$ may seem unsuitable for
   6.657 +resolution.  They have non-atomic premises, namely $P\Imp Q$ and $\Forall
   6.658 +x.P(x)$, while the conclusions of all the rules are atomic (they have the form
   6.659 +$Trueprop(\cdots)$).  Isabelle gets round the problem through a meta-inference
   6.660 +called \bfindex{lifting}.  Let us consider how to construct proofs such as
   6.661 +\[ \infer[({\imp}I)]{P\imp(Q\imp R)}
   6.662 +         {\infer[({\imp}I)]{Q\imp R}
   6.663 +                        {\infer*{R}{[P] & [Q]}}}
   6.664 +   \qquad
   6.665 +   \infer[(\forall I)]{\forall x\,y.P(x,y)}
   6.666 +         {\infer[(\forall I)]{\forall y.P(x,y)}{P(x,y)}}
   6.667 +\]
   6.668 +
   6.669 +\subsubsection{Lifting over assumptions}
   6.670 +\index{lifting!over assumptions|bold}
   6.671 +Lifting over $\theta\Imp{}$ is the following meta-inference rule:
   6.672 +\[ \infer{\List{\theta\Imp\phi@1; \ldots; \theta\Imp\phi@n} \Imp
   6.673 +          (\theta \Imp \phi)}
   6.674 +         {\List{\phi@1; \ldots; \phi@n} \Imp \phi} \]
   6.675 +This is clearly sound: if $\List{\phi@1; \ldots; \phi@n} \Imp \phi$ is true and
   6.676 +$\theta\Imp\phi@1$, \ldots, $\theta\Imp\phi@n$, $\theta$ are all true then
   6.677 +$\phi$ must be true.  Iterated lifting over a series of meta-formulae
   6.678 +$\theta@k$, \ldots, $\theta@1$ yields an object-rule whose conclusion is
   6.679 +$\List{\theta@1; \ldots; \theta@k} \Imp \phi$.  Typically the $\theta@i$ are
   6.680 +the assumptions in a natural deduction proof; lifting copies them into a rule's
   6.681 +premises and conclusion.
   6.682 +
   6.683 +When resolving two rules, Isabelle lifts the first one if necessary.  The
   6.684 +standard form of $({\imp}I)$ is
   6.685 +\[ (\Var{P} \Imp \Var{Q})  \Imp  \Var{P}\imp \Var{Q}.   \]
   6.686 +To resolve this rule with itself, Isabelle modifies one copy as follows: it
   6.687 +renames the unknowns to $\Var{P@1}$ and $\Var{Q@1}$, then lifts the rule over
   6.688 +$\Var{P}\Imp{}$:
   6.689 +\[ \List{\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}; \Var{P}} 
   6.690 +   \Imp  \Var{P@1}\imp \Var{Q@1}.   \]
   6.691 +Unifying $\Var{P}\Imp \Var{P@1}\imp\Var{Q@1}$ with $\Var{P} \Imp
   6.692 +\Var{Q}$ instantiates $\Var{Q}$ to ${\Var{P@1}\imp\Var{Q@1}}$.
   6.693 +Resolution yields
   6.694 +\[ (\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}) \Imp
   6.695 +\Var{P}\imp(\Var{P@1}\imp\Var{Q@1}).   \]
   6.696 +This represents the derived rule
   6.697 +\[ \infer{P\imp(Q\imp R).}{\infer*{R}{[P,Q]}} \]
   6.698 +
   6.699 +\subsubsection{Lifting over parameters}
   6.700 +\index{lifting!over parameters|bold}
   6.701 +An analogous form of lifting handles premises of the form $\Forall x\ldots\,$. 
   6.702 +Here, lifting prefixes an object-rule's premises and conclusion with $\Forall
   6.703 +x$.  At the same time, lifting introduces a dependence upon~$x$.  It replaces
   6.704 +each unknown $\Var{a}$ in the rule by $\Var{a'}(x)$, where $\Var{a'}$ is a new
   6.705 +unknown (by subscripting) of suitable type --- necessarily a function type.  In
   6.706 +short, lifting is the meta-inference
   6.707 +\[ \infer{\List{\Forall x.\phi@1^x; \ldots; \Forall x.\phi@n^x} 
   6.708 +           \Imp \Forall x.\phi^x,}
   6.709 +         {\List{\phi@1; \ldots; \phi@n} \Imp \phi} \]
   6.710 +where $\phi^x$ stands for the result of lifting unknowns over~$x$ in $\phi$. 
   6.711 +It is not hard to verify that this meta-inference is sound.
   6.712 +For example, $(\disj I)$ might be lifted to
   6.713 +\[ (\Forall x.\Var{P@1}(x)) \Imp (\Forall x. \Var{P@1}(x)\disj \Var{Q@1}(x))\]
   6.714 +and $(\forall I)$ to
   6.715 +\[ (\Forall x\,y.\Var{P@1}(x,y)) \Imp (\Forall x. \forall y.\Var{P@1}(x,y)). \]
   6.716 +Isabelle has renamed a bound variable in $(\forall I)$ from $x$ to~$y$,
   6.717 +avoiding a clash.  Resolving the above with $(\forall I)$ is the meta-inference
   6.718 +\[ \infer{\Forall x\,y.\Var{P@1}(x,y)) \Imp \forall x\,y.\Var{P@1}(x,y)) }
   6.719 +         {(\Forall x\,y.\Var{P@1}(x,y)) \Imp 
   6.720 +               (\Forall x. \forall y.\Var{P@1}(x,y))  &
   6.721 +          (\Forall x.\Var{P}(x)) \Imp (\forall x.\Var{P}(x))} \]
   6.722 +Here, $\Var{P}$ is replaced by $\lambda x.\forall y.\Var{P@1}(x,y)$; the
   6.723 +resolvent expresses the derived rule
   6.724 +\[ \vcenter{ \infer{\forall x\,y.Q(x,y)}{Q(x,y)} }
   6.725 +   \quad\hbox{provided $x$, $y$ not free in the assumptions} 
   6.726 +\] 
   6.727 +I discuss lifting and parameters at length elsewhere~\cite{paulson89}.
   6.728 +Miller goes into even greater detail~\cite{miller-jsc}.
   6.729 +
   6.730 +
   6.731 +\section{Backward proof by resolution}
   6.732 +\index{resolution!in backward proof}\index{proof!backward|bold}
   6.733 +Resolution is convenient for deriving simple rules and for reasoning
   6.734 +forward from facts.  It can also support backward proof, where we start
   6.735 +with a goal and refine it to progressively simpler subgoals until all have
   6.736 +been solved.  {\sc lcf} (and its descendants {\sc hol} and Nuprl) provide
   6.737 +tactics and tacticals, which constitute a high-level language for
   6.738 +expressing proof searches.  \bfindex{Tactics} perform primitive refinements
   6.739 +while \bfindex{tacticals} combine tactics.
   6.740 +
   6.741 +\index{LCF}
   6.742 +Isabelle's tactics and tacticals work differently from {\sc lcf}'s.  An
   6.743 +Isabelle rule is {\bf bidirectional}: there is no distinction between
   6.744 +inputs and outputs.  {\sc lcf} has a separate tactic for each rule;
   6.745 +Isabelle performs refinement by any rule in a uniform fashion, using
   6.746 +resolution.
   6.747 +
   6.748 +\index{subgoals|bold}\index{main goal|bold}
   6.749 +Isabelle works with meta-level theorems of the form
   6.750 +\( \List{\phi@1; \ldots; \phi@n} \Imp \phi \).
   6.751 +We have viewed this as the {\bf rule} with premises
   6.752 +$\phi@1$,~\ldots,~$\phi@n$ and conclusion~$\phi$.  It can also be viewed as
   6.753 +the \bfindex{proof state} with subgoals $\phi@1$,~\ldots,~$\phi@n$ and main
   6.754 +goal~$\phi$.
   6.755 +
   6.756 +To prove the formula~$\phi$, take $\phi\Imp \phi$ as the initial proof
   6.757 +state.  This assertion is, trivially, a theorem.  At a later stage in the
   6.758 +backward proof, a typical proof state is $\List{\phi@1; \ldots; \phi@n}
   6.759 +\Imp \phi$.  This proof state is a theorem, guaranteeing that the subgoals
   6.760 +$\phi@1$,~\ldots,~$\phi@n$ imply~$\phi$.  If $m=0$ then we have
   6.761 +proved~$\phi$ outright.  If $\phi$ contains unknowns, they may become
   6.762 +instantiated during the proof; a proof state may be $\List{\phi@1; \ldots;
   6.763 +\phi@n} \Imp \phi'$, where $\phi'$ is an instance of~$\phi$.
   6.764 +
   6.765 +\subsection{Refinement by resolution}
   6.766 +\index{refinement|bold}
   6.767 +To refine subgoal~$i$ of a proof state by a rule, perform the following
   6.768 +resolution: 
   6.769 +\[ \infer{\hbox{new proof state}}{\hbox{rule} & & \hbox{proof state}} \]
   6.770 +If the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after lifting
   6.771 +over subgoal~$i$, and the proof state is $\List{\phi@1; \ldots; \phi@n}
   6.772 +\Imp \phi$, then the new proof state is (for~$1\leq i\leq n$)
   6.773 +\[ (\List{\phi@1; \ldots; \phi@{i-1}; \psi'@1;
   6.774 +          \ldots; \psi'@m; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.  \]
   6.775 +Substitution~$s$ unifies $\psi'$ with~$\phi@i$.  In the proof state,
   6.776 +subgoal~$i$ is replaced by $m$ new subgoals, the rule's instantiated premises.
   6.777 +If some of the rule's unknowns are left un-instantiated, they become new
   6.778 +unknowns in the proof state.  Refinement by~$(\exists I)$, namely
   6.779 +\[ \Var{P}(\Var{t}) \Imp \exists x. \Var{P}(x), \]
   6.780 +inserts a new unknown derived from~$\Var{t}$ by subscripting and lifting.
   6.781 +We do not have to specify an `existential witness' when
   6.782 +applying~$(\exists I)$.  Further resolutions may instantiate unknowns in
   6.783 +the proof state.
   6.784 +
   6.785 +\subsection{Proof by assumption}
   6.786 +\index{proof!by assumption|bold}
   6.787 +In the course of a natural deduction proof, parameters $x@1$, \ldots,~$x@l$ and
   6.788 +assumptions $\theta@1$, \ldots, $\theta@k$ accumulate, forming a context for
   6.789 +each subgoal.  Repeated lifting steps can lift a rule into any context.  To
   6.790 +aid readability, Isabelle puts contexts into a normal form, gathering the
   6.791 +parameters at the front:
   6.792 +\begin{equation} \label{context-eqn}
   6.793 +\Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta. 
   6.794 +\end{equation}
   6.795 +Under the usual reading of the connectives, this expresses that $\theta$
   6.796 +follows from $\theta@1$,~\ldots~$\theta@k$ for arbitrary
   6.797 +$x@1$,~\ldots,~$x@l$.  It is trivially true if $\theta$ equals any of
   6.798 +$\theta@1$,~\ldots~$\theta@k$, or is unifiable with any of them.  This
   6.799 +models proof by assumption in natural deduction.
   6.800 +
   6.801 +Isabelle automates the meta-inference for proof by assumption.  Its arguments
   6.802 +are the meta-theorem $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, and some~$i$
   6.803 +from~1 to~$n$, where $\phi@i$ has the form~(\ref{context-eqn}).  Its results
   6.804 +are meta-theorems of the form
   6.805 +\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \phi@n} \Imp \phi)s \]
   6.806 +for each $s$ and~$j$ such that $s$ unifies $\lambda x@1 \ldots x@l. \theta@j$
   6.807 +with $\lambda x@1 \ldots x@l. \theta$.  Isabelle supplies the parameters
   6.808 +$x@1$,~\ldots,~$x@l$ to higher-order unification as bound variables, which
   6.809 +regards them as unique constants with a limited scope --- this enforces
   6.810 +parameter provisos~\cite{paulson89}.
   6.811 +
   6.812 +The premise represents a proof state with~$n$ subgoals, of which the~$i$th is
   6.813 +to be solved by assumption.  Isabelle searches the subgoal's context for an
   6.814 +assumption, say $\theta@j$, that can solve it by unification.  For each
   6.815 +unifier, the meta-inference returns an instantiated proof state from which the
   6.816 +$i$th subgoal has been removed.  Isabelle searches for a unifying assumption;
   6.817 +for readability and robustness, proofs do not refer to assumptions by number.
   6.818 +
   6.819 +Consider the proof state $(\List{P(a); P(b)} \Imp P(\Var{x})) \Imp Q(\Var{x})$.
   6.820 +Proof by assumption (with $i=1$, the only possibility) yields two results:
   6.821 +\begin{itemize}
   6.822 +  \item $Q(a)$, instantiating $\Var{x}\equiv a$
   6.823 +  \item $Q(b)$, instantiating $\Var{x}\equiv b$
   6.824 +\end{itemize}
   6.825 +Here, proof by assumption affects the main goal.  It could also affect
   6.826 +other subgoals.  Consider the effect of having the
   6.827 +additional subgoal ${\List{P(b); P(c)} \Imp P(\Var{x})}$.
   6.828 +
   6.829 +\subsection{A propositional proof} \label{prop-proof}
   6.830 +\index{examples!propositional}
   6.831 +Our first example avoids quantifiers.  Given the main goal $P\disj P\imp
   6.832 +P$, Isabelle creates the initial state
   6.833 +\[ (P\disj P\imp P)\Imp (P\disj P\imp P). \]
   6.834 +Bear in mind that every proof state we derive will be a meta-theorem,
   6.835 +expressing that the subgoals imply the main goal.  The first step is to refine
   6.836 +subgoal~1 by (${\imp}I)$, creating a new state where $P\disj P$ is an
   6.837 +assumption: 
   6.838 +\[ (P\disj P\Imp P)\Imp (P\disj P\imp P) \]
   6.839 +The next step is $(\disj E)$, which replaces subgoal~1 by three new subgoals. 
   6.840 +Because of lifting, each subgoal contains a copy of the context --- the
   6.841 +assumption $P\disj P$.  (In fact, this assumption is now redundant; we shall
   6.842 +shortly see how to get rid of it!)  The new proof state is the following
   6.843 +meta-theorem, laid out for clarity:
   6.844 +\[ \begin{array}{l@{}l@{\qquad\qquad}l} 
   6.845 +  \lbrakk\;& P\disj P\Imp \Var{P@1}\disj\Var{Q@1}; & \hbox{(subgoal 1)} \\
   6.846 +           & \List{P\disj P; \Var{P@1}} \Imp P;    & \hbox{(subgoal 2)} \\
   6.847 +           & \List{P\disj P; \Var{Q@1}} \Imp P     & \hbox{(subgoal 3)} \\
   6.848 +  \rbrakk\;& \Imp (P\disj P\imp P)                 & \hbox{(main goal)}
   6.849 +   \end{array} 
   6.850 +\]
   6.851 +Notice the unknowns in the proof state.  Because we have applied $(\disj E)$,
   6.852 +we must prove some disjunction, $\Var{P@1}\disj\Var{Q@1}$.  Of course,
   6.853 +subgoal~1 is provable by assumption.  This instantiates both $\Var{P@1}$ and
   6.854 +$\Var{Q@1}$ to~$P$ throughout the proof state:
   6.855 +\[ \begin{array}{l@{}l@{\qquad\qquad}l} 
   6.856 +    \lbrakk\;& \List{P\disj P; P} \Imp P; & \hbox{(subgoal 1)} \\
   6.857 +             & \List{P\disj P; P} \Imp P  & \hbox{(subgoal 2)} \\
   6.858 +    \rbrakk\;& \Imp (P\disj P\imp P)      & \hbox{(main goal)}
   6.859 +   \end{array} \]
   6.860 +Both of the remaining subgoals can be proved by assumption.  After two such
   6.861 +steps, the proof state is simply the meta-theorem $P\disj P\imp P$.  This is
   6.862 +our desired result.
   6.863 +
   6.864 +\subsection{A quantifier proof}
   6.865 +\index{examples!with quantifiers}
   6.866 +To illustrate quantifiers and $\Forall$-lifting, let us prove
   6.867 +$(\exists x.P(f(x)))\imp(\exists x.P(x))$.  The initial proof
   6.868 +state is the trivial meta-theorem 
   6.869 +\[ (\exists x.P(f(x)))\imp(\exists x.P(x)) \Imp 
   6.870 +   (\exists x.P(f(x)))\imp(\exists x.P(x)). \]
   6.871 +As above, the first step is refinement by (${\imp}I)$: 
   6.872 +\[ (\exists x.P(f(x))\Imp \exists x.P(x)) \Imp 
   6.873 +   (\exists x.P(f(x)))\imp(\exists x.P(x)) 
   6.874 +\]
   6.875 +The next step is $(\exists E)$, which replaces subgoal~1 by two new subgoals.
   6.876 +Both have the assumption $\exists x.P(f(x))$.  The new proof
   6.877 +state is the meta-theorem  
   6.878 +\[ \begin{array}{l@{}l@{\qquad\qquad}l} 
   6.879 +   \lbrakk\;& \exists x.P(f(x)) \Imp \exists x.\Var{P@1}(x); & \hbox{(subgoal 1)} \\
   6.880 +            & \Forall x.\List{\exists x.P(f(x)); \Var{P@1}(x)} \Imp 
   6.881 +                       \exists x.P(x)  & \hbox{(subgoal 2)} \\
   6.882 +    \rbrakk\;& \Imp (\exists x.P(f(x)))\imp(\exists x.P(x))  & \hbox{(main goal)}
   6.883 +   \end{array} 
   6.884 +\]
   6.885 +The unknown $\Var{P@1}$ appears in both subgoals.  Because we have applied
   6.886 +$(\exists E)$, we must prove $\exists x.\Var{P@1}(x)$, where $\Var{P@1}(x)$ may
   6.887 +become any formula possibly containing~$x$.  Proving subgoal~1 by assumption
   6.888 +instantiates $\Var{P@1}$ to~$\lambda x.P(f(x))$:  
   6.889 +\[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp 
   6.890 +         \exists x.P(x)\right) 
   6.891 +   \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) 
   6.892 +\]
   6.893 +The next step is refinement by $(\exists I)$.  The rule is lifted into the
   6.894 +context of the parameter~$x$ and the assumption $P(f(x))$.  This ensures that
   6.895 +the context is copied to the subgoal and allows the existential witness to
   6.896 +depend upon~$x$: 
   6.897 +\[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp 
   6.898 +         P(\Var{x@2}(x))\right) 
   6.899 +   \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) 
   6.900 +\]
   6.901 +The existential witness, $\Var{x@2}(x)$, consists of an unknown
   6.902 +applied to a parameter.  Proof by assumption unifies $\lambda x.P(f(x))$ 
   6.903 +with $\lambda x.P(\Var{x@2}(x))$, instantiating $\Var{x@2}$ to $f$.  The final
   6.904 +proof state contains no subgoals: $(\exists x.P(f(x)))\imp(\exists x.P(x))$.
   6.905 +
   6.906 +
   6.907 +\subsection{Tactics and tacticals}
   6.908 +\index{tactics|bold}\index{tacticals|bold}
   6.909 +{\bf Tactics} perform backward proof.  Isabelle tactics differ from those
   6.910 +of {\sc lcf}, {\sc hol} and Nuprl by operating on entire proof states,
   6.911 +rather than on individual subgoals.  An Isabelle tactic is a function that
   6.912 +takes a proof state and returns a sequence (lazy list) of possible
   6.913 +successor states.  Sequences are coded in ML as functions, a standard
   6.914 +technique~\cite{paulson91}.  Isabelle represents proof states by theorems.
   6.915 +
   6.916 +Basic tactics execute the meta-rules described above, operating on a
   6.917 +given subgoal.  The {\bf resolution tactics} take a list of rules and
   6.918 +return next states for each combination of rule and unifier.  The {\bf
   6.919 +assumption tactic} examines the subgoal's assumptions and returns next
   6.920 +states for each combination of assumption and unifier.  Lazy lists are
   6.921 +essential because higher-order resolution may return infinitely many
   6.922 +unifiers.  If there are no matching rules or assumptions then no next
   6.923 +states are generated; a tactic application that returns an empty list is
   6.924 +said to {\bf fail}.
   6.925 +
   6.926 +Sequences realize their full potential with {\bf tacticals} --- operators
   6.927 +for combining tactics.  Depth-first search, breadth-first search and
   6.928 +best-first search (where a heuristic function selects the best state to
   6.929 +explore) return their outcomes as a sequence.  Isabelle provides such
   6.930 +procedures in the form of tacticals.  Simpler procedures can be expressed
   6.931 +directly using the basic tacticals {\it THEN}, {\it ORELSE} and {\it REPEAT}:
   6.932 +\begin{description}
   6.933 +\item[$tac1\;THEN\;tac2$] is a tactic for sequential composition.  Applied
   6.934 +to a proof state, it returns all states reachable in two steps by applying
   6.935 +$tac1$ followed by~$tac2$.
   6.936 +
   6.937 +\item[$tac1\;ORELSE\;tac2$] is a choice tactic.  Applied to a state, it
   6.938 +tries~$tac1$ and returns the result if non-empty; otherwise, it uses~$tac2$.
   6.939 +
   6.940 +\item[$REPEAT\;tac$] is a repetition tactic.  Applied to a state, it
   6.941 +returns all states reachable by applying~$tac$ as long as possible (until
   6.942 +it would fail).  $REPEAT$ can be expressed in a few lines of \ML{} using
   6.943 +{\it THEN} and~{\it ORELSE}.
   6.944 +\end{description}
   6.945 +For instance, this tactic repeatedly applies $tac1$ and~$tac2$, giving
   6.946 +$tac1$ priority:
   6.947 +\[ REPEAT(tac1\;ORELSE\;tac2) \]
   6.948 +
   6.949 +
   6.950 +\section{Variations on resolution}
   6.951 +In principle, resolution and proof by assumption suffice to prove all
   6.952 +theorems.  However, specialized forms of resolution are helpful for working
   6.953 +with elimination rules.  Elim-resolution applies an elimination rule to an
   6.954 +assumption; destruct-resolution is similar, but applies a rule in a forward
   6.955 +style.
   6.956 +
   6.957 +The last part of the section shows how the techniques for proving theorems
   6.958 +can also serve to derive rules.
   6.959 +
   6.960 +\subsection{Elim-resolution}
   6.961 +\index{elim-resolution|bold}
   6.962 +Consider proving the theorem $((R\disj R)\disj R)\disj R\imp R$.  By
   6.963 +$({\imp}I)$, we prove $R$ from the assumption $((R\disj R)\disj R)\disj R$.
   6.964 +Applying $(\disj E)$ to this assumption yields two subgoals, one that
   6.965 +assumes~$R$ (and is therefore trivial) and one that assumes $(R\disj
   6.966 +R)\disj R$.  This subgoal admits another application of $(\disj E)$.  Since
   6.967 +natural deduction never discards assumptions, we eventually generate a
   6.968 +subgoal containing much that is redundant:
   6.969 +\[ \List{((R\disj R)\disj R)\disj R; (R\disj R)\disj R; R\disj R; R} \Imp R. \]
   6.970 +In general, using $(\disj E)$ on the assumption $P\disj Q$ creates two new
   6.971 +subgoals with the additional assumption $P$ or~$Q$.  In these subgoals,
   6.972 +$P\disj Q$ is redundant.  It wastes space; worse, it could make a theorem
   6.973 +prover repeatedly apply~$(\disj E)$, looping.  Other elimination rules pose
   6.974 +similar problems.  In first-order logic, only universally quantified
   6.975 +assumptions are sometimes needed more than once --- say, to prove
   6.976 +$P(f(f(a)))$ from the assumptions $\forall x.P(x)\imp P(f(x))$ and~$P(a)$.
   6.977 +
   6.978 +Many logics can be formulated as sequent calculi that delete redundant
   6.979 +assumptions after use.  The rule $(\disj E)$ might become
   6.980 +\[ \infer[\disj\hbox{-left}]
   6.981 +         {\Gamma,P\disj Q,\Delta \turn \Theta}
   6.982 +         {\Gamma,P,\Delta \turn \Theta && \Gamma,Q,\Delta \turn \Theta}  \] 
   6.983 +In backward proof, a goal containing $P\disj Q$ on the left of the~$\turn$
   6.984 +(that is, as an assumption) splits into two subgoals, replacing $P\disj Q$
   6.985 +by $P$ or~$Q$.  But the sequent calculus, with its explicit handling of
   6.986 +assumptions, can be tiresome to use.
   6.987 +
   6.988 +Elim-resolution is Isabelle's way of getting sequent calculus behaviour
   6.989 +from natural deduction rules.  It lets an elimination rule consume an
   6.990 +assumption.  Elim-resolution takes a rule $\List{\psi@1; \ldots; \psi@m}
   6.991 +\Imp \psi$ a proof state $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, and a
   6.992 +subgoal number~$i$.  The rule must have at least one premise, thus $m>0$.
   6.993 +Write the rule's lifted form as $\List{\psi'@1; \ldots; \psi'@m} \Imp
   6.994 +\psi'$.  Ordinary resolution would attempt to reduce~$\phi@i$,
   6.995 +replacing subgoal~$i$ by $m$ new ones.  Elim-resolution tries {\bf
   6.996 +simultaneously} to reduce~$\phi@i$ and to solve~$\psi'@1$ by assumption; it
   6.997 +returns a sequence of next states.  Each of these replaces subgoal~$i$ by
   6.998 +instances of $\psi'@2$, \ldots, $\psi'@m$ from which the selected
   6.999 +assumption has been deleted.  Suppose $\phi@i$ has the parameter~$x$ and
  6.1000 +assumptions $\theta@1$,~\ldots,~$\theta@k$.  Then $\psi'@1$, the rule's first
  6.1001 +premise after lifting, will be
  6.1002 +\( \Forall x. \List{\theta@1; \ldots; \theta@k}\Imp \psi^{x}@1 \).
  6.1003 +Elim-resolution tries to unify simultaneously $\psi'\qeq\phi@i$ and
  6.1004 +$\lambda x. \theta@j \qeq \lambda x. \psi^{x}@1$, for $j=1$,~\ldots,~$k$.
  6.1005 +
  6.1006 +Let us redo the example from~\S\ref{prop-proof}.  The elimination rule
  6.1007 +is~$(\disj E)$,
  6.1008 +\[ \List{\Var{P}\disj \Var{Q};\; \Var{P}\Imp \Var{R};\; \Var{Q}\Imp \Var{R}}
  6.1009 +      \Imp \Var{R}  \]
  6.1010 +and the proof state is $(P\disj P\Imp P)\Imp (P\disj P\imp P)$.  The
  6.1011 +lifted rule would be
  6.1012 +\[ \begin{array}{l@{}l}
  6.1013 +  \lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\
  6.1014 +           & \List{P\disj P ;\; \Var{P@1}} \Imp \Var{R@1};    \\
  6.1015 +           & \List{P\disj P ;\; \Var{Q@1}} \Imp \Var{R@1}     \\
  6.1016 +  \rbrakk\;& \Imp \Var{R@1}
  6.1017 +  \end{array} 
  6.1018 +\]
  6.1019 +Unification would take the simultaneous equations
  6.1020 +$P\disj P \qeq \Var{P@1}\disj\Var{Q@1}$ and $\Var{R@1} \qeq P$, yielding
  6.1021 +$\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$.  The new proof state
  6.1022 +would be simply
  6.1023 +\[ \List{P \Imp P;\; P \Imp P} \Imp (P\disj P\imp P). 
  6.1024 +\]
  6.1025 +Elim-resolution's simultaneous unification gives better control
  6.1026 +than ordinary resolution.  Recall the substitution rule:
  6.1027 +$$ \List{\Var{t}=\Var{u}; \Var{P}(\Var{t})} \Imp \Var{P}(\Var{u}) 
  6.1028 +   \eqno(subst) $$
  6.1029 +Unsuitable for ordinary resolution because $\Var{P}(\Var{u})$ admits many
  6.1030 +unifiers, $(subst)$ works well with elim-resolution.  It deletes some
  6.1031 +assumption of the form $x=y$ and replaces every~$y$ by~$x$ in the subgoal
  6.1032 +formula.  The simultaneous unification instantiates $\Var{u}$ to~$y$; if
  6.1033 +$y$ is not an unknown, then $\Var{P}(y)$ can easily be unified with another
  6.1034 +formula.  
  6.1035 +
  6.1036 +In logical parlance, the premise containing the connective to be eliminated
  6.1037 +is called the \bfindex{major premise}.  Elim-resolution expects the major
  6.1038 +premise to come first.  The order of the premises is significant in
  6.1039 +Isabelle.
  6.1040 +
  6.1041 +\subsection{Destruction rules} \label{destruct}
  6.1042 +\index{destruction rules|bold}\index{proof!forward}
  6.1043 +Looking back to Figure~\ref{fol-fig}, notice that there are two kinds of
  6.1044 +elimination rule.  The rules $({\conj}E1)$, $({\conj}E2)$, $({\imp}E)$ and
  6.1045 +$({\forall}E)$ extract the conclusion from the major premise.  In Isabelle
  6.1046 +parlance, such rules are called \bfindex{destruction rules}; they are readable
  6.1047 +and easy to use in forward proof.  The rules $({\disj}E)$, $({\bot}E)$ and
  6.1048 +$({\exists}E)$ work by discharging assumptions; they support backward proof
  6.1049 +in a style reminiscent of the sequent calculus.
  6.1050 +
  6.1051 +The latter style is the most general form of elimination rule.  In natural
  6.1052 +deduction, there is no way to recast $({\disj}E)$, $({\bot}E)$ or
  6.1053 +$({\exists}E)$ as destruction rules.  But we can write general elimination
  6.1054 +rules for $\conj$, $\imp$ and~$\forall$:
  6.1055 +\[
  6.1056 +\infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \qquad
  6.1057 +\infer{R}{P\imp Q & P & \infer*{R}{[Q]}}  \qquad
  6.1058 +\infer{Q}{\forall x.P & \infer*{Q}{[P[t/x]]}} 
  6.1059 +\]
  6.1060 +Because they are concise, destruction rules are simpler to derive than the
  6.1061 +corresponding elimination rules.  To facilitate their use in backward
  6.1062 +proof, Isabelle provides a means of transforming a destruction rule such as
  6.1063 +\[ \infer[\quad\hbox{to the elimination rule}\quad]{Q}{P@1 & \ldots & P@m} 
  6.1064 +   \infer{R.}{P@1 & \ldots & P@m & \infer*{R}{[Q]}} 
  6.1065 +\]
  6.1066 +\index{destruct-resolution|bold}
  6.1067 +{\bf Destruct-resolution} combines this transformation with
  6.1068 +elim-resolution.  It applies a destruction rule to some assumption of a
  6.1069 +subgoal.  Given the rule above, it replaces the assumption~$P@1$ by~$Q$,
  6.1070 +with new subgoals of showing instances of $P@2$, \ldots,~$P@m$.
  6.1071 +Destruct-resolution works forward from a subgoal's assumptions.  Ordinary
  6.1072 +resolution performs forward reasoning from theorems, as illustrated
  6.1073 +in~\S\ref{joining}. 
  6.1074 +
  6.1075 +
  6.1076 +\subsection{Deriving rules by resolution}  \label{deriving}
  6.1077 +\index{rules!derived|bold}
  6.1078 +The meta-logic, itself a form of the predicate calculus, is defined by a
  6.1079 +system of natural deduction rules.  Each theorem may depend upon
  6.1080 +meta-assumptions.  The theorem that~$\phi$ follows from the assumptions
  6.1081 +$\phi@1$, \ldots, $\phi@n$ is written
  6.1082 +\[ \phi \quad [\phi@1,\ldots,\phi@n]. \]
  6.1083 +A more conventional notation might be $\phi@1,\ldots,\phi@n \turn \phi$,
  6.1084 +but Isabelle's notation is more readable with large formulae.
  6.1085 +
  6.1086 +Meta-level natural deduction provides a convenient mechanism for deriving
  6.1087 +new object-level rules.  To derive the rule
  6.1088 +\[ \infer{\phi,}{\theta@1 & \ldots & \theta@k} \]
  6.1089 +assume the premises $\theta@1$,~\ldots,~$\theta@k$ at the
  6.1090 +meta-level.  Then prove $\phi$, possibly using these assumptions.
  6.1091 +Starting with a proof state $\phi\Imp\phi$, assumptions may accumulate,
  6.1092 +reaching a final state such as
  6.1093 +\[ \phi \quad [\theta@1,\ldots,\theta@k]. \]
  6.1094 +The meta-rule for $\Imp$ introduction discharges an assumption.
  6.1095 +Discharging them in the order $\theta@k,\ldots,\theta@1$ yields the
  6.1096 +meta-theorem $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, with no
  6.1097 +assumptions.  This represents the desired rule.
  6.1098 +Let us derive the general $\conj$ elimination rule:
  6.1099 +$$ \infer{R}{P\conj Q & \infer*{R}{[P,Q]}}  \eqno(\conj E)$$
  6.1100 +We assume $P\conj Q$ and $\List{P;Q}\Imp R$, and commence backward proof in
  6.1101 +the state $R\Imp R$.  Resolving this with the second assumption yields the
  6.1102 +state 
  6.1103 +\[ \phantom{\List{P\conj Q;\; P\conj Q}}
  6.1104 +   \llap{$\List{P;Q}$}\Imp R \quad [\,\List{P;Q}\Imp R\,]. \]
  6.1105 +Resolving subgoals~1 and~2 with $({\conj}E1)$ and $({\conj}E2)$,
  6.1106 +respectively, yields the state
  6.1107 +\[ \List{P\conj Q;\; P\conj Q}\Imp R \quad [\,\List{P;Q}\Imp R\,]. \]
  6.1108 +Resolving both subgoals with the assumption $P\conj Q$ yields
  6.1109 +\[ R \quad [\, \List{P;Q}\Imp R, P\conj Q \,]. \]
  6.1110 +The proof may use the meta-assumptions in any order, and as often as
  6.1111 +necessary; when finished, we discharge them in the correct order to
  6.1112 +obtain the desired form:
  6.1113 +\[ \List{P\conj Q;\; \List{P;Q}\Imp R} \Imp R \]
  6.1114 +We have derived the rule using free variables, which prevents their
  6.1115 +premature instantiation during the proof; we may now replace them by
  6.1116 +schematic variables.
  6.1117 +
  6.1118 +\begin{warn}
  6.1119 +Schematic variables are not allowed in (meta) assumptions because they would
  6.1120 +complicate lifting.  Assumptions remain fixed throughout a proof.
  6.1121 +\end{warn}
  6.1122 +
  6.1123 +% Local Variables: 
  6.1124 +% mode: latex
  6.1125 +% TeX-master: t
  6.1126 +% End: 
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/doc-src/Intro/gate.thy	Wed Nov 10 05:06:55 1993 +0100
     7.3 @@ -0,0 +1,5 @@
     7.4 +Gate = FOL +
     7.5 +consts  nand,xor :: "[o,o] => o"
     7.6 +rules   nand_def "nand(P,Q) == ~(P & Q)"
     7.7 +        xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
     7.8 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/doc-src/Intro/gate2.thy	Wed Nov 10 05:06:55 1993 +0100
     8.3 @@ -0,0 +1,8 @@
     8.4 +Gate2 = FOL +
     8.5 +consts  "~&"     :: "[o,o] => o" (infixl 35)
     8.6 +        "#"      :: "[o,o] => o" (infixl 30)
     8.7 +        If       :: "[o,o,o] => o"       ("if _ then _ else _")
     8.8 +rules   nand_def "P ~& Q == ~(P & Q)"    
     8.9 +        xor_def  "P # Q  == P & ~Q | ~P & Q"
    8.10 +        If_def   "if P then Q else R == P&Q | ~P&R"
    8.11 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/doc-src/Intro/getting.tex	Wed Nov 10 05:06:55 1993 +0100
     9.3 @@ -0,0 +1,896 @@
     9.4 +%% $Id$
     9.5 +\part{Getting started with Isabelle}
     9.6 +This Part describes how to perform simple proofs using Isabelle.  Although
     9.7 +it frequently refers to concepts from the previous Part, a user can get
     9.8 +started without understanding them in detail.
     9.9 +
    9.10 +As of this writing, Isabelle's user interface is \ML.  Proofs are conducted
    9.11 +by applying certain \ML{} functions, which update a stored proof state.
    9.12 +Logics are combined and extended by calling \ML{} functions.  All syntax
    9.13 +must be expressed using {\sc ascii} characters.  Menu-driven graphical
    9.14 +interfaces are under construction, but Isabelle users will always need to
    9.15 +know some \ML, at least to use tacticals.
    9.16 +
    9.17 +Object-logics are built upon Pure Isabelle, which implements the meta-logic
    9.18 +and provides certain fundamental data structures: types, terms, signatures,
    9.19 +theorems and theories, tactics and tacticals.  These data structures have
    9.20 +the corresponding \ML{} types {\tt typ}, {\tt term}, {\tt Sign.sg}, {\tt thm},
    9.21 +{\tt theory} and {\tt tactic}; tacticals have function types such as {\tt
    9.22 +tactic->tactic}.  Isabelle users can operate on these data structures by
    9.23 +writing \ML{} programs.
    9.24 +
    9.25 +\section{Forward proof}
    9.26 +\index{Isabelle!getting started}\index{ML}
    9.27 +This section describes the concrete syntax for types, terms and theorems,
    9.28 +and demonstrates forward proof.
    9.29 +
    9.30 +\subsection{Lexical matters}
    9.31 +\index{identifiers|bold}\index{reserved words|bold} 
    9.32 +An {\bf identifier} is a string of letters, digits, underscores~(\verb|_|)
    9.33 +and single quotes~({\tt'}), beginning with a letter.  Single quotes are
    9.34 +regarded as primes; for instance {\tt x'} is read as~$x'$.  Identifiers are
    9.35 +separated by white space and special characters.  {\bf Reserved words} are
    9.36 +identifiers that appear in Isabelle syntax definitions.
    9.37 +
    9.38 +An Isabelle theory can declare symbols composed of special characters, such
    9.39 +as {\tt=}, {\tt==}, {\tt=>} and {\tt==>}.  (The latter three are part of
    9.40 +the syntax of the meta-logic.)  Such symbols may be run together; thus if
    9.41 +\verb|}| and \verb|{| are used for set brackets then \verb|{{a},{a,b}}| is
    9.42 +valid notation for a set of sets --- but only if \verb|}}| and \verb|{{|
    9.43 +have not been declared as symbols!  The parser resolves any ambiguity by
    9.44 +taking the longest possible symbol that has been declared.  Thus the string
    9.45 +{\tt==>} is read as a single symbol.  But \hbox{\tt= =>} is read as two
    9.46 +symbols, as is \verb|}}|, as discussed above.
    9.47 +
    9.48 +Identifiers that are not reserved words may serve as free variables or
    9.49 +constants.  A type identifier consists of an identifier prefixed by a
    9.50 +prime, for example {\tt'a} and \hbox{\tt'hello}.  An unknown (or type
    9.51 +unknown) consists of a question mark, an identifier (or type identifier),
    9.52 +and a subscript.  The subscript, a non-negative integer, allows the
    9.53 +renaming of unknowns prior to unification.
    9.54 +
    9.55 +The subscript may appear after the identifier, separated by a dot; this
    9.56 +prevents ambiguity when the identifier ends with a digit.  Thus {\tt?z6.0}
    9.57 +has identifier \verb|"z6"| and subscript~0, while {\tt?a0.5} has identifier
    9.58 +\verb|"a0"| and subscript~5.  If the identifier does not end with a digit,
    9.59 +then no dot appears and a subscript of~0 is omitted; for example,
    9.60 +{\tt?hello} has identifier \verb|"hello"| and subscript zero, while
    9.61 +{\tt?z6} has identifier \verb|"z"| and subscript~6.  The same conventions
    9.62 +apply to type unknowns.  Note that the question mark is {\bf not} part of the
    9.63 +identifier! 
    9.64 +
    9.65 +
    9.66 +\subsection{Syntax of types and terms}
    9.67 +\index{Isabelle!syntax of}
    9.68 +\index{classes!built-in|bold}
    9.69 +Classes are denoted by identifiers; the built-in class \ttindex{logic}
    9.70 +contains the `logical' types.  Sorts are lists of classes enclosed in
    9.71 +braces~\{ and \}; singleton sorts may be abbreviated by dropping the braces.
    9.72 +
    9.73 +\index{types!syntax|bold}
    9.74 +Types are written with a syntax like \ML's.  The built-in type \ttindex{prop}
    9.75 +is the type of propositions.  Type variables can be constrained to particular
    9.76 +classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\{ord,arith\}}.
    9.77 +\[\dquotes
    9.78 +\begin{array}{lll}
    9.79 +    \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline
    9.80 +  t "::" C              & t :: C        & \hbox{class constraint} \\
    9.81 +  t "::" "\{"   C@1 "," \ldots "," C@n "\}" &
    9.82 +     t :: \{C@1,\dots,C@n\}             & \hbox{sort constraint} \\
    9.83 +  \sigma"=>"\tau        & \sigma\To\tau & \hbox{function type} \\
    9.84 +  "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau &
    9.85 +     [\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\
    9.86 +  "(" \tau@1"," \ldots "," \tau@n ")" tycon & 
    9.87 +     (\tau@1, \ldots, \tau@n)tycon      & \hbox{type construction}
    9.88 +\end{array} 
    9.89 +\]
    9.90 +Terms are those of the typed $\lambda$-calculus.
    9.91 +\index{terms!syntax|bold}
    9.92 +\[\dquotes
    9.93 +\begin{array}{lll}
    9.94 +    \multicolumn{3}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
    9.95 +  t "::" \sigma         & t :: \sigma   & \hbox{type constraint} \\
    9.96 +  "\%" x "." t          & \lambda x.t   & \hbox{abstraction} \\
    9.97 +  "\%" x@1\ldots x@n "." t  & \lambda x@1\ldots x@n.t & 
    9.98 +     \hbox{curried abstraction} \\
    9.99 +  t "(" u@1"," \ldots "," u@n ")" & 
   9.100 +  t (u@1, \ldots, u@n) & \hbox{curried application}
   9.101 +\end{array}  
   9.102 +\]
   9.103 +The theorems and rules of an object-logic are represented by theorems in
   9.104 +the meta-logic, which are expressed using meta-formulae.  Since the
   9.105 +meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{}
   9.106 +are just terms of type~\ttindex{prop}.  
   9.107 +\index{meta-formulae!syntax|bold}
   9.108 +\[\dquotes
   9.109 +  \begin{array}{l@{\quad}l@{\quad}l}
   9.110 +    \multicolumn{3}{c}{\hbox{ASCII Notation for Meta-Formulae}} \\ \hline
   9.111 +  a " == " b    & a\equiv b &   \hbox{meta-equality} \\
   9.112 +  a " =?= " b   & a\qeq b &     \hbox{flex-flex constraint} \\
   9.113 +  \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\
   9.114 +  "[|" \phi@1 ";" \ldots ";" \phi@n "|] ==> " \psi & 
   9.115 +  \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\
   9.116 +  "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\
   9.117 +  "!!" x@1\ldots x@n "." \phi & 
   9.118 +  \Forall x@1. \ldots \Forall x@n.\phi & \hbox{nested quantification}
   9.119 +  \end{array}
   9.120 +\]
   9.121 +Flex-flex constraints are meta-equalities arising from unification; they
   9.122 +require special treatment.  See~\S\ref{flexflex}.
   9.123 +\index{flex-flex equations}
   9.124 +
   9.125 +Most logics define the implicit coercion $Trueprop$ from object-formulae to
   9.126 +propositions.  
   9.127 +\index{Trueprop@{$Trueprop$}}
   9.128 +This could cause an ambiguity: in $P\Imp Q$, do the variables $P$ and $Q$
   9.129 +stand for meta-formulae or object-formulae?  If the latter, $P\Imp Q$
   9.130 +really abbreviates $Trueprop(P)\Imp Trueprop(Q)$.  To prevent such
   9.131 +ambiguities, Isabelle's syntax does not allow a meta-formula to consist of
   9.132 +a variable.  Variables of type~\ttindex{prop} are seldom useful, but you
   9.133 +can make a variable stand for a meta-formula by prefixing it with the
   9.134 +keyword \ttindex{PROP}:
   9.135 +\begin{ttbox} 
   9.136 +PROP ?psi ==> PROP ?theta 
   9.137 +\end{ttbox}
   9.138 +
   9.139 +Symbols of object-logics also must be rendered into {\sc ascii}, typically
   9.140 +as follows:
   9.141 +\[ \begin{tabular}{l@{\quad}l@{\quad}l}
   9.142 +      \tt True          & $\top$        & true \\
   9.143 +      \tt False         & $\bot$        & false \\
   9.144 +      \tt $P$ \& $Q$    & $P\conj Q$    & conjunction \\
   9.145 +      \tt $P$ | $Q$     & $P\disj Q$    & disjunction \\
   9.146 +      \verb'~' $P$      & $\neg P$      & negation \\
   9.147 +      \tt $P$ --> $Q$   & $P\imp Q$     & implication \\
   9.148 +      \tt $P$ <-> $Q$   & $P\bimp Q$    & bi-implication \\
   9.149 +      \tt ALL $x\,y\,z$ .\ $P$  & $\forall x\,y\,z.P$   & for all \\
   9.150 +      \tt EX  $x\,y\,z$ .\ $P$  & $\exists x\,y\,z.P$   & there exists
   9.151 +   \end{tabular}
   9.152 +\]
   9.153 +To illustrate the notation, consider two axioms for first-order logic:
   9.154 +$$ \List{P; Q} \Imp P\conj Q                 \eqno(\conj I) $$
   9.155 +$$ \List{\exists x.P(x);  \Forall x. P(x)\imp Q} \Imp Q  \eqno(\exists E) $$
   9.156 +Using the {\tt [|\ldots|]} shorthand, $({\conj}I)$ translates literally into
   9.157 +{\sc ascii} characters as
   9.158 +\begin{ttbox}
   9.159 +[| ?P; ?Q |] ==> ?P & ?Q
   9.160 +\end{ttbox}
   9.161 +The schematic variables let unification instantiate the rule.  To
   9.162 +avoid cluttering rules with question marks, Isabelle converts any free
   9.163 +variables in a rule to schematic variables; we normally write $({\conj}I)$ as
   9.164 +\begin{ttbox}
   9.165 +[| P; Q |] ==> P & Q
   9.166 +\end{ttbox}
   9.167 +This variables convention agrees with the treatment of variables in goals.
   9.168 +Free variables in a goal remain fixed throughout the proof.  After the
   9.169 +proof is finished, Isabelle converts them to scheme variables in the
   9.170 +resulting theorem.  Scheme variables in a goal may be replaced by terms
   9.171 +during the proof, supporting answer extraction, program synthesis, and so
   9.172 +forth.
   9.173 +
   9.174 +For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as
   9.175 +\begin{ttbox}
   9.176 +[| EX x.P(x);  !!x. P(x) ==> Q |] ==> Q
   9.177 +\end{ttbox}
   9.178 +
   9.179 +
   9.180 +\subsection{Basic operations on theorems}
   9.181 +\index{theorems!basic operations on|bold}
   9.182 +\index{LCF}
   9.183 +Meta-level theorems have type \ttindex{thm} and represent the theorems and
   9.184 +inference rules of object-logics.  Isabelle's meta-logic is implemented
   9.185 +using the {\sc lcf} approach: each meta-level inference rule is represented by
   9.186 +a function from theorems to theorems.  Object-level rules are taken as
   9.187 +axioms.
   9.188 +
   9.189 +The main theorem printing commands are {\tt prth}, {\tt prths} and~{\tt
   9.190 +  prthq}.  Of the other operations on theorems, most useful are {\tt RS}
   9.191 +and {\tt RSN}, which perform resolution.
   9.192 +
   9.193 +\index{printing commands|bold}
   9.194 +\begin{description}
   9.195 +\item[\ttindexbold{prth} {\it thm}]  pretty-prints {\it thm\/} at the terminal.
   9.196 +
   9.197 +\item[\ttindexbold{prths} {\it thms}]  pretty-prints {\it thms}, a list of
   9.198 +theorems.
   9.199 +
   9.200 +\item[\ttindexbold{prthq} {\it thmq}]  pretty-prints {\it thmq}, a sequence of
   9.201 +theorems; this is useful for inspecting the output of a tactic.
   9.202 +
   9.203 +\item[\tt$thm1$ RS $thm2$] \indexbold{*RS} resolves the conclusion of $thm1$
   9.204 +with the first premise of~$thm2$.
   9.205 +
   9.206 +\item[\tt$thm1$ RSN $(i,thm2)$] \indexbold{*RSN} resolves the conclusion of $thm1$
   9.207 +with the $i$th premise of~$thm2$.
   9.208 +
   9.209 +\item[\ttindexbold{standard} $thm$]  puts $thm$ into a standard
   9.210 +format.  It also renames schematic variables to have subscript zero,
   9.211 +improving readability and reducing subscript growth.
   9.212 +\end{description}
   9.213 +\index{ML}
   9.214 +The rules of a theory are normally bound to \ML\ identifiers.  Suppose we
   9.215 +are running an Isabelle session containing natural deduction first-order
   9.216 +logic.  Let us try an example given in~\S\ref{joining}.  We first print
   9.217 +\ttindex{mp}, which is the rule~$({\imp}E)$, then resolve it with itself.
   9.218 +\begin{ttbox} 
   9.219 +prth mp; 
   9.220 +{\out [| ?P --> ?Q; ?P |] ==> ?Q}
   9.221 +{\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm}
   9.222 +prth (mp RS mp);
   9.223 +{\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q}
   9.224 +{\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm}
   9.225 +\end{ttbox}
   9.226 +In the Isabelle documentation, user's input appears in {\tt typewriter
   9.227 +  characters}, and output appears in {\sltt slanted typewriter characters}.
   9.228 +\ML's response {\out val }~\ldots{} is compiler-dependent and will
   9.229 +sometimes be suppressed.  This session illustrates two formats for the
   9.230 +display of theorems.  Isabelle's top-level displays theorems as ML values,
   9.231 +enclosed in quotes.\footnote{This works under both Poly/ML and Standard ML
   9.232 +  of New Jersey.} Printing functions like {\tt prth} omit the quotes and
   9.233 +the surrounding {\tt val \ldots :\ thm}.
   9.234 +
   9.235 +To contrast {\tt RS} with {\tt RSN}, we resolve
   9.236 +\ttindex{conjunct1}, which stands for~$(\conj E1)$, with~\ttindex{mp}.
   9.237 +\begin{ttbox} 
   9.238 +conjunct1 RS mp;
   9.239 +{\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm}
   9.240 +conjunct1 RSN (2,mp);
   9.241 +{\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm}
   9.242 +\end{ttbox}
   9.243 +These correspond to the following proofs:
   9.244 +\[ \infer[({\imp}E)]{Q}{\infer[({\conj}E1)]{P\imp Q}{(P\imp Q)\conj Q@1} & P}
   9.245 +   \qquad
   9.246 +   \infer[({\imp}E)]{Q}{P\imp Q & \infer[({\conj}E1)]{P}{P\conj Q@1}} 
   9.247 +\]
   9.248 +The printing commands return their argument; the \ML{} identifier~{\tt it}
   9.249 +denotes the value just printed.  You may derive a rule by pasting other
   9.250 +rules together.  Below, \ttindex{spec} stands for~$(\forall E)$:
   9.251 +\begin{ttbox} 
   9.252 +spec;
   9.253 +{\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm}
   9.254 +it RS mp;
   9.255 +{\out val it = "[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==> ?Q2(?x1)" : thm}
   9.256 +it RS conjunct1;
   9.257 +{\out val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==> ?P6(?x2)"}
   9.258 +standard it;
   9.259 +{\out val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==> ?Pa(?x)"}
   9.260 +\end{ttbox}
   9.261 +By resolving $(\forall E)$ with (${\imp}E)$ and (${\conj}E1)$, we have
   9.262 +derived a destruction rule for formulae of the form $\forall x.
   9.263 +P(x)\imp(Q(x)\conj R(x))$.  Used with destruct-resolution, such specialized
   9.264 +rules provide a way of referring to particular assumptions.
   9.265 +
   9.266 +\subsection{Flex-flex equations} \label{flexflex}
   9.267 +\index{flex-flex equations|bold}\index{unknowns!of function type}
   9.268 +In higher-order unification, {\bf flex-flex} equations are those where both
   9.269 +sides begin with a function unknown, such as $\Var{f}(0)\qeq\Var{g}(0)$.
   9.270 +They admit a trivial unifier, here $\Var{f}\equiv \lambda x.\Var{a}$ and
   9.271 +$\Var{g}\equiv \lambda y.\Var{a}$, where $\Var{a}$ is a new unknown.  They
   9.272 +admit many other unifiers, such as $\Var{f} \equiv \lambda x.\Var{g}(0)$
   9.273 +and $\{\Var{f} \equiv \lambda x.x,\, \Var{g} \equiv \lambda x.0\}$.  Huet's
   9.274 +procedure does not enumerate the unifiers; instead, it retains flex-flex
   9.275 +equations as constraints on future unifications.  Flex-flex constraints
   9.276 +occasionally become attached to a proof state; more frequently, they appear
   9.277 +during use of {\tt RS} and~{\tt RSN}:
   9.278 +\begin{ttbox} 
   9.279 +refl;
   9.280 +{\out val it = "?a = ?a" : thm}
   9.281 +exI;
   9.282 +{\out val it = "?P(?x) ==> EX x. ?P(x)" : thm}
   9.283 +refl RS exI;
   9.284 +{\out val it = "?a3(?x) =?= ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)" : thm}
   9.285 +\end{ttbox}
   9.286 +
   9.287 +\noindent
   9.288 +Renaming variables, this is $\exists x.\Var{f}(x)=\Var{g}(x)$ with
   9.289 +the constraint ${\Var{f}(\Var{u})\qeq\Var{g}(\Var{u})}$.  Instances
   9.290 +satisfying the constraint include $\exists x.\Var{f}(x)=\Var{f}(x)$ and
   9.291 +$\exists x.x=\Var{u}$.  Calling \ttindex{flexflex_rule} removes all
   9.292 +constraints by applying the trivial unifier:\index{*prthq}
   9.293 +\begin{ttbox} 
   9.294 +prthq (flexflex_rule it);
   9.295 +{\out EX x. ?a4 = ?a4}
   9.296 +\end{ttbox} 
   9.297 +Isabelle simplifies flex-flex equations to eliminate redundant bound
   9.298 +variables.  In $\lambda x\,y.\Var{f}(k(y),x) \qeq \lambda x\,y.\Var{g}(y)$,
   9.299 +there is no bound occurrence of~$x$ on the right side; thus, there will be
   9.300 +none on the left, in a common instance of these terms.  Choosing a new
   9.301 +variable~$\Var{h}$, Isabelle assigns $\Var{f}\equiv \lambda u\,v.?h(u)$,
   9.302 +simplifying the left side to $\lambda x\,y.\Var{h}(k(y))$.  Dropping $x$
   9.303 +from the equation leaves $\lambda y.\Var{h}(k(y)) \qeq \lambda
   9.304 +y.\Var{g}(y)$.  By $\eta$-conversion, this simplifies to the assignment
   9.305 +$\Var{g}\equiv\lambda y.?h(k(y))$.
   9.306 +
   9.307 +\begin{warn}
   9.308 +\ttindex{RS} and \ttindex{RSN} fail (by raising exception {\tt THM}) unless
   9.309 +the resolution delivers {\bf exactly one} resolvent.  For multiple results,
   9.310 +use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists.  The
   9.311 +following example uses \ttindex{read_instantiate} to create an instance
   9.312 +of \ttindex{refl} containing no schematic variables.
   9.313 +\begin{ttbox} 
   9.314 +val reflk = read_instantiate [("a","k")] refl;
   9.315 +{\out val reflk = "k = k" : thm}
   9.316 +\end{ttbox}
   9.317 +
   9.318 +\noindent
   9.319 +A flex-flex constraint is no longer possible; resolution does not find a
   9.320 +unique unifier:
   9.321 +\begin{ttbox} 
   9.322 +reflk RS exI;
   9.323 +{\out uncaught exception THM}
   9.324 +\end{ttbox}
   9.325 +Using \ttindex{RL} this time, we discover that there are four unifiers, and
   9.326 +four resolvents:
   9.327 +\begin{ttbox} 
   9.328 +[reflk] RL [exI];
   9.329 +{\out val it = ["EX x. x = x", "EX x. k = x",}
   9.330 +{\out           "EX x. x = k", "EX x. k = k"] : thm list}
   9.331 +\end{ttbox} 
   9.332 +\end{warn}
   9.333 +
   9.334 +
   9.335 +\section{Backward proof}
   9.336 +Although {\tt RS} and {\tt RSN} are fine for simple forward reasoning,
   9.337 +large proofs require tactics.  Isabelle provides a suite of commands for
   9.338 +conducting a backward proof using tactics.
   9.339 +
   9.340 +\subsection{The basic tactics}
   9.341 +\index{tactics!basic|bold}
   9.342 +The tactics {\tt assume_tac}, {\tt
   9.343 +resolve_tac}, {\tt eresolve_tac}, and {\tt dresolve_tac} suffice for most
   9.344 +single-step proofs.  Although {\tt eresolve_tac} and {\tt dresolve_tac} are
   9.345 +not strictly necessary, they simplify proofs involving elimination and
   9.346 +destruction rules.  All the tactics act on a subgoal designated by a
   9.347 +positive integer~$i$, failing if~$i$ is out of range.  The resolution
   9.348 +tactics try their list of theorems in left-to-right order.
   9.349 +
   9.350 +\begin{description}
   9.351 +\item[\ttindexbold{assume_tac} {\it i}] is the tactic that attempts to solve
   9.352 +subgoal~$i$ by assumption.  Proof by assumption is not a trivial step; it
   9.353 +can falsify other subgoals by instantiating shared variables.  There may be
   9.354 +several ways of solving the subgoal by assumption.
   9.355 +
   9.356 +\item[\ttindexbold{resolve_tac} {\it thms} {\it i}]
   9.357 +is the basic resolution tactic, used for most proof steps.  The $thms$
   9.358 +represent object-rules, which are resolved against subgoal~$i$ of the proof
   9.359 +state.  For each rule, resolution forms next states by unifying the
   9.360 +conclusion with the subgoal and inserting instantiated premises in its
   9.361 +place.  A rule can admit many higher-order unifiers.  The tactic fails if
   9.362 +none of the rules generates next states.
   9.363 +
   9.364 +\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] 
   9.365 +performs elim-resolution.  Like
   9.366 +\hbox{\tt resolve_tac {\it thms} {\it i}} followed by \hbox{\tt assume_tac
   9.367 +{\it i}}, it applies a rule then solves its first premise by assumption.
   9.368 +But {\tt eresolve_tac} additionally deletes that assumption from any
   9.369 +subgoals arising from the resolution.
   9.370 +
   9.371 +
   9.372 +\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] 
   9.373 +performs destruct-resolution with the~$thms$, as described
   9.374 +in~\S\ref{destruct}.  It is useful for forward reasoning from the
   9.375 +assumptions.
   9.376 +\end{description}
   9.377 +
   9.378 +\subsection{Commands for backward proof}
   9.379 +\index{proof!commands for|bold}
   9.380 +Tactics are normally applied using the subgoal module, which maintains a
   9.381 +proof state and manages the proof construction.  It allows interactive
   9.382 +backtracking through the proof space, going away to prove lemmas, etc.; of
   9.383 +its many commands, most important are the following:
   9.384 +\begin{description}
   9.385 +\item[\ttindexbold{goal} {\it theory} {\it formula}; ] 
   9.386 +begins a new proof, where $theory$ is usually an \ML\ identifier
   9.387 +and the {\it formula\/} is written as an \ML\ string.
   9.388 +
   9.389 +\item[\ttindexbold{by} {\it tactic}; ] 
   9.390 +applies the {\it tactic\/} to the current proof
   9.391 +state, raising an exception if the tactic fails.
   9.392 +
   9.393 +\item[\ttindexbold{undo}(); ]  
   9.394 +reverts to the previous proof state.  Undo can be repeated but cannot be
   9.395 +undone.  Do not omit the parentheses; typing {\tt undo;} merely causes \ML\
   9.396 +to echo the value of that function.
   9.397 +
   9.398 +\item[\ttindexbold{result}()] 
   9.399 +returns the theorem just proved, in a standard format.  It fails if
   9.400 +unproved subgoals are left or if the main goal does not match the one you
   9.401 +started with.
   9.402 +\end{description}
   9.403 +The commands and tactics given above are cumbersome for interactive use.
   9.404 +Although our examples will use the full commands, you may prefer Isabelle's
   9.405 +shortcuts:
   9.406 +\begin{center} \tt
   9.407 +\indexbold{*br} \indexbold{*be} \indexbold{*bd} \indexbold{*ba}
   9.408 +\begin{tabular}{l@{\qquad\rm abbreviates\qquad}l}
   9.409 +    ba {\it i};           & by (assume_tac {\it i}); \\
   9.410 +
   9.411 +    br {\it thm} {\it i}; & by (resolve_tac [{\it thm}] {\it i}); \\
   9.412 +
   9.413 +    be {\it thm} {\it i}; & by (eresolve_tac [{\it thm}] {\it i}); \\
   9.414 +
   9.415 +    bd {\it thm} {\it i}; & by (dresolve_tac [{\it thm}] {\it i}); 
   9.416 +\end{tabular}
   9.417 +\end{center}
   9.418 +
   9.419 +\subsection{A trivial example in propositional logic}
   9.420 +\index{examples!propositional}
   9.421 +Directory {\tt FOL} of the Isabelle distribution defines the \ML\
   9.422 +identifier~\ttindex{FOL.thy}, which denotes the theory of first-order
   9.423 +logic.  Let us try the example from~\S\ref{prop-proof}, entering the goal
   9.424 +$P\disj P\imp P$ in that theory.\footnote{To run these examples, see the
   9.425 +file {\tt FOL/ex/intro.ML}.}
   9.426 +\begin{ttbox}
   9.427 +goal FOL.thy "P|P --> P"; 
   9.428 +{\out Level 0} 
   9.429 +{\out P | P --> P} 
   9.430 +{\out 1. P | P --> P} 
   9.431 +\end{ttbox}
   9.432 +Isabelle responds by printing the initial proof state, which has $P\disj
   9.433 +P\imp P$ as the main goal and the only subgoal.  The \bfindex{level} of the
   9.434 +state is the number of {\tt by} commands that have been applied to reach
   9.435 +it.  We now use \ttindex{resolve_tac} to apply the rule \ttindex{impI},
   9.436 +or~$({\imp}I)$, to subgoal~1:
   9.437 +\begin{ttbox}
   9.438 +by (resolve_tac [impI] 1); 
   9.439 +{\out Level 1} 
   9.440 +{\out P | P --> P} 
   9.441 +{\out 1. P | P ==> P}
   9.442 +\end{ttbox}
   9.443 +In the new proof state, subgoal~1 is $P$ under the assumption $P\disj P$.
   9.444 +(The meta-implication {\tt==>} indicates assumptions.)  We apply
   9.445 +\ttindex{disjE}, or~(${\disj}E)$, to that subgoal:
   9.446 +\begin{ttbox}
   9.447 +by (resolve_tac [disjE] 1); 
   9.448 +{\out Level 2} 
   9.449 +{\out P | P --> P} 
   9.450 +{\out 1. P | P ==> ?P1 | ?Q1} 
   9.451 +{\out 2. [| P | P; ?P1 |] ==> P} 
   9.452 +{\out 3. [| P | P; ?Q1 |] ==> P}
   9.453 +\end{ttbox}
   9.454 +At Level~2 there are three subgoals, each provable by
   9.455 +assumption.  We deviate from~\S\ref{prop-proof} by tackling subgoal~3
   9.456 +first, using \ttindex{assume_tac}.  This updates {\tt?Q1} to~{\tt P}.
   9.457 +\begin{ttbox}
   9.458 +by (assume_tac 3); 
   9.459 +{\out Level 3} 
   9.460 +{\out P | P --> P} 
   9.461 +{\out 1. P | P ==> ?P1 | P} 
   9.462 +{\out 2. [| P | P; ?P1 |] ==> P}
   9.463 +\end{ttbox}
   9.464 +Next we tackle subgoal~2, instantiating {\tt?P1} to~{\tt P}.
   9.465 +\begin{ttbox}
   9.466 +by (assume_tac 2); 
   9.467 +{\out Level 4} 
   9.468 +{\out P | P --> P} 
   9.469 +{\out 1. P | P ==> P | P}
   9.470 +\end{ttbox}
   9.471 +Lastly we prove the remaining subgoal by assumption:
   9.472 +\begin{ttbox}
   9.473 +by (assume_tac 1); 
   9.474 +{\out Level 5} 
   9.475 +{\out P | P --> P} 
   9.476 +{\out No subgoals!}
   9.477 +\end{ttbox}
   9.478 +Isabelle tells us that there are no longer any subgoals: the proof is
   9.479 +complete.  Calling \ttindex{result} returns the theorem.
   9.480 +\begin{ttbox}
   9.481 +val mythm = result(); 
   9.482 +{\out val mythm = "?P | ?P --> ?P" : thm} 
   9.483 +\end{ttbox}
   9.484 +Isabelle has replaced the free variable~{\tt P} by the scheme
   9.485 +variable~{\tt?P}\@.  Free variables in the proof state remain fixed
   9.486 +throughout the proof.  Isabelle finally converts them to scheme variables
   9.487 +so that the resulting theorem can be instantiated with any formula.
   9.488 +
   9.489 +
   9.490 +\subsection{Proving a distributive law}
   9.491 +\index{examples!propositional}
   9.492 +To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac}
   9.493 +and the tactical \ttindex{REPEAT}, we shall prove part of the distributive
   9.494 +law $(P\conj Q)\disj R \iff (P\disj R)\conj (Q\disj R)$.
   9.495 +
   9.496 +We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it:
   9.497 +\begin{ttbox}
   9.498 +goal FOL.thy "(P & Q) | R  --> (P | R)";
   9.499 +{\out Level 0}
   9.500 +{\out P & Q | R --> P | R}
   9.501 +{\out  1. P & Q | R --> P | R}
   9.502 +by (resolve_tac [impI] 1);
   9.503 +{\out Level 1}
   9.504 +{\out P & Q | R --> P | R}
   9.505 +{\out  1. P & Q | R ==> P | R}
   9.506 +\end{ttbox}
   9.507 +Previously we applied~(${\disj}E)$ using {\tt resolve_tac}, but 
   9.508 +\ttindex{eresolve_tac} deletes the assumption after use.  The resulting proof
   9.509 +state is simpler.
   9.510 +\begin{ttbox}
   9.511 +by (eresolve_tac [disjE] 1);
   9.512 +{\out Level 2}
   9.513 +{\out P & Q | R --> P | R}
   9.514 +{\out  1. P & Q ==> P | R}
   9.515 +{\out  2. R ==> P | R}
   9.516 +\end{ttbox}
   9.517 +Using \ttindex{dresolve_tac}, we can apply~(${\conj}E1)$ to subgoal~1,
   9.518 +replacing the assumption $P\conj Q$ by~$P$.  Normally we should apply the
   9.519 +rule~(${\conj}E)$, given in~\S\ref{destruct}.  That is an elimination rule
   9.520 +and requires {\tt eresolve_tac}; it would replace $P\conj Q$ by the two
   9.521 +assumptions~$P$ and~$Q$.  The present example does not need~$Q$.
   9.522 +\begin{ttbox}
   9.523 +by (dresolve_tac [conjunct1] 1);
   9.524 +{\out Level 3}
   9.525 +{\out P & Q | R --> P | R}
   9.526 +{\out  1. P ==> P | R}
   9.527 +{\out  2. R ==> P | R}
   9.528 +\end{ttbox}
   9.529 +The next two steps apply~(${\disj}I1$) and~(${\disj}I2$) in an obvious manner.
   9.530 +\begin{ttbox}
   9.531 +by (resolve_tac [disjI1] 1);
   9.532 +{\out Level 4}
   9.533 +{\out P & Q | R --> P | R}
   9.534 +{\out  1. P ==> P}
   9.535 +{\out  2. R ==> P | R}
   9.536 +\ttbreak
   9.537 +by (resolve_tac [disjI2] 2);
   9.538 +{\out Level 5}
   9.539 +{\out P & Q | R --> P | R}
   9.540 +{\out  1. P ==> P}
   9.541 +{\out  2. R ==> R}
   9.542 +\end{ttbox}
   9.543 +Two calls of~\ttindex{assume_tac} can finish the proof.  The
   9.544 +tactical~\ttindex{REPEAT} expresses a tactic that calls {\tt assume_tac~1}
   9.545 +as many times as possible.  We can restrict attention to subgoal~1 because
   9.546 +the other subgoals move up after subgoal~1 disappears.
   9.547 +\begin{ttbox}
   9.548 +by (REPEAT (assume_tac 1));
   9.549 +{\out Level 6}
   9.550 +{\out P & Q | R --> P | R}
   9.551 +{\out No subgoals!}
   9.552 +\end{ttbox}
   9.553 +
   9.554 +
   9.555 +\section{Quantifier reasoning}
   9.556 +\index{quantifiers!reasoning about}\index{parameters}\index{unknowns}
   9.557 +This section illustrates how Isabelle enforces quantifier provisos.
   9.558 +Quantifier rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a
   9.559 +function unknown and $x$ and~$z$ are parameters.  This may be replaced by
   9.560 +any term, possibly containing free occurrences of $x$ and~$z$.
   9.561 +
   9.562 +\subsection{Two quantifier proofs, successful and not}
   9.563 +\index{examples!with quantifiers}
   9.564 +Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an
   9.565 +attempted proof of the non-theorem $\exists y.\forall x.x=y$.  The former
   9.566 +proof succeeds, and the latter fails, because of the scope of quantified
   9.567 +variables~\cite{paulson89}.  Unification helps even in these trivial
   9.568 +proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$,
   9.569 +but we need never say so. This choice is forced by the reflexive law for
   9.570 +equality, and happens automatically.
   9.571 +
   9.572 +\subsubsection{The successful proof}
   9.573 +The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules
   9.574 +$(\forall I)$ and~$(\exists I)$.  We state the goal and apply $(\forall I)$:
   9.575 +\begin{ttbox}
   9.576 +goal FOL.thy "ALL x. EX y. x=y";
   9.577 +{\out Level 0}
   9.578 +{\out ALL x. EX y. x = y}
   9.579 +{\out  1. ALL x. EX y. x = y}
   9.580 +\ttbreak
   9.581 +by (resolve_tac [allI] 1);
   9.582 +{\out Level 1}
   9.583 +{\out ALL x. EX y. x = y}
   9.584 +{\out  1. !!x. EX y. x = y}
   9.585 +\end{ttbox}
   9.586 +The variable~{\tt x} is no longer universally quantified, but is a
   9.587 +parameter in the subgoal; thus, it is universally quantified at the
   9.588 +meta-level.  The subgoal must be proved for all possible values of~{\tt x}.
   9.589 +We apply the rule $(\exists I)$:
   9.590 +\begin{ttbox}
   9.591 +by (resolve_tac [exI] 1);
   9.592 +{\out Level 2}
   9.593 +{\out ALL x. EX y. x = y}
   9.594 +{\out  1. !!x. x = ?y1(x)}
   9.595 +\end{ttbox}
   9.596 +The bound variable {\tt y} has become {\tt?y1(x)}.  This term consists of
   9.597 +the function unknown~{\tt?y1} applied to the parameter~{\tt x}.
   9.598 +Instances of {\tt?y1(x)} may or may not contain~{\tt x}.  We resolve the
   9.599 +subgoal with the reflexivity axiom.
   9.600 +\begin{ttbox}
   9.601 +by (resolve_tac [refl] 1);
   9.602 +{\out Level 3}
   9.603 +{\out ALL x. EX y. x = y}
   9.604 +{\out No subgoals!}
   9.605 +\end{ttbox}
   9.606 +Let us consider what has happened in detail.  The reflexivity axiom is
   9.607 +lifted over~$x$ to become $\Forall x.\Var{f}(x)=\Var{f}(x)$, which is
   9.608 +unified with $\Forall x.x=\Var{y@1}(x)$.  The function unknowns $\Var{f}$
   9.609 +and~$\Var{y@1}$ are both instantiated to the identity function, and
   9.610 +$x=\Var{y@1}(x)$ collapses to~$x=x$ by $\beta$-reduction.
   9.611 +
   9.612 +\subsubsection{The unsuccessful proof}
   9.613 +We state the goal $\exists y.\forall x.x=y$, which is {\bf not} a theorem, and
   9.614 +try~$(\exists I)$:
   9.615 +\begin{ttbox}
   9.616 +goal FOL.thy "EX y. ALL x. x=y";
   9.617 +{\out Level 0}
   9.618 +{\out EX y. ALL x. x = y}
   9.619 +{\out  1. EX y. ALL x. x = y}
   9.620 +\ttbreak
   9.621 +by (resolve_tac [exI] 1);
   9.622 +{\out Level 1}
   9.623 +{\out EX y. ALL x. x = y}
   9.624 +{\out  1. ALL x. x = ?y}
   9.625 +\end{ttbox}
   9.626 +The unknown {\tt ?y} may be replaced by any term, but this can never
   9.627 +introduce another bound occurrence of~{\tt x}.  We now apply~$(\forall I)$:
   9.628 +\begin{ttbox}
   9.629 +by (resolve_tac [allI] 1);
   9.630 +{\out Level 2}
   9.631 +{\out EX y. ALL x. x = y}
   9.632 +{\out  1. !!x. x = ?y}
   9.633 +\end{ttbox}
   9.634 +Compare our position with the previous Level~2.  Instead of {\tt?y1(x)} we
   9.635 +have~{\tt?y}, whose instances may not contain the bound variable~{\tt x}.
   9.636 +The reflexivity axiom does not unify with subgoal~1.
   9.637 +\begin{ttbox}
   9.638 +by (resolve_tac [refl] 1);
   9.639 +{\out by: tactic returned no results}
   9.640 +\end{ttbox}
   9.641 +No other choice of rules seems likely to complete the proof.  Of course,
   9.642 +this is no guarantee that Isabelle cannot prove $\exists y.\forall x.x=y$
   9.643 +or other invalid assertions.  We must appeal to the soundness of
   9.644 +first-order logic and the faithfulness of its encoding in
   9.645 +Isabelle~\cite{paulson89}, and must trust the implementation.
   9.646 +
   9.647 +
   9.648 +\subsection{Nested quantifiers}
   9.649 +\index{examples!with quantifiers}
   9.650 +Multiple quantifiers create complex terms.  Proving $(\forall x\,y.P(x,y))
   9.651 +\imp (\forall z\,w.P(w,z))$, will demonstrate how parameters and
   9.652 +unknowns develop.  If they appear in the wrong order, the proof will fail.
   9.653 +This section concludes with a demonstration of {\tt REPEAT}
   9.654 +and~{\tt ORELSE}.  
   9.655 +
   9.656 +The start of the proof is routine.
   9.657 +\begin{ttbox}
   9.658 +goal FOL.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
   9.659 +{\out Level 0}
   9.660 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.661 +{\out  1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.662 +\ttbreak
   9.663 +by (resolve_tac [impI] 1);
   9.664 +{\out Level 1}
   9.665 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.666 +{\out  1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}
   9.667 +\end{ttbox}
   9.668 +
   9.669 +\subsubsection{The wrong approach}
   9.670 +Using \ttindex{dresolve_tac}, we apply the rule $(\forall E)$, bound to the
   9.671 +\ML\ identifier \ttindex{spec}.  Then we apply $(\forall I)$.
   9.672 +\begin{ttbox}
   9.673 +by (dresolve_tac [spec] 1);
   9.674 +{\out Level 2}
   9.675 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.676 +{\out  1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)}
   9.677 +\ttbreak
   9.678 +by (resolve_tac [allI] 1);
   9.679 +{\out Level 3}
   9.680 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.681 +{\out  1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)}
   9.682 +\end{ttbox}
   9.683 +The unknown {\tt ?u} and the parameter {\tt z} have appeared.  We again
   9.684 +apply $(\forall I)$ and~$(\forall E)$.
   9.685 +\begin{ttbox}
   9.686 +by (dresolve_tac [spec] 1);
   9.687 +{\out Level 4}
   9.688 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.689 +{\out  1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)}
   9.690 +\ttbreak
   9.691 +by (resolve_tac [allI] 1);
   9.692 +{\out Level 5}
   9.693 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.694 +{\out  1. !!z w. P(?x1,?y3(z)) ==> P(w,z)}
   9.695 +\end{ttbox}
   9.696 +The unknown {\tt ?y3} and the parameter {\tt w} have appeared.  Each
   9.697 +unknown is applied to the parameters existing at the time of its creation;
   9.698 +instances of {\tt ?x1} cannot contain~{\tt z} or~{\tt w}, while instances
   9.699 +of {\tt?y3(z)} can only contain~{\tt z}.  Because of these restrictions,
   9.700 +proof by assumption will fail.
   9.701 +\begin{ttbox}
   9.702 +by (assume_tac 1);
   9.703 +{\out by: tactic returned no results}
   9.704 +{\out uncaught exception ERROR}
   9.705 +\end{ttbox}
   9.706 +
   9.707 +\subsubsection{The right approach}
   9.708 +To do this proof, the rules must be applied in the correct order.
   9.709 +Eigenvariables should be created before unknowns.  The
   9.710 +\ttindex{choplev} command returns to an earlier stage of the proof;
   9.711 +let us return to the result of applying~$({\imp}I)$:
   9.712 +\begin{ttbox}
   9.713 +choplev 1;
   9.714 +{\out Level 1}
   9.715 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.716 +{\out  1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}
   9.717 +\end{ttbox}
   9.718 +Previously, we made the mistake of applying $(\forall E)$; this time, we
   9.719 +apply $(\forall I)$ twice.
   9.720 +\begin{ttbox}
   9.721 +by (resolve_tac [allI] 1);
   9.722 +{\out Level 2}
   9.723 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.724 +{\out  1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)}
   9.725 +\ttbreak
   9.726 +by (resolve_tac [allI] 1);
   9.727 +{\out Level 3}
   9.728 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.729 +{\out  1. !!z w. ALL x y. P(x,y) ==> P(w,z)}
   9.730 +\end{ttbox}
   9.731 +The parameters {\tt z} and~{\tt w} have appeared.  We now create the
   9.732 +unknowns:
   9.733 +\begin{ttbox}
   9.734 +by (dresolve_tac [spec] 1);
   9.735 +{\out Level 4}
   9.736 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.737 +{\out  1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)}
   9.738 +\ttbreak
   9.739 +by (dresolve_tac [spec] 1);
   9.740 +{\out Level 5}
   9.741 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.742 +{\out  1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)}
   9.743 +\end{ttbox}
   9.744 +Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt
   9.745 +z} and~{\tt w}:
   9.746 +\begin{ttbox}
   9.747 +by (assume_tac 1);
   9.748 +{\out Level 6}
   9.749 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.750 +{\out No subgoals!}
   9.751 +\end{ttbox}
   9.752 +
   9.753 +\subsubsection{A one-step proof using tacticals}
   9.754 +\index{tacticals}
   9.755 +\index{examples!of tacticals}
   9.756 +Repeated application of rules can be an effective theorem-proving
   9.757 +procedure, but the rules should be attempted in an order that delays the
   9.758 +creation of unknowns.  As we have just seen, \ttindex{allI} should be
   9.759 +attempted before~\ttindex{spec}, while \ttindex{assume_tac} generally can
   9.760 +be attempted first.  Such priorities can easily be expressed
   9.761 +using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}.  Let us return
   9.762 +to the original goal using \ttindex{choplev}:
   9.763 +\begin{ttbox}
   9.764 +choplev 0;
   9.765 +{\out Level 0}
   9.766 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.767 +{\out  1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.768 +\end{ttbox}
   9.769 +A repetitive procedure proves it:
   9.770 +\begin{ttbox}
   9.771 +by (REPEAT (assume_tac 1
   9.772 +     ORELSE resolve_tac [impI,allI] 1
   9.773 +     ORELSE dresolve_tac [spec] 1));
   9.774 +{\out Level 1}
   9.775 +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
   9.776 +{\out No subgoals!}
   9.777 +\end{ttbox}
   9.778 +
   9.779 +
   9.780 +\subsection{A realistic quantifier proof}
   9.781 +\index{examples!with quantifiers}
   9.782 +A proof of $(\forall x. P(x) \imp Q) \imp (\exists x. P(x)) \imp Q$
   9.783 +demonstrates the practical use of parameters and unknowns. 
   9.784 +Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we
   9.785 +use \ttindex{REPEAT}:
   9.786 +\begin{ttbox}
   9.787 +goal FOL.thy "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q";
   9.788 +{\out Level 0}
   9.789 +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
   9.790 +{\out  1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
   9.791 +\ttbreak
   9.792 +by (REPEAT (resolve_tac [impI] 1));
   9.793 +{\out Level 1}
   9.794 +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
   9.795 +{\out  1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q}
   9.796 +\end{ttbox}
   9.797 +We can eliminate the universal or the existential quantifier.  The
   9.798 +existential quantifier should be eliminated first, since this creates a
   9.799 +parameter.  The rule~$(\exists E)$ is bound to the
   9.800 +identifier~\ttindex{exE}.
   9.801 +\begin{ttbox}
   9.802 +by (eresolve_tac [exE] 1);
   9.803 +{\out Level 2}
   9.804 +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
   9.805 +{\out  1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q}
   9.806 +\end{ttbox}
   9.807 +The only possibility now is $(\forall E)$, a destruction rule.  We use 
   9.808 +\ttindex{dresolve_tac}, which discards the quantified assumption; it is
   9.809 +only needed once.
   9.810 +\begin{ttbox}
   9.811 +by (dresolve_tac [spec] 1);
   9.812 +{\out Level 3}
   9.813 +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
   9.814 +{\out  1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q}
   9.815 +\end{ttbox}
   9.816 +Because the parameter~{\tt x} appeared first, the unknown
   9.817 +term~{\tt?x3(x)} may depend upon it.  Had we eliminated the universal
   9.818 +quantifier before the existential, this would not be so.
   9.819 +
   9.820 +Although $({\imp}E)$ is a destruction rule, it works with 
   9.821 +\ttindex{eresolve_tac} to perform backward chaining.  This technique is
   9.822 +frequently useful.  
   9.823 +\begin{ttbox}
   9.824 +by (eresolve_tac [mp] 1);
   9.825 +{\out Level 4}
   9.826 +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
   9.827 +{\out  1. !!x. P(x) ==> P(?x3(x))}
   9.828 +\end{ttbox}
   9.829 +The tactic has reduced~{\tt Q} to~{\tt P(?x3(x))}, deleting the
   9.830 +implication.  The final step is trivial, thanks to the occurrence of~{\tt x}.
   9.831 +\begin{ttbox}
   9.832 +by (assume_tac 1);
   9.833 +{\out Level 5}
   9.834 +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
   9.835 +{\out No subgoals!}
   9.836 +\end{ttbox}
   9.837 +
   9.838 +
   9.839 +\subsection{The classical reasoning package}
   9.840 +\index{classical reasoning package}
   9.841 +Although Isabelle cannot compete with fully automatic theorem provers, it
   9.842 +provides enough automation to tackle substantial examples.  The classical
   9.843 +reasoning package can be set up for any classical natural deduction logic
   9.844 +--- see the {\em Reference Manual}.
   9.845 +
   9.846 +Rules are packaged into bundles called \bfindex{classical sets}.  The package
   9.847 +provides several tactics, which apply rules using naive algorithms, using
   9.848 +unification to handle quantifiers.  The most useful tactic
   9.849 +is~\ttindex{fast_tac}.  
   9.850 +
   9.851 +Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}.  (The
   9.852 +backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape
   9.853 +sequence, to break the long string over two lines.)
   9.854 +\begin{ttbox}
   9.855 +goal FOL.thy "(EX y. ALL x. J(y,x) <-> ~J(x,x))  \ttback
   9.856 +\ttback       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
   9.857 +{\out Level 0}
   9.858 +{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
   9.859 +{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
   9.860 +{\out  1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
   9.861 +{\out     ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
   9.862 +\end{ttbox}
   9.863 +The rules of classical logic are bundled as {\tt FOL_cs}.  We may solve
   9.864 +subgoal~1 at a stroke, using~\ttindex{fast_tac}.
   9.865 +\begin{ttbox}
   9.866 +by (fast_tac FOL_cs 1);
   9.867 +{\out Level 1}
   9.868 +{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
   9.869 +{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
   9.870 +{\out No subgoals!}
   9.871 +\end{ttbox}
   9.872 +Sceptics may examine the proof by calling the package's single-step
   9.873 +tactics, such as~{\tt step_tac}.  This would take up much space, however,
   9.874 +so let us proceed to the next example:
   9.875 +\begin{ttbox}
   9.876 +goal FOL.thy "ALL x. P(x,f(x)) <-> \ttback
   9.877 +\ttback       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
   9.878 +{\out Level 0}
   9.879 +{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
   9.880 +{\out  1. ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
   9.881 +\end{ttbox}
   9.882 +Again, subgoal~1 succumbs immediately.
   9.883 +\begin{ttbox}
   9.884 +by (fast_tac FOL_cs 1);
   9.885 +{\out Level 1}
   9.886 +{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
   9.887 +{\out No subgoals!}
   9.888 +\end{ttbox}
   9.889 +The classical reasoning package is not restricted to the usual logical
   9.890 +connectives.  The natural deduction rules for unions and intersections in
   9.891 +set theory resemble those for disjunction and conjunction, and in the
   9.892 +infinitary case, for quantifiers.  The package is valuable for reasoning in
   9.893 +set theory.
   9.894 +
   9.895 +
   9.896 +% Local Variables: 
   9.897 +% mode: latex
   9.898 +% TeX-master: t
   9.899 +% End: 
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/doc-src/Intro/intro.bbl	Wed Nov 10 05:06:55 1993 +0100
    10.3 @@ -0,0 +1,108 @@
    10.4 +\begin{thebibliography}{10}
    10.5 +
    10.6 +\bibitem{galton90}
    10.7 +Antony Galton.
    10.8 +\newblock {\em Logic for Information Technology}.
    10.9 +\newblock Wiley, 1990.
   10.10 +
   10.11 +\bibitem{gordon88a}
   10.12 +Michael J.~C. Gordon.
   10.13 +\newblock {HOL}: A proof generating system for higher-order logic.
   10.14 +\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em {VLSI}
   10.15 +  Specification, Verification and Synthesis}, pages 73--128. Kluwer Academic
   10.16 +  Publishers, 1988.
   10.17 +
   10.18 +\bibitem{gordon79}
   10.19 +Michael J.~C. Gordon, Robin Milner, and Christopher~P. Wadsworth.
   10.20 +\newblock {\em Edinburgh {LCF}: A Mechanised Logic of Computation}.
   10.21 +\newblock Springer LNCS 78, 1979.
   10.22 +
   10.23 +\bibitem{haskell-tutorial}
   10.24 +Paul Hudak and Joseph~H. Fasel.
   10.25 +\newblock A gentle introduction to {Haskell}.
   10.26 +\newblock {\em {ACM} {SIGPLAN} Notices}, 27(5), May 1992.
   10.27 +
   10.28 +\bibitem{haskell-report}
   10.29 +Paul Hudak, Simon~Peyton Jones, and Philip Wadler.
   10.30 +\newblock Report on the programming language {Haskell}: A non-strict, purely
   10.31 +  functional language.
   10.32 +\newblock {\em {ACM} {SIGPLAN} Notices}, 27(5), May 1992.
   10.33 +\newblock Version 1.2.
   10.34 +
   10.35 +\bibitem{huet75}
   10.36 +G.~P. Huet.
   10.37 +\newblock A unification algorithm for typed $\lambda$-calculus.
   10.38 +\newblock {\em Theoretical Computer Science}, 1:27--57, 1975.
   10.39 +
   10.40 +\bibitem{miller-jsc}
   10.41 +Dale Miller.
   10.42 +\newblock Unification under a mixed prefix.
   10.43 +\newblock {\em Journal of Symbolic Computation}, 14(4):321--358, 1992.
   10.44 +
   10.45 +\bibitem{nipkow-prehofer}
   10.46 +Tobias Nipkow and Christian Prehofer.
   10.47 +\newblock Type checking type classes.
   10.48 +\newblock In {\em 20th ACM Symp.\ Principles of Programming Languages}, 1993.
   10.49 +\newblock To appear.
   10.50 +
   10.51 +\bibitem{nordstrom90}
   10.52 +Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
   10.53 +\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
   10.54 +\newblock Oxford, 1990.
   10.55 +
   10.56 +\bibitem{paulson86}
   10.57 +Lawrence~C. Paulson.
   10.58 +\newblock Natural deduction as higher-order resolution.
   10.59 +\newblock {\em Journal of Logic Programming}, 3:237--258, 1986.
   10.60 +
   10.61 +\bibitem{paulson87}
   10.62 +Lawrence~C. Paulson.
   10.63 +\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
   10.64 +\newblock Cambridge University Press, 1987.
   10.65 +
   10.66 +\bibitem{paulson89}
   10.67 +Lawrence~C. Paulson.
   10.68 +\newblock The foundation of a generic theorem prover.
   10.69 +\newblock {\em Journal of Automated Reasoning}, 5:363--397, 1989.
   10.70 +
   10.71 +\bibitem{paulson700}
   10.72 +Lawrence~C. Paulson.
   10.73 +\newblock {Isabelle}: The next 700 theorem provers.
   10.74 +\newblock In P.~Odifreddi, editor, {\em Logic and Computer Science}, pages
   10.75 +  361--386. Academic Press, 1990.
   10.76 +
   10.77 +\bibitem{paulson91}
   10.78 +Lawrence~C. Paulson.
   10.79 +\newblock {\em {ML} for the Working Programmer}.
   10.80 +\newblock Cambridge University Press, 1991.
   10.81 +
   10.82 +\bibitem{paulson-handbook}
   10.83 +Lawrence~C. Paulson.
   10.84 +\newblock Designing a theorem prover.
   10.85 +\newblock In S.~Abramsky, D.~M. Gabbay, and T.~S.~E. Maibaum, editors, {\em
   10.86 +  Handbook of Logic in Computer Science}, volume~2, pages 415--475. Oxford
   10.87 +  University Press, 1992.
   10.88 +
   10.89 +\bibitem{pelletier86}
   10.90 +F.~J. Pelletier.
   10.91 +\newblock Seventy-five problems for testing automatic theorem provers.
   10.92 +\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
   10.93 +\newblock Errata, JAR 4 (1988), 235--236.
   10.94 +
   10.95 +\bibitem{reeves90}
   10.96 +Steve Reeves and Michael Clarke.
   10.97 +\newblock {\em Logic for Computer Science}.
   10.98 +\newblock Addison-Wesley, 1990.
   10.99 +
  10.100 +\bibitem{suppes72}
  10.101 +Patrick Suppes.
  10.102 +\newblock {\em Axiomatic Set Theory}.
  10.103 +\newblock Dover, 1972.
  10.104 +
  10.105 +\bibitem{wos-bledsoe}
  10.106 +Larry Wos.
  10.107 +\newblock Automated reasoning and {Bledsoe's} dream for the field.
  10.108 +\newblock In Robert~S. Boyer, editor, {\em Automated Reasoning: Essays in Honor
  10.109 +  of {Woody Bledsoe}}, pages 297--342. Kluwer Academic Publishers, 1991.
  10.110 +
  10.111 +\end{thebibliography}
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/doc-src/Intro/intro.ind	Wed Nov 10 05:06:55 1993 +0100
    11.3 @@ -0,0 +1,251 @@
    11.4 +\begin{theindex}
    11.5 +
    11.6 +  \item $\Forall$, \bold{5}, 7
    11.7 +  \item $\Imp$, \bold{5}
    11.8 +  \item $\To$, \bold{1}, \bold{3}
    11.9 +  \item $\equiv$, \bold{5}
   11.10 +
   11.11 +  \indexspace
   11.12 +
   11.13 +  \item {\tt allI}, 35
   11.14 +  \item arities
   11.15 +    \subitem declaring, 3, \bold{46}
   11.16 +  \item {\tt asm_simp_tac}, 55
   11.17 +  \item associativity of addition, 54
   11.18 +  \item {\tt assume_tac}, \bold{27}, 29, 30, 35, 43, 44
   11.19 +  \item assumptions, 6
   11.20 +
   11.21 +  \indexspace
   11.22 +
   11.23 +  \item {\tt ba}, \bold{28}
   11.24 +  \item {\tt back}, 54, 57
   11.25 +  \item backtracking, 57
   11.26 +  \item {\tt bd}, \bold{28}
   11.27 +  \item {\tt be}, \bold{28}
   11.28 +  \item {\tt br}, \bold{28}
   11.29 +  \item {\tt by}, \bold{28}
   11.30 +
   11.31 +  \indexspace
   11.32 +
   11.33 +  \item {\tt choplev}, 34, 35, 59
   11.34 +  \item classes, \bold{3}
   11.35 +    \subitem built-in, \bold{23}
   11.36 +  \item classical reasoning package, 36
   11.37 +  \item classical sets, \bold{36}
   11.38 +  \item {\tt conjunct1}, 25
   11.39 +  \item constants
   11.40 +    \subitem declaring, \bold{45}
   11.41 +
   11.42 +  \indexspace
   11.43 +
   11.44 +  \item definitions, \bold{5}
   11.45 +    \subitem reasoning about, \bold{40}
   11.46 +  \item {\tt DEPTH_FIRST}, 59
   11.47 +  \item destruct-resolution, \bold{20}
   11.48 +  \item destruction rules, \bold{20}
   11.49 +  \item {\tt disjE}, 29
   11.50 +  \item {\tt dres_inst_tac}, \bold{52}
   11.51 +  \item {\tt dresolve_tac}, \bold{28}, 30, 33, 36
   11.52 +
   11.53 +  \indexspace
   11.54 +
   11.55 +  \item eigenvariables, \see{parameters}{7}
   11.56 +  \item elim-resolution, \bold{18}
   11.57 +  \item equality
   11.58 +    \subitem meta-level, \bold{5}
   11.59 +  \item {\tt eres_inst_tac}, \bold{52}
   11.60 +  \item {\tt eresolve_tac}, \bold{27}, 30, 36, 43, 44
   11.61 +  \item examples
   11.62 +    \subitem of deriving rules, 38
   11.63 +    \subitem of induction, 52, 53
   11.64 +    \subitem of rewriting, 54
   11.65 +    \subitem of tacticals, 35
   11.66 +    \subitem of theories, 45--51, 56
   11.67 +    \subitem propositional, 16, 28, 30
   11.68 +    \subitem with quantifiers, 17, 31, 33, 35
   11.69 +  \item {\tt exE}, 35
   11.70 +
   11.71 +  \indexspace
   11.72 +
   11.73 +  \item {\tt FalseE}, 42
   11.74 +  \item {\tt fast_tac}, 36, 37
   11.75 +  \item flex-flex equations, \bold{5}, 23, \bold{26}
   11.76 +  \item {\tt flexflex_rule}, 26
   11.77 +  \item {\tt FOL}, 56
   11.78 +  \item {\tt FOL.thy}, 28
   11.79 +  \item folding, \bold{40}
   11.80 +
   11.81 +  \indexspace
   11.82 +
   11.83 +  \item {\tt goal}, \bold{28}, 38, 39, 41--43
   11.84 +  \item {\tt goalw}, 42, 43
   11.85 +
   11.86 +  \indexspace
   11.87 +
   11.88 +  \item {\tt has_fewer_prems}, 59
   11.89 +
   11.90 +  \indexspace
   11.91 +
   11.92 +  \item identifiers, \bold{22}
   11.93 +  \item imitation, \bold{10}
   11.94 +  \item {\tt impI}, 29, 41
   11.95 +  \item implication
   11.96 +    \subitem meta-level, \bold{5}
   11.97 +  \item infix operators, \bold{47}
   11.98 +  \item instantiation
   11.99 +    \subitem explicit, \bold{52}
  11.100 +  \item Isabelle
  11.101 +    \subitem definitions in, 40
  11.102 +    \subitem formalizing rules, \bold{5}
  11.103 +    \subitem formalizing syntax, \bold{1}
  11.104 +    \subitem getting started, 22
  11.105 +    \subitem object-logics supported, i
  11.106 +    \subitem overview, i
  11.107 +    \subitem proof construction in, \bold{9}
  11.108 +    \subitem release history, i
  11.109 +    \subitem syntax of, 23
  11.110 +
  11.111 +  \indexspace
  11.112 +
  11.113 +  \item LCF, i, 14, 24
  11.114 +  \item level, \bold{29}
  11.115 +  \item lifting, \bold{13}
  11.116 +    \subitem over assumptions, \bold{13}
  11.117 +    \subitem over parameters, \bold{13}
  11.118 +  \item {\tt logic}, 23
  11.119 +
  11.120 +  \indexspace
  11.121 +
  11.122 +  \item main goal, \bold{14}
  11.123 +  \item major premise, \bold{19}
  11.124 +  \item {\tt Match}, 39
  11.125 +  \item meta-formulae
  11.126 +    \subitem syntax, \bold{23}
  11.127 +  \item meta-logic, \bold{5}
  11.128 +  \item mixfix operators, \bold{47}
  11.129 +  \item ML, i, 22, 25
  11.130 +  \item {\tt mp}, 25
  11.131 +
  11.132 +  \indexspace
  11.133 +
  11.134 +  \item {\tt Nat}, \bold{51}
  11.135 +  \item {\tt Nat.thy}, 53
  11.136 +  \item {\tt not_def}, 41
  11.137 +  \item {\tt notE}, \bold{43}, 53
  11.138 +  \item {\tt notI}, \bold{41}, 53
  11.139 +
  11.140 +  \indexspace
  11.141 +
  11.142 +  \item {\tt ORELSE}, 35
  11.143 +  \item overloading, \bold{4}, 48
  11.144 +
  11.145 +  \indexspace
  11.146 +
  11.147 +  \item parameters, \bold{7}, 31
  11.148 +  \item printing commands, \bold{25}
  11.149 +  \item projection, \bold{10}
  11.150 +  \item {\tt Prolog}, 56
  11.151 +  \item Prolog interpreter, \bold{55}
  11.152 +  \item proof
  11.153 +    \subitem backward, \bold{14}
  11.154 +    \subitem by assumption, \bold{15}
  11.155 +    \subitem by induction, 52
  11.156 +    \subitem commands for, \bold{28}
  11.157 +    \subitem forward, 20
  11.158 +  \item proof state, \bold{14}
  11.159 +  \item {\tt PROP}, 24
  11.160 +  \item {\tt prop}, 23, 24
  11.161 +  \item {\tt prth}, \bold{25}
  11.162 +  \item {\tt prthq}, \bold{25}, 26
  11.163 +  \item {\tt prths}, \bold{25}
  11.164 +  \item {\tt Pure}, \bold{44}
  11.165 +
  11.166 +  \indexspace
  11.167 +
  11.168 +  \item quantifiers
  11.169 +    \subitem meta-level, \bold{5}
  11.170 +    \subitem reasoning about, 31
  11.171 +
  11.172 +  \indexspace
  11.173 +
  11.174 +  \item {\tt read_instantiate}, 27
  11.175 +  \item refinement, \bold{15}
  11.176 +    \subitem with instantiation, \bold{52}
  11.177 +  \item {\tt refl}, 27
  11.178 +  \item {\tt REPEAT}, 30, 35, 57, 59
  11.179 +  \item {\tt res_inst_tac}, \bold{52}, 54, 55
  11.180 +  \item reserved words, \bold{22}
  11.181 +  \item resolution, \bold{11}
  11.182 +    \subitem in backward proof, 14
  11.183 +  \item {\tt resolve_tac}, \bold{27}, 29, 43, 53
  11.184 +  \item {\tt result}, \bold{28}, 29, 38, 39, 44
  11.185 +  \item {\tt rewrite_goals_tac}, 41, 42
  11.186 +  \item {\tt rewrite_rule}, 42, 43
  11.187 +  \item rewriting
  11.188 +    \subitem meta-level, 40, \bold{40}
  11.189 +    \subitem object-level, 54
  11.190 +  \item {\tt RL}, 27
  11.191 +  \item {\tt RLN}, 27
  11.192 +  \item {\tt RS}, \bold{25}, 27, 43
  11.193 +  \item {\tt RSN}, \bold{25}, 27
  11.194 +  \item rules
  11.195 +    \subitem declaring, \bold{45}
  11.196 +    \subitem derived, 12, \bold{20}, 38, 40
  11.197 +    \subitem propositional, \bold{6}
  11.198 +    \subitem quantifier, \bold{7}
  11.199 +
  11.200 +  \indexspace
  11.201 +
  11.202 +  \item search
  11.203 +    \subitem depth-first, 58
  11.204 +  \item signatures, \bold{8}
  11.205 +  \item {\tt simp_tac}, 55
  11.206 +  \item simplification set, \bold{54}
  11.207 +  \item sorts, \bold{4}
  11.208 +  \item {\tt spec}, 26, 33, 35
  11.209 +  \item {\tt standard}, \bold{25}
  11.210 +  \item subgoals, \bold{14}
  11.211 +  \item substitution, \bold{7}
  11.212 +  \item {\tt Suc_inject}, 53
  11.213 +  \item {\tt Suc_neq_0}, 53
  11.214 +
  11.215 +  \indexspace
  11.216 +
  11.217 +  \item tacticals, \bold{14}, \bold{17}, 35
  11.218 +  \item Tactics, \bold{14}
  11.219 +  \item tactics, \bold{17}
  11.220 +    \subitem basic, \bold{27}
  11.221 +  \item terms
  11.222 +    \subitem syntax, \bold{23}
  11.223 +  \item theorems
  11.224 +    \subitem basic operations on, \bold{24}
  11.225 +  \item theories, \bold{8}
  11.226 +    \subitem defining, 44--52
  11.227 +  \item {\tt thm}, 24
  11.228 +  \item {\tt topthm}, 39
  11.229 +  \item {$Trueprop$}, 6, 7, 9, 23
  11.230 +  \item type constructors
  11.231 +    \subitem declaring, \bold{46}
  11.232 +  \item types, 1
  11.233 +    \subitem higher, \bold{4}
  11.234 +    \subitem polymorphic, \bold{3}
  11.235 +    \subitem simple, \bold{1}
  11.236 +    \subitem syntax, \bold{23}
  11.237 +
  11.238 +  \indexspace
  11.239 +
  11.240 +  \item {\tt undo}, \bold{28}
  11.241 +  \item unfolding, \bold{40}
  11.242 +  \item unification
  11.243 +    \subitem higher-order, \bold{10}, 53
  11.244 +  \item unknowns, \bold{9}, 31
  11.245 +    \subitem of function type, \bold{11}, 26
  11.246 +  \item {\tt use_thy}, \bold{44, 45}
  11.247 +
  11.248 +  \indexspace
  11.249 +
  11.250 +  \item variables
  11.251 +    \subitem bound, 7
  11.252 +    \subitem schematic, \see{unknowns}{9}
  11.253 +
  11.254 +\end{theindex}
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/doc-src/Intro/intro.tex	Wed Nov 10 05:06:55 1993 +0100
    12.3 @@ -0,0 +1,149 @@
    12.4 +\documentstyle[a4,12pt,proof,iman,alltt]{article}
    12.5 +%% $Id$
    12.6 +%% run    bibtex intro         to prepare bibliography
    12.7 +%% run    ../sedindex intro    to prepare index file
    12.8 +%prth *(\(.*\));          \1;      
    12.9 +%{\\out \(.*\)}          {\\out val it = "\1" : thm}
   12.10 +
   12.11 +\title{Introduction to Isabelle}   
   12.12 +\author{{\em Lawrence C. Paulson}\\
   12.13 +        Computer Laboratory \\ University of Cambridge \\[2ex]
   12.14 +        {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}}
   12.15 +}
   12.16 +\date{} 
   12.17 +\makeindex
   12.18 +
   12.19 +\underscoreoff
   12.20 +
   12.21 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
   12.22 +
   12.23 +\sloppy
   12.24 +\binperiod     %%%treat . like a binary operator
   12.25 +
   12.26 +\newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
   12.27 +\newcommand{\nand}{\mathbin{\lnot\&}} 
   12.28 +\newcommand{\xor}{\mathbin{\#}}
   12.29 +
   12.30 +\pagenumbering{roman} 
   12.31 +\begin{document}
   12.32 +\pagestyle{empty}
   12.33 +\begin{titlepage}
   12.34 +\maketitle 
   12.35 +\thispagestyle{empty}
   12.36 +\vfill
   12.37 +{\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
   12.38 +\end{titlepage}
   12.39 +
   12.40 +\pagestyle{headings}
   12.41 +\part*{Preface}
   12.42 +\index{Isabelle!overview}
   12.43 +\index{Isabelle!object-logics supported}
   12.44 +Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover.
   12.45 +It has been instantiated to support reasoning in several object-logics:
   12.46 +\begin{itemize}
   12.47 +\item first-order logic, constructive and classical versions
   12.48 +\item higher-order logic, similar to that of Gordon's {\sc
   12.49 +hol}~\cite{gordon88a}
   12.50 +\item Zermelo-Fraenkel set theory~\cite{suppes72}
   12.51 +\item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
   12.52 +\item the classical first-order sequent calculus, {\sc lk}
   12.53 +\item the modal logics $T$, $S4$, and $S43$
   12.54 +\item the Logic for Computable Functions~\cite{paulson87}
   12.55 +\end{itemize}
   12.56 +A logic's syntax and inference rules are specified declaratively; this
   12.57 +allows single-step proof construction.  Isabelle provides control
   12.58 +structures for expressing search procedures.  Isabelle also provides
   12.59 +several generic tools, such as simplifiers and classical theorem provers,
   12.60 +which can be applied to object-logics.
   12.61 +
   12.62 +\index{ML}
   12.63 +Isabelle is a large system, but beginners can get by with a small
   12.64 +repertoire of commands and a basic knowledge of how Isabelle works.  Some
   12.65 +knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user
   12.66 +interface.  Advanced Isabelle theorem proving can involve writing \ML{}
   12.67 +code, possibly with Isabelle's sources at hand.  My book
   12.68 +on~\ML{}~\cite{paulson91} covers much material connected with Isabelle,
   12.69 +including a simple theorem prover.  Users must be familiar with logic as
   12.70 +used in computer science; there are many good
   12.71 +texts~\cite{galton90,reeves90}.
   12.72 +
   12.73 +\index{LCF}
   12.74 +{\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an
   12.75 +ancestor of {\sc hol}, Nuprl, and several other systems.  Isabelle borrows
   12.76 +ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
   12.77 +abstract type; tactics and tacticals support backward proof.  But {\sc lcf}
   12.78 +represents object-level rules by functions, while Isabelle represents them
   12.79 +by terms.  You may find my other writings~\cite{paulson87,paulson-handbook}
   12.80 +helpful in understanding the relationship between {\sc lcf} and Isabelle.
   12.81 +
   12.82 +Isabelle does not keep a record of inference steps.  Each step is checked
   12.83 +at run time to ensure that theorems can only be constructed by applying
   12.84 +inference rules.  An Isabelle proof typically involves hundreds of
   12.85 +primitive inferences, and would be unintelligible if displayed.
   12.86 +Discarding proofs saves vast amounts of storage.  But can Isabelle be
   12.87 +trusted?  If desired, object-logics can be formalized such that each
   12.88 +theorem carries a proof term, which could be checked by another program.
   12.89 +Proofs can also be traced.
   12.90 +
   12.91 +\index{Isabelle!release history} Isabelle was first distributed in 1986.
   12.92 +The 1987 version introduced a higher-order meta-logic with an improved
   12.93 +treatment of quantifiers.  The 1988 version added limited polymorphism and
   12.94 +support for natural deduction.  The 1989 version included a parser and
   12.95 +pretty printer generator.  The 1992 version introduced type classes, to
   12.96 +support many-sorted and higher-order logics.  The current version provides
   12.97 +greater support for theories and is much faster.  Isabelle is still under
   12.98 +development and will continue to change.
   12.99 +
  12.100 +\subsubsection*{Overview} 
  12.101 +This manual consists of three parts.  
  12.102 +Part~I discusses the Isabelle's foundations.
  12.103 +Part~II, presents simple on-line sessions, starting with forward proof.
  12.104 +It also covers basic tactics and tacticals, and some commands for invoking
  12.105 +Part~III contains further examples for users with a bit of experience.
  12.106 +It explains how to derive rules define theories, and concludes with an
  12.107 +extended example: a Prolog interpreter.
  12.108 +
  12.109 +Isabelle's Reference Manual and Object-Logics manual contain more details.
  12.110 +They assume familiarity with the concepts presented here.
  12.111 +
  12.112 +
  12.113 +\subsubsection*{Acknowledgements} 
  12.114 +Tobias Nipkow contributed most of the section on ``Defining Theories''.
  12.115 +Sara Kalvala and Markus Wenzel suggested improvements.
  12.116 +
  12.117 +Tobias Nipkow has made immense contributions to Isabelle, including the
  12.118 +parser generator, type classes, and the simplifier.  Carsten Clasohm, Sonia
  12.119 +Mahjoub, Karin Nimmermann and Markus Wenzel also made improvements.
  12.120 +Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler,
  12.121 +Poly/{\sc ml}.  Many people have contributed to Isabelle's standard
  12.122 +object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el.
  12.123 +The research has been funded by the SERC (grants GR/G53279, GR/H40570) and
  12.124 +by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types).
  12.125 +
  12.126 +\newpage
  12.127 +\pagestyle{plain} \tableofcontents 
  12.128 +\newpage
  12.129 +
  12.130 +\newfont{\sanssi}{cmssi12}
  12.131 +\vspace*{2.5cm}
  12.132 +\begin{quote}
  12.133 +\raggedleft
  12.134 +{\sanssi
  12.135 +You can only find truth with logic\\
  12.136 +if you have already found truth without it.}\\
  12.137 +\bigskip
  12.138 +
  12.139 +G.K. Chesterton, {\em The Man who was Orthodox}
  12.140 +\end{quote}
  12.141 +
  12.142 +\clearfirst  \pagestyle{headings}
  12.143 +\include{foundations}
  12.144 +\include{getting}
  12.145 +\include{advanced}
  12.146 +
  12.147 +
  12.148 +\bibliographystyle{plain} \small\raggedright\frenchspacing
  12.149 +\bibliography{atp,funprog,general,logicprog,theory}
  12.150 +
  12.151 +\input{intro.ind}
  12.152 +\end{document}
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/doc-src/Intro/intro.toc	Wed Nov 10 05:06:55 1993 +0100
    13.3 @@ -0,0 +1,67 @@
    13.4 +\contentsline {part}{\uppercase {i}\phspace {1em}Foundations}{1}
    13.5 +\contentsline {section}{\numberline {1}Formalizing logical syntax in Isabelle}{1}
    13.6 +\contentsline {subsection}{\numberline {1.1}Simple types and constants}{1}
    13.7 +\contentsline {subsection}{\numberline {1.2}Polymorphic types and constants}{3}
    13.8 +\contentsline {subsection}{\numberline {1.3}Higher types and quantifiers}{4}
    13.9 +\contentsline {section}{\numberline {2}Formalizing logical rules in Isabelle}{5}
   13.10 +\contentsline {subsection}{\numberline {2.1}Expressing propositional rules}{6}
   13.11 +\contentsline {subsection}{\numberline {2.2}Quantifier rules and substitution}{7}
   13.12 +\contentsline {subsection}{\numberline {2.3}Signatures and theories}{8}
   13.13 +\contentsline {section}{\numberline {3}Proof construction in Isabelle}{9}
   13.14 +\contentsline {subsection}{\numberline {3.1}Higher-order unification}{10}
   13.15 +\contentsline {subsection}{\numberline {3.2}Joining rules by resolution}{11}
   13.16 +\contentsline {subsection}{\numberline {3.3}Lifting a rule into a context}{13}
   13.17 +\contentsline {subsubsection}{Lifting over assumptions}{13}
   13.18 +\contentsline {subsubsection}{Lifting over parameters}{13}
   13.19 +\contentsline {section}{\numberline {4}Backward proof by resolution}{14}
   13.20 +\contentsline {subsection}{\numberline {4.1}Refinement by resolution}{15}
   13.21 +\contentsline {subsection}{\numberline {4.2}Proof by assumption}{15}
   13.22 +\contentsline {subsection}{\numberline {4.3}A propositional proof}{16}
   13.23 +\contentsline {subsection}{\numberline {4.4}A quantifier proof}{17}
   13.24 +\contentsline {subsection}{\numberline {4.5}Tactics and tacticals}{17}
   13.25 +\contentsline {section}{\numberline {5}Variations on resolution}{18}
   13.26 +\contentsline {subsection}{\numberline {5.1}Elim-resolution}{18}
   13.27 +\contentsline {subsection}{\numberline {5.2}Destruction rules}{20}
   13.28 +\contentsline {subsection}{\numberline {5.3}Deriving rules by resolution}{20}
   13.29 +\contentsline {part}{\uppercase {ii}\phspace {1em}Getting started with Isabelle}{22}
   13.30 +\contentsline {section}{\numberline {6}Forward proof}{22}
   13.31 +\contentsline {subsection}{\numberline {6.1}Lexical matters}{22}
   13.32 +\contentsline {subsection}{\numberline {6.2}Syntax of types and terms}{23}
   13.33 +\contentsline {subsection}{\numberline {6.3}Basic operations on theorems}{24}
   13.34 +\contentsline {subsection}{\numberline {6.4}Flex-flex equations}{26}
   13.35 +\contentsline {section}{\numberline {7}Backward proof}{27}
   13.36 +\contentsline {subsection}{\numberline {7.1}The basic tactics}{27}
   13.37 +\contentsline {subsection}{\numberline {7.2}Commands for backward proof}{28}
   13.38 +\contentsline {subsection}{\numberline {7.3}A trivial example in propositional logic}{28}
   13.39 +\contentsline {subsection}{\numberline {7.4}Proving a distributive law}{30}
   13.40 +\contentsline {section}{\numberline {8}Quantifier reasoning}{31}
   13.41 +\contentsline {subsection}{\numberline {8.1}Two quantifier proofs, successful and not}{31}
   13.42 +\contentsline {subsubsection}{The successful proof}{31}
   13.43 +\contentsline {subsubsection}{The unsuccessful proof}{32}
   13.44 +\contentsline {subsection}{\numberline {8.2}Nested quantifiers}{33}
   13.45 +\contentsline {subsubsection}{The wrong approach}{33}
   13.46 +\contentsline {subsubsection}{The right approach}{34}
   13.47 +\contentsline {subsubsection}{A one-step proof using tacticals}{35}
   13.48 +\contentsline {subsection}{\numberline {8.3}A realistic quantifier proof}{35}
   13.49 +\contentsline {subsection}{\numberline {8.4}The classical reasoning package}{36}
   13.50 +\contentsline {part}{\uppercase {iii}\phspace {1em}Advanced methods}{38}
   13.51 +\contentsline {section}{\numberline {9}Deriving rules in Isabelle}{38}
   13.52 +\contentsline {subsection}{\numberline {9.1}Deriving a rule using tactics}{38}
   13.53 +\contentsline {subsection}{\numberline {9.2}Definitions and derived rules}{40}
   13.54 +\contentsline {subsubsection}{Deriving the introduction rule}{41}
   13.55 +\contentsline {subsubsection}{Deriving the elimination rule}{42}
   13.56 +\contentsline {section}{\numberline {10}Defining theories}{44}
   13.57 +\contentsline {subsection}{\numberline {10.1}Declaring constants and rules}{45}
   13.58 +\contentsline {subsection}{\numberline {10.2}Declaring type constructors}{46}
   13.59 +\contentsline {subsection}{\numberline {10.3}Infixes and Mixfixes}{47}
   13.60 +\contentsline {subsection}{\numberline {10.4}Overloading}{48}
   13.61 +\contentsline {subsection}{\numberline {10.5}Extending first-order logic with the natural numbers}{50}
   13.62 +\contentsline {subsection}{\numberline {10.6}Declaring the theory to Isabelle}{51}
   13.63 +\contentsline {section}{\numberline {11}Refinement with explicit instantiation}{52}
   13.64 +\contentsline {subsection}{\numberline {11.1}A simple proof by induction}{52}
   13.65 +\contentsline {subsection}{\numberline {11.2}An example of ambiguity in {\ptt resolve_tac}}{53}
   13.66 +\contentsline {subsection}{\numberline {11.3}Proving that addition is associative}{54}
   13.67 +\contentsline {section}{\numberline {12}A {\psc Prolog} interpreter}{55}
   13.68 +\contentsline {subsection}{\numberline {12.1}Simple executions}{56}
   13.69 +\contentsline {subsection}{\numberline {12.2}Backtracking}{57}
   13.70 +\contentsline {subsection}{\numberline {12.3}Depth-first search}{58}
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/doc-src/Intro/list.thy	Wed Nov 10 05:06:55 1993 +0100
    14.3 @@ -0,0 +1,6 @@
    14.4 +List = FOL +
    14.5 +types 	list 1
    14.6 +arities list	:: (term)term
    14.7 +consts	Nil	:: "'a list"
    14.8 +   	Cons	:: "['a, 'a list] => 'a list" 
    14.9 +end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/doc-src/Intro/prod.thy	Wed Nov 10 05:06:55 1993 +0100
    15.3 @@ -0,0 +1,9 @@
    15.4 +Prod = FOL +
    15.5 +types   "*" 2                                 (infixl 20)
    15.6 +arities "*"     :: (term,term)term
    15.7 +consts  fst     :: "'a * 'b => 'a"
    15.8 +        snd     :: "'a * 'b => 'b"
    15.9 +        Pair    :: "['a,'b] => 'a * 'b"       ("(1<_,/_>)")
   15.10 +rules   fst     "fst(<a,b>) = a"
   15.11 +        snd     "snd(<a,b>) = b"
   15.12 +end
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/doc-src/Intro/quant.txt	Wed Nov 10 05:06:55 1993 +0100
    16.3 @@ -0,0 +1,244 @@
    16.4 +(**** quantifier examples -- process using Doc/tout quant.txt  ****)
    16.5 +
    16.6 +Pretty.setmargin 72;  (*existing macros just allow this margin*)
    16.7 +print_depth 0;
    16.8 +
    16.9 +
   16.10 +goal Int_Rule.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
   16.11 +by (resolve_tac [impI] 1);
   16.12 +by (dresolve_tac [spec] 1);
   16.13 +by (resolve_tac [allI] 1);
   16.14 +by (dresolve_tac [spec] 1);
   16.15 +by (resolve_tac [allI] 1);
   16.16 +by (assume_tac 1);
   16.17 +choplev 1;
   16.18 +by (resolve_tac [allI] 1);
   16.19 +by (resolve_tac [allI] 1);
   16.20 +by (dresolve_tac [spec] 1);
   16.21 +by (dresolve_tac [spec] 1);
   16.22 +by (assume_tac 1);
   16.23 +
   16.24 +choplev 0;
   16.25 +by (REPEAT (assume_tac 1
   16.26 +     ORELSE resolve_tac [impI,allI] 1
   16.27 +     ORELSE dresolve_tac [spec] 1));
   16.28 +
   16.29 +
   16.30 +- goal Int_Rule.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
   16.31 +Level 0
   16.32 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.33 + 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.34 +val it = [] : thm list
   16.35 +- by (resolve_tac [impI] 1);
   16.36 +Level 1
   16.37 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.38 + 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)
   16.39 +val it = () : unit
   16.40 +- by (dresolve_tac [spec] 1);
   16.41 +Level 2
   16.42 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.43 + 1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)
   16.44 +val it = () : unit
   16.45 +- by (resolve_tac [allI] 1);
   16.46 +Level 3
   16.47 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.48 + 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)
   16.49 +val it = () : unit
   16.50 +- by (dresolve_tac [spec] 1);
   16.51 +Level 4
   16.52 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.53 + 1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)
   16.54 +val it = () : unit
   16.55 +- by (resolve_tac [allI] 1);
   16.56 +Level 5
   16.57 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.58 + 1. !!z w. P(?x1,?y3(z)) ==> P(w,z)
   16.59 +val it = () : unit
   16.60 +- by (assume_tac 1);
   16.61 +by: tactic returned no results
   16.62 +
   16.63 +uncaught exception ERROR
   16.64 +- choplev 1;
   16.65 +Level 1
   16.66 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.67 + 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)
   16.68 +val it = () : unit
   16.69 +- by (resolve_tac [allI] 1);
   16.70 +Level 2
   16.71 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.72 + 1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)
   16.73 +val it = () : unit
   16.74 +- by (resolve_tac [allI] 1);
   16.75 +Level 3
   16.76 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.77 + 1. !!z w. ALL x y. P(x,y) ==> P(w,z)
   16.78 +val it = () : unit
   16.79 +- by (dresolve_tac [spec] 1);
   16.80 +Level 4
   16.81 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.82 + 1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)
   16.83 +val it = () : unit
   16.84 +- by (dresolve_tac [spec] 1);
   16.85 +Level 5
   16.86 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.87 + 1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)
   16.88 +val it = () : unit
   16.89 +- by (assume_tac 1);
   16.90 +Level 6
   16.91 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.92 +No subgoals!
   16.93 +
   16.94 +> choplev 0;
   16.95 +Level 0
   16.96 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.97 + 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
   16.98 +> by (REPEAT (assume_tac 1
   16.99 +#      ORELSE resolve_tac [impI,allI] 1
  16.100 +#      ORELSE dresolve_tac [spec] 1));
  16.101 +Level 1
  16.102 +(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
  16.103 +No subgoals!
  16.104 +
  16.105 +
  16.106 +
  16.107 +goal FOL_thy "ALL x. EX y. x=y";
  16.108 +by (resolve_tac [allI] 1);
  16.109 +by (resolve_tac [exI] 1);
  16.110 +by (resolve_tac [refl] 1);
  16.111 +
  16.112 +- goal Int_Rule.thy "ALL x. EX y. x=y";
  16.113 +Level 0
  16.114 +ALL x. EX y. x = y
  16.115 + 1. ALL x. EX y. x = y
  16.116 +val it = [] : thm list
  16.117 +- by (resolve_tac [allI] 1);
  16.118 +Level 1
  16.119 +ALL x. EX y. x = y
  16.120 + 1. !!x. EX y. x = y
  16.121 +val it = () : unit
  16.122 +- by (resolve_tac [exI] 1);
  16.123 +Level 2
  16.124 +ALL x. EX y. x = y
  16.125 + 1. !!x. x = ?y1(x)
  16.126 +val it = () : unit
  16.127 +- by (resolve_tac [refl] 1);
  16.128 +Level 3
  16.129 +ALL x. EX y. x = y
  16.130 +No subgoals!
  16.131 +val it = () : unit
  16.132 +-
  16.133 +
  16.134 +goal FOL_thy "EX y. ALL x. x=y";
  16.135 +by (resolve_tac [exI] 1);
  16.136 +by (resolve_tac [allI] 1);
  16.137 +by (resolve_tac [refl] 1);
  16.138 +
  16.139 +- goal Int_Rule.thy "EX y. ALL x. x=y";
  16.140 +Level 0
  16.141 +EX y. ALL x. x = y
  16.142 + 1. EX y. ALL x. x = y
  16.143 +val it = [] : thm list
  16.144 +- by (resolve_tac [exI] 1);
  16.145 +Level 1
  16.146 +EX y. ALL x. x = y
  16.147 + 1. ALL x. x = ?y
  16.148 +val it = () : unit
  16.149 +- by (resolve_tac [allI] 1);
  16.150 +Level 2
  16.151 +EX y. ALL x. x = y
  16.152 + 1. !!x. x = ?y
  16.153 +val it = () : unit
  16.154 +- by (resolve_tac [refl] 1);
  16.155 +by: tactic returned no results
  16.156 +
  16.157 +uncaught exception ERROR
  16.158 +
  16.159 +
  16.160 +
  16.161 +goal FOL_thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
  16.162 +by (resolve_tac [exI, allI] 1);
  16.163 +by (resolve_tac [exI, allI] 1);
  16.164 +by (resolve_tac [exI, allI] 1);
  16.165 +by (resolve_tac [exI, allI] 1);
  16.166 +by (resolve_tac [exI, allI] 1);
  16.167 +
  16.168 +- goal Int_Rule.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
  16.169 +Level 0
  16.170 +EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
  16.171 + 1. EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
  16.172 +val it = [] : thm list
  16.173 +- by (resolve_tac [exI, allI] 1);
  16.174 +Level 1
  16.175 +EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
  16.176 + 1. ALL x. EX v. ALL y. EX w. P(?u,x,v,y,w)
  16.177 +val it = () : unit
  16.178 +- by (resolve_tac [exI, allI] 1);
  16.179 +Level 2
  16.180 +EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
  16.181 + 1. !!x. EX v. ALL y. EX w. P(?u,x,v,y,w)
  16.182 +val it = () : unit
  16.183 +- by (resolve_tac [exI, allI] 1);
  16.184 +Level 3
  16.185 +EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
  16.186 + 1. !!x. ALL y. EX w. P(?u,x,?v2(x),y,w)
  16.187 +val it = () : unit
  16.188 +- by (resolve_tac [exI, allI] 1);
  16.189 +Level 4
  16.190 +EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
  16.191 + 1. !!x y. EX w. P(?u,x,?v2(x),y,w)
  16.192 +val it = () : unit
  16.193 +- by (resolve_tac [exI, allI] 1);
  16.194 +Level 5
  16.195 +EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
  16.196 + 1. !!x y. P(?u,x,?v2(x),y,?w4(x,y))
  16.197 +val it = () : unit
  16.198 +
  16.199 +
  16.200 +goal FOL_thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q";
  16.201 +by (REPEAT (resolve_tac [impI] 1));
  16.202 +by (eresolve_tac [exE] 1);
  16.203 +by (dresolve_tac [spec] 1);
  16.204 +by (eresolve_tac [mp] 1);
  16.205 +by (assume_tac 1);
  16.206 +
  16.207 +- goal Int_Rule.thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q";
  16.208 +Level 0
  16.209 +(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
  16.210 + 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
  16.211 +val it = [] : thm list
  16.212 +- by (REPEAT (resolve_tac [impI] 1));
  16.213 +Level 1
  16.214 +(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
  16.215 + 1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q
  16.216 +val it = () : unit
  16.217 +- by (eresolve_tac [exE] 1);
  16.218 +Level 2
  16.219 +(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
  16.220 + 1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q
  16.221 +val it = () : unit
  16.222 +- by (dresolve_tac [spec] 1);
  16.223 +Level 3
  16.224 +(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
  16.225 + 1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q
  16.226 +val it = () : unit
  16.227 +- by (eresolve_tac [mp] 1);
  16.228 +Level 4
  16.229 +(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
  16.230 + 1. !!x. P(x) ==> P(?x3(x))
  16.231 +val it = () : unit
  16.232 +- by (assume_tac 1);
  16.233 +Level 5
  16.234 +(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
  16.235 +No subgoals!
  16.236 +
  16.237 +
  16.238 +goal FOL_thy "((EX x.P(x)) --> Q) --> (ALL x.P(x)-->Q)";
  16.239 +by (REPEAT (resolve_tac [impI] 1));
  16.240 +
  16.241 +
  16.242 +goal FOL_thy "(EX x.P(x) --> Q) --> (ALL x.P(x))-->Q";
  16.243 +by (REPEAT (resolve_tac [impI] 1));
  16.244 +by (eresolve_tac [exE] 1);
  16.245 +by (eresolve_tac [mp] 1);
  16.246 +by (eresolve_tac [spec] 1);
  16.247 +
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/doc-src/Intro/theorems-out.txt	Wed Nov 10 05:06:55 1993 +0100
    17.3 @@ -0,0 +1,65 @@
    17.4 +> goal Nat.thy "(k+m)+n = k+(m+n)";
    17.5 +Level 0
    17.6 +k + m + n = k + (m + n)
    17.7 + 1. k + m + n = k + (m + n)
    17.8 +val it = [] : thm list
    17.9 +> by (resolve_tac [induct] 1);
   17.10 +Level 1
   17.11 +k + m + n = k + (m + n)
   17.12 + 1. k + m + n = 0
   17.13 + 2. !!x. k + m + n = x ==> k + m + n = Suc(x)
   17.14 +val it = () : unit
   17.15 +> back();
   17.16 +Level 1
   17.17 +k + m + n = k + (m + n)
   17.18 + 1. k + m + n = k + 0
   17.19 + 2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)
   17.20 +val it = () : unit
   17.21 +> back();
   17.22 +Level 1
   17.23 +k + m + n = k + (m + n)
   17.24 + 1. k + m + 0 = k + (m + 0)
   17.25 + 2. !!x. k + m + x = k + (m + x) ==> k + m + Suc(x) = k + (m + Suc(x))
   17.26 +val it = () : unit
   17.27 +> back();
   17.28 +Level 1
   17.29 +k + m + n = k + (m + n)
   17.30 + 1. k + m + n = k + (m + 0)
   17.31 + 2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))
   17.32 +val it = () : unit
   17.33 +
   17.34 +> val nat_congs = prths (mk_congs Nat.thy ["Suc", "op +"]);
   17.35 +?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)
   17.36 +
   17.37 +[| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb
   17.38 +
   17.39 +?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)
   17.40 +[| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb
   17.41 +val nat_congs = [, ] : thm list
   17.42 +> val add_ss = FOL_ss  addcongs nat_congs
   17.43 +#                    addrews  [add_0, add_Suc];
   17.44 +val add_ss = ? : simpset
   17.45 +> goal Nat.thy "(k+m)+n = k+(m+n)";
   17.46 +Level 0
   17.47 +k + m + n = k + (m + n)
   17.48 + 1. k + m + n = k + (m + n)
   17.49 +val it = [] : thm list
   17.50 +> by (res_inst_tac [("n","k")] induct 1);
   17.51 +Level 1
   17.52 +k + m + n = k + (m + n)
   17.53 + 1. 0 + m + n = 0 + (m + n)
   17.54 + 2. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)
   17.55 +val it = () : unit
   17.56 +> by (SIMP_TAC add_ss 1);
   17.57 +Level 2
   17.58 +k + m + n = k + (m + n)
   17.59 + 1. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)
   17.60 +val it = () : unit
   17.61 +> by (ASM_SIMP_TAC add_ss 1);
   17.62 +Level 3
   17.63 +k + m + n = k + (m + n)
   17.64 +No subgoals!
   17.65 +val it = () : unit
   17.66 +> val add_assoc = result();
   17.67 +?k + ?m + ?n = ?k + (?m + ?n)
   17.68 +val add_assoc =  : thm
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/doc-src/Intro/theorems.txt	Wed Nov 10 05:06:55 1993 +0100
    18.3 @@ -0,0 +1,122 @@
    18.4 +Pretty.setmargin 72;  (*existing macros just allow this margin*)
    18.5 +print_depth 0;
    18.6 +
    18.7 +(*operations for "thm"*)
    18.8 +
    18.9 +prth mp; 
   18.10 +
   18.11 +prth (mp RS mp);
   18.12 +
   18.13 +prth (conjunct1 RS mp);
   18.14 +prth (conjunct1 RSN (2,mp));
   18.15 +
   18.16 +prth (mp RS conjunct1);
   18.17 +prth (spec RS it);
   18.18 +prth (standard it);
   18.19 +
   18.20 +prth spec;
   18.21 +prth (it RS mp);
   18.22 +prth (it RS conjunct1);
   18.23 +prth (standard it);
   18.24 +
   18.25 +- prth spec;
   18.26 +ALL x. ?P(x) ==> ?P(?x)
   18.27 +- prth (it RS mp);
   18.28 +[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==> ?Q2(?x1)
   18.29 +- prth (it RS conjunct1);
   18.30 +[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==> ?P6(?x2)
   18.31 +- prth (standard it);
   18.32 +[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==> ?Pa(?x)
   18.33 +
   18.34 +(*flexflex pairs*)
   18.35 +- prth refl;
   18.36 +?a = ?a
   18.37 +- prth exI;
   18.38 +?P(?x) ==> EX x. ?P(x)
   18.39 +- prth (refl RS exI);
   18.40 +?a3(?x) == ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)
   18.41 +- prthq (flexflex_rule it);
   18.42 +EX x. ?a4 = ?a4
   18.43 +
   18.44 +(*Usage of RL*)
   18.45 +- val reflk = prth (read_instantiate [("a","k")] refl);
   18.46 +k = k
   18.47 +val reflk = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
   18.48 +- prth (reflk RS exI);
   18.49 +
   18.50 +uncaught exception THM
   18.51 +- prths ([reflk] RL [exI]);
   18.52 +EX x. x = x
   18.53 +
   18.54 +EX x. k = x
   18.55 +
   18.56 +EX x. x = k
   18.57 +
   18.58 +EX x. k = k
   18.59 +
   18.60 +
   18.61 +
   18.62 +(*tactics *)
   18.63 +
   18.64 +goal cla_thy "P|P --> P";
   18.65 +by (resolve_tac [impI] 1);
   18.66 +by (resolve_tac [disjE] 1);
   18.67 +by (assume_tac 3);
   18.68 +by (assume_tac 2);
   18.69 +by (assume_tac 1);
   18.70 +val mythm = prth(result());
   18.71 +
   18.72 +
   18.73 +goal cla_thy "(P & Q) | R  --> (P | R)";
   18.74 +by (resolve_tac [impI] 1);
   18.75 +by (eresolve_tac [disjE] 1);
   18.76 +by (dresolve_tac [conjunct1] 1);
   18.77 +by (resolve_tac [disjI1] 1);
   18.78 +by (resolve_tac [disjI2] 2);
   18.79 +by (REPEAT (assume_tac 1));
   18.80 +
   18.81 +
   18.82 +- goal cla_thy "(P & Q) | R  --> (P | R)";
   18.83 +Level 0
   18.84 +P & Q | R --> P | R
   18.85 + 1. P & Q | R --> P | R
   18.86 +- by (resolve_tac [impI] 1);
   18.87 +Level 1
   18.88 +P & Q | R --> P | R
   18.89 + 1. P & Q | R ==> P | R
   18.90 +- by (eresolve_tac [disjE] 1);
   18.91 +Level 2
   18.92 +P & Q | R --> P | R
   18.93 + 1. P & Q ==> P | R
   18.94 + 2. R ==> P | R
   18.95 +- by (dresolve_tac [conjunct1] 1);
   18.96 +Level 3
   18.97 +P & Q | R --> P | R
   18.98 + 1. P ==> P | R
   18.99 + 2. R ==> P | R
  18.100 +- by (resolve_tac [disjI1] 1);
  18.101 +Level 4
  18.102 +P & Q | R --> P | R
  18.103 + 1. P ==> P
  18.104 + 2. R ==> P | R
  18.105 +- by (resolve_tac [disjI2] 2);
  18.106 +Level 5
  18.107 +P & Q | R --> P | R
  18.108 + 1. P ==> P
  18.109 + 2. R ==> R
  18.110 +- by (REPEAT (assume_tac 1));
  18.111 +Level 6
  18.112 +P & Q | R --> P | R
  18.113 +No subgoals!
  18.114 +
  18.115 +
  18.116 +goal cla_thy "(P | Q) | R  -->  P | (Q | R)";
  18.117 +by (resolve_tac [impI] 1);
  18.118 +by (eresolve_tac [disjE] 1);
  18.119 +by (eresolve_tac [disjE] 1);
  18.120 +by (resolve_tac [disjI1] 1);
  18.121 +by (resolve_tac [disjI2] 2);
  18.122 +by (resolve_tac [disjI1] 2);
  18.123 +by (resolve_tac [disjI2] 3);
  18.124 +by (resolve_tac [disjI2] 3);
  18.125 +by (REPEAT (assume_tac 1));