doc-src/Ref/goals.tex
author clasohm
Thu, 19 Jan 1995 16:05:21 +0100
changeset 866 2d3d020eef11
parent 507 a00301e9e64b
child 1222 d99d13a0213f
permissions -rw-r--r--
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of and theory_of_thm
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{Proof Management: The Subgoal Module}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\index{proofs|(}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
\index{subgoal module|(}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
\index{reading!goals|see{proofs, starting}}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
     6
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
     7
The subgoal module stores the current proof state\index{proof state} and
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
     8
many previous states; commands can produce new states or return to previous
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
     9
ones.  The {\em state list\/} at level $n$ is a list of pairs
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
\[ [(\psi@n,\Psi@n),\; (\psi@{n-1},\Psi@{n-1}),\; \ldots,\; (\psi@0,[])] \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
where $\psi@n$ is the current proof state, $\psi@{n-1}$ is the previous
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
one, \ldots, and $\psi@0$ is the initial proof state.  The $\Psi@i$ are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
sequences (lazy lists) of proof states, storing branch points where a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
tactic returned a list longer than one.  The state lists permit various
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
forms of backtracking.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
Chopping elements from the state list reverts to previous proof states.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
Besides this, the \ttindex{undo} command keeps a list of state lists.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
module actually maintains a stack of state lists, to support several
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
proofs at the same time.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
The subgoal module always contains some proof state.  At the start of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
Isabelle session, this state consists of a dummy formula.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
\section{Basic commands}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
Most proofs begin with {\tt goal} or {\tt goalw} and require no other
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
commands than {\tt by}, {\tt chop} and {\tt undo}.  They typically end with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
a call to {\tt result}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
\subsection{Starting a backward proof}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    31
\index{proofs!starting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
goal        : theory -> string -> thm list 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
goalw       : theory -> thm list -> string -> thm list 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
goalw_cterm : thm list -> Sign.cterm -> thm list 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
premises    : unit -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
The {\tt goal} commands start a new proof by setting the goal.  They
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
replace the current state list by a new one consisting of the initial proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
state.  They also empty the \ttindex{undo} list; this command cannot be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
undone!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
They all return a list of meta-hypotheses taken from the main goal.  If
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
this list is non-empty, bind its value to an \ML{} identifier by typing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
something like
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
\begin{ttbox} 
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
    47
val prems = goal{\it theory\/ formula};
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    48
\end{ttbox}\index{assumptions!of main goal}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
These assumptions serve as the premises when you are deriving a rule.  They
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
are also stored internally and can be retrieved later by the function {\tt
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    51
  premises}.  When the proof is finished, {\tt result} compares the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
stored assumptions with the actual assumptions in the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    54
\index{definitions!unfolding}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
Some of the commands unfold definitions using meta-rewrite rules.  This
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
    56
expansion affects both the initial subgoal and the premises, which would
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    57
otherwise require use of {\tt rewrite_goals_tac} and
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    58
{\tt rewrite_rule}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    60
\index{*"!"! symbol!in main goal}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    61
If the main goal has the form {\tt"!!{\it vars}.\ \ldots"}, with an
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    62
outermost quantifier, then the list of premises will be empty.  Subgoal~1
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    63
will contain the meta-quantified {\it vars\/} as parameters and the goal's
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    64
premises as assumptions.  This avoids having to call
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    65
\ttindex{cut_facts_tac} with the list of premises (\S\ref{cut_facts_tac}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    67
\begin{ttdescription}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    68
\item[\ttindexbold{goal} {\it theory} {\it formula};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
begins a new proof, where {\it theory} is usually an \ML\ identifier
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
and the {\it formula\/} is written as an \ML\ string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    72
\item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
is like {\tt goal} but also applies the list of {\it defs\/} as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
meta-rewrite rules to the first subgoal and the premises.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    75
\index{meta-rewriting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    77
\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct};] 
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    78
is a version of {\tt goalw} for programming applications.  The main goal is
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
supplied as a cterm, not as a string.  Typically, the cterm is created from
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
a term~$t$ by \hbox{\tt Sign.cterm_of (sign_of thy) $t$}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
\index{*Sign.cterm_of}\index{*sign_of}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
\item[\ttindexbold{premises}()] 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    84
returns the list of meta-hypotheses associated with the current proof (in
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    85
case you forgot to bind them to an \ML{} identifier).
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    86
\end{ttdescription}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    87
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
\subsection{Applying a tactic}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    90
\index{tactics!commands for applying}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
by   : tactic -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
byev : tactic list -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
These commands extend the state list.  They apply a tactic to the current
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
proof state.  If the tactic succeeds, it returns a non-empty sequence of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
next states.  The head of the sequence becomes the next state, while the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
tail is retained for backtracking (see~{\tt back}).
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    99
\begin{ttdescription} \item[\ttindexbold{by} {\it tactic};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
applies the {\it tactic\/} to the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   102
\item[\ttindexbold{byev} {\it tactics};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
applies the list of {\it tactics}, one at a time.  It is useful for testing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
calls to {\tt prove_goal}, and abbreviates \hbox{\tt by (EVERY {\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
tactics})}.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   106
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   108
\noindent{\it Error indications:}\nobreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
\begin{itemize}
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   110
\item {\footnotesize\tt "by:\ tactic failed"} means that the tactic
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   111
  returned an empty sequence when applied to the current proof state.
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   112
\item {\footnotesize\tt "Warning:\ same as previous level"} means that the
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   113
  new proof state is identical to the previous state.
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   114
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   115
  means that some rule was applied whose theory is outside the theory of
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   116
  the initial proof state.  This could signify a mistake such as expressing
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   117
  the goal in intuitionistic logic and proving it using classical logic.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   120
\subsection{Extracting and storing the proved theorem}
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   121
\label{ExtractingAndStoringTheProvedTheorem}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   122
\index{theorems!from subgoal module}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
\begin{ttbox} 
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   124
result    : unit -> thm
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   125
uresult   : unit -> thm
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   126
bind_thm  : string * thm -> unit
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   127
qed       : string -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
\end{ttbox}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   129
\begin{ttdescription}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   130
\item[\ttindexbold{result}()]\index{assumptions!of main goal}
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   131
  returns the final theorem, after converting the free variables to
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   132
  schematics.  It discharges the assumptions supplied to the matching 
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   133
  {\tt goal} command.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   135
  It raises an exception unless the proof state passes certain checks.  There
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   136
  must be no assumptions other than those supplied to {\tt goal}.  There
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   137
  must be no subgoals.  The theorem proved must be a (first-order) instance
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   138
  of the original goal, as stated in the {\tt goal} command.  This allows
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   139
  {\bf answer extraction} --- instantiation of variables --- but no other
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   140
  changes to the main goal.  The theorem proved must have the same signature
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   141
  as the initial proof state.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   143
  These checks are needed because an Isabelle tactic can return any proof
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   144
  state at all.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   145
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   146
\item[\ttindexbold{uresult}()] is like {\tt result()} but omits the checks.
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   147
  It is needed when the initial goal contains function unknowns, when
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   148
  definitions are unfolded in the main goal (by calling
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   149
  \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   150
  \ttindex{assume_ax} has been used.
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   151
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   152
\item[\ttindexbold{bind_thm}($name$, $thm$)]\index{theorems!storing of}
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   153
  stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules})
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   154
  in Isabelle's theorem database and in the ML variable $name$. The
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   155
  theorem can be retrieved from Isabelle's database by {\tt get_thm}
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   156
  (see \S\ref{BasicOperationsOnTheories}).
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   157
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   158
\item[\ttindexbold{qed} $name$]
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   159
  combines {\tt result} and {\tt bind_thm} in that it first uses {\tt
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   160
  result()} to get the theorem and then stores it like {\tt bind_thm}.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   161
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
\subsection{Undoing and backtracking}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
chop    : unit -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
choplev : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
back    : unit -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
undo    : unit -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
\end{ttbox}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   171
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
\item[\ttindexbold{chop}();] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
deletes the top level of the state list, cancelling the last \ttindex{by}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
command.  It provides a limited undo facility, and the {\tt undo} command
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
can cancel it.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
\item[\ttindexbold{choplev} {\it n};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
truncates the state list to level~{\it n}. 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
\item[\ttindexbold{back}();]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
searches the state list for a non-empty branch point, starting from the top
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
level.  The first one found becomes the current proof state --- the most
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   183
recent alternative branch is taken.  This is a form of interactive
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   184
backtracking.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
\item[\ttindexbold{undo}();] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
cancels the most recent change to the proof state by the commands \ttindex{by},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
{\tt chop}, {\tt choplev}, and~{\tt back}.  It {\bf cannot}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
cancel {\tt goal} or {\tt undo} itself.  It can be repeated to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
cancel a series of commands.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   191
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   192
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   193
\goodbreak
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   194
\noindent{\it Error indications for {\tt back}:}\par\nobreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
\begin{itemize}
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   196
\item{\footnotesize\tt"Warning:\ same as previous choice at this level"}
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   197
  means {\tt back} found a non-empty branch point, but that it contained
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   198
  the same proof state as the current one.
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   199
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   200
  means the signature of the alternative proof state differs from that of
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   201
  the current state.
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   202
\item {\footnotesize\tt "back:\ no alternatives"} means {\tt back} could
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   203
  find no alternative proof state.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
507
a00301e9e64b addition of show_brackets
lcp
parents: 332
diff changeset
   206
\subsection{Printing the proof state}\label{sec:goals-printing}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   207
\index{proof state!printing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
pr    : unit -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
prlev : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
goals_limit: int ref \hfill{\bf initially 10}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
\end{ttbox}
507
a00301e9e64b addition of show_brackets
lcp
parents: 332
diff changeset
   213
See also the printing control options described in
a00301e9e64b addition of show_brackets
lcp
parents: 332
diff changeset
   214
\S\ref{sec:printing-control}. 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   215
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
\item[\ttindexbold{pr}();] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
prints the current proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
\item[\ttindexbold{prlev} {\it n};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
prints the proof state at level {\it n}.  This allows you to review the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
previous steps of the proof.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   223
\item[\ttindexbold{goals_limit} := {\it k};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
specifies~$k$ as the maximum number of subgoals to print.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   225
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
\subsection{Timing}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   229
\index{timing statistics}\index{proofs!timing}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
proof_timing: bool ref \hfill{\bf initially false}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   234
\begin{ttdescription}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   235
\item[\ttindexbold{proof_timing} := true;] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
makes the \ttindex{by} and \ttindex{prove_goal} commands display how much
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
processor time was spent.  This information is compiler-dependent.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   238
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
\section{Shortcuts for applying tactics}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   242
\index{shortcuts!for {\tt by} commands}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
These commands call \ttindex{by} with common tactics.  Their chief purpose
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
is to minimise typing, although the scanning shortcuts are useful in their
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
own right.  Chapter~\ref{tactics} explains the tactics themselves.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
\subsection{Refining a given subgoal}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
\begin{ttbox} 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   249
ba  :             int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   250
br  : thm      -> int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   251
be  : thm      -> int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   252
bd  : thm      -> int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   253
brs : thm list -> int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   254
bes : thm list -> int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   255
bds : thm list -> int -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   258
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
\item[\ttindexbold{ba} {\it i};] 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   260
performs \hbox{\tt by (assume_tac {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
\item[\ttindexbold{br} {\it thm} {\it i};] 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   263
performs \hbox{\tt by (resolve_tac [{\it thm}] {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
\item[\ttindexbold{be} {\it thm} {\it i};] 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   266
performs \hbox{\tt by (eresolve_tac [{\it thm}] {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
\item[\ttindexbold{bd} {\it thm} {\it i};] 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   269
performs \hbox{\tt by (dresolve_tac [{\it thm}] {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
\item[\ttindexbold{brs} {\it thms} {\it i};] 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   272
performs \hbox{\tt by (resolve_tac {\it thms} {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
\item[\ttindexbold{bes} {\it thms} {\it i};] 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   275
performs \hbox{\tt by (eresolve_tac {\it thms} {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
\item[\ttindexbold{bds} {\it thms} {\it i};] 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   278
performs \hbox{\tt by (dresolve_tac {\it thms} {\it i});}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   279
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
\subsection{Scanning shortcuts}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
These shortcuts scan for a suitable subgoal (starting from subgoal~1).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
They refine the first subgoal for which the tactic succeeds.  Thus, they
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
require less typing than {\tt br}, etc.  They display the selected
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
subgoal's number; please watch this, for it may not be what you expect!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
\begin{ttbox} 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   289
fa  : unit     -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   290
fr  : thm      -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   291
fe  : thm      -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   292
fd  : thm      -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   293
frs : thm list -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   294
fes : thm list -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   295
fds : thm list -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   298
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
\item[\ttindexbold{fa}();] 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   300
solves some subgoal by assumption.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
\item[\ttindexbold{fr} {\it thm};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
refines some subgoal using \hbox{\tt resolve_tac [{\it thm}]}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
\item[\ttindexbold{fe} {\it thm};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
refines some subgoal using \hbox{\tt eresolve_tac [{\it thm}]}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
\item[\ttindexbold{fd} {\it thm};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
refines some subgoal using \hbox{\tt dresolve_tac [{\it thm}]}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
\item[\ttindexbold{frs} {\it thms};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
refines some subgoal using \hbox{\tt resolve_tac {\it thms}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
\item[\ttindexbold{fes} {\it thms};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
refines some subgoal using \hbox{\tt eresolve_tac {\it thms}} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
\item[\ttindexbold{fds} {\it thms};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
refines some subgoal using \hbox{\tt dresolve_tac {\it thms}} 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   319
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
\subsection{Other shortcuts}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
bw  : thm -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
bws : thm list -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
ren : string -> int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
\end{ttbox}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   327
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
\item[\ttindexbold{bw} {\it def};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
performs \hbox{\tt by (rewrite_goals_tac [{\it def}]);}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
It unfolds definitions in the subgoals (but not the main goal), by
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   331
meta-rewriting with the given definition.
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   332
\index{meta-rewriting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
\item[\ttindexbold{bws}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
is like {\tt bw} but takes a list of definitions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
\item[\ttindexbold{ren} {\it names} {\it i};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
performs \hbox{\tt by (rename_tac {\it names} {\it i});} it renames
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   339
parameters in subgoal~$i$.  (Ignore the message {\footnotesize\tt Warning:\
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   340
  same as previous level}.)
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   341
\index{parameters!renaming}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   342
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   345
\section{Executing batch proofs}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   346
\index{batch execution}
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   347
\begin{ttbox}
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   348
prove_goal :         theory->          string->(thm list->tactic list)->thm
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   349
qed_goal   : string->theory->          string->(thm list->tactic list)->unit
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   350
prove_goalw:         theory->thm list->string->(thm list->tactic list)->thm
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   351
qed_goalw  : string->theory->thm list->string->(thm list->tactic list)->unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
\end{ttbox}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   354
These batch functions create an initial proof state, then apply a tactic to
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   355
it, yielding a sequence of final proof states.  The head of the sequence is
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
returned, provided it is an instance of the theorem originally proposed.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
The forms {\tt prove_goal}, {\tt prove_goalw} and {\tt prove_goalw_cterm}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   358
are analogous to {\tt goal}, {\tt goalw} and {\tt goalw_cterm}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
The tactic is specified by a function from theorem lists to tactic lists.
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   361
The function is applied to the list of meta-assumptions taken from
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   362
the main goal.  The resulting tactics are applied in sequence (using {\tt
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   363
  EVERY}).  For example, a proof consisting of the commands
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
val prems = goal {\it theory} {\it formula};
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
by \(tac@1\);  \ldots  by \(tac@n\);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
val my_thm = result();
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
can be transformed to an expression as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
val my_thm = prove_goal {\it theory} {\it formula}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
 (fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
The methods perform identical processing of the initial {\it formula} and
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   375
the final proof state.  But {\tt prove_goal} executes the tactic as a
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   376
atomic operation, bypassing the subgoal module; the current interactive
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   377
proof is unaffected.
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   378
%
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   379
\begin{ttdescription}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   380
\item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
executes a proof of the {\it formula\/} in the given {\it theory}, using
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
the given tactic function.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   384
\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;]
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   385
acts like {\tt prove_goal} but also stores the resulting theorem in
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   386
Isabelle's theorem database and in the ML variable $name$ (see
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   387
\S\ref{ExtractingAndStoringTheProvedTheorem}).
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   388
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
\item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   390
      {\it tacsf};]\index{meta-rewriting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
is like {\tt prove_goal} but also applies the list of {\it defs\/} as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
meta-rewrite rules to the first subgoal and the premises.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   394
\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;]
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   395
is analogous to {\tt qed_goal}.
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   396
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
\item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   398
      {\it tacsf};] 
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   399
is a version of {\tt prove_goalw} for programming applications.  The main
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
goal is supplied as a cterm, not as a string.  Typically, the cterm is
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   401
created from a term~$t$ as follows:
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   402
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   403
Sign.cterm_of (sign_of thy) \(t\)
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   404
\end{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
\index{*Sign.cterm_of}\index{*sign_of}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   406
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   409
\section{Managing multiple proofs}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   410
\index{proofs!managing multiple}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
You may save the current state of the subgoal module and resume work on it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
later.  This serves two purposes.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
\begin{enumerate}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
\item At some point, you may be uncertain of the next step, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
wish to experiment.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
\item During a proof, you may see that a lemma should be proved first.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
\end{enumerate}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
Each saved proof state consists of a list of levels; \ttindex{chop} behaves
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
independently for each of the saved proofs.  In addition, each saved state
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
carries a separate \ttindex{undo} list.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   423
\subsection{The stack of proof states}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   424
\index{proofs!stacking}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
push_proof   : unit -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
pop_proof    : unit -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
rotate_proof : unit -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
The subgoal module maintains a stack of proof states.  Most subgoal
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   431
commands affect only the top of the stack.  The \ttindex{goal} command {\em
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   432
replaces\/} the top of the stack; the only command that pushes a proof on the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
stack is {\tt push_proof}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
To save some point of the proof, call {\tt push_proof}.  You may now
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   436
state a lemma using {\tt goal}, or simply continue to apply tactics.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
Later, you can return to the saved point by calling {\tt pop_proof} or 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
{\tt rotate_proof}. 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
To view the entire stack, call {\tt rotate_proof} repeatedly; as it rotates
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
the stack, it prints the new top element.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   443
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
\item[\ttindexbold{push_proof}();]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
duplicates the top element of the stack, pushing a copy of the current
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
proof state on to the stack.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   447
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
\item[\ttindexbold{pop_proof}();]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
discards the top element of the stack.  It returns the list of
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   450
assumptions associated with the new proof;  you should bind these to an
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
\ML\ identifier.  They can also be obtained by calling \ttindex{premises}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   453
\item[\ttindexbold{rotate_proof}();]
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   454
\index{assumptions!of main goal}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
rotates the stack, moving the top element to the bottom.  It returns the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
list of assumptions associated with the new proof.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   457
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   460
\subsection{Saving and restoring proof states}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   461
\index{proofs!saving and restoring}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
save_proof    : unit -> proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
restore_proof : proof -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   466
States of the subgoal module may be saved as \ML\ values of
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   467
type~\mltydx{proof}, and later restored.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   469
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
\item[\ttindexbold{save_proof}();]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
returns the current state, which is on top of the stack.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   473
\item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   474
  replaces the top of the stack by~{\it prf}.  It returns the list of
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   475
  assumptions associated with the new proof.
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   476
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   479
\section{Debugging and inspecting}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   480
\index{tactics!debugging}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
These specialized operations support the debugging of tactics.  They refer
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   482
to the current proof state of the subgoal module.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   484
\subsection{Reading and printing terms}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   485
\index{terms!reading of}\index{terms!printing of}\index{types!printing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
read    : string -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
prin    : term -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
printyp : typ -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
These read and print terms (or types) using the syntax associated with the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   494
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
\item[\ttindexbold{read} {\it string}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
reads the {\it string} as a term, without type checking.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
\item[\ttindexbold{prin} {\it t};]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
prints the term~$t$ at the terminal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
\item[\ttindexbold{printyp} {\it T};]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
prints the type~$T$ at the terminal.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   503
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   505
\subsection{Inspecting the proof state}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   506
\index{proofs!inspecting the state}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
topthm  : unit -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
getgoal : int -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
gethyps : int -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   513
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
\item[\ttindexbold{topthm}()]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
returns the proof state as an Isabelle theorem.  This is what \ttindex{by}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
would supply to a tactic at this point.  It omits the post-processing of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
\ttindex{result} and \ttindex{uresult}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
\item[\ttindexbold{getgoal} {\it i}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
returns subgoal~$i$ of the proof state, as a term.  You may print
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   521
this using {\tt prin}, though you may have to examine the internal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
data structure in order to locate the problem!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   524
\item[\ttindexbold{gethyps} {\it i}]
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   525
  returns the hypotheses of subgoal~$i$ as meta-level assumptions.  In
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   526
  these theorems, the subgoal's parameters become free variables.  This
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   527
  command is supplied for debugging uses of \ttindex{METAHYPS}.
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   528
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   530
\subsection{Filtering lists of rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
filter_goal: (term*term->bool) -> thm list -> int -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   535
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
\item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
applies \hbox{\tt filter_thms {\it could}} to subgoal~$i$ of the proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   538
state and returns the list of theorems that survive the filtering. 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   539
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   540
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
\index{subgoal module|)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   542
\index{proofs|)}