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