doc-src/Intro/foundations.tex
author boehmes
Tue, 07 Dec 2010 15:44:38 +0100
changeset 41064 0c447a17770a
parent 9695 ec7d7f877712
child 42637 381fdcab0f36
permissions -rw-r--r--
updated SMT certificates
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
3106
wenzelm
parents: 3103
diff changeset
     2
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     3
\part{Foundations} 
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
     4
The following sections discuss Isabelle's logical foundations in detail:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     5
representing logical syntax in the typed $\lambda$-calculus; expressing
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     6
inference rules in Isabelle's meta-logic; combining rules by resolution.
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
     7
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
     8
If you wish to use Isabelle immediately, please turn to
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
     9
page~\pageref{chap:getting}.  You can always read about foundations later,
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    10
either by returning to this point or by looking up particular items in the
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    11
index.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    12
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    13
\begin{figure} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    14
\begin{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    15
  \neg P   & \hbox{abbreviates} & P\imp\bot \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    16
  P\bimp Q & \hbox{abbreviates} & (P\imp Q) \conj (Q\imp P)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    17
\end{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    18
\vskip 4ex
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    19
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    20
\(\begin{array}{c@{\qquad\qquad}c}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    21
  \infer[({\conj}I)]{P\conj Q}{P & Q}  &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    22
  \infer[({\conj}E1)]{P}{P\conj Q} \qquad 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    23
  \infer[({\conj}E2)]{Q}{P\conj Q} \\[4ex]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    24
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    25
  \infer[({\disj}I1)]{P\disj Q}{P} \qquad 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    26
  \infer[({\disj}I2)]{P\disj Q}{Q} &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    27
  \infer[({\disj}E)]{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}}\\[4ex]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    28
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    29
  \infer[({\imp}I)]{P\imp Q}{\infer*{Q}{[P]}} &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    30
  \infer[({\imp}E)]{Q}{P\imp Q & P}  \\[4ex]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    31
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    32
  &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    33
  \infer[({\bot}E)]{P}{\bot}\\[4ex]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    34
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    35
  \infer[({\forall}I)*]{\forall x.P}{P} &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    36
  \infer[({\forall}E)]{P[t/x]}{\forall x.P} \\[3ex]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    37
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    38
  \infer[({\exists}I)]{\exists x.P}{P[t/x]} &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    39
  \infer[({\exists}E)*]{Q}{{\exists x.P} & \infer*{Q}{[P]} } \\[3ex]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    40
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    41
  {t=t} \,(refl)   &  \vcenter{\infer[(subst)]{P[u/x]}{t=u & P[t/x]}} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    42
\end{array} \)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    43
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    44
\bigskip\bigskip
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    45
*{\em Eigenvariable conditions\/}:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    46
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    47
$\forall I$: provided $x$ is not free in the assumptions
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    48
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    49
$\exists E$: provided $x$ is not free in $Q$ or any assumption except $P$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    50
\caption{Intuitionistic first-order logic} \label{fol-fig}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    51
\end{figure}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    52
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    53
\section{Formalizing logical syntax in Isabelle}\label{sec:logical-syntax}
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
    54
\index{first-order logic}
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
    55
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    56
Figure~\ref{fol-fig} presents intuitionistic first-order logic,
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    57
including equality.  Let us see how to formalize
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    58
this logic in Isabelle, illustrating the main features of Isabelle's
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    59
polymorphic meta-logic.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    60
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
    61
\index{lambda calc@$\lambda$-calculus} 
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
    62
Isabelle represents syntax using the simply typed $\lambda$-calculus.  We
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
    63
declare a type for each syntactic category of the logic.  We declare a
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
    64
constant for each symbol of the logic, giving each $n$-place operation an
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
    65
$n$-argument curried function type.  Most importantly,
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
    66
$\lambda$-abstraction represents variable binding in quantifiers.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    67
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
    68
\index{types!syntax of}\index{types!function}\index{*fun type} 
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
    69
\index{type constructors}
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
    70
Isabelle has \ML-style polymorphic types such as~$(\alpha)list$, where
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
    71
$list$ is a type constructor and $\alpha$ is a type variable; for example,
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    72
$(bool)list$ is the type of lists of booleans.  Function types have the
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
    73
form $(\sigma,\tau)fun$ or $\sigma\To\tau$, where $\sigma$ and $\tau$ are
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
    74
types.  Curried function types may be abbreviated:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    75
\[  \sigma@1\To (\cdots \sigma@n\To \tau\cdots)  \quad \hbox{as} \quad
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    76
[\sigma@1, \ldots, \sigma@n] \To \tau \]
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    77
 
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    78
\index{terms!syntax of} The syntax for terms is summarised below.
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    79
Note that there are two versions of function application syntax
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    80
available in Isabelle: either $t\,u$, which is the usual form for
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    81
higher-order languages, or $t(u)$, trying to look more like
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3106
diff changeset
    82
first-order.  The latter syntax is used throughout the manual.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    83
\[ 
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
    84
\index{lambda abs@$\lambda$-abstractions}\index{function applications}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    85
\begin{array}{ll}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    86
  t :: \tau   & \hbox{type constraint, on a term or bound variable} \\
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    87
  \lambda x.t   & \hbox{abstraction} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    88
  \lambda x@1\ldots x@n.t
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    89
        & \hbox{curried abstraction, $\lambda x@1. \ldots \lambda x@n.t$} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    90
  t(u)          & \hbox{application} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    91
  t (u@1, \ldots, u@n) & \hbox{curried application, $t(u@1)\ldots(u@n)$} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    92
\end{array}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    93
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    94
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    95
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    96
\subsection{Simple types and constants}\index{types!simple|bold} 
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    97
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    98
The syntactic categories of our logic (Fig.\ts\ref{fol-fig}) are {\bf
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    99
  formulae} and {\bf terms}.  Formulae denote truth values, so (following
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   100
tradition) let us call their type~$o$.  To allow~0 and~$Suc(t)$ as terms,
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   101
let us declare a type~$nat$ of natural numbers.  Later, we shall see
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   102
how to admit terms of other types.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   103
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   104
\index{constants}\index{*nat type}\index{*o type}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   105
After declaring the types~$o$ and~$nat$, we may declare constants for the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   106
symbols of our logic.  Since $\bot$ denotes a truth value (falsity) and 0
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   107
denotes a number, we put \begin{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   108
  \bot  & :: & o \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   109
  0     & :: & nat.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   110
\end{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   111
If a symbol requires operands, the corresponding constant must have a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   112
function type.  In our logic, the successor function
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   113
($Suc$) is from natural numbers to natural numbers, negation ($\neg$) is a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   114
function from truth values to truth values, and the binary connectives are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   115
curried functions taking two truth values as arguments: 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   116
\begin{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   117
  Suc    & :: & nat\To nat  \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   118
  {\neg} & :: & o\To o      \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   119
  \conj,\disj,\imp,\bimp  & :: & [o,o]\To o 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   120
\end{eqnarray*}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   121
The binary connectives can be declared as infixes, with appropriate
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   122
precedences, so that we write $P\conj Q\disj R$ instead of
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   123
$\disj(\conj(P,Q), R)$.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   124
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   125
Section~\ref{sec:defining-theories} below describes the syntax of Isabelle
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   126
theory files and illustrates it by extending our logic with mathematical
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   127
induction.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   128
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   129
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   130
\subsection{Polymorphic types and constants} \label{polymorphic}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   131
\index{types!polymorphic|bold}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   132
\index{equality!polymorphic}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   133
\index{constants!polymorphic}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   134
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   135
Which type should we assign to the equality symbol?  If we tried
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   136
$[nat,nat]\To o$, then equality would be restricted to the natural
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   137
numbers; we should have to declare different equality symbols for each
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   138
type.  Isabelle's type system is polymorphic, so we could declare
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   139
\begin{eqnarray*}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   140
  {=}  & :: & [\alpha,\alpha]\To o,
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   141
\end{eqnarray*}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   142
where the type variable~$\alpha$ ranges over all types.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   143
But this is also wrong.  The declaration is too polymorphic; $\alpha$
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   144
includes types like~$o$ and $nat\To nat$.  Thus, it admits
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   145
$\bot=\neg(\bot)$ and $Suc=Suc$ as formulae, which is acceptable in
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   146
higher-order logic but not in first-order logic.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   147
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   148
Isabelle's {\bf type classes}\index{classes} control
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   149
polymorphism~\cite{nipkow-prehofer}.  Each type variable belongs to a
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   150
class, which denotes a set of types.  Classes are partially ordered by the
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   151
subclass relation, which is essentially the subset relation on the sets of
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   152
types.  They closely resemble the classes of the functional language
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   153
Haskell~\cite{haskell-tutorial,haskell-report}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   154
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   155
\index{*logic class}\index{*term class}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   156
Isabelle provides the built-in class $logic$, which consists of the logical
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   157
types: the ones we want to reason about.  Let us declare a class $term$, to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   158
consist of all legal types of terms in our logic.  The subclass structure
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   159
is now $term\le logic$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   160
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   161
\index{*nat type}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   162
We put $nat$ in class $term$ by declaring $nat{::}term$.  We declare the
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   163
equality constant by
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   164
\begin{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   165
  {=}  & :: & [\alpha{::}term,\alpha]\To o 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   166
\end{eqnarray*}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   167
where $\alpha{::}term$ constrains the type variable~$\alpha$ to class
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   168
$term$.  Such type variables resemble Standard~\ML's equality type
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   169
variables.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   170
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   171
We give~$o$ and function types the class $logic$ rather than~$term$, since
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   172
they are not legal types for terms.  We may introduce new types of class
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   173
$term$ --- for instance, type $string$ or $real$ --- at any time.  We can
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   174
even declare type constructors such as~$list$, and state that type
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   175
$(\tau)list$ belongs to class~$term$ provided $\tau$ does; equality
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   176
applies to lists of natural numbers but not to lists of formulae.  We may
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   177
summarize this paragraph by a set of {\bf arity declarations} for type
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   178
constructors:\index{arities!declaring}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   179
\begin{eqnarray*}\index{*o type}\index{*fun type}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   180
  o             & :: & logic \\
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   181
  fun           & :: & (logic,logic)logic \\
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   182
  nat, string, real     & :: & term \\
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   183
  list          & :: & (term)term
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   184
\end{eqnarray*}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   185
(Recall that $fun$ is the type constructor for function types.)
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   186
In \rmindex{higher-order logic}, equality does apply to truth values and
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   187
functions;  this requires the arity declarations ${o::term}$
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   188
and ${fun::(term,term)term}$.  The class system can also handle
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   189
overloading.\index{overloading|bold} We could declare $arith$ to be the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   190
subclass of $term$ consisting of the `arithmetic' types, such as~$nat$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   191
Then we could declare the operators
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   192
\begin{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   193
  {+},{-},{\times},{/}  & :: & [\alpha{::}arith,\alpha]\To \alpha
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   194
\end{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   195
If we declare new types $real$ and $complex$ of class $arith$, then we
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   196
in effect have three sets of operators:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   197
\begin{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   198
  {+},{-},{\times},{/}  & :: & [nat,nat]\To nat \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   199
  {+},{-},{\times},{/}  & :: & [real,real]\To real \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   200
  {+},{-},{\times},{/}  & :: & [complex,complex]\To complex 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   201
\end{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   202
Isabelle will regard these as distinct constants, each of which can be defined
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   203
separately.  We could even introduce the type $(\alpha)vector$ and declare
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   204
its arity as $(arith)arith$.  Then we could declare the constant
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   205
\begin{eqnarray*}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   206
  {+}  & :: & [(\alpha)vector,(\alpha)vector]\To (\alpha)vector 
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   207
\end{eqnarray*}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   208
and specify it in terms of ${+} :: [\alpha,\alpha]\To \alpha$.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   209
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   210
A type variable may belong to any finite number of classes.  Suppose that
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   211
we had declared yet another class $ord \le term$, the class of all
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   212
`ordered' types, and a constant
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   213
\begin{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   214
  {\le}  & :: & [\alpha{::}ord,\alpha]\To o.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   215
\end{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   216
In this context the variable $x$ in $x \le (x+x)$ will be assigned type
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   217
$\alpha{::}\{arith,ord\}$, which means $\alpha$ belongs to both $arith$ and
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   218
$ord$.  Semantically the set $\{arith,ord\}$ should be understood as the
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   219
intersection of the sets of types represented by $arith$ and $ord$.  Such
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   220
intersections of classes are called \bfindex{sorts}.  The empty
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   221
intersection of classes, $\{\}$, contains all types and is thus the {\bf
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   222
  universal sort}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   223
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   224
Even with overloading, each term has a unique, most general type.  For this
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   225
to be possible, the class and type declarations must satisfy certain
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   226
technical constraints; see 
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   227
\iflabelundefined{sec:ref-defining-theories}%
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   228
           {Sect.\ Defining Theories in the {\em Reference Manual}}%
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   229
           {\S\ref{sec:ref-defining-theories}}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   230
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   231
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   232
\subsection{Higher types and quantifiers}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   233
\index{types!higher|bold}\index{quantifiers}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   234
Quantifiers are regarded as operations upon functions.  Ignoring polymorphism
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   235
for the moment, consider the formula $\forall x. P(x)$, where $x$ ranges
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   236
over type~$nat$.  This is true if $P(x)$ is true for all~$x$.  Abstracting
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   237
$P(x)$ into a function, this is the same as saying that $\lambda x.P(x)$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   238
returns true for all arguments.  Thus, the universal quantifier can be
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   239
represented by a constant
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   240
\begin{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   241
  \forall  & :: & (nat\To o) \To o,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   242
\end{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   243
which is essentially an infinitary truth table.  The representation of $\forall
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   244
x. P(x)$ is $\forall(\lambda x. P(x))$.  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   245
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   246
The existential quantifier is treated
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   247
in the same way.  Other binding operators are also easily handled; for
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   248
instance, the summation operator $\Sigma@{k=i}^j f(k)$ can be represented as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   249
$\Sigma(i,j,\lambda k.f(k))$, where
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   250
\begin{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   251
  \Sigma  & :: & [nat,nat, nat\To nat] \To nat.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   252
\end{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   253
Quantifiers may be polymorphic.  We may define $\forall$ and~$\exists$ over
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   254
all legal types of terms, not just the natural numbers, and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   255
allow summations over all arithmetic types:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   256
\begin{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   257
   \forall,\exists      & :: & (\alpha{::}term\To o) \To o \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   258
   \Sigma               & :: & [nat,nat, nat\To \alpha{::}arith] \To \alpha
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   259
\end{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   260
Observe that the index variables still have type $nat$, while the values
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   261
being summed may belong to any arithmetic type.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   262
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   263
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   264
\section{Formalizing logical rules in Isabelle}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   265
\index{meta-implication|bold}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   266
\index{meta-quantifiers|bold}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   267
\index{meta-equality|bold}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   268
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   269
Object-logics are formalized by extending Isabelle's
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1865
diff changeset
   270
meta-logic~\cite{paulson-found}, which is intuitionistic higher-order logic.
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   271
The meta-level connectives are {\bf implication}, the {\bf universal
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   272
  quantifier}, and {\bf equality}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   273
\begin{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   274
  \item The implication \(\phi\Imp \psi\) means `\(\phi\) implies
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   275
\(\psi\)', and expresses logical {\bf entailment}.  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   276
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   277
  \item The quantification \(\Forall x.\phi\) means `\(\phi\) is true for
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   278
all $x$', and expresses {\bf generality} in rules and axiom schemes. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   279
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   280
\item The equality \(a\equiv b\) means `$a$ equals $b$', for expressing
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   281
  {\bf definitions} (see~\S\ref{definitions}).\index{definitions}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   282
  Equalities left over from the unification process, so called {\bf
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   283
    flex-flex constraints},\index{flex-flex constraints} are written $a\qeq
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   284
  b$.  The two equality symbols have the same logical meaning.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   285
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   286
\end{itemize}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   287
The syntax of the meta-logic is formalized in the same manner
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   288
as object-logics, using the simply typed $\lambda$-calculus.  Analogous to
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   289
type~$o$ above, there is a built-in type $prop$ of meta-level truth values.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   290
Meta-level formulae will have this type.  Type $prop$ belongs to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   291
class~$logic$; also, $\sigma\To\tau$ belongs to $logic$ provided $\sigma$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   292
and $\tau$ do.  Here are the types of the built-in connectives:
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   293
\begin{eqnarray*}\index{*prop type}\index{*logic class}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   294
  \Imp     & :: & [prop,prop]\To prop \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   295
  \Forall  & :: & (\alpha{::}logic\To prop) \To prop \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   296
  {\equiv} & :: & [\alpha{::}\{\},\alpha]\To prop \\
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   297
  \qeq & :: & [\alpha{::}\{\},\alpha]\To prop
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   298
\end{eqnarray*}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   299
The polymorphism in $\Forall$ is restricted to class~$logic$ to exclude
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   300
certain types, those used just for parsing.  The type variable
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   301
$\alpha{::}\{\}$ ranges over the universal sort.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   302
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   303
In our formalization of first-order logic, we declared a type~$o$ of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   304
object-level truth values, rather than using~$prop$ for this purpose.  If
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   305
we declared the object-level connectives to have types such as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   306
${\neg}::prop\To prop$, then these connectives would be applicable to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   307
meta-level formulae.  Keeping $prop$ and $o$ as separate types maintains
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   308
the distinction between the meta-level and the object-level.  To formalize
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   309
the inference rules, we shall need to relate the two levels; accordingly,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   310
we declare the constant
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   311
\index{*Trueprop constant}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   312
\begin{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   313
  Trueprop & :: & o\To prop.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   314
\end{eqnarray*}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   315
We may regard $Trueprop$ as a meta-level predicate, reading $Trueprop(P)$ as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   316
`$P$ is true at the object-level.'  Put another way, $Trueprop$ is a coercion
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   317
from $o$ to $prop$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   318
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   319
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   320
\subsection{Expressing propositional rules}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   321
\index{rules!propositional}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   322
We shall illustrate the use of the meta-logic by formalizing the rules of
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   323
Fig.\ts\ref{fol-fig}.  Each object-level rule is expressed as a meta-level
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   324
axiom. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   325
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   326
One of the simplest rules is $(\conj E1)$.  Making
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   327
everything explicit, its formalization in the meta-logic is
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   328
$$
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   329
\Forall P\;Q. Trueprop(P\conj Q) \Imp Trueprop(P).   \eqno(\conj E1)
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   330
$$
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   331
This may look formidable, but it has an obvious reading: for all object-level
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   332
truth values $P$ and~$Q$, if $P\conj Q$ is true then so is~$P$.  The
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   333
reading is correct because the meta-logic has simple models, where
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   334
types denote sets and $\Forall$ really means `for all.'
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   335
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   336
\index{*Trueprop constant}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   337
Isabelle adopts notational conventions to ease the writing of rules.  We may
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   338
hide the occurrences of $Trueprop$ by making it an implicit coercion.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   339
Outer universal quantifiers may be dropped.  Finally, the nested implication
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   340
\index{meta-implication}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   341
\[  \phi@1\Imp(\cdots \phi@n\Imp\psi\cdots) \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   342
may be abbreviated as $\List{\phi@1; \ldots; \phi@n} \Imp \psi$, which
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   343
formalizes a rule of $n$~premises.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   344
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   345
Using these conventions, the conjunction rules become the following axioms.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   346
These fully specify the properties of~$\conj$:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   347
$$ \List{P; Q} \Imp P\conj Q                 \eqno(\conj I) $$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   348
$$ P\conj Q \Imp P  \qquad  P\conj Q \Imp Q  \eqno(\conj E1,2) $$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   349
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   350
\noindent
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   351
Next, consider the disjunction rules.  The discharge of assumption in
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   352
$(\disj E)$ is expressed  using $\Imp$:
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   353
\index{assumptions!discharge of}%
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   354
$$ P \Imp P\disj Q  \qquad  Q \Imp P\disj Q  \eqno(\disj I1,2) $$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   355
$$ \List{P\disj Q; P\Imp R; Q\Imp R} \Imp R  \eqno(\disj E) $$
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   356
%
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   357
To understand this treatment of assumptions in natural
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   358
deduction, look at implication.  The rule $({\imp}I)$ is the classic
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   359
example of natural deduction: to prove that $P\imp Q$ is true, assume $P$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   360
is true and show that $Q$ must then be true.  More concisely, if $P$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   361
implies $Q$ (at the meta-level), then $P\imp Q$ is true (at the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   362
object-level).  Showing the coercion explicitly, this is formalized as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   363
\[ (Trueprop(P)\Imp Trueprop(Q)) \Imp Trueprop(P\imp Q). \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   364
The rule $({\imp}E)$ is straightforward; hiding $Trueprop$, the axioms to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   365
specify $\imp$ are 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   366
$$ (P \Imp Q)  \Imp  P\imp Q   \eqno({\imp}I) $$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   367
$$ \List{P\imp Q; P}  \Imp Q.  \eqno({\imp}E) $$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   368
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   369
\noindent
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   370
Finally, the intuitionistic contradiction rule is formalized as the axiom
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   371
$$ \bot \Imp P.   \eqno(\bot E) $$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   372
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   373
\begin{warn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   374
Earlier versions of Isabelle, and certain
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1865
diff changeset
   375
papers~\cite{paulson-found,paulson700}, use $\List{P}$ to mean $Trueprop(P)$.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   376
\end{warn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   377
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   378
\subsection{Quantifier rules and substitution}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   379
\index{quantifiers}\index{rules!quantifier}\index{substitution|bold}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   380
\index{variables!bound}\index{lambda abs@$\lambda$-abstractions}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   381
\index{function applications}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   382
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   383
Isabelle expresses variable binding using $\lambda$-abstraction; for instance,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   384
$\forall x.P$ is formalized as $\forall(\lambda x.P)$.  Recall that $F(t)$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   385
is Isabelle's syntax for application of the function~$F$ to the argument~$t$;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   386
it is not a meta-notation for substitution.  On the other hand, a substitution
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   387
will take place if $F$ has the form $\lambda x.P$;  Isabelle transforms
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   388
$(\lambda x.P)(t)$ to~$P[t/x]$ by $\beta$-conversion.  Thus, we can express
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   389
inference rules that involve substitution for bound variables.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   390
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   391
\index{parameters|bold}\index{eigenvariables|see{parameters}}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   392
A logic may attach provisos to certain of its rules, especially quantifier
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   393
rules.  We cannot hope to formalize arbitrary provisos.  Fortunately, those
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   394
typical of quantifier rules always have the same form, namely `$x$ not free in
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   395
\ldots {\it (some set of formulae)},' where $x$ is a variable (called a {\bf
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   396
parameter} or {\bf eigenvariable}) in some premise.  Isabelle treats
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   397
provisos using~$\Forall$, its inbuilt notion of `for all'.
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   398
\index{meta-quantifiers}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   399
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   400
The purpose of the proviso `$x$ not free in \ldots' is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   401
to ensure that the premise may not make assumptions about the value of~$x$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   402
and therefore holds for all~$x$.  We formalize $(\forall I)$ by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   403
\[ \left(\Forall x. Trueprop(P(x))\right) \Imp Trueprop(\forall x.P(x)). \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   404
This means, `if $P(x)$ is true for all~$x$, then $\forall x.P(x)$ is true.'
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   405
The $\forall E$ rule exploits $\beta$-conversion.  Hiding $Trueprop$, the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   406
$\forall$ axioms are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   407
$$ \left(\Forall x. P(x)\right)  \Imp  \forall x.P(x)   \eqno(\forall I) $$
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   408
$$ (\forall x.P(x))  \Imp P(t).  \eqno(\forall E) $$
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   409
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   410
\noindent
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   411
We have defined the object-level universal quantifier~($\forall$)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   412
using~$\Forall$.  But we do not require meta-level counterparts of all the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   413
connectives of the object-logic!  Consider the existential quantifier: 
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   414
$$ P(t)  \Imp  \exists x.P(x)  \eqno(\exists I) $$
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   415
$$ \List{\exists x.P(x);\; \Forall x. P(x)\Imp Q} \Imp Q  \eqno(\exists E) $$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   416
Let us verify $(\exists E)$ semantically.  Suppose that the premises
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   417
hold; since $\exists x.P(x)$ is true, we may choose an~$a$ such that $P(a)$ is
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   418
true.  Instantiating $\Forall x. P(x)\Imp Q$ with $a$ yields $P(a)\Imp Q$, and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   419
we obtain the desired conclusion, $Q$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   420
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   421
The treatment of substitution deserves mention.  The rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   422
\[ \infer{P[u/t]}{t=u & P} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   423
would be hard to formalize in Isabelle.  It calls for replacing~$t$ by $u$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   424
throughout~$P$, which cannot be expressed using $\beta$-conversion.  Our
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   425
rule~$(subst)$ uses~$P$ as a template for substitution, inferring $P[u/x]$
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   426
from~$P[t/x]$.  When we formalize this as an axiom, the template becomes a
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   427
function variable:
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   428
$$ \List{t=u; P(t)} \Imp P(u).  \eqno(subst) $$
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   429
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   430
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   431
\subsection{Signatures and theories}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   432
\index{signatures|bold}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   433
6170
9a59cf8ae9b5 standard spelling: type-checking
paulson
parents: 3485
diff changeset
   434
A {\bf signature} contains the information necessary for type-checking,
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   435
parsing and pretty printing a term.  It specifies type classes and their
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   436
relationships, types and their arities, constants and their types, etc.  It
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   437
also contains grammar rules, specified using mixfix declarations.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   438
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   439
Two signatures can be merged provided their specifications are compatible ---
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   440
they must not, for example, assign different types to the same constant.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   441
Under similar conditions, a signature can be extended.  Signatures are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   442
managed internally by Isabelle; users seldom encounter them.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   443
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   444
\index{theories|bold} A {\bf theory} consists of a signature plus a collection
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   445
of axioms.  The Pure theory contains only the meta-logic.  Theories can be
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   446
combined provided their signatures are compatible.  A theory definition
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   447
extends an existing theory with further signature specifications --- classes,
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   448
types, constants and mixfix declarations --- plus lists of axioms and
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   449
definitions etc., expressed as strings to be parsed.  A theory can formalize a
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   450
small piece of mathematics, such as lists and their operations, or an entire
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   451
logic.  A mathematical development typically involves many theories in a
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   452
hierarchy.  For example, the Pure theory could be extended to form a theory
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   453
for Fig.\ts\ref{fol-fig}; this could be extended in two separate ways to form
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   454
a theory for natural numbers and a theory for lists; the union of these two
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6592
diff changeset
   455
could be extended into a theory defining the length of a list:
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   456
\begin{tt}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   457
\[
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   458
\begin{array}{c@{}c@{}c@{}c@{}c}
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   459
     {}   &     {}   &\hbox{Pure}&     {}  &     {}  \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   460
     {}   &     {}   &  \downarrow &     {}   &     {}   \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   461
     {}   &     {}   &\hbox{FOL} &     {}   &     {}   \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   462
     {}   & \swarrow &     {}    & \searrow &     {}   \\
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   463
 \hbox{Nat} &   {}   &     {}    &     {}   & \hbox{List} \\
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   464
     {}   & \searrow &     {}    & \swarrow &     {}   \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   465
     {}   &     {} &\hbox{Nat}+\hbox{List}&  {}   &     {}   \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   466
     {}   &     {}   &  \downarrow &     {}   &     {}   \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   467
     {}   &     {} & \hbox{Length} &  {}   &     {}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   468
\end{array}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   469
\]
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   470
\end{tt}%
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   471
Each Isabelle proof typically works within a single theory, which is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   472
associated with the proof state.  However, many different theories may
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   473
coexist at the same time, and you may work in each of these during a single
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   474
session.  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   475
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   476
\begin{warn}\index{constants!clashes with variables}%
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   477
  Confusing problems arise if you work in the wrong theory.  Each theory
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   478
  defines its own syntax.  An identifier may be regarded in one theory as a
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   479
  constant and in another as a variable, for example.
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   480
\end{warn}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   481
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   482
\section{Proof construction in Isabelle}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   483
I have elsewhere described the meta-logic and demonstrated it by
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1865
diff changeset
   484
formalizing first-order logic~\cite{paulson-found}.  There is a one-to-one
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   485
correspondence between meta-level proofs and object-level proofs.  To each
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   486
use of a meta-level axiom, such as $(\forall I)$, there is a use of the
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   487
corresponding object-level rule.  Object-level assumptions and parameters
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   488
have meta-level counterparts.  The meta-level formalization is {\bf
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   489
  faithful}, admitting no incorrect object-level inferences, and {\bf
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   490
  adequate}, admitting all correct object-level inferences.  These
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   491
properties must be demonstrated separately for each object-logic.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   492
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   493
The meta-logic is defined by a collection of inference rules, including
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   494
equational rules for the $\lambda$-calculus and logical rules.  The rules
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   495
for~$\Imp$ and~$\Forall$ resemble those for~$\imp$ and~$\forall$ in
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   496
Fig.\ts\ref{fol-fig}.  Proofs performed using the primitive meta-rules
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   497
would be lengthy; Isabelle proofs normally use certain derived rules.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   498
{\bf Resolution}, in particular, is convenient for backward proof.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   499
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   500
Unification is central to theorem proving.  It supports quantifier
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   501
reasoning by allowing certain `unknown' terms to be instantiated later,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   502
possibly in stages.  When proving that the time required to sort $n$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   503
integers is proportional to~$n^2$, we need not state the constant of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   504
proportionality; when proving that a hardware adder will deliver the sum of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   505
its inputs, we need not state how many clock ticks will be required.  Such
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   506
quantities often emerge from the proof.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   507
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   508
Isabelle provides {\bf schematic variables}, or {\bf
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   509
  unknowns},\index{unknowns} for unification.  Logically, unknowns are free
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   510
variables.  But while ordinary variables remain fixed, unification may
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   511
instantiate unknowns.  Unknowns are written with a ?\ prefix and are
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   512
frequently subscripted: $\Var{a}$, $\Var{a@1}$, $\Var{a@2}$, \ldots,
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   513
$\Var{P}$, $\Var{P@1}$, \ldots.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   514
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   515
Recall that an inference rule of the form
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   516
\[ \infer{\phi}{\phi@1 & \ldots & \phi@n} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   517
is formalized in Isabelle's meta-logic as the axiom
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   518
$\List{\phi@1; \ldots; \phi@n} \Imp \phi$.\index{resolution}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   519
Such axioms resemble Prolog's Horn clauses, and can be combined by
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   520
resolution --- Isabelle's principal proof method.  Resolution yields both
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   521
forward and backward proof.  Backward proof works by unifying a goal with
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   522
the conclusion of a rule, whose premises become new subgoals.  Forward proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   523
works by unifying theorems with the premises of a rule, deriving a new theorem.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   524
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   525
Isabelle formulae require an extended notion of resolution.
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   526
They differ from Horn clauses in two major respects:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   527
\begin{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   528
  \item They are written in the typed $\lambda$-calculus, and therefore must be
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   529
resolved using higher-order unification.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   530
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   531
\item The constituents of a clause need not be atomic formulae.  Any
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   532
  formula of the form $Trueprop(\cdots)$ is atomic, but axioms such as
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   533
  ${\imp}I$ and $\forall I$ contain non-atomic formulae.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   534
\end{itemize}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   535
Isabelle has little in common with classical resolution theorem provers
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   536
such as Otter~\cite{wos-bledsoe}.  At the meta-level, Isabelle proves
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   537
theorems in their positive form, not by refutation.  However, an
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   538
object-logic that includes a contradiction rule may employ a refutation
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   539
proof procedure.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   540
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   541
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   542
\subsection{Higher-order unification}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   543
\index{unification!higher-order|bold}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   544
Unification is equation solving.  The solution of $f(\Var{x},c) \qeq
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   545
f(d,\Var{y})$ is $\Var{x}\equiv d$ and $\Var{y}\equiv c$.  {\bf
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   546
Higher-order unification} is equation solving for typed $\lambda$-terms.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   547
To handle $\beta$-conversion, it must reduce $(\lambda x.t)u$ to $t[u/x]$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   548
That is easy --- in the typed $\lambda$-calculus, all reduction sequences
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   549
terminate at a normal form.  But it must guess the unknown
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   550
function~$\Var{f}$ in order to solve the equation
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   551
\begin{equation} \label{hou-eqn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   552
 \Var{f}(t) \qeq g(u@1,\ldots,u@k).
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   553
\end{equation}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   554
Huet's~\cite{huet75} search procedure solves equations by imitation and
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   555
projection.  {\bf Imitation} makes~$\Var{f}$ apply the leading symbol (if a
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   556
constant) of the right-hand side.  To solve equation~(\ref{hou-eqn}), it
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   557
guesses
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   558
\[ \Var{f} \equiv \lambda x. g(\Var{h@1}(x),\ldots,\Var{h@k}(x)), \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   559
where $\Var{h@1}$, \ldots, $\Var{h@k}$ are new unknowns.  Assuming there are no
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   560
other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   561
set of equations
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   562
\[ \Var{h@1}(t)\qeq u@1 \quad\ldots\quad \Var{h@k}(t)\qeq u@k. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   563
If the procedure solves these equations, instantiating $\Var{h@1}$, \ldots,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   564
$\Var{h@k}$, then it yields an instantiation for~$\Var{f}$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   565
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   566
{\bf Projection} makes $\Var{f}$ apply one of its arguments.  To solve
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   567
equation~(\ref{hou-eqn}), if $t$ expects~$m$ arguments and delivers a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   568
result of suitable type, it guesses
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   569
\[ \Var{f} \equiv \lambda x. x(\Var{h@1}(x),\ldots,\Var{h@m}(x)), \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   570
where $\Var{h@1}$, \ldots, $\Var{h@m}$ are new unknowns.  Assuming there are no
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   571
other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   572
equation 
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   573
\[ t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k). \]
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   574
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   575
\begin{warn}\index{unification!incompleteness of}%
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   576
Huet's unification procedure is complete.  Isabelle's polymorphic version,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   577
which solves for type unknowns as well as for term unknowns, is incomplete.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   578
The problem is that projection requires type information.  In
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   579
equation~(\ref{hou-eqn}), if the type of~$t$ is unknown, then projections
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   580
are possible for all~$m\geq0$, and the types of the $\Var{h@i}$ will be
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   581
similarly unconstrained.  Therefore, Isabelle never attempts such
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   582
projections, and may fail to find unifiers where a type unknown turns out
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   583
to be a function type.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   584
\end{warn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   585
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   586
\index{unknowns!function|bold}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   587
Given $\Var{f}(t@1,\ldots,t@n)\qeq u$, Huet's procedure could make up to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   588
$n+1$ guesses.  The search tree and set of unifiers may be infinite.  But
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   589
higher-order unification can work effectively, provided you are careful
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   590
with {\bf function unknowns}:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   591
\begin{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   592
  \item Equations with no function unknowns are solved using first-order
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   593
unification, extended to treat bound variables.  For example, $\lambda x.x
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   594
\qeq \lambda x.\Var{y}$ has no solution because $\Var{y}\equiv x$ would
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   595
capture the free variable~$x$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   596
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   597
  \item An occurrence of the term $\Var{f}(x,y,z)$, where the arguments are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   598
distinct bound variables, causes no difficulties.  Its projections can only
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   599
match the corresponding variables.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   600
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   601
  \item Even an equation such as $\Var{f}(a)\qeq a+a$ is all right.  It has
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   602
four solutions, but Isabelle evaluates them lazily, trying projection before
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3106
diff changeset
   603
imitation.  The first solution is usually the one desired:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   604
\[ \Var{f}\equiv \lambda x. x+x \quad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   605
   \Var{f}\equiv \lambda x. a+x \quad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   606
   \Var{f}\equiv \lambda x. x+a \quad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   607
   \Var{f}\equiv \lambda x. a+a \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   608
  \item  Equations such as $\Var{f}(\Var{x},\Var{y})\qeq t$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   609
$\Var{f}(\Var{g}(x))\qeq t$ admit vast numbers of unifiers, and must be
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   610
avoided. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   611
\end{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   612
In problematic cases, you may have to instantiate some unknowns before
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   613
invoking unification. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   614
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   615
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   616
\subsection{Joining rules by resolution} \label{joining}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   617
\index{resolution|bold}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   618
Let $\List{\psi@1; \ldots; \psi@m} \Imp \psi$ and $\List{\phi@1; \ldots;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   619
\phi@n} \Imp \phi$ be two Isabelle theorems, representing object-level rules. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   620
Choosing some~$i$ from~1 to~$n$, suppose that $\psi$ and $\phi@i$ have a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   621
higher-order unifier.  Writing $Xs$ for the application of substitution~$s$ to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   622
expression~$X$, this means there is some~$s$ such that $\psi s\equiv \phi@i s$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   623
By resolution, we may conclude
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   624
\[ (\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   625
          \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   626
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   627
The substitution~$s$ may instantiate unknowns in both rules.  In short,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   628
resolution is the following rule:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   629
\[ \infer[(\psi s\equiv \phi@i s)]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   630
         {(\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   631
          \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   632
         {\List{\psi@1; \ldots; \psi@m} \Imp \psi & &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   633
          \List{\phi@1; \ldots; \phi@n} \Imp \phi}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   634
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   635
It operates at the meta-level, on Isabelle theorems, and is justified by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   636
the properties of $\Imp$ and~$\Forall$.  It takes the number~$i$ (for
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   637
$1\leq i\leq n$) as a parameter and may yield infinitely many conclusions,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   638
one for each unifier of $\psi$ with $\phi@i$.  Isabelle returns these
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   639
conclusions as a sequence (lazy list).
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   640
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   641
Resolution expects the rules to have no outer quantifiers~($\Forall$).
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   642
It may rename or instantiate any schematic variables, but leaves free
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   643
variables unchanged.  When constructing a theory, Isabelle puts the
3106
wenzelm
parents: 3103
diff changeset
   644
rules into a standard form with all free variables converted into
wenzelm
parents: 3103
diff changeset
   645
schematic ones; for instance, $({\imp}E)$ becomes
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   646
\[ \List{\Var{P}\imp \Var{Q}; \Var{P}}  \Imp \Var{Q}. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   647
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   648
When resolving two rules, the unknowns in the first rule are renamed, by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   649
subscripting, to make them distinct from the unknowns in the second rule.  To
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   650
resolve $({\imp}E)$ with itself, the first copy of the rule becomes
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   651
\[ \List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}}  \Imp \Var{Q@1}. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   652
Resolving this with $({\imp}E)$ in the first premise, unifying $\Var{Q@1}$ with
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   653
$\Var{P}\imp \Var{Q}$, is the meta-level inference
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   654
\[ \infer{\List{\Var{P@1}\imp (\Var{P}\imp \Var{Q}); \Var{P@1}; \Var{P}} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   655
           \Imp\Var{Q}.}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   656
         {\List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}}  \Imp \Var{Q@1} & &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   657
          \List{\Var{P}\imp \Var{Q}; \Var{P}}  \Imp \Var{Q}}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   658
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   659
Renaming the unknowns in the resolvent, we have derived the
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   660
object-level rule\index{rules!derived}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   661
\[ \infer{Q.}{R\imp (P\imp Q)  &  R  &  P}  \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   662
Joining rules in this fashion is a simple way of proving theorems.  The
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   663
derived rules are conservative extensions of the object-logic, and may permit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   664
simpler proofs.  Let us consider another example.  Suppose we have the axiom
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   665
$$ \forall x\,y. Suc(x)=Suc(y)\imp x=y. \eqno (inject) $$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   666
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   667
\noindent 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   668
The standard form of $(\forall E)$ is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   669
$\forall x.\Var{P}(x)  \Imp \Var{P}(\Var{t})$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   670
Resolving $(inject)$ with $(\forall E)$ replaces $\Var{P}$ by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   671
$\lambda x. \forall y. Suc(x)=Suc(y)\imp x=y$ and leaves $\Var{t}$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   672
unchanged, yielding  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   673
\[ \forall y. Suc(\Var{t})=Suc(y)\imp \Var{t}=y. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   674
Resolving this with $(\forall E)$ puts a subscript on~$\Var{t}$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   675
and yields
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   676
\[ Suc(\Var{t@1})=Suc(\Var{t})\imp \Var{t@1}=\Var{t}. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   677
Resolving this with $({\imp}E)$ increases the subscripts and yields
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   678
\[ Suc(\Var{t@2})=Suc(\Var{t@1})\Imp \Var{t@2}=\Var{t@1}. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   679
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   680
We have derived the rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   681
\[ \infer{m=n,}{Suc(m)=Suc(n)} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   682
which goes directly from $Suc(m)=Suc(n)$ to $m=n$.  It is handy for simplifying
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   683
an equation like $Suc(Suc(Suc(m)))=Suc(Suc(Suc(0)))$.  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   684
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   685
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   686
\section{Lifting a rule into a context}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   687
The rules $({\imp}I)$ and $(\forall I)$ may seem unsuitable for
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   688
resolution.  They have non-atomic premises, namely $P\Imp Q$ and $\Forall
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   689
x.P(x)$, while the conclusions of all the rules are atomic (they have the form
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   690
$Trueprop(\cdots)$).  Isabelle gets round the problem through a meta-inference
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   691
called \bfindex{lifting}.  Let us consider how to construct proofs such as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   692
\[ \infer[({\imp}I)]{P\imp(Q\imp R)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   693
         {\infer[({\imp}I)]{Q\imp R}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   694
                        {\infer*{R}{[P,Q]}}}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   695
   \qquad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   696
   \infer[(\forall I)]{\forall x\,y.P(x,y)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   697
         {\infer[(\forall I)]{\forall y.P(x,y)}{P(x,y)}}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   698
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   699
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   700
\subsection{Lifting over assumptions}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   701
\index{assumptions!lifting over}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   702
Lifting over $\theta\Imp{}$ is the following meta-inference rule:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   703
\[ \infer{\List{\theta\Imp\phi@1; \ldots; \theta\Imp\phi@n} \Imp
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   704
          (\theta \Imp \phi)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   705
         {\List{\phi@1; \ldots; \phi@n} \Imp \phi} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   706
This is clearly sound: if $\List{\phi@1; \ldots; \phi@n} \Imp \phi$ is true and
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   707
$\theta\Imp\phi@1$, \ldots, $\theta\Imp\phi@n$ and $\theta$ are all true then
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   708
$\phi$ must be true.  Iterated lifting over a series of meta-formulae
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   709
$\theta@k$, \ldots, $\theta@1$ yields an object-rule whose conclusion is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   710
$\List{\theta@1; \ldots; \theta@k} \Imp \phi$.  Typically the $\theta@i$ are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   711
the assumptions in a natural deduction proof; lifting copies them into a rule's
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   712
premises and conclusion.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   713
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   714
When resolving two rules, Isabelle lifts the first one if necessary.  The
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   715
standard form of $({\imp}I)$ is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   716
\[ (\Var{P} \Imp \Var{Q})  \Imp  \Var{P}\imp \Var{Q}.   \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   717
To resolve this rule with itself, Isabelle modifies one copy as follows: it
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   718
renames the unknowns to $\Var{P@1}$ and $\Var{Q@1}$, then lifts the rule over
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   719
$\Var{P}\Imp{}$ to obtain
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   720
\[ (\Var{P}\Imp (\Var{P@1} \Imp \Var{Q@1})) \Imp (\Var{P} \Imp 
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   721
   (\Var{P@1}\imp \Var{Q@1})).   \]
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   722
Using the $\List{\cdots}$ abbreviation, this can be written as
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   723
\[ \List{\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}; \Var{P}} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   724
   \Imp  \Var{P@1}\imp \Var{Q@1}.   \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   725
Unifying $\Var{P}\Imp \Var{P@1}\imp\Var{Q@1}$ with $\Var{P} \Imp
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   726
\Var{Q}$ instantiates $\Var{Q}$ to ${\Var{P@1}\imp\Var{Q@1}}$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   727
Resolution yields
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   728
\[ (\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}) \Imp
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   729
\Var{P}\imp(\Var{P@1}\imp\Var{Q@1}).   \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   730
This represents the derived rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   731
\[ \infer{P\imp(Q\imp R).}{\infer*{R}{[P,Q]}} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   732
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   733
\subsection{Lifting over parameters}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   734
\index{parameters!lifting over}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   735
An analogous form of lifting handles premises of the form $\Forall x\ldots\,$. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   736
Here, lifting prefixes an object-rule's premises and conclusion with $\Forall
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   737
x$.  At the same time, lifting introduces a dependence upon~$x$.  It replaces
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   738
each unknown $\Var{a}$ in the rule by $\Var{a'}(x)$, where $\Var{a'}$ is a new
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   739
unknown (by subscripting) of suitable type --- necessarily a function type.  In
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   740
short, lifting is the meta-inference
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   741
\[ \infer{\List{\Forall x.\phi@1^x; \ldots; \Forall x.\phi@n^x} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   742
           \Imp \Forall x.\phi^x,}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   743
         {\List{\phi@1; \ldots; \phi@n} \Imp \phi} \]
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   744
%
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   745
where $\phi^x$ stands for the result of lifting unknowns over~$x$ in
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   746
$\phi$.  It is not hard to verify that this meta-inference is sound.  If
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   747
$\phi\Imp\psi$ then $\phi^x\Imp\psi^x$ for all~$x$; so if $\phi^x$ is true
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   748
for all~$x$ then so is $\psi^x$.  Thus, from $\phi\Imp\psi$ we conclude
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   749
$(\Forall x.\phi^x) \Imp (\Forall x.\psi^x)$.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   750
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   751
For example, $(\disj I)$ might be lifted to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   752
\[ (\Forall x.\Var{P@1}(x)) \Imp (\Forall x. \Var{P@1}(x)\disj \Var{Q@1}(x))\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   753
and $(\forall I)$ to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   754
\[ (\Forall x\,y.\Var{P@1}(x,y)) \Imp (\Forall x. \forall y.\Var{P@1}(x,y)). \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   755
Isabelle has renamed a bound variable in $(\forall I)$ from $x$ to~$y$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   756
avoiding a clash.  Resolving the above with $(\forall I)$ is the meta-inference
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   757
\[ \infer{\Forall x\,y.\Var{P@1}(x,y)) \Imp \forall x\,y.\Var{P@1}(x,y)) }
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   758
         {(\Forall x\,y.\Var{P@1}(x,y)) \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   759
               (\Forall x. \forall y.\Var{P@1}(x,y))  &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   760
          (\Forall x.\Var{P}(x)) \Imp (\forall x.\Var{P}(x))} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   761
Here, $\Var{P}$ is replaced by $\lambda x.\forall y.\Var{P@1}(x,y)$; the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   762
resolvent expresses the derived rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   763
\[ \vcenter{ \infer{\forall x\,y.Q(x,y)}{Q(x,y)} }
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   764
   \quad\hbox{provided $x$, $y$ not free in the assumptions} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   765
\] 
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1865
diff changeset
   766
I discuss lifting and parameters at length elsewhere~\cite{paulson-found}.
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   767
Miller goes into even greater detail~\cite{miller-mixed}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   768
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   769
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   770
\section{Backward proof by resolution}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   771
\index{resolution!in backward proof}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   772
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   773
Resolution is convenient for deriving simple rules and for reasoning
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   774
forward from facts.  It can also support backward proof, where we start
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   775
with a goal and refine it to progressively simpler subgoals until all have
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   776
been solved.  {\sc lcf} and its descendants {\sc hol} and Nuprl provide
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   777
tactics and tacticals, which constitute a sophisticated language for
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   778
expressing proof searches.  {\bf Tactics} refine subgoals while {\bf
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   779
  tacticals} combine tactics.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   780
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   781
\index{LCF system}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   782
Isabelle's tactics and tacticals work differently from {\sc lcf}'s.  An
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   783
Isabelle rule is bidirectional: there is no distinction between
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   784
inputs and outputs.  {\sc lcf} has a separate tactic for each rule;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   785
Isabelle performs refinement by any rule in a uniform fashion, using
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   786
resolution.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   787
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   788
Isabelle works with meta-level theorems of the form
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   789
\( \List{\phi@1; \ldots; \phi@n} \Imp \phi \).
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   790
We have viewed this as the {\bf rule} with premises
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   791
$\phi@1$,~\ldots,~$\phi@n$ and conclusion~$\phi$.  It can also be viewed as
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   792
the {\bf proof state}\index{proof state}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   793
with subgoals $\phi@1$,~\ldots,~$\phi@n$ and main
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   794
goal~$\phi$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   795
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   796
To prove the formula~$\phi$, take $\phi\Imp \phi$ as the initial proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   797
state.  This assertion is, trivially, a theorem.  At a later stage in the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   798
backward proof, a typical proof state is $\List{\phi@1; \ldots; \phi@n}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   799
\Imp \phi$.  This proof state is a theorem, ensuring that the subgoals
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   800
$\phi@1$,~\ldots,~$\phi@n$ imply~$\phi$.  If $n=0$ then we have
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   801
proved~$\phi$ outright.  If $\phi$ contains unknowns, they may become
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   802
instantiated during the proof; a proof state may be $\List{\phi@1; \ldots;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   803
\phi@n} \Imp \phi'$, where $\phi'$ is an instance of~$\phi$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   804
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   805
\subsection{Refinement by resolution}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   806
To refine subgoal~$i$ of a proof state by a rule, perform the following
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   807
resolution: 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   808
\[ \infer{\hbox{new proof state}}{\hbox{rule} & & \hbox{proof state}} \]
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   809
Suppose the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   810
lifting over subgoal~$i$'s assumptions and parameters.  If the proof state
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   811
is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, then the new proof state is
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   812
(for~$1\leq i\leq n$)
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   813
\[ (\List{\phi@1; \ldots; \phi@{i-1}; \psi'@1;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   814
          \ldots; \psi'@m; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.  \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   815
Substitution~$s$ unifies $\psi'$ with~$\phi@i$.  In the proof state,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   816
subgoal~$i$ is replaced by $m$ new subgoals, the rule's instantiated premises.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   817
If some of the rule's unknowns are left un-instantiated, they become new
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   818
unknowns in the proof state.  Refinement by~$(\exists I)$, namely
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   819
\[ \Var{P}(\Var{t}) \Imp \exists x. \Var{P}(x), \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   820
inserts a new unknown derived from~$\Var{t}$ by subscripting and lifting.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   821
We do not have to specify an `existential witness' when
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   822
applying~$(\exists I)$.  Further resolutions may instantiate unknowns in
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   823
the proof state.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   824
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   825
\subsection{Proof by assumption}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   826
\index{assumptions!use of}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   827
In the course of a natural deduction proof, parameters $x@1$, \ldots,~$x@l$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   828
assumptions $\theta@1$, \ldots, $\theta@k$ accumulate, forming a context for
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   829
each subgoal.  Repeated lifting steps can lift a rule into any context.  To
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   830
aid readability, Isabelle puts contexts into a normal form, gathering the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   831
parameters at the front:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   832
\begin{equation} \label{context-eqn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   833
\Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   834
\end{equation}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   835
Under the usual reading of the connectives, this expresses that $\theta$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   836
follows from $\theta@1$,~\ldots~$\theta@k$ for arbitrary
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   837
$x@1$,~\ldots,~$x@l$.  It is trivially true if $\theta$ equals any of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   838
$\theta@1$,~\ldots~$\theta@k$, or is unifiable with any of them.  This
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   839
models proof by assumption in natural deduction.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   840
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   841
Isabelle automates the meta-inference for proof by assumption.  Its arguments
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   842
are the meta-theorem $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, and some~$i$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   843
from~1 to~$n$, where $\phi@i$ has the form~(\ref{context-eqn}).  Its results
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   844
are meta-theorems of the form
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   845
\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \phi@n} \Imp \phi)s \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   846
for each $s$ and~$j$ such that $s$ unifies $\lambda x@1 \ldots x@l. \theta@j$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   847
with $\lambda x@1 \ldots x@l. \theta$.  Isabelle supplies the parameters
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   848
$x@1$,~\ldots,~$x@l$ to higher-order unification as bound variables, which
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   849
regards them as unique constants with a limited scope --- this enforces
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1865
diff changeset
   850
parameter provisos~\cite{paulson-found}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   851
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   852
The premise represents a proof state with~$n$ subgoals, of which the~$i$th
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   853
is to be solved by assumption.  Isabelle searches the subgoal's context for
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   854
an assumption~$\theta@j$ that can solve it.  For each unifier, the
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   855
meta-inference returns an instantiated proof state from which the $i$th
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   856
subgoal has been removed.  Isabelle searches for a unifying assumption; for
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   857
readability and robustness, proofs do not refer to assumptions by number.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   858
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   859
Consider the proof state 
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   860
\[ (\List{P(a); P(b)} \Imp P(\Var{x})) \Imp Q(\Var{x}). \]
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   861
Proof by assumption (with $i=1$, the only possibility) yields two results:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   862
\begin{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   863
  \item $Q(a)$, instantiating $\Var{x}\equiv a$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   864
  \item $Q(b)$, instantiating $\Var{x}\equiv b$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   865
\end{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   866
Here, proof by assumption affects the main goal.  It could also affect
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   867
other subgoals; if we also had the subgoal ${\List{P(b); P(c)} \Imp
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   868
  P(\Var{x})}$, then $\Var{x}\equiv a$ would transform it to ${\List{P(b);
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   869
    P(c)} \Imp P(a)}$, which might be unprovable.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   870
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   871
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   872
\subsection{A propositional proof} \label{prop-proof}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   873
\index{examples!propositional}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   874
Our first example avoids quantifiers.  Given the main goal $P\disj P\imp
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   875
P$, Isabelle creates the initial state
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   876
\[ (P\disj P\imp P)\Imp (P\disj P\imp P). \] 
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   877
%
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   878
Bear in mind that every proof state we derive will be a meta-theorem,
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   879
expressing that the subgoals imply the main goal.  Our aim is to reach the
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   880
state $P\disj P\imp P$; this meta-theorem is the desired result.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   881
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   882
The first step is to refine subgoal~1 by (${\imp}I)$, creating a new state
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   883
where $P\disj P$ is an assumption:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   884
\[ (P\disj P\Imp P)\Imp (P\disj P\imp P) \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   885
The next step is $(\disj E)$, which replaces subgoal~1 by three new subgoals. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   886
Because of lifting, each subgoal contains a copy of the context --- the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   887
assumption $P\disj P$.  (In fact, this assumption is now redundant; we shall
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   888
shortly see how to get rid of it!)  The new proof state is the following
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   889
meta-theorem, laid out for clarity:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   890
\[ \begin{array}{l@{}l@{\qquad\qquad}l} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   891
  \lbrakk\;& P\disj P\Imp \Var{P@1}\disj\Var{Q@1}; & \hbox{(subgoal 1)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   892
           & \List{P\disj P; \Var{P@1}} \Imp P;    & \hbox{(subgoal 2)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   893
           & \List{P\disj P; \Var{Q@1}} \Imp P     & \hbox{(subgoal 3)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   894
  \rbrakk\;& \Imp (P\disj P\imp P)                 & \hbox{(main goal)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   895
   \end{array} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   896
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   897
Notice the unknowns in the proof state.  Because we have applied $(\disj E)$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   898
we must prove some disjunction, $\Var{P@1}\disj\Var{Q@1}$.  Of course,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   899
subgoal~1 is provable by assumption.  This instantiates both $\Var{P@1}$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   900
$\Var{Q@1}$ to~$P$ throughout the proof state:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   901
\[ \begin{array}{l@{}l@{\qquad\qquad}l} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   902
    \lbrakk\;& \List{P\disj P; P} \Imp P; & \hbox{(subgoal 1)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   903
             & \List{P\disj P; P} \Imp P  & \hbox{(subgoal 2)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   904
    \rbrakk\;& \Imp (P\disj P\imp P)      & \hbox{(main goal)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   905
   \end{array} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   906
Both of the remaining subgoals can be proved by assumption.  After two such
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   907
steps, the proof state is $P\disj P\imp P$.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   908
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   909
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   910
\subsection{A quantifier proof}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   911
\index{examples!with quantifiers}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   912
To illustrate quantifiers and $\Forall$-lifting, let us prove
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   913
$(\exists x.P(f(x)))\imp(\exists x.P(x))$.  The initial proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   914
state is the trivial meta-theorem 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   915
\[ (\exists x.P(f(x)))\imp(\exists x.P(x)) \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   916
   (\exists x.P(f(x)))\imp(\exists x.P(x)). \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   917
As above, the first step is refinement by (${\imp}I)$: 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   918
\[ (\exists x.P(f(x))\Imp \exists x.P(x)) \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   919
   (\exists x.P(f(x)))\imp(\exists x.P(x)) 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   920
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   921
The next step is $(\exists E)$, which replaces subgoal~1 by two new subgoals.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   922
Both have the assumption $\exists x.P(f(x))$.  The new proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   923
state is the meta-theorem  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   924
\[ \begin{array}{l@{}l@{\qquad\qquad}l} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   925
   \lbrakk\;& \exists x.P(f(x)) \Imp \exists x.\Var{P@1}(x); & \hbox{(subgoal 1)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   926
            & \Forall x.\List{\exists x.P(f(x)); \Var{P@1}(x)} \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   927
                       \exists x.P(x)  & \hbox{(subgoal 2)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   928
    \rbrakk\;& \Imp (\exists x.P(f(x)))\imp(\exists x.P(x))  & \hbox{(main goal)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   929
   \end{array} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   930
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   931
The unknown $\Var{P@1}$ appears in both subgoals.  Because we have applied
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   932
$(\exists E)$, we must prove $\exists x.\Var{P@1}(x)$, where $\Var{P@1}(x)$ may
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   933
become any formula possibly containing~$x$.  Proving subgoal~1 by assumption
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   934
instantiates $\Var{P@1}$ to~$\lambda x.P(f(x))$:  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   935
\[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   936
         \exists x.P(x)\right) 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   937
   \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   938
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   939
The next step is refinement by $(\exists I)$.  The rule is lifted into the
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   940
context of the parameter~$x$ and the assumption $P(f(x))$.  This copies
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   941
the context to the subgoal and allows the existential witness to
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   942
depend upon~$x$: 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   943
\[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   944
         P(\Var{x@2}(x))\right) 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   945
   \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   946
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   947
The existential witness, $\Var{x@2}(x)$, consists of an unknown
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   948
applied to a parameter.  Proof by assumption unifies $\lambda x.P(f(x))$ 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   949
with $\lambda x.P(\Var{x@2}(x))$, instantiating $\Var{x@2}$ to $f$.  The final
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   950
proof state contains no subgoals: $(\exists x.P(f(x)))\imp(\exists x.P(x))$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   951
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   952
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   953
\subsection{Tactics and tacticals}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   954
\index{tactics|bold}\index{tacticals|bold}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   955
{\bf Tactics} perform backward proof.  Isabelle tactics differ from those
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   956
of {\sc lcf}, {\sc hol} and Nuprl by operating on entire proof states,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   957
rather than on individual subgoals.  An Isabelle tactic is a function that
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   958
takes a proof state and returns a sequence (lazy list) of possible
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   959
successor states.  Lazy lists are coded in ML as functions, a standard
6592
c120262044b6 Now uses manual.bib; some references updated
paulson
parents: 6170
diff changeset
   960
technique~\cite{paulson-ml2}.  Isabelle represents proof states by theorems.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   961
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   962
Basic tactics execute the meta-rules described above, operating on a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   963
given subgoal.  The {\bf resolution tactics} take a list of rules and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   964
return next states for each combination of rule and unifier.  The {\bf
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   965
assumption tactic} examines the subgoal's assumptions and returns next
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   966
states for each combination of assumption and unifier.  Lazy lists are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   967
essential because higher-order resolution may return infinitely many
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   968
unifiers.  If there are no matching rules or assumptions then no next
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   969
states are generated; a tactic application that returns an empty list is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   970
said to {\bf fail}.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   971
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   972
Sequences realize their full potential with {\bf tacticals} --- operators
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   973
for combining tactics.  Depth-first search, breadth-first search and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   974
best-first search (where a heuristic function selects the best state to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   975
explore) return their outcomes as a sequence.  Isabelle provides such
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   976
procedures in the form of tacticals.  Simpler procedures can be expressed
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   977
directly using the basic tacticals {\tt THEN}, {\tt ORELSE} and {\tt REPEAT}:
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   978
\begin{ttdescription}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   979
\item[$tac1$ THEN $tac2$] is a tactic for sequential composition.  Applied
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   980
to a proof state, it returns all states reachable in two steps by applying
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   981
$tac1$ followed by~$tac2$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   982
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   983
\item[$tac1$ ORELSE $tac2$] is a choice tactic.  Applied to a state, it
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   984
tries~$tac1$ and returns the result if non-empty; otherwise, it uses~$tac2$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   985
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   986
\item[REPEAT $tac$] is a repetition tactic.  Applied to a state, it
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   987
returns all states reachable by applying~$tac$ as long as possible --- until
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   988
it would fail.  
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   989
\end{ttdescription}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   990
For instance, this tactic repeatedly applies $tac1$ and~$tac2$, giving
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   991
$tac1$ priority:
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   992
\begin{center} \tt
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   993
REPEAT($tac1$ ORELSE $tac2$)
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   994
\end{center}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   995
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   996
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   997
\section{Variations on resolution}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   998
In principle, resolution and proof by assumption suffice to prove all
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   999
theorems.  However, specialized forms of resolution are helpful for working
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1000
with elimination rules.  Elim-resolution applies an elimination rule to an
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1001
assumption; destruct-resolution is similar, but applies a rule in a forward
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1002
style.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1003
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1004
The last part of the section shows how the techniques for proving theorems
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1005
can also serve to derive rules.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1006
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1007
\subsection{Elim-resolution}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1008
\index{elim-resolution|bold}\index{assumptions!deleting}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1009
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1010
Consider proving the theorem $((R\disj R)\disj R)\disj R\imp R$.  By
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1011
$({\imp}I)$, we prove~$R$ from the assumption $((R\disj R)\disj R)\disj R$.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1012
Applying $(\disj E)$ to this assumption yields two subgoals, one that
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1013
assumes~$R$ (and is therefore trivial) and one that assumes $(R\disj
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1014
R)\disj R$.  This subgoal admits another application of $(\disj E)$.  Since
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1015
natural deduction never discards assumptions, we eventually generate a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1016
subgoal containing much that is redundant:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1017
\[ \List{((R\disj R)\disj R)\disj R; (R\disj R)\disj R; R\disj R; R} \Imp R. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1018
In general, using $(\disj E)$ on the assumption $P\disj Q$ creates two new
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1019
subgoals with the additional assumption $P$ or~$Q$.  In these subgoals,
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1020
$P\disj Q$ is redundant.  Other elimination rules behave
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1021
similarly.  In first-order logic, only universally quantified
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1022
assumptions are sometimes needed more than once --- say, to prove
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1023
$P(f(f(a)))$ from the assumptions $\forall x.P(x)\imp P(f(x))$ and~$P(a)$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1024
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1025
Many logics can be formulated as sequent calculi that delete redundant
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1026
assumptions after use.  The rule $(\disj E)$ might become
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1027
\[ \infer[\disj\hbox{-left}]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1028
         {\Gamma,P\disj Q,\Delta \turn \Theta}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1029
         {\Gamma,P,\Delta \turn \Theta && \Gamma,Q,\Delta \turn \Theta}  \] 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1030
In backward proof, a goal containing $P\disj Q$ on the left of the~$\turn$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1031
(that is, as an assumption) splits into two subgoals, replacing $P\disj Q$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1032
by $P$ or~$Q$.  But the sequent calculus, with its explicit handling of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1033
assumptions, can be tiresome to use.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1034
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1035
Elim-resolution is Isabelle's way of getting sequent calculus behaviour
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1036
from natural deduction rules.  It lets an elimination rule consume an
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1037
assumption.  Elim-resolution combines two meta-theorems:
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1038
\begin{itemize}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1039
  \item a rule $\List{\psi@1; \ldots; \psi@m} \Imp \psi$
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1040
  \item a proof state $\List{\phi@1; \ldots; \phi@n} \Imp \phi$
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1041
\end{itemize}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1042
The rule must have at least one premise, thus $m>0$.  Write the rule's
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1043
lifted form as $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$.  Suppose we
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1044
wish to change subgoal number~$i$.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1045
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1046
Ordinary resolution would attempt to reduce~$\phi@i$,
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1047
replacing subgoal~$i$ by $m$ new ones.  Elim-resolution tries
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1048
simultaneously to reduce~$\phi@i$ and to solve~$\psi'@1$ by assumption; it
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1049
returns a sequence of next states.  Each of these replaces subgoal~$i$ by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1050
instances of $\psi'@2$, \ldots, $\psi'@m$ from which the selected
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1051
assumption has been deleted.  Suppose $\phi@i$ has the parameter~$x$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1052
assumptions $\theta@1$,~\ldots,~$\theta@k$.  Then $\psi'@1$, the rule's first
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1053
premise after lifting, will be
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1054
\( \Forall x. \List{\theta@1; \ldots; \theta@k}\Imp \psi^{x}@1 \).
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1055
Elim-resolution tries to unify $\psi'\qeq\phi@i$ and
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1056
$\lambda x. \theta@j \qeq \lambda x. \psi^{x}@1$ simultaneously, for
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1057
$j=1$,~\ldots,~$k$. 
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1058
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1059
Let us redo the example from~\S\ref{prop-proof}.  The elimination rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1060
is~$(\disj E)$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1061
\[ \List{\Var{P}\disj \Var{Q};\; \Var{P}\Imp \Var{R};\; \Var{Q}\Imp \Var{R}}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1062
      \Imp \Var{R}  \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1063
and the proof state is $(P\disj P\Imp P)\Imp (P\disj P\imp P)$.  The
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1064
lifted rule is
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1065
\[ \begin{array}{l@{}l}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1066
  \lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1067
           & \List{P\disj P ;\; \Var{P@1}} \Imp \Var{R@1};    \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1068
           & \List{P\disj P ;\; \Var{Q@1}} \Imp \Var{R@1}     \\
1865
484956c42436 Fixed typo regarding lifting over P|P
paulson
parents: 331
diff changeset
  1069
  \rbrakk\;& \Imp (P\disj P \Imp \Var{R@1})
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1070
  \end{array} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1071
\]
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1072
Unification takes the simultaneous equations
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1073
$P\disj P \qeq \Var{P@1}\disj\Var{Q@1}$ and $\Var{R@1} \qeq P$, yielding
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1074
$\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$.  The new proof state
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1075
is simply
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1076
\[ \List{P \Imp P;\; P \Imp P} \Imp (P\disj P\imp P). 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1077
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1078
Elim-resolution's simultaneous unification gives better control
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1079
than ordinary resolution.  Recall the substitution rule:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1080
$$ \List{\Var{t}=\Var{u}; \Var{P}(\Var{t})} \Imp \Var{P}(\Var{u}) 
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
  1081
\eqno(subst) $$
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1082
Unsuitable for ordinary resolution because $\Var{P}(\Var{u})$ admits many
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1083
unifiers, $(subst)$ works well with elim-resolution.  It deletes some
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1084
assumption of the form $x=y$ and replaces every~$y$ by~$x$ in the subgoal
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1085
formula.  The simultaneous unification instantiates $\Var{u}$ to~$y$; if
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1086
$y$ is not an unknown, then $\Var{P}(y)$ can easily be unified with another
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1087
formula.  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1088
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1089
In logical parlance, the premise containing the connective to be eliminated
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1090
is called the \bfindex{major premise}.  Elim-resolution expects the major
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1091
premise to come first.  The order of the premises is significant in
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1092
Isabelle.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1093
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1094
\subsection{Destruction rules} \label{destruct}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1095
\index{rules!destruction}\index{rules!elimination}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1096
\index{forward proof}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1097
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1098
Looking back to Fig.\ts\ref{fol-fig}, notice that there are two kinds of
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1099
elimination rule.  The rules $({\conj}E1)$, $({\conj}E2)$, $({\imp}E)$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1100
$({\forall}E)$ extract the conclusion from the major premise.  In Isabelle
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1101
parlance, such rules are called {\bf destruction rules}; they are readable
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1102
and easy to use in forward proof.  The rules $({\disj}E)$, $({\bot}E)$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1103
$({\exists}E)$ work by discharging assumptions; they support backward proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1104
in a style reminiscent of the sequent calculus.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1106
The latter style is the most general form of elimination rule.  In natural
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1107
deduction, there is no way to recast $({\disj}E)$, $({\bot}E)$ or
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1108
$({\exists}E)$ as destruction rules.  But we can write general elimination
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1109
rules for $\conj$, $\imp$ and~$\forall$:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1110
\[
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1111
\infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \qquad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1112
\infer{R}{P\imp Q & P & \infer*{R}{[Q]}}  \qquad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1113
\infer{Q}{\forall x.P & \infer*{Q}{[P[t/x]]}} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1114
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1115
Because they are concise, destruction rules are simpler to derive than the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1116
corresponding elimination rules.  To facilitate their use in backward
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1117
proof, Isabelle provides a means of transforming a destruction rule such as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1118
\[ \infer[\quad\hbox{to the elimination rule}\quad]{Q}{P@1 & \ldots & P@m} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1119
   \infer{R.}{P@1 & \ldots & P@m & \infer*{R}{[Q]}} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1120
\]
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1121
{\bf Destruct-resolution}\index{destruct-resolution} combines this
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1122
transformation with elim-resolution.  It applies a destruction rule to some
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1123
assumption of a subgoal.  Given the rule above, it replaces the
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1124
assumption~$P@1$ by~$Q$, with new subgoals of showing instances of $P@2$,
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1125
\ldots,~$P@m$.  Destruct-resolution works forward from a subgoal's
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1126
assumptions.  Ordinary resolution performs forward reasoning from theorems,
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1127
as illustrated in~\S\ref{joining}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1128
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1129
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1130
\subsection{Deriving rules by resolution}  \label{deriving}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1131
\index{rules!derived|bold}\index{meta-assumptions!syntax of}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1132
The meta-logic, itself a form of the predicate calculus, is defined by a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1133
system of natural deduction rules.  Each theorem may depend upon
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1134
meta-assumptions.  The theorem that~$\phi$ follows from the assumptions
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1135
$\phi@1$, \ldots, $\phi@n$ is written
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1136
\[ \phi \quad [\phi@1,\ldots,\phi@n]. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1137
A more conventional notation might be $\phi@1,\ldots,\phi@n \turn \phi$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1138
but Isabelle's notation is more readable with large formulae.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1139
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1140
Meta-level natural deduction provides a convenient mechanism for deriving
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1141
new object-level rules.  To derive the rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1142
\[ \infer{\phi,}{\theta@1 & \ldots & \theta@k} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1143
assume the premises $\theta@1$,~\ldots,~$\theta@k$ at the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1144
meta-level.  Then prove $\phi$, possibly using these assumptions.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1145
Starting with a proof state $\phi\Imp\phi$, assumptions may accumulate,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1146
reaching a final state such as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1147
\[ \phi \quad [\theta@1,\ldots,\theta@k]. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1148
The meta-rule for $\Imp$ introduction discharges an assumption.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1149
Discharging them in the order $\theta@k,\ldots,\theta@1$ yields the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1150
meta-theorem $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, with no
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1151
assumptions.  This represents the desired rule.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1152
Let us derive the general $\conj$ elimination rule:
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
  1153
$$ \infer{R}{P\conj Q & \infer*{R}{[P,Q]}}  \eqno(\conj E) $$
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1154
We assume $P\conj Q$ and $\List{P;Q}\Imp R$, and commence backward proof in
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1155
the state $R\Imp R$.  Resolving this with the second assumption yields the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1156
state 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1157
\[ \phantom{\List{P\conj Q;\; P\conj Q}}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1158
   \llap{$\List{P;Q}$}\Imp R \quad [\,\List{P;Q}\Imp R\,]. \]
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1159
Resolving subgoals~1 and~2 with~$({\conj}E1)$ and~$({\conj}E2)$,
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1160
respectively, yields the state
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1161
\[ \List{P\conj \Var{Q@1};\; \Var{P@2}\conj Q}\Imp R 
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1162
   \quad [\,\List{P;Q}\Imp R\,]. 
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1163
\]
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1164
The unknowns $\Var{Q@1}$ and~$\Var{P@2}$ arise from unconstrained
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1165
subformulae in the premises of~$({\conj}E1)$ and~$({\conj}E2)$.  Resolving
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1166
both subgoals with the assumption $P\conj Q$ instantiates the unknowns to yield
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1167
\[ R \quad [\, \List{P;Q}\Imp R, P\conj Q \,]. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1168
The proof may use the meta-assumptions in any order, and as often as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1169
necessary; when finished, we discharge them in the correct order to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1170
obtain the desired form:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1171
\[ \List{P\conj Q;\; \List{P;Q}\Imp R} \Imp R \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1172
We have derived the rule using free variables, which prevents their
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1173
premature instantiation during the proof; we may now replace them by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1174
schematic variables.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1175
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1176
\begin{warn}
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1177
  Schematic variables are not allowed in meta-assumptions, for a variety of
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1178
  reasons.  Meta-assumptions remain fixed throughout a proof.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1179
\end{warn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1180