doc-src/Ref/thm.tex
author paulson
Fri, 27 Nov 1998 13:13:22 +0100
changeset 5980 2e9314c07146
parent 5777 5c0aa825c18e
child 6097 04515352f19e
permissions -rw-r--r--
added Real/Hyperreal
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} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
RSN : thm * (int * thm) -> thm                 \hfill{\bf infix}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
RS  : thm * thm -> thm                         \hfill{\bf infix}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
MRS : thm list * thm -> thm                    \hfill{\bf infix}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
RLN : thm list * (int * thm list) -> thm list  \hfill{\bf infix}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
RL  : thm list * thm list -> thm list          \hfill{\bf infix}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    81
MRL : thm list list * thm list -> thm list     \hfill{\bf infix}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    83
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
    84
functions are especially useful with destruction rules.  To store
5c18634db55d Under RS added cross reference to bind_thm
lcp
parents: 866
diff changeset
    85
the result in the theorem database, use \ttindex{bind_thm}
5c18634db55d Under RS added cross reference to bind_thm
lcp
parents: 866
diff changeset
    86
(\S\ref{ExtractingAndStoringTheProvedTheorem}). 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    87
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
\item[\tt$thm@1$ RSN $(i,thm@2)$] \indexbold{*RSN} 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    89
  resolves the conclusion of $thm@1$ with the $i$th premise of~$thm@2$.
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    90
  Unless there is precisely one resolvent it raises exception
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
    91
  \xdx{THM}; in that case, use {\tt RLN}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
\item[\tt$thm@1$ RS $thm@2$] \indexbold{*RS} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
abbreviates \hbox{\tt$thm@1$ RSN $(1,thm@2)$}.  Thus, it resolves the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
conclusion of $thm@1$ with the first premise of~$thm@2$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
\item[\tt {$[thm@1,\ldots,thm@n]$} MRS $thm$] \indexbold{*MRS} 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
    98
  uses {\tt RSN} to resolve $thm@i$ against premise~$i$ of $thm$, for
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
  $i=n$, \ldots,~1.  This applies $thm@n$, \ldots, $thm@1$ to the first $n$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
  premises of $thm$.  Because the theorems are used from right to left, it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
  does not matter if the $thm@i$ create new premises.  {\tt MRS} is useful
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
  for expressing proof trees.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
151
c5e636ca6576 corrected some obvious errors;
wenzelm
parents: 104
diff changeset
   104
\item[\tt$thms@1$ RLN $(i,thms@2)$] \indexbold{*RLN} 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   105
  joins lists of theorems.  For every $thm@1$ in $thms@1$ and $thm@2$ in
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   106
  $thms@2$, it resolves the conclusion of $thm@1$ with the $i$th premise
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   107
  of~$thm@2$, accumulating the results. 
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$ RL $thms@2$] \indexbold{*RL} 
c5e636ca6576 corrected some obvious errors;
wenzelm
parents: 104
diff changeset
   110
abbreviates \hbox{\tt$thms@1$ RLN $(1,thms@2)$}. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
\item[\tt {$[thms@1,\ldots,thms@n]$} MRL $thms$] \indexbold{*MRL} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
is analogous to {\tt MRS}, but combines theorem lists rather than theorems.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
It too is useful for expressing proof trees.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   115
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
\subsection{Expanding definitions in theorems}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   119
\index{meta-rewriting!in theorems}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
rewrite_rule       : thm list -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
rewrite_goals_rule : thm list -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   124
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
\item[\ttindexbold{rewrite_rule} {\it defs} {\it thm}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
unfolds the {\it defs} throughout the theorem~{\it thm}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
\item[\ttindexbold{rewrite_goals_rule} {\it defs} {\it thm}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
unfolds the {\it defs} in the premises of~{\it thm}, but leaves the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
conclusion unchanged.  This rule underlies \ttindex{rewrite_goals_tac}, but 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
serves little purpose in forward proof.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   132
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
4383
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   135
\subsection{Instantiating unknowns in a theorem} \label{sec:instantiate}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   136
\index{instantiation}
286
e7efbf03562b first draft of Springer book
lcp
parents: 151
diff changeset
   137
\begin{ttbox}
4383
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   138
read_instantiate    :                (string*string) list -> thm -> thm
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   139
read_instantiate_sg :     Sign.sg -> (string*string) list -> thm -> thm
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   140
cterm_instantiate   :                  (cterm*cterm) list -> thm -> thm
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   141
instantiate'      : ctyp option list -> cterm option list -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
These meta-rules instantiate type and term unknowns in a theorem.  They are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
occasionally useful.  They can prevent difficulties with higher-order
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
unification, and define specialized versions of rules.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   146
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
\item[\ttindexbold{read_instantiate} {\it insts} {\it thm}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
processes the instantiations {\it insts} and instantiates the rule~{\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
thm}.  The processing of instantiations is described
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   150
in \S\ref{res_inst_tac}, under {\tt res_inst_tac}.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
Use {\tt res_inst_tac}, not {\tt read_instantiate}, to instantiate a rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
and refine a particular subgoal.  The tactic allows instantiation by the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
subgoal's parameters, and reads the instantiations using the signature
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   155
associated with the proof state.
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   156
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   157
Use {\tt read_instantiate_sg} below if {\it insts\/} appears to be treated
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   158
incorrectly.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   160
\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
   161
  is like \texttt{read_instantiate {\it insts}~{\it thm}}, but it reads
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   162
  the instantiations under signature~{\it sg}.  This is necessary to
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   163
  instantiate a rule from a general theory, such as first-order logic,
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   164
  using the notation of some specialized theory.  Use the function {\tt
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   165
    sign_of} to get a theory's signature.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
\item[\ttindexbold{cterm_instantiate} {\it ctpairs} {\it thm}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
is similar to {\tt read_instantiate}, but the instantiations are provided
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
as pairs of certified terms, not as strings to be read.
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   170
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   171
\item[\ttindexbold{instantiate'} {\it ctyps} {\it cterms} {\it thm}]
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   172
  instantiates {\it thm} according to the positional arguments {\it
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   173
    ctyps} and {\it cterms}.  Counting from left to right, schematic
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   174
  variables $?x$ are either replaced by $t$ for any argument
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   175
  \texttt{Some\(\;t\)}, or left unchanged in case of \texttt{None} or
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   176
  if the end of the argument list is encountered.  Types are
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   177
  instantiated before terms.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   178
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   179
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 332
diff changeset
   182
\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   183
\index{theorems!standardizing}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
\begin{ttbox} 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   185
standard         :           thm -> thm
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   186
zero_var_indexes :           thm -> thm
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   187
make_elim        :           thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
rule_by_tactic   : tactic -> thm -> thm
4607
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   189
rotate_prems     :    int -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   191
\begin{ttdescription}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   192
\item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   193
  of object-rules.  It discharges all meta-assumptions, replaces free
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   194
  variables by schematic variables, renames schematic variables to
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   195
  have subscript zero, also strips outer (meta) quantifiers and
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   196
  removes dangling sort hypotheses.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
\item[\ttindexbold{zero_var_indexes} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
makes all schematic variables have subscript zero, renaming them to avoid
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
clashes. 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
\item[\ttindexbold{make_elim} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
\index{rules!converting destruction to elimination}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
converts $thm$, a destruction rule of the form $\List{P@1;\ldots;P@m}\Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
Q$, to the elimination rule $\List{P@1; \ldots; P@m; Q\Imp R}\Imp R$.  This
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
is the basis for destruct-resolution: {\tt dresolve_tac}, etc.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
\item[\ttindexbold{rule_by_tactic} {\it tac} {\it thm}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
  applies {\it tac\/} to the {\it thm}, freezing its variables first, then
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
  yields the proof state returned by the tactic.  In typical usage, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
  {\it thm\/} represents an instance of a rule with several premises, some
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
  with contradictory assumptions (because of the instantiation).  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
  tactic proves those subgoals and does whatever else it can, and returns
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
  whatever is left.
4607
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   215
  
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   216
\item[\ttindexbold{rotate_prems} $k$ $thm$] rotates the premises of $thm$ to
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   217
  the left by~$k$ positions.  It requires $0\leq k\leq n$, where $n$ is the
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   218
  number of premises; the rotation has no effect if $k$ is at either extreme.
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   219
  Used with \texttt{eresolve_tac}\index{*eresolve_tac!on other than first
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   220
    premise}, it gives the effect of applying the tactic to some other premise
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
   221
  of $thm$ than the first.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   222
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
\subsection{Taking a theorem apart}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   226
\index{theorems!taking apart}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
\index{flex-flex constraints}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
\begin{ttbox} 
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   229
cprop_of      : thm -> cterm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
concl_of      : thm -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
prems_of      : thm -> term list
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   232
cprems_of     : thm -> cterm list
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
nprems_of     : thm -> int
4383
25704541008b Tidying to fix overfull lines, etc
paulson
parents: 4376
diff changeset
   234
tpairs_of     : thm -> (term*term) list
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   235
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
   236
theory_of_thm : thm -> theory
4597
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4383
diff changeset
   237
dest_state    : thm * int -> (term*term) list * term list * term * term
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   238
rep_thm       : thm -> {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int,
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   239
                        shyps: sort list, hyps: term list, prop: term\ttrbrace
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   240
crep_thm      : thm -> {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int,
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   241
                        shyps: sort list, hyps: cterm list, prop: cterm\ttrbrace
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   243
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   244
\item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   245
  a certified term.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   246
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   247
\item[\ttindexbold{concl_of} $thm$] returns the conclusion of $thm$ as
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   248
  a term.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   249
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   250
\item[\ttindexbold{prems_of} $thm$] returns the premises of $thm$ as a
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   251
  list of terms.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   252
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   253
\item[\ttindexbold{cprems_of} $thm$] returns the premises of $thm$ as
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   254
  a list of certified terms.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
\item[\ttindexbold{nprems_of} $thm$] 
286
e7efbf03562b first draft of Springer book
lcp
parents: 151
diff changeset
   257
returns the number of premises in $thm$, and is equivalent to {\tt
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   258
  length~(prems_of~$thm$)}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   260
\item[\ttindexbold{tpairs_of} $thm$] returns the flex-flex constraints
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   261
  of $thm$.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   262
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   263
\item[\ttindexbold{sign_of_thm} $thm$] returns the signature
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   264
  associated with $thm$.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   265
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   266
\item[\ttindexbold{theory_of_thm} $thm$] returns the theory associated
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   267
  with $thm$.  Note that this does a lookup in Isabelle's global
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   268
  database of loaded theories.
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 332
diff changeset
   269
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
\item[\ttindexbold{dest_state} $(thm,i)$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
(this will be an implication if there are more than $i$ subgoals).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   275
\item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   276
  containing the statement of~$thm$ ({\tt prop}), its list of
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   277
  meta-assumptions ({\tt hyps}), its derivation ({\tt der}), a bound
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   278
  on the maximum subscript of its unknowns ({\tt maxidx}), and a
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   279
  reference to its signature ({\tt sign_ref}).  The {\tt shyps} field
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   280
  is discussed below.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   281
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   282
\item[\ttindexbold{crep_thm} $thm$] like \texttt{rep_thm}, but returns
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   283
  the hypotheses and statement as certified terms.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   284
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   285
\end{ttdescription}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   286
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   287
5777
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   288
\subsection{*Sort hypotheses} \label{sec:sort-hyps}
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   289
\index{sort hypotheses}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   290
\begin{ttbox} 
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   291
force_strip_shyps : bool ref \hfill{\bf initially true}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   292
\end{ttbox}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   293
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   294
\begin{ttdescription}
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   295
\item[\ttindexbold{force_strip_shyps}]
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   296
causes sort hypotheses to be deleted, printing a warning.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   297
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
2044
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   299
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
   300
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
   301
syntactic classification of types --- for example, FOL distinguishes between
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   302
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
   303
this may result in some sorts becoming {\em empty\/}: where one cannot exhibit
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   304
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
   305
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   306
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
   307
sort, then that theorem has no instances.  It is basically an instance
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   308
of {\em ex falso quodlibet}.  But what if it is used to prove another
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   309
theorem that no longer involves that sort?  The latter theorem holds
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   310
only if under an additional non-emptiness assumption.
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   311
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   312
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
   313
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
   314
{\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
   315
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
   316
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
   317
critical ones, asserting non-emptiness of the corresponding sorts.
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   318
 
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   319
Isabelle tries to remove extraneous sorts from the {\tt shyps} field whenever
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   320
non-emptiness can be established by looking at the theorem's signature: from
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   321
the {\tt arities} information, etc.  Because its current implementation is
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   322
highly incomplete, the flag shown above is available.  Setting it to true (the
e8d52d05530a Improved discussion of shyps thanks to Markus Wenzel
paulson
parents: 2040
diff changeset
   323
default) allows existing proofs to run.
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   324
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
\subsection{Tracing flags for unification}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   327
\index{tracing!of unification}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
Unify.trace_simp   : bool ref \hfill{\bf initially false}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
Unify.trace_types  : bool ref \hfill{\bf initially false}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
Unify.trace_bound  : int ref \hfill{\bf initially 10}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
Unify.search_bound : int ref \hfill{\bf initially 20}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
Tracing the search may be useful when higher-order unification behaves
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
unexpectedly.  Letting {\tt res_inst_tac} circumvent the problem is easier,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
though.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   337
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   338
\item[set Unify.trace_simp;] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
causes tracing of the simplification phase.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   341
\item[set Unify.trace_types;] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
generates warnings of incompleteness, when unification is not considering
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
all possible instantiations of type unknowns.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   345
\item[Unify.trace_bound := $n$;] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
causes unification to print tracing information once it reaches depth~$n$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
Use $n=0$ for full tracing.  At the default value of~10, tracing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
information is almost never printed.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   350
\item[Unify.search_bound := $n$;] causes unification to limit its
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   351
  search to depth~$n$.  Because of this bound, higher-order
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   352
  unification cannot return an infinite sequence, though it can return
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   353
  a very long one.  The search rarely approaches the default value
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   354
  of~20.  If the search is cut off, unification prints a warning
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   355
  \texttt{Unification bound exceeded}.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   356
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   359
\section{*Primitive meta-level inference rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
\index{meta-rules|(}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   361
These implement the meta-logic in the style of the {\sc lcf} system,
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   362
as functions from theorems to theorems.  They are, rarely, useful for
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   363
deriving results in the pure theory.  Mainly, they are included for
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   364
completeness, and most users should not bother with them.  The
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   365
meta-rules raise exception \xdx{THM} to signal malformed premises,
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   366
incompatible signatures and similar errors.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   368
\index{meta-assumptions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
The meta-logic uses natural deduction.  Each theorem may depend on
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   370
meta-level assumptions.  Certain rules, such as $({\Imp}I)$,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
discharge assumptions; in most other rules, the conclusion depends on all
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
of the assumptions of the premises.  Formally, the system works with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
assertions of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
\[ \phi \quad [\phi@1,\ldots,\phi@n], \]
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   375
where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions.  This can be
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   376
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
   377
\phi$.  Do not confuse meta-level assumptions with the object-level
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   378
assumptions in a subgoal, which are represented in the meta-logic
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   379
using~$\Imp$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
Each theorem has a signature.  Certified terms have a signature.  When a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
rule takes several premises and certified terms, it merges the signatures
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
to make a signature for the conclusion.  This fails if the signatures are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
incompatible. 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
5777
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   386
\medskip
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   387
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   388
The following presentation of primitive rules ignores sort
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   389
hypotheses\index{sort hypotheses} (see also \S\ref{sec:sort-hyps}).  These are
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   390
handled transparently by the logic implementation.
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   391
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   392
\bigskip
5c0aa825c18e shyps note for prim. rules;
wenzelm
parents: 5371
diff changeset
   393
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   394
\index{meta-implication}
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   395
The {\bf implication} rules are $({\Imp}I)$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
and $({\Imp}E)$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}}  \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
   \infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi}  \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   400
\index{meta-equality}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
Equality of truth values means logical equivalence:
3524
c02cb15830de fixed EqI meta rule;
wenzelm
parents: 3485
diff changeset
   402
\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi &
c02cb15830de fixed EqI meta rule;
wenzelm
parents: 3485
diff changeset
   403
                                       \psi\Imp\phi}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
   \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
   \infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   407
The {\bf equality} rules are reflexivity, symmetry, and transitivity:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
\[ {a\equiv a}\,(refl)  \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
   \infer[(sym)]{b\equiv a}{a\equiv b}  \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
   \infer[(trans)]{a\equiv c}{a\equiv b & b\equiv c}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   412
\index{lambda calc@$\lambda$-calculus}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
The $\lambda$-conversions are $\alpha$-conversion, $\beta$-conversion, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
extensionality:\footnote{$\alpha$-conversion holds if $y$ is not free
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
in~$a$; $(ext)$ holds if $x$ is not free in the assumptions, $f$, or~$g$.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
\[ {(\lambda x.a) \equiv (\lambda y.a[y/x])}    \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
   {((\lambda x.a)(b)) \equiv a[b/x]}           \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
   \infer[(ext)]{f\equiv g}{f(x) \equiv g(x)}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   420
The {\bf abstraction} and {\bf combination} rules let conversions be
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   421
applied to subterms:\footnote{Abstraction holds if $x$ is not free in the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
assumptions.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
\[  \infer[(abs)]{(\lambda x.a) \equiv (\lambda x.b)}{a\equiv b}   \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
    \infer[(comb)]{f(a)\equiv g(b)}{f\equiv g & a\equiv b}   \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   426
\index{meta-quantifiers}
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   427
The {\bf universal quantification} rules are $(\Forall I)$ and $(\Forall
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
E)$:\footnote{$(\Forall I)$ holds if $x$ is not free in the assumptions.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
\[ \infer[(\Forall I)]{\Forall x.\phi}{\phi}        \qquad
286
e7efbf03562b first draft of Springer book
lcp
parents: 151
diff changeset
   430
   \infer[(\Forall E)]{\phi[b/x]}{\Forall x.\phi}   \]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   433
\subsection{Assumption rule}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   434
\index{meta-assumptions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   436
assume: cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   438
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
\item[\ttindexbold{assume} $ct$] 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   440
makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
The rule checks that $ct$ has type $prop$ and contains no unknowns, which
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   442
are not allowed in assumptions.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   443
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   445
\subsection{Implication rules}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   446
\index{meta-implication}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   447
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   448
implies_intr      : cterm -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   449
implies_intr_list : cterm list -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
implies_intr_hyps : thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
implies_elim      : thm -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
implies_elim_list : thm -> thm list -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   454
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
\item[\ttindexbold{implies_intr} $ct$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
is $({\Imp}I)$, where $ct$ is the assumption to discharge, say~$\phi$.  It
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   457
maps the premise~$\psi$ to the conclusion $\phi\Imp\psi$, removing all
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   458
occurrences of~$\phi$ from the assumptions.  The rule checks that $ct$ has
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   459
type $prop$. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
\item[\ttindexbold{implies_intr_list} $cts$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
applies $({\Imp}I)$ repeatedly, on every element of the list~$cts$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
\item[\ttindexbold{implies_intr_hyps} $thm$] 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   465
applies $({\Imp}I)$ to discharge all the hypotheses (assumptions) of~$thm$.
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   466
It maps the premise $\phi \; [\phi@1,\ldots,\phi@n]$ to the conclusion
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
$\List{\phi@1,\ldots,\phi@n}\Imp\phi$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
\item[\ttindexbold{implies_elim} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
applies $({\Imp}E)$ to $thm@1$ and~$thm@2$.  It maps the premises $\phi\Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
\psi$ and $\phi$ to the conclusion~$\psi$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
\item[\ttindexbold{implies_elim_list} $thm$ $thms$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
applies $({\Imp}E)$ repeatedly to $thm$, using each element of~$thms$ in
151
c5e636ca6576 corrected some obvious errors;
wenzelm
parents: 104
diff changeset
   475
turn.  It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   477
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   479
\subsection{Logical equivalence rules}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   480
\index{meta-equality}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
\begin{ttbox} 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   482
equal_intr : thm -> thm -> thm 
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   483
equal_elim : thm -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   485
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
\item[\ttindexbold{equal_intr} $thm@1$ $thm@2$] 
332
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   487
applies $({\equiv}I)$ to $thm@1$ and~$thm@2$.  It maps the premises~$\psi$
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   488
and~$\phi$ to the conclusion~$\phi\equiv\psi$; the assumptions are those of
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   489
the first premise with~$\phi$ removed, plus those of
01b87a921967 final Springer copy
lcp
parents: 326
diff changeset
   490
the second premise with~$\psi$ removed.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
\item[\ttindexbold{equal_elim} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
applies $({\equiv}E)$ to $thm@1$ and~$thm@2$.  It maps the premises
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
$\phi\equiv\psi$ and $\phi$ to the conclusion~$\psi$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   495
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
\subsection{Equality rules}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   499
\index{meta-equality}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   501
reflexive  : cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
symmetric  : thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
transitive : thm -> thm -> thm
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{reflexive} $ct$] 
151
c5e636ca6576 corrected some obvious errors;
wenzelm
parents: 104
diff changeset
   507
makes the theorem \(ct\equiv ct\). 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
\item[\ttindexbold{symmetric} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
maps the premise $a\equiv b$ to the conclusion $b\equiv a$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
\item[\ttindexbold{transitive} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
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
   514
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
\subsection{The $\lambda$-conversion rules}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   518
\index{lambda calc@$\lambda$-calculus}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   520
beta_conversion : cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   521
extensional     : thm -> thm
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   522
abstract_rule   : string -> cterm -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
combination     : thm -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
\end{ttbox} 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   525
There is no rule for $\alpha$-conversion because Isabelle regards
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   526
$\alpha$-convertible theorems as equal.
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   527
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
\item[\ttindexbold{beta_conversion} $ct$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
makes the theorem $((\lambda x.a)(b)) \equiv a[b/x]$, where $ct$ is the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
term $(\lambda x.a)(b)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
\item[\ttindexbold{extensional} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
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
   535
variable (provided it does not occur in the assumptions); it must not occur
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
in $f$ or~$g$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   538
\item[\ttindexbold{abstract_rule} $v$ $x$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   539
maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   540
(\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
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
   542
variable (provided it does not occur in the assumptions).  In the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
conclusion, the bound variable is named~$v$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   544
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   545
\item[\ttindexbold{combination} $thm@1$ $thm@2$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   546
maps the premises $f\equiv g$ and $a\equiv b$ to the conclusion~$f(a)\equiv
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   547
g(b)$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   548
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   551
\subsection{Forall introduction rules}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   552
\index{meta-quantifiers}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   554
forall_intr       : cterm      -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   555
forall_intr_list  : cterm list -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   556
forall_intr_frees :               thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   557
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   559
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   560
\item[\ttindexbold{forall_intr} $x$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   561
applies $({\Forall}I)$, abstracting over all occurrences (if any!) of~$x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   562
The rule maps the premise $\phi$ to the conclusion $\Forall x.\phi$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
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
   564
variable (provided it does not occur in the assumptions).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   565
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
\item[\ttindexbold{forall_intr_list} $xs$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   567
applies $({\Forall}I)$ repeatedly, on every element of the list~$xs$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   568
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
\item[\ttindexbold{forall_intr_frees} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
applies $({\Forall}I)$ repeatedly, generalizing over all the free variables
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
of the premise.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   572
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   573
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   574
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   575
\subsection{Forall elimination rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   576
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   577
forall_elim       : cterm      -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   578
forall_elim_list  : cterm list -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   579
forall_elim_var   :        int -> thm -> thm
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   580
forall_elim_vars  :        int -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   581
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   583
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   584
\item[\ttindexbold{forall_elim} $ct$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   585
applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   586
$\phi[ct/x]$.  The rule checks that $ct$ and $x$ have the same type.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   587
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   588
\item[\ttindexbold{forall_elim_list} $cts$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   589
applies $({\Forall}E)$ repeatedly, on every element of the list~$cts$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   590
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   591
\item[\ttindexbold{forall_elim_var} $k$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   592
applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   593
$\phi[\Var{x@k}/x]$.  Thus, it replaces the outermost $\Forall$-bound
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
variable by an unknown having subscript~$k$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   595
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   596
\item[\ttindexbold{forall_elim_vars} $ks$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   597
applies {\tt forall_elim_var} repeatedly, for every element of the list~$ks$.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   598
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   599
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   600
\subsection{Instantiation of unknowns}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   601
\index{instantiation}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   602
\begin{ttbox} 
3135
233aba197bf2 tuned spaces;
wenzelm
parents: 3108
diff changeset
   603
instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list -> thm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   604
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   605
\begin{ttdescription}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   606
\item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$] 
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   607
simultaneously substitutes types for type unknowns (the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   608
$tyinsts$) and terms for term unknowns (the $insts$).  Instantiations are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   609
given as $(v,t)$ pairs, where $v$ is an unknown and $t$ is a term (of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   610
same type as $v$) or a type (of the same sort as~$v$).  All the unknowns
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
must be distinct.  The rule normalizes its conclusion.
4376
407f786d3059 instantiate';
wenzelm
parents: 4317
diff changeset
   612
407f786d3059 instantiate';
wenzelm
parents: 4317
diff changeset
   613
Note that \ttindex{instantiate'} (see \S\ref{sec:instantiate})
407f786d3059 instantiate';
wenzelm
parents: 4317
diff changeset
   614
provides a more convenient interface to this rule.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   615
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   616
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   617
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   618
\subsection{Freezing/thawing type unknowns}
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   619
\index{type unknowns!freezing/thawing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   620
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   621
freezeT: thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   622
varifyT: thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   623
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   624
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   625
\item[\ttindexbold{freezeT} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   626
converts all the type unknowns in $thm$ to free type variables.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   627
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   628
\item[\ttindexbold{varifyT} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   629
converts all the free type variables in $thm$ to type unknowns.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   630
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   631
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   632
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   633
\section{Derived rules for goal-directed proof}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   634
Most of these rules have the sole purpose of implementing particular
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   635
tactics.  There are few occasions for applying them directly to a theorem.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   636
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   637
\subsection{Proof by assumption}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   638
\index{meta-assumptions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   639
\begin{ttbox} 
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   640
assumption    : int -> thm -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   641
eq_assumption : int -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   642
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   643
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   644
\item[\ttindexbold{assumption} {\it i} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   645
attempts to solve premise~$i$ of~$thm$ by assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   646
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   647
\item[\ttindexbold{eq_assumption}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   648
is like {\tt assumption} but does not use unification.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   649
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   650
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   651
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   652
\subsection{Resolution}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   653
\index{resolution}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   654
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   655
biresolution : bool -> (bool*thm)list -> int -> thm
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   656
               -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   657
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   658
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   659
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$] 
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   660
performs bi-resolution on subgoal~$i$ of $state$, using the list of $\it
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   661
(flag,rule)$ pairs.  For each pair, it applies resolution if the flag
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   662
is~{\tt false} and elim-resolution if the flag is~{\tt true}.  If $match$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
is~{\tt true}, the $state$ is not instantiated.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   664
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   665
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   666
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   667
\subsection{Composition: resolution without lifting}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   668
\index{resolution!without lifting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   669
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   670
compose   : thm * int * thm -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   671
COMP      : thm * thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   672
bicompose : bool -> bool * thm * int -> int -> thm
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   673
            -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   674
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   675
In forward proof, a typical use of composition is to regard an assertion of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   676
the form $\phi\Imp\psi$ as atomic.  Schematic variables are not renamed, so
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   677
beware of clashes!
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   678
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   679
\item[\ttindexbold{compose} ($thm@1$, $i$, $thm@2$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   680
uses $thm@1$, regarded as an atomic formula, to solve premise~$i$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
of~$thm@2$.  Let $thm@1$ and $thm@2$ be $\psi$ and $\List{\phi@1; \ldots;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
\phi@n} \Imp \phi$.  For each $s$ that unifies~$\psi$ and $\phi@i$, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   683
result list contains the theorem
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   684
\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   685
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   686
1119
49ed9a415637 Indexing of COMP
lcp
parents: 876
diff changeset
   687
\item[$thm@1$ \ttindexbold{COMP} $thm@2$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   688
calls \hbox{\tt compose ($thm@1$, 1, $thm@2$)} and returns the result, if
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   689
unique; otherwise, it raises exception~\xdx{THM}\@.  It is
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   690
analogous to {\tt RS}\@.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   691
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   692
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
   693
that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P$, which is the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   694
principle of contrapositives.  Then the result would be the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   695
derived rule $\neg(b=a)\Imp\neg(a=b)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   696
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   697
\item[\ttindexbold{bicompose} $match$ ($flag$, $rule$, $m$) $i$ $state$]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   698
refines subgoal~$i$ of $state$ using $rule$, without lifting.  The $rule$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   699
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
   700
$\psi$ need not be atomic; thus $m$ determines the number of new
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   701
subgoals.  If $flag$ is {\tt true} then it performs elim-resolution --- it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   702
solves the first premise of~$rule$ by assumption and deletes that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   703
assumption.  If $match$ is~{\tt true}, the $state$ is not instantiated.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   704
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   705
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   706
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   707
\subsection{Other meta-rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   708
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2044
diff changeset
   709
trivial            : cterm -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   710
lift_rule          : (thm * int) -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   711
rename_params_rule : string list * int -> thm -> thm
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3657
diff changeset
   712
flexflex_rule      : thm -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   713
\end{ttbox}
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   714
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   715
\item[\ttindexbold{trivial} $ct$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   716
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   717
This is the initial state for a goal-directed proof of~$\phi$.  The rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   718
checks that $ct$ has type~$prop$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   719
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   720
\item[\ttindexbold{lift_rule} ($state$, $i$) $rule$] \index{lifting}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   721
prepares $rule$ for resolution by lifting it over the parameters and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   722
assumptions of subgoal~$i$ of~$state$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   723
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   724
\item[\ttindexbold{rename_params_rule} ({\it names}, {\it i}) $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   725
uses the $names$ to rename the parameters of premise~$i$ of $thm$.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   726
names must be distinct.  If there are fewer names than parameters, then the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   727
rule renames the innermost parameters and may modify the remaining ones to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   728
ensure that all the parameters are distinct.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   729
\index{parameters!renaming}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   730
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   731
\item[\ttindexbold{flexflex_rule} $thm$]  \index{flex-flex constraints}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   732
removes all flex-flex pairs from $thm$ using the trivial unifier.
326
bef614030e24 penultimate Springer draft
lcp
parents: 286
diff changeset
   733
\end{ttdescription}
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   734
\index{meta-rules|)}
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   735
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   736
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1590
diff changeset
   737
\section{Proof objects}\label{sec:proofObjects}
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   738
\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
   739
theorem.  The proof object contains all logical inferences in detail, while
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   740
omitting bookkeeping steps that have no logical meaning to an outside
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   741
observer.  Rewriting steps are recorded in similar detail as the output of
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   742
simplifier tracing.  The proof object can be inspected by a separate
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   743
proof-checker, for example.
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   744
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   745
Full proof objects are large.  They multiply storage requirements by about
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   746
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
   747
fail.  Isabelle normally builds minimal proof objects, which include only uses
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   748
of oracles.  You can also request an intermediate level of detail, containing
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   749
uses of oracles, axioms and theorems.  These smaller proof objects indicate a
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   750
theorem's dependencies.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   751
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   752
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
   753
increase your confidence in Isabelle.  They let you inspect proofs constructed
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   754
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
   755
oracles.  Seldom will proof objects be given whole to an automatic
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   756
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
   757
interpret them sensibly.  For example, when scrutinizing a theorem's
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   758
derivation for dependence upon some oracle or axiom, remember to scrutinize
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   759
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
   760
the {\tt Theorem} constructor.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   761
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   762
Proof objects are expressed using a polymorphic type of variable-branching
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   763
trees.  Proof objects (formally known as {\em derivations\/}) are trees
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   764
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
   765
file {\tt Pure/thm.ML}.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   766
\begin{ttbox} 
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   767
datatype 'a mtree = Join of 'a * 'a mtree list;
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   768
datatype rule     = \(\ldots\);
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   769
type deriv        = rule mtree;
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   770
\end{ttbox}
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   771
%
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   772
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
   773
record: 
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   774
\begin{ttbox} 
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   775
#der (rep_thm conjI);
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   776
{\out Join (Theorem "HOL.conjI", [Join (MinProof,[])]) : deriv}
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   777
\end{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   778
This proof object identifies a labelled theorem, {\tt conjI} of theory
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   779
\texttt{HOL}, whose underlying proof has not been recorded; all we
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   780
have is {\tt MinProof}.
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
Nontrivial proof objects are unreadably large and complex.  Isabelle provides
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   783
several functions to help you inspect them informally.  These functions omit
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   784
the more obscure inferences and attempt to restructure the others into natural
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   785
formats, linear or tree-structured.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   786
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   787
\begin{ttbox} 
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   788
keep_derivs  : deriv_kind ref
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   789
Deriv.size   : deriv -> int
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   790
Deriv.drop   : 'a mtree * int -> 'a mtree
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   791
Deriv.linear : deriv -> deriv list
1876
b163e192a2bf Corrected typo involving derivations
paulson
parents: 1846
diff changeset
   792
Deriv.tree   : deriv -> Deriv.orule mtree
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   793
\end{ttbox}
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   794
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   795
\begin{ttdescription}
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   796
\item[\ttindexbold{keep_derivs} := MinDeriv $|$ ThmDeriv $|$ FullDeriv;] 
4597
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4383
diff changeset
   797
specifies one of the options for keeping derivations.  They can be
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   798
minimal (oracles only), include theorems and axioms, or be full.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   799
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   800
\item[\ttindexbold{Deriv.size} $der$] yields the size of a derivation,
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   801
  excluding lemmas.
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   802
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   803
\item[\ttindexbold{Deriv.drop} ($tree$,$n$)] returns the subtree $n$ levels
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   804
  down, always following the first child.  It is good for stripping off
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   805
  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
   806
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   807
\item[\ttindexbold{Deriv.linear} $der$] converts a derivation into a linear
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   808
  format, replacing the deep nesting by a list of rules.  Intuitively, this
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   809
  reveals the single-step Isabelle proof that is constructed internally by
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   810
  tactics.  
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
\item[\ttindexbold{Deriv.tree} $der$] converts a derivation into an
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   813
  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
   814
  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
   815
  itself derived in some way.  Nested resolutions are unravelled, but other
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   816
  operations on rules (such as rewriting) are left as-is.  
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   817
\end{ttdescription}
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   818
2040
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   819
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
   820
theorems (constructor {\tt Theorem}) they encounter in a derivation.  Applying
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   821
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
   822
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
   823
constructor.
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   824
6db93e6f1b11 Documented sort hypotheses and improved discussion of derivations
paulson
parents: 1876
diff changeset
   825
1590
1547174673e1 Describes proof objects and Deriv module
paulson
parents: 1119
diff changeset
   826
\index{proof objects|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   827
\index{theorems|)}
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   828
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   829
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   830
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   831
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   832
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   833
%%% End: