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 manysorted firstorder 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 ZermeloFraenkel

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 higherorder logic of Church~\cite{church40},

343

24 
which is also implemented by Gordon's~{\sc hol} system~\cite{mgordonhol}.


25 
This objectlogic should not be confused with Isabelle's metalogic, which is

104

26 
also a form of higherorder logic.

318

27 


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


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

104

30 

318

31 
\item[\thydx{CTT}] is a version of MartinL\"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 firstorder 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}


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


45 
are currently undocumented.

104

46 

287

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.

104

50 


51 


52 
\section{Syntax definitions}

318

53 
The syntax of each logic is presented using a contextfree grammar.

104

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,~$$

318

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

104

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

318

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.

104

71 


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

318

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


74 
firstorder logic, where $\exists$ has lower priority than $\disj$,


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

104

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

318

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

104

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

318

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

104

93 


94 
To avoid excess detail, the logic descriptions adopt a semiformal style.


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

318

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.

104

100 


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

343

102 
example, the formulae of firstorder logic have type~$o$. Every

104

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

318

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

104

107 
separate possibility in the grammar for formulae.


108 


109 

318

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

104

111 
Most objectlogics come with simple proof procedures. These are reasonably


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


113 
can do singlestep proofs using \verbresolve_tac and


114 
\verbassume_tac, referring to the inference rules of the logic by {\sc


115 
ml} identifiers.


116 

318

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 
\]

104

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

343

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

318

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

104

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 depthfirst or


142 
bestfirst strategy.
