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