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