doc-src/Ref/thm.tex
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 9499 7e6988210488
child 11163 14732e3eaa6e
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:
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
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   197
\begin{ttdescription}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   198
\item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   199
  of object-rules.  It discharges all meta-assumptions, replaces free
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   200
  variables by schematic variables, renames schematic variables to
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   201
  have subscript zero, also strips outer (meta) quantifiers and
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   202
  removes dangling sort hypotheses.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
\item[\ttindexbold{zero_var_indexes} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
makes all schematic variables have subscript zero, renaming them to avoid
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
clashes. 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
\item[\ttindexbold{make_elim} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
\index{rules!converting destruction to elimination}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   210
converts $thm$, which should be  a destruction rule of the form
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   211
$\List{P@1;\ldots;P@m}\Imp 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
Q$, to the elimination rule $\List{P@1; \ldots; P@m; Q\Imp R}\Imp R$.  This
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
is the basis for destruct-resolution: {\tt dresolve_tac}, etc.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
\item[\ttindexbold{rule_by_tactic} {\it tac} {\it thm}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
  applies {\it tac\/} to the {\it thm}, freezing its variables first, then
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
  yields the proof state returned by the tactic.  In typical usage, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
  {\it thm\/} represents an instance of a rule with several premises, some
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
  with contradictory assumptions (because of the instantiation).  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
  tactic proves those subgoals and does whatever else it can, and returns
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
  whatever is left.
4607
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   222
  
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   223
\item[\ttindexbold{rotate_prems} $k$ $thm$] rotates the premises of $thm$ to
8969
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   224
  the left by~$k$ positions (to the right if $k<0$).  It simply calls
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   225
  \texttt{permute_prems}, below, with $j=0$.  Used with
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   226
  \texttt{eresolve_tac}\index{*eresolve_tac!on other than first premise}, it
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   227
  gives the effect of applying the tactic to some other premise of $thm$ than
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   228
  the first.
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   229
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   230
\item[\ttindexbold{permute_prems} $j$ $k$ $thm$] rotates the premises of $thm$
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   231
  leaving the first $j$ premises unchanged.  It
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   232
  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
   233
  positive then it rotates the remaining $n-j$ premises to the left; if $k$ is
23c6e0ca0086 documented permute_prems
paulson
parents: 8136
diff changeset
   234
  negative then it rotates the premises to the right.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   235
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
\subsection{Taking a theorem apart}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   239
\index{theorems!taking apart}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
\index{flex-flex constraints}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
\begin{ttbox} 
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   242
cprop_of      : thm -> cterm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
concl_of      : thm -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
prems_of      : thm -> term list
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   245
cprems_of     : thm -> cterm list
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
nprems_of     : thm -> int
4383
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   247
tpairs_of     : thm -> (term*term) list
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   248
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
   249
theory_of_thm : thm -> theory
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   250
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
   251
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
   252
                     shyps: sort list, hyps: term list, prop: term\}
9499
7e6988210488 rep_thm: 'der' field has additional bool for oracles;
wenzelm
parents: 9288
diff changeset
   253
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
   254
                     shyps: sort list, hyps: cterm list, prop:{\ts}cterm\}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   256
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   257
\item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   258
  a certified term.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   259
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   260
\item[\ttindexbold{concl_of} $thm$] returns the conclusion of $thm$ as
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   261
  a term.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   262
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   263
\item[\ttindexbold{prems_of} $thm$] returns the premises of $thm$ as a
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   264
  list of terms.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   265
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   266
\item[\ttindexbold{cprems_of} $thm$] returns the premises of $thm$ as
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   267
  a list of certified terms.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
\item[\ttindexbold{nprems_of} $thm$] 
286
e7efbf03562b first draft of Springer book
lcp
parents: 151
diff changeset
   270
returns the number of premises in $thm$, and is equivalent to {\tt
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   271
  length~(prems_of~$thm$)}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   273
\item[\ttindexbold{tpairs_of} $thm$] returns the flex-flex constraints
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   274
  of $thm$.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   275
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   276
\item[\ttindexbold{sign_of_thm} $thm$] returns the signature
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   277
  associated with $thm$.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   278
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   279
\item[\ttindexbold{theory_of_thm} $thm$] returns the theory associated
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   280
  with $thm$.  Note that this does a lookup in Isabelle's global
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   281
  database of loaded theories.
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 332
diff changeset
   282
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
\item[\ttindexbold{dest_state} $(thm,i)$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
(this will be an implication if there are more than $i$ subgoals).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   288
\item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   289
  containing the statement of~$thm$ ({\tt prop}), its list of
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   290
  meta-assumptions ({\tt hyps}), its derivation ({\tt der}), a bound
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   291
  on the maximum subscript of its unknowns ({\tt maxidx}), and a
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   292
  reference to its signature ({\tt sign_ref}).  The {\tt shyps} field
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   293
  is discussed below.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   294
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   295
\item[\ttindexbold{crep_thm} $thm$] like \texttt{rep_thm}, but returns
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   296
  the hypotheses and statement as certified terms.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   297
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   298
\end{ttdescription}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   299
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   300
5777
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   301
\subsection{*Sort hypotheses} \label{sec:sort-hyps}
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   302
\index{sort hypotheses}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   303
\begin{ttbox} 
7644
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   304
strip_shyps         : thm -> thm
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   305
strip_shyps_warning : thm -> thm
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   306
\end{ttbox}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   307
2044
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   308
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
   309
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
   310
syntactic classification of types --- for example, FOL distinguishes between
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   311
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
   312
this may result in some sorts becoming {\em empty\/}: where one cannot exhibit
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   313
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
   314
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   315
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
   316
sort, then that theorem has no instances.  It is basically an instance
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   317
of {\em ex falso quodlibet}.  But what if it is used to prove another
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   318
theorem that no longer involves that sort?  The latter theorem holds
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   319
only if under an additional non-emptiness assumption.
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   320
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   321
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
   322
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
   323
{\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
   324
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
   325
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
   326
critical ones, asserting non-emptiness of the corresponding sorts.
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   327
 
7644
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   328
Isabelle automatically removes extraneous sorts from the {\tt shyps} field at
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   329
the end of a proof, provided that non-emptiness can be established by looking
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   330
at the theorem's signature: from the {\tt classes} and {\tt arities}
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   331
information.  This operation is performed by \texttt{strip_shyps} and
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   332
\texttt{strip_shyps_warning}.
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   333
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   334
\begin{ttdescription}
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   335
  
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   336
\item[\ttindexbold{strip_shyps} $thm$] removes any extraneous sort hypotheses
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   337
  that can be witnessed from the type signature.
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   338
  
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   339
\item[\ttindexbold{strip_shyps_warning}] is like \texttt{strip_shyps}, but
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   340
  issues a warning message of any pending sort hypotheses that do not have a
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   341
  (syntactic) witness.
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   342
054ecaf3ca22 strip_shyps(_warning);
wenzelm
parents: 6924
diff changeset
   343
\end{ttdescription}
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   344
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
\subsection{Tracing flags for unification}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   347
\index{tracing!of unification}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
\begin{ttbox} 
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   349
Unify.trace_simp   : bool ref \hfill\textbf{initially false}
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   350
Unify.trace_types  : bool ref \hfill\textbf{initially false}
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   351
Unify.trace_bound  : int ref \hfill\textbf{initially 10}
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   352
Unify.search_bound : int ref \hfill\textbf{initially 20}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
Tracing the search may be useful when higher-order unification behaves
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
unexpectedly.  Letting {\tt res_inst_tac} circumvent the problem is easier,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
though.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   357
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   358
\item[set Unify.trace_simp;] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
causes tracing of the simplification phase.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   361
\item[set Unify.trace_types;] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
generates warnings of incompleteness, when unification is not considering
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
all possible instantiations of type unknowns.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   365
\item[Unify.trace_bound := $n$;] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
causes unification to print tracing information once it reaches depth~$n$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
Use $n=0$ for full tracing.  At the default value of~10, tracing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
information is almost never printed.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   370
\item[Unify.search_bound := $n$;] prevents unification from
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   371
  searching past the depth~$n$.  Because of this bound, higher-order
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   372
  unification cannot return an infinite sequence, though it can return
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   373
  an exponentially long one.  The search rarely approaches the default value
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   374
  of~20.  If the search is cut off, unification prints a warning
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   375
  \texttt{Unification bound exceeded}.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   376
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   379
\section{*Primitive meta-level inference rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
\index{meta-rules|(}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   381
These implement the meta-logic in the style of the {\sc lcf} system,
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   382
as functions from theorems to theorems.  They are, rarely, useful for
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   383
deriving results in the pure theory.  Mainly, they are included for
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   384
completeness, and most users should not bother with them.  The
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   385
meta-rules raise exception \xdx{THM} to signal malformed premises,
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   386
incompatible signatures and similar errors.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   388
\index{meta-assumptions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
The meta-logic uses natural deduction.  Each theorem may depend on
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   390
meta-level assumptions.  Certain rules, such as $({\Imp}I)$,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
discharge assumptions; in most other rules, the conclusion depends on all
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
of the assumptions of the premises.  Formally, the system works with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
assertions of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
\[ \phi \quad [\phi@1,\ldots,\phi@n], \]
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   395
where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions.  This can be
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   396
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
   397
\phi$.  Do not confuse meta-level assumptions with the object-level
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   398
assumptions in a subgoal, which are represented in the meta-logic
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   399
using~$\Imp$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
Each theorem has a signature.  Certified terms have a signature.  When a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
rule takes several premises and certified terms, it merges the signatures
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
to make a signature for the conclusion.  This fails if the signatures are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
incompatible. 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
5777
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   406
\medskip
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   407
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   408
The following presentation of primitive rules ignores sort
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   409
hypotheses\index{sort hypotheses} (see also \S\ref{sec:sort-hyps}).  These are
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   410
handled transparently by the logic implementation.
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   411
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   412
\bigskip
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   413
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   414
\index{meta-implication}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   415
The \textbf{implication} rules are $({\Imp}I)$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
and $({\Imp}E)$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}}  \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
   \infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi}  \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   420
\index{meta-equality}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
Equality of truth values means logical equivalence:
3524
c02cb15830de fixed EqI meta rule;
wenzelm
parents: 3485
diff changeset
   422
\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi &
c02cb15830de fixed EqI meta rule;
wenzelm
parents: 3485
diff changeset
   423
                                       \psi\Imp\phi}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
   \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
   \infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   427
The \textbf{equality} rules are reflexivity, symmetry, and transitivity:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
\[ {a\equiv a}\,(refl)  \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
   \infer[(sym)]{b\equiv a}{a\equiv b}  \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
   \infer[(trans)]{a\equiv c}{a\equiv b & b\equiv c}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   432
\index{lambda calc@$\lambda$-calculus}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
The $\lambda$-conversions are $\alpha$-conversion, $\beta$-conversion, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
extensionality:\footnote{$\alpha$-conversion holds if $y$ is not free
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
in~$a$; $(ext)$ holds if $x$ is not free in the assumptions, $f$, or~$g$.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
\[ {(\lambda x.a) \equiv (\lambda y.a[y/x])}    \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
   {((\lambda x.a)(b)) \equiv a[b/x]}           \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
   \infer[(ext)]{f\equiv g}{f(x) \equiv g(x)}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   440
The \textbf{abstraction} and \textbf{combination} rules let conversions be
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   441
applied to subterms:\footnote{Abstraction holds if $x$ is not free in the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
assumptions.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
\[  \infer[(abs)]{(\lambda x.a) \equiv (\lambda x.b)}{a\equiv b}   \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
    \infer[(comb)]{f(a)\equiv g(b)}{f\equiv g & a\equiv b}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   446
\index{meta-quantifiers}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   447
The \textbf{universal quantification} rules are $(\Forall I)$ and $(\Forall
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
E)$:\footnote{$(\Forall I)$ holds if $x$ is not free in the assumptions.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
\[ \infer[(\Forall I)]{\Forall x.\phi}{\phi}        \qquad
286
e7efbf03562b first draft of Springer book
lcp
parents: 151
diff changeset
   450
   \infer[(\Forall E)]{\phi[b/x]}{\Forall x.\phi}   \]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   453
\subsection{Assumption rule}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   454
\index{meta-assumptions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   456
assume: cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   458
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
\item[\ttindexbold{assume} $ct$] 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   460
makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
The rule checks that $ct$ has type $prop$ and contains no unknowns, which
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   462
are not allowed in assumptions.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   463
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   465
\subsection{Implication rules}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   466
\index{meta-implication}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   468
implies_intr      : cterm -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   469
implies_intr_list : cterm list -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
implies_intr_hyps : thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
implies_elim      : thm -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
implies_elim_list : thm -> thm list -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   474
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
\item[\ttindexbold{implies_intr} $ct$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
is $({\Imp}I)$, where $ct$ is the assumption to discharge, say~$\phi$.  It
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   477
maps the premise~$\psi$ to the conclusion $\phi\Imp\psi$, removing all
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   478
occurrences of~$\phi$ from the assumptions.  The rule checks that $ct$ has
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   479
type $prop$. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   480
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
\item[\ttindexbold{implies_intr_list} $cts$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
applies $({\Imp}I)$ repeatedly, on every element of the list~$cts$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
\item[\ttindexbold{implies_intr_hyps} $thm$] 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   485
applies $({\Imp}I)$ to discharge all the hypotheses (assumptions) of~$thm$.
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   486
It maps the premise $\phi \; [\phi@1,\ldots,\phi@n]$ to the conclusion
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
$\List{\phi@1,\ldots,\phi@n}\Imp\phi$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
\item[\ttindexbold{implies_elim} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
applies $({\Imp}E)$ to $thm@1$ and~$thm@2$.  It maps the premises $\phi\Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
\psi$ and $\phi$ to the conclusion~$\psi$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
\item[\ttindexbold{implies_elim_list} $thm$ $thms$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
applies $({\Imp}E)$ repeatedly to $thm$, using each element of~$thms$ in
151
c5e636ca6576 corrected some obvious errors;
wenzelm
parents: 104
diff changeset
   495
turn.  It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   497
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   499
\subsection{Logical equivalence rules}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   500
\index{meta-equality}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
\begin{ttbox} 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   502
equal_intr : thm -> thm -> thm 
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   503
equal_elim : thm -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   505
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   506
\item[\ttindexbold{equal_intr} $thm@1$ $thm@2$] 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   507
applies $({\equiv}I)$ to $thm@1$ and~$thm@2$.  It maps the premises~$\psi$
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   508
and~$\phi$ to the conclusion~$\phi\equiv\psi$; the assumptions are those of
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   509
the first premise with~$\phi$ removed, plus those of
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   510
the second premise with~$\psi$ removed.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
\item[\ttindexbold{equal_elim} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
applies $({\equiv}E)$ to $thm@1$ and~$thm@2$.  It maps the premises
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
$\phi\equiv\psi$ and $\phi$ to the conclusion~$\psi$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   515
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
\subsection{Equality rules}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   519
\index{meta-equality}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   521
reflexive  : cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
symmetric  : thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
transitive : thm -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   525
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
\item[\ttindexbold{reflexive} $ct$] 
151
c5e636ca6576 corrected some obvious errors;
wenzelm
parents: 104
diff changeset
   527
makes the theorem \(ct\equiv ct\). 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
\item[\ttindexbold{symmetric} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
maps the premise $a\equiv b$ to the conclusion $b\equiv a$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
\item[\ttindexbold{transitive} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
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
   534
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
\subsection{The $\lambda$-conversion rules}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   538
\index{lambda calc@$\lambda$-calculus}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   539
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   540
beta_conversion : cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
extensional     : thm -> thm
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   542
abstract_rule   : string -> cterm -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
combination     : thm -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   544
\end{ttbox} 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   545
There is no rule for $\alpha$-conversion because Isabelle regards
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   546
$\alpha$-convertible theorems as equal.
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   547
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   548
\item[\ttindexbold{beta_conversion} $ct$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
makes the theorem $((\lambda x.a)(b)) \equiv a[b/x]$, where $ct$ is the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
term $(\lambda x.a)(b)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   552
\item[\ttindexbold{extensional} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   554
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
   555
variable (provided it does not occur in the assumptions); it must not occur
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   556
in $f$ or~$g$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   557
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
\item[\ttindexbold{abstract_rule} $v$ $x$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   560
(\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   561
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
   562
variable (provided it does not occur in the assumptions).  In the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
conclusion, the bound variable is named~$v$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   564
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   565
\item[\ttindexbold{combination} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
maps the premises $f\equiv g$ and $a\equiv b$ to the conclusion~$f(a)\equiv
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   567
g(b)$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   568
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   571
\subsection{Forall introduction rules}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   572
\index{meta-quantifiers}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   573
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   574
forall_intr       : cterm      -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   575
forall_intr_list  : cterm list -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   576
forall_intr_frees :               thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   577
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   578
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   579
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   580
\item[\ttindexbold{forall_intr} $x$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   581
applies $({\Forall}I)$, abstracting over all occurrences (if any!) of~$x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
The rule maps the premise $\phi$ to the conclusion $\Forall x.\phi$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   583
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
   584
variable (provided it does not occur in the assumptions).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   585
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   586
\item[\ttindexbold{forall_intr_list} $xs$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   587
applies $({\Forall}I)$ repeatedly, on every element of the list~$xs$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   588
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   589
\item[\ttindexbold{forall_intr_frees} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   590
applies $({\Forall}I)$ repeatedly, generalizing over all the free variables
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   591
of the premise.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   592
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   593
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   595
\subsection{Forall elimination rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   596
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   597
forall_elim       : cterm      -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   598
forall_elim_list  : cterm list -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   599
forall_elim_var   :        int -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   600
forall_elim_vars  :        int -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   601
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   602
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   603
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   604
\item[\ttindexbold{forall_elim} $ct$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   605
applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   606
$\phi[ct/x]$.  The rule checks that $ct$ and $x$ have the same type.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   607
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   608
\item[\ttindexbold{forall_elim_list} $cts$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   609
applies $({\Forall}E)$ repeatedly, on every element of the list~$cts$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   610
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
\item[\ttindexbold{forall_elim_var} $k$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   612
applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   613
$\phi[\Var{x@k}/x]$.  Thus, it replaces the outermost $\Forall$-bound
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   614
variable by an unknown having subscript~$k$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   615
9258
2121ff73a37d fixed typos reported by Jeremy Dawson
paulson
parents: 8969
diff changeset
   616
\item[\ttindexbold{forall_elim_vars} $k$ $thm$] 
2121ff73a37d fixed typos reported by Jeremy Dawson
paulson
parents: 8969
diff changeset
   617
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
   618
the form $\Forall x.\phi$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   619
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   620
8135
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   621
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   622
\subsection{Instantiation of unknowns}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   623
\index{instantiation}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   624
\begin{alltt}\footnotesize
3135
233aba197bf2 tuned spaces;
wenzelm
parents: 3108
diff changeset
   625
instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list -> thm -> thm
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   626
\end{alltt}
8135
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   627
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
   628
\ttindexbold{Thm.instantiate}, which merely performs the instantiation and can
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   629
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
   630
\ttindexbold{Drule.instantiate}, which normalizes its conclusion.
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   631
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   632
\begin{ttdescription}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 8135
diff changeset
   633
\item[\ttindexbold{instantiate} ($tyinsts$,$insts$) $thm$] 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   634
simultaneously substitutes types for type unknowns (the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   635
$tyinsts$) and terms for term unknowns (the $insts$).  Instantiations are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   636
given as $(v,t)$ pairs, where $v$ is an unknown and $t$ is a term (of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   637
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
   638
must be distinct.  
4376
407f786d3059 instantiate';
wenzelm
parents: 4317
diff changeset
   639
8135
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   640
In some cases, \ttindex{instantiate'} (see \S\ref{sec:instantiate})
4376
407f786d3059 instantiate';
wenzelm
parents: 4317
diff changeset
   641
provides a more convenient interface to this rule.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   642
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   643
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   644
8135
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   645
ad1c4a678196 Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents: 7871
diff changeset
   646
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   647
\subsection{Freezing/thawing type unknowns}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   648
\index{type unknowns!freezing/thawing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   649
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   650
freezeT: thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   651
varifyT: thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   652
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   653
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   654
\item[\ttindexbold{freezeT} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   655
converts all the type unknowns in $thm$ to free type variables.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   656
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   657
\item[\ttindexbold{varifyT} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   658
converts all the free type variables in $thm$ to type unknowns.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   659
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   660
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   661
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   662
\section{Derived rules for goal-directed proof}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
Most of these rules have the sole purpose of implementing particular
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   664
tactics.  There are few occasions for applying them directly to a theorem.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   665
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   666
\subsection{Proof by assumption}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   667
\index{meta-assumptions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   668
\begin{ttbox} 
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   669
assumption    : int -> thm -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   670
eq_assumption : int -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   671
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   672
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   673
\item[\ttindexbold{assumption} {\it i} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   674
attempts to solve premise~$i$ of~$thm$ by assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   675
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   676
\item[\ttindexbold{eq_assumption}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   677
is like {\tt assumption} but does not use unification.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   678
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   679
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   680
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
\subsection{Resolution}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   682
\index{resolution}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   683
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   684
biresolution : bool -> (bool*thm)list -> int -> thm
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   685
               -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   686
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   687
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   688
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$] 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   689
performs bi-resolution on subgoal~$i$ of $state$, using the list of $\it
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   690
(flag,rule)$ pairs.  For each pair, it applies resolution if the flag
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   691
is~{\tt false} and elim-resolution if the flag is~{\tt true}.  If $match$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   692
is~{\tt true}, the $state$ is not instantiated.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   693
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   694
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   695
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   696
\subsection{Composition: resolution without lifting}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   697
\index{resolution!without lifting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   698
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   699
compose   : thm * int * thm -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   700
COMP      : thm * thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   701
bicompose : bool -> bool * thm * int -> int -> thm
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   702
            -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   703
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   704
In forward proof, a typical use of composition is to regard an assertion of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   705
the form $\phi\Imp\psi$ as atomic.  Schematic variables are not renamed, so
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   706
beware of clashes!
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   707
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   708
\item[\ttindexbold{compose} ($thm@1$, $i$, $thm@2$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   709
uses $thm@1$, regarded as an atomic formula, to solve premise~$i$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   710
of~$thm@2$.  Let $thm@1$ and $thm@2$ be $\psi$ and $\List{\phi@1; \ldots;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   711
\phi@n} \Imp \phi$.  For each $s$ that unifies~$\psi$ and $\phi@i$, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   712
result list contains the theorem
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   713
\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   714
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   715
1119
49ed9a415637 Indexing of COMP
lcp
parents: 876
diff changeset
   716
\item[$thm@1$ \ttindexbold{COMP} $thm@2$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   717
calls \hbox{\tt compose ($thm@1$, 1, $thm@2$)} and returns the result, if
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   718
unique; otherwise, it raises exception~\xdx{THM}\@.  It is
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   719
analogous to {\tt RS}\@.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   720
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   721
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
   722
that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P$, which is the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   723
principle of contrapositives.  Then the result would be the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   724
derived rule $\neg(b=a)\Imp\neg(a=b)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   725
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   726
\item[\ttindexbold{bicompose} $match$ ($flag$, $rule$, $m$) $i$ $state$]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   727
refines subgoal~$i$ of $state$ using $rule$, without lifting.  The $rule$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   728
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
   729
$\psi$ need not be atomic; thus $m$ determines the number of new
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   730
subgoals.  If $flag$ is {\tt true} then it performs elim-resolution --- it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   731
solves the first premise of~$rule$ by assumption and deletes that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   732
assumption.  If $match$ is~{\tt true}, the $state$ is not instantiated.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   733
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   734
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   735
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   736
\subsection{Other meta-rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   737
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   738
trivial            : cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   739
lift_rule          : (thm * int) -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   740
rename_params_rule : string list * int -> thm -> thm
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   741
flexflex_rule      : thm -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   742
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   743
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   744
\item[\ttindexbold{trivial} $ct$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   745
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   746
This is the initial state for a goal-directed proof of~$\phi$.  The rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   747
checks that $ct$ has type~$prop$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   748
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   749
\item[\ttindexbold{lift_rule} ($state$, $i$) $rule$] \index{lifting}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   750
prepares $rule$ for resolution by lifting it over the parameters and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   751
assumptions of subgoal~$i$ of~$state$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   752
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   753
\item[\ttindexbold{rename_params_rule} ({\it names}, {\it i}) $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   754
uses the $names$ to rename the parameters of premise~$i$ of $thm$.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   755
names must be distinct.  If there are fewer names than parameters, then the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   756
rule renames the innermost parameters and may modify the remaining ones to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   757
ensure that all the parameters are distinct.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   758
\index{parameters!renaming}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   759
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   760
\item[\ttindexbold{flexflex_rule} $thm$]  \index{flex-flex constraints}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   761
removes all flex-flex pairs from $thm$ using the trivial unifier.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   762
\end{ttdescription}
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   763
\index{meta-rules|)}
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   764
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   765
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1590
diff changeset
   766
\section{Proof objects}\label{sec:proofObjects}
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   767
\index{proof objects|(} Isabelle can record the full meta-level proof of each
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   768
theorem.  The proof object contains all logical inferences in detail, while
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   769
omitting bookkeeping steps that have no logical meaning to an outside
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   770
observer.  Rewriting steps are recorded in similar detail as the output of
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   771
simplifier tracing.  The proof object can be inspected by a separate
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   772
proof-checker, for example.
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   773
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   774
Full proof objects are large.  They multiply storage requirements by about
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   775
seven; attempts to build large logics (such as {\sc zf} and {\sc hol}) may
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   776
fail.  Isabelle normally builds minimal proof objects, which include only uses
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   777
of oracles.  You can also request an intermediate level of detail, containing
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   778
uses of oracles, axioms and theorems.  These smaller proof objects indicate a
6924
7e166f8d412e Theorems involving oracles will be printed with a suffixed \verb|[!]|;
wenzelm
parents: 6097
diff changeset
   779
theorem's dependencies.  Theorems involving oracles will be printed with a
7e166f8d412e Theorems involving oracles will be printed with a suffixed \verb|[!]|;
wenzelm
parents: 6097
diff changeset
   780
suffixed \verb|[!]| to point out the different quality of confidence achieved.
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   781
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   782
Isabelle provides proof objects for the sake of transparency.  Their aim is to
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   783
increase your confidence in Isabelle.  They let you inspect proofs constructed
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   784
by the classical reasoner or simplifier, and inform you of all uses of
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   785
oracles.  Seldom will proof objects be given whole to an automatic
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   786
proof-checker: none has been written.  It is up to you to examine and
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   787
interpret them sensibly.  For example, when scrutinizing a theorem's
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   788
derivation for dependence upon some oracle or axiom, remember to scrutinize
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   789
all of its lemmas.  Their proofs are included in the main derivation, through
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   790
the {\tt Theorem} constructor.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   791
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   792
Proof objects are expressed using a polymorphic type of variable-branching
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   793
trees.  Proof objects (formally known as {\em derivations\/}) are trees
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   794
labelled by rules, where {\tt rule} is a complicated datatype declared in the
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   795
file {\tt Pure/thm.ML}.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   796
\begin{ttbox} 
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   797
datatype 'a mtree = Join of 'a * 'a mtree list;
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   798
datatype rule     = \(\ldots\);
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   799
type deriv        = rule mtree;
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   800
\end{ttbox}
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   801
%
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   802
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
   803
record: 
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   804
\begin{ttbox} 
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   805
#der (rep_thm conjI);
6097
04515352f19e fixed deriv;
wenzelm
parents: 5777
diff changeset
   806
{\out Join (Theorem ("HOL.conjI", []), [Join (MinProof,[])]) : deriv}
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   807
\end{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   808
This proof object identifies a labelled theorem, {\tt conjI} of theory
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   809
\texttt{HOL}, whose underlying proof has not been recorded; all we
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   810
have is {\tt MinProof}.
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   811
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   812
Nontrivial proof objects are unreadably large and complex.  Isabelle provides
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   813
several functions to help you inspect them informally.  These functions omit
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   814
the more obscure inferences and attempt to restructure the others into natural
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   815
formats, linear or tree-structured.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   816
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   817
\begin{ttbox} 
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   818
keep_derivs  : deriv_kind ref
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   819
Deriv.size   : deriv -> int
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   820
Deriv.drop   : 'a mtree * int -> 'a mtree
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   821
Deriv.linear : deriv -> deriv list
1876
b163e192a2bf Corrected typo involving derivations
paulson
parents: 1846
diff changeset
   822
Deriv.tree   : deriv -> Deriv.orule mtree
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   823
\end{ttbox}
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   824
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   825
\begin{ttdescription}
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   826
\item[\ttindexbold{keep_derivs} := MinDeriv $|$ ThmDeriv $|$ FullDeriv;] 
4597
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4383
diff changeset
   827
specifies one of the options for keeping derivations.  They can be
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   828
minimal (oracles only), include theorems and axioms, or be full.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   829
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   830
\item[\ttindexbold{Deriv.size} $der$] yields the size of a derivation,
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   831
  excluding lemmas.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   832
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   833
\item[\ttindexbold{Deriv.drop} ($tree$,$n$)] returns the subtree $n$ levels
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   834
  down, always following the first child.  It is good for stripping off
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   835
  outer level inferences that are used to put a theorem into standard form.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   836
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   837
\item[\ttindexbold{Deriv.linear} $der$] converts a derivation into a linear
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   838
  format, replacing the deep nesting by a list of rules.  Intuitively, this
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   839
  reveals the single-step Isabelle proof that is constructed internally by
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   840
  tactics.  
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   841
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   842
\item[\ttindexbold{Deriv.tree} $der$] converts a derivation into an
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   843
  object-level proof tree.  A resolution by an object-rule is converted to a
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   844
  tree node labelled by that rule.  Complications arise if the object-rule is
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   845
  itself derived in some way.  Nested resolutions are unravelled, but other
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   846
  operations on rules (such as rewriting) are left as-is.  
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   847
\end{ttdescription}
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   848
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   849
Functions {\tt Deriv.linear} and {\tt Deriv.tree} omit the proof of any named
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   850
theorems (constructor {\tt Theorem}) they encounter in a derivation.  Applying
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   851
them directly to the derivation of a named theorem is therefore pointless.
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   852
Use {\tt Deriv.drop} with argument~1 to skip over the initial {\tt Theorem}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   853
constructor.
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   854
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   855
\index{proof objects|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   856
\index{theorems|)}
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   857
7871
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   858
\medskip
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   859
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   860
The dependencies of theorems can be viewed using the function \ttindexbold{thm_deps}:
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   861
\begin{ttbox}
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   862
thm_deps [\(thm@1\), \(\ldots\), \(thm@n\)];
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   863
\end{ttbox}
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   864
generates the dependency graph of the theorems $thm@1$, $\ldots$, $thm@n$ and
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   865
displays it using Isabelle's graph browser. This function expects derivations
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   866
to be enabled. The structure \texttt{ThmDeps} contains the two functions
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   867
\begin{ttbox}
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   868
enable : unit -> unit
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   869
disable : unit -> unit
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   870
\end{ttbox}
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   871
which set \texttt{keep_derivs} appropriately.
30fb773113a1 Documented thm_deps.
berghofe
parents: 7644
diff changeset
   872
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   873
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   874
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   875
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   876
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   877
%%% End: