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