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