doc-src/Ref/goals.tex
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 8995 61e1ca01d4a3
child 13479 7123ae179212
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
\chapter{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}
5391
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    27
Most proofs begin with \texttt{Goal} or \texttt{Goalw} and require no other
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
    28
commands than \texttt{by}, \texttt{chop} and \texttt{undo}.  They typically end
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
    29
with a call to \texttt{qed}.
104
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}
5391
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    32
\begin{ttbox}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    33
Goal        :                       string -> thm list
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    34
Goalw       :           thm list -> string -> thm list
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    35
goal        : theory ->             string -> thm list 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
goalw       : theory -> thm list -> string -> thm list 
8968
2e88a982f96b better indentation
paulson
parents: 8136
diff changeset
    37
goalw_cterm :           thm list -> cterm  -> thm list 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
premises    : unit -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
\end{ttbox}
5391
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    40
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    41
The goal commands start a new proof by setting the goal.  They replace
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    42
the current state list by a new one consisting of the initial proof
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    43
state.  They also empty the \ttindex{undo} list; this command cannot
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    44
be undone!
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
They all return a list of meta-hypotheses taken from the main goal.  If
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
this list is non-empty, bind its value to an \ML{} identifier by typing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
something like
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
\begin{ttbox} 
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
    50
val prems = goal{\it theory\/ formula};
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    51
\end{ttbox}\index{assumptions!of main goal}
5391
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    52
These assumptions typically serve as the premises when you are
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    53
deriving a rule.  They are also stored internally and can be retrieved
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    54
later by the function \texttt{premises}.  When the proof is finished,
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    55
\texttt{qed} compares the stored assumptions with the actual
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    56
assumptions in the proof state.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    57
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    58
The capital versions of \texttt{Goal} are the basic user level
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    59
commands and should be preferred over the more primitive lowercase
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    60
\texttt{goal} commands.  Apart from taking the current theory context
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    61
as implicit argument, the former ones try to be smart in handling
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    62
meta-hypotheses when deriving rules.  Thus \texttt{prems} have to be
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    63
seldom bound explicitly, the effect is as if \texttt{cut_facts_tac}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    64
had been called automatically.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    66
\index{definitions!unfolding}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
Some of the commands unfold definitions using meta-rewrite rules.  This
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
    68
expansion affects both the initial subgoal and the premises, which would
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
    69
otherwise require use of \texttt{rewrite_goals_tac} and
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
    70
\texttt{rewrite_rule}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    72
\begin{ttdescription}
5391
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    73
\item[\ttindexbold{Goal} {\it formula};] begins a new proof, where
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    74
  {\it formula\/} is written as an \ML\ string.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    75
  
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    76
\item[\ttindexbold{Goalw} {\it defs} {\it formula};] is like
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    77
  \texttt{Goal} but also applies the list of {\it defs\/} as
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    78
  meta-rewrite rules to the first subgoal and the premises.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    79
  \index{meta-rewriting}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
    80
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    81
\item[\ttindexbold{goal} {\it theory} {\it formula};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
begins a new proof, where {\it theory} is usually an \ML\ identifier
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
and the {\it formula\/} is written as an \ML\ string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    85
\item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
    86
is like \texttt{goal} but also applies the list of {\it defs\/} as
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
meta-rewrite rules to the first subgoal and the premises.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    88
\index{meta-rewriting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
8978
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
    90
\item[\ttindexbold{goalw_cterm} {\it defs} {\it ct};] is
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
    91
  a version of \texttt{goalw} intended for programming.  The main
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
    92
  goal is supplied as a cterm, not as a string.  See also
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
    93
  \texttt{prove_goalw_cterm}, \S\ref{sec:executing-batch}. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
\item[\ttindexbold{premises}()] 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    96
returns the list of meta-hypotheses associated with the current proof (in
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    97
case you forgot to bind them to an \ML{} identifier).
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    98
\end{ttdescription}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
    99
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
\subsection{Applying a tactic}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   102
\index{tactics!commands for applying}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
by   : tactic -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
byev : tactic list -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
These commands extend the state list.  They apply a tactic to the current
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
proof state.  If the tactic succeeds, it returns a non-empty sequence of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
next states.  The head of the sequence becomes the next state, while the
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   110
tail is retained for backtracking (see~\texttt{back}).
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   111
\begin{ttdescription} \item[\ttindexbold{by} {\it tactic};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
applies the {\it tactic\/} to the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   114
\item[\ttindexbold{byev} {\it tactics};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
applies the list of {\it tactics}, one at a time.  It is useful for testing
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   116
calls to \texttt{prove_goal}, and abbreviates \texttt{by (EVERY {\it
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
tactics})}.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   118
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   120
\noindent{\it Error indications:}\nobreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
\begin{itemize}
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   122
\item {\footnotesize\tt "by:\ tactic failed"} means that the tactic
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   123
  returned an empty sequence when applied to the current proof state.
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   124
\item {\footnotesize\tt "Warning:\ same as previous level"} means that the
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   125
  new proof state is identical to the previous state.
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   126
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   127
  means that some rule was applied whose theory is outside the theory of
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   128
  the initial proof state.  This could signify a mistake such as expressing
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   129
  the goal in intuitionistic logic and proving it using classical logic.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   132
\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
   133
\label{ExtractingAndStoringTheProvedTheorem}
1233
2856f382f033 minor corrections to indexing; added thms_containing
paulson
parents: 1225
diff changeset
   134
\index{theorems!extracting proved}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
\begin{ttbox} 
7421
0577bb18b1ab added bind_thms, store_thms;
wenzelm
parents: 6569
diff changeset
   136
qed        : string -> unit
7446
f43d3670a3cd added no_qed;
wenzelm
parents: 7421
diff changeset
   137
no_qed     : unit -> unit
7421
0577bb18b1ab added bind_thms, store_thms;
wenzelm
parents: 6569
diff changeset
   138
result     : unit -> thm
0577bb18b1ab added bind_thms, store_thms;
wenzelm
parents: 6569
diff changeset
   139
uresult    : unit -> thm
0577bb18b1ab added bind_thms, store_thms;
wenzelm
parents: 6569
diff changeset
   140
bind_thm   : string * thm -> unit
0577bb18b1ab added bind_thms, store_thms;
wenzelm
parents: 6569
diff changeset
   141
bind_thms  : string * thm list -> unit
0577bb18b1ab added bind_thms, store_thms;
wenzelm
parents: 6569
diff changeset
   142
store_thm  : string * thm -> thm
0577bb18b1ab added bind_thms, store_thms;
wenzelm
parents: 6569
diff changeset
   143
store_thms : string * thm list -> thm list
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
\end{ttbox}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   145
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   146
\item[\ttindexbold{qed} $name$;] is the usual way of ending a proof.
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   147
  It combines \texttt{result} and \texttt{bind_thm}: it gets the theorem
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   148
  using \texttt{result()} and stores it the theorem database associated
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   149
  with its theory.  See below for details.
7446
f43d3670a3cd added no_qed;
wenzelm
parents: 7421
diff changeset
   150
  
f43d3670a3cd added no_qed;
wenzelm
parents: 7421
diff changeset
   151
\item[\ttindexbold{no_qed}();] indicates that the proof is not concluded by a
f43d3670a3cd added no_qed;
wenzelm
parents: 7421
diff changeset
   152
  proper \texttt{qed} command.  This is a do-nothing operation, it merely
f43d3670a3cd added no_qed;
wenzelm
parents: 7421
diff changeset
   153
  helps user interfaces such as Proof~General \cite{proofgeneral} to figure
f43d3670a3cd added no_qed;
wenzelm
parents: 7421
diff changeset
   154
  out the structure of the {\ML} text.
1283
ea8b657a9c92 Documented store_thm and moved qed to top
paulson
parents: 1233
diff changeset
   155
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   156
\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
   157
  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
   158
  schematics.  It discharges the assumptions supplied to the matching 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   159
  \texttt{goal} command.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   161
  It raises an exception unless the proof state passes certain checks.  There
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   162
  must be no assumptions other than those supplied to \texttt{goal}.  There
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   163
  must be no subgoals.  The theorem proved must be a (first-order) instance
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   164
  of the original goal, as stated in the \texttt{goal} command.  This allows
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   165
  {\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
   166
  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
   167
  as the initial proof state.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   169
  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
   170
  state at all.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   171
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   172
\item[\ttindexbold{uresult}()] is like \texttt{result()} but omits the checks.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   173
  It is needed when the initial goal contains function unknowns, when
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   174
  definitions are unfolded in the main goal (by calling
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   175
  \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   176
  \ttindex{assume_ax} has been used.
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   177
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   178
\item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing}
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   179
  stores \texttt{standard $thm$} (see \S\ref{MiscellaneousForwardRules})
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   180
  in the theorem database associated with its theory and in the {\ML}
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   181
  variable $name$.  The theorem can be retrieved from the database
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   182
  using \texttt{get_thm} (see \S\ref{BasicOperationsOnTheories}).
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   183
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   184
\item[\ttindexbold{store_thm} ($name$, $thm$)]\index{theorems!storing}
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   185
  stores $thm$ in the theorem database associated with its theory and
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   186
  returns that theorem.
7421
0577bb18b1ab added bind_thms, store_thms;
wenzelm
parents: 6569
diff changeset
   187
  
7990
0a604b2fc2b1 updated;
wenzelm
parents: 7805
diff changeset
   188
\item[\ttindexbold{bind_thms} \textrm{and} \ttindexbold{store_thms}] are similar to
7421
0577bb18b1ab added bind_thms, store_thms;
wenzelm
parents: 6569
diff changeset
   189
  \texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems.
0577bb18b1ab added bind_thms, store_thms;
wenzelm
parents: 6569
diff changeset
   190
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   191
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
7990
0a604b2fc2b1 updated;
wenzelm
parents: 7805
diff changeset
   193
The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be the empty
0a604b2fc2b1 updated;
wenzelm
parents: 7805
diff changeset
   194
string as well; in that case the result is \emph{not} stored, but proper
0a604b2fc2b1 updated;
wenzelm
parents: 7805
diff changeset
   195
checks and presentation of the result still apply.
7591
2d89d12f31eb qed "";
wenzelm
parents: 7446
diff changeset
   196
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
5391
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   198
\subsection{Extracting axioms and stored theorems}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   199
\index{theories!axioms of}\index{axioms!extracting}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   200
\index{theories!theorems of}\index{theorems!extracting}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   201
\begin{ttbox}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   202
thm       : xstring -> thm
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   203
thms      : xstring -> thm list
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   204
get_axiom : theory -> xstring -> thm
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   205
get_thm   : theory -> xstring -> thm
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   206
get_thms  : theory -> xstring -> thm list
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   207
axioms_of : theory -> (string * thm) list
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   208
thms_of   : theory -> (string * thm) list
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   209
assume_ax : theory -> string -> thm
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   210
\end{ttbox}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   211
\begin{ttdescription}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   212
  
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   213
\item[\ttindexbold{thm} $name$] is the basic user function for
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   214
  extracting stored theorems from the current theory context.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   215
  
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   216
\item[\ttindexbold{thms} $name$] is like \texttt{thm}, but returns a
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   217
  whole list associated with $name$ rather than a single theorem.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   218
  Typically this will be collections stored by packages, e.g.\ 
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   219
  \verb|list.simps|.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   220
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   221
\item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   222
  given $name$ from $thy$ or any of its ancestors, raising exception
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   223
  \xdx{THEORY} if none exists.  Merging theories can cause several
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   224
  axioms to have the same name; {\tt get_axiom} returns an arbitrary
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   225
  one.  Usually, axioms are also stored as theorems and may be
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   226
  retrieved via \texttt{get_thm} as well.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   227
  
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   228
\item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   229
    get_axiom}, but looks for a theorem stored in the theory's
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   230
  database.  Like {\tt get_axiom} it searches all parents of a theory
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   231
  if the theorem is not found directly in $thy$.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   232
  
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   233
\item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   234
  for retrieving theorem lists stored within the theory.  It returns a
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   235
  singleton list if $name$ actually refers to a theorem rather than a
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   236
  theorem list.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   237
  
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   238
\item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   239
  node, not including the ones of its ancestors.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   240
  
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   241
\item[\ttindexbold{thms_of} $thy$] returns all theorems stored within
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   242
  the database of this theory node, not including the ones of its
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   243
  ancestors.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   244
  
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   245
\item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   246
  using the syntax of $thy$, following the same conventions as axioms
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   247
  in a theory definition.  You can thus pretend that {\it formula} is
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   248
  an axiom and use the resulting theorem like an axiom.  Actually {\tt
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   249
    assume_ax} returns an assumption; \ttindex{qed} and
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   250
  \ttindex{result} complain about additional assumptions, but
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   251
  \ttindex{uresult} does not.
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   252
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   253
For example, if {\it formula} is
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   254
\hbox{\tt a=b ==> b=a} then the resulting theorem has the form
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   255
\hbox{\verb'?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]'}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   256
\end{ttdescription}
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   257
8b22b93dba2c Goal, Goalw;
wenzelm
parents: 5371
diff changeset
   258
1222
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   259
\subsection{Retrieving theorems}
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   260
\index{theorems!retrieving}
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   261
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   262
The following functions retrieve theorems (together with their names)
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   263
from the theorem database that is associated with the current proof
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   264
state's theory.  They can only find theorems that have explicitly been
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   265
stored in the database using \ttindex{qed}, \ttindex{bind_thm} or
1222
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   266
related functions.
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   267
\begin{ttbox} 
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   268
findI           :          int -> (string * thm) list
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   269
findE           :   int -> int -> (string * thm) list
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   270
findEs          :          int -> (string * thm) list
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   271
thms_containing : xstring list -> (string * thm) list
1222
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   272
\end{ttbox}
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   273
\begin{ttdescription}
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   274
\item[\ttindexbold{findI} $i$]\index{assumptions!of main goal}
1225
35703accdf31 minor polishing of text on findI, etc.
paulson
parents: 1222
diff changeset
   275
  returns all ``introduction rules'' applicable to subgoal $i$ --- all
1222
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   276
  theorems whose conclusion matches (rather than unifies with) subgoal
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   277
  $i$.  Useful in connection with \texttt{resolve_tac}.
1222
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   278
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   279
\item[\ttindexbold{findE} $n$ $i$] returns all ``elimination rules''
1225
35703accdf31 minor polishing of text on findI, etc.
paulson
parents: 1222
diff changeset
   280
  applicable to premise $n$ of subgoal $i$ --- all those theorems whose
35703accdf31 minor polishing of text on findI, etc.
paulson
parents: 1222
diff changeset
   281
  first premise matches premise $n$ of subgoal $i$.  Useful in connection with
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   282
  \texttt{eresolve_tac} and \texttt{dresolve_tac}.
1222
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   283
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   284
\item[\ttindexbold{findEs} $i$] returns all ``elimination rules'' applicable
1225
35703accdf31 minor polishing of text on findI, etc.
paulson
parents: 1222
diff changeset
   285
  to subgoal $i$ --- all those theorems whose first premise matches some
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   286
  premise of subgoal $i$.  Useful in connection with \texttt{eresolve_tac} and
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   287
  \texttt{dresolve_tac}.
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   288
  
7805
0ae9ddc36fe0 theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents: 7591
diff changeset
   289
\item[\ttindexbold{thms_containing} $consts$] returns all theorems that
0ae9ddc36fe0 theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents: 7591
diff changeset
   290
  contain \emph{all} of the given constants.
1222
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   291
\end{ttdescription}
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   292
d99d13a0213f Documented findI, findE, findEs, thms_containing.
nipkow
parents: 866
diff changeset
   293
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
\subsection{Undoing and backtracking}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
chop    : unit -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
choplev : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
back    : unit -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
undo    : unit -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
\end{ttbox}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   301
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
\item[\ttindexbold{chop}();] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
deletes the top level of the state list, cancelling the last \ttindex{by}
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   304
command.  It provides a limited undo facility, and the \texttt{undo} command
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
can cancel it.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
\item[\ttindexbold{choplev} {\it n};] 
2128
4e8644805af2 Documents the use of negative arguments to choplev and prlev
paulson
parents: 1283
diff changeset
   308
truncates the state list to level~{\it n}, if $n\geq0$.  A negative value
4e8644805af2 Documents the use of negative arguments to choplev and prlev
paulson
parents: 1283
diff changeset
   309
of~$n$ refers to the $n$th previous level: 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   310
\hbox{\verb|choplev ~1|} has the same effect as \texttt{chop}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
\item[\ttindexbold{back}();]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
searches the state list for a non-empty branch point, starting from the top
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
level.  The first one found becomes the current proof state --- the most
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   315
recent alternative branch is taken.  This is a form of interactive
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   316
backtracking.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
\item[\ttindexbold{undo}();] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
cancels the most recent change to the proof state by the commands \ttindex{by},
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   320
\texttt{chop}, \texttt{choplev}, and~\texttt{back}.  It {\bf cannot}
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   321
cancel \texttt{goal} or \texttt{undo} itself.  It can be repeated to
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
cancel a series of commands.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   323
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   324
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   325
\goodbreak
6569
wenzelm
parents: 6170
diff changeset
   326
\noindent{\it Error indications for {\tt back}:}\par\nobreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
\begin{itemize}
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   328
\item{\footnotesize\tt"Warning:\ same as previous choice at this level"}
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   329
  means \texttt{back} found a non-empty branch point, but that it contained
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   330
  the same proof state as the current one.
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   331
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   332
  means the signature of the alternative proof state differs from that of
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   333
  the current state.
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   334
\item {\footnotesize\tt "back:\ no alternatives"} means \texttt{back} could
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   335
  find no alternative proof state.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
507
a00301e9e64b addition of show_brackets
lcp
parents: 332
diff changeset
   338
\subsection{Printing the proof state}\label{sec:goals-printing}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   339
\index{proof state!printing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
pr    : unit -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
prlev : int -> unit
2528
bc6e29c776d6 Documents the new command "prlim"
paulson
parents: 2128
diff changeset
   343
prlim : int -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
goals_limit: int ref \hfill{\bf initially 10}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
\end{ttbox}
2528
bc6e29c776d6 Documents the new command "prlim"
paulson
parents: 2128
diff changeset
   346
See also the printing control options described 
bc6e29c776d6 Documents the new command "prlim"
paulson
parents: 2128
diff changeset
   347
in~\S\ref{sec:printing-control}. 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   348
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
\item[\ttindexbold{pr}();] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
prints the current proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
\item[\ttindexbold{prlev} {\it n};] 
2128
4e8644805af2 Documents the use of negative arguments to choplev and prlev
paulson
parents: 1283
diff changeset
   353
prints the proof state at level {\it n}, if $n\geq0$.  A negative value
4e8644805af2 Documents the use of negative arguments to choplev and prlev
paulson
parents: 1283
diff changeset
   354
of~$n$ refers to the $n$th previous level.  This command allows
4e8644805af2 Documents the use of negative arguments to choplev and prlev
paulson
parents: 1283
diff changeset
   355
you to review earlier stages of the proof.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
2528
bc6e29c776d6 Documents the new command "prlim"
paulson
parents: 2128
diff changeset
   357
\item[\ttindexbold{prlim} {\it k};] 
bc6e29c776d6 Documents the new command "prlim"
paulson
parents: 2128
diff changeset
   358
prints the current proof state, limiting the number of subgoals to~$k$.  It
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   359
updates \texttt{goals_limit} (see below) and is helpful when there are many
2528
bc6e29c776d6 Documents the new command "prlim"
paulson
parents: 2128
diff changeset
   360
subgoals. 
bc6e29c776d6 Documents the new command "prlim"
paulson
parents: 2128
diff changeset
   361
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   362
\item[\ttindexbold{goals_limit} := {\it k};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
specifies~$k$ as the maximum number of subgoals to print.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   364
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
\subsection{Timing}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   368
\index{timing statistics}\index{proofs!timing}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
\begin{ttbox} 
8995
61e1ca01d4a3 proof_timing replaced by global timing;
wenzelm
parents: 8978
diff changeset
   370
timing: bool ref \hfill{\bf initially false}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   373
\begin{ttdescription}
8995
61e1ca01d4a3 proof_timing replaced by global timing;
wenzelm
parents: 8978
diff changeset
   374
\item[set \ttindexbold{timing};] enables global timing in Isabelle.  In
61e1ca01d4a3 proof_timing replaced by global timing;
wenzelm
parents: 8978
diff changeset
   375
  particular, this makes the \ttindex{by} and \ttindex{prove_goal} commands
61e1ca01d4a3 proof_timing replaced by global timing;
wenzelm
parents: 8978
diff changeset
   376
  display how much processor time was spent.  This information is
61e1ca01d4a3 proof_timing replaced by global timing;
wenzelm
parents: 8978
diff changeset
   377
  compiler-dependent.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   378
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
\section{Shortcuts for applying tactics}
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   382
\index{shortcuts!for \texttt{by} commands}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
These commands call \ttindex{by} with common tactics.  Their chief purpose
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
is to minimise typing, although the scanning shortcuts are useful in their
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
own right.  Chapter~\ref{tactics} explains the tactics themselves.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
\subsection{Refining a given subgoal}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
\begin{ttbox} 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   389
ba  :             int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   390
br  : thm      -> int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   391
be  : thm      -> int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   392
bd  : thm      -> int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   393
brs : thm list -> int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   394
bes : thm list -> int -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   395
bds : thm list -> int -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   398
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
\item[\ttindexbold{ba} {\it i};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   400
performs \texttt{by (assume_tac {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
\item[\ttindexbold{br} {\it thm} {\it i};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   403
performs \texttt{by (resolve_tac [{\it thm}] {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
\item[\ttindexbold{be} {\it thm} {\it i};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   406
performs \texttt{by (eresolve_tac [{\it thm}] {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
\item[\ttindexbold{bd} {\it thm} {\it i};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   409
performs \texttt{by (dresolve_tac [{\it thm}] {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
\item[\ttindexbold{brs} {\it thms} {\it i};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   412
performs \texttt{by (resolve_tac {\it thms} {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
\item[\ttindexbold{bes} {\it thms} {\it i};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   415
performs \texttt{by (eresolve_tac {\it thms} {\it i});}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
\item[\ttindexbold{bds} {\it thms} {\it i};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   418
performs \texttt{by (dresolve_tac {\it thms} {\it i});}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   419
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
\subsection{Scanning shortcuts}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
These shortcuts scan for a suitable subgoal (starting from subgoal~1).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
They refine the first subgoal for which the tactic succeeds.  Thus, they
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   425
require less typing than \texttt{br}, etc.  They display the selected
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
subgoal's number; please watch this, for it may not be what you expect!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
\begin{ttbox} 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   429
fa  : unit     -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   430
fr  : thm      -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   431
fe  : thm      -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   432
fd  : thm      -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   433
frs : thm list -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   434
fes : thm list -> unit
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   435
fds : thm list -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   438
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
\item[\ttindexbold{fa}();] 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   440
solves some subgoal by assumption.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
\item[\ttindexbold{fr} {\it thm};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   443
refines some subgoal using \texttt{resolve_tac [{\it thm}]}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
\item[\ttindexbold{fe} {\it thm};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   446
refines some subgoal using \texttt{eresolve_tac [{\it thm}]}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   447
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
\item[\ttindexbold{fd} {\it thm};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   449
refines some subgoal using \texttt{dresolve_tac [{\it thm}]}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
\item[\ttindexbold{frs} {\it thms};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   452
refines some subgoal using \texttt{resolve_tac {\it thms}}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
\item[\ttindexbold{fes} {\it thms};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   455
refines some subgoal using \texttt{eresolve_tac {\it thms}} 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
\item[\ttindexbold{fds} {\it thms};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   458
refines some subgoal using \texttt{dresolve_tac {\it thms}} 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   459
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
\subsection{Other shortcuts}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
bw  : thm -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
bws : thm list -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
ren : string -> int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   466
\end{ttbox}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   467
\begin{ttdescription}
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   468
\item[\ttindexbold{bw} {\it def};] performs \texttt{by
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   469
    (rewrite_goals_tac [{\it def}]);} It unfolds definitions in the
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   470
  subgoals (but not the main goal), by meta-rewriting with the given
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   471
  definition (see also \S\ref{sec:rewrite_goals}).
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   472
  \index{meta-rewriting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
\item[\ttindexbold{bws}] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   475
is like \texttt{bw} but takes a list of definitions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
\item[\ttindexbold{ren} {\it names} {\it i};] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   478
performs \texttt{by (rename_tac {\it names} {\it i});} it renames
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   479
parameters in subgoal~$i$.  (Ignore the message {\footnotesize\tt Warning:\
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   480
  same as previous level}.)
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   481
\index{parameters!renaming}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   482
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
8978
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
   485
\section{Executing batch proofs}\label{sec:executing-batch}
3128
d01d4c0c4b44 New acknowledgements; fixed overfull lines and tables
paulson
parents: 3108
diff changeset
   486
\index{batch execution}%
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7990
diff changeset
   487
To save space below, let type \texttt{tacfn} abbreviate \texttt{thm list ->
3128
d01d4c0c4b44 New acknowledgements; fixed overfull lines and tables
paulson
parents: 3108
diff changeset
   488
  tactic list}, which is the type of a tactical proof.
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   489
\begin{ttbox}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7990
diff changeset
   490
prove_goal :           theory ->             string -> tacfn -> thm
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7990
diff changeset
   491
qed_goal   : string -> theory ->             string -> tacfn -> unit
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7990
diff changeset
   492
prove_goalw:           theory -> thm list -> string -> tacfn -> thm
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7990
diff changeset
   493
qed_goalw  : string -> theory -> thm list -> string -> tacfn -> unit
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7990
diff changeset
   494
prove_goalw_cterm:               thm list -> cterm  -> tacfn -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
\end{ttbox}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   496
These batch functions create an initial proof state, then apply a tactic to
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   497
it, yielding a sequence of final proof states.  The head of the sequence is
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
returned, provided it is an instance of the theorem originally proposed.
8978
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
   499
The forms \texttt{prove_goal}, \texttt{prove_goalw} and
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
   500
\texttt{prove_goalw_cterm} are analogous to \texttt{goal}, \texttt{goalw} and
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
   501
\texttt{goalw_cterm}.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
The tactic is specified by a function from theorem lists to tactic lists.
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   504
The function is applied to the list of meta-assumptions taken from
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   505
the main goal.  The resulting tactics are applied in sequence (using {\tt
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   506
  EVERY}).  For example, a proof consisting of the commands
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
val prems = goal {\it theory} {\it formula};
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
by \(tac@1\);  \ldots  by \(tac@n\);
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2611
diff changeset
   510
qed "my_thm";
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
can be transformed to an expression as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2611
diff changeset
   514
qed_goal "my_thm" {\it theory} {\it formula}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
 (fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
The methods perform identical processing of the initial {\it formula} and
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   518
the final proof state.  But \texttt{prove_goal} executes the tactic as a
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   519
atomic operation, bypassing the subgoal module; the current interactive
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   520
proof is unaffected.
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   521
%
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   522
\begin{ttdescription}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   523
\item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
executes a proof of the {\it formula\/} in the given {\it theory}, using
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
the given tactic function.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   527
\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7990
diff changeset
   528
  like \texttt{prove_goal} but it also stores the resulting theorem in the
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   529
  theorem database associated with its theory and in the {\ML}
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   530
  variable $name$ (see \S\ref{ExtractingAndStoringTheProvedTheorem}).
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   531
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
\item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   533
      {\it tacsf};]\index{meta-rewriting}
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   534
is like \texttt{prove_goal} but also applies the list of {\it defs\/} as
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
meta-rewrite rules to the first subgoal and the premises.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   537
\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;]
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   538
is analogous to \texttt{qed_goal}.
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 507
diff changeset
   539
8978
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
   540
\item[\ttindexbold{prove_goalw_cterm} {\it defs} {\it ct}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   541
      {\it tacsf};] 
8978
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
   542
is a version of \texttt{prove_goalw} intended for programming.  The main
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
   543
goal is supplied as a cterm, not as a string.  A cterm carries a theory with
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
   544
      it, and can be created from a term~$t$ by
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   545
\begin{ttbox}
8978
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
   546
cterm_of (sign_of thy) \(t\)        
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   547
\end{ttbox}
8978
894d76cbf56d fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents: 8968
diff changeset
   548
  \index{*cterm_of}\index{*sign_of}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   549
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   552
\section{Managing multiple proofs}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   553
\index{proofs!managing multiple}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   554
You may save the current state of the subgoal module and resume work on it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   555
later.  This serves two purposes.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   556
\begin{enumerate}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   557
\item At some point, you may be uncertain of the next step, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
wish to experiment.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   560
\item During a proof, you may see that a lemma should be proved first.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   561
\end{enumerate}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   562
Each saved proof state consists of a list of levels; \ttindex{chop} behaves
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
independently for each of the saved proofs.  In addition, each saved state
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   564
carries a separate \ttindex{undo} list.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   565
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   566
\subsection{The stack of proof states}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   567
\index{proofs!stacking}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   568
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
push_proof   : unit -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
pop_proof    : unit -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
rotate_proof : unit -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   572
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   573
The subgoal module maintains a stack of proof states.  Most subgoal
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   574
commands affect only the top of the stack.  The \ttindex{Goal} command {\em
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   575
replaces\/} the top of the stack; the only command that pushes a proof on the
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   576
stack is \texttt{push_proof}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   577
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   578
To save some point of the proof, call \texttt{push_proof}.  You may now
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   579
state a lemma using \texttt{goal}, or simply continue to apply tactics.
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   580
Later, you can return to the saved point by calling \texttt{pop_proof} or 
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   581
\texttt{rotate_proof}. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   583
To view the entire stack, call \texttt{rotate_proof} repeatedly; as it rotates
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   584
the stack, it prints the new top element.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   585
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   586
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   587
\item[\ttindexbold{push_proof}();]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   588
duplicates the top element of the stack, pushing a copy of the current
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   589
proof state on to the stack.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   590
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   591
\item[\ttindexbold{pop_proof}();]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   592
discards the top element of the stack.  It returns the list of
332
01b87a921967 final Springer copy
lcp
parents: 321
diff changeset
   593
assumptions associated with the new proof;  you should bind these to an
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
\ML\ identifier.  They can also be obtained by calling \ttindex{premises}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   595
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   596
\item[\ttindexbold{rotate_proof}();]
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   597
\index{assumptions!of main goal}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   598
rotates the stack, moving the top element to the bottom.  It returns the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   599
list of assumptions associated with the new proof.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   600
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   601
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   602
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   603
\subsection{Saving and restoring proof states}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   604
\index{proofs!saving and restoring}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   605
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   606
save_proof    : unit -> proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   607
restore_proof : proof -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   608
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   609
States of the subgoal module may be saved as \ML\ values of
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   610
type~\mltydx{proof}, and later restored.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   612
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   613
\item[\ttindexbold{save_proof}();]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   614
returns the current state, which is on top of the stack.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   615
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   616
\item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   617
  replaces the top of the stack by~{\it prf}.  It returns the list of
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   618
  assumptions associated with the new proof.
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   619
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   620
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   621
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3128
diff changeset
   622
\section{*Debugging and inspecting}
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   623
\index{tactics!debugging}
2611
a5b6a632768d Strengthened warnings concerning topthm(), etc.
paulson
parents: 2528
diff changeset
   624
These functions can be useful when you are debugging a tactic.  They refer
a5b6a632768d Strengthened warnings concerning topthm(), etc.
paulson
parents: 2528
diff changeset
   625
to the current proof state stored in the subgoal module.  A tactic
a5b6a632768d Strengthened warnings concerning topthm(), etc.
paulson
parents: 2528
diff changeset
   626
should never call them; it should operate on the proof state supplied as its
a5b6a632768d Strengthened warnings concerning topthm(), etc.
paulson
parents: 2528
diff changeset
   627
argument.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   628
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   629
\subsection{Reading and printing terms}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   630
\index{terms!reading of}\index{terms!printing of}\index{types!printing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   631
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   632
read    : string -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   633
prin    : term -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   634
printyp : typ -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   635
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   636
These read and print terms (or types) using the syntax associated with the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   637
proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   638
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   639
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   640
\item[\ttindexbold{read} {\it string}]  
6170
9a59cf8ae9b5 standard spelling: type-checking
paulson
parents: 5391
diff changeset
   641
reads the {\it string} as a term, without type-checking.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   642
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   643
\item[\ttindexbold{prin} {\it t};]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   644
prints the term~$t$ at the terminal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   645
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   646
\item[\ttindexbold{printyp} {\it T};]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   647
prints the type~$T$ at the terminal.
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   648
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   649
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   650
\subsection{Inspecting the proof state}
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   651
\index{proofs!inspecting the state}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   652
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   653
topthm  : unit -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   654
getgoal : int -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   655
gethyps : int -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   656
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   657
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   658
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   659
\item[\ttindexbold{topthm}()]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   660
returns the proof state as an Isabelle theorem.  This is what \ttindex{by}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   661
would supply to a tactic at this point.  It omits the post-processing of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   662
\ttindex{result} and \ttindex{uresult}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   664
\item[\ttindexbold{getgoal} {\it i}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   665
returns subgoal~$i$ of the proof state, as a term.  You may print
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   666
this using \texttt{prin}, though you may have to examine the internal
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   667
data structure in order to locate the problem!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   668
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   669
\item[\ttindexbold{gethyps} {\it i}]
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   670
  returns the hypotheses of subgoal~$i$ as meta-level assumptions.  In
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   671
  these theorems, the subgoal's parameters become free variables.  This
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   672
  command is supplied for debugging uses of \ttindex{METAHYPS}.
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   673
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   674
2611
a5b6a632768d Strengthened warnings concerning topthm(), etc.
paulson
parents: 2528
diff changeset
   675
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   676
\subsection{Filtering lists of rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   677
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   678
filter_goal: (term*term->bool) -> thm list -> int -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   679
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   680
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   681
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
\item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}] 
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4374
diff changeset
   683
applies \texttt{filter_thms {\it could}} to subgoal~$i$ of the proof
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   684
state and returns the list of theorems that survive the filtering. 
321
998f1c5adafb penultimate Springer draft
lcp
parents: 286
diff changeset
   685
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   686
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   687
\index{subgoal module|)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   688
\index{proofs|)}
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   689
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   690
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   691
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   692
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   693
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   694
%%% End: