doc-src/Intro/foundations.tex
author wenzelm
Thu, 17 Jul 1997 15:03:38 +0200
changeset 3524 c02cb15830de
parent 3485 f27a30a18a17
child 6170 9a59cf8ae9b5
permissions -rw-r--r--
fixed EqI meta rule;
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
105
216d6ed87399 Initial revision
lcp
parents:
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
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   444
\index{theories|bold} A {\bf theory} consists of a signature plus a
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   445
collection of axioms.  The {\Pure} theory contains only the
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   446
meta-logic.  Theories can be combined provided their signatures are
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   447
compatible.  A theory definition extends an existing theory with
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   448
further signature specifications --- classes, types, constants and
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   449
mixfix declarations --- plus lists of axioms and definitions etc.,
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   450
expressed as strings to be parsed.  A theory can formalize a small
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   451
piece of mathematics, such as lists and their operations, or an entire
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   452
logic.  A mathematical development typically involves many theories in
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   453
a hierarchy.  For example, the {\Pure} theory could be extended to
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   454
form a theory for Fig.\ts\ref{fol-fig}; this could be extended in two
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   455
separate ways to form a theory for natural numbers and a theory for
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   456
lists; the union of these two could be extended into a theory defining
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   457
the length of a list:
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   458
\begin{tt}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   459
\[
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   460
\begin{array}{c@{}c@{}c@{}c@{}c}
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   461
     {}   &     {}   &\hbox{Pure}&     {}  &     {}  \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   462
     {}   &     {}   &  \downarrow &     {}   &     {}   \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   463
     {}   &     {}   &\hbox{FOL} &     {}   &     {}   \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   464
     {}   & \swarrow &     {}    & \searrow &     {}   \\
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   465
 \hbox{Nat} &   {}   &     {}    &     {}   & \hbox{List} \\
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   466
     {}   & \searrow &     {}    & \swarrow &     {}   \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   467
     {}   &     {} &\hbox{Nat}+\hbox{List}&  {}   &     {}   \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   468
     {}   &     {}   &  \downarrow &     {}   &     {}   \\
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   469
     {}   &     {} & \hbox{Length} &  {}   &     {}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   470
\end{array}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   471
\]
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   472
\end{tt}%
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   473
Each Isabelle proof typically works within a single theory, which is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   474
associated with the proof state.  However, many different theories may
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   475
coexist at the same time, and you may work in each of these during a single
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   476
session.  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   477
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   478
\begin{warn}\index{constants!clashes with variables}%
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   479
  Confusing problems arise if you work in the wrong theory.  Each theory
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   480
  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
   481
  constant and in another as a variable, for example.
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   482
\end{warn}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   483
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   484
\section{Proof construction in Isabelle}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   485
I have elsewhere described the meta-logic and demonstrated it by
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1865
diff changeset
   486
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
   487
correspondence between meta-level proofs and object-level proofs.  To each
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   488
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
   489
corresponding object-level rule.  Object-level assumptions and parameters
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   490
have meta-level counterparts.  The meta-level formalization is {\bf
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   491
  faithful}, admitting no incorrect object-level inferences, and {\bf
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   492
  adequate}, admitting all correct object-level inferences.  These
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   493
properties must be demonstrated separately for each object-logic.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   494
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   495
The meta-logic is defined by a collection of inference rules, including
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   496
equational rules for the $\lambda$-calculus and logical rules.  The rules
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   497
for~$\Imp$ and~$\Forall$ resemble those for~$\imp$ and~$\forall$ in
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   498
Fig.\ts\ref{fol-fig}.  Proofs performed using the primitive meta-rules
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   499
would be lengthy; Isabelle proofs normally use certain derived rules.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   500
{\bf Resolution}, in particular, is convenient for backward proof.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   501
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   502
Unification is central to theorem proving.  It supports quantifier
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   503
reasoning by allowing certain `unknown' terms to be instantiated later,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   504
possibly in stages.  When proving that the time required to sort $n$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   505
integers is proportional to~$n^2$, we need not state the constant of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   506
proportionality; when proving that a hardware adder will deliver the sum of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   507
its inputs, we need not state how many clock ticks will be required.  Such
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   508
quantities often emerge from the proof.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   509
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   510
Isabelle provides {\bf schematic variables}, or {\bf
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   511
  unknowns},\index{unknowns} for unification.  Logically, unknowns are free
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   512
variables.  But while ordinary variables remain fixed, unification may
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   513
instantiate unknowns.  Unknowns are written with a ?\ prefix and are
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   514
frequently subscripted: $\Var{a}$, $\Var{a@1}$, $\Var{a@2}$, \ldots,
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   515
$\Var{P}$, $\Var{P@1}$, \ldots.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   516
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   517
Recall that an inference rule of the form
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   518
\[ \infer{\phi}{\phi@1 & \ldots & \phi@n} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   519
is formalized in Isabelle's meta-logic as the axiom
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   520
$\List{\phi@1; \ldots; \phi@n} \Imp \phi$.\index{resolution}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   521
Such axioms resemble Prolog's Horn clauses, and can be combined by
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   522
resolution --- Isabelle's principal proof method.  Resolution yields both
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   523
forward and backward proof.  Backward proof works by unifying a goal with
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   524
the conclusion of a rule, whose premises become new subgoals.  Forward proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   525
works by unifying theorems with the premises of a rule, deriving a new theorem.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   526
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   527
Isabelle formulae require an extended notion of resolution.
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   528
They differ from Horn clauses in two major respects:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   529
\begin{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   530
  \item They are written in the typed $\lambda$-calculus, and therefore must be
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   531
resolved using higher-order unification.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   532
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   533
\item The constituents of a clause need not be atomic formulae.  Any
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   534
  formula of the form $Trueprop(\cdots)$ is atomic, but axioms such as
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   535
  ${\imp}I$ and $\forall I$ contain non-atomic formulae.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   536
\end{itemize}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   537
Isabelle has little in common with classical resolution theorem provers
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   538
such as Otter~\cite{wos-bledsoe}.  At the meta-level, Isabelle proves
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   539
theorems in their positive form, not by refutation.  However, an
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   540
object-logic that includes a contradiction rule may employ a refutation
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   541
proof procedure.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   542
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   543
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   544
\subsection{Higher-order unification}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   545
\index{unification!higher-order|bold}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   546
Unification is equation solving.  The solution of $f(\Var{x},c) \qeq
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   547
f(d,\Var{y})$ is $\Var{x}\equiv d$ and $\Var{y}\equiv c$.  {\bf
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   548
Higher-order unification} is equation solving for typed $\lambda$-terms.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   549
To handle $\beta$-conversion, it must reduce $(\lambda x.t)u$ to $t[u/x]$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   550
That is easy --- in the typed $\lambda$-calculus, all reduction sequences
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   551
terminate at a normal form.  But it must guess the unknown
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   552
function~$\Var{f}$ in order to solve the equation
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   553
\begin{equation} \label{hou-eqn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   554
 \Var{f}(t) \qeq g(u@1,\ldots,u@k).
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   555
\end{equation}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   556
Huet's~\cite{huet75} search procedure solves equations by imitation and
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   557
projection.  {\bf Imitation} makes~$\Var{f}$ apply the leading symbol (if a
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   558
constant) of the right-hand side.  To solve equation~(\ref{hou-eqn}), it
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   559
guesses
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   560
\[ \Var{f} \equiv \lambda x. g(\Var{h@1}(x),\ldots,\Var{h@k}(x)), \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   561
where $\Var{h@1}$, \ldots, $\Var{h@k}$ are new unknowns.  Assuming there are no
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   562
other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   563
set of equations
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   564
\[ \Var{h@1}(t)\qeq u@1 \quad\ldots\quad \Var{h@k}(t)\qeq u@k. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   565
If the procedure solves these equations, instantiating $\Var{h@1}$, \ldots,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   566
$\Var{h@k}$, then it yields an instantiation for~$\Var{f}$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   567
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   568
{\bf Projection} makes $\Var{f}$ apply one of its arguments.  To solve
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   569
equation~(\ref{hou-eqn}), if $t$ expects~$m$ arguments and delivers a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   570
result of suitable type, it guesses
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   571
\[ \Var{f} \equiv \lambda x. x(\Var{h@1}(x),\ldots,\Var{h@m}(x)), \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   572
where $\Var{h@1}$, \ldots, $\Var{h@m}$ are new unknowns.  Assuming there are no
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   573
other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   574
equation 
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   575
\[ 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
   576
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   577
\begin{warn}\index{unification!incompleteness of}%
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   578
Huet's unification procedure is complete.  Isabelle's polymorphic version,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   579
which solves for type unknowns as well as for term unknowns, is incomplete.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   580
The problem is that projection requires type information.  In
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   581
equation~(\ref{hou-eqn}), if the type of~$t$ is unknown, then projections
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   582
are possible for all~$m\geq0$, and the types of the $\Var{h@i}$ will be
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   583
similarly unconstrained.  Therefore, Isabelle never attempts such
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   584
projections, and may fail to find unifiers where a type unknown turns out
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   585
to be a function type.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   586
\end{warn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   587
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   588
\index{unknowns!function|bold}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   589
Given $\Var{f}(t@1,\ldots,t@n)\qeq u$, Huet's procedure could make up to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   590
$n+1$ guesses.  The search tree and set of unifiers may be infinite.  But
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   591
higher-order unification can work effectively, provided you are careful
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   592
with {\bf function unknowns}:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   593
\begin{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   594
  \item Equations with no function unknowns are solved using first-order
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   595
unification, extended to treat bound variables.  For example, $\lambda x.x
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   596
\qeq \lambda x.\Var{y}$ has no solution because $\Var{y}\equiv x$ would
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   597
capture the free variable~$x$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   598
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   599
  \item An occurrence of the term $\Var{f}(x,y,z)$, where the arguments are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   600
distinct bound variables, causes no difficulties.  Its projections can only
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   601
match the corresponding variables.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   602
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   603
  \item Even an equation such as $\Var{f}(a)\qeq a+a$ is all right.  It has
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   604
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
   605
imitation.  The first solution is usually the one desired:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   606
\[ \Var{f}\equiv \lambda x. x+x \quad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   607
   \Var{f}\equiv \lambda x. a+x \quad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   608
   \Var{f}\equiv \lambda x. x+a \quad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   609
   \Var{f}\equiv \lambda x. a+a \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   610
  \item  Equations such as $\Var{f}(\Var{x},\Var{y})\qeq t$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   611
$\Var{f}(\Var{g}(x))\qeq t$ admit vast numbers of unifiers, and must be
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   612
avoided. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   613
\end{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   614
In problematic cases, you may have to instantiate some unknowns before
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   615
invoking unification. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   616
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   617
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   618
\subsection{Joining rules by resolution} \label{joining}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   619
\index{resolution|bold}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   620
Let $\List{\psi@1; \ldots; \psi@m} \Imp \psi$ and $\List{\phi@1; \ldots;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   621
\phi@n} \Imp \phi$ be two Isabelle theorems, representing object-level rules. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   622
Choosing some~$i$ from~1 to~$n$, suppose that $\psi$ and $\phi@i$ have a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   623
higher-order unifier.  Writing $Xs$ for the application of substitution~$s$ to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   624
expression~$X$, this means there is some~$s$ such that $\psi s\equiv \phi@i s$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   625
By resolution, we may conclude
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   626
\[ (\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   627
          \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   628
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   629
The substitution~$s$ may instantiate unknowns in both rules.  In short,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   630
resolution is the following rule:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   631
\[ \infer[(\psi s\equiv \phi@i s)]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   632
         {(\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   633
          \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   634
         {\List{\psi@1; \ldots; \psi@m} \Imp \psi & &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   635
          \List{\phi@1; \ldots; \phi@n} \Imp \phi}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   636
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   637
It operates at the meta-level, on Isabelle theorems, and is justified by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   638
the properties of $\Imp$ and~$\Forall$.  It takes the number~$i$ (for
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   639
$1\leq i\leq n$) as a parameter and may yield infinitely many conclusions,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   640
one for each unifier of $\psi$ with $\phi@i$.  Isabelle returns these
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   641
conclusions as a sequence (lazy list).
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   642
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   643
Resolution expects the rules to have no outer quantifiers~($\Forall$).
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   644
It may rename or instantiate any schematic variables, but leaves free
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   645
variables unchanged.  When constructing a theory, Isabelle puts the
3106
wenzelm
parents: 3103
diff changeset
   646
rules into a standard form with all free variables converted into
wenzelm
parents: 3103
diff changeset
   647
schematic ones; for instance, $({\imp}E)$ becomes
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   648
\[ \List{\Var{P}\imp \Var{Q}; \Var{P}}  \Imp \Var{Q}. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   649
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   650
When resolving two rules, the unknowns in the first rule are renamed, by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   651
subscripting, to make them distinct from the unknowns in the second rule.  To
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   652
resolve $({\imp}E)$ with itself, the first copy of the rule becomes
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   653
\[ \List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}}  \Imp \Var{Q@1}. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   654
Resolving this with $({\imp}E)$ in the first premise, unifying $\Var{Q@1}$ with
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   655
$\Var{P}\imp \Var{Q}$, is the meta-level inference
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   656
\[ \infer{\List{\Var{P@1}\imp (\Var{P}\imp \Var{Q}); \Var{P@1}; \Var{P}} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   657
           \Imp\Var{Q}.}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   658
         {\List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}}  \Imp \Var{Q@1} & &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   659
          \List{\Var{P}\imp \Var{Q}; \Var{P}}  \Imp \Var{Q}}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   660
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   661
Renaming the unknowns in the resolvent, we have derived the
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   662
object-level rule\index{rules!derived}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   663
\[ \infer{Q.}{R\imp (P\imp Q)  &  R  &  P}  \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   664
Joining rules in this fashion is a simple way of proving theorems.  The
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   665
derived rules are conservative extensions of the object-logic, and may permit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   666
simpler proofs.  Let us consider another example.  Suppose we have the axiom
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   667
$$ \forall x\,y. Suc(x)=Suc(y)\imp x=y. \eqno (inject) $$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   668
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   669
\noindent 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   670
The standard form of $(\forall E)$ is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   671
$\forall x.\Var{P}(x)  \Imp \Var{P}(\Var{t})$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   672
Resolving $(inject)$ with $(\forall E)$ replaces $\Var{P}$ by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   673
$\lambda x. \forall y. Suc(x)=Suc(y)\imp x=y$ and leaves $\Var{t}$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   674
unchanged, yielding  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   675
\[ \forall y. Suc(\Var{t})=Suc(y)\imp \Var{t}=y. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   676
Resolving this with $(\forall E)$ puts a subscript on~$\Var{t}$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   677
and yields
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   678
\[ Suc(\Var{t@1})=Suc(\Var{t})\imp \Var{t@1}=\Var{t}. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   679
Resolving this with $({\imp}E)$ increases the subscripts and yields
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   680
\[ Suc(\Var{t@2})=Suc(\Var{t@1})\Imp \Var{t@2}=\Var{t@1}. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   681
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   682
We have derived the rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   683
\[ \infer{m=n,}{Suc(m)=Suc(n)} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   684
which goes directly from $Suc(m)=Suc(n)$ to $m=n$.  It is handy for simplifying
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   685
an equation like $Suc(Suc(Suc(m)))=Suc(Suc(Suc(0)))$.  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   686
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   687
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   688
\section{Lifting a rule into a context}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   689
The rules $({\imp}I)$ and $(\forall I)$ may seem unsuitable for
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   690
resolution.  They have non-atomic premises, namely $P\Imp Q$ and $\Forall
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   691
x.P(x)$, while the conclusions of all the rules are atomic (they have the form
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   692
$Trueprop(\cdots)$).  Isabelle gets round the problem through a meta-inference
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   693
called \bfindex{lifting}.  Let us consider how to construct proofs such as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   694
\[ \infer[({\imp}I)]{P\imp(Q\imp R)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   695
         {\infer[({\imp}I)]{Q\imp R}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   696
                        {\infer*{R}{[P,Q]}}}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   697
   \qquad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   698
   \infer[(\forall I)]{\forall x\,y.P(x,y)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   699
         {\infer[(\forall I)]{\forall y.P(x,y)}{P(x,y)}}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   700
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   701
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   702
\subsection{Lifting over assumptions}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   703
\index{assumptions!lifting over}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   704
Lifting over $\theta\Imp{}$ is the following meta-inference rule:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   705
\[ \infer{\List{\theta\Imp\phi@1; \ldots; \theta\Imp\phi@n} \Imp
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   706
          (\theta \Imp \phi)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   707
         {\List{\phi@1; \ldots; \phi@n} \Imp \phi} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   708
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
   709
$\theta\Imp\phi@1$, \ldots, $\theta\Imp\phi@n$ and $\theta$ are all true then
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   710
$\phi$ must be true.  Iterated lifting over a series of meta-formulae
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   711
$\theta@k$, \ldots, $\theta@1$ yields an object-rule whose conclusion is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   712
$\List{\theta@1; \ldots; \theta@k} \Imp \phi$.  Typically the $\theta@i$ are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   713
the assumptions in a natural deduction proof; lifting copies them into a rule's
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   714
premises and conclusion.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   715
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   716
When resolving two rules, Isabelle lifts the first one if necessary.  The
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   717
standard form of $({\imp}I)$ is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   718
\[ (\Var{P} \Imp \Var{Q})  \Imp  \Var{P}\imp \Var{Q}.   \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   719
To resolve this rule with itself, Isabelle modifies one copy as follows: it
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   720
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
   721
$\Var{P}\Imp{}$ to obtain
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   722
\[ (\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
   723
   (\Var{P@1}\imp \Var{Q@1})).   \]
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   724
Using the $\List{\cdots}$ abbreviation, this can be written as
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   725
\[ \List{\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}; \Var{P}} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   726
   \Imp  \Var{P@1}\imp \Var{Q@1}.   \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   727
Unifying $\Var{P}\Imp \Var{P@1}\imp\Var{Q@1}$ with $\Var{P} \Imp
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   728
\Var{Q}$ instantiates $\Var{Q}$ to ${\Var{P@1}\imp\Var{Q@1}}$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   729
Resolution yields
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   730
\[ (\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}) \Imp
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   731
\Var{P}\imp(\Var{P@1}\imp\Var{Q@1}).   \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   732
This represents the derived rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   733
\[ \infer{P\imp(Q\imp R).}{\infer*{R}{[P,Q]}} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   734
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   735
\subsection{Lifting over parameters}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   736
\index{parameters!lifting over}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   737
An analogous form of lifting handles premises of the form $\Forall x\ldots\,$. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   738
Here, lifting prefixes an object-rule's premises and conclusion with $\Forall
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   739
x$.  At the same time, lifting introduces a dependence upon~$x$.  It replaces
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   740
each unknown $\Var{a}$ in the rule by $\Var{a'}(x)$, where $\Var{a'}$ is a new
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   741
unknown (by subscripting) of suitable type --- necessarily a function type.  In
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   742
short, lifting is the meta-inference
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   743
\[ \infer{\List{\Forall x.\phi@1^x; \ldots; \Forall x.\phi@n^x} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   744
           \Imp \Forall x.\phi^x,}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   745
         {\List{\phi@1; \ldots; \phi@n} \Imp \phi} \]
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   746
%
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   747
where $\phi^x$ stands for the result of lifting unknowns over~$x$ in
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   748
$\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
   749
$\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
   750
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
   751
$(\Forall x.\phi^x) \Imp (\Forall x.\psi^x)$.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   752
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   753
For example, $(\disj I)$ might be lifted to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   754
\[ (\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
   755
and $(\forall I)$ to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   756
\[ (\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
   757
Isabelle has renamed a bound variable in $(\forall I)$ from $x$ to~$y$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   758
avoiding a clash.  Resolving the above with $(\forall I)$ is the meta-inference
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   759
\[ \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
   760
         {(\Forall x\,y.\Var{P@1}(x,y)) \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   761
               (\Forall x. \forall y.\Var{P@1}(x,y))  &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   762
          (\Forall x.\Var{P}(x)) \Imp (\forall x.\Var{P}(x))} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   763
Here, $\Var{P}$ is replaced by $\lambda x.\forall y.\Var{P@1}(x,y)$; the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   764
resolvent expresses the derived rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   765
\[ \vcenter{ \infer{\forall x\,y.Q(x,y)}{Q(x,y)} }
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   766
   \quad\hbox{provided $x$, $y$ not free in the assumptions} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   767
\] 
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1865
diff changeset
   768
I discuss lifting and parameters at length elsewhere~\cite{paulson-found}.
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   769
Miller goes into even greater detail~\cite{miller-mixed}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   770
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   771
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   772
\section{Backward proof by resolution}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   773
\index{resolution!in backward proof}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   774
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   775
Resolution is convenient for deriving simple rules and for reasoning
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   776
forward from facts.  It can also support backward proof, where we start
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   777
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
   778
been solved.  {\sc lcf} and its descendants {\sc hol} and Nuprl provide
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   779
tactics and tacticals, which constitute a sophisticated language for
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   780
expressing proof searches.  {\bf Tactics} refine subgoals while {\bf
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   781
  tacticals} combine tactics.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   782
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   783
\index{LCF system}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   784
Isabelle's tactics and tacticals work differently from {\sc lcf}'s.  An
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   785
Isabelle rule is bidirectional: there is no distinction between
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   786
inputs and outputs.  {\sc lcf} has a separate tactic for each rule;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   787
Isabelle performs refinement by any rule in a uniform fashion, using
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   788
resolution.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   789
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   790
Isabelle works with meta-level theorems of the form
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   791
\( \List{\phi@1; \ldots; \phi@n} \Imp \phi \).
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   792
We have viewed this as the {\bf rule} with premises
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   793
$\phi@1$,~\ldots,~$\phi@n$ and conclusion~$\phi$.  It can also be viewed as
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   794
the {\bf proof state}\index{proof state}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   795
with subgoals $\phi@1$,~\ldots,~$\phi@n$ and main
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   796
goal~$\phi$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   797
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   798
To prove the formula~$\phi$, take $\phi\Imp \phi$ as the initial proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   799
state.  This assertion is, trivially, a theorem.  At a later stage in the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   800
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
   801
\Imp \phi$.  This proof state is a theorem, ensuring that the subgoals
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   802
$\phi@1$,~\ldots,~$\phi@n$ imply~$\phi$.  If $n=0$ then we have
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   803
proved~$\phi$ outright.  If $\phi$ contains unknowns, they may become
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   804
instantiated during the proof; a proof state may be $\List{\phi@1; \ldots;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   805
\phi@n} \Imp \phi'$, where $\phi'$ is an instance of~$\phi$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   806
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   807
\subsection{Refinement by resolution}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   808
To refine subgoal~$i$ of a proof state by a rule, perform the following
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   809
resolution: 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   810
\[ \infer{\hbox{new proof state}}{\hbox{rule} & & \hbox{proof state}} \]
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   811
Suppose the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   812
lifting over subgoal~$i$'s assumptions and parameters.  If the proof state
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   813
is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, then the new proof state is
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   814
(for~$1\leq i\leq n$)
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   815
\[ (\List{\phi@1; \ldots; \phi@{i-1}; \psi'@1;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   816
          \ldots; \psi'@m; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.  \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   817
Substitution~$s$ unifies $\psi'$ with~$\phi@i$.  In the proof state,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   818
subgoal~$i$ is replaced by $m$ new subgoals, the rule's instantiated premises.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   819
If some of the rule's unknowns are left un-instantiated, they become new
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   820
unknowns in the proof state.  Refinement by~$(\exists I)$, namely
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   821
\[ \Var{P}(\Var{t}) \Imp \exists x. \Var{P}(x), \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   822
inserts a new unknown derived from~$\Var{t}$ by subscripting and lifting.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   823
We do not have to specify an `existential witness' when
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   824
applying~$(\exists I)$.  Further resolutions may instantiate unknowns in
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   825
the proof state.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   826
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   827
\subsection{Proof by assumption}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   828
\index{assumptions!use of}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   829
In the course of a natural deduction proof, parameters $x@1$, \ldots,~$x@l$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   830
assumptions $\theta@1$, \ldots, $\theta@k$ accumulate, forming a context for
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   831
each subgoal.  Repeated lifting steps can lift a rule into any context.  To
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   832
aid readability, Isabelle puts contexts into a normal form, gathering the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   833
parameters at the front:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   834
\begin{equation} \label{context-eqn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   835
\Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   836
\end{equation}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   837
Under the usual reading of the connectives, this expresses that $\theta$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   838
follows from $\theta@1$,~\ldots~$\theta@k$ for arbitrary
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   839
$x@1$,~\ldots,~$x@l$.  It is trivially true if $\theta$ equals any of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   840
$\theta@1$,~\ldots~$\theta@k$, or is unifiable with any of them.  This
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   841
models proof by assumption in natural deduction.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   842
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   843
Isabelle automates the meta-inference for proof by assumption.  Its arguments
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   844
are the meta-theorem $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, and some~$i$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   845
from~1 to~$n$, where $\phi@i$ has the form~(\ref{context-eqn}).  Its results
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   846
are meta-theorems of the form
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   847
\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \phi@n} \Imp \phi)s \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   848
for each $s$ and~$j$ such that $s$ unifies $\lambda x@1 \ldots x@l. \theta@j$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   849
with $\lambda x@1 \ldots x@l. \theta$.  Isabelle supplies the parameters
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   850
$x@1$,~\ldots,~$x@l$ to higher-order unification as bound variables, which
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   851
regards them as unique constants with a limited scope --- this enforces
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1865
diff changeset
   852
parameter provisos~\cite{paulson-found}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   853
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   854
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
   855
is to be solved by assumption.  Isabelle searches the subgoal's context for
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   856
an assumption~$\theta@j$ that can solve it.  For each unifier, the
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   857
meta-inference returns an instantiated proof state from which the $i$th
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   858
subgoal has been removed.  Isabelle searches for a unifying assumption; for
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   859
readability and robustness, proofs do not refer to assumptions by number.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   860
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   861
Consider the proof state 
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   862
\[ (\List{P(a); P(b)} \Imp P(\Var{x})) \Imp Q(\Var{x}). \]
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   863
Proof by assumption (with $i=1$, the only possibility) yields two results:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   864
\begin{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   865
  \item $Q(a)$, instantiating $\Var{x}\equiv a$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   866
  \item $Q(b)$, instantiating $\Var{x}\equiv b$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   867
\end{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   868
Here, proof by assumption affects the main goal.  It could also affect
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   869
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
   870
  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
   871
    P(c)} \Imp P(a)}$, which might be unprovable.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   872
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   873
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   874
\subsection{A propositional proof} \label{prop-proof}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   875
\index{examples!propositional}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   876
Our first example avoids quantifiers.  Given the main goal $P\disj P\imp
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   877
P$, Isabelle creates the initial state
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   878
\[ (P\disj P\imp P)\Imp (P\disj P\imp P). \] 
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   879
%
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   880
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
   881
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
   882
state $P\disj P\imp P$; this meta-theorem is the desired result.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   883
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   884
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
   885
where $P\disj P$ is an assumption:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   886
\[ (P\disj P\Imp P)\Imp (P\disj P\imp P) \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   887
The next step is $(\disj E)$, which replaces subgoal~1 by three new subgoals. 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   888
Because of lifting, each subgoal contains a copy of the context --- the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   889
assumption $P\disj P$.  (In fact, this assumption is now redundant; we shall
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   890
shortly see how to get rid of it!)  The new proof state is the following
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   891
meta-theorem, laid out for clarity:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   892
\[ \begin{array}{l@{}l@{\qquad\qquad}l} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   893
  \lbrakk\;& P\disj P\Imp \Var{P@1}\disj\Var{Q@1}; & \hbox{(subgoal 1)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   894
           & \List{P\disj P; \Var{P@1}} \Imp P;    & \hbox{(subgoal 2)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   895
           & \List{P\disj P; \Var{Q@1}} \Imp P     & \hbox{(subgoal 3)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   896
  \rbrakk\;& \Imp (P\disj P\imp P)                 & \hbox{(main goal)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   897
   \end{array} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   898
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   899
Notice the unknowns in the proof state.  Because we have applied $(\disj E)$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   900
we must prove some disjunction, $\Var{P@1}\disj\Var{Q@1}$.  Of course,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   901
subgoal~1 is provable by assumption.  This instantiates both $\Var{P@1}$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   902
$\Var{Q@1}$ to~$P$ throughout the proof state:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   903
\[ \begin{array}{l@{}l@{\qquad\qquad}l} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   904
    \lbrakk\;& \List{P\disj P; P} \Imp P; & \hbox{(subgoal 1)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   905
             & \List{P\disj P; P} \Imp P  & \hbox{(subgoal 2)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   906
    \rbrakk\;& \Imp (P\disj P\imp P)      & \hbox{(main goal)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   907
   \end{array} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   908
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
   909
steps, the proof state is $P\disj P\imp P$.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   910
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   911
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   912
\subsection{A quantifier proof}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   913
\index{examples!with quantifiers}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   914
To illustrate quantifiers and $\Forall$-lifting, let us prove
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   915
$(\exists x.P(f(x)))\imp(\exists x.P(x))$.  The initial proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   916
state is the trivial meta-theorem 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   917
\[ (\exists x.P(f(x)))\imp(\exists x.P(x)) \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   918
   (\exists x.P(f(x)))\imp(\exists x.P(x)). \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   919
As above, the first step is refinement by (${\imp}I)$: 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   920
\[ (\exists x.P(f(x))\Imp \exists x.P(x)) \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   921
   (\exists x.P(f(x)))\imp(\exists x.P(x)) 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   922
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   923
The next step is $(\exists E)$, which replaces subgoal~1 by two new subgoals.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   924
Both have the assumption $\exists x.P(f(x))$.  The new proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   925
state is the meta-theorem  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   926
\[ \begin{array}{l@{}l@{\qquad\qquad}l} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   927
   \lbrakk\;& \exists x.P(f(x)) \Imp \exists x.\Var{P@1}(x); & \hbox{(subgoal 1)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   928
            & \Forall x.\List{\exists x.P(f(x)); \Var{P@1}(x)} \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   929
                       \exists x.P(x)  & \hbox{(subgoal 2)} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   930
    \rbrakk\;& \Imp (\exists x.P(f(x)))\imp(\exists x.P(x))  & \hbox{(main goal)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   931
   \end{array} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   932
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   933
The unknown $\Var{P@1}$ appears in both subgoals.  Because we have applied
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   934
$(\exists E)$, we must prove $\exists x.\Var{P@1}(x)$, where $\Var{P@1}(x)$ may
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   935
become any formula possibly containing~$x$.  Proving subgoal~1 by assumption
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   936
instantiates $\Var{P@1}$ to~$\lambda x.P(f(x))$:  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   937
\[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   938
         \exists x.P(x)\right) 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   939
   \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   940
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   941
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
   942
context of the parameter~$x$ and the assumption $P(f(x))$.  This copies
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   943
the context to the subgoal and allows the existential witness to
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   944
depend upon~$x$: 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   945
\[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   946
         P(\Var{x@2}(x))\right) 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   947
   \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   948
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   949
The existential witness, $\Var{x@2}(x)$, consists of an unknown
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   950
applied to a parameter.  Proof by assumption unifies $\lambda x.P(f(x))$ 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   951
with $\lambda x.P(\Var{x@2}(x))$, instantiating $\Var{x@2}$ to $f$.  The final
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   952
proof state contains no subgoals: $(\exists x.P(f(x)))\imp(\exists x.P(x))$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   953
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   954
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   955
\subsection{Tactics and tacticals}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   956
\index{tactics|bold}\index{tacticals|bold}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   957
{\bf Tactics} perform backward proof.  Isabelle tactics differ from those
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   958
of {\sc lcf}, {\sc hol} and Nuprl by operating on entire proof states,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   959
rather than on individual subgoals.  An Isabelle tactic is a function that
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   960
takes a proof state and returns a sequence (lazy list) of possible
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   961
successor states.  Lazy lists are coded in ML as functions, a standard
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   962
technique~\cite{paulson91}.  Isabelle represents proof states by theorems.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   963
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   964
Basic tactics execute the meta-rules described above, operating on a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   965
given subgoal.  The {\bf resolution tactics} take a list of rules and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   966
return next states for each combination of rule and unifier.  The {\bf
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   967
assumption tactic} examines the subgoal's assumptions and returns next
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   968
states for each combination of assumption and unifier.  Lazy lists are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   969
essential because higher-order resolution may return infinitely many
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   970
unifiers.  If there are no matching rules or assumptions then no next
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   971
states are generated; a tactic application that returns an empty list is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   972
said to {\bf fail}.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   973
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   974
Sequences realize their full potential with {\bf tacticals} --- operators
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   975
for combining tactics.  Depth-first search, breadth-first search and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   976
best-first search (where a heuristic function selects the best state to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   977
explore) return their outcomes as a sequence.  Isabelle provides such
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   978
procedures in the form of tacticals.  Simpler procedures can be expressed
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   979
directly using the basic tacticals {\tt THEN}, {\tt ORELSE} and {\tt REPEAT}:
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   980
\begin{ttdescription}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   981
\item[$tac1$ THEN $tac2$] is a tactic for sequential composition.  Applied
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   982
to a proof state, it returns all states reachable in two steps by applying
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   983
$tac1$ followed by~$tac2$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   984
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   985
\item[$tac1$ ORELSE $tac2$] is a choice tactic.  Applied to a state, it
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   986
tries~$tac1$ and returns the result if non-empty; otherwise, it uses~$tac2$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   987
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   988
\item[REPEAT $tac$] is a repetition tactic.  Applied to a state, it
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   989
returns all states reachable by applying~$tac$ as long as possible --- until
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
   990
it would fail.  
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   991
\end{ttdescription}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   992
For instance, this tactic repeatedly applies $tac1$ and~$tac2$, giving
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   993
$tac1$ priority:
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   994
\begin{center} \tt
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   995
REPEAT($tac1$ ORELSE $tac2$)
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
   996
\end{center}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   997
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   998
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   999
\section{Variations on resolution}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1000
In principle, resolution and proof by assumption suffice to prove all
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1001
theorems.  However, specialized forms of resolution are helpful for working
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1002
with elimination rules.  Elim-resolution applies an elimination rule to an
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1003
assumption; destruct-resolution is similar, but applies a rule in a forward
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1004
style.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1005
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1006
The last part of the section shows how the techniques for proving theorems
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1007
can also serve to derive rules.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1008
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1009
\subsection{Elim-resolution}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1010
\index{elim-resolution|bold}\index{assumptions!deleting}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1011
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1012
Consider proving the theorem $((R\disj R)\disj R)\disj R\imp R$.  By
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1013
$({\imp}I)$, we prove~$R$ from the assumption $((R\disj R)\disj R)\disj R$.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1014
Applying $(\disj E)$ to this assumption yields two subgoals, one that
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1015
assumes~$R$ (and is therefore trivial) and one that assumes $(R\disj
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1016
R)\disj R$.  This subgoal admits another application of $(\disj E)$.  Since
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1017
natural deduction never discards assumptions, we eventually generate a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1018
subgoal containing much that is redundant:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1019
\[ \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
  1020
In general, using $(\disj E)$ on the assumption $P\disj Q$ creates two new
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1021
subgoals with the additional assumption $P$ or~$Q$.  In these subgoals,
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1022
$P\disj Q$ is redundant.  Other elimination rules behave
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1023
similarly.  In first-order logic, only universally quantified
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1024
assumptions are sometimes needed more than once --- say, to prove
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1025
$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
  1026
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1027
Many logics can be formulated as sequent calculi that delete redundant
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1028
assumptions after use.  The rule $(\disj E)$ might become
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1029
\[ \infer[\disj\hbox{-left}]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1030
         {\Gamma,P\disj Q,\Delta \turn \Theta}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1031
         {\Gamma,P,\Delta \turn \Theta && \Gamma,Q,\Delta \turn \Theta}  \] 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1032
In backward proof, a goal containing $P\disj Q$ on the left of the~$\turn$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1033
(that is, as an assumption) splits into two subgoals, replacing $P\disj Q$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1034
by $P$ or~$Q$.  But the sequent calculus, with its explicit handling of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1035
assumptions, can be tiresome to use.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1036
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1037
Elim-resolution is Isabelle's way of getting sequent calculus behaviour
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1038
from natural deduction rules.  It lets an elimination rule consume an
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1039
assumption.  Elim-resolution combines two meta-theorems:
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1040
\begin{itemize}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1041
  \item a rule $\List{\psi@1; \ldots; \psi@m} \Imp \psi$
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1042
  \item a proof state $\List{\phi@1; \ldots; \phi@n} \Imp \phi$
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1043
\end{itemize}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1044
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
  1045
lifted form as $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$.  Suppose we
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1046
wish to change subgoal number~$i$.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1047
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1048
Ordinary resolution would attempt to reduce~$\phi@i$,
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1049
replacing subgoal~$i$ by $m$ new ones.  Elim-resolution tries
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1050
simultaneously to reduce~$\phi@i$ and to solve~$\psi'@1$ by assumption; it
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1051
returns a sequence of next states.  Each of these replaces subgoal~$i$ by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1052
instances of $\psi'@2$, \ldots, $\psi'@m$ from which the selected
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1053
assumption has been deleted.  Suppose $\phi@i$ has the parameter~$x$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1054
assumptions $\theta@1$,~\ldots,~$\theta@k$.  Then $\psi'@1$, the rule's first
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1055
premise after lifting, will be
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1056
\( \Forall x. \List{\theta@1; \ldots; \theta@k}\Imp \psi^{x}@1 \).
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1057
Elim-resolution tries to unify $\psi'\qeq\phi@i$ and
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1058
$\lambda x. \theta@j \qeq \lambda x. \psi^{x}@1$ simultaneously, for
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1059
$j=1$,~\ldots,~$k$. 
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1060
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1061
Let us redo the example from~\S\ref{prop-proof}.  The elimination rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1062
is~$(\disj E)$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1063
\[ \List{\Var{P}\disj \Var{Q};\; \Var{P}\Imp \Var{R};\; \Var{Q}\Imp \Var{R}}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1064
      \Imp \Var{R}  \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1065
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
  1066
lifted rule is
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1067
\[ \begin{array}{l@{}l}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1068
  \lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1069
           & \List{P\disj P ;\; \Var{P@1}} \Imp \Var{R@1};    \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1070
           & \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
  1071
  \rbrakk\;& \Imp (P\disj P \Imp \Var{R@1})
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1072
  \end{array} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1073
\]
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1074
Unification takes the simultaneous equations
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1075
$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
  1076
$\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
  1077
is simply
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1078
\[ \List{P \Imp P;\; P \Imp P} \Imp (P\disj P\imp P). 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1079
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1080
Elim-resolution's simultaneous unification gives better control
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1081
than ordinary resolution.  Recall the substitution rule:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1082
$$ \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
  1083
\eqno(subst) $$
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1084
Unsuitable for ordinary resolution because $\Var{P}(\Var{u})$ admits many
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1085
unifiers, $(subst)$ works well with elim-resolution.  It deletes some
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1086
assumption of the form $x=y$ and replaces every~$y$ by~$x$ in the subgoal
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1087
formula.  The simultaneous unification instantiates $\Var{u}$ to~$y$; if
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1088
$y$ is not an unknown, then $\Var{P}(y)$ can easily be unified with another
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1089
formula.  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1090
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1091
In logical parlance, the premise containing the connective to be eliminated
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1092
is called the \bfindex{major premise}.  Elim-resolution expects the major
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1093
premise to come first.  The order of the premises is significant in
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1094
Isabelle.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1095
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1096
\subsection{Destruction rules} \label{destruct}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1097
\index{rules!destruction}\index{rules!elimination}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1098
\index{forward proof}
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1099
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
  1100
Looking back to Fig.\ts\ref{fol-fig}, notice that there are two kinds of
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1101
elimination rule.  The rules $({\conj}E1)$, $({\conj}E2)$, $({\imp}E)$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1102
$({\forall}E)$ extract the conclusion from the major premise.  In Isabelle
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1103
parlance, such rules are called {\bf destruction rules}; they are readable
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1104
and easy to use in forward proof.  The rules $({\disj}E)$, $({\bot}E)$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1105
$({\exists}E)$ work by discharging assumptions; they support backward proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1106
in a style reminiscent of the sequent calculus.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1107
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1108
The latter style is the most general form of elimination rule.  In natural
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1109
deduction, there is no way to recast $({\disj}E)$, $({\bot}E)$ or
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1110
$({\exists}E)$ as destruction rules.  But we can write general elimination
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1111
rules for $\conj$, $\imp$ and~$\forall$:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1112
\[
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1113
\infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \qquad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1114
\infer{R}{P\imp Q & P & \infer*{R}{[Q]}}  \qquad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1115
\infer{Q}{\forall x.P & \infer*{Q}{[P[t/x]]}} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1116
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1117
Because they are concise, destruction rules are simpler to derive than the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1118
corresponding elimination rules.  To facilitate their use in backward
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1119
proof, Isabelle provides a means of transforming a destruction rule such as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1120
\[ \infer[\quad\hbox{to the elimination rule}\quad]{Q}{P@1 & \ldots & P@m} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1121
   \infer{R.}{P@1 & \ldots & P@m & \infer*{R}{[Q]}} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1122
\]
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1123
{\bf Destruct-resolution}\index{destruct-resolution} combines this
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1124
transformation with elim-resolution.  It applies a destruction rule to some
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1125
assumption of a subgoal.  Given the rule above, it replaces the
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1126
assumption~$P@1$ by~$Q$, with new subgoals of showing instances of $P@2$,
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1127
\ldots,~$P@m$.  Destruct-resolution works forward from a subgoal's
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1128
assumptions.  Ordinary resolution performs forward reasoning from theorems,
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1129
as illustrated in~\S\ref{joining}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1130
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1131
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1132
\subsection{Deriving rules by resolution}  \label{deriving}
312
7ceea59b4748 penultimate Springer draft
lcp
parents: 296
diff changeset
  1133
\index{rules!derived|bold}\index{meta-assumptions!syntax of}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1134
The meta-logic, itself a form of the predicate calculus, is defined by a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1135
system of natural deduction rules.  Each theorem may depend upon
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1136
meta-assumptions.  The theorem that~$\phi$ follows from the assumptions
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1137
$\phi@1$, \ldots, $\phi@n$ is written
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1138
\[ \phi \quad [\phi@1,\ldots,\phi@n]. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1139
A more conventional notation might be $\phi@1,\ldots,\phi@n \turn \phi$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1140
but Isabelle's notation is more readable with large formulae.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1141
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1142
Meta-level natural deduction provides a convenient mechanism for deriving
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1143
new object-level rules.  To derive the rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1144
\[ \infer{\phi,}{\theta@1 & \ldots & \theta@k} \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1145
assume the premises $\theta@1$,~\ldots,~$\theta@k$ at the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1146
meta-level.  Then prove $\phi$, possibly using these assumptions.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1147
Starting with a proof state $\phi\Imp\phi$, assumptions may accumulate,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1148
reaching a final state such as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1149
\[ \phi \quad [\theta@1,\ldots,\theta@k]. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1150
The meta-rule for $\Imp$ introduction discharges an assumption.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1151
Discharging them in the order $\theta@k,\ldots,\theta@1$ yields the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1152
meta-theorem $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, with no
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1153
assumptions.  This represents the desired rule.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1154
Let us derive the general $\conj$ elimination rule:
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
  1155
$$ \infer{R}{P\conj Q & \infer*{R}{[P,Q]}}  \eqno(\conj E) $$
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1156
We assume $P\conj Q$ and $\List{P;Q}\Imp R$, and commence backward proof in
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1157
the state $R\Imp R$.  Resolving this with the second assumption yields the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1158
state 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1159
\[ \phantom{\List{P\conj Q;\; P\conj Q}}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1160
   \llap{$\List{P;Q}$}\Imp R \quad [\,\List{P;Q}\Imp R\,]. \]
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1161
Resolving subgoals~1 and~2 with~$({\conj}E1)$ and~$({\conj}E2)$,
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1162
respectively, yields the state
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1163
\[ \List{P\conj \Var{Q@1};\; \Var{P@2}\conj Q}\Imp R 
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1164
   \quad [\,\List{P;Q}\Imp R\,]. 
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1165
\]
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1166
The unknowns $\Var{Q@1}$ and~$\Var{P@2}$ arise from unconstrained
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1167
subformulae in the premises of~$({\conj}E1)$ and~$({\conj}E2)$.  Resolving
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1168
both subgoals with the assumption $P\conj Q$ instantiates the unknowns to yield
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1169
\[ R \quad [\, \List{P;Q}\Imp R, P\conj Q \,]. \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1170
The proof may use the meta-assumptions in any order, and as often as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1171
necessary; when finished, we discharge them in the correct order to
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1172
obtain the desired form:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1173
\[ \List{P\conj Q;\; \List{P;Q}\Imp R} \Imp R \]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1174
We have derived the rule using free variables, which prevents their
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1175
premature instantiation during the proof; we may now replace them by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1176
schematic variables.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1177
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1178
\begin{warn}
331
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1179
  Schematic variables are not allowed in meta-assumptions, for a variety of
13660d5f6a77 final Springer copy
lcp
parents: 312
diff changeset
  1180
  reasons.  Meta-assumptions remain fixed throughout a proof.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1181
\end{warn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
  1182