26782
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Generic}%
|
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
\isanewline
|
|
7 |
\isanewline
|
|
8 |
%
|
|
9 |
\endisadelimtheory
|
|
10 |
%
|
|
11 |
\isatagtheory
|
|
12 |
\isacommand{theory}\isamarkupfalse%
|
|
13 |
\ Generic\isanewline
|
|
14 |
\isakeyword{imports}\ CPure\isanewline
|
|
15 |
\isakeyword{begin}%
|
|
16 |
\endisatagtheory
|
|
17 |
{\isafoldtheory}%
|
|
18 |
%
|
|
19 |
\isadelimtheory
|
|
20 |
%
|
|
21 |
\endisadelimtheory
|
|
22 |
%
|
|
23 |
\isamarkupchapter{Generic tools and packages \label{ch:gen-tools}%
|
|
24 |
}
|
|
25 |
\isamarkuptrue%
|
|
26 |
%
|
|
27 |
\isamarkupsection{Specification commands%
|
|
28 |
}
|
|
29 |
\isamarkuptrue%
|
|
30 |
%
|
|
31 |
\isamarkupsubsection{Derived specifications%
|
|
32 |
}
|
|
33 |
\isamarkuptrue%
|
|
34 |
%
|
|
35 |
\begin{isamarkuptext}%
|
|
36 |
\begin{matharray}{rcll}
|
|
37 |
\indexdef{}{command}{axiomatization}\mbox{\isa{\isacommand{axiomatization}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
|
|
38 |
\indexdef{}{command}{definition}\mbox{\isa{\isacommand{definition}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
39 |
\indexdef{}{attribute}{defn}\mbox{\isa{defn}} & : & \isaratt \\
|
|
40 |
\indexdef{}{command}{abbreviation}\mbox{\isa{\isacommand{abbreviation}}} & : & \isarkeep{local{\dsh}theory} \\
|
26842
|
41 |
\indexdef{}{command}{print-abbrevs}\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
26782
|
42 |
\indexdef{}{command}{notation}\mbox{\isa{\isacommand{notation}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
43 |
\indexdef{}{command}{no-notation}\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
44 |
\end{matharray}
|
|
45 |
|
|
46 |
These specification mechanisms provide a slightly more abstract view
|
|
47 |
than the underlying primitives of \mbox{\isa{\isacommand{consts}}}, \mbox{\isa{\isacommand{defs}}} (see \secref{sec:consts}), and \mbox{\isa{\isacommand{axioms}}} (see
|
|
48 |
\secref{sec:axms-thms}). In particular, type-inference is commonly
|
|
49 |
available, and result names need not be given.
|
|
50 |
|
|
51 |
\begin{rail}
|
|
52 |
'axiomatization' target? fixes? ('where' specs)?
|
|
53 |
;
|
|
54 |
'definition' target? (decl 'where')? thmdecl? prop
|
|
55 |
;
|
|
56 |
'abbreviation' target? mode? (decl 'where')? prop
|
|
57 |
;
|
|
58 |
('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
|
|
59 |
;
|
|
60 |
|
|
61 |
fixes: ((name ('::' type)? mixfix? | vars) + 'and')
|
|
62 |
;
|
|
63 |
specs: (thmdecl? props + 'and')
|
|
64 |
;
|
|
65 |
decl: name ('::' type)? mixfix?
|
|
66 |
;
|
|
67 |
\end{rail}
|
|
68 |
|
|
69 |
\begin{descr}
|
|
70 |
|
26842
|
71 |
\item [\mbox{\isa{\isacommand{axiomatization}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] introduces several constants
|
26782
|
72 |
simultaneously and states axiomatic properties for these. The
|
|
73 |
constants are marked as being specified once and for all, which
|
|
74 |
prevents additional specifications being issued later on.
|
|
75 |
|
|
76 |
Note that axiomatic specifications are only appropriate when
|
|
77 |
declaring a new logical system. Normal applications should only use
|
|
78 |
definitional mechanisms!
|
|
79 |
|
26842
|
80 |
\item [\mbox{\isa{\isacommand{definition}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] produces an
|
|
81 |
internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification
|
26782
|
82 |
given as \isa{eq}, which is then turned into a proven fact. The
|
|
83 |
given proposition may deviate from internal meta-level equality
|
|
84 |
according to the rewrite rules declared as \mbox{\isa{defn}} by the
|
26842
|
85 |
object-logic. This usually covers object-level equality \isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}} and equivalence \isa{{\isachardoublequote}A\ {\isasymleftrightarrow}\ B{\isachardoublequote}}. End-users normally need not
|
26782
|
86 |
change the \mbox{\isa{defn}} setup.
|
|
87 |
|
|
88 |
Definitions may be presented with explicit arguments on the LHS, as
|
26842
|
89 |
well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of
|
|
90 |
\isa{{\isachardoublequote}f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} and \isa{{\isachardoublequote}y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u{\isachardoublequote}} instead of an
|
|
91 |
unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}.
|
26782
|
92 |
|
26842
|
93 |
\item [\mbox{\isa{\isacommand{abbreviation}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] introduces
|
26782
|
94 |
a syntactic constant which is associated with a certain term
|
|
95 |
according to the meta-level equality \isa{eq}.
|
|
96 |
|
|
97 |
Abbreviations participate in the usual type-inference process, but
|
|
98 |
are expanded before the logic ever sees them. Pretty printing of
|
|
99 |
terms involves higher-order rewriting with rules stemming from
|
|
100 |
reverted abbreviations. This needs some care to avoid overlapping
|
|
101 |
or looping syntactic replacements!
|
|
102 |
|
|
103 |
The optional \isa{mode} specification restricts output to a
|
|
104 |
particular print mode; using ``\isa{input}'' here achieves the
|
|
105 |
effect of one-way abbreviations. The mode may also include an
|
|
106 |
``\mbox{\isa{\isakeyword{output}}}'' qualifier that affects the concrete syntax
|
|
107 |
declared for abbreviations, cf.\ \mbox{\isa{\isacommand{syntax}}} in
|
|
108 |
\secref{sec:syn-trans}.
|
|
109 |
|
|
110 |
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}] prints all constant abbreviations
|
|
111 |
of the current context.
|
|
112 |
|
26842
|
113 |
\item [\mbox{\isa{\isacommand{notation}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix
|
26782
|
114 |
syntax with an existing constant or fixed variable. This is a
|
|
115 |
robust interface to the underlying \mbox{\isa{\isacommand{syntax}}} primitive
|
|
116 |
(\secref{sec:syn-trans}). Type declaration and internal syntactic
|
|
117 |
representation of the given entity is retrieved from the context.
|
|
118 |
|
|
119 |
\item [\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}] is similar to \mbox{\isa{\isacommand{notation}}}, but removes the specified syntax annotation from the
|
|
120 |
present context.
|
|
121 |
|
|
122 |
\end{descr}
|
|
123 |
|
|
124 |
All of these specifications support local theory targets (cf.\
|
|
125 |
\secref{sec:target}).%
|
|
126 |
\end{isamarkuptext}%
|
|
127 |
\isamarkuptrue%
|
|
128 |
%
|
|
129 |
\isamarkupsubsection{Generic declarations%
|
|
130 |
}
|
|
131 |
\isamarkuptrue%
|
|
132 |
%
|
|
133 |
\begin{isamarkuptext}%
|
|
134 |
Arbitrary operations on the background context may be wrapped-up as
|
|
135 |
generic declaration elements. Since the underlying concept of local
|
|
136 |
theories may be subject to later re-interpretation, there is an
|
|
137 |
additional dependency on a morphism that tells the difference of the
|
|
138 |
original declaration context wrt.\ the application context
|
|
139 |
encountered later on. A fact declaration is an important special
|
|
140 |
case: it consists of a theorem which is applied to the context by
|
|
141 |
means of an attribute.
|
|
142 |
|
|
143 |
\begin{matharray}{rcl}
|
|
144 |
\indexdef{}{command}{declaration}\mbox{\isa{\isacommand{declaration}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
145 |
\indexdef{}{command}{declare}\mbox{\isa{\isacommand{declare}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
146 |
\end{matharray}
|
|
147 |
|
|
148 |
\begin{rail}
|
|
149 |
'declaration' target? text
|
|
150 |
;
|
|
151 |
'declare' target? (thmrefs + 'and')
|
|
152 |
;
|
|
153 |
\end{rail}
|
|
154 |
|
|
155 |
\begin{descr}
|
|
156 |
|
|
157 |
\item [\mbox{\isa{\isacommand{declaration}}}~\isa{d}] adds the declaration
|
|
158 |
function \isa{d} of ML type \verb|declaration|, to the current
|
|
159 |
local theory under construction. In later application contexts, the
|
|
160 |
function is transformed according to the morphisms being involved in
|
|
161 |
the interpretation hierarchy.
|
|
162 |
|
|
163 |
\item [\mbox{\isa{\isacommand{declare}}}~\isa{thms}] declares theorems to the
|
|
164 |
current local theory context. No theorem binding is involved here,
|
|
165 |
unlike \mbox{\isa{\isacommand{theorems}}} or \mbox{\isa{\isacommand{lemmas}}} (cf.\
|
|
166 |
\secref{sec:axms-thms}), so \mbox{\isa{\isacommand{declare}}} only has the effect
|
|
167 |
of applying attributes as included in the theorem specification.
|
|
168 |
|
|
169 |
\end{descr}%
|
|
170 |
\end{isamarkuptext}%
|
|
171 |
\isamarkuptrue%
|
|
172 |
%
|
|
173 |
\isamarkupsubsection{Local theory targets \label{sec:target}%
|
|
174 |
}
|
|
175 |
\isamarkuptrue%
|
|
176 |
%
|
|
177 |
\begin{isamarkuptext}%
|
|
178 |
A local theory target is a context managed separately within the
|
|
179 |
enclosing theory. Contexts may introduce parameters (fixed
|
|
180 |
variables) and assumptions (hypotheses). Definitions and theorems
|
|
181 |
depending on the context may be added incrementally later on. Named
|
|
182 |
contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
|
26842
|
183 |
(cf.\ \secref{sec:class}); the name ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' signifies the
|
26782
|
184 |
global theory context.
|
|
185 |
|
|
186 |
\begin{matharray}{rcll}
|
|
187 |
\indexdef{}{command}{context}\mbox{\isa{\isacommand{context}}} & : & \isartrans{theory}{local{\dsh}theory} \\
|
|
188 |
\indexdef{}{command}{end}\mbox{\isa{\isacommand{end}}} & : & \isartrans{local{\dsh}theory}{theory} \\
|
|
189 |
\end{matharray}
|
|
190 |
|
|
191 |
\indexouternonterm{target}
|
|
192 |
\begin{rail}
|
|
193 |
'context' name 'begin'
|
|
194 |
;
|
|
195 |
|
|
196 |
target: '(' 'in' name ')'
|
|
197 |
;
|
|
198 |
\end{rail}
|
|
199 |
|
|
200 |
\begin{descr}
|
|
201 |
|
26842
|
202 |
\item [\mbox{\isa{\isacommand{context}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}}] recommences an
|
26782
|
203 |
existing locale or class context \isa{c}. Note that locale and
|
|
204 |
class definitions allow to include the \indexref{}{keyword}{begin}\mbox{\isa{\isakeyword{begin}}}
|
|
205 |
keyword as well, in order to continue the local theory immediately
|
|
206 |
after the initial specification.
|
|
207 |
|
|
208 |
\item [\mbox{\isa{\isacommand{end}}}] concludes the current local theory and
|
|
209 |
continues the enclosing global theory. Note that a non-local
|
|
210 |
\mbox{\isa{\isacommand{end}}} has a different meaning: it concludes the theory
|
|
211 |
itself (\secref{sec:begin-thy}).
|
|
212 |
|
26842
|
213 |
\item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}}] given after any local theory command
|
|
214 |
specifies an immediate target, e.g.\ ``\mbox{\isa{\isacommand{definition}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\mbox{\isa{\isacommand{theorem}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''. This works both in a local or
|
26782
|
215 |
global theory context; the current target context will be suspended
|
26842
|
216 |
for this command only. Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will
|
26788
|
217 |
always produce a global result independently of the current target
|
|
218 |
context.
|
26782
|
219 |
|
|
220 |
\end{descr}
|
|
221 |
|
|
222 |
The exact meaning of results produced within a local theory context
|
|
223 |
depends on the underlying target infrastructure (locale, type class
|
|
224 |
etc.). The general idea is as follows, considering a context named
|
26842
|
225 |
\isa{c} with parameter \isa{x} and assumption \isa{{\isachardoublequote}A{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}}.
|
26782
|
226 |
|
|
227 |
Definitions are exported by introducing a global version with
|
|
228 |
additional arguments; a syntactic abbreviation links the long form
|
|
229 |
with the abstract version of the target context. For example,
|
26842
|
230 |
\isa{{\isachardoublequote}a\ {\isasymequiv}\ t{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a\ {\isacharquery}x\ {\isasymequiv}\ t{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}} at the theory
|
|
231 |
level (for arbitrary \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}), together with a local
|
|
232 |
abbreviation \isa{{\isachardoublequote}c\ {\isasymequiv}\ c{\isachardot}a\ x{\isachardoublequote}} in the target context (for the
|
26782
|
233 |
fixed parameter \isa{x}).
|
|
234 |
|
|
235 |
Theorems are exported by discharging the assumptions and
|
26842
|
236 |
generalizing the parameters of the context. For example, \isa{{\isachardoublequote}a{\isacharcolon}\ B{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a{\isacharcolon}\ A{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}\ {\isasymLongrightarrow}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}}, again for arbitrary
|
|
237 |
\isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}.%
|
26782
|
238 |
\end{isamarkuptext}%
|
|
239 |
\isamarkuptrue%
|
|
240 |
%
|
|
241 |
\isamarkupsubsection{Locales \label{sec:locale}%
|
|
242 |
}
|
|
243 |
\isamarkuptrue%
|
|
244 |
%
|
|
245 |
\begin{isamarkuptext}%
|
|
246 |
Locales are named local contexts, consisting of a list of
|
|
247 |
declaration elements that are modeled after the Isar proof context
|
|
248 |
commands (cf.\ \secref{sec:proof-context}).%
|
|
249 |
\end{isamarkuptext}%
|
|
250 |
\isamarkuptrue%
|
|
251 |
%
|
|
252 |
\isamarkupsubsubsection{Locale specifications%
|
|
253 |
}
|
|
254 |
\isamarkuptrue%
|
|
255 |
%
|
|
256 |
\begin{isamarkuptext}%
|
|
257 |
\begin{matharray}{rcl}
|
|
258 |
\indexdef{}{command}{locale}\mbox{\isa{\isacommand{locale}}} & : & \isartrans{theory}{local{\dsh}theory} \\
|
26842
|
259 |
\indexdef{}{command}{print-locale}\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
260 |
\indexdef{}{command}{print-locales}\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
26782
|
261 |
\indexdef{}{method}{intro-locales}\mbox{\isa{intro{\isacharunderscore}locales}} & : & \isarmeth \\
|
|
262 |
\indexdef{}{method}{unfold-locales}\mbox{\isa{unfold{\isacharunderscore}locales}} & : & \isarmeth \\
|
|
263 |
\end{matharray}
|
|
264 |
|
|
265 |
\indexouternonterm{contextexpr}\indexouternonterm{contextelem}
|
|
266 |
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
|
|
267 |
\indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
|
|
268 |
\begin{rail}
|
|
269 |
'locale' ('(open)')? name ('=' localeexpr)? 'begin'?
|
|
270 |
;
|
|
271 |
'print\_locale' '!'? localeexpr
|
|
272 |
;
|
|
273 |
localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
|
|
274 |
;
|
|
275 |
|
|
276 |
contextexpr: nameref | '(' contextexpr ')' |
|
|
277 |
(contextexpr (name mixfix? +)) | (contextexpr + '+')
|
|
278 |
;
|
|
279 |
contextelem: fixes | constrains | assumes | defines | notes
|
|
280 |
;
|
|
281 |
fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
|
|
282 |
;
|
|
283 |
constrains: 'constrains' (name '::' type + 'and')
|
|
284 |
;
|
|
285 |
assumes: 'assumes' (thmdecl? props + 'and')
|
|
286 |
;
|
|
287 |
defines: 'defines' (thmdecl? prop proppat? + 'and')
|
|
288 |
;
|
|
289 |
notes: 'notes' (thmdef? thmrefs + 'and')
|
|
290 |
;
|
|
291 |
includes: 'includes' contextexpr
|
|
292 |
;
|
|
293 |
\end{rail}
|
|
294 |
|
|
295 |
\begin{descr}
|
|
296 |
|
26842
|
297 |
\item [\mbox{\isa{\isacommand{locale}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}}] defines a
|
26782
|
298 |
new locale \isa{loc} as a context consisting of a certain view of
|
|
299 |
existing locales (\isa{import}) plus some additional elements
|
|
300 |
(\isa{body}). Both \isa{import} and \isa{body} are optional;
|
|
301 |
the degenerate form \mbox{\isa{\isacommand{locale}}}~\isa{loc} defines an empty
|
|
302 |
locale, which may still be useful to collect declarations of facts
|
|
303 |
later on. Type-inference on locale expressions automatically takes
|
|
304 |
care of the most general typing that the combined context elements
|
|
305 |
may acquire.
|
|
306 |
|
|
307 |
The \isa{import} consists of a structured context expression,
|
|
308 |
consisting of references to existing locales, renamed contexts, or
|
26842
|
309 |
merged contexts. Renaming uses positional notation: \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed
|
|
310 |
parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that
|
26782
|
311 |
position. Renaming by default deletes concrete syntax, but new
|
|
312 |
syntax may by specified with a mixfix annotation. An exeption of
|
26842
|
313 |
this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it
|
26782
|
314 |
be changed. Merging proceeds from left-to-right, suppressing any
|
|
315 |
duplicates stemming from different paths through the import
|
|
316 |
hierarchy.
|
|
317 |
|
|
318 |
The \isa{body} consists of basic context elements, further context
|
|
319 |
expressions may be included as well.
|
|
320 |
|
|
321 |
\begin{descr}
|
|
322 |
|
26842
|
323 |
\item [\mbox{\isa{\isakeyword{fixes}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares a local
|
26782
|
324 |
parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both
|
26842
|
325 |
are optional). The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced
|
26782
|
326 |
implicitly in this context.
|
|
327 |
|
26842
|
328 |
\item [\mbox{\isa{\isakeyword{constrains}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}] introduces a type
|
26782
|
329 |
constraint \isa{{\isasymtau}} on the local parameter \isa{x}.
|
|
330 |
|
26842
|
331 |
\item [\mbox{\isa{\isakeyword{assumes}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}]
|
26782
|
332 |
introduces local premises, similar to \mbox{\isa{\isacommand{assume}}} within a
|
|
333 |
proof (cf.\ \secref{sec:proof-context}).
|
|
334 |
|
26842
|
335 |
\item [\mbox{\isa{\isakeyword{defines}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}}] defines a previously
|
26788
|
336 |
declared parameter. This is similar to \mbox{\isa{\isacommand{def}}} within a
|
|
337 |
proof (cf.\ \secref{sec:proof-context}), but \mbox{\isa{\isakeyword{defines}}}
|
26782
|
338 |
takes an equational proposition instead of variable-term pair. The
|
|
339 |
left-hand side of the equation may have additional arguments, e.g.\
|
26842
|
340 |
``\mbox{\isa{\isakeyword{defines}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''.
|
26782
|
341 |
|
26842
|
342 |
\item [\mbox{\isa{\isakeyword{notes}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
|
26782
|
343 |
reconsiders facts within a local context. Most notably, this may
|
|
344 |
include arbitrary declarations in any attribute specifications
|
|
345 |
included here, e.g.\ a local \mbox{\isa{simp}} rule.
|
|
346 |
|
26788
|
347 |
\item [\mbox{\isa{\isakeyword{includes}}}~\isa{c}] copies the specified context
|
26782
|
348 |
in a statically scoped manner. Only available in the long goal
|
|
349 |
format of \secref{sec:goals}.
|
|
350 |
|
|
351 |
In contrast, the initial \isa{import} specification of a locale
|
|
352 |
expression maintains a dynamic relation to the locales being
|
|
353 |
referenced (benefiting from any later fact declarations in the
|
|
354 |
obvious manner).
|
|
355 |
|
|
356 |
\end{descr}
|
|
357 |
|
26842
|
358 |
Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given
|
26788
|
359 |
in the syntax of \mbox{\isa{\isakeyword{assumes}}} and \mbox{\isa{\isakeyword{defines}}} above
|
26782
|
360 |
are illegal in locale definitions. In the long goal format of
|
|
361 |
\secref{sec:goals}, term bindings may be included as expected,
|
|
362 |
though.
|
|
363 |
|
|
364 |
\medskip By default, locale specifications are ``closed up'' by
|
|
365 |
turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
|
|
366 |
(modulo local definitions). The predicate statement covers only the
|
|
367 |
newly specified assumptions, omitting the content of included locale
|
|
368 |
expressions. The full cumulative view is only provided on export,
|
|
369 |
involving another predicate \isa{loc} that refers to the complete
|
|
370 |
specification text.
|
|
371 |
|
|
372 |
In any case, the predicate arguments are those locale parameters
|
|
373 |
that actually occur in the respective piece of text. Also note that
|
|
374 |
these predicates operate at the meta-level in theory, but the locale
|
|
375 |
packages attempts to internalize statements according to the
|
|
376 |
object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and
|
26842
|
377 |
\isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
|
26782
|
378 |
\secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
|
|
379 |
|
26842
|
380 |
The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option of a locale specification prevents both
|
26782
|
381 |
the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate
|
|
382 |
constructions. Predicates are also omitted for empty specification
|
|
383 |
texts.
|
|
384 |
|
26842
|
385 |
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the
|
26782
|
386 |
specified locale expression in a flattened form. The notable
|
|
387 |
special case \mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}~\isa{loc} just prints the
|
|
388 |
contents of the named locale, but keep in mind that type-inference
|
|
389 |
will normalize type variables according to the usual alphabetical
|
26788
|
390 |
order. The command omits \mbox{\isa{\isakeyword{notes}}} elements by default.
|
26842
|
391 |
Use \mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
|
26782
|
392 |
|
|
393 |
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}] prints the names of all locales
|
|
394 |
of the current theory.
|
|
395 |
|
|
396 |
\item [\mbox{\isa{intro{\isacharunderscore}locales}} and \mbox{\isa{unfold{\isacharunderscore}locales}}]
|
|
397 |
repeatedly expand all introduction rules of locale predicates of the
|
|
398 |
theory. While \mbox{\isa{intro{\isacharunderscore}locales}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to
|
|
399 |
assumptions, \mbox{\isa{unfold{\isacharunderscore}locales}} is more aggressive and applies
|
|
400 |
\isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale
|
|
401 |
specifications entailed by the context, both from target and
|
26788
|
402 |
\mbox{\isa{\isakeyword{includes}}} statements, and from interpretations (see
|
26782
|
403 |
below). New goals that are entailed by the current context are
|
|
404 |
discharged automatically.
|
|
405 |
|
|
406 |
\end{descr}%
|
|
407 |
\end{isamarkuptext}%
|
|
408 |
\isamarkuptrue%
|
|
409 |
%
|
|
410 |
\isamarkupsubsubsection{Interpretation of locales%
|
|
411 |
}
|
|
412 |
\isamarkuptrue%
|
|
413 |
%
|
|
414 |
\begin{isamarkuptext}%
|
|
415 |
Locale expressions (more precisely, \emph{context expressions}) may
|
|
416 |
be instantiated, and the instantiated facts added to the current
|
|
417 |
context. This requires a proof of the instantiated specification
|
|
418 |
and is called \emph{locale interpretation}. Interpretation is
|
26788
|
419 |
possible in theories and locales (command \mbox{\isa{\isacommand{interpretation}}}) and also within a proof body (command \mbox{\isa{\isacommand{interpret}}}).
|
26782
|
420 |
|
|
421 |
\begin{matharray}{rcl}
|
|
422 |
\indexdef{}{command}{interpretation}\mbox{\isa{\isacommand{interpretation}}} & : & \isartrans{theory}{proof(prove)} \\
|
|
423 |
\indexdef{}{command}{interpret}\mbox{\isa{\isacommand{interpret}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
|
26842
|
424 |
\indexdef{}{command}{print-interps}\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
26782
|
425 |
\end{matharray}
|
|
426 |
|
|
427 |
\indexouternonterm{interp}
|
|
428 |
\begin{rail}
|
|
429 |
'interpretation' (interp | name ('<' | subseteq) contextexpr)
|
|
430 |
;
|
|
431 |
'interpret' interp
|
|
432 |
;
|
|
433 |
'print\_interps' '!'? name
|
|
434 |
;
|
|
435 |
instantiation: ('[' (inst+) ']')?
|
|
436 |
;
|
|
437 |
interp: thmdecl? \\ (contextexpr instantiation |
|
|
438 |
name instantiation 'where' (thmdecl? prop + 'and'))
|
|
439 |
;
|
|
440 |
\end{rail}
|
|
441 |
|
|
442 |
\begin{descr}
|
|
443 |
|
26842
|
444 |
\item [\mbox{\isa{\isacommand{interpretation}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
|
26782
|
445 |
|
|
446 |
The first form of \mbox{\isa{\isacommand{interpretation}}} interprets \isa{expr} in the theory. The instantiation is given as a list of terms
|
|
447 |
\isa{insts} and is positional. All parameters must receive an
|
|
448 |
instantiation term --- with the exception of defined parameters.
|
|
449 |
These are, if omitted, derived from the defining equation and other
|
|
450 |
instantiations. Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
|
|
451 |
|
|
452 |
The command generates proof obligations for the instantiated
|
|
453 |
specifications (assumes and defines elements). Once these are
|
|
454 |
discharged by the user, instantiated facts are added to the theory
|
|
455 |
in a post-processing phase.
|
|
456 |
|
|
457 |
Additional equations, which are unfolded in facts during
|
|
458 |
post-processing, may be given after the keyword \mbox{\isa{\isakeyword{where}}}.
|
|
459 |
This is useful for interpreting concepts introduced through
|
|
460 |
definition specification elements. The equations must be proved.
|
|
461 |
Note that if equations are present, the context expression is
|
|
462 |
restricted to a locale name.
|
|
463 |
|
|
464 |
The command is aware of interpretations already active in the
|
|
465 |
theory. No proof obligations are generated for those, neither is
|
|
466 |
post-processing applied to their facts. This avoids duplication of
|
|
467 |
interpreted facts, in particular. Note that, in the case of a
|
|
468 |
locale with import, parts of the interpretation may already be
|
|
469 |
active. The command will only generate proof obligations and
|
|
470 |
process facts for new parts.
|
|
471 |
|
|
472 |
The context expression may be preceded by a name and/or attributes.
|
|
473 |
These take effect in the post-processing of facts. The name is used
|
|
474 |
to prefix fact names, for example to avoid accidental hiding of
|
|
475 |
other facts. Attributes are applied after attributes of the
|
|
476 |
interpreted facts.
|
|
477 |
|
|
478 |
Adding facts to locales has the effect of adding interpreted facts
|
|
479 |
to the theory for all active interpretations also. That is,
|
|
480 |
interpretations dynamically participate in any facts added to
|
|
481 |
locales.
|
|
482 |
|
26842
|
483 |
\item [\mbox{\isa{\isacommand{interpretation}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}]
|
26782
|
484 |
|
|
485 |
This form of the command interprets \isa{expr} in the locale
|
|
486 |
\isa{name}. It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}. As in the
|
|
487 |
localized version of the theorem command, the proof is in the
|
|
488 |
context of \isa{name}. After the proof obligation has been
|
|
489 |
dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
|
|
490 |
context \isa{name} is subsequently entered. Note that, like
|
|
491 |
import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
|
|
492 |
Like facts of renamed context elements, facts obtained by
|
|
493 |
interpretation may be accessed by prefixing with the parameter
|
|
494 |
renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
|
|
495 |
|
|
496 |
Unlike interpretation in theories, instantiation is confined to the
|
|
497 |
renaming of parameters, which may be specified as part of the
|
|
498 |
context expression \isa{expr}. Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
|
|
499 |
|
|
500 |
Only specification fragments of \isa{expr} that are not already
|
|
501 |
part of \isa{name} (be it imported, derived or a derived fragment
|
|
502 |
of the import) are considered by interpretation. This enables
|
|
503 |
circular interpretations.
|
|
504 |
|
|
505 |
If interpretations of \isa{name} exist in the current theory, the
|
|
506 |
command adds interpretations for \isa{expr} as well, with the same
|
|
507 |
prefix and attributes, although only for fragments of \isa{expr}
|
|
508 |
that are not interpreted in the theory already.
|
|
509 |
|
26842
|
510 |
\item [\mbox{\isa{\isacommand{interpret}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
|
26782
|
511 |
interprets \isa{expr} in the proof context and is otherwise
|
26788
|
512 |
similar to interpretation in theories.
|
26782
|
513 |
|
|
514 |
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}~\isa{loc}] prints the
|
|
515 |
interpretations of a particular locale \isa{loc} that are active
|
|
516 |
in the current context, either theory or proof context. The
|
|
517 |
exclamation point argument triggers printing of \emph{witness}
|
|
518 |
theorems justifying interpretations. These are normally omitted
|
|
519 |
from the output.
|
|
520 |
|
|
521 |
\end{descr}
|
|
522 |
|
|
523 |
\begin{warn}
|
|
524 |
Since attributes are applied to interpreted theorems,
|
|
525 |
interpretation may modify the context of common proof tools, e.g.\
|
|
526 |
the Simplifier or Classical Reasoner. Since the behavior of such
|
|
527 |
automated reasoning tools is \emph{not} stable under
|
|
528 |
interpretation morphisms, manual declarations might have to be
|
|
529 |
issued.
|
|
530 |
\end{warn}
|
|
531 |
|
|
532 |
\begin{warn}
|
|
533 |
An interpretation in a theory may subsume previous
|
|
534 |
interpretations. This happens if the same specification fragment
|
|
535 |
is interpreted twice and the instantiation of the second
|
|
536 |
interpretation is more general than the interpretation of the
|
|
537 |
first. A warning is issued, since it is likely that these could
|
|
538 |
have been generalized in the first place. The locale package does
|
|
539 |
not attempt to remove subsumed interpretations.
|
|
540 |
\end{warn}%
|
|
541 |
\end{isamarkuptext}%
|
|
542 |
\isamarkuptrue%
|
|
543 |
%
|
|
544 |
\isamarkupsubsection{Classes \label{sec:class}%
|
|
545 |
}
|
|
546 |
\isamarkuptrue%
|
|
547 |
%
|
|
548 |
\begin{isamarkuptext}%
|
|
549 |
A class is a particular locale with \emph{exactly one} type variable
|
|
550 |
\isa{{\isasymalpha}}. Beyond the underlying locale, a corresponding type class
|
|
551 |
is established which is interpreted logically as axiomatic type
|
|
552 |
class \cite{Wenzel:1997:TPHOL} whose logical content are the
|
|
553 |
assumptions of the locale. Thus, classes provide the full
|
|
554 |
generality of locales combined with the commodity of type classes
|
|
555 |
(notably type-inference). See \cite{isabelle-classes} for a short
|
|
556 |
tutorial.
|
|
557 |
|
|
558 |
\begin{matharray}{rcl}
|
|
559 |
\indexdef{}{command}{class}\mbox{\isa{\isacommand{class}}} & : & \isartrans{theory}{local{\dsh}theory} \\
|
|
560 |
\indexdef{}{command}{instantiation}\mbox{\isa{\isacommand{instantiation}}} & : & \isartrans{theory}{local{\dsh}theory} \\
|
|
561 |
\indexdef{}{command}{instance}\mbox{\isa{\isacommand{instance}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
|
|
562 |
\indexdef{}{command}{subclass}\mbox{\isa{\isacommand{subclass}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
|
26842
|
563 |
\indexdef{}{command}{print-classes}\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
26782
|
564 |
\indexdef{}{method}{intro-classes}\mbox{\isa{intro{\isacharunderscore}classes}} & : & \isarmeth \\
|
|
565 |
\end{matharray}
|
|
566 |
|
|
567 |
\begin{rail}
|
|
568 |
'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
|
|
569 |
'begin'?
|
|
570 |
;
|
|
571 |
'instantiation' (nameref + 'and') '::' arity 'begin'
|
|
572 |
;
|
|
573 |
'instance'
|
|
574 |
;
|
|
575 |
'subclass' target? nameref
|
|
576 |
;
|
|
577 |
'print\_classes'
|
|
578 |
;
|
|
579 |
|
|
580 |
superclassexpr: nameref | (nameref '+' superclassexpr)
|
|
581 |
;
|
|
582 |
\end{rail}
|
|
583 |
|
|
584 |
\begin{descr}
|
|
585 |
|
26842
|
586 |
\item [\mbox{\isa{\isacommand{class}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}}] defines
|
26782
|
587 |
a new class \isa{c}, inheriting from \isa{superclasses}. This
|
|
588 |
introduces a locale \isa{c} with import of all locales \isa{superclasses}.
|
|
589 |
|
26788
|
590 |
Any \mbox{\isa{\isakeyword{fixes}}} in \isa{body} are lifted to the global
|
26842
|
591 |
theory level (\emph{class operations} \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} of class \isa{c}), mapping the local type parameter
|
|
592 |
\isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}.
|
26782
|
593 |
|
26788
|
594 |
Likewise, \mbox{\isa{\isakeyword{assumes}}} in \isa{body} are also lifted,
|
26842
|
595 |
mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its
|
|
596 |
corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The
|
26782
|
597 |
corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly
|
|
598 |
--- the \mbox{\isa{intro{\isacharunderscore}classes}} method takes care of the details of
|
|
599 |
class membership proofs.
|
|
600 |
|
26842
|
601 |
\item [\mbox{\isa{\isacommand{instantiation}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}{\isachardoublequote}}] opens a theory target (cf.\
|
|
602 |
\secref{sec:target}) which allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding to sort \isa{s} at the
|
|
603 |
particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}. A plain \mbox{\isa{\isacommand{instance}}} command
|
26782
|
604 |
in the target body poses a goal stating these type arities. The
|
|
605 |
target is concluded by an \indexref{}{command}{end}\mbox{\isa{\isacommand{end}}} command.
|
|
606 |
|
|
607 |
Note that a list of simultaneous type constructors may be given;
|
|
608 |
this corresponds nicely to mutual recursive type definitions, e.g.\
|
|
609 |
in Isabelle/HOL.
|
|
610 |
|
|
611 |
\item [\mbox{\isa{\isacommand{instance}}}] in an instantiation target body sets
|
|
612 |
up a goal stating the type arities claimed at the opening \mbox{\isa{\isacommand{instantiation}}}. The proof would usually proceed by \mbox{\isa{intro{\isacharunderscore}classes}}, and then establish the characteristic theorems of
|
|
613 |
the type classes involved. After finishing the proof, the
|
|
614 |
background theory will be augmented by the proven type arities.
|
|
615 |
|
|
616 |
\item [\mbox{\isa{\isacommand{subclass}}}~\isa{c}] in a class context for class
|
|
617 |
\isa{d} sets up a goal stating that class \isa{c} is logically
|
|
618 |
contained in class \isa{d}. After finishing the proof, class
|
|
619 |
\isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
|
|
620 |
|
|
621 |
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}] prints all classes in the current
|
|
622 |
theory.
|
|
623 |
|
|
624 |
\item [\mbox{\isa{intro{\isacharunderscore}classes}}] repeatedly expands all class
|
|
625 |
introduction rules of this theory. Note that this method usually
|
|
626 |
needs not be named explicitly, as it is already included in the
|
|
627 |
default proof step (e.g.\ of \mbox{\isa{\isacommand{proof}}}). In particular,
|
|
628 |
instantiation of trivial (syntactic) classes may be performed by a
|
|
629 |
single ``\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}'' proof step.
|
|
630 |
|
|
631 |
\end{descr}%
|
|
632 |
\end{isamarkuptext}%
|
|
633 |
\isamarkuptrue%
|
|
634 |
%
|
|
635 |
\isamarkupsubsubsection{The class target%
|
|
636 |
}
|
|
637 |
\isamarkuptrue%
|
|
638 |
%
|
|
639 |
\begin{isamarkuptext}%
|
|
640 |
%FIXME check
|
|
641 |
|
|
642 |
A named context may refer to a locale (cf.\ \secref{sec:target}).
|
|
643 |
If this locale is also a class \isa{c}, apart from the common
|
|
644 |
locale target behaviour the following happens.
|
|
645 |
|
|
646 |
\begin{itemize}
|
|
647 |
|
26842
|
648 |
\item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the
|
|
649 |
local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}}
|
|
650 |
are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}
|
|
651 |
referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.
|
26782
|
652 |
|
|
653 |
\item Local theorem bindings are lifted as are assumptions.
|
|
654 |
|
26842
|
655 |
\item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and
|
|
656 |
global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly. Type inference
|
26782
|
657 |
resolves ambiguities. In rare cases, manual type annotations are
|
|
658 |
needed.
|
|
659 |
|
|
660 |
\end{itemize}%
|
|
661 |
\end{isamarkuptext}%
|
|
662 |
\isamarkuptrue%
|
|
663 |
%
|
|
664 |
\isamarkupsubsection{Axiomatic type classes \label{sec:axclass}%
|
|
665 |
}
|
|
666 |
\isamarkuptrue%
|
|
667 |
%
|
|
668 |
\begin{isamarkuptext}%
|
|
669 |
\begin{matharray}{rcl}
|
|
670 |
\indexdef{}{command}{axclass}\mbox{\isa{\isacommand{axclass}}} & : & \isartrans{theory}{theory} \\
|
|
671 |
\indexdef{}{command}{instance}\mbox{\isa{\isacommand{instance}}} & : & \isartrans{theory}{proof(prove)} \\
|
|
672 |
\end{matharray}
|
|
673 |
|
|
674 |
Axiomatic type classes are Isabelle/Pure's primitive
|
|
675 |
\emph{definitional} interface to type classes. For practical
|
|
676 |
applications, you should consider using classes
|
|
677 |
(cf.~\secref{sec:classes}) which provide high level interface.
|
|
678 |
|
|
679 |
\begin{rail}
|
|
680 |
'axclass' classdecl (axmdecl prop +)
|
|
681 |
;
|
|
682 |
'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
|
|
683 |
;
|
|
684 |
\end{rail}
|
|
685 |
|
|
686 |
\begin{descr}
|
|
687 |
|
26842
|
688 |
\item [\mbox{\isa{\isacommand{axclass}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}}] defines an axiomatic type class as the intersection of
|
26782
|
689 |
existing classes, with additional axioms holding. Class axioms may
|
|
690 |
not contain more than one type variable. The class axioms (with
|
|
691 |
implicit sort constraints added) are bound to the given names.
|
|
692 |
Furthermore a class introduction rule is generated (being bound as
|
|
693 |
\isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \mbox{\isa{intro{\isacharunderscore}classes}} to support instantiation proofs of this class.
|
|
694 |
|
|
695 |
The ``class axioms'' are stored as theorems according to the given
|
26842
|
696 |
name specifications, adding \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix;
|
26782
|
697 |
the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
|
|
698 |
|
26842
|
699 |
\item [\mbox{\isa{\isacommand{instance}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and
|
|
700 |
\mbox{\isa{\isacommand{instance}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}]
|
26782
|
701 |
setup a goal stating a class relation or type arity. The proof
|
|
702 |
would usually proceed by \mbox{\isa{intro{\isacharunderscore}classes}}, and then establish
|
|
703 |
the characteristic theorems of the type classes involved. After
|
|
704 |
finishing the proof, the theory will be augmented by a type
|
|
705 |
signature declaration corresponding to the resulting theorem.
|
|
706 |
|
|
707 |
\end{descr}%
|
|
708 |
\end{isamarkuptext}%
|
|
709 |
\isamarkuptrue%
|
|
710 |
%
|
|
711 |
\isamarkupsubsection{Arbitrary overloading%
|
|
712 |
}
|
|
713 |
\isamarkuptrue%
|
|
714 |
%
|
|
715 |
\begin{isamarkuptext}%
|
|
716 |
Isabelle/Pure's definitional schemes support certain forms of
|
|
717 |
overloading (see \secref{sec:consts}). At most occassions
|
|
718 |
overloading will be used in a Haskell-like fashion together with
|
|
719 |
type classes by means of \mbox{\isa{\isacommand{instantiation}}} (see
|
|
720 |
\secref{sec:class}). Sometimes low-level overloading is desirable.
|
|
721 |
The \mbox{\isa{\isacommand{overloading}}} target provides a convenient view for
|
|
722 |
end-users.
|
|
723 |
|
|
724 |
\begin{matharray}{rcl}
|
|
725 |
\indexdef{}{command}{overloading}\mbox{\isa{\isacommand{overloading}}} & : & \isartrans{theory}{local{\dsh}theory} \\
|
|
726 |
\end{matharray}
|
|
727 |
|
|
728 |
\begin{rail}
|
|
729 |
'overloading' \\
|
|
730 |
( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
|
|
731 |
\end{rail}
|
|
732 |
|
|
733 |
\begin{descr}
|
|
734 |
|
26842
|
735 |
\item [\mbox{\isa{\isacommand{overloading}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}]
|
26782
|
736 |
opens a theory target (cf.\ \secref{sec:target}) which allows to
|
|
737 |
specify constants with overloaded definitions. These are identified
|
26842
|
738 |
by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type
|
26782
|
739 |
instances. The definitions themselves are established using common
|
26842
|
740 |
specification tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as
|
26782
|
741 |
reference to the corresponding constants. The target is concluded
|
|
742 |
by \mbox{\isa{\isacommand{end}}}.
|
|
743 |
|
26842
|
744 |
A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
|
26782
|
745 |
the corresponding definition, which is occasionally useful for
|
|
746 |
exotic overloading. It is at the discretion of the user to avoid
|
|
747 |
malformed theory specifications!
|
|
748 |
|
|
749 |
\end{descr}%
|
|
750 |
\end{isamarkuptext}%
|
|
751 |
\isamarkuptrue%
|
|
752 |
%
|
|
753 |
\isamarkupsubsection{Configuration options%
|
|
754 |
}
|
|
755 |
\isamarkuptrue%
|
|
756 |
%
|
|
757 |
\begin{isamarkuptext}%
|
|
758 |
Isabelle/Pure maintains a record of named configuration options
|
|
759 |
within the theory or proof context, with values of type \verb|bool|, \verb|int|, or \verb|string|. Tools may declare
|
|
760 |
options in ML, and then refer to these values (relative to the
|
|
761 |
context). Thus global reference variables are easily avoided. The
|
|
762 |
user may change the value of a configuration option by means of an
|
|
763 |
associated attribute of the same name. This form of context
|
|
764 |
declaration works particularly well with commands such as \mbox{\isa{\isacommand{declare}}} or \mbox{\isa{\isacommand{using}}}.
|
|
765 |
|
|
766 |
For historical reasons, some tools cannot take the full proof
|
|
767 |
context into account and merely refer to the background theory.
|
|
768 |
This is accommodated by configuration options being declared as
|
|
769 |
``global'', which may not be changed within a local context.
|
|
770 |
|
|
771 |
\begin{matharray}{rcll}
|
|
772 |
\indexdef{}{command}{print-configs}\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}} & : & \isarkeep{theory~|~proof} \\
|
|
773 |
\end{matharray}
|
|
774 |
|
|
775 |
\begin{rail}
|
|
776 |
name ('=' ('true' | 'false' | int | name))?
|
|
777 |
\end{rail}
|
|
778 |
|
|
779 |
\begin{descr}
|
|
780 |
|
|
781 |
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}] prints the available
|
|
782 |
configuration options, with names, types, and current values.
|
|
783 |
|
26842
|
784 |
\item [\isa{{\isachardoublequote}name\ {\isacharequal}\ value{\isachardoublequote}}] as an attribute expression modifies
|
26782
|
785 |
the named option, with the syntax of the value depending on the
|
|
786 |
option's type. For \verb|bool| the default value is \isa{true}. Any attempt to change a global option in a local context is
|
|
787 |
ignored.
|
|
788 |
|
|
789 |
\end{descr}%
|
|
790 |
\end{isamarkuptext}%
|
|
791 |
\isamarkuptrue%
|
|
792 |
%
|
|
793 |
\isamarkupsection{Derived proof schemes%
|
|
794 |
}
|
|
795 |
\isamarkuptrue%
|
|
796 |
%
|
|
797 |
\isamarkupsubsection{Generalized elimination \label{sec:obtain}%
|
|
798 |
}
|
|
799 |
\isamarkuptrue%
|
|
800 |
%
|
|
801 |
\begin{isamarkuptext}%
|
|
802 |
\begin{matharray}{rcl}
|
|
803 |
\indexdef{}{command}{obtain}\mbox{\isa{\isacommand{obtain}}} & : & \isartrans{proof(state)}{proof(prove)} \\
|
26842
|
804 |
\indexdef{}{command}{guess}\mbox{\isa{\isacommand{guess}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(state)}{proof(prove)} \\
|
26782
|
805 |
\end{matharray}
|
|
806 |
|
|
807 |
Generalized elimination means that additional elements with certain
|
|
808 |
properties may be introduced in the current context, by virtue of a
|
|
809 |
locally proven ``soundness statement''. Technically speaking, the
|
|
810 |
\mbox{\isa{\isacommand{obtain}}} language element is like a declaration of
|
|
811 |
\mbox{\isa{\isacommand{fix}}} and \mbox{\isa{\isacommand{assume}}} (see also see
|
|
812 |
\secref{sec:proof-context}), together with a soundness proof of its
|
|
813 |
additional claim. According to the nature of existential reasoning,
|
|
814 |
assumptions get eliminated from any result exported from the context
|
|
815 |
later, provided that the corresponding parameters do \emph{not}
|
|
816 |
occur in the conclusion.
|
|
817 |
|
|
818 |
\begin{rail}
|
|
819 |
'obtain' parname? (vars + 'and') 'where' (props + 'and')
|
|
820 |
;
|
|
821 |
'guess' (vars + 'and')
|
|
822 |
;
|
|
823 |
\end{rail}
|
|
824 |
|
|
825 |
The derived Isar command \mbox{\isa{\isacommand{obtain}}} is defined as follows
|
26842
|
826 |
(where \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k{\isachardoublequote}} shall refer to (optional)
|
26782
|
827 |
facts indicated for forward chaining).
|
|
828 |
\begin{matharray}{l}
|
26842
|
829 |
\isa{{\isachardoublequote}{\isasymlangle}using\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k{\isasymrangle}{\isachardoublequote}}~~\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]
|
|
830 |
\quad \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}} \\
|
26782
|
831 |
\quad \mbox{\isa{\isacommand{proof}}}~\isa{succeed} \\
|
|
832 |
\qquad \mbox{\isa{\isacommand{fix}}}~\isa{thesis} \\
|
26842
|
833 |
\qquad \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}} \\
|
26782
|
834 |
\qquad \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}}~\isa{thesis} \\
|
|
835 |
\quad\qquad \mbox{\isa{\isacommand{apply}}}~\isa{{\isacharminus}} \\
|
26842
|
836 |
\quad\qquad \mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k\ \ {\isasymlangle}proof{\isasymrangle}{\isachardoublequote}} \\
|
26782
|
837 |
\quad \mbox{\isa{\isacommand{qed}}} \\
|
26842
|
838 |
\quad \mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\mbox{\isa{\isacommand{assume}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} \\
|
26782
|
839 |
\end{matharray}
|
|
840 |
|
|
841 |
Typically, the soundness proof is relatively straight-forward, often
|
|
842 |
just by canonical automated tools such as ``\mbox{\isa{\isacommand{by}}}~\isa{simp}'' or ``\mbox{\isa{\isacommand{by}}}~\isa{blast}''. Accordingly, the
|
|
843 |
``\isa{that}'' reduction above is declared as simplification and
|
|
844 |
introduction rule.
|
|
845 |
|
|
846 |
In a sense, \mbox{\isa{\isacommand{obtain}}} represents at the level of Isar
|
|
847 |
proofs what would be meta-logical existential quantifiers and
|
|
848 |
conjunctions. This concept has a broad range of useful
|
|
849 |
applications, ranging from plain elimination (or introduction) of
|
|
850 |
object-level existential and conjunctions, to elimination over
|
|
851 |
results of symbolic evaluation of recursive definitions, for
|
|
852 |
example. Also note that \mbox{\isa{\isacommand{obtain}}} without parameters acts
|
|
853 |
much like \mbox{\isa{\isacommand{have}}}, where the result is treated as a
|
|
854 |
genuine assumption.
|
|
855 |
|
|
856 |
An alternative name to be used instead of ``\isa{that}'' above may
|
|
857 |
be given in parentheses.
|
|
858 |
|
|
859 |
\medskip The improper variant \mbox{\isa{\isacommand{guess}}} is similar to
|
|
860 |
\mbox{\isa{\isacommand{obtain}}}, but derives the obtained statement from the
|
|
861 |
course of reasoning! The proof starts with a fixed goal \isa{thesis}. The subsequent proof may refine this to anything of the
|
26842
|
862 |
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
|
26782
|
863 |
final goal state is then used as reduction rule for the obtain
|
26842
|
864 |
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
|
26782
|
865 |
proof context from being polluted by ad-hoc variables. The variable
|
|
866 |
names and type constraints given as arguments for \mbox{\isa{\isacommand{guess}}}
|
|
867 |
specify a prefix of obtained parameters explicitly in the text.
|
|
868 |
|
|
869 |
It is important to note that the facts introduced by \mbox{\isa{\isacommand{obtain}}} and \mbox{\isa{\isacommand{guess}}} may not be polymorphic: any
|
|
870 |
type-variables occurring here are fixed in the present context!%
|
|
871 |
\end{isamarkuptext}%
|
|
872 |
\isamarkuptrue%
|
|
873 |
%
|
|
874 |
\isamarkupsubsection{Calculational reasoning \label{sec:calculation}%
|
|
875 |
}
|
|
876 |
\isamarkuptrue%
|
|
877 |
%
|
|
878 |
\begin{isamarkuptext}%
|
|
879 |
\begin{matharray}{rcl}
|
|
880 |
\indexdef{}{command}{also}\mbox{\isa{\isacommand{also}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
881 |
\indexdef{}{command}{finally}\mbox{\isa{\isacommand{finally}}} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
882 |
\indexdef{}{command}{moreover}\mbox{\isa{\isacommand{moreover}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
883 |
\indexdef{}{command}{ultimately}\mbox{\isa{\isacommand{ultimately}}} & : & \isartrans{proof(state)}{proof(chain)} \\
|
26842
|
884 |
\indexdef{}{command}{print-trans-rules}\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
26782
|
885 |
\mbox{\isa{trans}} & : & \isaratt \\
|
|
886 |
\mbox{\isa{sym}} & : & \isaratt \\
|
|
887 |
\mbox{\isa{symmetric}} & : & \isaratt \\
|
|
888 |
\end{matharray}
|
|
889 |
|
|
890 |
Calculational proof is forward reasoning with implicit application
|
26842
|
891 |
of transitivity rules (such those of \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymle}{\isachardoublequote}},
|
|
892 |
\isa{{\isachardoublequote}{\isacharless}{\isachardoublequote}}). Isabelle/Isar maintains an auxiliary fact register
|
26782
|
893 |
\indexref{}{fact}{calculation}\mbox{\isa{calculation}} for accumulating results obtained by
|
|
894 |
transitivity composed with the current result. Command \mbox{\isa{\isacommand{also}}} updates \mbox{\isa{calculation}} involving \mbox{\isa{this}}, while
|
|
895 |
\mbox{\isa{\isacommand{finally}}} exhibits the final \mbox{\isa{calculation}} by
|
|
896 |
forward chaining towards the next goal statement. Both commands
|
|
897 |
require valid current facts, i.e.\ may occur only after commands
|
|
898 |
that produce theorems such as \mbox{\isa{\isacommand{assume}}}, \mbox{\isa{\isacommand{note}}}, or some finished proof of \mbox{\isa{\isacommand{have}}}, \mbox{\isa{\isacommand{show}}} etc. The \mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}
|
|
899 |
commands are similar to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}},
|
|
900 |
but only collect further results in \mbox{\isa{calculation}} without
|
|
901 |
applying any rules yet.
|
|
902 |
|
26842
|
903 |
Also note that the implicit term abbreviation ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' has
|
26782
|
904 |
its canonical application with calculational proofs. It refers to
|
|
905 |
the argument of the preceding statement. (The argument of a curried
|
|
906 |
infix expression happens to be its right-hand side.)
|
|
907 |
|
|
908 |
Isabelle/Isar calculations are implicitly subject to block structure
|
|
909 |
in the sense that new threads of calculational reasoning are
|
|
910 |
commenced for any new block (as opened by a local goal, for
|
|
911 |
example). This means that, apart from being able to nest
|
|
912 |
calculations, there is no separate \emph{begin-calculation} command
|
|
913 |
required.
|
|
914 |
|
|
915 |
\medskip The Isar calculation proof commands may be defined as
|
|
916 |
follows:\footnote{We suppress internal bookkeeping such as proper
|
|
917 |
handling of block-structure.}
|
|
918 |
|
|
919 |
\begin{matharray}{rcl}
|
26842
|
920 |
\mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
|
|
921 |
\mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\[0.5ex]
|
26782
|
922 |
\mbox{\isa{\isacommand{finally}}} & \equiv & \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
|
26842
|
923 |
\mbox{\isa{\isacommand{moreover}}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
|
26782
|
924 |
\mbox{\isa{\isacommand{ultimately}}} & \equiv & \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\
|
|
925 |
\end{matharray}
|
|
926 |
|
|
927 |
\begin{rail}
|
|
928 |
('also' | 'finally') ('(' thmrefs ')')?
|
|
929 |
;
|
|
930 |
'trans' (() | 'add' | 'del')
|
|
931 |
;
|
|
932 |
\end{rail}
|
|
933 |
|
|
934 |
\begin{descr}
|
|
935 |
|
26842
|
936 |
\item [\mbox{\isa{\isacommand{also}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}]
|
26782
|
937 |
maintains the auxiliary \mbox{\isa{calculation}} register as follows.
|
|
938 |
The first occurrence of \mbox{\isa{\isacommand{also}}} in some calculational
|
|
939 |
thread initializes \mbox{\isa{calculation}} by \mbox{\isa{this}}. Any
|
|
940 |
subsequent \mbox{\isa{\isacommand{also}}} on the same level of block-structure
|
|
941 |
updates \mbox{\isa{calculation}} by some transitivity rule applied to
|
|
942 |
\mbox{\isa{calculation}} and \mbox{\isa{this}} (in that order). Transitivity
|
|
943 |
rules are picked from the current context, unless alternative rules
|
|
944 |
are given as explicit arguments.
|
|
945 |
|
26842
|
946 |
\item [\mbox{\isa{\isacommand{finally}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}]
|
26782
|
947 |
maintaining \mbox{\isa{calculation}} in the same way as \mbox{\isa{\isacommand{also}}}, and concludes the current calculational thread. The final
|
|
948 |
result is exhibited as fact for forward chaining towards the next
|
|
949 |
goal. Basically, \mbox{\isa{\isacommand{finally}}} just abbreviates \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\mbox{\isa{calculation}}. Typical idioms for
|
|
950 |
concluding calculational proofs are ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{show}}}~\isa{{\isacharquery}thesis}~\mbox{\isa{\isacommand{{\isachardot}}}}'' and ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{have}}}~\isa{{\isasymphi}}~\mbox{\isa{\isacommand{{\isachardot}}}}''.
|
|
951 |
|
|
952 |
\item [\mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}] are
|
|
953 |
analogous to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}}, but collect
|
|
954 |
results only, without applying rules.
|
|
955 |
|
|
956 |
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}] prints the list of
|
|
957 |
transitivity rules (for calculational commands \mbox{\isa{\isacommand{also}}} and
|
|
958 |
\mbox{\isa{\isacommand{finally}}}) and symmetry rules (for the \mbox{\isa{symmetric}} operation and single step elimination patters) of the
|
|
959 |
current context.
|
|
960 |
|
|
961 |
\item [\mbox{\isa{trans}}] declares theorems as transitivity rules.
|
|
962 |
|
|
963 |
\item [\mbox{\isa{sym}}] declares symmetry rules, as well as
|
|
964 |
\mbox{\isa{Pure{\isachardot}elim{\isacharquery}}} rules.
|
|
965 |
|
|
966 |
\item [\mbox{\isa{symmetric}}] resolves a theorem with some rule
|
|
967 |
declared as \mbox{\isa{sym}} in the current context. For example,
|
26842
|
968 |
``\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcolon}\ x\ {\isacharequal}\ y{\isachardoublequote}}'' produces a
|
26782
|
969 |
swapped fact derived from that assumption.
|
|
970 |
|
|
971 |
In structured proof texts it is often more appropriate to use an
|
26842
|
972 |
explicit single-step elimination proof, such as ``\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}}~\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}y\ {\isacharequal}\ x{\isachardoublequote}}~\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}''.
|
26782
|
973 |
|
|
974 |
\end{descr}%
|
|
975 |
\end{isamarkuptext}%
|
|
976 |
\isamarkuptrue%
|
|
977 |
%
|
|
978 |
\isamarkupsection{Proof tools%
|
|
979 |
}
|
|
980 |
\isamarkuptrue%
|
|
981 |
%
|
|
982 |
\isamarkupsubsection{Miscellaneous methods and attributes \label{sec:misc-meth-att}%
|
|
983 |
}
|
|
984 |
\isamarkuptrue%
|
|
985 |
%
|
|
986 |
\begin{isamarkuptext}%
|
|
987 |
\begin{matharray}{rcl}
|
|
988 |
\indexdef{}{method}{unfold}\mbox{\isa{unfold}} & : & \isarmeth \\
|
|
989 |
\indexdef{}{method}{fold}\mbox{\isa{fold}} & : & \isarmeth \\
|
|
990 |
\indexdef{}{method}{insert}\mbox{\isa{insert}} & : & \isarmeth \\[0.5ex]
|
26842
|
991 |
\indexdef{}{method}{erule}\mbox{\isa{erule}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
992 |
\indexdef{}{method}{drule}\mbox{\isa{drule}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
993 |
\indexdef{}{method}{frule}\mbox{\isa{frule}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
26782
|
994 |
\indexdef{}{method}{succeed}\mbox{\isa{succeed}} & : & \isarmeth \\
|
|
995 |
\indexdef{}{method}{fail}\mbox{\isa{fail}} & : & \isarmeth \\
|
|
996 |
\end{matharray}
|
|
997 |
|
|
998 |
\begin{rail}
|
|
999 |
('fold' | 'unfold' | 'insert') thmrefs
|
|
1000 |
;
|
|
1001 |
('erule' | 'drule' | 'frule') ('('nat')')? thmrefs
|
|
1002 |
;
|
|
1003 |
\end{rail}
|
|
1004 |
|
|
1005 |
\begin{descr}
|
|
1006 |
|
26842
|
1007 |
\item [\mbox{\isa{unfold}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and \mbox{\isa{fold}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] expand (or fold back) the
|
26782
|
1008 |
given definitions throughout all goals; any chained facts provided
|
|
1009 |
are inserted into the goal and subject to rewriting as well.
|
|
1010 |
|
26842
|
1011 |
\item [\mbox{\isa{insert}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] inserts
|
26782
|
1012 |
theorems as facts into all goals of the proof state. Note that
|
|
1013 |
current facts indicated for forward chaining are ignored.
|
|
1014 |
|
26842
|
1015 |
\item [\mbox{\isa{erule}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, \mbox{\isa{drule}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, and \mbox{\isa{frule}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] are similar to the basic \mbox{\isa{rule}}
|
26782
|
1016 |
method (see \secref{sec:pure-meth-att}), but apply rules by
|
|
1017 |
elim-resolution, destruct-resolution, and forward-resolution,
|
|
1018 |
respectively \cite{isabelle-ref}. The optional natural number
|
|
1019 |
argument (default 0) specifies additional assumption steps to be
|
|
1020 |
performed here.
|
|
1021 |
|
|
1022 |
Note that these methods are improper ones, mainly serving for
|
|
1023 |
experimentation and tactic script emulation. Different modes of
|
|
1024 |
basic rule application are usually expressed in Isar at the proof
|
|
1025 |
language level, rather than via implicit proof state manipulations.
|
|
1026 |
For example, a proper single-step elimination would be done using
|
|
1027 |
the plain \mbox{\isa{rule}} method, with forward chaining of current
|
|
1028 |
facts.
|
|
1029 |
|
|
1030 |
\item [\mbox{\isa{succeed}}] yields a single (unchanged) result; it is
|
26842
|
1031 |
the identity of the ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' method combinator (cf.\
|
26782
|
1032 |
\secref{sec:syn-meth}).
|
|
1033 |
|
|
1034 |
\item [\mbox{\isa{fail}}] yields an empty result sequence; it is the
|
26842
|
1035 |
identity of the ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' method combinator (cf.\
|
26782
|
1036 |
\secref{sec:syn-meth}).
|
|
1037 |
|
|
1038 |
\end{descr}
|
|
1039 |
|
|
1040 |
\begin{matharray}{rcl}
|
|
1041 |
\indexdef{}{attribute}{tagged}\mbox{\isa{tagged}} & : & \isaratt \\
|
|
1042 |
\indexdef{}{attribute}{untagged}\mbox{\isa{untagged}} & : & \isaratt \\[0.5ex]
|
|
1043 |
\indexdef{}{attribute}{THEN}\mbox{\isa{THEN}} & : & \isaratt \\
|
|
1044 |
\indexdef{}{attribute}{COMP}\mbox{\isa{COMP}} & : & \isaratt \\[0.5ex]
|
|
1045 |
\indexdef{}{attribute}{unfolded}\mbox{\isa{unfolded}} & : & \isaratt \\
|
|
1046 |
\indexdef{}{attribute}{folded}\mbox{\isa{folded}} & : & \isaratt \\[0.5ex]
|
|
1047 |
\indexdef{}{attribute}{rotated}\mbox{\isa{rotated}} & : & \isaratt \\
|
|
1048 |
\indexdef{Pure}{attribute}{elim-format}\mbox{\isa{elim{\isacharunderscore}format}} & : & \isaratt \\
|
26842
|
1049 |
\indexdef{}{attribute}{standard}\mbox{\isa{standard}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
|
|
1050 |
\indexdef{}{attribute}{no-vars}\mbox{\isa{no{\isacharunderscore}vars}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
|
26782
|
1051 |
\end{matharray}
|
|
1052 |
|
|
1053 |
\begin{rail}
|
|
1054 |
'tagged' nameref
|
|
1055 |
;
|
|
1056 |
'untagged' name
|
|
1057 |
;
|
|
1058 |
('THEN' | 'COMP') ('[' nat ']')? thmref
|
|
1059 |
;
|
|
1060 |
('unfolded' | 'folded') thmrefs
|
|
1061 |
;
|
|
1062 |
'rotated' ( int )?
|
|
1063 |
\end{rail}
|
|
1064 |
|
|
1065 |
\begin{descr}
|
|
1066 |
|
26842
|
1067 |
\item [\mbox{\isa{tagged}}~\isa{{\isachardoublequote}name\ arg{\isachardoublequote}} and \mbox{\isa{untagged}}~\isa{name}] add and remove \emph{tags} of some theorem.
|
26782
|
1068 |
Tags may be any list of string pairs that serve as formal comment.
|
|
1069 |
The first string is considered the tag name, the second its
|
|
1070 |
argument. Note that \mbox{\isa{untagged}} removes any tags of the
|
|
1071 |
same name.
|
|
1072 |
|
|
1073 |
\item [\mbox{\isa{THEN}}~\isa{a} and \mbox{\isa{COMP}}~\isa{a}]
|
|
1074 |
compose rules by resolution. \mbox{\isa{THEN}} resolves with the
|
|
1075 |
first premise of \isa{a} (an alternative position may be also
|
|
1076 |
specified); the \mbox{\isa{COMP}} version skips the automatic
|
26842
|
1077 |
lifting process that is normally intended (cf.\ \verb|"op RS"| and
|
|
1078 |
\verb|"op COMP"| in \cite[\S5]{isabelle-ref}).
|
26782
|
1079 |
|
26842
|
1080 |
\item [\mbox{\isa{unfolded}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and
|
|
1081 |
\mbox{\isa{folded}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] expand and fold
|
26782
|
1082 |
back again the given definitions throughout a rule.
|
|
1083 |
|
|
1084 |
\item [\mbox{\isa{rotated}}~\isa{n}] rotate the premises of a
|
|
1085 |
theorem by \isa{n} (default 1).
|
|
1086 |
|
|
1087 |
\item [\mbox{\isa{Pure{\isachardot}elim{\isacharunderscore}format}}] turns a destruction rule into
|
|
1088 |
elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}.
|
|
1089 |
|
|
1090 |
Note that the Classical Reasoner (\secref{sec:classical}) provides
|
|
1091 |
its own version of this operation.
|
|
1092 |
|
|
1093 |
\item [\mbox{\isa{standard}}] puts a theorem into the standard form
|
|
1094 |
of object-rules at the outermost theory level. Note that this
|
|
1095 |
operation violates the local proof context (including active
|
|
1096 |
locales).
|
|
1097 |
|
|
1098 |
\item [\mbox{\isa{no{\isacharunderscore}vars}}] replaces schematic variables by free
|
|
1099 |
ones; this is mainly for tuning output of pretty printed theorems.
|
|
1100 |
|
|
1101 |
\end{descr}%
|
|
1102 |
\end{isamarkuptext}%
|
|
1103 |
\isamarkuptrue%
|
|
1104 |
%
|
|
1105 |
\isamarkupsubsection{Further tactic emulations \label{sec:tactics}%
|
|
1106 |
}
|
|
1107 |
\isamarkuptrue%
|
|
1108 |
%
|
|
1109 |
\begin{isamarkuptext}%
|
|
1110 |
The following improper proof methods emulate traditional tactics.
|
|
1111 |
These admit direct access to the goal state, which is normally
|
|
1112 |
considered harmful! In particular, this may involve both numbered
|
|
1113 |
goal addressing (default 1), and dynamic instantiation within the
|
|
1114 |
scope of some subgoal.
|
|
1115 |
|
|
1116 |
\begin{warn}
|
|
1117 |
Dynamic instantiations refer to universally quantified parameters
|
|
1118 |
of a subgoal (the dynamic context) rather than fixed variables and
|
|
1119 |
term abbreviations of a (static) Isar context.
|
|
1120 |
\end{warn}
|
|
1121 |
|
|
1122 |
Tactic emulation methods, unlike their ML counterparts, admit
|
|
1123 |
simultaneous instantiation from both dynamic and static contexts.
|
|
1124 |
If names occur in both contexts goal parameters hide locally fixed
|
|
1125 |
variables. Likewise, schematic variables refer to term
|
|
1126 |
abbreviations, if present in the static context. Otherwise the
|
|
1127 |
schematic variable is interpreted as a schematic variable and left
|
|
1128 |
to be solved by unification with certain parts of the subgoal.
|
|
1129 |
|
|
1130 |
Note that the tactic emulation proof methods in Isabelle/Isar are
|
|
1131 |
consistently named \isa{foo{\isacharunderscore}tac}. Note also that variable names
|
|
1132 |
occurring on left hand sides of instantiations must be preceded by a
|
|
1133 |
question mark if they coincide with a keyword or contain dots. This
|
|
1134 |
is consistent with the attribute \mbox{\isa{where}} (see
|
|
1135 |
\secref{sec:pure-meth-att}).
|
|
1136 |
|
|
1137 |
\begin{matharray}{rcl}
|
26842
|
1138 |
\indexdef{}{method}{rule-tac}\mbox{\isa{rule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
1139 |
\indexdef{}{method}{erule-tac}\mbox{\isa{erule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
1140 |
\indexdef{}{method}{drule-tac}\mbox{\isa{drule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
1141 |
\indexdef{}{method}{frule-tac}\mbox{\isa{frule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
1142 |
\indexdef{}{method}{cut-tac}\mbox{\isa{cut{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
1143 |
\indexdef{}{method}{thin-tac}\mbox{\isa{thin{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
1144 |
\indexdef{}{method}{subgoal-tac}\mbox{\isa{subgoal{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
1145 |
\indexdef{}{method}{rename-tac}\mbox{\isa{rename{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
1146 |
\indexdef{}{method}{rotate-tac}\mbox{\isa{rotate{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
1147 |
\indexdef{}{method}{tactic}\mbox{\isa{tactic}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
26782
|
1148 |
\end{matharray}
|
|
1149 |
|
|
1150 |
\begin{rail}
|
|
1151 |
( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
|
|
1152 |
( insts thmref | thmrefs )
|
|
1153 |
;
|
|
1154 |
'subgoal\_tac' goalspec? (prop +)
|
|
1155 |
;
|
|
1156 |
'rename\_tac' goalspec? (name +)
|
|
1157 |
;
|
|
1158 |
'rotate\_tac' goalspec? int?
|
|
1159 |
;
|
|
1160 |
'tactic' text
|
|
1161 |
;
|
|
1162 |
|
|
1163 |
insts: ((name '=' term) + 'and') 'in'
|
|
1164 |
;
|
|
1165 |
\end{rail}
|
|
1166 |
|
|
1167 |
\begin{descr}
|
|
1168 |
|
|
1169 |
\item [\mbox{\isa{rule{\isacharunderscore}tac}} etc.] do resolution of rules with explicit
|
|
1170 |
instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite[\S3]{isabelle-ref}).
|
|
1171 |
|
|
1172 |
Multiple rules may be only given if there is no instantiation; then
|
|
1173 |
\mbox{\isa{rule{\isacharunderscore}tac}} is the same as \verb|resolve_tac| in ML (see
|
|
1174 |
\cite[\S3]{isabelle-ref}).
|
|
1175 |
|
|
1176 |
\item [\mbox{\isa{cut{\isacharunderscore}tac}}] inserts facts into the proof state as
|
|
1177 |
assumption of a subgoal, see also \verb|cut_facts_tac| in
|
|
1178 |
\cite[\S3]{isabelle-ref}. Note that the scope of schematic
|
|
1179 |
variables is spread over the main goal statement. Instantiations
|
|
1180 |
may be given as well, see also ML tactic \verb|cut_inst_tac| in
|
|
1181 |
\cite[\S3]{isabelle-ref}.
|
|
1182 |
|
|
1183 |
\item [\mbox{\isa{thin{\isacharunderscore}tac}}~\isa{{\isasymphi}}] deletes the specified
|
|
1184 |
assumption from a subgoal; note that \isa{{\isasymphi}} may contain schematic
|
|
1185 |
variables. See also \verb|thin_tac| in \cite[\S3]{isabelle-ref}.
|
|
1186 |
|
|
1187 |
\item [\mbox{\isa{subgoal{\isacharunderscore}tac}}~\isa{{\isasymphi}}] adds \isa{{\isasymphi}} as an
|
|
1188 |
assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite[\S3]{isabelle-ref}.
|
|
1189 |
|
26842
|
1190 |
\item [\mbox{\isa{rename{\isacharunderscore}tac}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}}] renames
|
|
1191 |
parameters of a goal according to the list \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}, which refers to the \emph{suffix} of variables.
|
26782
|
1192 |
|
|
1193 |
\item [\mbox{\isa{rotate{\isacharunderscore}tac}}~\isa{n}] rotates the assumptions of a
|
|
1194 |
goal by \isa{n} positions: from right to left if \isa{n} is
|
|
1195 |
positive, and from left to right if \isa{n} is negative; the
|
|
1196 |
default value is 1. See also \verb|rotate_tac| in
|
|
1197 |
\cite[\S3]{isabelle-ref}.
|
|
1198 |
|
26842
|
1199 |
\item [\mbox{\isa{tactic}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] produces a proof method from
|
26782
|
1200 |
any ML text of type \verb|tactic|. Apart from the usual ML
|
|
1201 |
environment and the current implicit theory context, the ML code may
|
|
1202 |
refer to the following locally bound values:
|
|
1203 |
|
|
1204 |
%FIXME check
|
|
1205 |
{\footnotesize\begin{verbatim}
|
|
1206 |
val ctxt : Proof.context
|
|
1207 |
val facts : thm list
|
|
1208 |
val thm : string -> thm
|
|
1209 |
val thms : string -> thm list
|
|
1210 |
\end{verbatim}}
|
|
1211 |
|
|
1212 |
Here \verb|ctxt| refers to the current proof context, \verb|facts| indicates any current facts for forward-chaining, and \verb|thm|~/~\verb|thms| retrieve named facts (including global theorems)
|
|
1213 |
from the context.
|
|
1214 |
|
|
1215 |
\end{descr}%
|
|
1216 |
\end{isamarkuptext}%
|
|
1217 |
\isamarkuptrue%
|
|
1218 |
%
|
|
1219 |
\isamarkupsubsection{The Simplifier \label{sec:simplifier}%
|
|
1220 |
}
|
|
1221 |
\isamarkuptrue%
|
|
1222 |
%
|
|
1223 |
\isamarkupsubsubsection{Simplification methods%
|
|
1224 |
}
|
|
1225 |
\isamarkuptrue%
|
|
1226 |
%
|
|
1227 |
\begin{isamarkuptext}%
|
|
1228 |
\begin{matharray}{rcl}
|
|
1229 |
\indexdef{}{method}{simp}\mbox{\isa{simp}} & : & \isarmeth \\
|
|
1230 |
\indexdef{}{method}{simp-all}\mbox{\isa{simp{\isacharunderscore}all}} & : & \isarmeth \\
|
|
1231 |
\end{matharray}
|
|
1232 |
|
|
1233 |
\indexouternonterm{simpmod}
|
|
1234 |
\begin{rail}
|
|
1235 |
('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
|
|
1236 |
;
|
|
1237 |
|
|
1238 |
opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' | 'depth\_limit' ':' nat) ')'
|
|
1239 |
;
|
|
1240 |
simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
|
|
1241 |
'split' (() | 'add' | 'del')) ':' thmrefs
|
|
1242 |
;
|
|
1243 |
\end{rail}
|
|
1244 |
|
|
1245 |
\begin{descr}
|
|
1246 |
|
|
1247 |
\item [\mbox{\isa{simp}}] invokes the Simplifier, after declaring
|
|
1248 |
additional rules according to the arguments given. Note that the
|
|
1249 |
\railtterm{only} modifier first removes all other rewrite rules,
|
|
1250 |
congruences, and looper tactics (including splits), and then behaves
|
|
1251 |
like \railtterm{add}.
|
|
1252 |
|
|
1253 |
\medskip The \railtterm{cong} modifiers add or delete Simplifier
|
|
1254 |
congruence rules (see also \cite{isabelle-ref}), the default is to
|
|
1255 |
add.
|
|
1256 |
|
|
1257 |
\medskip The \railtterm{split} modifiers add or delete rules for the
|
|
1258 |
Splitter (see also \cite{isabelle-ref}), the default is to add.
|
|
1259 |
This works only if the Simplifier method has been properly setup to
|
|
1260 |
include the Splitter (all major object logics such HOL, HOLCF, FOL,
|
|
1261 |
ZF do this already).
|
|
1262 |
|
|
1263 |
\item [\mbox{\isa{simp{\isacharunderscore}all}}] is similar to \mbox{\isa{simp}}, but acts on
|
|
1264 |
all goals (backwards from the last to the first one).
|
|
1265 |
|
|
1266 |
\end{descr}
|
|
1267 |
|
|
1268 |
By default the Simplifier methods take local assumptions fully into
|
|
1269 |
account, using equational assumptions in the subsequent
|
|
1270 |
normalization process, or simplifying assumptions themselves (cf.\
|
|
1271 |
\verb|asm_full_simp_tac| in \cite[\S10]{isabelle-ref}). In
|
|
1272 |
structured proofs this is usually quite well behaved in practice:
|
|
1273 |
just the local premises of the actual goal are involved, additional
|
|
1274 |
facts may be inserted via explicit forward-chaining (via \mbox{\isa{\isacommand{then}}}, \mbox{\isa{\isacommand{from}}}, \mbox{\isa{\isacommand{using}}} etc.). The full
|
26842
|
1275 |
context of premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang)
|
26782
|
1276 |
argument is given, which should be used with some care, though.
|
|
1277 |
|
|
1278 |
Additional Simplifier options may be specified to tune the behavior
|
|
1279 |
further (mostly for unstructured scripts with many accidental local
|
26842
|
1280 |
facts): ``\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}}'' means assumptions are ignored
|
|
1281 |
completely (cf.\ \verb|simp_tac|), ``\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}}'' means
|
26782
|
1282 |
assumptions are used in the simplification of the conclusion but are
|
26842
|
1283 |
not themselves simplified (cf.\ \verb|asm_simp_tac|), and ``\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}{\isachardoublequote}}'' means assumptions are simplified but are not used
|
26782
|
1284 |
in the simplification of each other or the conclusion (cf.\ \verb|full_simp_tac|). For compatibility reasons, there is also an option
|
26842
|
1285 |
``\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharunderscore}lr{\isacharparenright}{\isachardoublequote}}'', which means that an assumption is only used
|
26782
|
1286 |
for simplifying assumptions which are to the right of it (cf.\ \verb|asm_lr_simp_tac|).
|
|
1287 |
|
26842
|
1288 |
Giving an option ``\isa{{\isachardoublequote}{\isacharparenleft}depth{\isacharunderscore}limit{\isacharcolon}\ n{\isacharparenright}{\isachardoublequote}}'' limits the number of
|
26782
|
1289 |
recursive invocations of the simplifier during conditional
|
|
1290 |
rewriting.
|
|
1291 |
|
|
1292 |
\medskip The Splitter package is usually configured to work as part
|
26842
|
1293 |
of the Simplifier. The effect of repeatedly applying \verb|split_tac| can be simulated by ``\isa{{\isachardoublequote}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}''. There is also a separate \isa{split}
|
26782
|
1294 |
method available for single-step case splitting.%
|
|
1295 |
\end{isamarkuptext}%
|
|
1296 |
\isamarkuptrue%
|
|
1297 |
%
|
|
1298 |
\isamarkupsubsubsection{Declaring rules%
|
|
1299 |
}
|
|
1300 |
\isamarkuptrue%
|
|
1301 |
%
|
|
1302 |
\begin{isamarkuptext}%
|
|
1303 |
\begin{matharray}{rcl}
|
26842
|
1304 |
\indexdef{}{command}{print-simpset}\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
26782
|
1305 |
\indexdef{}{attribute}{simp}\mbox{\isa{simp}} & : & \isaratt \\
|
|
1306 |
\indexdef{}{attribute}{cong}\mbox{\isa{cong}} & : & \isaratt \\
|
|
1307 |
\indexdef{}{attribute}{split}\mbox{\isa{split}} & : & \isaratt \\
|
|
1308 |
\end{matharray}
|
|
1309 |
|
|
1310 |
\begin{rail}
|
|
1311 |
('simp' | 'cong' | 'split') (() | 'add' | 'del')
|
|
1312 |
;
|
|
1313 |
\end{rail}
|
|
1314 |
|
|
1315 |
\begin{descr}
|
|
1316 |
|
|
1317 |
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}] prints the collection of rules
|
|
1318 |
declared to the Simplifier, which is also known as ``simpset''
|
|
1319 |
internally \cite{isabelle-ref}.
|
|
1320 |
|
|
1321 |
\item [\mbox{\isa{simp}}] declares simplification rules.
|
|
1322 |
|
|
1323 |
\item [\mbox{\isa{cong}}] declares congruence rules.
|
|
1324 |
|
|
1325 |
\item [\mbox{\isa{split}}] declares case split rules.
|
|
1326 |
|
|
1327 |
\end{descr}%
|
|
1328 |
\end{isamarkuptext}%
|
|
1329 |
\isamarkuptrue%
|
|
1330 |
%
|
|
1331 |
\isamarkupsubsubsection{Simplification procedures%
|
|
1332 |
}
|
|
1333 |
\isamarkuptrue%
|
|
1334 |
%
|
|
1335 |
\begin{isamarkuptext}%
|
|
1336 |
\begin{matharray}{rcl}
|
|
1337 |
\indexdef{}{command}{simproc-setup}\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
1338 |
simproc & : & \isaratt \\
|
|
1339 |
\end{matharray}
|
|
1340 |
|
|
1341 |
\begin{rail}
|
|
1342 |
'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
|
|
1343 |
;
|
|
1344 |
|
|
1345 |
'simproc' (('add' ':')? | 'del' ':') (name+)
|
|
1346 |
;
|
|
1347 |
\end{rail}
|
|
1348 |
|
|
1349 |
\begin{descr}
|
|
1350 |
|
|
1351 |
\item [\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}] defines a named simplification
|
|
1352 |
procedure that is invoked by the Simplifier whenever any of the
|
|
1353 |
given term patterns match the current redex. The implementation,
|
26842
|
1354 |
which is provided as ML source text, needs to be of type \verb|"morphism -> simpset -> cterm -> thm option"|, where the \verb|cterm| represents the current redex \isa{r} and the result is
|
|
1355 |
supposed to be some proven rewrite rule \isa{{\isachardoublequote}r\ {\isasymequiv}\ r{\isacharprime}{\isachardoublequote}} (or a
|
26782
|
1356 |
generalized version), or \verb|NONE| to indicate failure. The
|
|
1357 |
\verb|simpset| argument holds the full context of the current
|
|
1358 |
Simplifier invocation, including the actual Isar proof context. The
|
|
1359 |
\verb|morphism| informs about the difference of the original
|
|
1360 |
compilation context wrt.\ the one of the actual application later
|
|
1361 |
on. The optional \mbox{\isa{\isakeyword{identifier}}} specifies theorems that
|
|
1362 |
represent the logical content of the abstract theory of this
|
|
1363 |
simproc.
|
|
1364 |
|
|
1365 |
Morphisms and identifiers are only relevant for simprocs that are
|
|
1366 |
defined within a local target context, e.g.\ in a locale.
|
|
1367 |
|
26842
|
1368 |
\item [\isa{{\isachardoublequote}simproc\ add{\isacharcolon}\ name{\isachardoublequote}} and \isa{{\isachardoublequote}simproc\ del{\isacharcolon}\ name{\isachardoublequote}}]
|
26782
|
1369 |
add or delete named simprocs to the current Simplifier context. The
|
|
1370 |
default is to add a simproc. Note that \mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}
|
|
1371 |
already adds the new simproc to the subsequent context.
|
|
1372 |
|
|
1373 |
\end{descr}%
|
|
1374 |
\end{isamarkuptext}%
|
|
1375 |
\isamarkuptrue%
|
|
1376 |
%
|
|
1377 |
\isamarkupsubsubsection{Forward simplification%
|
|
1378 |
}
|
|
1379 |
\isamarkuptrue%
|
|
1380 |
%
|
|
1381 |
\begin{isamarkuptext}%
|
|
1382 |
\begin{matharray}{rcl}
|
|
1383 |
\indexdef{}{attribute}{simplified}\mbox{\isa{simplified}} & : & \isaratt \\
|
|
1384 |
\end{matharray}
|
|
1385 |
|
|
1386 |
\begin{rail}
|
|
1387 |
'simplified' opt? thmrefs?
|
|
1388 |
;
|
|
1389 |
|
26788
|
1390 |
opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
|
26782
|
1391 |
;
|
|
1392 |
\end{rail}
|
|
1393 |
|
|
1394 |
\begin{descr}
|
|
1395 |
|
26842
|
1396 |
\item [\mbox{\isa{simplified}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}]
|
26782
|
1397 |
causes a theorem to be simplified, either by exactly the specified
|
26842
|
1398 |
rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}}, or the implicit Simplifier
|
26782
|
1399 |
context if no arguments are given. The result is fully simplified
|
|
1400 |
by default, including assumptions and conclusion; the options \isa{no{\isacharunderscore}asm} etc.\ tune the Simplifier in the same way as the for the
|
|
1401 |
\isa{simp} method.
|
|
1402 |
|
|
1403 |
Note that forward simplification restricts the simplifier to its
|
|
1404 |
most basic operation of term rewriting; solver and looper tactics
|
|
1405 |
\cite{isabelle-ref} are \emph{not} involved here. The \isa{simplified} attribute should be only rarely required under normal
|
|
1406 |
circumstances.
|
|
1407 |
|
|
1408 |
\end{descr}%
|
|
1409 |
\end{isamarkuptext}%
|
|
1410 |
\isamarkuptrue%
|
|
1411 |
%
|
|
1412 |
\isamarkupsubsubsection{Low-level equational reasoning%
|
|
1413 |
}
|
|
1414 |
\isamarkuptrue%
|
|
1415 |
%
|
|
1416 |
\begin{isamarkuptext}%
|
|
1417 |
\begin{matharray}{rcl}
|
26842
|
1418 |
\indexdef{}{method}{subst}\mbox{\isa{subst}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
1419 |
\indexdef{}{method}{hypsubst}\mbox{\isa{hypsubst}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
|
1420 |
\indexdef{}{method}{split}\mbox{\isa{split}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
|
26782
|
1421 |
\end{matharray}
|
|
1422 |
|
|
1423 |
\begin{rail}
|
|
1424 |
'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
|
|
1425 |
;
|
|
1426 |
'split' ('(' 'asm' ')')? thmrefs
|
|
1427 |
;
|
|
1428 |
\end{rail}
|
|
1429 |
|
|
1430 |
These methods provide low-level facilities for equational reasoning
|
|
1431 |
that are intended for specialized applications only. Normally,
|
|
1432 |
single step calculations would be performed in a structured text
|
|
1433 |
(see also \secref{sec:calculation}), while the Simplifier methods
|
|
1434 |
provide the canonical way for automated normalization (see
|
|
1435 |
\secref{sec:simplifier}).
|
|
1436 |
|
|
1437 |
\begin{descr}
|
|
1438 |
|
|
1439 |
\item [\mbox{\isa{subst}}~\isa{eq}] performs a single substitution
|
|
1440 |
step using rule \isa{eq}, which may be either a meta or object
|
|
1441 |
equality.
|
|
1442 |
|
26842
|
1443 |
\item [\mbox{\isa{subst}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ eq{\isachardoublequote}}] substitutes in an
|
26782
|
1444 |
assumption.
|
|
1445 |
|
26842
|
1446 |
\item [\mbox{\isa{subst}}~\isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs several
|
26782
|
1447 |
substitutions in the conclusion. The numbers \isa{i} to \isa{j}
|
|
1448 |
indicate the positions to substitute at. Positions are ordered from
|
|
1449 |
the top of the term tree moving down from left to right. For
|
26842
|
1450 |
example, in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}} there are three positions
|
|
1451 |
where commutativity of \isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}} is applicable: 1 refers to the
|
|
1452 |
whole term, 2 to \isa{{\isachardoublequote}a\ {\isacharplus}\ b{\isachardoublequote}} and 3 to \isa{{\isachardoublequote}c\ {\isacharplus}\ d{\isachardoublequote}}.
|
26782
|
1453 |
|
26842
|
1454 |
If the positions in the list \isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}{\isachardoublequote}} are non-overlapping
|
|
1455 |
(e.g.\ \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}\ {\isadigit{3}}{\isacharparenright}{\isachardoublequote}} in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}}) you may
|
26782
|
1456 |
assume all substitutions are performed simultaneously. Otherwise
|
|
1457 |
the behaviour of \isa{subst} is not specified.
|
|
1458 |
|
26842
|
1459 |
\item [\mbox{\isa{subst}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ {\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs the
|
|
1460 |
substitutions in the assumptions. Positions \isa{{\isachardoublequote}{\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{1}}{\isachardoublequote}}
|
|
1461 |
refer to assumption 1, positions \isa{{\isachardoublequote}i\isactrlsub {\isadigit{1}}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{2}}{\isachardoublequote}}
|
26782
|
1462 |
to assumption 2, and so on.
|
|
1463 |
|
|
1464 |
\item [\mbox{\isa{hypsubst}}] performs substitution using some
|
26842
|
1465 |
assumption; this only works for equations of the form \isa{{\isachardoublequote}x\ {\isacharequal}\ t{\isachardoublequote}} where \isa{x} is a free or bound variable.
|
26782
|
1466 |
|
26842
|
1467 |
\item [\mbox{\isa{split}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] performs
|
26782
|
1468 |
single-step case splitting using the given rules. By default,
|
26842
|
1469 |
splitting is performed in the conclusion of a goal; the \isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}{\isachardoublequote}} option indicates to operate on assumptions instead.
|
26782
|
1470 |
|
|
1471 |
Note that the \mbox{\isa{simp}} method already involves repeated
|
|
1472 |
application of split rules as declared in the current context.
|
|
1473 |
|
|
1474 |
\end{descr}%
|
|
1475 |
\end{isamarkuptext}%
|
|
1476 |
\isamarkuptrue%
|
|
1477 |
%
|
|
1478 |
\isamarkupsubsection{The Classical Reasoner \label{sec:classical}%
|
|
1479 |
}
|
|
1480 |
\isamarkuptrue%
|
|
1481 |
%
|
|
1482 |
\isamarkupsubsubsection{Basic methods%
|
|
1483 |
}
|
|
1484 |
\isamarkuptrue%
|
|
1485 |
%
|
|
1486 |
\begin{isamarkuptext}%
|
|
1487 |
\begin{matharray}{rcl}
|
|
1488 |
\indexdef{}{method}{rule}\mbox{\isa{rule}} & : & \isarmeth \\
|
|
1489 |
\indexdef{}{method}{contradiction}\mbox{\isa{contradiction}} & : & \isarmeth \\
|
|
1490 |
\indexdef{}{method}{intro}\mbox{\isa{intro}} & : & \isarmeth \\
|
|
1491 |
\indexdef{}{method}{elim}\mbox{\isa{elim}} & : & \isarmeth \\
|
|
1492 |
\end{matharray}
|
|
1493 |
|
|
1494 |
\begin{rail}
|
|
1495 |
('rule' | 'intro' | 'elim') thmrefs?
|
|
1496 |
;
|
|
1497 |
\end{rail}
|
|
1498 |
|
|
1499 |
\begin{descr}
|
|
1500 |
|
|
1501 |
\item [\mbox{\isa{rule}}] as offered by the Classical Reasoner is a
|
|
1502 |
refinement over the primitive one (see \secref{sec:pure-meth-att}).
|
|
1503 |
Both versions essentially work the same, but the classical version
|
|
1504 |
observes the classical rule context in addition to that of
|
|
1505 |
Isabelle/Pure.
|
|
1506 |
|
|
1507 |
Common object logics (HOL, ZF, etc.) declare a rich collection of
|
|
1508 |
classical rules (even if these would qualify as intuitionistic
|
|
1509 |
ones), but only few declarations to the rule context of
|
|
1510 |
Isabelle/Pure (\secref{sec:pure-meth-att}).
|
|
1511 |
|
|
1512 |
\item [\mbox{\isa{contradiction}}] solves some goal by contradiction,
|
26842
|
1513 |
deriving any result from both \isa{{\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}} and \isa{A}. Chained
|
26782
|
1514 |
facts, which are guaranteed to participate, may appear in either
|
|
1515 |
order.
|
|
1516 |
|
|
1517 |
\item [\mbox{\isa{intro}} and \mbox{\isa{elim}}] repeatedly refine
|
|
1518 |
some goal by intro- or elim-resolution, after having inserted any
|
|
1519 |
chained facts. Exactly the rules given as arguments are taken into
|
|
1520 |
account; this allows fine-tuned decomposition of a proof problem, in
|
|
1521 |
contrast to common automated tools.
|
|
1522 |
|
|
1523 |
\end{descr}%
|
|
1524 |
\end{isamarkuptext}%
|
|
1525 |
\isamarkuptrue%
|
|
1526 |
%
|
|
1527 |
\isamarkupsubsubsection{Automated methods%
|
|
1528 |
}
|
|
1529 |
\isamarkuptrue%
|
|
1530 |
%
|
|
1531 |
\begin{isamarkuptext}%
|
|
1532 |
\begin{matharray}{rcl}
|
|
1533 |
\indexdef{}{method}{blast}\mbox{\isa{blast}} & : & \isarmeth \\
|
|
1534 |
\indexdef{}{method}{fast}\mbox{\isa{fast}} & : & \isarmeth \\
|
|
1535 |
\indexdef{}{method}{slow}\mbox{\isa{slow}} & : & \isarmeth \\
|
|
1536 |
\indexdef{}{method}{best}\mbox{\isa{best}} & : & \isarmeth \\
|
|
1537 |
\indexdef{}{method}{safe}\mbox{\isa{safe}} & : & \isarmeth \\
|
|
1538 |
\indexdef{}{method}{clarify}\mbox{\isa{clarify}} & : & \isarmeth \\
|
|
1539 |
\end{matharray}
|
|
1540 |
|
|
1541 |
\indexouternonterm{clamod}
|
|
1542 |
\begin{rail}
|
|
1543 |
'blast' ('!' ?) nat? (clamod *)
|
|
1544 |
;
|
|
1545 |
('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
|
|
1546 |
;
|
|
1547 |
|
|
1548 |
clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
|
|
1549 |
;
|
|
1550 |
\end{rail}
|
|
1551 |
|
|
1552 |
\begin{descr}
|
|
1553 |
|
|
1554 |
\item [\mbox{\isa{blast}}] refers to the classical tableau prover (see
|
|
1555 |
\verb|blast_tac| in \cite[\S11]{isabelle-ref}). The optional
|
|
1556 |
argument specifies a user-supplied search bound (default 20).
|
|
1557 |
|
|
1558 |
\item [\mbox{\isa{fast}}, \mbox{\isa{slow}}, \mbox{\isa{best}}, \mbox{\isa{safe}}, and \mbox{\isa{clarify}}] refer to the generic classical
|
|
1559 |
reasoner. See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite[\S11]{isabelle-ref} for
|
|
1560 |
more information.
|
|
1561 |
|
|
1562 |
\end{descr}
|
|
1563 |
|
|
1564 |
Any of the above methods support additional modifiers of the context
|
|
1565 |
of classical rules. Their semantics is analogous to the attributes
|
|
1566 |
given before. Facts provided by forward chaining are inserted into
|
26842
|
1567 |
the goal before commencing proof search. The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''~argument causes the full context of assumptions to be
|
26782
|
1568 |
included as well.%
|
|
1569 |
\end{isamarkuptext}%
|
|
1570 |
\isamarkuptrue%
|
|
1571 |
%
|
|
1572 |
\isamarkupsubsubsection{Combined automated methods \label{sec:clasimp}%
|
|
1573 |
}
|
|
1574 |
\isamarkuptrue%
|
|
1575 |
%
|
|
1576 |
\begin{isamarkuptext}%
|
|
1577 |
\begin{matharray}{rcl}
|
|
1578 |
\indexdef{}{method}{auto}\mbox{\isa{auto}} & : & \isarmeth \\
|
|
1579 |
\indexdef{}{method}{force}\mbox{\isa{force}} & : & \isarmeth \\
|
|
1580 |
\indexdef{}{method}{clarsimp}\mbox{\isa{clarsimp}} & : & \isarmeth \\
|
|
1581 |
\indexdef{}{method}{fastsimp}\mbox{\isa{fastsimp}} & : & \isarmeth \\
|
|
1582 |
\indexdef{}{method}{slowsimp}\mbox{\isa{slowsimp}} & : & \isarmeth \\
|
|
1583 |
\indexdef{}{method}{bestsimp}\mbox{\isa{bestsimp}} & : & \isarmeth \\
|
|
1584 |
\end{matharray}
|
|
1585 |
|
|
1586 |
\indexouternonterm{clasimpmod}
|
|
1587 |
\begin{rail}
|
|
1588 |
'auto' '!'? (nat nat)? (clasimpmod *)
|
|
1589 |
;
|
|
1590 |
('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
|
|
1591 |
;
|
|
1592 |
|
|
1593 |
clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
|
|
1594 |
('cong' | 'split') (() | 'add' | 'del') |
|
|
1595 |
'iff' (((() | 'add') '?'?) | 'del') |
|
|
1596 |
(('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
|
|
1597 |
\end{rail}
|
|
1598 |
|
|
1599 |
\begin{descr}
|
|
1600 |
|
|
1601 |
\item [\mbox{\isa{auto}}, \mbox{\isa{force}}, \mbox{\isa{clarsimp}}, \mbox{\isa{fastsimp}}, \mbox{\isa{slowsimp}}, and \mbox{\isa{bestsimp}}] provide
|
|
1602 |
access to Isabelle's combined simplification and classical reasoning
|
|
1603 |
tactics. These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier
|
|
1604 |
added as wrapper, see \cite[\S11]{isabelle-ref} for more
|
|
1605 |
information. The modifier arguments correspond to those given in
|
|
1606 |
\secref{sec:simplifier} and \secref{sec:classical}. Just note that
|
|
1607 |
the ones related to the Simplifier are prefixed by \railtterm{simp}
|
|
1608 |
here.
|
|
1609 |
|
|
1610 |
Facts provided by forward chaining are inserted into the goal before
|
26842
|
1611 |
doing the search. The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' argument causes the full
|
26782
|
1612 |
context of assumptions to be included as well.
|
|
1613 |
|
|
1614 |
\end{descr}%
|
|
1615 |
\end{isamarkuptext}%
|
|
1616 |
\isamarkuptrue%
|
|
1617 |
%
|
|
1618 |
\isamarkupsubsubsection{Declaring rules%
|
|
1619 |
}
|
|
1620 |
\isamarkuptrue%
|
|
1621 |
%
|
|
1622 |
\begin{isamarkuptext}%
|
|
1623 |
\begin{matharray}{rcl}
|
26842
|
1624 |
\indexdef{}{command}{print-claset}\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
26782
|
1625 |
\indexdef{}{attribute}{intro}\mbox{\isa{intro}} & : & \isaratt \\
|
|
1626 |
\indexdef{}{attribute}{elim}\mbox{\isa{elim}} & : & \isaratt \\
|
|
1627 |
\indexdef{}{attribute}{dest}\mbox{\isa{dest}} & : & \isaratt \\
|
|
1628 |
\indexdef{}{attribute}{rule}\mbox{\isa{rule}} & : & \isaratt \\
|
|
1629 |
\indexdef{}{attribute}{iff}\mbox{\isa{iff}} & : & \isaratt \\
|
|
1630 |
\end{matharray}
|
|
1631 |
|
|
1632 |
\begin{rail}
|
|
1633 |
('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
|
|
1634 |
;
|
|
1635 |
'rule' 'del'
|
|
1636 |
;
|
|
1637 |
'iff' (((() | 'add') '?'?) | 'del')
|
|
1638 |
;
|
|
1639 |
\end{rail}
|
|
1640 |
|
|
1641 |
\begin{descr}
|
|
1642 |
|
|
1643 |
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}] prints the collection of rules
|
|
1644 |
declared to the Classical Reasoner, which is also known as
|
|
1645 |
``claset'' internally \cite{isabelle-ref}.
|
|
1646 |
|
|
1647 |
\item [\mbox{\isa{intro}}, \mbox{\isa{elim}}, and \mbox{\isa{dest}}]
|
|
1648 |
declare introduction, elimination, and destruction rules,
|
|
1649 |
respectively. By default, rules are considered as \emph{unsafe}
|
26842
|
1650 |
(i.e.\ not applied blindly without backtracking), while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' classifies as \emph{safe}. Rule declarations marked by
|
|
1651 |
``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' coincide with those of Isabelle/Pure, cf.\
|
26782
|
1652 |
\secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
|
|
1653 |
of the \mbox{\isa{rule}} method). The optional natural number
|
|
1654 |
specifies an explicit weight argument, which is ignored by automated
|
|
1655 |
tools, but determines the search order of single rule steps.
|
|
1656 |
|
|
1657 |
\item [\mbox{\isa{rule}}~\isa{del}] deletes introduction,
|
|
1658 |
elimination, or destruction rules from the context.
|
|
1659 |
|
|
1660 |
\item [\mbox{\isa{iff}}] declares logical equivalences to the
|
|
1661 |
Simplifier and the Classical reasoner at the same time.
|
|
1662 |
Non-conditional rules result in a ``safe'' introduction and
|
|
1663 |
elimination pair; conditional ones are considered ``unsafe''. Rules
|
26842
|
1664 |
with negative conclusion are automatically inverted (using \isa{{\isachardoublequote}{\isasymnot}{\isachardoublequote}}-elimination internally).
|
26782
|
1665 |
|
26842
|
1666 |
The ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' version of \mbox{\isa{iff}} declares rules to
|
26782
|
1667 |
the Isabelle/Pure context only, and omits the Simplifier
|
|
1668 |
declaration.
|
|
1669 |
|
|
1670 |
\end{descr}%
|
|
1671 |
\end{isamarkuptext}%
|
|
1672 |
\isamarkuptrue%
|
|
1673 |
%
|
|
1674 |
\isamarkupsubsubsection{Classical operations%
|
|
1675 |
}
|
|
1676 |
\isamarkuptrue%
|
|
1677 |
%
|
|
1678 |
\begin{isamarkuptext}%
|
|
1679 |
\begin{matharray}{rcl}
|
|
1680 |
\indexdef{}{attribute}{swapped}\mbox{\isa{swapped}} & : & \isaratt \\
|
|
1681 |
\end{matharray}
|
|
1682 |
|
|
1683 |
\begin{descr}
|
|
1684 |
|
|
1685 |
\item [\mbox{\isa{swapped}}] turns an introduction rule into an
|
26842
|
1686 |
elimination, by resolving with the classical swap principle \isa{{\isachardoublequote}{\isacharparenleft}{\isasymnot}\ B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymLongrightarrow}\ B{\isacharparenright}{\isachardoublequote}}.
|
26782
|
1687 |
|
|
1688 |
\end{descr}%
|
|
1689 |
\end{isamarkuptext}%
|
|
1690 |
\isamarkuptrue%
|
|
1691 |
%
|
|
1692 |
\isamarkupsubsection{Proof by cases and induction \label{sec:cases-induct}%
|
|
1693 |
}
|
|
1694 |
\isamarkuptrue%
|
|
1695 |
%
|
|
1696 |
\isamarkupsubsubsection{Rule contexts%
|
|
1697 |
}
|
|
1698 |
\isamarkuptrue%
|
|
1699 |
%
|
|
1700 |
\begin{isamarkuptext}%
|
|
1701 |
\begin{matharray}{rcl}
|
|
1702 |
\indexdef{}{command}{case}\mbox{\isa{\isacommand{case}}} & : & \isartrans{proof(state)}{proof(state)} \\
|
26842
|
1703 |
\indexdef{}{command}{print-cases}\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
|
26782
|
1704 |
\indexdef{}{attribute}{case-names}\mbox{\isa{case{\isacharunderscore}names}} & : & \isaratt \\
|
|
1705 |
\indexdef{}{attribute}{case-conclusion}\mbox{\isa{case{\isacharunderscore}conclusion}} & : & \isaratt \\
|
|
1706 |
\indexdef{}{attribute}{params}\mbox{\isa{params}} & : & \isaratt \\
|
|
1707 |
\indexdef{}{attribute}{consumes}\mbox{\isa{consumes}} & : & \isaratt \\
|
|
1708 |
\end{matharray}
|
|
1709 |
|
|
1710 |
The puristic way to build up Isar proof contexts is by explicit
|
|
1711 |
language elements like \mbox{\isa{\isacommand{fix}}}, \mbox{\isa{\isacommand{assume}}},
|
|
1712 |
\mbox{\isa{\isacommand{let}}} (see \secref{sec:proof-context}). This is adequate
|
|
1713 |
for plain natural deduction, but easily becomes unwieldy in concrete
|
|
1714 |
verification tasks, which typically involve big induction rules with
|
|
1715 |
several cases.
|
|
1716 |
|
|
1717 |
The \mbox{\isa{\isacommand{case}}} command provides a shorthand to refer to a
|
|
1718 |
local context symbolically: certain proof methods provide an
|
26842
|
1719 |
environment of named ``cases'' of the form \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}; the effect of ``\mbox{\isa{\isacommand{case}}}~\isa{c}'' is then equivalent to ``\mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''. Term bindings may be covered as well, notably
|
26788
|
1720 |
\mbox{\isa{{\isacharquery}case}} for the main conclusion.
|
26782
|
1721 |
|
26842
|
1722 |
By default, the ``terminology'' \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of
|
26782
|
1723 |
a case value is marked as hidden, i.e.\ there is no way to refer to
|
|
1724 |
such parameters in the subsequent proof text. After all, original
|
|
1725 |
rule parameters stem from somewhere outside of the current proof
|
26842
|
1726 |
text. By using the explicit form ``\mbox{\isa{\isacommand{case}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ y\isactrlsub {\isadigit{1}}\ {\isasymdots}\ y\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' instead, the proof author is able to
|
26782
|
1727 |
chose local names that fit nicely into the current context.
|
|
1728 |
|
|
1729 |
\medskip It is important to note that proper use of \mbox{\isa{\isacommand{case}}} does not provide means to peek at the current goal state,
|
|
1730 |
which is not directly observable in Isar! Nonetheless, goal
|
26842
|
1731 |
refinement commands do provide named cases \isa{{\isachardoublequote}goal\isactrlsub i{\isachardoublequote}}
|
|
1732 |
for each subgoal \isa{{\isachardoublequote}i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of the resulting goal state.
|
26782
|
1733 |
Using this extra feature requires great care, because some bits of
|
|
1734 |
the internal tactical machinery intrude the proof text. In
|
|
1735 |
particular, parameter names stemming from the left-over of automated
|
|
1736 |
reasoning tools are usually quite unpredictable.
|
|
1737 |
|
|
1738 |
Under normal circumstances, the text of cases emerge from standard
|
|
1739 |
elimination or induction rules, which in turn are derived from
|
|
1740 |
previous theory specifications in a canonical way (say from
|
|
1741 |
\mbox{\isa{\isacommand{inductive}}} definitions).
|
|
1742 |
|
|
1743 |
\medskip Proper cases are only available if both the proof method
|
|
1744 |
and the rules involved support this. By using appropriate
|
|
1745 |
attributes, case names, conclusions, and parameters may be also
|
|
1746 |
declared by hand. Thus variant versions of rules that have been
|
|
1747 |
derived manually become ready to use in advanced case analysis
|
|
1748 |
later.
|
|
1749 |
|
|
1750 |
\begin{rail}
|
|
1751 |
'case' (caseref | '(' caseref ((name | underscore) +) ')')
|
|
1752 |
;
|
|
1753 |
caseref: nameref attributes?
|
|
1754 |
;
|
|
1755 |
|
|
1756 |
'case\_names' (name +)
|
|
1757 |
;
|
|
1758 |
'case\_conclusion' name (name *)
|
|
1759 |
;
|
|
1760 |
'params' ((name *) + 'and')
|
|
1761 |
;
|
|
1762 |
'consumes' nat?
|
|
1763 |
;
|
|
1764 |
\end{rail}
|
|
1765 |
|
|
1766 |
\begin{descr}
|
|
1767 |
|
26842
|
1768 |
\item [\mbox{\isa{\isacommand{case}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}]
|
|
1769 |
invokes a named local context \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub m{\isachardoublequote}}, as provided by an appropriate
|
26782
|
1770 |
proof method (such as \indexref{}{method}{cases}\mbox{\isa{cases}} and \indexref{}{method}{induct}\mbox{\isa{induct}}).
|
26842
|
1771 |
The command ``\mbox{\isa{\isacommand{case}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' abbreviates ``\mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''.
|
26782
|
1772 |
|
|
1773 |
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}] prints all local contexts of the
|
|
1774 |
current state, using Isar proof language notation.
|
|
1775 |
|
26842
|
1776 |
\item [\mbox{\isa{case{\isacharunderscore}names}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k{\isachardoublequote}}]
|
26782
|
1777 |
declares names for the local contexts of premises of a theorem;
|
26842
|
1778 |
\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k{\isachardoublequote}} refers to the \emph{suffix} of the
|
26782
|
1779 |
list of premises.
|
|
1780 |
|
26842
|
1781 |
\item [\mbox{\isa{case{\isacharunderscore}conclusion}}~\isa{{\isachardoublequote}c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k{\isachardoublequote}}] declares names for the conclusions of a named premise
|
|
1782 |
\isa{c}; here \isa{{\isachardoublequote}d\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlsub k{\isachardoublequote}} refers to the
|
26782
|
1783 |
prefix of arguments of a logical formula built by nesting a binary
|
26842
|
1784 |
connective (e.g.\ \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}).
|
26782
|
1785 |
|
|
1786 |
Note that proof methods such as \mbox{\isa{induct}} and \mbox{\isa{coinduct}} already provide a default name for the conclusion as a
|
|
1787 |
whole. The need to name subformulas only arises with cases that
|
|
1788 |
split into several sub-cases, as in common co-induction rules.
|
|
1789 |
|
26842
|
1790 |
\item [\mbox{\isa{params}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] renames the innermost parameters of
|
|
1791 |
premises \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of some theorem. An empty list of names
|
26782
|
1792 |
may be given to skip positions, leaving the present parameters
|
|
1793 |
unchanged.
|
|
1794 |
|
|
1795 |
Note that the default usage of case rules does \emph{not} directly
|
|
1796 |
expose parameters to the proof context.
|
|
1797 |
|
|
1798 |
\item [\mbox{\isa{consumes}}~\isa{n}] declares the number of
|
|
1799 |
``major premises'' of a rule, i.e.\ the number of facts to be
|
|
1800 |
consumed when it is applied by an appropriate proof method. The
|
26842
|
1801 |
default value of \mbox{\isa{consumes}} is \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}, which is
|
26782
|
1802 |
appropriate for the usual kind of cases and induction rules for
|
|
1803 |
inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any
|
|
1804 |
\mbox{\isa{consumes}} declaration given are treated as if
|
|
1805 |
\mbox{\isa{consumes}}~\isa{{\isadigit{0}}} had been specified.
|
|
1806 |
|
|
1807 |
Note that explicit \mbox{\isa{consumes}} declarations are only
|
|
1808 |
rarely needed; this is already taken care of automatically by the
|
|
1809 |
higher-level \mbox{\isa{cases}}, \mbox{\isa{induct}}, and
|
|
1810 |
\mbox{\isa{coinduct}} declarations.
|
|
1811 |
|
|
1812 |
\end{descr}%
|
|
1813 |
\end{isamarkuptext}%
|
|
1814 |
\isamarkuptrue%
|
|
1815 |
%
|
|
1816 |
\isamarkupsubsubsection{Proof methods%
|
|
1817 |
}
|
|
1818 |
\isamarkuptrue%
|
|
1819 |
%
|
|
1820 |
\begin{isamarkuptext}%
|
|
1821 |
\begin{matharray}{rcl}
|
|
1822 |
\indexdef{}{method}{cases}\mbox{\isa{cases}} & : & \isarmeth \\
|
|
1823 |
\indexdef{}{method}{induct}\mbox{\isa{induct}} & : & \isarmeth \\
|
|
1824 |
\indexdef{}{method}{coinduct}\mbox{\isa{coinduct}} & : & \isarmeth \\
|
|
1825 |
\end{matharray}
|
|
1826 |
|
|
1827 |
The \mbox{\isa{cases}}, \mbox{\isa{induct}}, and \mbox{\isa{coinduct}}
|
|
1828 |
methods provide a uniform interface to common proof techniques over
|
|
1829 |
datatypes, inductive predicates (or sets), recursive functions etc.
|
|
1830 |
The corresponding rules may be specified and instantiated in a
|
|
1831 |
casual manner. Furthermore, these methods provide named local
|
|
1832 |
contexts that may be invoked via the \mbox{\isa{\isacommand{case}}} proof command
|
|
1833 |
within the subsequent proof text. This accommodates compact proof
|
|
1834 |
texts even when reasoning about large specifications.
|
|
1835 |
|
|
1836 |
The \mbox{\isa{induct}} method also provides some additional
|
|
1837 |
infrastructure in order to be applicable to structure statements
|
|
1838 |
(either using explicit meta-level connectives, or including facts
|
|
1839 |
and parameters separately). This avoids cumbersome encoding of
|
|
1840 |
``strengthened'' inductive statements within the object-logic.
|
|
1841 |
|
|
1842 |
\begin{rail}
|
|
1843 |
'cases' (insts * 'and') rule?
|
|
1844 |
;
|
|
1845 |
'induct' (definsts * 'and') \\ arbitrary? taking? rule?
|
|
1846 |
;
|
|
1847 |
'coinduct' insts taking rule?
|
|
1848 |
;
|
|
1849 |
|
|
1850 |
rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
|
|
1851 |
;
|
|
1852 |
definst: name ('==' | equiv) term | inst
|
|
1853 |
;
|
|
1854 |
definsts: ( definst *)
|
|
1855 |
;
|
|
1856 |
arbitrary: 'arbitrary' ':' ((term *) 'and' +)
|
|
1857 |
;
|
|
1858 |
taking: 'taking' ':' insts
|
|
1859 |
;
|
|
1860 |
\end{rail}
|
|
1861 |
|
|
1862 |
\begin{descr}
|
|
1863 |
|
26842
|
1864 |
\item [\mbox{\isa{cases}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] applies method \mbox{\isa{rule}} with an appropriate case distinction theorem, instantiated to
|
26782
|
1865 |
the subjects \isa{insts}. Symbolic case names are bound according
|
|
1866 |
to the rule's local contexts.
|
|
1867 |
|
|
1868 |
The rule is determined as follows, according to the facts and
|
|
1869 |
arguments passed to the \mbox{\isa{cases}} method:
|
|
1870 |
|
|
1871 |
\medskip
|
|
1872 |
\begin{tabular}{llll}
|
26788
|
1873 |
facts & & arguments & rule \\\hline
|
|
1874 |
& \mbox{\isa{cases}} & & classical case split \\
|
|
1875 |
& \mbox{\isa{cases}} & \isa{t} & datatype exhaustion (type of \isa{t}) \\
|
26842
|
1876 |
\isa{{\isachardoublequote}{\isasymturnstile}\ A\ t{\isachardoublequote}} & \mbox{\isa{cases}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & inductive predicate/set elimination (of \isa{A}) \\
|
|
1877 |
\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \mbox{\isa{cases}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
|
26782
|
1878 |
\end{tabular}
|
|
1879 |
\medskip
|
|
1880 |
|
|
1881 |
Several instantiations may be given, referring to the \emph{suffix}
|
|
1882 |
of premises of the case rule; within each premise, the \emph{prefix}
|
|
1883 |
of variables is instantiated. In most situations, only a single
|
|
1884 |
term needs to be specified; this refers to the first variable of the
|
|
1885 |
last premise (it is usually the same for all cases).
|
|
1886 |
|
26842
|
1887 |
\item [\mbox{\isa{induct}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] is analogous to the
|
26782
|
1888 |
\mbox{\isa{cases}} method, but refers to induction rules, which are
|
|
1889 |
determined as follows:
|
|
1890 |
|
|
1891 |
\medskip
|
|
1892 |
\begin{tabular}{llll}
|
26788
|
1893 |
facts & & arguments & rule \\\hline
|
26842
|
1894 |
& \mbox{\isa{induct}} & \isa{{\isachardoublequote}P\ x{\isachardoublequote}} & datatype induction (type of \isa{x}) \\
|
|
1895 |
\isa{{\isachardoublequote}{\isasymturnstile}\ A\ x{\isachardoublequote}} & \mbox{\isa{induct}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set induction (of \isa{A}) \\
|
|
1896 |
\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \mbox{\isa{induct}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
|
26782
|
1897 |
\end{tabular}
|
|
1898 |
\medskip
|
|
1899 |
|
|
1900 |
Several instantiations may be given, each referring to some part of
|
|
1901 |
a mutual inductive definition or datatype --- only related partial
|
|
1902 |
induction rules may be used together, though. Any of the lists of
|
26842
|
1903 |
terms \isa{{\isachardoublequote}P{\isacharcomma}\ x{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} refers to the \emph{suffix} of variables
|
26782
|
1904 |
present in the induction rule. This enables the writer to specify
|
|
1905 |
only induction variables, or both predicates and variables, for
|
|
1906 |
example.
|
|
1907 |
|
26842
|
1908 |
Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}
|
26782
|
1909 |
introduce local definitions, which are inserted into the claim and
|
|
1910 |
discharged after applying the induction rule. Equalities reappear
|
|
1911 |
in the inductive cases, but have been transformed according to the
|
|
1912 |
induction principle being involved here. In order to achieve
|
|
1913 |
practically useful induction hypotheses, some variables occurring in
|
|
1914 |
\isa{t} need to be fixed (see below).
|
|
1915 |
|
26842
|
1916 |
The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
|
|
1917 |
specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction. Thus
|
26782
|
1918 |
induction hypotheses may become sufficiently general to get the
|
|
1919 |
proof through. Together with definitional instantiations, one may
|
|
1920 |
effectively perform induction over expressions of a certain
|
|
1921 |
structure.
|
|
1922 |
|
26842
|
1923 |
The optional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
|
26782
|
1924 |
specification provides additional instantiations of a prefix of
|
|
1925 |
pending variables in the rule. Such schematic induction rules
|
|
1926 |
rarely occur in practice, though.
|
|
1927 |
|
26842
|
1928 |
\item [\mbox{\isa{coinduct}}~\isa{{\isachardoublequote}inst\ R{\isachardoublequote}}] is analogous to the
|
26782
|
1929 |
\mbox{\isa{induct}} method, but refers to coinduction rules, which are
|
|
1930 |
determined as follows:
|
|
1931 |
|
|
1932 |
\medskip
|
|
1933 |
\begin{tabular}{llll}
|
26788
|
1934 |
goal & & arguments & rule \\\hline
|
|
1935 |
& \mbox{\isa{coinduct}} & \isa{x} & type coinduction (type of \isa{x}) \\
|
26842
|
1936 |
\isa{{\isachardoublequote}A\ x{\isachardoublequote}} & \mbox{\isa{coinduct}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set coinduction (of \isa{A}) \\
|
|
1937 |
\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \mbox{\isa{coinduct}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
|
26782
|
1938 |
\end{tabular}
|
|
1939 |
|
|
1940 |
Coinduction is the dual of induction. Induction essentially
|
26842
|
1941 |
eliminates \isa{{\isachardoublequote}A\ x{\isachardoublequote}} towards a generic result \isa{{\isachardoublequote}P\ x{\isachardoublequote}},
|
|
1942 |
while coinduction introduces \isa{{\isachardoublequote}A\ x{\isachardoublequote}} starting with \isa{{\isachardoublequote}B\ x{\isachardoublequote}}, for a suitable ``bisimulation'' \isa{B}. The cases of a
|
26782
|
1943 |
coinduct rule are typically named after the predicates or sets being
|
|
1944 |
covered, while the conclusions consist of several alternatives being
|
|
1945 |
named after the individual destructor patterns.
|
|
1946 |
|
|
1947 |
The given instantiation refers to the \emph{suffix} of variables
|
|
1948 |
occurring in the rule's major premise, or conclusion if unavailable.
|
26842
|
1949 |
An additional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
|
26782
|
1950 |
specification may be required in order to specify the bisimulation
|
|
1951 |
to be used in the coinduction step.
|
|
1952 |
|
|
1953 |
\end{descr}
|
|
1954 |
|
|
1955 |
Above methods produce named local contexts, as determined by the
|
|
1956 |
instantiated rule as given in the text. Beyond that, the \mbox{\isa{induct}} and \mbox{\isa{coinduct}} methods guess further instantiations
|
|
1957 |
from the goal specification itself. Any persisting unresolved
|
|
1958 |
schematic variables of the resulting rule will render the the
|
|
1959 |
corresponding case invalid. The term binding \mbox{\isa{{\isacharquery}case}} for
|
|
1960 |
the conclusion will be provided with each case, provided that term
|
|
1961 |
is fully specified.
|
|
1962 |
|
|
1963 |
The \mbox{\isa{\isacommand{print{\isacharunderscore}cases}}} command prints all named cases present
|
|
1964 |
in the current proof state.
|
|
1965 |
|
|
1966 |
\medskip Despite the additional infrastructure, both \mbox{\isa{cases}}
|
|
1967 |
and \mbox{\isa{coinduct}} merely apply a certain rule, after
|
|
1968 |
instantiation, while conforming due to the usual way of monotonic
|
26842
|
1969 |
natural deduction: the context of a structured statement \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ {\isasymdots}{\isachardoublequote}}
|
26782
|
1970 |
reappears unchanged after the case split.
|
|
1971 |
|
|
1972 |
The \mbox{\isa{induct}} method is fundamentally different in this
|
|
1973 |
respect: the meta-level structure is passed through the
|
|
1974 |
``recursive'' course involved in the induction. Thus the original
|
|
1975 |
statement is basically replaced by separate copies, corresponding to
|
|
1976 |
the induction hypotheses and conclusion; the original goal context
|
|
1977 |
is no longer available. Thus local assumptions, fixed parameters
|
|
1978 |
and definitions effectively participate in the inductive rephrasing
|
|
1979 |
of the original statement.
|
|
1980 |
|
|
1981 |
In induction proofs, local assumptions introduced by cases are split
|
|
1982 |
into two different kinds: \isa{hyps} stemming from the rule and
|
|
1983 |
\isa{prems} from the goal statement. This is reflected in the
|
|
1984 |
extracted cases accordingly, so invoking ``\mbox{\isa{\isacommand{case}}}~\isa{c}'' will provide separate facts \isa{c{\isachardot}hyps} and \isa{c{\isachardot}prems},
|
|
1985 |
as well as fact \isa{c} to hold the all-inclusive list.
|
|
1986 |
|
|
1987 |
\medskip Facts presented to either method are consumed according to
|
|
1988 |
the number of ``major premises'' of the rule involved, which is
|
|
1989 |
usually 0 for plain cases and induction rules of datatypes etc.\ and
|
|
1990 |
1 for rules of inductive predicates or sets and the like. The
|
|
1991 |
remaining facts are inserted into the goal verbatim before the
|
|
1992 |
actual \isa{cases}, \isa{induct}, or \isa{coinduct} rule is
|
|
1993 |
applied.%
|
|
1994 |
\end{isamarkuptext}%
|
|
1995 |
\isamarkuptrue%
|
|
1996 |
%
|
|
1997 |
\isamarkupsubsubsection{Declaring rules%
|
|
1998 |
}
|
|
1999 |
\isamarkuptrue%
|
|
2000 |
%
|
|
2001 |
\begin{isamarkuptext}%
|
|
2002 |
\begin{matharray}{rcl}
|
26842
|
2003 |
\indexdef{}{command}{print-induct-rules}\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
26782
|
2004 |
\indexdef{}{attribute}{cases}\mbox{\isa{cases}} & : & \isaratt \\
|
|
2005 |
\indexdef{}{attribute}{induct}\mbox{\isa{induct}} & : & \isaratt \\
|
|
2006 |
\indexdef{}{attribute}{coinduct}\mbox{\isa{coinduct}} & : & \isaratt \\
|
|
2007 |
\end{matharray}
|
|
2008 |
|
|
2009 |
\begin{rail}
|
|
2010 |
'cases' spec
|
|
2011 |
;
|
|
2012 |
'induct' spec
|
|
2013 |
;
|
|
2014 |
'coinduct' spec
|
|
2015 |
;
|
|
2016 |
|
|
2017 |
spec: ('type' | 'pred' | 'set') ':' nameref
|
|
2018 |
;
|
|
2019 |
\end{rail}
|
|
2020 |
|
|
2021 |
\begin{descr}
|
|
2022 |
|
|
2023 |
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}] prints cases and induct
|
|
2024 |
rules for predicates (or sets) and types of the current context.
|
|
2025 |
|
|
2026 |
\item [\mbox{\isa{cases}}, \mbox{\isa{induct}}, and \mbox{\isa{coinduct}}] (as attributes) augment the corresponding context of
|
|
2027 |
rules for reasoning about (co)inductive predicates (or sets) and
|
|
2028 |
types, using the corresponding methods of the same name. Certain
|
|
2029 |
definitional packages of object-logics usually declare emerging
|
|
2030 |
cases and induction rules as expected, so users rarely need to
|
|
2031 |
intervene.
|
|
2032 |
|
|
2033 |
Manual rule declarations usually refer to the \mbox{\isa{case{\isacharunderscore}names}} and \mbox{\isa{params}} attributes to adjust names of
|
|
2034 |
cases and parameters of a rule; the \mbox{\isa{consumes}}
|
|
2035 |
declaration is taken care of automatically: \mbox{\isa{consumes}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \mbox{\isa{consumes}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules.
|
|
2036 |
|
|
2037 |
\end{descr}%
|
|
2038 |
\end{isamarkuptext}%
|
|
2039 |
\isamarkuptrue%
|
|
2040 |
%
|
26790
|
2041 |
\isamarkupsection{General logic setup \label{sec:object-logic}%
|
|
2042 |
}
|
|
2043 |
\isamarkuptrue%
|
|
2044 |
%
|
|
2045 |
\begin{isamarkuptext}%
|
|
2046 |
\begin{matharray}{rcl}
|
|
2047 |
\indexdef{}{command}{judgment}\mbox{\isa{\isacommand{judgment}}} & : & \isartrans{theory}{theory} \\
|
|
2048 |
\indexdef{}{method}{atomize}\mbox{\isa{atomize}} & : & \isarmeth \\
|
|
2049 |
\indexdef{}{attribute}{atomize}\mbox{\isa{atomize}} & : & \isaratt \\
|
|
2050 |
\indexdef{}{attribute}{rule-format}\mbox{\isa{rule{\isacharunderscore}format}} & : & \isaratt \\
|
|
2051 |
\indexdef{}{attribute}{rulify}\mbox{\isa{rulify}} & : & \isaratt \\
|
|
2052 |
\end{matharray}
|
|
2053 |
|
|
2054 |
The very starting point for any Isabelle object-logic is a ``truth
|
|
2055 |
judgment'' that links object-level statements to the meta-logic
|
|
2056 |
(with its minimal language of \isa{prop} that covers universal
|
26842
|
2057 |
quantification \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and implication \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}).
|
26790
|
2058 |
|
|
2059 |
Common object-logics are sufficiently expressive to internalize rule
|
26842
|
2060 |
statements over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} within their own
|
26790
|
2061 |
language. This is useful in certain situations where a rule needs
|
|
2062 |
to be viewed as an atomic statement from the meta-level perspective,
|
26842
|
2063 |
e.g.\ \isa{{\isachardoublequote}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}} versus \isa{{\isachardoublequote}{\isasymforall}x\ {\isasymin}\ A{\isachardot}\ P\ x{\isachardoublequote}}.
|
26790
|
2064 |
|
|
2065 |
From the following language elements, only the \mbox{\isa{atomize}}
|
|
2066 |
method and \mbox{\isa{rule{\isacharunderscore}format}} attribute are occasionally
|
|
2067 |
required by end-users, the rest is for those who need to setup their
|
|
2068 |
own object-logic. In the latter case existing formulations of
|
|
2069 |
Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
|
|
2070 |
|
|
2071 |
Generic tools may refer to the information provided by object-logic
|
|
2072 |
declarations internally.
|
|
2073 |
|
|
2074 |
\begin{rail}
|
|
2075 |
'judgment' constdecl
|
|
2076 |
;
|
|
2077 |
'atomize' ('(' 'full' ')')?
|
|
2078 |
;
|
|
2079 |
'rule\_format' ('(' 'noasm' ')')?
|
|
2080 |
;
|
|
2081 |
\end{rail}
|
|
2082 |
|
|
2083 |
\begin{descr}
|
|
2084 |
|
26842
|
2085 |
\item [\mbox{\isa{\isacommand{judgment}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares
|
26790
|
2086 |
constant \isa{c} as the truth judgment of the current
|
|
2087 |
object-logic. Its type \isa{{\isasymsigma}} should specify a coercion of the
|
|
2088 |
category of object-level propositions to \isa{prop} of the Pure
|
26842
|
2089 |
meta-logic; the mixfix annotation \isa{{\isachardoublequote}{\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} would typically
|
26790
|
2090 |
just link the object language (internally of syntactic category
|
|
2091 |
\isa{logic}) with that of \isa{prop}. Only one \mbox{\isa{\isacommand{judgment}}} declaration may be given in any theory development.
|
|
2092 |
|
|
2093 |
\item [\mbox{\isa{atomize}} (as a method)] rewrites any non-atomic
|
|
2094 |
premises of a sub-goal, using the meta-level equations declared via
|
|
2095 |
\mbox{\isa{atomize}} (as an attribute) beforehand. As a result,
|
|
2096 |
heavily nested goals become amenable to fundamental operations such
|
26842
|
2097 |
as resolution (cf.\ the \mbox{\isa{rule}} method). Giving the ``\isa{{\isachardoublequote}{\isacharparenleft}full{\isacharparenright}{\isachardoublequote}}'' option here means to turn the whole subgoal into an
|
26790
|
2098 |
object-statement (if possible), including the outermost parameters
|
|
2099 |
and assumptions as well.
|
|
2100 |
|
|
2101 |
A typical collection of \mbox{\isa{atomize}} rules for a particular
|
|
2102 |
object-logic would provide an internalization for each of the
|
26842
|
2103 |
connectives of \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}, and \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}}.
|
26790
|
2104 |
Meta-level conjunction should be covered as well (this is
|
|
2105 |
particularly important for locales, see \secref{sec:locale}).
|
|
2106 |
|
|
2107 |
\item [\mbox{\isa{rule{\isacharunderscore}format}}] rewrites a theorem by the
|
|
2108 |
equalities declared as \mbox{\isa{rulify}} rules in the current
|
|
2109 |
object-logic. By default, the result is fully normalized, including
|
26842
|
2110 |
assumptions and conclusions at any depth. The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}}
|
26790
|
2111 |
option restricts the transformation to the conclusion of a rule.
|
|
2112 |
|
|
2113 |
In common object-logics (HOL, FOL, ZF), the effect of \mbox{\isa{rule{\isacharunderscore}format}} is to replace (bounded) universal quantification
|
26842
|
2114 |
(\isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}}) and implication (\isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}}) by the corresponding
|
|
2115 |
rule statements over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}.
|
26790
|
2116 |
|
|
2117 |
\end{descr}%
|
|
2118 |
\end{isamarkuptext}%
|
|
2119 |
\isamarkuptrue%
|
|
2120 |
%
|
26782
|
2121 |
\isadelimtheory
|
|
2122 |
%
|
|
2123 |
\endisadelimtheory
|
|
2124 |
%
|
|
2125 |
\isatagtheory
|
|
2126 |
\isacommand{end}\isamarkupfalse%
|
|
2127 |
%
|
|
2128 |
\endisatagtheory
|
|
2129 |
{\isafoldtheory}%
|
|
2130 |
%
|
|
2131 |
\isadelimtheory
|
|
2132 |
%
|
|
2133 |
\endisadelimtheory
|
|
2134 |
\isanewline
|
|
2135 |
\end{isabellebody}%
|
|
2136 |
%%% Local Variables:
|
|
2137 |
%%% mode: latex
|
|
2138 |
%%% TeX-master: "root"
|
|
2139 |
%%% End:
|