Intro/document/getting.tex

9 special screen font.  The meta-logic and main object-logics already
23 and demonstrates forward proof.  The examples are set in first-order logic.
24 The command to start Isabelle running first-order logic is
41 as {\tt=}, {\tt==}, {\tt=>} and {\tt==>}.  (The latter three are part of
45 have not been declared as symbols!  The parser resolves any ambiguity by
57 mark, an identifier (or type identifier), and a subscript.  The subscript,
60 \footnote{The subscript may appear after the identifier, separated by a
66   zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6.  The same
67   conventions apply to type unknowns.  The question mark is {\it not\/}
79 with a syntax like \ML's.  The built-in type \tydx{prop} is the type
116 The theorems and rules of an object-logic are represented by theorems in
179 The schematic variables let unification instantiate the rule.  To avoid
208 The main theorem printing commands are \texttt{prth}, \texttt{prths} and~{\tt
235 The rules of a theory are normally bound to \ML\ identifiers.  Suppose we are
319 The mysterious symbol \texttt{[.]} indicates that the result is subject to
352 use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists.  The
385 \subsection{The basic tactics}
386 The tactics \texttt{assume_tac}, {\tt
391 positive integer~$i$, failing if~$i$ is out of range.  The resolution
402   is the basic resolution tactic, used for most proof steps.  The $thms$
406   place.  A rule can admit many higher-order unifiers.  The tactic fails if
450 The commands and tactics given above are cumbersome for interactive use.
480 P\imp P$ as the main goal and the only subgoal.  The {\bf level} of the
491 (The meta-implication {\tt==>} indicates assumptions.)  We apply
560 \ttindex{eresolve_tac} deletes the assumption after use.  The resulting proof
582 The next two steps apply~(${\disj}I1$) and~(${\disj}I2$) in an obvious manner.
596 Two calls of \texttt{assume_tac} can finish the proof.  The
622 attempted proof of the non-theorem $\exists y.\forall x.x=y$.  The former
629 \paragraph{The successful proof.}
630 The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules
643 The variable~\texttt{x} is no longer universally quantified, but is a
645 meta-level.  The subgoal must be proved for all possible values of~\texttt{x}.
654 The bound variable \texttt{y} has become {\tt?y1(x)}.  This term consists of
664 Let us consider what has happened in detail.  The reflexivity axiom is
666 unified with $\Forall x.x=\Var{y@1}(x)$.  The function unknowns $\Var{f}$
670 \paragraph{The unsuccessful proof.}
684 The unknown \texttt{?y} may be replaced by any term, but this can never
694 The reflexivity axiom does not unify with subgoal~1.
726 \paragraph{The wrong approach.}
740 The unknown \texttt{?x1} and the parameter \texttt{z} have appeared.  We again
753 The unknown \texttt{?y3} and the parameter \texttt{w} have appeared.  Each
764 \paragraph{The right approach.}
766 Parameters should be created before unknowns.  The
787 The parameters \texttt{z} and~\texttt{w} have appeared.  We now create the
853 We can eliminate the universal or the existential quantifier.  The
855 parameter.  The rule~$(\exists E)$ is bound to the
863 The only possibility now is $(\forall E)$, a destruction rule.  We use
884 The tactic has reduced~\texttt{Q} to~\texttt{P(?x3(x))}, deleting the
885 implication.  The final step is trivial, thanks to the occurrence of~\texttt{x}.
894 \subsection{The classical reasoner}
897 The classical
904 Rules are packaged into {\bf classical sets}.  The classical reasoner
906 Unification handles quantifiers as shown above.  The most useful tactic
909 Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}.  (The
951 The classical reasoner is not restricted to the usual logical connectives.
952 The natural deduction rules for unions and intersections resemble those for
953 disjunction and conjunction.  The rules for infinite unions and