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