doc-src/Intro/getting.tex
author wenzelm
Thu, 15 May 1997 14:49:41 +0200
changeset 3199 c572a6c21b28
parent 3127 4cc2fe62f7c3
child 3485 f27a30a18a17
permissions -rw-r--r--
remove FIXME;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
     2
\part{Getting Started with Isabelle}\label{chap:getting}
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
     3
Let us consider how to perform simple proofs using Isabelle.  At
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
     4
present, Isabelle's user interface is \ML.  Proofs are conducted by
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
     5
applying certain \ML{} functions, which update a stored proof state.
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
     6
Basically, all syntax must be expressed using plain {\sc ascii}
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
     7
characters. There are also mechanisms built into Isabelle that support
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
     8
alternative syntaxes, for example using mathematical symbols from a
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
     9
special screen font. The meta-logic and major object-logics already
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    10
provide such fancy output as an option.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    11
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    12
Object-logics are built upon Pure Isabelle, which implements the
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    13
meta-logic and provides certain fundamental data structures: types,
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    14
terms, signatures, theorems and theories, tactics and tacticals.
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    15
These data structures have the corresponding \ML{} types {\tt typ},
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    16
{\tt term}, {\tt Sign.sg}, {\tt thm}, {\tt theory} and {\tt tactic};
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    17
tacticals have function types such as {\tt tactic->tactic}.  Isabelle
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    18
users can operate on these data structures by writing \ML{} programs.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    19
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
    20
\section{Forward proof}\label{sec:forward} \index{forward proof|(}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    21
This section describes the concrete syntax for types, terms and theorems,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    22
and demonstrates forward proof.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    23
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    24
\subsection{Lexical matters}
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
    25
\index{identifiers}\index{reserved words} 
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    26
An {\bf identifier} is a string of letters, digits, underscores~(\verb|_|)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    27
and single quotes~({\tt'}), beginning with a letter.  Single quotes are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    28
regarded as primes; for instance {\tt x'} is read as~$x'$.  Identifiers are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    29
separated by white space and special characters.  {\bf Reserved words} are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    30
identifiers that appear in Isabelle syntax definitions.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    31
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    32
An Isabelle theory can declare symbols composed of special characters, such
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    33
as {\tt=}, {\tt==}, {\tt=>} and {\tt==>}.  (The latter three are part of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    34
the syntax of the meta-logic.)  Such symbols may be run together; thus if
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    35
\verb|}| and \verb|{| are used for set brackets then \verb|{{a},{a,b}}| is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    36
valid notation for a set of sets --- but only if \verb|}}| and \verb|{{|
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    37
have not been declared as symbols!  The parser resolves any ambiguity by
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    38
taking the longest possible symbol that has been declared.  Thus the string
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    39
{\tt==>} is read as a single symbol.  But \hbox{\tt= =>} is read as two
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    40
symbols.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    41
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    42
Identifiers that are not reserved words may serve as free variables or
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    43
constants.  A {\bf type identifier} consists of an identifier prefixed by a
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    44
prime, for example {\tt'a} and \hbox{\tt'hello}.  Type identifiers stand
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    45
for (free) type variables, which remain fixed during a proof.
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    46
\index{type identifiers}
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    47
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    48
An {\bf unknown}\index{unknowns} (or type unknown) consists of a question
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    49
mark, an identifier (or type identifier), and a subscript.  The subscript,
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    50
a non-negative integer,
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    51
allows the renaming of unknowns prior to unification.%
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    52
\footnote{The subscript may appear after the identifier, separated by a
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    53
  dot; this prevents ambiguity when the identifier ends with a digit.  Thus
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    54
  {\tt?z6.0} has identifier {\tt"z6"} and subscript~0, while {\tt?a0.5}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    55
  has identifier {\tt"a0"} and subscript~5.  If the identifier does not
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    56
  end with a digit, then no dot appears and a subscript of~0 is omitted;
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    57
  for example, {\tt?hello} has identifier {\tt"hello"} and subscript
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    58
  zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6.  The same
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    59
  conventions apply to type unknowns.  The question mark is {\it not\/}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    60
  part of the identifier!}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    61
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    62
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    63
\subsection{Syntax of types and terms}
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
    64
\index{classes!built-in|bold}\index{syntax!of types and terms}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
    65
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
    66
Classes are denoted by identifiers; the built-in class \cldx{logic}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    67
contains the `logical' types.  Sorts are lists of classes enclosed in
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
    68
braces~\} and \{; singleton sorts may be abbreviated by dropping the braces.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    69
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    70
\index{types!syntax of|bold}\index{sort constraints} Types are written
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    71
with a syntax like \ML's.  The built-in type \tydx{prop} is the type
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    72
of propositions.  Type variables can be constrained to particular
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    73
classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\ttlbrace
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    74
  ord, arith\ttrbrace}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    75
\[\dquotes
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
    76
\index{*:: symbol}\index{*=> symbol}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
    77
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
    78
\index{*[ symbol}\index{*] symbol}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    79
\begin{array}{lll}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    80
    \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    81
  \alpha "::" C              & \alpha :: C        & \hbox{class constraint} \\
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
    82
  \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    83
     \alpha :: \{C@1,\dots,C@n\}             & \hbox{sort constraint} \\
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    84
  \sigma " => " \tau        & \sigma\To\tau & \hbox{function type} \\
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    85
  "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau &
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    86
     [\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    87
  "(" \tau@1"," \ldots "," \tau@n ")" tycon & 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    88
     (\tau@1, \ldots, \tau@n)tycon      & \hbox{type construction}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    89
\end{array} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    90
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    91
Terms are those of the typed $\lambda$-calculus.
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
    92
\index{terms!syntax of|bold}\index{type constraints}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    93
\[\dquotes
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
    94
\index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
    95
\index{*:: symbol}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    96
\begin{array}{lll}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    97
    \multicolumn{3}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    98
  t "::" \sigma         & t :: \sigma   & \hbox{type constraint} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    99
  "\%" x "." t          & \lambda x.t   & \hbox{abstraction} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   100
  "\%" x@1\ldots x@n "." t  & \lambda x@1\ldots x@n.t & 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   101
     \hbox{curried abstraction} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   102
  t "(" u@1"," \ldots "," u@n ")" & 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   103
  t (u@1, \ldots, u@n) & \hbox{curried application}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   104
\end{array}  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   105
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   106
The theorems and rules of an object-logic are represented by theorems in
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   107
the meta-logic, which are expressed using meta-formulae.  Since the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   108
meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{}
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   109
are just terms of type~{\tt prop}.  
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   110
\index{meta-implication}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   111
\index{meta-quantifiers}\index{meta-equality}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   112
\index{*"!"! symbol}\index{*"["| symbol}\index{*"|"] symbol}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   113
\index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   114
\[\dquotes
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   115
  \begin{array}{l@{\quad}l@{\quad}l}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   116
    \multicolumn{3}{c}{\hbox{ASCII Notation for Meta-Formulae}} \\ \hline
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   117
  a " == " b    & a\equiv b &   \hbox{meta-equality} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   118
  a " =?= " b   & a\qeq b &     \hbox{flex-flex constraint} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   119
  \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   120
  "[|" \phi@1 ";" \ldots ";" \phi@n "|] ==> " \psi & 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   121
  \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   122
  "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   123
  "!!" x@1\ldots x@n "." \phi & 
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   124
  \Forall x@1. \ldots x@n.\phi & \hbox{nested quantification}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   125
  \end{array}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   126
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   127
Flex-flex constraints are meta-equalities arising from unification; they
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   128
require special treatment.  See~\S\ref{flexflex}.
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   129
\index{flex-flex constraints}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   130
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   131
\index{*Trueprop constant}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   132
Most logics define the implicit coercion $Trueprop$ from object-formulae to
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   133
propositions.  This could cause an ambiguity: in $P\Imp Q$, do the
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   134
variables $P$ and $Q$ stand for meta-formulae or object-formulae?  If the
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   135
latter, $P\Imp Q$ really abbreviates $Trueprop(P)\Imp Trueprop(Q)$.  To
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   136
prevent such ambiguities, Isabelle's syntax does not allow a meta-formula
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   137
to consist of a variable.  Variables of type~\tydx{prop} are seldom
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   138
useful, but you can make a variable stand for a meta-formula by prefixing
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   139
it with the symbol {\tt PROP}:\index{*PROP symbol}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   140
\begin{ttbox} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   141
PROP ?psi ==> PROP ?theta 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   142
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   143
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   144
Symbols of object-logics are typically rendered into {\sc ascii} as
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   145
follows:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   146
\[ \begin{tabular}{l@{\quad}l@{\quad}l}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   147
      \tt True          & $\top$        & true \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   148
      \tt False         & $\bot$        & false \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   149
      \tt $P$ \& $Q$    & $P\conj Q$    & conjunction \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   150
      \tt $P$ | $Q$     & $P\disj Q$    & disjunction \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   151
      \verb'~' $P$      & $\neg P$      & negation \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   152
      \tt $P$ --> $Q$   & $P\imp Q$     & implication \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   153
      \tt $P$ <-> $Q$   & $P\bimp Q$    & bi-implication \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   154
      \tt ALL $x\,y\,z$ .\ $P$  & $\forall x\,y\,z.P$   & for all \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   155
      \tt EX  $x\,y\,z$ .\ $P$  & $\exists x\,y\,z.P$   & there exists
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   156
   \end{tabular}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   157
\]
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   158
To illustrate the notation, consider two axioms for first-order logic:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   159
$$ \List{P; Q} \Imp P\conj Q                 \eqno(\conj I) $$
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   160
$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   161
$({\conj}I)$ translates into {\sc ascii} characters as
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   162
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   163
[| ?P; ?Q |] ==> ?P & ?Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   164
\end{ttbox}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   165
The schematic variables let unification instantiate the rule.  To avoid
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   166
cluttering logic definitions with question marks, Isabelle converts any
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   167
free variables in a rule to schematic variables; we normally declare
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   168
$({\conj}I)$ as
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   169
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   170
[| P; Q |] ==> P & Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   171
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   172
This variables convention agrees with the treatment of variables in goals.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   173
Free variables in a goal remain fixed throughout the proof.  After the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   174
proof is finished, Isabelle converts them to scheme variables in the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   175
resulting theorem.  Scheme variables in a goal may be replaced by terms
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   176
during the proof, supporting answer extraction, program synthesis, and so
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   177
forth.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   178
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   179
For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   180
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   181
[| EX x.P(x);  !!x. P(x) ==> Q |] ==> Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   182
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   183
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   184
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   185
\subsection{Basic operations on theorems}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   186
\index{theorems!basic operations on|bold}
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   187
\index{LCF system}
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   188
Meta-level theorems have the \ML{} type \mltydx{thm}.  They represent the
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   189
theorems and inference rules of object-logics.  Isabelle's meta-logic is
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   190
implemented using the {\sc lcf} approach: each meta-level inference rule is
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   191
represented by a function from theorems to theorems.  Object-level rules
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   192
are taken as axioms.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   193
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   194
The main theorem printing commands are {\tt prth}, {\tt prths} and~{\tt
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   195
  prthq}.  Of the other operations on theorems, most useful are {\tt RS}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   196
and {\tt RSN}, which perform resolution.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   197
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   198
\index{theorems!printing of}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   199
\begin{ttdescription}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   200
\item[\ttindex{prth} {\it thm};]
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   201
  pretty-prints {\it thm\/} at the terminal.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   202
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   203
\item[\ttindex{prths} {\it thms};]
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   204
  pretty-prints {\it thms}, a list of theorems.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   205
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   206
\item[\ttindex{prthq} {\it thmq};]
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   207
  pretty-prints {\it thmq}, a sequence of theorems; this is useful for
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   208
  inspecting the output of a tactic.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   209
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   210
\item[$thm1$ RS $thm2$] \index{*RS} 
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   211
  resolves the conclusion of $thm1$ with the first premise of~$thm2$.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   212
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   213
\item[$thm1$ RSN $(i,thm2)$] \index{*RSN} 
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   214
  resolves the conclusion of $thm1$ with the $i$th premise of~$thm2$.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   215
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   216
\item[\ttindex{standard} $thm$]  
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   217
  puts $thm$ into a standard format.  It also renames schematic variables
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   218
  to have subscript zero, improving readability and reducing subscript
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   219
  growth.
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   220
\end{ttdescription}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   221
The rules of a theory are normally bound to \ML\ identifiers.  Suppose we
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   222
are running an Isabelle session containing theory~\FOL, natural deduction
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   223
first-order logic.\footnote{For a listing of the \FOL{} rules and their
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   224
  \ML{} names, turn to
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   225
\iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}%
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   226
           {page~\pageref{fol-rules}}.}
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   227
Let us try an example given in~\S\ref{joining}.  We
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   228
first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   229
itself.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   230
\begin{ttbox} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   231
prth mp; 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   232
{\out [| ?P --> ?Q; ?P |] ==> ?Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   233
{\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   234
prth (mp RS mp);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   235
{\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   236
{\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   237
\end{ttbox}
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   238
User input appears in {\footnotesize\tt typewriter characters}, and output
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   239
appears in {\sltt slanted typewriter characters}.  \ML's response {\out val
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   240
  }~\ldots{} is compiler-dependent and will sometimes be suppressed.  This
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   241
session illustrates two formats for the display of theorems.  Isabelle's
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   242
top-level displays theorems as \ML{} values, enclosed in quotes.  Printing
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   243
commands like {\tt prth} omit the quotes and the surrounding {\tt val
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   244
  \ldots :\ thm}.  Ignoring their side-effects, the commands are identity
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   245
functions.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   246
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   247
To contrast {\tt RS} with {\tt RSN}, we resolve
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   248
\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   249
\begin{ttbox} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   250
conjunct1 RS mp;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   251
{\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   252
conjunct1 RSN (2,mp);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   253
{\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   254
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   255
These correspond to the following proofs:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   256
\[ \infer[({\imp}E)]{Q}{\infer[({\conj}E1)]{P\imp Q}{(P\imp Q)\conj Q@1} & P}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   257
   \qquad
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   258
   \infer[({\imp}E)]{Q}{P\imp Q & \infer[({\conj}E1)]{P}{P\conj Q@1}} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   259
\]
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   260
%
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   261
Rules can be derived by pasting other rules together.  Let us join
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   262
\tdx{spec}, which stands for~$(\forall E)$, with {\tt mp} and {\tt
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   263
  conjunct1}.  In \ML{}, the identifier~{\tt it} denotes the value just
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   264
printed.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   265
\begin{ttbox} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   266
spec;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   267
{\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   268
it RS mp;
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   269
{\out val it = "[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==>}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   270
{\out           ?Q2(?x1)" : thm}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   271
it RS conjunct1;
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   272
{\out val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==>}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   273
{\out           ?P6(?x2)" : thm}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   274
standard it;
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   275
{\out val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==>}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   276
{\out           ?Pa(?x)" : thm}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   277
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   278
By resolving $(\forall E)$ with (${\imp}E)$ and (${\conj}E1)$, we have
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   279
derived a destruction rule for formulae of the form $\forall x.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   280
P(x)\imp(Q(x)\conj R(x))$.  Used with destruct-resolution, such specialized
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   281
rules provide a way of referring to particular assumptions.
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   282
\index{assumptions!use of}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   283
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   284
\subsection{*Flex-flex constraints} \label{flexflex}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   285
\index{flex-flex constraints|bold}\index{unknowns!function}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   286
In higher-order unification, {\bf flex-flex} equations are those where both
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   287
sides begin with a function unknown, such as $\Var{f}(0)\qeq\Var{g}(0)$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   288
They admit a trivial unifier, here $\Var{f}\equiv \lambda x.\Var{a}$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   289
$\Var{g}\equiv \lambda y.\Var{a}$, where $\Var{a}$ is a new unknown.  They
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   290
admit many other unifiers, such as $\Var{f} \equiv \lambda x.\Var{g}(0)$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   291
and $\{\Var{f} \equiv \lambda x.x,\, \Var{g} \equiv \lambda x.0\}$.  Huet's
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   292
procedure does not enumerate the unifiers; instead, it retains flex-flex
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   293
equations as constraints on future unifications.  Flex-flex constraints
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   294
occasionally become attached to a proof state; more frequently, they appear
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   295
during use of {\tt RS} and~{\tt RSN}:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   296
\begin{ttbox} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   297
refl;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   298
{\out val it = "?a = ?a" : thm}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   299
exI;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   300
{\out val it = "?P(?x) ==> EX x. ?P(x)" : thm}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   301
refl RS exI;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   302
{\out val it = "?a3(?x) =?= ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)" : thm}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   303
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   304
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   305
\noindent
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   306
Renaming variables, this is $\exists x.\Var{f}(x)=\Var{g}(x)$ with
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   307
the constraint ${\Var{f}(\Var{u})\qeq\Var{g}(\Var{u})}$.  Instances
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   308
satisfying the constraint include $\exists x.\Var{f}(x)=\Var{f}(x)$ and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   309
$\exists x.x=\Var{u}$.  Calling \ttindex{flexflex_rule} removes all
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   310
constraints by applying the trivial unifier:\index{*prthq}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   311
\begin{ttbox} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   312
prthq (flexflex_rule it);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   313
{\out EX x. ?a4 = ?a4}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   314
\end{ttbox} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   315
Isabelle simplifies flex-flex equations to eliminate redundant bound
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   316
variables.  In $\lambda x\,y.\Var{f}(k(y),x) \qeq \lambda x\,y.\Var{g}(y)$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   317
there is no bound occurrence of~$x$ on the right side; thus, there will be
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   318
none on the left in a common instance of these terms.  Choosing a new
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   319
variable~$\Var{h}$, Isabelle assigns $\Var{f}\equiv \lambda u\,v.?h(u)$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   320
simplifying the left side to $\lambda x\,y.\Var{h}(k(y))$.  Dropping $x$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   321
from the equation leaves $\lambda y.\Var{h}(k(y)) \qeq \lambda
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   322
y.\Var{g}(y)$.  By $\eta$-conversion, this simplifies to the assignment
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   323
$\Var{g}\equiv\lambda y.?h(k(y))$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   324
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   325
\begin{warn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   326
\ttindex{RS} and \ttindex{RSN} fail (by raising exception {\tt THM}) unless
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   327
the resolution delivers {\bf exactly one} resolvent.  For multiple results,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   328
use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists.  The
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   329
following example uses \ttindex{read_instantiate} to create an instance
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   330
of \tdx{refl} containing no schematic variables.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   331
\begin{ttbox} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   332
val reflk = read_instantiate [("a","k")] refl;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   333
{\out val reflk = "k = k" : thm}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   334
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   335
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   336
\noindent
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   337
A flex-flex constraint is no longer possible; resolution does not find a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   338
unique unifier:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   339
\begin{ttbox} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   340
reflk RS exI;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   341
{\out uncaught exception THM}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   342
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   343
Using \ttindex{RL} this time, we discover that there are four unifiers, and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   344
four resolvents:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   345
\begin{ttbox} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   346
[reflk] RL [exI];
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   347
{\out val it = ["EX x. x = x", "EX x. k = x",}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   348
{\out           "EX x. x = k", "EX x. k = k"] : thm list}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   349
\end{ttbox} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   350
\end{warn}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   351
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   352
\index{forward proof|)}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   353
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   354
\section{Backward proof}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   355
Although {\tt RS} and {\tt RSN} are fine for simple forward reasoning,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   356
large proofs require tactics.  Isabelle provides a suite of commands for
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   357
conducting a backward proof using tactics.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   358
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   359
\subsection{The basic tactics}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   360
The tactics {\tt assume_tac}, {\tt
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   361
resolve_tac}, {\tt eresolve_tac}, and {\tt dresolve_tac} suffice for most
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   362
single-step proofs.  Although {\tt eresolve_tac} and {\tt dresolve_tac} are
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   363
not strictly necessary, they simplify proofs involving elimination and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   364
destruction rules.  All the tactics act on a subgoal designated by a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   365
positive integer~$i$, failing if~$i$ is out of range.  The resolution
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   366
tactics try their list of theorems in left-to-right order.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   367
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   368
\begin{ttdescription}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   369
\item[\ttindex{assume_tac} {\it i}] \index{tactics!assumption}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   370
  is the tactic that attempts to solve subgoal~$i$ by assumption.  Proof by
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   371
  assumption is not a trivial step; it can falsify other subgoals by
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   372
  instantiating shared variables.  There may be several ways of solving the
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   373
  subgoal by assumption.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   374
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   375
\item[\ttindex{resolve_tac} {\it thms} {\it i}]\index{tactics!resolution}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   376
  is the basic resolution tactic, used for most proof steps.  The $thms$
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   377
  represent object-rules, which are resolved against subgoal~$i$ of the
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   378
  proof state.  For each rule, resolution forms next states by unifying the
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   379
  conclusion with the subgoal and inserting instantiated premises in its
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   380
  place.  A rule can admit many higher-order unifiers.  The tactic fails if
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   381
  none of the rules generates next states.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   382
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   383
\item[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elim-resolution}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   384
  performs elim-resolution.  Like {\tt resolve_tac~{\it thms}~{\it i\/}}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   385
  followed by {\tt assume_tac~{\it i}}, it applies a rule then solves its
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   386
  first premise by assumption.  But {\tt eresolve_tac} additionally deletes
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   387
  that assumption from any subgoals arising from the resolution.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   388
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   389
\item[\ttindex{dresolve_tac} {\it thms} {\it i}]
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   390
  \index{forward proof}\index{destruct-resolution}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   391
  performs destruct-resolution with the~$thms$, as described
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   392
  in~\S\ref{destruct}.  It is useful for forward reasoning from the
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   393
  assumptions.
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   394
\end{ttdescription}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   395
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   396
\subsection{Commands for backward proof}
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   397
\index{proofs!commands for}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   398
Tactics are normally applied using the subgoal module, which maintains a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   399
proof state and manages the proof construction.  It allows interactive
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   400
backtracking through the proof space, going away to prove lemmas, etc.; of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   401
its many commands, most important are the following:
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   402
\begin{ttdescription}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   403
\item[\ttindex{goal} {\it theory} {\it formula}; ] 
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   404
begins a new proof, where $theory$ is usually an \ML\ identifier
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   405
and the {\it formula\/} is written as an \ML\ string.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   406
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   407
\item[\ttindex{by} {\it tactic}; ] 
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   408
applies the {\it tactic\/} to the current proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   409
state, raising an exception if the tactic fails.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   410
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   411
\item[\ttindex{undo}(); ]
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   412
  reverts to the previous proof state.  Undo can be repeated but cannot be
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   413
  undone.  Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   414
  causes \ML\ to echo the value of that function.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   415
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   416
\item[\ttindex{result}();]
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   417
returns the theorem just proved, in a standard format.  It fails if
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   418
unproved subgoals are left, etc.
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   419
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   420
\item[\ttindex{qed} {\it name};] is the usual way of ending a proof.
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   421
  It gets the theorem using {\tt result}, stores it in Isabelle's
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   422
  theorem database and binds it to an \ML{} identifier.
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   423
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   424
\end{ttdescription}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   425
The commands and tactics given above are cumbersome for interactive use.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   426
Although our examples will use the full commands, you may prefer Isabelle's
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   427
shortcuts:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   428
\begin{center} \tt
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   429
\index{*br} \index{*be} \index{*bd} \index{*ba}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   430
\begin{tabular}{l@{\qquad\rm abbreviates\qquad}l}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   431
    ba {\it i};           & by (assume_tac {\it i}); \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   432
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   433
    br {\it thm} {\it i}; & by (resolve_tac [{\it thm}] {\it i}); \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   434
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   435
    be {\it thm} {\it i}; & by (eresolve_tac [{\it thm}] {\it i}); \\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   436
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   437
    bd {\it thm} {\it i}; & by (dresolve_tac [{\it thm}] {\it i}); 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   438
\end{tabular}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   439
\end{center}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   440
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   441
\subsection{A trivial example in propositional logic}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   442
\index{examples!propositional}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   443
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   444
Directory {\tt FOL} of the Isabelle distribution defines the theory of
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   445
first-order logic.  Let us try the example from \S\ref{prop-proof},
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   446
entering the goal $P\disj P\imp P$ in that theory.\footnote{To run these
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   447
  examples, see the file {\tt FOL/ex/intro.ML}.  The files {\tt README} and
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   448
  {\tt Makefile} on the directories {\tt Pure} and {\tt FOL} explain how to
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   449
  build first-order logic.}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   450
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   451
goal FOL.thy "P|P --> P"; 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   452
{\out Level 0} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   453
{\out P | P --> P} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   454
{\out 1. P | P --> P} 
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   455
\end{ttbox}\index{level of a proof}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   456
Isabelle responds by printing the initial proof state, which has $P\disj
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   457
P\imp P$ as the main goal and the only subgoal.  The {\bf level} of the
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   458
state is the number of {\tt by} commands that have been applied to reach
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   459
it.  We now use \ttindex{resolve_tac} to apply the rule \tdx{impI},
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   460
or~$({\imp}I)$, to subgoal~1:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   461
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   462
by (resolve_tac [impI] 1); 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   463
{\out Level 1} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   464
{\out P | P --> P} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   465
{\out 1. P | P ==> P}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   466
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   467
In the new proof state, subgoal~1 is $P$ under the assumption $P\disj P$.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   468
(The meta-implication {\tt==>} indicates assumptions.)  We apply
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   469
\tdx{disjE}, or~(${\disj}E)$, to that subgoal:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   470
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   471
by (resolve_tac [disjE] 1); 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   472
{\out Level 2} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   473
{\out P | P --> P} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   474
{\out 1. P | P ==> ?P1 | ?Q1} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   475
{\out 2. [| P | P; ?P1 |] ==> P} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   476
{\out 3. [| P | P; ?Q1 |] ==> P}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   477
\end{ttbox}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   478
At Level~2 there are three subgoals, each provable by assumption.  We
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   479
deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   480
\ttindex{assume_tac}.  This affects subgoal~1, updating {\tt?Q1} to~{\tt
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   481
  P}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   482
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   483
by (assume_tac 3); 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   484
{\out Level 3} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   485
{\out P | P --> P} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   486
{\out 1. P | P ==> ?P1 | P} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   487
{\out 2. [| P | P; ?P1 |] ==> P}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   488
\end{ttbox}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   489
Next we tackle subgoal~2, instantiating {\tt?P1} to~{\tt P} in subgoal~1.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   490
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   491
by (assume_tac 2); 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   492
{\out Level 4} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   493
{\out P | P --> P} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   494
{\out 1. P | P ==> P | P}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   495
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   496
Lastly we prove the remaining subgoal by assumption:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   497
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   498
by (assume_tac 1); 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   499
{\out Level 5} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   500
{\out P | P --> P} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   501
{\out No subgoals!}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   502
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   503
Isabelle tells us that there are no longer any subgoals: the proof is
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   504
complete.  Calling {\tt qed} stores the theorem.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   505
\begin{ttbox}
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   506
qed "mythm";
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   507
{\out val mythm = "?P | ?P --> ?P" : thm} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   508
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   509
Isabelle has replaced the free variable~{\tt P} by the scheme
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   510
variable~{\tt?P}\@.  Free variables in the proof state remain fixed
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   511
throughout the proof.  Isabelle finally converts them to scheme variables
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   512
so that the resulting theorem can be instantiated with any formula.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   513
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   514
As an exercise, try doing the proof as in \S\ref{prop-proof}, observing how
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   515
instantiations affect the proof state.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   516
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   517
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   518
\subsection{Part of a distributive law}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   519
\index{examples!propositional}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   520
To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac}
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   521
and the tactical {\tt REPEAT}, let us prove part of the distributive
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   522
law 
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   523
\[ (P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R). \]
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   524
We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   525
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   526
goal FOL.thy "(P & Q) | R  --> (P | R)";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   527
{\out Level 0}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   528
{\out P & Q | R --> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   529
{\out  1. P & Q | R --> P | R}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   530
\ttbreak
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   531
by (resolve_tac [impI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   532
{\out Level 1}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   533
{\out P & Q | R --> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   534
{\out  1. P & Q | R ==> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   535
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   536
Previously we applied~(${\disj}E)$ using {\tt resolve_tac}, but 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   537
\ttindex{eresolve_tac} deletes the assumption after use.  The resulting proof
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   538
state is simpler.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   539
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   540
by (eresolve_tac [disjE] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   541
{\out Level 2}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   542
{\out P & Q | R --> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   543
{\out  1. P & Q ==> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   544
{\out  2. R ==> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   545
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   546
Using \ttindex{dresolve_tac}, we can apply~(${\conj}E1)$ to subgoal~1,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   547
replacing the assumption $P\conj Q$ by~$P$.  Normally we should apply the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   548
rule~(${\conj}E)$, given in~\S\ref{destruct}.  That is an elimination rule
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   549
and requires {\tt eresolve_tac}; it would replace $P\conj Q$ by the two
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   550
assumptions~$P$ and~$Q$.  Because the present example does not need~$Q$, we
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   551
may try out {\tt dresolve_tac}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   552
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   553
by (dresolve_tac [conjunct1] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   554
{\out Level 3}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   555
{\out P & Q | R --> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   556
{\out  1. P ==> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   557
{\out  2. R ==> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   558
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   559
The next two steps apply~(${\disj}I1$) and~(${\disj}I2$) in an obvious manner.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   560
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   561
by (resolve_tac [disjI1] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   562
{\out Level 4}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   563
{\out P & Q | R --> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   564
{\out  1. P ==> P}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   565
{\out  2. R ==> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   566
\ttbreak
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   567
by (resolve_tac [disjI2] 2);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   568
{\out Level 5}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   569
{\out P & Q | R --> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   570
{\out  1. P ==> P}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   571
{\out  2. R ==> R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   572
\end{ttbox}
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   573
Two calls of {\tt assume_tac} can finish the proof.  The
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   574
tactical~\ttindex{REPEAT} here expresses a tactic that calls {\tt assume_tac~1}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   575
as many times as possible.  We can restrict attention to subgoal~1 because
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   576
the other subgoals move up after subgoal~1 disappears.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   577
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   578
by (REPEAT (assume_tac 1));
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   579
{\out Level 6}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   580
{\out P & Q | R --> P | R}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   581
{\out No subgoals!}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   582
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   583
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   584
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   585
\section{Quantifier reasoning}
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   586
\index{quantifiers}\index{parameters}\index{unknowns}\index{unknowns!function}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   587
This section illustrates how Isabelle enforces quantifier provisos.
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   588
Suppose that $x$, $y$ and~$z$ are parameters of a subgoal.  Quantifier
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   589
rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   590
unknown.  Instantiating $\Var{f}$ to $\lambda x\,z.t$ has the effect of
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   591
replacing~$\Var{f}(x,z)$ by~$t$, where the term~$t$ may contain free
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   592
occurrences of~$x$ and~$z$.  On the other hand, no instantiation
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   593
of~$\Var{f}$ can replace~$\Var{f}(x,z)$ by a term containing free
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   594
occurrences of~$y$, since parameters are bound variables.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   595
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   596
\subsection{Two quantifier proofs: a success and a failure}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   597
\index{examples!with quantifiers}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   598
Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   599
attempted proof of the non-theorem $\exists y.\forall x.x=y$.  The former
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   600
proof succeeds, and the latter fails, because of the scope of quantified
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 331
diff changeset
   601
variables~\cite{paulson-found}.  Unification helps even in these trivial
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   602
proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   603
but we need never say so. This choice is forced by the reflexive law for
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   604
equality, and happens automatically.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   605
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   606
\paragraph{The successful proof.}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   607
The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   608
$(\forall I)$ and~$(\exists I)$.  We state the goal and apply $(\forall I)$:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   609
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   610
goal FOL.thy "ALL x. EX y. x=y";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   611
{\out Level 0}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   612
{\out ALL x. EX y. x = y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   613
{\out  1. ALL x. EX y. x = y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   614
\ttbreak
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   615
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   616
{\out Level 1}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   617
{\out ALL x. EX y. x = y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   618
{\out  1. !!x. EX y. x = y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   619
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   620
The variable~{\tt x} is no longer universally quantified, but is a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   621
parameter in the subgoal; thus, it is universally quantified at the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   622
meta-level.  The subgoal must be proved for all possible values of~{\tt x}.
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   623
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   624
To remove the existential quantifier, we apply the rule $(\exists I)$:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   625
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   626
by (resolve_tac [exI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   627
{\out Level 2}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   628
{\out ALL x. EX y. x = y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   629
{\out  1. !!x. x = ?y1(x)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   630
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   631
The bound variable {\tt y} has become {\tt?y1(x)}.  This term consists of
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   632
the function unknown~{\tt?y1} applied to the parameter~{\tt x}.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   633
Instances of {\tt?y1(x)} may or may not contain~{\tt x}.  We resolve the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   634
subgoal with the reflexivity axiom.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   635
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   636
by (resolve_tac [refl] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   637
{\out Level 3}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   638
{\out ALL x. EX y. x = y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   639
{\out No subgoals!}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   640
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   641
Let us consider what has happened in detail.  The reflexivity axiom is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   642
lifted over~$x$ to become $\Forall x.\Var{f}(x)=\Var{f}(x)$, which is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   643
unified with $\Forall x.x=\Var{y@1}(x)$.  The function unknowns $\Var{f}$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   644
and~$\Var{y@1}$ are both instantiated to the identity function, and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   645
$x=\Var{y@1}(x)$ collapses to~$x=x$ by $\beta$-reduction.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   646
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   647
\paragraph{The unsuccessful proof.}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   648
We state the goal $\exists y.\forall x.x=y$, which is not a theorem, and
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   649
try~$(\exists I)$:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   650
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   651
goal FOL.thy "EX y. ALL x. x=y";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   652
{\out Level 0}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   653
{\out EX y. ALL x. x = y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   654
{\out  1. EX y. ALL x. x = y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   655
\ttbreak
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   656
by (resolve_tac [exI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   657
{\out Level 1}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   658
{\out EX y. ALL x. x = y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   659
{\out  1. ALL x. x = ?y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   660
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   661
The unknown {\tt ?y} may be replaced by any term, but this can never
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   662
introduce another bound occurrence of~{\tt x}.  We now apply~$(\forall I)$:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   663
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   664
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   665
{\out Level 2}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   666
{\out EX y. ALL x. x = y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   667
{\out  1. !!x. x = ?y}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   668
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   669
Compare our position with the previous Level~2.  Instead of {\tt?y1(x)} we
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   670
have~{\tt?y}, whose instances may not contain the bound variable~{\tt x}.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   671
The reflexivity axiom does not unify with subgoal~1.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   672
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   673
by (resolve_tac [refl] 1);
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   674
{\out by: tactic failed}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   675
\end{ttbox}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   676
There can be no proof of $\exists y.\forall x.x=y$ by the soundness of
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   677
first-order logic.  I have elsewhere proved the faithfulness of Isabelle's
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 331
diff changeset
   678
encoding of first-order logic~\cite{paulson-found}; there could, of course, be
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   679
faults in the implementation.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   680
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   681
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   682
\subsection{Nested quantifiers}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   683
\index{examples!with quantifiers}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   684
Multiple quantifiers create complex terms.  Proving 
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   685
\[ (\forall x\,y.P(x,y)) \imp (\forall z\,w.P(w,z)) \] 
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   686
will demonstrate how parameters and unknowns develop.  If they appear in
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   687
the wrong order, the proof will fail.
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   688
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   689
This section concludes with a demonstration of {\tt REPEAT}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   690
and~{\tt ORELSE}.  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   691
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   692
goal FOL.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   693
{\out Level 0}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   694
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   695
{\out  1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   696
\ttbreak
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   697
by (resolve_tac [impI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   698
{\out Level 1}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   699
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   700
{\out  1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   701
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   702
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   703
\paragraph{The wrong approach.}
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   704
Using {\tt dresolve_tac}, we apply the rule $(\forall E)$, bound to the
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   705
\ML\ identifier \tdx{spec}.  Then we apply $(\forall I)$.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   706
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   707
by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   708
{\out Level 2}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   709
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   710
{\out  1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   711
\ttbreak
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   712
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   713
{\out Level 3}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   714
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   715
{\out  1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   716
\end{ttbox}
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   717
The unknown {\tt ?x1} and the parameter {\tt z} have appeared.  We again
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   718
apply $(\forall E)$ and~$(\forall I)$.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   719
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   720
by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   721
{\out Level 4}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   722
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   723
{\out  1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   724
\ttbreak
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   725
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   726
{\out Level 5}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   727
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   728
{\out  1. !!z w. P(?x1,?y3(z)) ==> P(w,z)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   729
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   730
The unknown {\tt ?y3} and the parameter {\tt w} have appeared.  Each
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   731
unknown is applied to the parameters existing at the time of its creation;
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   732
instances of~{\tt ?x1} cannot contain~{\tt z} or~{\tt w}, while instances
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   733
of {\tt?y3(z)} can only contain~{\tt z}.  Due to the restriction on~{\tt ?x1},
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   734
proof by assumption will fail.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   735
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   736
by (assume_tac 1);
3103
98af809fee46 misc updates, tuning, cleanup;
wenzelm
parents: 1878
diff changeset
   737
{\out by: tactic failed}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   738
{\out uncaught exception ERROR}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   739
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   740
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   741
\paragraph{The right approach.}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   742
To do this proof, the rules must be applied in the correct order.
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   743
Parameters should be created before unknowns.  The
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   744
\ttindex{choplev} command returns to an earlier stage of the proof;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   745
let us return to the result of applying~$({\imp}I)$:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   746
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   747
choplev 1;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   748
{\out Level 1}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   749
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   750
{\out  1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   751
\end{ttbox}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   752
Previously we made the mistake of applying $(\forall E)$ before $(\forall I)$.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   753
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   754
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   755
{\out Level 2}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   756
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   757
{\out  1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   758
\ttbreak
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   759
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   760
{\out Level 3}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   761
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   762
{\out  1. !!z w. ALL x y. P(x,y) ==> P(w,z)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   763
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   764
The parameters {\tt z} and~{\tt w} have appeared.  We now create the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   765
unknowns:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   766
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   767
by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   768
{\out Level 4}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   769
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   770
{\out  1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   771
\ttbreak
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   772
by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   773
{\out Level 5}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   774
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   775
{\out  1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   776
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   777
Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   778
z} and~{\tt w}:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   779
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   780
by (assume_tac 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   781
{\out Level 6}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   782
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   783
{\out No subgoals!}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   784
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   785
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   786
\paragraph{A one-step proof using tacticals.}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   787
\index{tacticals} \index{examples!of tacticals} 
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   788
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   789
Repeated application of rules can be effective, but the rules should be
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   790
attempted in the correct order.  Let us return to the original goal using
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   791
\ttindex{choplev}:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   792
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   793
choplev 0;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   794
{\out Level 0}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   795
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   796
{\out  1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   797
\end{ttbox}
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   798
As we have just seen, \tdx{allI} should be attempted
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   799
before~\tdx{spec}, while \ttindex{assume_tac} generally can be
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   800
attempted first.  Such priorities can easily be expressed
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   801
using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   802
\begin{ttbox}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   803
by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   804
     ORELSE dresolve_tac [spec] 1));
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   805
{\out Level 1}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   806
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   807
{\out No subgoals!}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   808
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   809
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   810
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   811
\subsection{A realistic quantifier proof}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   812
\index{examples!with quantifiers}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   813
To see the practical use of parameters and unknowns, let us prove half of
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   814
the equivalence 
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   815
\[ (\forall x. P(x) \imp Q) \,\bimp\, ((\exists x. P(x)) \imp Q). \]
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   816
We state the left-to-right half to Isabelle in the normal way.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   817
Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   818
use {\tt REPEAT}:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   819
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   820
goal FOL.thy "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   821
{\out Level 0}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   822
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   823
{\out  1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   824
\ttbreak
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   825
by (REPEAT (resolve_tac [impI] 1));
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   826
{\out Level 1}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   827
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   828
{\out  1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   829
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   830
We can eliminate the universal or the existential quantifier.  The
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   831
existential quantifier should be eliminated first, since this creates a
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   832
parameter.  The rule~$(\exists E)$ is bound to the
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   833
identifier~\tdx{exE}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   834
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   835
by (eresolve_tac [exE] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   836
{\out Level 2}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   837
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   838
{\out  1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   839
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   840
The only possibility now is $(\forall E)$, a destruction rule.  We use 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   841
\ttindex{dresolve_tac}, which discards the quantified assumption; it is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   842
only needed once.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   843
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   844
by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   845
{\out Level 3}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   846
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   847
{\out  1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   848
\end{ttbox}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   849
Because we applied $(\exists E)$ before $(\forall E)$, the unknown
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   850
term~{\tt?x3(x)} may depend upon the parameter~{\tt x}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   851
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   852
Although $({\imp}E)$ is a destruction rule, it works with 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   853
\ttindex{eresolve_tac} to perform backward chaining.  This technique is
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   854
frequently useful.  
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   855
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   856
by (eresolve_tac [mp] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   857
{\out Level 4}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   858
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   859
{\out  1. !!x. P(x) ==> P(?x3(x))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   860
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   861
The tactic has reduced~{\tt Q} to~{\tt P(?x3(x))}, deleting the
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   862
implication.  The final step is trivial, thanks to the occurrence of~{\tt x}.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   863
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   864
by (assume_tac 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   865
{\out Level 5}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   866
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   867
{\out No subgoals!}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   868
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   869
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   870
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   871
\subsection{The classical reasoner}
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   872
\index{classical reasoner}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   873
Although Isabelle cannot compete with fully automatic theorem provers, it
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   874
provides enough automation to tackle substantial examples.  The classical
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   875
reasoner can be set up for any classical natural deduction logic;
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   876
see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   877
        {Chap.\ts\ref{chap:classical}}. 
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   878
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   879
Rules are packaged into {\bf classical sets}.  The classical reasoner
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   880
provides several tactics, which apply rules using naive algorithms.
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   881
Unification handles quantifiers as shown above.  The most useful tactic
3127
4cc2fe62f7c3 New acknowledgements; no Fast_tac
paulson
parents: 3103
diff changeset
   882
is~\ttindex{Blast_tac}.  
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   883
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   884
Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}.  (The
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   885
backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   886
sequence, to break the long string over two lines.)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   887
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   888
goal FOL.thy "(EX y. ALL x. J(y,x) <-> ~J(x,x))  \ttback
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   889
\ttback       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   890
{\out Level 0}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   891
{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   892
{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   893
{\out  1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   894
{\out     ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   895
\end{ttbox}
3127
4cc2fe62f7c3 New acknowledgements; no Fast_tac
paulson
parents: 3103
diff changeset
   896
\ttindex{Blast_tac} proves subgoal~1 at a stroke.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   897
\begin{ttbox}
3127
4cc2fe62f7c3 New acknowledgements; no Fast_tac
paulson
parents: 3103
diff changeset
   898
by (Blast_tac 1);
4cc2fe62f7c3 New acknowledgements; no Fast_tac
paulson
parents: 3103
diff changeset
   899
{\out Depth = 0}
4cc2fe62f7c3 New acknowledgements; no Fast_tac
paulson
parents: 3103
diff changeset
   900
{\out Depth = 1}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   901
{\out Level 1}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   902
{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   903
{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   904
{\out No subgoals!}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   905
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   906
Sceptics may examine the proof by calling the package's single-step
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   907
tactics, such as~{\tt step_tac}.  This would take up much space, however,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   908
so let us proceed to the next example:
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   909
\begin{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   910
goal FOL.thy "ALL x. P(x,f(x)) <-> \ttback
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   911
\ttback       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   912
{\out Level 0}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   913
{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   914
{\out  1. ALL x. P(x,f(x)) <->}
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 105
diff changeset
   915
{\out     (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   916
\end{ttbox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   917
Again, subgoal~1 succumbs immediately.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   918
\begin{ttbox}
3127
4cc2fe62f7c3 New acknowledgements; no Fast_tac
paulson
parents: 3103
diff changeset
   919
by (Blast_tac 1);
4cc2fe62f7c3 New acknowledgements; no Fast_tac
paulson
parents: 3103
diff changeset
   920
{\out Depth = 0}
4cc2fe62f7c3 New acknowledgements; no Fast_tac
paulson
parents: 3103
diff changeset
   921
{\out Depth = 1}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   922
{\out Level 1}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   923
{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   924
{\out No subgoals!}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   925
\end{ttbox}
331
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   926
The classical reasoner is not restricted to the usual logical connectives.
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   927
The natural deduction rules for unions and intersections resemble those for
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   928
disjunction and conjunction.  The rules for infinite unions and
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   929
intersections resemble those for quantifiers.  Given such rules, the classical
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   930
reasoner is effective for reasoning in set theory.
13660d5f6a77 final Springer copy
lcp
parents: 311
diff changeset
   931