26869
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Proof}%
|
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
\isanewline
|
|
7 |
\isanewline
|
|
8 |
%
|
|
9 |
\endisadelimtheory
|
|
10 |
%
|
|
11 |
\isatagtheory
|
|
12 |
\isacommand{theory}\isamarkupfalse%
|
|
13 |
\ Proof\isanewline
|
|
14 |
\isakeyword{imports}\ Main\isanewline
|
|
15 |
\isakeyword{begin}%
|
|
16 |
\endisatagtheory
|
|
17 |
{\isafoldtheory}%
|
|
18 |
%
|
|
19 |
\isadelimtheory
|
|
20 |
%
|
|
21 |
\endisadelimtheory
|
|
22 |
%
|
|
23 |
\isamarkupchapter{Proofs%
|
|
24 |
}
|
|
25 |
\isamarkuptrue%
|
|
26 |
%
|
26870
|
27 |
\begin{isamarkuptext}%
|
|
28 |
Proof commands perform transitions of Isar/VM machine
|
|
29 |
configurations, which are block-structured, consisting of a stack of
|
|
30 |
nodes with three main components: logical proof context, current
|
|
31 |
facts, and open goals. Isar/VM transitions are \emph{typed}
|
|
32 |
according to the following three different modes of operation:
|
|
33 |
|
|
34 |
\begin{descr}
|
|
35 |
|
|
36 |
\item [\isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}}] means that a new goal has just been
|
|
37 |
stated that is now to be \emph{proven}; the next command may refine
|
|
38 |
it by some proof method, and enter a sub-proof to establish the
|
|
39 |
actual result.
|
|
40 |
|
|
41 |
\item [\isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}}] is like a nested theory mode: the
|
|
42 |
context may be augmented by \emph{stating} additional assumptions,
|
|
43 |
intermediate results etc.
|
|
44 |
|
|
45 |
\item [\isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}}] is intermediate between \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} and \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}}: existing facts (i.e.\
|
26902
|
46 |
the contents of the special ``\indexref{}{fact}{this}\hyperlink{fact.this}{\mbox{\isa{this}}}'' register) have been
|
26870
|
47 |
just picked up in order to be used when refining the goal claimed
|
|
48 |
next.
|
|
49 |
|
|
50 |
\end{descr}
|
|
51 |
|
|
52 |
The proof mode indicator may be read as a verb telling the writer
|
|
53 |
what kind of operation may be performed next. The corresponding
|
|
54 |
typings of proof commands restricts the shape of well-formed proof
|
|
55 |
texts to particular command sequences. So dynamic arrangements of
|
|
56 |
commands eventually turn out as static texts of a certain structure.
|
|
57 |
\Appref{ap:refcard} gives a simplified grammar of the overall
|
|
58 |
(extensible) language emerging that way.%
|
|
59 |
\end{isamarkuptext}%
|
|
60 |
\isamarkuptrue%
|
|
61 |
%
|
|
62 |
\isamarkupsection{Context elements \label{sec:proof-context}%
|
|
63 |
}
|
|
64 |
\isamarkuptrue%
|
|
65 |
%
|
|
66 |
\begin{isamarkuptext}%
|
|
67 |
\begin{matharray}{rcl}
|
26902
|
68 |
\indexdef{}{command}{fix}\hypertarget{command.fix}{\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
69 |
\indexdef{}{command}{assume}\hypertarget{command.assume}{\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
70 |
\indexdef{}{command}{presume}\hypertarget{command.presume}{\hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
71 |
\indexdef{}{command}{def}\hypertarget{command.def}{\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
26870
|
72 |
\end{matharray}
|
|
73 |
|
|
74 |
The logical proof context consists of fixed variables and
|
|
75 |
assumptions. The former closely correspond to Skolem constants, or
|
|
76 |
meta-level universal quantification as provided by the Isabelle/Pure
|
|
77 |
logical framework. Introducing some \emph{arbitrary, but fixed}
|
26902
|
78 |
variable via ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}'' results in a local value
|
26870
|
79 |
that may be used in the subsequent proof as any other variable or
|
|
80 |
constant. Furthermore, any result \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} exported from
|
|
81 |
the context will be universally closed wrt.\ \isa{x} at the
|
|
82 |
outermost level: \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} (this is expressed in normal
|
|
83 |
form using Isabelle's meta-variables).
|
|
84 |
|
|
85 |
Similarly, introducing some assumption \isa{{\isasymchi}} has two effects.
|
|
86 |
On the one hand, a local theorem is created that may be used as a
|
|
87 |
fact in subsequent proof steps. On the other hand, any result
|
|
88 |
\isa{{\isachardoublequote}{\isasymchi}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} exported from the context becomes conditional wrt.\
|
|
89 |
the assumption: \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymchi}\ {\isasymLongrightarrow}\ {\isasymphi}{\isachardoublequote}}. Thus, solving an enclosing goal
|
|
90 |
using such a result would basically introduce a new subgoal stemming
|
|
91 |
from the assumption. How this situation is handled depends on the
|
26902
|
92 |
version of assumption command used: while \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}
|
26870
|
93 |
insists on solving the subgoal by unification with some premise of
|
26902
|
94 |
the goal, \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} leaves the subgoal unchanged in order
|
26870
|
95 |
to be proved later by the user.
|
|
96 |
|
26902
|
97 |
Local definitions, introduced by ``\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'', are achieved by combining ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}'' with
|
26870
|
98 |
another version of assumption that causes any hypothetical equation
|
|
99 |
\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}} to be eliminated by the reflexivity rule. Thus,
|
|
100 |
exporting some result \isa{{\isachardoublequote}x\ {\isasymequiv}\ t\ {\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} yields \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}t{\isacharbrackright}{\isachardoublequote}}.
|
|
101 |
|
|
102 |
\begin{rail}
|
|
103 |
'fix' (vars + 'and')
|
|
104 |
;
|
|
105 |
('assume' | 'presume') (props + 'and')
|
|
106 |
;
|
|
107 |
'def' (def + 'and')
|
|
108 |
;
|
|
109 |
def: thmdecl? \\ name ('==' | equiv) term termpat?
|
|
110 |
;
|
|
111 |
\end{rail}
|
|
112 |
|
|
113 |
\begin{descr}
|
|
114 |
|
26902
|
115 |
\item [\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}] introduces a local variable
|
26870
|
116 |
\isa{x} that is \emph{arbitrary, but fixed.}
|
|
117 |
|
26902
|
118 |
\item [\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} and \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] introduce a local fact \isa{{\isachardoublequote}{\isasymphi}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} by
|
26870
|
119 |
assumption. Subsequent results applied to an enclosing goal (e.g.\
|
26902
|
120 |
by \indexref{}{command}{show}\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}) are handled as follows: \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} expects to be able to unify with existing premises in the
|
|
121 |
goal, while \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} leaves \isa{{\isasymphi}} as new subgoals.
|
26870
|
122 |
|
|
123 |
Several lists of assumptions may be given (separated by
|
26902
|
124 |
\indexref{}{keyword}{and}\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}; the resulting list of current facts consists
|
26870
|
125 |
of all of these concatenated.
|
|
126 |
|
26902
|
127 |
\item [\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}] introduces a local
|
26870
|
128 |
(non-polymorphic) definition. In results exported from the context,
|
26902
|
129 |
\isa{x} is replaced by \isa{t}. Basically, ``\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'', with the resulting
|
26870
|
130 |
hypothetical equation solved by reflexivity.
|
|
131 |
|
|
132 |
The default name for the definitional equation is \isa{x{\isacharunderscore}def}.
|
|
133 |
Several simultaneous definitions may be given at the same time.
|
|
134 |
|
|
135 |
\end{descr}
|
|
136 |
|
26902
|
137 |
The special name \indexref{}{fact}{prems}\hyperlink{fact.prems}{\mbox{\isa{prems}}} refers to all assumptions of the
|
26870
|
138 |
current context as a list of theorems. This feature should be used
|
|
139 |
with great care! It is better avoided in final proof texts.%
|
|
140 |
\end{isamarkuptext}%
|
|
141 |
\isamarkuptrue%
|
|
142 |
%
|
|
143 |
\isamarkupsection{Facts and forward chaining%
|
|
144 |
}
|
|
145 |
\isamarkuptrue%
|
|
146 |
%
|
|
147 |
\begin{isamarkuptext}%
|
|
148 |
\begin{matharray}{rcl}
|
26902
|
149 |
\indexdef{}{command}{note}\hypertarget{command.note}{\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
150 |
\indexdef{}{command}{then}\hypertarget{command.then}{\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
151 |
\indexdef{}{command}{from}\hypertarget{command.from}{\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
152 |
\indexdef{}{command}{with}\hypertarget{command.with}{\hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
153 |
\indexdef{}{command}{using}\hypertarget{command.using}{\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}} & : & \isartrans{proof(prove)}{proof(prove)} \\
|
|
154 |
\indexdef{}{command}{unfolding}\hypertarget{command.unfolding}{\hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}} & : & \isartrans{proof(prove)}{proof(prove)} \\
|
26870
|
155 |
\end{matharray}
|
|
156 |
|
|
157 |
New facts are established either by assumption or proof of local
|
|
158 |
statements. Any fact will usually be involved in further proofs,
|
|
159 |
either as explicit arguments of proof methods, or when forward
|
26902
|
160 |
chaining towards the next goal via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} (and variants);
|
|
161 |
\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}} and \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}} are composite forms
|
|
162 |
involving \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}. The \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} elements
|
26870
|
163 |
augments the collection of used facts \emph{after} a goal has been
|
26902
|
164 |
stated. Note that the special theorem name \indexref{}{fact}{this}\hyperlink{fact.this}{\mbox{\isa{this}}} refers
|
26870
|
165 |
to the most recently established facts, but only \emph{before}
|
|
166 |
issuing a follow-up claim.
|
|
167 |
|
|
168 |
\begin{rail}
|
|
169 |
'note' (thmdef? thmrefs + 'and')
|
|
170 |
;
|
|
171 |
('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
|
|
172 |
;
|
|
173 |
\end{rail}
|
|
174 |
|
|
175 |
\begin{descr}
|
|
176 |
|
26902
|
177 |
\item [\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
|
26870
|
178 |
recalls existing facts \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub n{\isachardoublequote}}, binding
|
|
179 |
the result as \isa{a}. Note that attributes may be involved as
|
|
180 |
well, both on the left and right hand sides.
|
|
181 |
|
26902
|
182 |
\item [\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}] indicates forward chaining by the current
|
26870
|
183 |
facts in order to establish the goal to be claimed next. The
|
|
184 |
initial proof method invoked to refine that will be offered the
|
|
185 |
facts to do ``anything appropriate'' (see also
|
26902
|
186 |
\secref{sec:proof-steps}). For example, method \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}
|
26870
|
187 |
(see \secref{sec:pure-meth-att}) would typically do an elimination
|
|
188 |
rather than an introduction. Automatic methods usually insert the
|
|
189 |
facts into the goal state before operation. This provides a simple
|
|
190 |
scheme to control relevance of facts in automated proof search.
|
|
191 |
|
26902
|
192 |
\item [\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{b}] abbreviates ``\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{b}~\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}''; thus \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} is
|
|
193 |
equivalent to ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}''.
|
26870
|
194 |
|
26902
|
195 |
\item [\hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
|
|
196 |
abbreviates ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n\ {\isasymAND}\ this{\isachardoublequote}}''; thus the forward chaining is from earlier facts together
|
26870
|
197 |
with the current ones.
|
|
198 |
|
26902
|
199 |
\item [\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] augments
|
26870
|
200 |
the facts being currently indicated for use by a subsequent
|
26902
|
201 |
refinement step (such as \indexref{}{command}{apply}\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} or \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}).
|
26870
|
202 |
|
26902
|
203 |
\item [\hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] is
|
|
204 |
structurally similar to \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}, but unfolds definitional
|
26870
|
205 |
equations \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} throughout the goal state
|
|
206 |
and facts.
|
|
207 |
|
|
208 |
\end{descr}
|
|
209 |
|
|
210 |
Forward chaining with an empty list of theorems is the same as not
|
26902
|
211 |
chaining at all. Thus ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{nothing}'' has no
|
26870
|
212 |
effect apart from entering \isa{{\isachardoublequote}prove{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode, since
|
26902
|
213 |
\indexref{}{fact}{nothing}\hyperlink{fact.nothing}{\mbox{\isa{nothing}}} is bound to the empty list of theorems.
|
26870
|
214 |
|
26902
|
215 |
Basic proof methods (such as \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}) expect multiple
|
26870
|
216 |
facts to be given in their proper order, corresponding to a prefix
|
|
217 |
of the premises of the rule involved. Note that positions may be
|
26902
|
218 |
easily skipped using something like \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isachardoublequote}{\isacharunderscore}\ {\isasymAND}\ a\ {\isasymAND}\ b{\isachardoublequote}}, for example. This involves the trivial rule
|
26870
|
219 |
\isa{{\isachardoublequote}PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}{\isachardoublequote}}, which is bound in Isabelle/Pure as
|
26902
|
220 |
``\indexref{}{fact}{\_}\hyperlink{fact._}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore).
|
26870
|
221 |
|
26902
|
222 |
Automated methods (such as \hyperlink{method.simp}{\mbox{\isa{simp}}} or \hyperlink{method.auto}{\mbox{\isa{auto}}}) just
|
26870
|
223 |
insert any given facts before their usual operation. Depending on
|
|
224 |
the kind of procedure involved, the order of facts is less
|
|
225 |
significant here.%
|
|
226 |
\end{isamarkuptext}%
|
|
227 |
\isamarkuptrue%
|
|
228 |
%
|
|
229 |
\isamarkupsection{Goal statements \label{sec:goals}%
|
|
230 |
}
|
|
231 |
\isamarkuptrue%
|
|
232 |
%
|
|
233 |
\begin{isamarkuptext}%
|
|
234 |
\begin{matharray}{rcl}
|
26902
|
235 |
\indexdef{}{command}{lemma}\hypertarget{command.lemma}{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
|
|
236 |
\indexdef{}{command}{theorem}\hypertarget{command.theorem}{\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
|
|
237 |
\indexdef{}{command}{corollary}\hypertarget{command.corollary}{\hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
|
|
238 |
\indexdef{}{command}{have}\hypertarget{command.have}{\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
|
|
239 |
\indexdef{}{command}{show}\hypertarget{command.show}{\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
|
|
240 |
\indexdef{}{command}{hence}\hypertarget{command.hence}{\hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}}} & : & \isartrans{proof(state)}{proof(prove)} \\
|
|
241 |
\indexdef{}{command}{thus}\hypertarget{command.thus}{\hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}}} & : & \isartrans{proof(state)}{proof(prove)} \\
|
|
242 |
\indexdef{}{command}{print\_statement}\hypertarget{command.print_statement}{\hyperlink{command.print_statement}{\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
26870
|
243 |
\end{matharray}
|
|
244 |
|
|
245 |
From a theory context, proof mode is entered by an initial goal
|
26902
|
246 |
command such as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}, \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}, or
|
|
247 |
\hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}. Within a proof, new claims may be
|
26870
|
248 |
introduced locally as well; four variants are available here to
|
|
249 |
indicate whether forward chaining of facts should be performed
|
26902
|
250 |
initially (via \indexref{}{command}{then}\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}), and whether the final result
|
26870
|
251 |
is meant to solve some pending goal.
|
|
252 |
|
|
253 |
Goals may consist of multiple statements, resulting in a list of
|
|
254 |
facts eventually. A pending multi-goal is internally represented as
|
|
255 |
a meta-level conjunction (printed as \isa{{\isachardoublequote}{\isacharampersand}{\isacharampersand}{\isachardoublequote}}), which is usually
|
|
256 |
split into the corresponding number of sub-goals prior to an initial
|
26902
|
257 |
method application, via \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}
|
|
258 |
(\secref{sec:proof-steps}) or \indexref{}{command}{apply}\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}
|
|
259 |
(\secref{sec:tactic-commands}). The \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}} method
|
26870
|
260 |
covered in \secref{sec:cases-induct} acts on multiple claims
|
|
261 |
simultaneously.
|
|
262 |
|
|
263 |
Claims at the theory level may be either in short or long form. A
|
|
264 |
short goal merely consists of several simultaneous propositions
|
|
265 |
(often just one). A long goal includes an explicit context
|
|
266 |
specification for the subsequent conclusion, involving local
|
|
267 |
parameters and assumptions. Here the role of each part of the
|
|
268 |
statement is explicitly marked by separate keywords (see also
|
|
269 |
\secref{sec:locale}); the local assumptions being introduced here
|
26902
|
270 |
are available as \indexref{}{fact}{assms}\hyperlink{fact.assms}{\mbox{\isa{assms}}} in the proof. Moreover, there
|
|
271 |
are two kinds of conclusions: \indexdef{}{element}{shows}\hypertarget{element.shows}{\hyperlink{element.shows}{\mbox{\isa{\isakeyword{shows}}}}} states several
|
26870
|
272 |
simultaneous propositions (essentially a big conjunction), while
|
26902
|
273 |
\indexdef{}{element}{obtains}\hypertarget{element.obtains}{\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}}} claims several simultaneous simultaneous
|
26870
|
274 |
contexts of (essentially a big disjunction of eliminated parameters
|
|
275 |
and assumptions, cf.\ \secref{sec:obtain}).
|
|
276 |
|
|
277 |
\begin{rail}
|
|
278 |
('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
|
|
279 |
;
|
|
280 |
('have' | 'show' | 'hence' | 'thus') goal
|
|
281 |
;
|
|
282 |
'print\_statement' modes? thmrefs
|
|
283 |
;
|
|
284 |
|
|
285 |
goal: (props + 'and')
|
|
286 |
;
|
|
287 |
longgoal: thmdecl? (contextelem *) conclusion
|
|
288 |
;
|
|
289 |
conclusion: 'shows' goal | 'obtains' (parname? case + '|')
|
|
290 |
;
|
|
291 |
case: (vars + 'and') 'where' (props + 'and')
|
|
292 |
;
|
|
293 |
\end{rail}
|
|
294 |
|
|
295 |
\begin{descr}
|
|
296 |
|
26902
|
297 |
\item [\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] enters proof mode with
|
26870
|
298 |
\isa{{\isasymphi}} as main goal, eventually resulting in some fact \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} to be put back into the target context. An additional
|
|
299 |
\railnonterm{context} specification may build up an initial proof
|
|
300 |
context for the subsequent claim; this includes local definitions
|
26902
|
301 |
and syntax as well, see the definition of \hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}} in
|
26870
|
302 |
\secref{sec:locale}.
|
|
303 |
|
26902
|
304 |
\item [\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} and \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] are essentially the same as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}, but the facts are internally marked as
|
26870
|
305 |
being of a different kind. This discrimination acts like a formal
|
|
306 |
comment.
|
|
307 |
|
26902
|
308 |
\item [\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] claims a local goal,
|
26870
|
309 |
eventually resulting in a fact within the current logical context.
|
|
310 |
This operation is completely independent of any pending sub-goals of
|
26902
|
311 |
an enclosing goal statements, so \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} may be freely
|
26870
|
312 |
used for experimental exploration of potential results within a
|
|
313 |
proof body.
|
|
314 |
|
26902
|
315 |
\item [\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] is like \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} plus a second stage to refine some pending
|
26870
|
316 |
sub-goal for each one of the finished result, after having been
|
|
317 |
exported into the corresponding context (at the head of the
|
26902
|
318 |
sub-proof of this \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} command).
|
26870
|
319 |
|
|
320 |
To accommodate interactive debugging, resulting rules are printed
|
|
321 |
before being applied internally. Even more, interactive execution
|
26902
|
322 |
of \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} predicts potential failure and displays the
|
26870
|
323 |
resulting error as a warning beforehand. Watch out for the
|
|
324 |
following message:
|
|
325 |
|
|
326 |
%FIXME proper antiquitation
|
|
327 |
\begin{ttbox}
|
|
328 |
Problem! Local statement will fail to solve any pending goal
|
|
329 |
\end{ttbox}
|
|
330 |
|
26902
|
331 |
\item [\hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}}] abbreviates ``\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}'', i.e.\ claims a local goal to be proven by forward
|
|
332 |
chaining the current facts. Note that \hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}} is also
|
|
333 |
equivalent to ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}''.
|
26870
|
334 |
|
26902
|
335 |
\item [\hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}}] abbreviates ``\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}''. Note that \hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}} is also equivalent to
|
|
336 |
``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}''.
|
26870
|
337 |
|
26902
|
338 |
\item [\hyperlink{command.print_statement}{\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}}~\isa{a}] prints facts from the
|
26870
|
339 |
current theory or proof context in long statement form, according to
|
26902
|
340 |
the syntax for \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} given above.
|
26870
|
341 |
|
|
342 |
\end{descr}
|
|
343 |
|
|
344 |
Any goal statement causes some term abbreviations (such as
|
26902
|
345 |
\indexref{}{variable}{?thesis}\hyperlink{variable.?thesis}{\mbox{\isa{{\isacharquery}thesis}}}) to be bound automatically, see also
|
26870
|
346 |
\secref{sec:term-abbrev}. Furthermore, the local context of a
|
26902
|
347 |
(non-atomic) goal is provided via the \indexref{}{case}{rule\_context}\hyperlink{case.rule_context}{\mbox{\isa{rule{\isacharunderscore}context}}} case.
|
26870
|
348 |
|
26902
|
349 |
The optional case names of \indexref{}{element}{obtains}\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}} have a twofold
|
26870
|
350 |
meaning: (1) during the of this claim they refer to the the local
|
|
351 |
context introductions, (2) the resulting rule is annotated
|
|
352 |
accordingly to support symbolic case splits when used with the
|
26902
|
353 |
\indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} method (cf. \secref{sec:cases-induct}).
|
26870
|
354 |
|
|
355 |
\medskip
|
|
356 |
|
|
357 |
\begin{warn}
|
|
358 |
Isabelle/Isar suffers theory-level goal statements to contain
|
|
359 |
\emph{unbound schematic variables}, although this does not conform
|
|
360 |
to the aim of human-readable proof documents! The main problem
|
|
361 |
with schematic goals is that the actual outcome is usually hard to
|
|
362 |
predict, depending on the behavior of the proof methods applied
|
|
363 |
during the course of reasoning. Note that most semi-automated
|
|
364 |
methods heavily depend on several kinds of implicit rule
|
|
365 |
declarations within the current theory context. As this would
|
|
366 |
also result in non-compositional checking of sub-proofs,
|
|
367 |
\emph{local goals} are not allowed to be schematic at all.
|
|
368 |
Nevertheless, schematic goals do have their use in Prolog-style
|
|
369 |
interactive synthesis of proven results, usually by stepwise
|
|
370 |
refinement via emulation of traditional Isabelle tactic scripts
|
|
371 |
(see also \secref{sec:tactic-commands}). In any case, users
|
|
372 |
should know what they are doing.
|
|
373 |
\end{warn}%
|
|
374 |
\end{isamarkuptext}%
|
|
375 |
\isamarkuptrue%
|
|
376 |
%
|
|
377 |
\isamarkupsection{Initial and terminal proof steps \label{sec:proof-steps}%
|
|
378 |
}
|
|
379 |
\isamarkuptrue%
|
|
380 |
%
|
|
381 |
\begin{isamarkuptext}%
|
|
382 |
\begin{matharray}{rcl}
|
26902
|
383 |
\indexdef{}{command}{proof}\hypertarget{command.proof}{\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}} & : & \isartrans{proof(prove)}{proof(state)} \\
|
|
384 |
\indexdef{}{command}{qed}\hypertarget{command.qed}{\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
|
|
385 |
\indexdef{}{command}{by}\hypertarget{command.by}{\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
|
386 |
\indexdef{}{command}{..}\hypertarget{command.ddot}{\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
|
387 |
\indexdef{}{command}{.}\hypertarget{command.dot}{\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
|
388 |
\indexdef{}{command}{sorry}\hypertarget{command.sorry}{\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
26870
|
389 |
\end{matharray}
|
|
390 |
|
|
391 |
Arbitrary goal refinement via tactics is considered harmful.
|
|
392 |
Structured proof composition in Isar admits proof methods to be
|
|
393 |
invoked in two places only.
|
|
394 |
|
|
395 |
\begin{enumerate}
|
|
396 |
|
26902
|
397 |
\item An \emph{initial} refinement step \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} reduces a newly stated goal to a number
|
26870
|
398 |
of sub-goals that are to be solved later. Facts are passed to
|
|
399 |
\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} for forward chaining, if so indicated by \isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode.
|
|
400 |
|
26902
|
401 |
\item A \emph{terminal} conclusion step \indexref{}{command}{qed}\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} is intended to solve remaining goals. No facts are
|
26870
|
402 |
passed to \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
|
|
403 |
|
|
404 |
\end{enumerate}
|
|
405 |
|
|
406 |
The only other (proper) way to affect pending goals in a proof body
|
26902
|
407 |
is by \indexref{}{command}{show}\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, which involves an explicit statement of
|
26870
|
408 |
what is to be solved eventually. Thus we avoid the fundamental
|
|
409 |
problem of unstructured tactic scripts that consist of numerous
|
|
410 |
consecutive goal transformations, with invisible effects.
|
|
411 |
|
|
412 |
\medskip As a general rule of thumb for good proof style, initial
|
|
413 |
proof methods should either solve the goal completely, or constitute
|
|
414 |
some well-understood reduction to new sub-goals. Arbitrary
|
|
415 |
automatic proof tools that are prone leave a large number of badly
|
|
416 |
structured sub-goals are no help in continuing the proof document in
|
|
417 |
an intelligible manner.
|
|
418 |
|
|
419 |
Unless given explicitly by the user, the default initial method is
|
26902
|
420 |
``\indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}'', which applies a single standard elimination
|
26870
|
421 |
or introduction rule according to the topmost symbol involved.
|
|
422 |
There is no separate default terminal method. Any remaining goals
|
|
423 |
are always solved by assumption in the very last step.
|
|
424 |
|
|
425 |
\begin{rail}
|
|
426 |
'proof' method?
|
|
427 |
;
|
|
428 |
'qed' method?
|
|
429 |
;
|
|
430 |
'by' method method?
|
|
431 |
;
|
|
432 |
('.' | '..' | 'sorry')
|
|
433 |
;
|
|
434 |
\end{rail}
|
|
435 |
|
|
436 |
\begin{descr}
|
|
437 |
|
26902
|
438 |
\item [\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}] refines the goal by
|
26870
|
439 |
proof method \isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}; facts for forward chaining are
|
|
440 |
passed if so indicated by \isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode.
|
|
441 |
|
26902
|
442 |
\item [\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}] refines any remaining
|
26870
|
443 |
goals by proof method \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} and concludes the
|
|
444 |
sub-proof by assumption. If the goal had been \isa{{\isachardoublequote}show{\isachardoublequote}} (or
|
|
445 |
\isa{{\isachardoublequote}thus{\isachardoublequote}}), some pending sub-goal is solved as well by the rule
|
|
446 |
resulting from the result \emph{exported} into the enclosing goal
|
|
447 |
context. Thus \isa{{\isachardoublequote}qed{\isachardoublequote}} may fail for two reasons: either \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} fails, or the resulting rule does not fit to any
|
|
448 |
pending goal\footnote{This includes any additional ``strong''
|
26902
|
449 |
assumptions as introduced by \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}.} of the enclosing
|
26870
|
450 |
context. Debugging such a situation might involve temporarily
|
26902
|
451 |
changing \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} into \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, or weakening the
|
|
452 |
local context by replacing occurrences of \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} by
|
|
453 |
\hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}.
|
26870
|
454 |
|
26902
|
455 |
\item [\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}}] is a
|
26870
|
456 |
\emph{terminal proof}\index{proof!terminal}; it abbreviates
|
26902
|
457 |
\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\isa{{\isachardoublequote}qed{\isachardoublequote}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}, but with backtracking across both methods. Debugging
|
|
458 |
an unsuccessful \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}}
|
26870
|
459 |
command can be done by expanding its definition; in many cases
|
26902
|
460 |
\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} (or even \isa{{\isachardoublequote}apply{\isachardoublequote}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}) is already sufficient to see the
|
26870
|
461 |
problem.
|
|
462 |
|
26902
|
463 |
\item [``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}''] is a \emph{default
|
|
464 |
proof}\index{proof!default}; it abbreviates \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}rule{\isachardoublequote}}.
|
26870
|
465 |
|
26902
|
466 |
\item [``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}''] is a \emph{trivial
|
|
467 |
proof}\index{proof!trivial}; it abbreviates \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}this{\isachardoublequote}}.
|
26870
|
468 |
|
26902
|
469 |
\item [\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}}] is a \emph{fake proof}\index{proof!fake}
|
26870
|
470 |
pretending to solve the pending claim without further ado. This
|
|
471 |
only works in interactive development, or if the \verb|quick_and_dirty| flag is enabled (in ML). Facts emerging from fake
|
|
472 |
proofs are not the real thing. Internally, each theorem container
|
|
473 |
is tainted by an oracle invocation, which is indicated as ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' in the printed result.
|
|
474 |
|
26902
|
475 |
The most important application of \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} is to support
|
26870
|
476 |
experimentation and top-down proof development.
|
|
477 |
|
|
478 |
\end{descr}%
|
|
479 |
\end{isamarkuptext}%
|
|
480 |
\isamarkuptrue%
|
|
481 |
%
|
|
482 |
\isamarkupsection{Fundamental methods and attributes \label{sec:pure-meth-att}%
|
|
483 |
}
|
|
484 |
\isamarkuptrue%
|
|
485 |
%
|
|
486 |
\begin{isamarkuptext}%
|
|
487 |
The following proof methods and attributes refer to basic logical
|
|
488 |
operations of Isar. Further methods and attributes are provided by
|
|
489 |
several generic and object-logic specific tools and packages (see
|
|
490 |
\chref{ch:gen-tools} and \chref{ch:hol}).
|
|
491 |
|
|
492 |
\begin{matharray}{rcl}
|
26902
|
493 |
\indexdef{}{method}{-}\hypertarget{method.-}{\hyperlink{method.-}{\mbox{\isa{{\isacharminus}}}}} & : & \isarmeth \\
|
|
494 |
\indexdef{}{method}{fact}\hypertarget{method.fact}{\hyperlink{method.fact}{\mbox{\isa{fact}}}} & : & \isarmeth \\
|
|
495 |
\indexdef{}{method}{assumption}\hypertarget{method.assumption}{\hyperlink{method.assumption}{\mbox{\isa{assumption}}}} & : & \isarmeth \\
|
|
496 |
\indexdef{}{method}{this}\hypertarget{method.this}{\hyperlink{method.this}{\mbox{\isa{this}}}} & : & \isarmeth \\
|
|
497 |
\indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isarmeth \\
|
|
498 |
\indexdef{}{method}{iprover}\hypertarget{method.iprover}{\hyperlink{method.iprover}{\mbox{\isa{iprover}}}} & : & \isarmeth \\[0.5ex]
|
|
499 |
\indexdef{Pure}{attribute}{intro}\hypertarget{attribute.Pure.intro}{\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}} & : & \isaratt \\
|
|
500 |
\indexdef{Pure}{attribute}{elim}\hypertarget{attribute.Pure.elim}{\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}} & : & \isaratt \\
|
|
501 |
\indexdef{Pure}{attribute}{dest}\hypertarget{attribute.Pure.dest}{\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}} & : & \isaratt \\
|
|
502 |
\indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isaratt \\[0.5ex]
|
|
503 |
\indexdef{}{attribute}{OF}\hypertarget{attribute.OF}{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}} & : & \isaratt \\
|
|
504 |
\indexdef{}{attribute}{of}\hypertarget{attribute.of}{\hyperlink{attribute.of}{\mbox{\isa{of}}}} & : & \isaratt \\
|
|
505 |
\indexdef{}{attribute}{where}\hypertarget{attribute.where}{\hyperlink{attribute.where}{\mbox{\isa{where}}}} & : & \isaratt \\
|
26870
|
506 |
\end{matharray}
|
|
507 |
|
|
508 |
\begin{rail}
|
|
509 |
'fact' thmrefs?
|
|
510 |
;
|
|
511 |
'rule' thmrefs?
|
|
512 |
;
|
|
513 |
'iprover' ('!' ?) (rulemod *)
|
|
514 |
;
|
|
515 |
rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
|
|
516 |
;
|
|
517 |
('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
|
|
518 |
;
|
|
519 |
'rule' 'del'
|
|
520 |
;
|
|
521 |
'OF' thmrefs
|
|
522 |
;
|
|
523 |
'of' insts ('concl' ':' insts)?
|
|
524 |
;
|
|
525 |
'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
|
|
526 |
;
|
|
527 |
\end{rail}
|
|
528 |
|
|
529 |
\begin{descr}
|
|
530 |
|
26902
|
531 |
\item [``\hyperlink{method.-}{\mbox{\isa{{\isacharminus}}}}'' (minus)] does nothing but insert the
|
26870
|
532 |
forward chaining facts as premises into the goal. Note that command
|
26902
|
533 |
\indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} without any method actually performs a single
|
|
534 |
reduction step using the \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}} method; thus a plain
|
|
535 |
\emph{do-nothing} proof step would be ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' rather than \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} alone.
|
26870
|
536 |
|
26902
|
537 |
\item [\hyperlink{method.fact}{\mbox{\isa{fact}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] composes
|
26870
|
538 |
some fact from \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} (or implicitly from
|
|
539 |
the current proof context) modulo unification of schematic type and
|
|
540 |
term variables. The rule structure is not taken into account, i.e.\
|
|
541 |
meta-level implication is considered atomic. This is the same
|
|
542 |
principle underlying literal facts (cf.\ \secref{sec:syn-att}):
|
26902
|
543 |
``\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}~\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{fact}'' is
|
|
544 |
equivalent to ``\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\verb|`|\isa{{\isasymphi}}\verb|`|'' provided that \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} is an instance of some known
|
26870
|
545 |
\isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} in the proof context.
|
|
546 |
|
26902
|
547 |
\item [\hyperlink{method.assumption}{\mbox{\isa{assumption}}}] solves some goal by a single assumption
|
26870
|
548 |
step. All given facts are guaranteed to participate in the
|
|
549 |
refinement; this means there may be only 0 or 1 in the first place.
|
26902
|
550 |
Recall that \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} (\secref{sec:proof-steps}) already
|
26870
|
551 |
concludes any remaining sub-goals by assumption, so structured
|
26902
|
552 |
proofs usually need not quote the \hyperlink{method.assumption}{\mbox{\isa{assumption}}} method at
|
26870
|
553 |
all.
|
|
554 |
|
26902
|
555 |
\item [\hyperlink{method.this}{\mbox{\isa{this}}}] applies all of the current facts directly as
|
|
556 |
rules. Recall that ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}'' (dot) abbreviates ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{this}''.
|
26870
|
557 |
|
26902
|
558 |
\item [\hyperlink{method.rule}{\mbox{\isa{rule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] applies some
|
26870
|
559 |
rule given as argument in backward manner; facts are used to reduce
|
26902
|
560 |
the rule before applying it to the goal. Thus \hyperlink{method.rule}{\mbox{\isa{rule}}}
|
26870
|
561 |
without facts is plain introduction, while with facts it becomes
|
|
562 |
elimination.
|
|
563 |
|
26902
|
564 |
When no arguments are given, the \hyperlink{method.rule}{\mbox{\isa{rule}}} method tries to pick
|
26870
|
565 |
appropriate rules automatically, as declared in the current context
|
26902
|
566 |
using the \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}},
|
|
567 |
\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} attributes (see below). This is the
|
|
568 |
default behavior of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}''
|
|
569 |
(double-dot) steps (see \secref{sec:proof-steps}).
|
26870
|
570 |
|
26902
|
571 |
\item [\hyperlink{method.iprover}{\mbox{\isa{iprover}}}] performs intuitionistic proof search,
|
26870
|
572 |
depending on specifically declared rules from the context, or given
|
|
573 |
as explicit arguments. Chained facts are inserted into the goal
|
26902
|
574 |
before commencing proof search; ``\hyperlink{method.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''
|
|
575 |
means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well.
|
26870
|
576 |
|
26902
|
577 |
Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
|
|
578 |
\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
|
|
579 |
``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
|
|
580 |
applied aggressively (without considering back-tracking later).
|
|
581 |
Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the
|
|
582 |
single-step \hyperlink{method.rule}{\mbox{\isa{rule}}} method still observes these). An
|
|
583 |
explicit weight annotation may be given as well; otherwise the
|
|
584 |
number of rule premises will be taken into account here.
|
26870
|
585 |
|
26902
|
586 |
\item [\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, and
|
|
587 |
\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}] declare introduction, elimination, and
|
|
588 |
destruct rules, to be used with the \hyperlink{method.rule}{\mbox{\isa{rule}}} and \hyperlink{method.iprover}{\mbox{\isa{iprover}}} methods. Note that the latter will ignore rules declared
|
|
589 |
with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' are used most
|
|
590 |
aggressively.
|
26870
|
591 |
|
|
592 |
The classical reasoner (see \secref{sec:classical}) introduces its
|
|
593 |
own variants of these attributes; use qualified names to access the
|
26902
|
594 |
present versions of Isabelle/Pure, i.e.\ \hyperlink{attribute.Pure.Pure.intro}{\mbox{\isa{Pure{\isachardot}intro}}}.
|
26870
|
595 |
|
26902
|
596 |
\item [\hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del}] undeclares introduction,
|
26870
|
597 |
elimination, or destruct rules.
|
|
598 |
|
26902
|
599 |
\item [\hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] applies some
|
26870
|
600 |
theorem to all of the given rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}}
|
|
601 |
(in parallel). This corresponds to the \verb|"op MRS"| operation in
|
|
602 |
ML, but note the reversed order. Positions may be effectively
|
|
603 |
skipped by including ``\isa{{\isacharunderscore}}'' (underscore) as argument.
|
|
604 |
|
26902
|
605 |
\item [\hyperlink{attribute.of}{\mbox{\isa{of}}}~\isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}] performs
|
26870
|
606 |
positional instantiation of term variables. The terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}} are substituted for any schematic
|
26895
|
607 |
variables occurring in a theorem from left to right; ``\isa{{\isacharunderscore}}''
|
|
608 |
(underscore) indicates to skip a position. Arguments following a
|
|
609 |
``\isa{{\isachardoublequote}concl{\isacharcolon}{\isachardoublequote}}'' specification refer to positions of the
|
|
610 |
conclusion of a rule.
|
26870
|
611 |
|
26902
|
612 |
\item [\hyperlink{attribute.where}{\mbox{\isa{where}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isacharequal}\ t\isactrlsub n{\isachardoublequote}}] performs named instantiation of schematic
|
26870
|
613 |
type and term variables occurring in a theorem. Schematic variables
|
|
614 |
have to be specified on the left-hand side (e.g.\ \isa{{\isachardoublequote}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{3}}{\isachardoublequote}}).
|
|
615 |
The question mark may be omitted if the variable name is a plain
|
|
616 |
identifier without index. As type instantiations are inferred from
|
|
617 |
term instantiations, explicit type instantiations are seldom
|
|
618 |
necessary.
|
|
619 |
|
|
620 |
\end{descr}%
|
|
621 |
\end{isamarkuptext}%
|
|
622 |
\isamarkuptrue%
|
|
623 |
%
|
|
624 |
\isamarkupsection{Term abbreviations \label{sec:term-abbrev}%
|
|
625 |
}
|
|
626 |
\isamarkuptrue%
|
|
627 |
%
|
|
628 |
\begin{isamarkuptext}%
|
|
629 |
\begin{matharray}{rcl}
|
26902
|
630 |
\indexdef{}{command}{let}\hypertarget{command.let}{\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
631 |
\indexdef{}{keyword}{is}\hypertarget{keyword.is}{\hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}}} & : & syntax \\
|
26870
|
632 |
\end{matharray}
|
|
633 |
|
26902
|
634 |
Abbreviations may be either bound by explicit \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}~\isa{{\isachardoublequote}p\ {\isasymequiv}\ t{\isachardoublequote}} statements, or by annotating assumptions or
|
26870
|
635 |
goal statements with a list of patterns ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}''. In both cases, higher-order matching is invoked to
|
|
636 |
bind extra-logical term variables, which may be either named
|
|
637 |
schematic variables of the form \isa{{\isacharquery}x}, or nameless dummies
|
26902
|
638 |
``\hyperlink{variable._}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore). Note that in the \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}
|
|
639 |
form the patterns occur on the left-hand side, while the \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns are in postfix position.
|
26870
|
640 |
|
|
641 |
Polymorphism of term bindings is handled in Hindley-Milner style,
|
|
642 |
similar to ML. Type variables referring to local assumptions or
|
|
643 |
open goal statements are \emph{fixed}, while those of finished
|
26902
|
644 |
results or bound by \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} may occur in \emph{arbitrary}
|
26870
|
645 |
instances later. Even though actual polymorphism should be rarely
|
|
646 |
used in practice, this mechanism is essential to achieve proper
|
|
647 |
incremental type-inference, as the user proceeds to build up the
|
|
648 |
Isar proof text from left to right.
|
|
649 |
|
|
650 |
\medskip Term abbreviations are quite different from local
|
26902
|
651 |
definitions as introduced via \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} (see
|
26870
|
652 |
\secref{sec:proof-context}). The latter are visible within the
|
|
653 |
logic as actual equations, while abbreviations disappear during the
|
26902
|
654 |
input process just after type checking. Also note that \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} does not support polymorphism.
|
26870
|
655 |
|
|
656 |
\begin{rail}
|
|
657 |
'let' ((term + 'and') '=' term + 'and')
|
|
658 |
;
|
|
659 |
\end{rail}
|
|
660 |
|
26902
|
661 |
The syntax of \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns follows \railnonterm{termpat}
|
26870
|
662 |
or \railnonterm{proppat} (see \secref{sec:term-decls}).
|
|
663 |
|
|
664 |
\begin{descr}
|
|
665 |
|
26902
|
666 |
\item [\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ p\isactrlsub n\ {\isacharequal}\ t\isactrlsub n{\isachardoublequote}}] binds any text variables in patterns \isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isachardoublequote}} by simultaneous higher-order matching
|
26870
|
667 |
against terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}}.
|
|
668 |
|
26902
|
669 |
\item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}] resembles \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}, but matches \isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isachardoublequote}} against the
|
|
670 |
preceding statement. Also note that \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} is not a
|
|
671 |
separate command, but part of others (such as \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}},
|
|
672 |
\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} etc.).
|
26870
|
673 |
|
|
674 |
\end{descr}
|
|
675 |
|
|
676 |
Some \emph{implicit} term abbreviations\index{term abbreviations}
|
|
677 |
for goals and facts are available as well. For any open goal,
|
26902
|
678 |
\indexref{}{variable}{thesis}\hyperlink{variable.thesis}{\mbox{\isa{thesis}}} refers to its object-level statement,
|
26870
|
679 |
abstracted over any meta-level parameters (if present). Likewise,
|
26902
|
680 |
\indexref{}{variable}{this}\hyperlink{variable.this}{\mbox{\isa{this}}} is bound for fact statements resulting from
|
|
681 |
assumptions or finished goals. In case \hyperlink{variable.this}{\mbox{\isa{this}}} refers to
|
26870
|
682 |
an object-logic statement that is an application \isa{{\isachardoublequote}f\ t{\isachardoublequote}}, then
|
26902
|
683 |
\isa{t} is bound to the special text variable ``\hyperlink{variable.dots}{\mbox{\isa{{\isasymdots}}}}''
|
26870
|
684 |
(three dots). The canonical application of this convenience are
|
|
685 |
calculational proofs (see \secref{sec:calculation}).%
|
|
686 |
\end{isamarkuptext}%
|
|
687 |
\isamarkuptrue%
|
|
688 |
%
|
|
689 |
\isamarkupsection{Block structure%
|
|
690 |
}
|
|
691 |
\isamarkuptrue%
|
|
692 |
%
|
|
693 |
\begin{isamarkuptext}%
|
|
694 |
\begin{matharray}{rcl}
|
26902
|
695 |
\indexdef{}{command}{next}\hypertarget{command.next}{\hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
696 |
\indexdef{}{command}{\{}\hypertarget{command.braceleft}{\hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isacharbraceleft}}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
697 |
\indexdef{}{command}{\}}\hypertarget{command.braceright}{\hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isacharbraceright}}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
26870
|
698 |
\end{matharray}
|
|
699 |
|
|
700 |
While Isar is inherently block-structured, opening and closing
|
|
701 |
blocks is mostly handled rather casually, with little explicit
|
|
702 |
user-intervention. Any local goal statement automatically opens
|
|
703 |
\emph{two} internal blocks, which are closed again when concluding
|
26902
|
704 |
the sub-proof (by \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} etc.). Sections of different
|
|
705 |
context within a sub-proof may be switched via \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}},
|
26870
|
706 |
which is just a single block-close followed by block-open again.
|
26902
|
707 |
The effect of \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} is to reset the local proof context;
|
26870
|
708 |
there is no goal focus involved here!
|
|
709 |
|
|
710 |
For slightly more advanced applications, there are explicit block
|
|
711 |
parentheses as well. These typically achieve a stronger forward
|
|
712 |
style of reasoning.
|
|
713 |
|
|
714 |
\begin{descr}
|
|
715 |
|
26902
|
716 |
\item [\hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}}] switches to a fresh block within a
|
26870
|
717 |
sub-proof, resetting the local context to the initial one.
|
|
718 |
|
26902
|
719 |
\item [\hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isacharbraceleft}}}}} and \hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isacharbraceright}}}}}] explicitly open and close
|
|
720 |
blocks. Any current facts pass through ``\hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isacharbraceleft}}}}}''
|
|
721 |
unchanged, while ``\hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isacharbraceright}}}}}'' causes any result to be
|
26870
|
722 |
\emph{exported} into the enclosing context. Thus fixed variables
|
|
723 |
are generalized, assumptions discharged, and local definitions
|
|
724 |
unfolded (cf.\ \secref{sec:proof-context}). There is no difference
|
26902
|
725 |
of \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} and \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} in this mode of
|
26870
|
726 |
forward reasoning --- in contrast to plain backward reasoning with
|
26902
|
727 |
the result exported at \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} time.
|
26870
|
728 |
|
|
729 |
\end{descr}%
|
|
730 |
\end{isamarkuptext}%
|
|
731 |
\isamarkuptrue%
|
|
732 |
%
|
|
733 |
\isamarkupsection{Emulating tactic scripts \label{sec:tactic-commands}%
|
|
734 |
}
|
|
735 |
\isamarkuptrue%
|
|
736 |
%
|
|
737 |
\begin{isamarkuptext}%
|
|
738 |
The Isar provides separate commands to accommodate tactic-style
|
|
739 |
proof scripts within the same system. While being outside the
|
|
740 |
orthodox Isar proof language, these might come in handy for
|
|
741 |
interactive exploration and debugging, or even actual tactical proof
|
|
742 |
within new-style theories (to benefit from document preparation, for
|
|
743 |
example). See also \secref{sec:tactics} for actual tactics, that
|
|
744 |
have been encapsulated as proof methods. Proper proof methods may
|
|
745 |
be used in scripts, too.
|
|
746 |
|
|
747 |
\begin{matharray}{rcl}
|
26902
|
748 |
\indexdef{}{command}{apply}\hypertarget{command.apply}{\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(prove)}{proof(prove)} \\
|
|
749 |
\indexdef{}{command}{apply\_end}\hypertarget{command.apply_end}{\hyperlink{command.apply_end}{\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
750 |
\indexdef{}{command}{done}\hypertarget{command.done}{\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(prove)}{proof(state)} \\
|
|
751 |
\indexdef{}{command}{defer}\hypertarget{command.defer}{\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof}{proof} \\
|
|
752 |
\indexdef{}{command}{prefer}\hypertarget{command.prefer}{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof}{proof} \\
|
|
753 |
\indexdef{}{command}{back}\hypertarget{command.back}{\hyperlink{command.back}{\mbox{\isa{\isacommand{back}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof}{proof} \\
|
26870
|
754 |
\end{matharray}
|
|
755 |
|
|
756 |
\begin{rail}
|
|
757 |
( 'apply' | 'apply\_end' ) method
|
|
758 |
;
|
|
759 |
'defer' nat?
|
|
760 |
;
|
|
761 |
'prefer' nat
|
|
762 |
;
|
|
763 |
\end{rail}
|
|
764 |
|
|
765 |
\begin{descr}
|
|
766 |
|
26902
|
767 |
\item [\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{m}] applies proof method \isa{m}
|
|
768 |
in initial position, but unlike \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} it retains
|
26870
|
769 |
``\isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}}'' mode. Thus consecutive method
|
|
770 |
applications may be given just as in tactic scripts.
|
|
771 |
|
|
772 |
Facts are passed to \isa{m} as indicated by the goal's
|
|
773 |
forward-chain mode, and are \emph{consumed} afterwards. Thus any
|
26902
|
774 |
further \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} command would always work in a purely
|
26870
|
775 |
backward manner.
|
|
776 |
|
26902
|
777 |
\item [\hyperlink{command.apply_end}{\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}}~\isa{{\isachardoublequote}m{\isachardoublequote}}] applies proof method
|
26870
|
778 |
\isa{m} as if in terminal position. Basically, this simulates a
|
26902
|
779 |
multi-step tactic script for \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, but may be given
|
26870
|
780 |
anywhere within the proof body.
|
|
781 |
|
26895
|
782 |
No facts are passed to \isa{m} here. Furthermore, the static
|
26902
|
783 |
context is that of the enclosing goal (as for actual \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}). Thus the proof method may not refer to any assumptions
|
26870
|
784 |
introduced in the current body, for example.
|
|
785 |
|
26902
|
786 |
\item [\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}}] completes a proof script, provided that
|
26870
|
787 |
the current goal state is solved completely. Note that actual
|
26902
|
788 |
structured proof commands (e.g.\ ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}'' or \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}}) may be used to conclude proof scripts as well.
|
26870
|
789 |
|
26902
|
790 |
\item [\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}~\isa{n} and \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}~\isa{n}] shuffle the list of pending goals: \hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}} puts off
|
26870
|
791 |
sub-goal \isa{n} to the end of the list (\isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}} by
|
26902
|
792 |
default), while \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}} brings sub-goal \isa{n} to the
|
26870
|
793 |
front.
|
|
794 |
|
26902
|
795 |
\item [\hyperlink{command.back}{\mbox{\isa{\isacommand{back}}}}] does back-tracking over the result
|
26870
|
796 |
sequence of the latest proof command. Basically, any proof command
|
|
797 |
may return multiple results.
|
|
798 |
|
|
799 |
\end{descr}
|
|
800 |
|
|
801 |
Any proper Isar proof method may be used with tactic script commands
|
26902
|
802 |
such as \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}. A few additional emulations of actual
|
26870
|
803 |
tactics are provided as well; these would be never used in actual
|
|
804 |
structured proofs, of course.%
|
|
805 |
\end{isamarkuptext}%
|
|
806 |
\isamarkuptrue%
|
|
807 |
%
|
|
808 |
\isamarkupsection{Omitting proofs%
|
|
809 |
}
|
|
810 |
\isamarkuptrue%
|
|
811 |
%
|
|
812 |
\begin{isamarkuptext}%
|
|
813 |
\begin{matharray}{rcl}
|
26902
|
814 |
\indexdef{}{command}{oops}\hypertarget{command.oops}{\hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}} & : & \isartrans{proof}{theory} \\
|
26870
|
815 |
\end{matharray}
|
|
816 |
|
26902
|
817 |
The \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} command discontinues the current proof
|
26870
|
818 |
attempt, while considering the partial proof text as properly
|
|
819 |
processed. This is conceptually quite different from ``faking''
|
26902
|
820 |
actual proofs via \indexref{}{command}{sorry}\hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} (see
|
|
821 |
\secref{sec:proof-steps}): \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not observe the
|
26870
|
822 |
proof structure at all, but goes back right to the theory level.
|
26902
|
823 |
Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem
|
26870
|
824 |
--- there is no intended claim to be able to complete the proof
|
|
825 |
anyhow.
|
|
826 |
|
26902
|
827 |
A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
|
26870
|
828 |
\emph{within} the system itself, in conjunction with the document
|
|
829 |
preparation tools of Isabelle described in \cite{isabelle-sys}.
|
|
830 |
Thus partial or even wrong proof attempts can be discussed in a
|
|
831 |
logically sound manner. Note that the Isabelle {\LaTeX} macros can
|
|
832 |
be easily adapted to print something like ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' instead of
|
26902
|
833 |
the keyword ``\hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}''.
|
26870
|
834 |
|
26902
|
835 |
\medskip The \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} command is undo-able, unlike
|
|
836 |
\indexref{}{command}{kill}\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} (see \secref{sec:history}). The effect is to
|
26870
|
837 |
get back to the theory just before the opening of the proof.%
|
|
838 |
\end{isamarkuptext}%
|
|
839 |
\isamarkuptrue%
|
|
840 |
%
|
|
841 |
\isamarkupsection{Generalized elimination \label{sec:obtain}%
|
|
842 |
}
|
|
843 |
\isamarkuptrue%
|
|
844 |
%
|
|
845 |
\begin{isamarkuptext}%
|
|
846 |
\begin{matharray}{rcl}
|
26902
|
847 |
\indexdef{}{command}{obtain}\hypertarget{command.obtain}{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}} & : & \isartrans{proof(state)}{proof(prove)} \\
|
|
848 |
\indexdef{}{command}{guess}\hypertarget{command.guess}{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(state)}{proof(prove)} \\
|
26870
|
849 |
\end{matharray}
|
|
850 |
|
|
851 |
Generalized elimination means that additional elements with certain
|
|
852 |
properties may be introduced in the current context, by virtue of a
|
|
853 |
locally proven ``soundness statement''. Technically speaking, the
|
26902
|
854 |
\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} language element is like a declaration of
|
|
855 |
\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}} and \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} (see also see
|
26870
|
856 |
\secref{sec:proof-context}), together with a soundness proof of its
|
|
857 |
additional claim. According to the nature of existential reasoning,
|
|
858 |
assumptions get eliminated from any result exported from the context
|
|
859 |
later, provided that the corresponding parameters do \emph{not}
|
|
860 |
occur in the conclusion.
|
|
861 |
|
|
862 |
\begin{rail}
|
|
863 |
'obtain' parname? (vars + 'and') 'where' (props + 'and')
|
|
864 |
;
|
|
865 |
'guess' (vars + 'and')
|
|
866 |
;
|
|
867 |
\end{rail}
|
|
868 |
|
26902
|
869 |
The derived Isar command \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} is defined as follows
|
26870
|
870 |
(where \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k{\isachardoublequote}} shall refer to (optional)
|
|
871 |
facts indicated for forward chaining).
|
|
872 |
\begin{matharray}{l}
|
26902
|
873 |
\isa{{\isachardoublequote}{\isasymlangle}using\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k{\isasymrangle}{\isachardoublequote}}~~\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ \ {\isasymlangle}proof{\isasymrangle}\ {\isasymequiv}{\isachardoublequote}} \\[1ex]
|
|
874 |
\quad \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}{\isasymAnd}thesis{\isachardot}\ {\isacharparenleft}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isacharparenright}\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
|
|
875 |
\quad \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{succeed} \\
|
|
876 |
\qquad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{thesis} \\
|
|
877 |
\qquad \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}that\ {\isacharbrackleft}Pure{\isachardot}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
|
|
878 |
\qquad \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{thesis} \\
|
|
879 |
\quad\qquad \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{{\isacharminus}} \\
|
|
880 |
\quad\qquad \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k\ \ {\isasymlangle}proof{\isasymrangle}{\isachardoublequote}} \\
|
|
881 |
\quad \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} \\
|
|
882 |
\quad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} \\
|
26870
|
883 |
\end{matharray}
|
|
884 |
|
|
885 |
Typically, the soundness proof is relatively straight-forward, often
|
26902
|
886 |
just by canonical automated tools such as ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{simp}'' or ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{blast}''. Accordingly, the
|
26870
|
887 |
``\isa{that}'' reduction above is declared as simplification and
|
|
888 |
introduction rule.
|
|
889 |
|
26902
|
890 |
In a sense, \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} represents at the level of Isar
|
26870
|
891 |
proofs what would be meta-logical existential quantifiers and
|
|
892 |
conjunctions. This concept has a broad range of useful
|
|
893 |
applications, ranging from plain elimination (or introduction) of
|
|
894 |
object-level existential and conjunctions, to elimination over
|
|
895 |
results of symbolic evaluation of recursive definitions, for
|
26902
|
896 |
example. Also note that \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} without parameters acts
|
|
897 |
much like \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, where the result is treated as a
|
26870
|
898 |
genuine assumption.
|
|
899 |
|
|
900 |
An alternative name to be used instead of ``\isa{that}'' above may
|
|
901 |
be given in parentheses.
|
|
902 |
|
26902
|
903 |
\medskip The improper variant \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}} is similar to
|
|
904 |
\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}, but derives the obtained statement from the
|
26870
|
905 |
course of reasoning! The proof starts with a fixed goal \isa{thesis}. The subsequent proof may refine this to anything of the
|
|
906 |
form like \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}}, but must not introduce new subgoals. The
|
|
907 |
final goal state is then used as reduction rule for the obtain
|
|
908 |
scheme described above. Obtained parameters \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} are marked as internal by default, which prevents the
|
|
909 |
proof context from being polluted by ad-hoc variables. The variable
|
26902
|
910 |
names and type constraints given as arguments for \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}
|
26870
|
911 |
specify a prefix of obtained parameters explicitly in the text.
|
|
912 |
|
26902
|
913 |
It is important to note that the facts introduced by \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} and \hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}} may not be polymorphic: any
|
26870
|
914 |
type-variables occurring here are fixed in the present context!%
|
|
915 |
\end{isamarkuptext}%
|
|
916 |
\isamarkuptrue%
|
|
917 |
%
|
|
918 |
\isamarkupsection{Calculational reasoning \label{sec:calculation}%
|
|
919 |
}
|
|
920 |
\isamarkuptrue%
|
|
921 |
%
|
|
922 |
\begin{isamarkuptext}%
|
|
923 |
\begin{matharray}{rcl}
|
26902
|
924 |
\indexdef{}{command}{also}\hypertarget{command.also}{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
925 |
\indexdef{}{command}{finally}\hypertarget{command.finally}{\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
926 |
\indexdef{}{command}{moreover}\hypertarget{command.moreover}{\hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
927 |
\indexdef{}{command}{ultimately}\hypertarget{command.ultimately}{\hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}}} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
928 |
\indexdef{}{command}{print\_trans\_rules}\hypertarget{command.print_trans_rules}{\hyperlink{command.print_trans_rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
929 |
\hyperlink{attribute.trans}{\mbox{\isa{trans}}} & : & \isaratt \\
|
|
930 |
\hyperlink{attribute.sym}{\mbox{\isa{sym}}} & : & \isaratt \\
|
|
931 |
\hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} & : & \isaratt \\
|
26870
|
932 |
\end{matharray}
|
|
933 |
|
|
934 |
Calculational proof is forward reasoning with implicit application
|
|
935 |
of transitivity rules (such those of \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymle}{\isachardoublequote}},
|
|
936 |
\isa{{\isachardoublequote}{\isacharless}{\isachardoublequote}}). Isabelle/Isar maintains an auxiliary fact register
|
26902
|
937 |
\indexref{}{fact}{calculation}\hyperlink{fact.calculation}{\mbox{\isa{calculation}}} for accumulating results obtained by
|
|
938 |
transitivity composed with the current result. Command \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} updates \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} involving \hyperlink{fact.this}{\mbox{\isa{this}}}, while
|
|
939 |
\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} exhibits the final \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by
|
26870
|
940 |
forward chaining towards the next goal statement. Both commands
|
|
941 |
require valid current facts, i.e.\ may occur only after commands
|
26902
|
942 |
that produce theorems such as \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}, or some finished proof of \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} etc. The \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} and \hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}}
|
|
943 |
commands are similar to \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}},
|
|
944 |
but only collect further results in \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} without
|
26870
|
945 |
applying any rules yet.
|
|
946 |
|
|
947 |
Also note that the implicit term abbreviation ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' has
|
|
948 |
its canonical application with calculational proofs. It refers to
|
|
949 |
the argument of the preceding statement. (The argument of a curried
|
|
950 |
infix expression happens to be its right-hand side.)
|
|
951 |
|
|
952 |
Isabelle/Isar calculations are implicitly subject to block structure
|
|
953 |
in the sense that new threads of calculational reasoning are
|
|
954 |
commenced for any new block (as opened by a local goal, for
|
|
955 |
example). This means that, apart from being able to nest
|
|
956 |
calculations, there is no separate \emph{begin-calculation} command
|
|
957 |
required.
|
|
958 |
|
|
959 |
\medskip The Isar calculation proof commands may be defined as
|
|
960 |
follows:\footnote{We suppress internal bookkeeping such as proper
|
|
961 |
handling of block-structure.}
|
|
962 |
|
|
963 |
\begin{matharray}{rcl}
|
26902
|
964 |
\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
|
|
965 |
\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\[0.5ex]
|
|
966 |
\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} & \equiv & \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{calculation} \\[0.5ex]
|
|
967 |
\hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
|
|
968 |
\hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}} & \equiv & \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{calculation} \\
|
26870
|
969 |
\end{matharray}
|
|
970 |
|
|
971 |
\begin{rail}
|
|
972 |
('also' | 'finally') ('(' thmrefs ')')?
|
|
973 |
;
|
|
974 |
'trans' (() | 'add' | 'del')
|
|
975 |
;
|
|
976 |
\end{rail}
|
|
977 |
|
|
978 |
\begin{descr}
|
|
979 |
|
26902
|
980 |
\item [\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}]
|
|
981 |
maintains the auxiliary \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} register as follows.
|
|
982 |
The first occurrence of \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} in some calculational
|
|
983 |
thread initializes \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by \hyperlink{fact.this}{\mbox{\isa{this}}}. Any
|
|
984 |
subsequent \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} on the same level of block-structure
|
|
985 |
updates \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by some transitivity rule applied to
|
|
986 |
\hyperlink{fact.calculation}{\mbox{\isa{calculation}}} and \hyperlink{fact.this}{\mbox{\isa{this}}} (in that order). Transitivity
|
26870
|
987 |
rules are picked from the current context, unless alternative rules
|
|
988 |
are given as explicit arguments.
|
|
989 |
|
26902
|
990 |
\item [\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}]
|
|
991 |
maintaining \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} in the same way as \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}, and concludes the current calculational thread. The final
|
26870
|
992 |
result is exhibited as fact for forward chaining towards the next
|
26902
|
993 |
goal. Basically, \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} just abbreviates \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\hyperlink{fact.calculation}{\mbox{\isa{calculation}}}. Typical idioms for
|
|
994 |
concluding calculational proofs are ``\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{{\isacharquery}thesis}~\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}'' and ``\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isasymphi}}~\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}''.
|
26870
|
995 |
|
26902
|
996 |
\item [\hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} and \hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}}] are
|
|
997 |
analogous to \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}, but collect
|
26870
|
998 |
results only, without applying rules.
|
|
999 |
|
26902
|
1000 |
\item [\hyperlink{command.print_trans_rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}}] prints the list of
|
|
1001 |
transitivity rules (for calculational commands \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and
|
|
1002 |
\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}) and symmetry rules (for the \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} operation and single step elimination patters) of the
|
26870
|
1003 |
current context.
|
|
1004 |
|
26902
|
1005 |
\item [\hyperlink{attribute.trans}{\mbox{\isa{trans}}}] declares theorems as transitivity rules.
|
26870
|
1006 |
|
26902
|
1007 |
\item [\hyperlink{attribute.sym}{\mbox{\isa{sym}}}] declares symmetry rules, as well as
|
|
1008 |
\hyperlink{attribute.Pure.elim}{\mbox{\isa{Pure{\isachardot}elim}}}\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}} rules.
|
26870
|
1009 |
|
26902
|
1010 |
\item [\hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}}] resolves a theorem with some rule
|
|
1011 |
declared as \hyperlink{attribute.sym}{\mbox{\isa{sym}}} in the current context. For example,
|
|
1012 |
``\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcolon}\ x\ {\isacharequal}\ y{\isachardoublequote}}'' produces a
|
26870
|
1013 |
swapped fact derived from that assumption.
|
|
1014 |
|
|
1015 |
In structured proof texts it is often more appropriate to use an
|
26902
|
1016 |
explicit single-step elimination proof, such as ``\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}}~\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}y\ {\isacharequal}\ x{\isachardoublequote}}~\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}''.
|
26870
|
1017 |
|
|
1018 |
\end{descr}%
|
|
1019 |
\end{isamarkuptext}%
|
|
1020 |
\isamarkuptrue%
|
|
1021 |
%
|
26869
|
1022 |
\isadelimtheory
|
|
1023 |
%
|
|
1024 |
\endisadelimtheory
|
|
1025 |
%
|
|
1026 |
\isatagtheory
|
|
1027 |
\isacommand{end}\isamarkupfalse%
|
|
1028 |
%
|
|
1029 |
\endisatagtheory
|
|
1030 |
{\isafoldtheory}%
|
|
1031 |
%
|
|
1032 |
\isadelimtheory
|
|
1033 |
%
|
|
1034 |
\endisadelimtheory
|
|
1035 |
\isanewline
|
|
1036 |
\end{isabellebody}%
|
|
1037 |
%%% Local Variables:
|
|
1038 |
%%% mode: latex
|
|
1039 |
%%% TeX-master: "root"
|
|
1040 |
%%% End:
|