--- a/doc-src/Intro/advanced.tex Wed Aug 13 17:24:59 2003 +0200
+++ b/doc-src/Intro/advanced.tex Wed Aug 13 17:44:01 2003 +0200
@@ -48,14 +48,20 @@
\item If one or more premises involves the meta-connectives $\Forall$ or
$\Imp$, then the command sets the goal to be $\phi$ and returns a list
consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.
- These meta-assumptions are also recorded internally, allowing
+ These meta-level assumptions are also recorded internally, allowing
\texttt{result} (which is called by \texttt{qed}) to discharge them in the
original order.
\end{itemize}
Rules that discharge assumptions or introduce eigenvariables have complex
-premises, and the second case applies.
+premises, and the second case applies. In this section, many of the
+theorems are subject to meta-level assumptions, so we make them visible by by setting the
+\ttindex{show_hyps} flag:
+\begin{ttbox}
+set show_hyps;
+{\out val it = true : bool}
+\end{ttbox}
-Let us derive $\conj$ elimination. Until now, calling \texttt{Goal} has
+Now, we are ready to derive $\conj$ elimination. Until now, calling \texttt{Goal} has
returned an empty list, which we have ignored. In this example, the list
contains the two premises of the rule, since one of them involves the $\Imp$
connective. We bind them to the \ML\ identifiers \texttt{major} and {\tt
@@ -357,7 +363,9 @@
\end{ttbox}
where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,
$rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be
-enclosed in quotation marks.
+enclosed in quotation marks. Rules are simply axioms; they are
+called \emph{rules} because they are mainly used to specify the inference
+rules when defining a new logic.
\indexbold{definitions} The {\bf definition part} is similar, but with
the keyword \texttt{defs} instead of \texttt{rules}. {\bf Definitions} are
@@ -368,10 +376,10 @@
of the equation instead of abstracted on the right-hand side.
Isabelle checks for common errors in definitions, such as extra
-variables on the right-hand side, but currently does not a complete
-test of well-formedness. Thus determined users can write
-non-conservative `definitions' by using mutual recursion, for example;
-the consequences of such actions are their responsibility.
+variables on the right-hand side and cyclic dependencies, that could
+least to inconsistency. It is still essential to take care:
+theorems proved on the basis of incorrect definitions are useless,
+your system can be consistent and yet still wrong.
\index{examples!of theories} This example theory extends first-order
logic by declaring and defining two constants, {\em nand} and {\em
@@ -682,7 +690,8 @@
\end{ttbox}
Because $nat$ and $bool$ have class $arith$, we can use $0$, $1$ and $+$ at
either type. The type constraints in the axioms are vital. Without
-constraints, the $x$ in $1+x = x$ would have type $\alpha{::}arith$
+constraints, the $x$ in $1+x = 1$ (axiom \texttt{or1l})
+would have type $\alpha{::}arith$
and the axiom would hold for any type of class $arith$. This would
collapse $nat$ to a trivial type:
\[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \]
@@ -998,7 +1007,7 @@
{\out Suc(x) + m + n = Suc(x) + (m + n)}
\end{ttbox}
The inductive step requires rewriting by the equations for addition
-together the induction hypothesis, which is also an equation. The
+and with the induction hypothesis, which is also an equation. The
tactic~\ttindex{Asm_simp_tac} rewrites using the implicit
simplification set and any useful assumptions:
\begin{ttbox}
@@ -1219,7 +1228,7 @@
{\out rev(?x, a : b : c : Nil)}
{\out 1. rev(?x, a : b : c : Nil)}
\ttbreak
-by (DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1));
+by prolog_tac;
{\out Level 1}
{\out rev(c : b : a : Nil, a : b : c : Nil)}
{\out No subgoals!}
--- a/doc-src/Intro/deriv.txt Wed Aug 13 17:24:59 2003 +0200
+++ b/doc-src/Intro/deriv.txt Wed Aug 13 17:44:01 2003 +0200
@@ -4,7 +4,7 @@
print_depth 0;
-val [major,minor] = goal Int_Rule.thy
+val [major,minor] = goal IFOL.thy
"[| P&Q; [| P; Q |] ==> R |] ==> R";
prth minor;
by (resolve_tac [minor] 1);
--- a/doc-src/Intro/getting.tex Wed Aug 13 17:24:59 2003 +0200
+++ b/doc-src/Intro/getting.tex Wed Aug 13 17:44:01 2003 +0200
@@ -1,12 +1,13 @@
%% $Id$
-\part{Getting Started with Isabelle}\label{chap:getting}
-Let us consider how to perform simple proofs using Isabelle. At
-present, Isabelle's user interface is \ML. Proofs are conducted by
+\part{Using Isabelle from the ML Top-Level}\label{chap:getting}
+
+Most Isabelle users write proof scripts using the Isar language, as described in the \emph{Tutorial}, and debug them through the Proof General user interface~\cite{proofgeneral}. Isabelle's original user interface --- based on the \ML{} top-level --- is still available, however.
+Proofs are conducted by
applying certain \ML{} functions, which update a stored proof state.
-Basically, all syntax must be expressed using plain {\sc ascii}
-characters. There are also mechanisms built into Isabelle that support
+All syntax can be expressed using plain {\sc ascii}
+characters, but Isabelle can support
alternative syntaxes, for example using mathematical symbols from a
-special screen font. The meta-logic and major object-logics already
+special screen font. The meta-logic and main object-logics already
provide such fancy output as an option.
Object-logics are built upon Pure Isabelle, which implements the
@@ -167,7 +168,7 @@
\]
To illustrate the notation, consider two axioms for first-order logic:
$$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$
-$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$
+$$ \List{\exists x. P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$
$({\conj}I)$ translates into {\sc ascii} characters as
\begin{ttbox}
[| ?P; ?Q |] ==> ?P & ?Q
@@ -188,7 +189,7 @@
For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as
\begin{ttbox}
-[| EX x.P(x); !!x. P(x) ==> Q |] ==> Q
+[| EX x. P(x); !!x. P(x) ==> Q |] ==> Q
\end{ttbox}
@@ -251,8 +252,8 @@
session illustrates two formats for the display of theorems. Isabelle's
top-level displays theorems as \ML{} values, enclosed in quotes. Printing
commands like \texttt{prth} omit the quotes and the surrounding \texttt{val
- \ldots :\ thm}. Ignoring their side-effects, the commands are identity
-functions.
+ \ldots :\ thm}. Ignoring their side-effects, the printing commands are
+identity functions.
To contrast \texttt{RS} with \texttt{RSN}, we resolve
\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}.
@@ -309,7 +310,17 @@
exI;
{\out val it = "?P(?x) ==> EX x. ?P(x)" : thm}
refl RS exI;
-{\out val it = "?a3(?x) =?= ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)" : thm}
+{\out val it = "EX x. ?a3(x) = ?a2(x)" [.] : thm}
+\end{ttbox}
+%
+The mysterious symbol \texttt{[.]} indicates that the result is subject to
+a meta-level hypothesis. We can make all such hypotheses visible by setting the
+\ttindexbold{show_hyps} flag:
+\begin{ttbox}
+set show_hyps;
+{\out val it = true : bool}
+refl RS exI;
+{\out val it = "EX x. ?a3(x) = ?a2(x)" ["?a3(?x) =?= ?a2(?x)"] : thm}
\end{ttbox}
\noindent
@@ -348,7 +359,9 @@
unique unifier:
\begin{ttbox}
reflk RS exI;
-{\out uncaught exception THM}
+{\out uncaught exception}
+{\out THM ("RSN: multiple unifiers", 1,}
+{\out ["k = k", "?P(?x) ==> EX x. ?P(x)"])}
\end{ttbox}
Using \ttindex{RL} this time, we discover that there are four unifiers, and
four resolvents:
@@ -411,8 +424,7 @@
its many commands, most important are the following:
\begin{ttdescription}
\item[\ttindex{Goal} {\it formula}; ]
-begins a new proof, where $theory$ is usually an \ML\ identifier
-and the {\it formula\/} is written as an \ML\ string.
+begins a new proof, where the {\it formula\/} is written as an \ML\ string.
\item[\ttindex{by} {\it tactic}; ]
applies the {\it tactic\/} to the current proof
@@ -825,7 +837,7 @@
Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we
use \texttt{REPEAT}:
\begin{ttbox}
-Goal "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q";
+Goal "(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q";
{\out Level 0}
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
{\out 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
@@ -878,11 +890,13 @@
\subsection{The classical reasoner}
\index{classical reasoner}
-Although Isabelle cannot compete with fully automatic theorem provers, it
-provides enough automation to tackle substantial examples. The classical
+Isabelle provides enough automation to tackle substantial examples.
+The classical
reasoner can be set up for any classical natural deduction logic;
see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
{Chap.\ts\ref{chap:classical}}.
+It cannot compete with fully automatic theorem provers, but it is
+competitive with tools found in other interactive provers.
Rules are packaged into {\bf classical sets}. The classical reasoner
provides several tactics, which apply rules using naive algorithms.
--- a/doc-src/Intro/intro.tex Wed Aug 13 17:24:59 2003 +0200
+++ b/doc-src/Intro/intro.tex Wed Aug 13 17:44:01 2003 +0200
@@ -31,6 +31,16 @@
\pagestyle{empty}
\begin{titlepage}
\maketitle
+\emph{Note}: this document is part of the earlier Isabelle documentation,
+which is largely superseded by the Isabelle/HOL
+\emph{Tutorial}~\cite{isa-tutorial}. It describes the old-style theory
+syntax and shows how to conduct proofs using the
+ML top level. This style of interaction is largely obsolete:
+most Isabelle proofs are now written using the Isar
+language and the Proof General interface. However, this paper contains valuable
+information that is not available elsewhere. Its examples are based
+on first-order logic rather than higher-order logic.
+
\thispagestyle{empty}
\vfill
{\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
@@ -58,12 +68,13 @@
several generic tools, such as simplifiers and classical theorem provers,
which can be applied to object-logics.
+Isabelle is a large system, but beginners can get by with a small
+repertoire of commands and a basic knowledge of how Isabelle works.
+The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some
+knowledge of Standard~\ML{}, because Isabelle is written in \ML{};
\index{ML}
-Isabelle is a large system, but beginners can get by with a small
-repertoire of commands and a basic knowledge of how Isabelle works. Some
-knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user
-interface. Advanced Isabelle theorem proving can involve writing \ML{}
-code, possibly with Isabelle's sources at hand. My book
+if you are prepared to writing \ML{}
+code, you can get Isabelle to do almost anything. My book
on~\ML{}~\cite{paulson-ml2} covers much material connected with Isabelle,
including a simple theorem prover. Users must be familiar with logic as
used in computer science; there are many good
@@ -83,8 +94,10 @@
treatment of quantifiers. The 1988 version added limited polymorphism and
support for natural deduction. The 1989 version included a parser and
pretty printer generator. The 1992 version introduced type classes, to
-support many-sorted and higher-order logics. The current version provides
-greater support for theories and is much faster. Isabelle is still under
+support many-sorted and higher-order logics. The 1994 version introduced
+greater support for theories. The most important recent change is the
+introduction of the Isar proof language, thanks to Markus Wenzel.
+Isabelle is still under
development and will continue to change.
\subsubsection*{Overview}
@@ -101,7 +114,7 @@
\subsubsection*{Acknowledgements}
Tobias Nipkow contributed most of the section on defining theories.
-Stefan Berghofer and Sara Kalvala suggested improvements.
+Stefan Berghofer, Sara Kalvala and Viktor Kuncak suggested improvements.
Tobias Nipkow has made immense contributions to Isabelle, including the parser
generator, type classes, and the simplifier. Carsten Clasohm and Markus