doc-src/Logics/intro.tex
 author paulson Fri Feb 16 18:00:47 1996 +0100 (1996-02-16) changeset 1512 ce37c64244c0 parent 343 8d77f767bd26 child 3139 671a5f2cac6a permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 %% $Id$

     2 \chapter{Basic Concepts}

     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

     8 \begin{ttdescription}

     9 \item[\thydx{FOL}] is many-sorted first-order logic with natural

    10 deduction.  It comes in both constructive and classical versions.

    11

    12 \item[\thydx{ZF}] is axiomatic set theory, using the Zermelo-Fraenkel

    13 axioms~\cite{suppes72}.  It is built upon classical~\FOL{}.

    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{}.

    18

    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},

    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

    26 also a form of higher-order logic.

    27

    28 \item[\thydx{HOLCF}] is an alternative version of {\sc lcf}, defined

    29   as an extension of {\tt HOL}\@.

    30

    31 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type

    32 Theory~\cite{nordstrom90}, with extensional equality.  Universes are not

    33 included.

    34

    35 \item[\thydx{LK}] is another version of first-order logic, a classical

    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

    39 \item[\thydx{Modal}] implements the modal logics $T$, $S4$,

    40   and~$S43$.  It is built upon~\LK{}.

    41

    42 \item[\thydx{Cube}] is Barendregt's $\lambda$-cube.

    43 \end{ttdescription}

    44 The logics {\tt CCL}, {\tt LCF}, {\tt HOLCF}, {\tt Modal} and {\tt Cube}

    45 are currently undocumented.

    46

    47 You should not read this before reading {\em Introduction to Isabelle\/}

    48 and performing some Isabelle proofs.  Consult the {\em Reference Manual}

    49 for more information on tactics, packages, etc.

    50

    51

    52 \section{Syntax definitions}

    53 The syntax of each logic is presented using a context-free grammar.

    54 These grammars obey the following conventions:

    55 \begin{itemize}

    56 \item identifiers denote nonterminal symbols

    57 \item {\tt typewriter} font denotes terminal symbols

    58 \item parentheses $(\ldots)$ express grouping

    59 \item constructs followed by a Kleene star, such as $id^*$ and $(\ldots)^*$

    60 can be repeated~0 or more times

    61 \item alternatives are separated by a vertical bar,~$|$

    62 \item the symbol for alphanumeric identifiers is~{\it id\/}

    63 \item the symbol for scheme variables is~{\it var}

    64 \end{itemize}

    65 To reduce the number of nonterminals and grammar rules required, Isabelle's

    66 syntax module employs {\bf priorities},\index{priorities} or precedences.

    67 Each grammar rule is given by a mixfix declaration, which has a priority,

    68 and each argument place has a priority.  This general approach handles

    69 infix operators that associate either to the left or to the right, as well

    70 as prefix and binding operators.

    71

    72 In a syntactically valid expression, an operator's arguments never involve

    73 an operator of lower priority unless brackets are used.  Consider

    74 first-order logic, where $\exists$ has lower priority than $\disj$,

    75 which has lower priority than $\conj$.  There, $P\conj Q \disj R$

    76 abbreviates $(P\conj Q) \disj R$ rather than $P\conj (Q\disj R)$.  Also,

    77 $\exists x.P\disj Q$ abbreviates $\exists x.(P\disj Q)$ rather than

    78 $(\exists x.P)\disj Q$.  Note especially that $P\disj(\exists x.Q)$

    79 becomes syntactically invalid if the brackets are removed.

    80

    81 A {\bf binder} is a symbol associated with a constant of type

    82 $(\sigma\To\tau)\To\tau'$.  For instance, we may declare~$\forall$ as a

    83 binder for the constant~$All$, which has type $(\alpha\To o)\To o$.  This

    84 defines the syntax $\forall x.t$ to mean $All(\lambda x.t)$.  We can

    85 also write $\forall x@1\ldots x@m.t$ to abbreviate $\forall x@1. \ldots   86 \forall x@m.t$; this is possible for any constant provided that $\tau$ and

    87 $\tau'$ are the same type.  \HOL's description operator $\epsilon x.P(x)$

    88 has type $(\alpha\To bool)\To\alpha$ and can bind only one variable, except

    89 when $\alpha$ is $bool$.  \ZF's bounded quantifier $\forall x\in A.P(x)$

    90 cannot be declared as a binder because it has type $[i, i\To o]\To o$.  The

    91 syntax for binders allows type constraints on bound variables, as in

    92 $\forall (x{::}\alpha) \; (y{::}\beta). R(x,y)$

    93

    94 To avoid excess detail, the logic descriptions adopt a semi-formal style.

    95 Infix operators and binding operators are listed in separate tables, which

    96 include their priorities.  Grammar descriptions do not include numeric

    97 priorities; instead, the rules appear in order of decreasing priority.

    98 This should suffice for most purposes; for full details, please consult the

    99 actual syntax definitions in the {\tt.thy} files.

   100

   101 Each nonterminal symbol is associated with some Isabelle type.  For

   102 example, the formulae of first-order logic have type~$o$.  Every

   103 Isabelle expression of type~$o$ is therefore a formula.  These include

   104 atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more

   105 generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have

   106 suitable types.  Therefore, expression of type~$o$' is listed as a

   107 separate possibility in the grammar for formulae.

   108

   109

   110 \section{Proof procedures}\label{sec:safe}

   111 Most object-logics come with simple proof procedures.  These are reasonably

   112 powerful for interactive use, though often simplistic and incomplete.  You

   113 can do single-step proofs using \verb|resolve_tac| and

   114 \verb|assume_tac|, referring to the inference rules of the logic by {\sc

   115 ml} identifiers.

   116

   117 For theorem proving, rules can be classified as {\bf safe} or {\bf unsafe}.

   118 A rule is safe if applying it to a provable goal always yields provable

   119 subgoals.  If a rule is safe then it can be applied automatically to a goal

   120 without destroying our chances of finding a proof.  For instance, all the

   121 rules of the classical sequent calculus {\sc lk} are safe.  Universal

   122 elimination is unsafe if the formula $\all{x}P(x)$ is deleted after use.

   123 Other unsafe rules include the following:

   124 $\infer[({\disj}I1)]{P\disj Q}{P} \qquad   125 \infer[({\imp}E)]{Q}{P\imp Q & P} \qquad   126 \infer[({\exists}I)]{\exists x.P}{P[t/x]}   127$

   128

   129 Proof procedures use safe rules whenever possible, delaying the application

   130 of unsafe rules. Those safe rules are preferred that generate the fewest

   131 subgoals. Safe rules are (by definition) deterministic, while the unsafe

   132 rules require search. The design of a suitable set of rules can be as

   133 important as the strategy for applying them.

   134

   135 Many of the proof procedures use backtracking.  Typically they attempt to

   136 solve subgoal~$i$ by repeatedly applying a certain tactic to it.  This

   137 tactic, which is known as a {\bf step tactic}, resolves a selection of

   138 rules with subgoal~$i$. This may replace one subgoal by many;  the

   139 search persists until there are fewer subgoals in total than at the start.

   140 Backtracking happens when the search reaches a dead end: when the step

   141 tactic fails.  Alternative outcomes are then searched by a depth-first or

   142 best-first strategy.
`