author | paulson |
Fri, 27 Nov 1998 13:13:22 +0100 | |
changeset 5980 | 2e9314c07146 |
parent 3486 | 10cf84e5d2c2 |
permissions | -rw-r--r-- |
104 | 1 |
%% $Id$ |
287 | 2 |
\chapter{Basic Concepts} |
104 | 3 |
Several logics come with Isabelle. Many of them are sufficiently developed |
4 |
to serve as comfortable reasoning environments. They are also good |
|
5 |
starting points for defining new logics. Each logic is distributed with |
|
6 |
sample proofs, some of which are described in this document. |
|
7 |
||
318 | 8 |
\begin{ttdescription} |
9 |
\item[\thydx{FOL}] is many-sorted first-order logic with natural |
|
104 | 10 |
deduction. It comes in both constructive and classical versions. |
11 |
||
318 | 12 |
\item[\thydx{ZF}] is axiomatic set theory, using the Zermelo-Fraenkel |
104 | 13 |
axioms~\cite{suppes72}. It is built upon classical~\FOL{}. |
318 | 14 |
|
15 |
\item[\thydx{CCL}] is Martin Coen's Classical Computational Logic, |
|
16 |
which is the basis of a preliminary method for deriving programs from |
|
17 |
proofs~\cite{coen92}. It is built upon classical~\FOL{}. |
|
104 | 18 |
|
318 | 19 |
\item[\thydx{LCF}] is a version of Scott's Logic for Computable |
20 |
Functions, which is also implemented by the~{\sc lcf} |
|
21 |
system~\cite{paulson87}. It is built upon classical~\FOL{}. |
|
22 |
||
23 |
\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40}, |
|
343 | 24 |
which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}. |
25 |
This object-logic should not be confused with Isabelle's meta-logic, which is |
|
104 | 26 |
also a form of higher-order logic. |
318 | 27 |
|
3139 | 28 |
\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an |
29 |
extension of {\tt HOL}\@. |
|
104 | 30 |
|
318 | 31 |
\item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type |
104 | 32 |
Theory~\cite{nordstrom90}, with extensional equality. Universes are not |
33 |
included. |
|
34 |
||
318 | 35 |
\item[\thydx{LK}] is another version of first-order logic, a classical |
104 | 36 |
sequent calculus. Sequents have the form $A@1,\ldots,A@m\turn |
37 |
B@1,\ldots,B@n$; rules are applied using associative matching. |
|
38 |
||
318 | 39 |
\item[\thydx{Modal}] implements the modal logics $T$, $S4$, |
40 |
and~$S43$. It is built upon~\LK{}. |
|
104 | 41 |
|
318 | 42 |
\item[\thydx{Cube}] is Barendregt's $\lambda$-cube. |
43 |
\end{ttdescription} |
|
3151 | 44 |
The logics {\tt CCL}, {\tt LCF}, {\tt HOLCF}, {\tt Modal} and {\tt |
3486
10cf84e5d2c2
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3216
diff
changeset
|
45 |
Cube} are currently undocumented. All object-logics' sources are |
3151 | 46 |
distributed with Isabelle (see the directory \texttt{src}). They are |
3216 | 47 |
also available for browsing on the WWW at: |
48 |
\begin{ttbox} |
|
49 |
http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/ |
|
50 |
\end{ttbox} |
|
51 |
Note that this is not necessarily consistent with your local sources! |
|
104 | 52 |
|
3216 | 53 |
\medskip You should not read this manual before reading {\em |
54 |
Introduction to Isabelle\/} and performing some Isabelle proofs. |
|
55 |
Consult the {\em Reference Manual} for more information on tactics, |
|
56 |
packages, etc. |
|
104 | 57 |
|
58 |
||
59 |
\section{Syntax definitions} |
|
318 | 60 |
The syntax of each logic is presented using a context-free grammar. |
104 | 61 |
These grammars obey the following conventions: |
62 |
\begin{itemize} |
|
63 |
\item identifiers denote nonterminal symbols |
|
64 |
\item {\tt typewriter} font denotes terminal symbols |
|
65 |
\item parentheses $(\ldots)$ express grouping |
|
66 |
\item constructs followed by a Kleene star, such as $id^*$ and $(\ldots)^*$ |
|
67 |
can be repeated~0 or more times |
|
68 |
\item alternatives are separated by a vertical bar,~$|$ |
|
318 | 69 |
\item the symbol for alphanumeric identifiers is~{\it id\/} |
104 | 70 |
\item the symbol for scheme variables is~{\it var} |
71 |
\end{itemize} |
|
72 |
To reduce the number of nonterminals and grammar rules required, Isabelle's |
|
318 | 73 |
syntax module employs {\bf priorities},\index{priorities} or precedences. |
74 |
Each grammar rule is given by a mixfix declaration, which has a priority, |
|
75 |
and each argument place has a priority. This general approach handles |
|
76 |
infix operators that associate either to the left or to the right, as well |
|
77 |
as prefix and binding operators. |
|
104 | 78 |
|
79 |
In a syntactically valid expression, an operator's arguments never involve |
|
318 | 80 |
an operator of lower priority unless brackets are used. Consider |
81 |
first-order logic, where $\exists$ has lower priority than $\disj$, |
|
82 |
which has lower priority than $\conj$. There, $P\conj Q \disj R$ |
|
104 | 83 |
abbreviates $(P\conj Q) \disj R$ rather than $P\conj (Q\disj R)$. Also, |
84 |
$\exists x.P\disj Q$ abbreviates $\exists x.(P\disj Q)$ rather than |
|
85 |
$(\exists x.P)\disj Q$. Note especially that $P\disj(\exists x.Q)$ |
|
86 |
becomes syntactically invalid if the brackets are removed. |
|
87 |
||
88 |
A {\bf binder} is a symbol associated with a constant of type |
|
3139 | 89 |
$(\sigma\To\tau)\To\tau'$. For instance, we may declare~$\forall$ as |
90 |
a binder for the constant~$All$, which has type $(\alpha\To o)\To o$. |
|
91 |
This defines the syntax $\forall x.t$ to mean $All(\lambda x.t)$. We |
|
92 |
can also write $\forall x@1\ldots x@m.t$ to abbreviate $\forall x@1. |
|
93 |
\ldots \forall x@m.t$; this is possible for any constant provided that |
|
94 |
$\tau$ and $\tau'$ are the same type. \HOL's description operator |
|
95 |
$\varepsilon x.P\,x$ has type $(\alpha\To bool)\To\alpha$ and can bind |
|
96 |
only one variable, except when $\alpha$ is $bool$. \ZF's bounded |
|
97 |
quantifier $\forall x\in A.P(x)$ cannot be declared as a binder |
|
98 |
because it has type $[i, i\To o]\To o$. The syntax for binders allows |
|
99 |
type constraints on bound variables, as in |
|
3151 | 100 |
\[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \] |
104 | 101 |
|
102 |
To avoid excess detail, the logic descriptions adopt a semi-formal style. |
|
103 |
Infix operators and binding operators are listed in separate tables, which |
|
318 | 104 |
include their priorities. Grammar descriptions do not include numeric |
105 |
priorities; instead, the rules appear in order of decreasing priority. |
|
106 |
This should suffice for most purposes; for full details, please consult the |
|
107 |
actual syntax definitions in the {\tt.thy} files. |
|
104 | 108 |
|
109 |
Each nonterminal symbol is associated with some Isabelle type. For |
|
343 | 110 |
example, the formulae of first-order logic have type~$o$. Every |
104 | 111 |
Isabelle expression of type~$o$ is therefore a formula. These include |
112 |
atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more |
|
113 |
generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have |
|
318 | 114 |
suitable types. Therefore, `expression of type~$o$' is listed as a |
104 | 115 |
separate possibility in the grammar for formulae. |
116 |
||
117 |
||
318 | 118 |
\section{Proof procedures}\label{sec:safe} |
104 | 119 |
Most object-logics come with simple proof procedures. These are reasonably |
120 |
powerful for interactive use, though often simplistic and incomplete. You |
|
121 |
can do single-step proofs using \verb|resolve_tac| and |
|
122 |
\verb|assume_tac|, referring to the inference rules of the logic by {\sc |
|
123 |
ml} identifiers. |
|
124 |
||
318 | 125 |
For theorem proving, rules can be classified as {\bf safe} or {\bf unsafe}. |
126 |
A rule is safe if applying it to a provable goal always yields provable |
|
127 |
subgoals. If a rule is safe then it can be applied automatically to a goal |
|
128 |
without destroying our chances of finding a proof. For instance, all the |
|
129 |
rules of the classical sequent calculus {\sc lk} are safe. Universal |
|
130 |
elimination is unsafe if the formula $\all{x}P(x)$ is deleted after use. |
|
131 |
Other unsafe rules include the following: |
|
132 |
\[ \infer[({\disj}I1)]{P\disj Q}{P} \qquad |
|
133 |
\infer[({\imp}E)]{Q}{P\imp Q & P} \qquad |
|
134 |
\infer[({\exists}I)]{\exists x.P}{P[t/x]} |
|
135 |
\] |
|
104 | 136 |
|
137 |
Proof procedures use safe rules whenever possible, delaying the application |
|
3486
10cf84e5d2c2
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3216
diff
changeset
|
138 |
of unsafe rules. Those safe rules are preferred that generate the fewest |
10cf84e5d2c2
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3216
diff
changeset
|
139 |
subgoals. Safe rules are (by definition) deterministic, while the unsafe |
10cf84e5d2c2
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3216
diff
changeset
|
140 |
rules require search. The design of a suitable set of rules can be as |
104 | 141 |
important as the strategy for applying them. |
142 |
||
143 |
Many of the proof procedures use backtracking. Typically they attempt to |
|
144 |
solve subgoal~$i$ by repeatedly applying a certain tactic to it. This |
|
343 | 145 |
tactic, which is known as a {\bf step tactic}, resolves a selection of |
3486
10cf84e5d2c2
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3216
diff
changeset
|
146 |
rules with subgoal~$i$. This may replace one subgoal by many; the |
104 | 147 |
search persists until there are fewer subgoals in total than at the start. |
148 |
Backtracking happens when the search reaches a dead end: when the step |
|
149 |
tactic fails. Alternative outcomes are then searched by a depth-first or |
|
150 |
best-first strategy. |