doc-src/Ref/thm.tex
author obua
Fri, 16 Sep 2005 21:02:15 +0200
changeset 17440 df77edc4f5d0
parent 11625 74cdf24724ea
child 30184 37969710e61f
permissions -rw-r--r--
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
\chapter{Theorems and Forward Proof}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\index{theorems|(}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
     4
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
     5
Theorems, which represent the axioms, theorems and rules of
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
     6
object-logics, have type \mltydx{thm}.  This chapter begins by
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
     7
describing operations that print theorems and that join them in
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
     8
forward proof.  Most theorem operations are intended for advanced
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
     9
applications, such as programming new proof procedures.  Many of these
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
    10
operations refer to signatures, certified terms and certified types,
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
    11
which have the \ML{} types {\tt Sign.sg}, {\tt cterm} and {\tt ctyp}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
    12
and are discussed in Chapter~\ref{theories}.  Beginning users should
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
    13
ignore such complexities --- and skip all but the first section of
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
    14
this chapter.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
The theorem operations do not print error messages.  Instead, they raise
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    17
exception~\xdx{THM}\@.  Use \ttindex{print_exn} to display
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
exceptions nicely:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
allI RS mp  handle e => print_exn e;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
{\out Exception THM raised:}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
{\out RSN: no unifiers -- premise 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
{\out (!!x. ?P(x)) ==> ALL x. ?P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
{\out [| ?P --> ?Q; ?P |] ==> ?Q}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
{\out}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
{\out uncaught exception THM}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
\section{Basic operations on theorems}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
\subsection{Pretty-printing a theorem}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    32
\index{theorems!printing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
\begin{ttbox} 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    34
prth          : thm -> thm
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    35
prths         : thm list -> thm list
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
    36
prthq         : thm Seq.seq -> thm Seq.seq
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    37
print_thm     : thm -> unit
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    38
print_goals   : int -> thm -> unit
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    39
string_of_thm : thm -> string
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    41
The first three commands are for interactive use.  They are identity
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    42
functions that display, then return, their argument.  The \ML{} identifier
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    43
{\tt it} will refer to the value just displayed.
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    44
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    45
The others are for use in programs.  Functions with result type {\tt unit}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    46
are convenient for imperative programming.
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    47
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    48
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
\item[\ttindexbold{prth} {\it thm}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
prints {\it thm\/} at the terminal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
\item[\ttindexbold{prths} {\it thms}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
prints {\it thms}, a list of theorems.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
\item[\ttindexbold{prthq} {\it thmq}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
prints {\it thmq}, a sequence of theorems.  It is useful for inspecting
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
the output of a tactic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
\item[\ttindexbold{print_thm} {\it thm}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
prints {\it thm\/} at the terminal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
\item[\ttindexbold{print_goals} {\it limit\/} {\it thm}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
prints {\it thm\/} in goal style, with the premises as subgoals.  It prints
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
at most {\it limit\/} subgoals.  The subgoal module calls {\tt print_goals}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
to display proof states.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
\item[\ttindexbold{string_of_thm} {\it thm}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
converts {\it thm\/} to a string.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    69
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    72
\subsection{Forward proof: joining rules by resolution}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    73
\index{theorems!joining by resolution}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    74
\index{resolution}\index{forward proof}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
\begin{ttbox} 
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
    76
RSN : thm * (int * thm) -> thm                 \hfill\textbf{infix}
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
    77
RS  : thm * thm -> thm                         \hfill\textbf{infix}
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
    78
MRS : thm list * thm -> thm                    \hfill\textbf{infix}
9288
06a55195741b infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents: 9258
diff changeset
    79
OF  : thm * thm list -> thm                    \hfill\textbf{infix}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
    80
RLN : thm list * (int * thm list) -> thm list  \hfill\textbf{infix}
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
    81
RL  : thm list * thm list -> thm list          \hfill\textbf{infix}
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
    82
MRL : thm list list * thm list -> thm list     \hfill\textbf{infix}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    84
Joining rules together is a simple way of deriving new rules.  These
876
5c18634db55d Under RS added cross reference to bind_thm
lcp
parents: 866
diff changeset
    85
functions are especially useful with destruction rules.  To store
5c18634db55d Under RS added cross reference to bind_thm
lcp
parents: 866
diff changeset
    86
the result in the theorem database, use \ttindex{bind_thm}
5c18634db55d Under RS added cross reference to bind_thm
lcp
parents: 866
diff changeset
    87
(\S\ref{ExtractingAndStoringTheProvedTheorem}). 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    88
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
\item[\tt$thm@1$ RSN $(i,thm@2)$] \indexbold{*RSN} 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    90
  resolves the conclusion of $thm@1$ with the $i$th premise of~$thm@2$.
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    91
  Unless there is precisely one resolvent it raises exception
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    92
  \xdx{THM}; in that case, use {\tt RLN}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
\item[\tt$thm@1$ RS $thm@2$] \indexbold{*RS} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
abbreviates \hbox{\tt$thm@1$ RSN $(1,thm@2)$}.  Thus, it resolves the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
conclusion of $thm@1$ with the first premise of~$thm@2$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
\item[\tt {$[thm@1,\ldots,thm@n]$} MRS $thm$] \indexbold{*MRS} 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
    99
  uses {\tt RSN} to resolve $thm@i$ against premise~$i$ of $thm$, for
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
  $i=n$, \ldots,~1.  This applies $thm@n$, \ldots, $thm@1$ to the first $n$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
  premises of $thm$.  Because the theorems are used from right to left, it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
  does not matter if the $thm@i$ create new premises.  {\tt MRS} is useful
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
  for expressing proof trees.
9288
06a55195741b infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents: 9258
diff changeset
   104
  
06a55195741b infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents: 9258
diff changeset
   105
\item[\tt {$thm$ OF $[thm@1,\ldots,thm@n]$}] \indexbold{*OF} is the same as
06a55195741b infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents: 9258
diff changeset
   106
  \texttt{$[thm@1,\ldots,thm@n]$ MRS $thm$}, with slightly more readable
06a55195741b infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents: 9258
diff changeset
   107
  argument order, though.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
151
c5e636ca6576 corrected some obvious errors;
wenzelm
parents: 104
diff changeset
   109
\item[\tt$thms@1$ RLN $(i,thms@2)$] \indexbold{*RLN} 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   110
  joins lists of theorems.  For every $thm@1$ in $thms@1$ and $thm@2$ in
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   111
  $thms@2$, it resolves the conclusion of $thm@1$ with the $i$th premise
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   112
  of~$thm@2$, accumulating the results. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
151
c5e636ca6576 corrected some obvious errors;
wenzelm
parents: 104
diff changeset
   114
\item[\tt$thms@1$ RL $thms@2$] \indexbold{*RL} 
c5e636ca6576 corrected some obvious errors;
wenzelm
parents: 104
diff changeset
   115
abbreviates \hbox{\tt$thms@1$ RLN $(1,thms@2)$}. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
\item[\tt {$[thms@1,\ldots,thms@n]$} MRL $thms$] \indexbold{*MRL} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
is analogous to {\tt MRS}, but combines theorem lists rather than theorems.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
It too is useful for expressing proof trees.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   120
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
\subsection{Expanding definitions in theorems}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   124
\index{meta-rewriting!in theorems}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
rewrite_rule       : thm list -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
rewrite_goals_rule : thm list -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   129
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
\item[\ttindexbold{rewrite_rule} {\it defs} {\it thm}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
unfolds the {\it defs} throughout the theorem~{\it thm}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
\item[\ttindexbold{rewrite_goals_rule} {\it defs} {\it thm}]  
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   134
unfolds the {\it defs} in the premises of~{\it thm}, but it leaves the
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   135
conclusion unchanged.  This rule is the basis for \ttindex{rewrite_goals_tac},
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   136
but it serves little purpose in forward proof.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   137
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
4383
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   140
\subsection{Instantiating unknowns in a theorem} \label{sec:instantiate}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   141
\index{instantiation}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   142
\begin{alltt}\footnotesize
4383
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   143
read_instantiate    :                (string*string) list -> thm -> thm
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   144
read_instantiate_sg :     Sign.sg -> (string*string) list -> thm -> thm
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   145
cterm_instantiate   :                  (cterm*cterm) list -> thm -> thm
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   146
instantiate'      : ctyp option list -> cterm option list -> thm -> thm
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   147
\end{alltt}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
These meta-rules instantiate type and term unknowns in a theorem.  They are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
occasionally useful.  They can prevent difficulties with higher-order
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
unification, and define specialized versions of rules.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   151
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
\item[\ttindexbold{read_instantiate} {\it insts} {\it thm}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
processes the instantiations {\it insts} and instantiates the rule~{\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
thm}.  The processing of instantiations is described
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   155
in \S\ref{res_inst_tac}, under {\tt res_inst_tac}.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
Use {\tt res_inst_tac}, not {\tt read_instantiate}, to instantiate a rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
and refine a particular subgoal.  The tactic allows instantiation by the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
subgoal's parameters, and reads the instantiations using the signature
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   160
associated with the proof state.
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   161
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   162
Use {\tt read_instantiate_sg} below if {\it insts\/} appears to be treated
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   163
incorrectly.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   165
\item[\ttindexbold{read_instantiate_sg} {\it sg} {\it insts} {\it thm}]
4597
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4383
diff changeset
   166
  is like \texttt{read_instantiate {\it insts}~{\it thm}}, but it reads
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   167
  the instantiations under signature~{\it sg}.  This is necessary to
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   168
  instantiate a rule from a general theory, such as first-order logic,
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   169
  using the notation of some specialized theory.  Use the function {\tt
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   170
    sign_of} to get a theory's signature.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
\item[\ttindexbold{cterm_instantiate} {\it ctpairs} {\it thm}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
is similar to {\tt read_instantiate}, but the instantiations are provided
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
as pairs of certified terms, not as strings to be read.
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   175
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   176
\item[\ttindexbold{instantiate'} {\it ctyps} {\it cterms} {\it thm}]
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   177
  instantiates {\it thm} according to the positional arguments {\it
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   178
    ctyps} and {\it cterms}.  Counting from left to right, schematic
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   179
  variables $?x$ are either replaced by $t$ for any argument
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   180
  \texttt{Some\(\;t\)}, or left unchanged in case of \texttt{None} or
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   181
  if the end of the argument list is encountered.  Types are
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   182
  instantiated before terms.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   183
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   184
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 332
diff changeset
   187
\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   188
\index{theorems!standardizing}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
\begin{ttbox} 
8969
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   190
standard         :               thm -> thm
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   191
zero_var_indexes :               thm -> thm
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   192
make_elim        :               thm -> thm
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   193
rule_by_tactic   :     tactic -> thm -> thm
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   194
rotate_prems     :        int -> thm -> thm
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   195
permute_prems    : int -> int -> thm -> thm
11163
14732e3eaa6e added rearrange_prems
oheimb
parents: 9499
diff changeset
   196
rearrange_prems  :   int list -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   198
\begin{ttdescription}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   199
\item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   200
  of object-rules.  It discharges all meta-assumptions, replaces free
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   201
  variables by schematic variables, renames schematic variables to
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   202
  have subscript zero, also strips outer (meta) quantifiers and
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   203
  removes dangling sort hypotheses.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
\item[\ttindexbold{zero_var_indexes} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
makes all schematic variables have subscript zero, renaming them to avoid
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
clashes. 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
\item[\ttindexbold{make_elim} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
\index{rules!converting destruction to elimination}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   211
converts $thm$, which should be  a destruction rule of the form
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   212
$\List{P@1;\ldots;P@m}\Imp 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
Q$, to the elimination rule $\List{P@1; \ldots; P@m; Q\Imp R}\Imp R$.  This
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
is the basis for destruct-resolution: {\tt dresolve_tac}, etc.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
\item[\ttindexbold{rule_by_tactic} {\it tac} {\it thm}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
  applies {\it tac\/} to the {\it thm}, freezing its variables first, then
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
  yields the proof state returned by the tactic.  In typical usage, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
  {\it thm\/} represents an instance of a rule with several premises, some
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
  with contradictory assumptions (because of the instantiation).  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
  tactic proves those subgoals and does whatever else it can, and returns
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
  whatever is left.
4607
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   223
  
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   224
\item[\ttindexbold{rotate_prems} $k$ $thm$] rotates the premises of $thm$ to
8969
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   225
  the left by~$k$ positions (to the right if $k<0$).  It simply calls
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   226
  \texttt{permute_prems}, below, with $j=0$.  Used with
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   227
  \texttt{eresolve_tac}\index{*eresolve_tac!on other than first premise}, it
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   228
  gives the effect of applying the tactic to some other premise of $thm$ than
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   229
  the first.
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   230
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   231
\item[\ttindexbold{permute_prems} $j$ $k$ $thm$] rotates the premises of $thm$
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   232
  leaving the first $j$ premises unchanged.  It
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   233
  requires $0\leq j\leq n$, where $n$ is the number of premises.  If $k$ is
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   234
  positive then it rotates the remaining $n-j$ premises to the left; if $k$ is
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   235
  negative then it rotates the premises to the right.
11163
14732e3eaa6e added rearrange_prems
oheimb
parents: 9499
diff changeset
   236
14732e3eaa6e added rearrange_prems
oheimb
parents: 9499
diff changeset
   237
\item[\ttindexbold{rearrange_prems} $ps$ $thm$] permutes the premises of $thm$
14732e3eaa6e added rearrange_prems
oheimb
parents: 9499
diff changeset
   238
   where the value at the $i$-th position (counting from $0$) in the list $ps$
14732e3eaa6e added rearrange_prems
oheimb
parents: 9499
diff changeset
   239
   gives the position within the original thm to be transferred to position $i$.
14732e3eaa6e added rearrange_prems
oheimb
parents: 9499
diff changeset
   240
   Any remaining trailing positions are left unchanged.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   241
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
\subsection{Taking a theorem apart}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   245
\index{theorems!taking apart}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
\index{flex-flex constraints}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
\begin{ttbox} 
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   248
cprop_of      : thm -> cterm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
concl_of      : thm -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
prems_of      : thm -> term list
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   251
cprems_of     : thm -> cterm list
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
nprems_of     : thm -> int
4383
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   253
tpairs_of     : thm -> (term*term) list
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   254
sign_of_thm   : thm -> Sign.sg
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 332
diff changeset
   255
theory_of_thm : thm -> theory
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   256
dest_state : thm * int -> (term*term) list * term list * term * term
9499
7e6988210488 rep_thm: 'der' field has additional bool for oracles;
wenzelm
parents: 9288
diff changeset
   257
rep_thm    : thm -> \{sign_ref: Sign.sg_ref, der: bool * deriv, maxidx: int,
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   258
                     shyps: sort list, hyps: term list, prop: term\}
9499
7e6988210488 rep_thm: 'der' field has additional bool for oracles;
wenzelm
parents: 9288
diff changeset
   259
crep_thm   : thm -> \{sign_ref: Sign.sg_ref, der: bool * deriv, maxidx: int,
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   260
                     shyps: sort list, hyps: cterm list, prop:{\ts}cterm\}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   262
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   263
\item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   264
  a certified term.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   265
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   266
\item[\ttindexbold{concl_of} $thm$] returns the conclusion of $thm$ as
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   267
  a term.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   268
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   269
\item[\ttindexbold{prems_of} $thm$] returns the premises of $thm$ as a
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   270
  list of terms.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   271
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   272
\item[\ttindexbold{cprems_of} $thm$] returns the premises of $thm$ as
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   273
  a list of certified terms.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
\item[\ttindexbold{nprems_of} $thm$] 
286
e7efbf03562b first draft of Springer book
lcp
parents: 151
diff changeset
   276
returns the number of premises in $thm$, and is equivalent to {\tt
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   277
  length~(prems_of~$thm$)}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   279
\item[\ttindexbold{tpairs_of} $thm$] returns the flex-flex constraints
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   280
  of $thm$.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   281
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   282
\item[\ttindexbold{sign_of_thm} $thm$] returns the signature
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   283
  associated with $thm$.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   284
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   285
\item[\ttindexbold{theory_of_thm} $thm$] returns the theory associated
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   286
  with $thm$.  Note that this does a lookup in Isabelle's global
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   287
  database of loaded theories.
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 332
diff changeset
   288
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
\item[\ttindexbold{dest_state} $(thm,i)$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
(this will be an implication if there are more than $i$ subgoals).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   294
\item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   295
  containing the statement of~$thm$ ({\tt prop}), its list of
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   296
  meta-assumptions ({\tt hyps}), its derivation ({\tt der}), a bound
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   297
  on the maximum subscript of its unknowns ({\tt maxidx}), and a
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   298
  reference to its signature ({\tt sign_ref}).  The {\tt shyps} field
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   299
  is discussed below.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   300
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   301
\item[\ttindexbold{crep_thm} $thm$] like \texttt{rep_thm}, but returns
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   302
  the hypotheses and statement as certified terms.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   303
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   304
\end{ttdescription}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   305
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   306
5777
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   307
\subsection{*Sort hypotheses} \label{sec:sort-hyps}
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   308
\index{sort hypotheses}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   309
\begin{ttbox} 
7644
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   310
strip_shyps         : thm -> thm
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   311
strip_shyps_warning : thm -> thm
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   312
\end{ttbox}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   313
2044
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   314
Isabelle's type variables are decorated with sorts, constraining them to
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   315
certain ranges of types.  This has little impact when sorts only serve for
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   316
syntactic classification of types --- for example, FOL distinguishes between
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   317
terms and other types.  But when type classes are introduced through axioms,
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   318
this may result in some sorts becoming {\em empty\/}: where one cannot exhibit
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   319
a type belonging to it because certain sets of axioms are unsatisfiable.
2044
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   320
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   321
If a theorem contains a type variable that is constrained by an empty
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   322
sort, then that theorem has no instances.  It is basically an instance
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   323
of {\em ex falso quodlibet}.  But what if it is used to prove another
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   324
theorem that no longer involves that sort?  The latter theorem holds
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   325
only if under an additional non-emptiness assumption.
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   326
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   327
Therefore, Isabelle's theorems carry around sort hypotheses.  The {\tt
2044
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   328
shyps} field is a list of sorts occurring in type variables in the current
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   329
{\tt prop} and {\tt hyps} fields.  It may also includes sorts used in the
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   330
theorem's proof that no longer appear in the {\tt prop} or {\tt hyps}
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   331
fields --- so-called {\em dangling\/} sort constraints.  These are the
2044
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   332
critical ones, asserting non-emptiness of the corresponding sorts.
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   333
 
7644
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   334
Isabelle automatically removes extraneous sorts from the {\tt shyps} field at
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   335
the end of a proof, provided that non-emptiness can be established by looking
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   336
at the theorem's signature: from the {\tt classes} and {\tt arities}
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   337
information.  This operation is performed by \texttt{strip_shyps} and
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   338
\texttt{strip_shyps_warning}.
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   339
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   340
\begin{ttdescription}
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   341
  
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   342
\item[\ttindexbold{strip_shyps} $thm$] removes any extraneous sort hypotheses
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   343
  that can be witnessed from the type signature.
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   344
  
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   345
\item[\ttindexbold{strip_shyps_warning}] is like \texttt{strip_shyps}, but
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   346
  issues a warning message of any pending sort hypotheses that do not have a
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   347
  (syntactic) witness.
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   348
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   349
\end{ttdescription}
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   350
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
\subsection{Tracing flags for unification}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   353
\index{tracing!of unification}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
\begin{ttbox} 
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   355
Unify.trace_simp   : bool ref \hfill\textbf{initially false}
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   356
Unify.trace_types  : bool ref \hfill\textbf{initially false}
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   357
Unify.trace_bound  : int ref \hfill\textbf{initially 10}
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   358
Unify.search_bound : int ref \hfill\textbf{initially 20}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
Tracing the search may be useful when higher-order unification behaves
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
unexpectedly.  Letting {\tt res_inst_tac} circumvent the problem is easier,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
though.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   363
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   364
\item[set Unify.trace_simp;] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
causes tracing of the simplification phase.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   367
\item[set Unify.trace_types;] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
generates warnings of incompleteness, when unification is not considering
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
all possible instantiations of type unknowns.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   371
\item[Unify.trace_bound := $n$;] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
causes unification to print tracing information once it reaches depth~$n$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
Use $n=0$ for full tracing.  At the default value of~10, tracing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
information is almost never printed.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   376
\item[Unify.search_bound := $n$;] prevents unification from
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   377
  searching past the depth~$n$.  Because of this bound, higher-order
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   378
  unification cannot return an infinite sequence, though it can return
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   379
  an exponentially long one.  The search rarely approaches the default value
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   380
  of~20.  If the search is cut off, unification prints a warning
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   381
  \texttt{Unification bound exceeded}.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   382
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   385
\section{*Primitive meta-level inference rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
\index{meta-rules|(}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   387
These implement the meta-logic in the style of the {\sc lcf} system,
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   388
as functions from theorems to theorems.  They are, rarely, useful for
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   389
deriving results in the pure theory.  Mainly, they are included for
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   390
completeness, and most users should not bother with them.  The
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   391
meta-rules raise exception \xdx{THM} to signal malformed premises,
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   392
incompatible signatures and similar errors.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   394
\index{meta-assumptions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
The meta-logic uses natural deduction.  Each theorem may depend on
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   396
meta-level assumptions.  Certain rules, such as $({\Imp}I)$,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
discharge assumptions; in most other rules, the conclusion depends on all
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
of the assumptions of the premises.  Formally, the system works with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
assertions of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
\[ \phi \quad [\phi@1,\ldots,\phi@n], \]
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   401
where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions.  This can be
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   402
also read as a single conclusion sequent $\phi@1,\ldots,\phi@n \vdash
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   403
\phi$.  Do not confuse meta-level assumptions with the object-level
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   404
assumptions in a subgoal, which are represented in the meta-logic
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   405
using~$\Imp$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
Each theorem has a signature.  Certified terms have a signature.  When a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
rule takes several premises and certified terms, it merges the signatures
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
to make a signature for the conclusion.  This fails if the signatures are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
incompatible. 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
5777
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   412
\medskip
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   413
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   414
The following presentation of primitive rules ignores sort
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   415
hypotheses\index{sort hypotheses} (see also \S\ref{sec:sort-hyps}).  These are
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   416
handled transparently by the logic implementation.
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   417
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   418
\bigskip
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   419
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   420
\index{meta-implication}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   421
The \textbf{implication} rules are $({\Imp}I)$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
and $({\Imp}E)$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}}  \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
   \infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi}  \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   426
\index{meta-equality}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
Equality of truth values means logical equivalence:
3524
c02cb15830de fixed EqI meta rule;
wenzelm
parents: 3485
diff changeset
   428
\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi &
c02cb15830de fixed EqI meta rule;
wenzelm
parents: 3485
diff changeset
   429
                                       \psi\Imp\phi}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
   \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
   \infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   433
The \textbf{equality} rules are reflexivity, symmetry, and transitivity:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
\[ {a\equiv a}\,(refl)  \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
   \infer[(sym)]{b\equiv a}{a\equiv b}  \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
   \infer[(trans)]{a\equiv c}{a\equiv b & b\equiv c}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   438
\index{lambda calc@$\lambda$-calculus}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
The $\lambda$-conversions are $\alpha$-conversion, $\beta$-conversion, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
extensionality:\footnote{$\alpha$-conversion holds if $y$ is not free
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
in~$a$; $(ext)$ holds if $x$ is not free in the assumptions, $f$, or~$g$.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
\[ {(\lambda x.a) \equiv (\lambda y.a[y/x])}    \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
   {((\lambda x.a)(b)) \equiv a[b/x]}           \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
   \infer[(ext)]{f\equiv g}{f(x) \equiv g(x)}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   446
The \textbf{abstraction} and \textbf{combination} rules let conversions be
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   447
applied to subterms:\footnote{Abstraction holds if $x$ is not free in the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
assumptions.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
\[  \infer[(abs)]{(\lambda x.a) \equiv (\lambda x.b)}{a\equiv b}   \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
    \infer[(comb)]{f(a)\equiv g(b)}{f\equiv g & a\equiv b}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   452
\index{meta-quantifiers}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   453
The \textbf{universal quantification} rules are $(\Forall I)$ and $(\Forall
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
E)$:\footnote{$(\Forall I)$ holds if $x$ is not free in the assumptions.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
\[ \infer[(\Forall I)]{\Forall x.\phi}{\phi}        \qquad
286
e7efbf03562b first draft of Springer book
lcp
parents: 151
diff changeset
   456
   \infer[(\Forall E)]{\phi[b/x]}{\Forall x.\phi}   \]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   459
\subsection{Assumption rule}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   460
\index{meta-assumptions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   462
assume: cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   464
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
\item[\ttindexbold{assume} $ct$] 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   466
makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
The rule checks that $ct$ has type $prop$ and contains no unknowns, which
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   468
are not allowed in assumptions.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   469
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   471
\subsection{Implication rules}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   472
\index{meta-implication}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   474
implies_intr      : cterm -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   475
implies_intr_list : cterm list -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
implies_intr_hyps : thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
implies_elim      : thm -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
implies_elim_list : thm -> thm list -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   479
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   480
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
\item[\ttindexbold{implies_intr} $ct$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
is $({\Imp}I)$, where $ct$ is the assumption to discharge, say~$\phi$.  It
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   483
maps the premise~$\psi$ to the conclusion $\phi\Imp\psi$, removing all
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   484
occurrences of~$\phi$ from the assumptions.  The rule checks that $ct$ has
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   485
type $prop$. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
\item[\ttindexbold{implies_intr_list} $cts$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
applies $({\Imp}I)$ repeatedly, on every element of the list~$cts$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
\item[\ttindexbold{implies_intr_hyps} $thm$] 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   491
applies $({\Imp}I)$ to discharge all the hypotheses (assumptions) of~$thm$.
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   492
It maps the premise $\phi \; [\phi@1,\ldots,\phi@n]$ to the conclusion
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
$\List{\phi@1,\ldots,\phi@n}\Imp\phi$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
\item[\ttindexbold{implies_elim} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
applies $({\Imp}E)$ to $thm@1$ and~$thm@2$.  It maps the premises $\phi\Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
\psi$ and $\phi$ to the conclusion~$\psi$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
\item[\ttindexbold{implies_elim_list} $thm$ $thms$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
applies $({\Imp}E)$ repeatedly to $thm$, using each element of~$thms$ in
151
c5e636ca6576 corrected some obvious errors;
wenzelm
parents: 104
diff changeset
   501
turn.  It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   503
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   505
\subsection{Logical equivalence rules}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   506
\index{meta-equality}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
\begin{ttbox} 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   508
equal_intr : thm -> thm -> thm 
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   509
equal_elim : thm -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   511
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
\item[\ttindexbold{equal_intr} $thm@1$ $thm@2$] 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   513
applies $({\equiv}I)$ to $thm@1$ and~$thm@2$.  It maps the premises~$\psi$
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   514
and~$\phi$ to the conclusion~$\phi\equiv\psi$; the assumptions are those of
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   515
the first premise with~$\phi$ removed, plus those of
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   516
the second premise with~$\psi$ removed.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
\item[\ttindexbold{equal_elim} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
applies $({\equiv}E)$ to $thm@1$ and~$thm@2$.  It maps the premises
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
$\phi\equiv\psi$ and $\phi$ to the conclusion~$\psi$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   521
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
\subsection{Equality rules}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   525
\index{meta-equality}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   527
reflexive  : cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
symmetric  : thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
transitive : thm -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   531
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
\item[\ttindexbold{reflexive} $ct$] 
151
c5e636ca6576 corrected some obvious errors;
wenzelm
parents: 104
diff changeset
   533
makes the theorem \(ct\equiv ct\). 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
\item[\ttindexbold{symmetric} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
maps the premise $a\equiv b$ to the conclusion $b\equiv a$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   538
\item[\ttindexbold{transitive} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   539
maps the premises $a\equiv b$ and $b\equiv c$ to the conclusion~${a\equiv c}$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   540
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   542
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
\subsection{The $\lambda$-conversion rules}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   544
\index{lambda calc@$\lambda$-calculus}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   545
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   546
beta_conversion : cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   547
extensional     : thm -> thm
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   548
abstract_rule   : string -> cterm -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
combination     : thm -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
\end{ttbox} 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   551
There is no rule for $\alpha$-conversion because Isabelle regards
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   552
$\alpha$-convertible theorems as equal.
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   553
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   554
\item[\ttindexbold{beta_conversion} $ct$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   555
makes the theorem $((\lambda x.a)(b)) \equiv a[b/x]$, where $ct$ is the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   556
term $(\lambda x.a)(b)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   557
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
\item[\ttindexbold{extensional} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   560
Parameter~$x$ is taken from the premise.  It may be an unknown or a free
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   561
variable (provided it does not occur in the assumptions); it must not occur
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   562
in $f$ or~$g$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   564
\item[\ttindexbold{abstract_rule} $v$ $x$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   565
maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
(\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   567
Parameter~$x$ is supplied as a cterm.  It may be an unknown or a free
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   568
variable (provided it does not occur in the assumptions).  In the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
conclusion, the bound variable is named~$v$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
\item[\ttindexbold{combination} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   572
maps the premises $f\equiv g$ and $a\equiv b$ to the conclusion~$f(a)\equiv
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   573
g(b)$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   574
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   575
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   576
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   577
\subsection{Forall introduction rules}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   578
\index{meta-quantifiers}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   579
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   580
forall_intr       : cterm      -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   581
forall_intr_list  : cterm list -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   582
forall_intr_frees :               thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   583
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   584
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   585
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   586
\item[\ttindexbold{forall_intr} $x$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   587
applies $({\Forall}I)$, abstracting over all occurrences (if any!) of~$x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   588
The rule maps the premise $\phi$ to the conclusion $\Forall x.\phi$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   589
Parameter~$x$ is supplied as a cterm.  It may be an unknown or a free
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   590
variable (provided it does not occur in the assumptions).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   591
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   592
\item[\ttindexbold{forall_intr_list} $xs$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   593
applies $({\Forall}I)$ repeatedly, on every element of the list~$xs$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   595
\item[\ttindexbold{forall_intr_frees} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   596
applies $({\Forall}I)$ repeatedly, generalizing over all the free variables
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   597
of the premise.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   598
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   599
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   600
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   601
\subsection{Forall elimination rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   602
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   603
forall_elim       : cterm      -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   604
forall_elim_list  : cterm list -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   605
forall_elim_var   :        int -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   606
forall_elim_vars  :        int -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   607
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   608
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   609
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   610
\item[\ttindexbold{forall_elim} $ct$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   612
$\phi[ct/x]$.  The rule checks that $ct$ and $x$ have the same type.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   613
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   614
\item[\ttindexbold{forall_elim_list} $cts$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   615
applies $({\Forall}E)$ repeatedly, on every element of the list~$cts$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   616
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   617
\item[\ttindexbold{forall_elim_var} $k$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   618
applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   619
$\phi[\Var{x@k}/x]$.  Thus, it replaces the outermost $\Forall$-bound
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   620
variable by an unknown having subscript~$k$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   621
9258
2121ff73a37d fixed typos reported by Jeremy Dawson
paulson
parents: 8969
diff changeset
   622
\item[\ttindexbold{forall_elim_vars} $k$ $thm$] 
2121ff73a37d fixed typos reported by Jeremy Dawson
paulson
parents: 8969
diff changeset
   623
applies {\tt forall_elim_var}~$k$ repeatedly until the theorem no longer has
2121ff73a37d fixed typos reported by Jeremy Dawson
paulson
parents: 8969
diff changeset
   624
the form $\Forall x.\phi$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   625
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   626
8135
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   627
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   628
\subsection{Instantiation of unknowns}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   629
\index{instantiation}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   630
\begin{alltt}\footnotesize
3135
233aba197bf2 tuned spaces;
wenzelm
parents: 3108
diff changeset
   631
instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list -> thm -> thm
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   632
\end{alltt}
8135
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   633
There are two versions of this rule.  The primitive one is
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   634
\ttindexbold{Thm.instantiate}, which merely performs the instantiation and can
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   635
produce a conclusion not in normal form.  A derived version is  
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   636
\ttindexbold{Drule.instantiate}, which normalizes its conclusion.
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   637
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   638
\begin{ttdescription}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   639
\item[\ttindexbold{instantiate} ($tyinsts$,$insts$) $thm$] 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   640
simultaneously substitutes types for type unknowns (the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   641
$tyinsts$) and terms for term unknowns (the $insts$).  Instantiations are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   642
given as $(v,t)$ pairs, where $v$ is an unknown and $t$ is a term (of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   643
same type as $v$) or a type (of the same sort as~$v$).  All the unknowns
8135
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   644
must be distinct.  
4376
407f786d3059 instantiate';
wenzelm
parents: 4317
diff changeset
   645
8135
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   646
In some cases, \ttindex{instantiate'} (see \S\ref{sec:instantiate})
4376
407f786d3059 instantiate';
wenzelm
parents: 4317
diff changeset
   647
provides a more convenient interface to this rule.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   648
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   649
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   650
8135
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   651
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   652
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   653
\subsection{Freezing/thawing type unknowns}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   654
\index{type unknowns!freezing/thawing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   655
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   656
freezeT: thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   657
varifyT: thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   658
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   659
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   660
\item[\ttindexbold{freezeT} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   661
converts all the type unknowns in $thm$ to free type variables.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   662
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
\item[\ttindexbold{varifyT} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   664
converts all the free type variables in $thm$ to type unknowns.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   665
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   666
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   667
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   668
\section{Derived rules for goal-directed proof}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   669
Most of these rules have the sole purpose of implementing particular
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   670
tactics.  There are few occasions for applying them directly to a theorem.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   671
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   672
\subsection{Proof by assumption}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   673
\index{meta-assumptions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   674
\begin{ttbox} 
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   675
assumption    : int -> thm -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   676
eq_assumption : int -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   677
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   678
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   679
\item[\ttindexbold{assumption} {\it i} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   680
attempts to solve premise~$i$ of~$thm$ by assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
\item[\ttindexbold{eq_assumption}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   683
is like {\tt assumption} but does not use unification.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   684
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   685
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   686
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   687
\subsection{Resolution}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   688
\index{resolution}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   689
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   690
biresolution : bool -> (bool*thm)list -> int -> thm
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   691
               -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   692
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   693
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   694
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$] 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   695
performs bi-resolution on subgoal~$i$ of $state$, using the list of $\it
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   696
(flag,rule)$ pairs.  For each pair, it applies resolution if the flag
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   697
is~{\tt false} and elim-resolution if the flag is~{\tt true}.  If $match$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   698
is~{\tt true}, the $state$ is not instantiated.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   699
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   700
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   701
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   702
\subsection{Composition: resolution without lifting}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   703
\index{resolution!without lifting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   704
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   705
compose   : thm * int * thm -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   706
COMP      : thm * thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   707
bicompose : bool -> bool * thm * int -> int -> thm
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   708
            -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   709
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   710
In forward proof, a typical use of composition is to regard an assertion of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   711
the form $\phi\Imp\psi$ as atomic.  Schematic variables are not renamed, so
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   712
beware of clashes!
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   713
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   714
\item[\ttindexbold{compose} ($thm@1$, $i$, $thm@2$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   715
uses $thm@1$, regarded as an atomic formula, to solve premise~$i$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   716
of~$thm@2$.  Let $thm@1$ and $thm@2$ be $\psi$ and $\List{\phi@1; \ldots;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   717
\phi@n} \Imp \phi$.  For each $s$ that unifies~$\psi$ and $\phi@i$, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   718
result list contains the theorem
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   719
\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   720
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   721
1119
49ed9a415637 Indexing of COMP
lcp
parents: 876
diff changeset
   722
\item[$thm@1$ \ttindexbold{COMP} $thm@2$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   723
calls \hbox{\tt compose ($thm@1$, 1, $thm@2$)} and returns the result, if
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   724
unique; otherwise, it raises exception~\xdx{THM}\@.  It is
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   725
analogous to {\tt RS}\@.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   726
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   727
For example, suppose that $thm@1$ is $a=b\Imp b=a$, a symmetry rule, and
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   728
that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P$, which is the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   729
principle of contrapositives.  Then the result would be the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   730
derived rule $\neg(b=a)\Imp\neg(a=b)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   731
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   732
\item[\ttindexbold{bicompose} $match$ ($flag$, $rule$, $m$) $i$ $state$]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   733
refines subgoal~$i$ of $state$ using $rule$, without lifting.  The $rule$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   734
is taken to have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   735
$\psi$ need not be atomic; thus $m$ determines the number of new
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   736
subgoals.  If $flag$ is {\tt true} then it performs elim-resolution --- it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   737
solves the first premise of~$rule$ by assumption and deletes that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   738
assumption.  If $match$ is~{\tt true}, the $state$ is not instantiated.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   739
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   740
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   741
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   742
\subsection{Other meta-rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   743
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   744
trivial            : cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   745
lift_rule          : (thm * int) -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   746
rename_params_rule : string list * int -> thm -> thm
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   747
flexflex_rule      : thm -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   748
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   749
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   750
\item[\ttindexbold{trivial} $ct$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   751
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   752
This is the initial state for a goal-directed proof of~$\phi$.  The rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   753
checks that $ct$ has type~$prop$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   754
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   755
\item[\ttindexbold{lift_rule} ($state$, $i$) $rule$] \index{lifting}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   756
prepares $rule$ for resolution by lifting it over the parameters and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   757
assumptions of subgoal~$i$ of~$state$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   758
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   759
\item[\ttindexbold{rename_params_rule} ({\it names}, {\it i}) $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   760
uses the $names$ to rename the parameters of premise~$i$ of $thm$.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   761
names must be distinct.  If there are fewer names than parameters, then the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   762
rule renames the innermost parameters and may modify the remaining ones to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   763
ensure that all the parameters are distinct.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   764
\index{parameters!renaming}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   765
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   766
\item[\ttindexbold{flexflex_rule} $thm$]  \index{flex-flex constraints}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   767
removes all flex-flex pairs from $thm$ using the trivial unifier.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   768
\end{ttdescription}
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   769
\index{meta-rules|)}
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   770
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   771
11622
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   772
\section{Proof terms}\label{sec:proofObjects}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   773
\index{proof terms|(} Isabelle can record the full meta-level proof of each
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   774
theorem.  The proof term contains all logical inferences in detail.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   775
%while
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   776
%omitting bookkeeping steps that have no logical meaning to an outside
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   777
%observer.  Rewriting steps are recorded in similar detail as the output of
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   778
%simplifier tracing. 
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   779
Resolution and rewriting steps are broken down to primitive rules of the
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   780
meta-logic. The proof term can be inspected by a separate proof-checker,
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   781
for example.
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   782
11622
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   783
According to the well-known {\em Curry-Howard isomorphism}, a proof can
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   784
be viewed as a $\lambda$-term. Following this idea, proofs
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   785
in Isabelle are internally represented by a datatype similar to the one for
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   786
terms described in \S\ref{sec:terms}.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   787
\begin{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   788
infix 8 % %%;
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   789
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   790
datatype proof =
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   791
   PBound of int
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   792
 | Abst of string * typ option * proof
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   793
 | AbsP of string * term option * proof
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   794
 | op % of proof * term option
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   795
 | op %% of proof * proof
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   796
 | Hyp of term
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   797
 | PThm of (string * (string * string list) list) *
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   798
           proof * term * typ list option
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   799
 | PAxm of string * term * typ list option
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   800
 | Oracle of string * term * typ list option
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   801
 | MinProof of proof list;
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   802
\end{ttbox}
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   803
11622
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   804
\begin{ttdescription}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   805
\item[\ttindexbold{Abst} ($a$, $\tau$, $prf$)] is the abstraction over
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   806
a {\it term variable} of type $\tau$ in the body $prf$. Logically, this
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   807
corresponds to $\bigwedge$ introduction. The name $a$ is used only for
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   808
parsing and printing.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   809
\item[\ttindexbold{AbsP} ($a$, $\varphi$, $prf$)] is the abstraction
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   810
over a {\it proof variable} standing for a proof of proposition $\varphi$
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   811
in the body $prf$. This corresponds to $\Longrightarrow$ introduction.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   812
\item[$prf$ \% $t$] \index{\%@{\tt\%}|bold}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   813
is the application of proof $prf$ to term $t$
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   814
which corresponds to $\bigwedge$ elimination.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   815
\item[$prf@1$ \%\% $prf@2$] \index{\%\%@{\tt\%\%}|bold}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   816
is the application of proof $prf@1$ to
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   817
proof $prf@2$ which corresponds to $\Longrightarrow$ elimination.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   818
\item[\ttindexbold{PBound} $i$] is a {\em proof variable} with de Bruijn
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   819
\cite{debruijn72} index $i$.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   820
\item[\ttindexbold{Hyp} $\varphi$] corresponds to the use of a meta level
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   821
hypothesis $\varphi$.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   822
\item[\ttindexbold{PThm} (($name$, $tags$), $prf$, $\varphi$, $\overline{\tau}$)]
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   823
stands for a pre-proved theorem, where $name$ is the name of the theorem,
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   824
$prf$ is its actual proof, $\varphi$ is the proven proposition,
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   825
and $\overline{\tau}$ is
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   826
a type assignment for the type variables occurring in the proposition.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   827
\item[\ttindexbold{PAxm} ($name$, $\varphi$, $\overline{\tau}$)]
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   828
corresponds to the use of an axiom with name $name$ and proposition
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   829
$\varphi$, where $\overline{\tau}$ is a type assignment for the type
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   830
variables occurring in the proposition.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   831
\item[\ttindexbold{Oracle} ($name$, $\varphi$, $\overline{\tau}$)]
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   832
denotes the invocation of an oracle with name $name$ which produced
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   833
a proposition $\varphi$, where $\overline{\tau}$ is a type assignment
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   834
for the type variables occurring in the proposition.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   835
\item[\ttindexbold{MinProof} $prfs$]
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   836
represents a {\em minimal proof} where $prfs$ is a list of theorems,
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   837
axioms or oracles.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   838
\end{ttdescription}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   839
Note that there are no separate constructors
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   840
for abstraction and application on the level of {\em types}, since
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   841
instantiation of type variables is accomplished via the type assignments
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   842
attached to {\tt Thm}, {\tt Axm} and {\tt Oracle}.
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   843
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   844
Each theorem's derivation is stored as the {\tt der} field of its internal
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   845
record: 
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   846
\begin{ttbox} 
11622
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   847
#2 (#der (rep_thm conjI));
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   848
{\out PThm (("HOL.conjI", []),}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   849
{\out   AbsP ("H", None, AbsP ("H", None, \dots)), \dots, None) %}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   850
{\out     None % None : Proofterm.proof}
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   851
\end{ttbox}
11622
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   852
This proof term identifies a labelled theorem, {\tt conjI} of theory
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   853
\texttt{HOL}, whose underlying proof is
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   854
{\tt AbsP ("H", None, AbsP ("H", None, $\dots$))}. 
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   855
The theorem is applied to two (implicit) term arguments, which correspond
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   856
to the two variables occurring in its proposition.
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   857
11622
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   858
Isabelle's inference kernel can produce proof objects with different
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   859
levels of detail. This is controlled via the global reference variable
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   860
\ttindexbold{proofs}:
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   861
\begin{ttdescription}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   862
\item[proofs := 0;] only record uses of oracles
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   863
\item[proofs := 1;] record uses of oracles as well as dependencies
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   864
  on other theorems and axioms
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   865
\item[proofs := 2;] record inferences in full detail
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   866
\end{ttdescription}
11622
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   867
Reconstruction and checking of proofs as described in \S\ref{sec:reconstruct_proofs}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   868
will not work for proofs constructed with {\tt proofs} set to
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   869
{\tt 0} or {\tt 1}.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   870
Theorems involving oracles will be printed with a
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   871
suffixed \verb|[!]| to point out the different quality of confidence achieved.
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   872
7871
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   873
\medskip
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   874
11622
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   875
The dependencies of theorems can be viewed using the function
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   876
\ttindexbold{thm_deps}\index{theorems!dependencies}:
7871
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   877
\begin{ttbox}
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   878
thm_deps [\(thm@1\), \(\ldots\), \(thm@n\)];
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   879
\end{ttbox}
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   880
generates the dependency graph of the theorems $thm@1$, $\ldots$, $thm@n$ and
11622
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   881
displays it using Isabelle's graph browser. For this to work properly,
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   882
the theorems in question have to be proved with {\tt proofs} set to a value
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   883
greater than {\tt 0}. You can use
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   884
\begin{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   885
ThmDeps.enable : unit -> unit
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   886
ThmDeps.disable : unit -> unit
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   887
\end{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   888
to set \texttt{proofs} appropriately.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   889
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   890
\subsection{Reconstructing and checking proof terms}\label{sec:reconstruct_proofs}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   891
\index{proof terms!reconstructing}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   892
\index{proof terms!checking}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   893
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   894
When looking at the above datatype of proofs more closely, one notices that
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   895
some arguments of constructors are {\it optional}. The reason for this is that
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   896
keeping a full proof term for each theorem would result in enormous memory
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   897
requirements. Fortunately, typical proof terms usually contain quite a lot of
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   898
redundant information that can be reconstructed from the context. Therefore,
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   899
Isabelle's inference kernel creates only {\em partial} (or {\em implicit})
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   900
\index{proof terms!partial} proof terms, in which
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   901
all typing information in terms, all term and type labels of abstractions
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   902
{\tt AbsP} and {\tt Abst}, and (if possible) some argument terms of
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   903
\verb!%! are omitted. The following functions are available for
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   904
reconstructing and checking proof terms:
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   905
\begin{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   906
Reconstruct.reconstruct_proof :
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   907
  Sign.sg -> term -> Proofterm.proof -> Proofterm.proof
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   908
Reconstruct.expand_proof :
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   909
  Sign.sg -> string list -> Proofterm.proof -> Proofterm.proof
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   910
ProofChecker.thm_of_proof : theory -> Proofterm.proof -> thm
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   911
\end{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   912
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   913
\begin{ttdescription}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   914
\item[Reconstruct.reconstruct_proof $sg$ $t$ $prf$]
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   915
turns the partial proof $prf$ into a full proof of the
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   916
proposition denoted by $t$, with respect to signature $sg$.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   917
Reconstruction will fail with an error message if $prf$
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   918
is not a proof of $t$, is ill-formed, or does not contain
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   919
sufficient information for reconstruction by
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   920
{\em higher order pattern unification}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   921
\cite{nipkow-patterns, Berghofer-Nipkow:2000:TPHOL}.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   922
The latter may only happen for proofs
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   923
built up ``by hand'' but not for those produced automatically
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   924
by Isabelle's inference kernel.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   925
\item[Reconstruct.expand_proof $sg$
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   926
  \ttlbrack$name@1$, $\ldots$, $name@n${\ttrbrack} $prf$]
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   927
expands and reconstructs the proofs of all theorems with names
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   928
$name@1$, $\ldots$, $name@n$ in the (full) proof $prf$.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   929
\item[ProofChecker.thm_of_proof $thy$ $prf$] turns the (full) proof
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   930
$prf$ into a theorem with respect to theory $thy$ by replaying
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   931
it using only primitive rules from Isabelle's inference kernel.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   932
\end{ttdescription}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   933
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   934
\subsection{Parsing and printing proof terms}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   935
\index{proof terms!parsing}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   936
\index{proof terms!printing}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   937
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   938
Isabelle offers several functions for parsing and printing
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   939
proof terms. The concrete syntax for proof terms is described
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   940
in Fig.\ts\ref{fig:proof_gram}.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   941
Implicit term arguments in partial proofs are indicated
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   942
by ``{\tt _}''.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   943
Type arguments for theorems and axioms may be specified using
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   944
\verb!%! or ``$\cdot$'' with an argument of the form {\tt TYPE($type$)}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   945
(see \S\ref{sec:basic_syntax}).
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   946
They must appear before any other term argument of a theorem
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   947
or axiom. In contrast to term arguments, type arguments may
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   948
be completely omitted.
7871
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   949
\begin{ttbox}
11625
74cdf24724ea Tuned section about parsing and printing proof terms.
berghofe
parents: 11622
diff changeset
   950
ProofSyntax.read_proof : theory -> bool -> string -> Proofterm.proof
74cdf24724ea Tuned section about parsing and printing proof terms.
berghofe
parents: 11622
diff changeset
   951
ProofSyntax.pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
74cdf24724ea Tuned section about parsing and printing proof terms.
berghofe
parents: 11622
diff changeset
   952
ProofSyntax.pretty_proof_of : bool -> thm -> Pretty.T
74cdf24724ea Tuned section about parsing and printing proof terms.
berghofe
parents: 11622
diff changeset
   953
ProofSyntax.print_proof_of : bool -> thm -> unit
7871
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   954
\end{ttbox}
11622
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   955
\begin{figure}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   956
\begin{center}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   957
\begin{tabular}{rcl}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   958
$proof$  & $=$ & {\tt Lam} $params${\tt .} $proof$ ~~$|$~~
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   959
                 $\Lambda params${\tt .} $proof$ \\
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   960
         & $|$ & $proof$ \verb!%! $any$ ~~$|$~~
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   961
                 $proof$ $\cdot$ $any$ \\
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   962
         & $|$ & $proof$ \verb!%%! $proof$ ~~$|$~~
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   963
                 $proof$ {\boldmath$\cdot$} $proof$ \\
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   964
         & $|$ & $id$ ~~$|$~~ $longid$ \\\\
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   965
$param$  & $=$ & $idt$ ~~$|$~~ $idt$ {\tt :} $prop$ ~~$|$~~
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   966
                 {\tt (} $param$ {\tt )} \\\\
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   967
$params$ & $=$ & $param$ ~~$|$~~ $param$ $params$
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   968
\end{tabular}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   969
\end{center}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   970
\caption{Proof term syntax}\label{fig:proof_gram}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   971
\end{figure}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   972
The function {\tt read_proof} reads in a proof term with
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   973
respect to a given theory. The boolean flag indicates whether
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   974
the proof term to be parsed contains explicit typing information
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   975
to be taken into account.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   976
Usually, typing information is left implicit and
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   977
is inferred during proof reconstruction. The pretty printing
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   978
functions operating on theorems take a boolean flag as an
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   979
argument which indicates whether the proof term should
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   980
be reconstructed before printing.
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   981
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   982
The following example (based on Isabelle/HOL) illustrates how
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   983
to parse and check proof terms. We start by parsing a partial
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   984
proof term
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   985
\begin{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   986
val prf = ProofSyntax.read_proof Main.thy false
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   987
  "impI % _ % _ %% (Lam H : _. conjE % _ % _ % _ %% H %%
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   988
     (Lam (H1 : _) H2 : _. conjI % _ % _ %% H2 %% H1))";
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   989
{\out val prf = PThm (("HOL.impI", []), \dots, \dots, None) % None % None %%}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   990
{\out   AbsP ("H", None, PThm (("HOL.conjE", []), \dots, \dots, None) %}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   991
{\out     None % None % None %% PBound 0 %%}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   992
{\out     AbsP ("H1", None, AbsP ("H2", None, \dots))) : Proofterm.proof}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   993
\end{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   994
The statement to be established by this proof is
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   995
\begin{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   996
val t = term_of
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   997
  (read_cterm (sign_of Main.thy) ("A & B --> B & A", propT));
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   998
{\out val t = Const ("Trueprop", "bool => prop") $}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
   999
{\out   (Const ("op -->", "[bool, bool] => bool") $}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1000
{\out     \dots $ \dots : Term.term}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1001
\end{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1002
Using {\tt t} we can reconstruct the full proof
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1003
\begin{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1004
val prf' = Reconstruct.reconstruct_proof (sign_of Main.thy) t prf;
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1005
{\out val prf' = PThm (("HOL.impI", []), \dots, \dots, Some []) %}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1006
{\out   Some (Const ("op &", \dots) $ Free ("A", \dots) $ Free ("B", \dots)) %}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1007
{\out   Some (Const ("op &", \dots) $ Free ("B", \dots) $ Free ("A", \dots)) %%}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1008
{\out   AbsP ("H", Some (Const ("Trueprop", \dots) $ \dots), \dots)}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1009
{\out     : Proofterm.proof}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1010
\end{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1011
This proof can finally be turned into a theorem
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1012
\begin{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1013
val thm = ProofChecker.thm_of_proof Main.thy prf';
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1014
{\out val thm = "A & B --> B & A" : Thm.thm}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1015
\end{ttbox}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1016
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1017
\index{proof terms|)}
27f858e70b3f Added documentation for proof terms.
berghofe
parents: 11163
diff changeset
  1018
\index{theorems|)}
7871
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
  1019
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
  1020
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
  1021
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
  1022
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
  1023
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
  1024
%%% End: