Made doc compatible with the system.
7 chapter {* Theory specifications *}
9 section {* Defining theories \label{sec:begin-thy} *}
12 \begin{matharray}{rcl}
13 @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\
14 @{command_def (global) "end"} & : & \isartrans{theory}{toplevel} \\
17 Isabelle/Isar theories are defined via theory file, which contain
18 both specifications and proofs; occasionally definitional mechanisms
19 also require some explicit proof. The theory body may be
20 sub-structered by means of \emph{local theory} target mechanisms,
21 notably @{command "locale"} and @{command "class"}.
23 The first ``real'' command of any theory has to be @{command
24 "theory"}, which starts a new theory based on the merge of existing
25 ones. Just preceding the @{command "theory"} keyword, there may be
26 an optional @{command "header"} declaration, which is relevant to
27 document preparation only; it acts very much like a special
28 pre-theory markup command (cf.\ \secref{sec:markup}). The @{command
29 (global) "end"} command concludes a theory development; it has to be
30 the very last command of any theory file loaded in batch-mode.
33 'theory' name 'imports' (name +) uses? 'begin'
36 uses: 'uses' ((name | parname) +);
41 \item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots>
42 B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the
43 merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
45 Due to inclusion of several ancestors, the overall theory structure
46 emerging in an Isabelle session forms a directed acyclic graph
47 (DAG). Isabelle's theory loader ensures that the sources
48 contributing to the development graph are always up-to-date.
49 Changed files are automatically reloaded when processing theory
52 The optional @{keyword_def "uses"} specification declares additional
53 dependencies on extra files (usually ML sources). Files will be
54 loaded immediately (as ML), unless the name is put in parentheses,
55 which merely documents the dependency to be resolved later in the
56 text (typically via explicit @{command_ref "use"} in the body text,
59 \item [@{command (global) "end"}] concludes the current theory
66 section {* Local theory targets \label{sec:target} *}
69 A local theory target is a context managed separately within the
70 enclosing theory. Contexts may introduce parameters (fixed
71 variables) and assumptions (hypotheses). Definitions and theorems
72 depending on the context may be added incrementally later on. Named
73 contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
74 (cf.\ \secref{sec:class}); the name ``@{text "-"}'' signifies the
75 global theory context.
77 \begin{matharray}{rcll}
78 @{command_def "context"} & : & \isartrans{theory}{local{\dsh}theory} \\
79 @{command_def (local) "end"} & : & \isartrans{local{\dsh}theory}{theory} \\
82 \indexouternonterm{target}
84 'context' name 'begin'
87 target: '(' 'in' name ')'
93 \item [@{command "context"}~@{text "c \<BEGIN>"}] recommences an
94 existing locale or class context @{text c}. Note that locale and
95 class definitions allow to include the @{keyword "begin"} keyword as
96 well, in order to continue the local theory immediately after the
97 initial specification.
99 \item [@{command (local) "end"}] concludes the current local theory
100 and continues the enclosing global theory. Note that a global
101 @{command (global) "end"} has a different meaning: it concludes the
102 theory itself (\secref{sec:begin-thy}).
104 \item [@{text "(\<IN> c)"}] given after any local theory command
105 specifies an immediate target, e.g.\ ``@{command
106 "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
107 "theorem"}~@{text "(\<IN> c) \<dots>"}''. This works both in a local or
108 global theory context; the current target context will be suspended
109 for this command only. Note that ``@{text "(\<IN> -)"}'' will
110 always produce a global result independently of the current target
115 The exact meaning of results produced within a local theory context
116 depends on the underlying target infrastructure (locale, type class
117 etc.). The general idea is as follows, considering a context named
118 @{text c} with parameter @{text x} and assumption @{text "A[x]"}.
120 Definitions are exported by introducing a global version with
121 additional arguments; a syntactic abbreviation links the long form
122 with the abstract version of the target context. For example,
123 @{text "a \<equiv> t[x]"} becomes @{text "c.a ?x \<equiv> t[?x]"} at the theory
124 level (for arbitrary @{text "?x"}), together with a local
125 abbreviation @{text "c \<equiv> c.a x"} in the target context (for the
126 fixed parameter @{text x}).
128 Theorems are exported by discharging the assumptions and
129 generalizing the parameters of the context. For example, @{text "a:
130 B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
135 section {* Basic specification elements *}
138 \begin{matharray}{rcll}
139 @{command_def "axiomatization"} & : & \isarkeep{theory} & (axiomatic!)\\
140 @{command_def "definition"} & : & \isarkeep{local{\dsh}theory} \\
141 @{attribute_def "defn"} & : & \isaratt \\
142 @{command_def "abbreviation"} & : & \isarkeep{local{\dsh}theory} \\
143 @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
144 @{command_def "notation"} & : & \isarkeep{local{\dsh}theory} \\
145 @{command_def "no_notation"} & : & \isarkeep{local{\dsh}theory} \\
148 These specification mechanisms provide a slightly more abstract view
149 than the underlying primitives of @{command "consts"}, @{command
150 "defs"} (see \secref{sec:consts}), and @{command "axioms"} (see
151 \secref{sec:axms-thms}). In particular, type-inference is commonly
152 available, and result names need not be given.
155 'axiomatization' target? fixes? ('where' specs)?
157 'definition' target? (decl 'where')? thmdecl? prop
159 'abbreviation' target? mode? (decl 'where')? prop
161 ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
164 fixes: ((name ('::' type)? mixfix? | vars) + 'and')
166 specs: (thmdecl? props + 'and')
168 decl: name ('::' type)? mixfix?
174 \item [@{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m
175 \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}] introduces several constants
176 simultaneously and states axiomatic properties for these. The
177 constants are marked as being specified once and for all, which
178 prevents additional specifications being issued later on.
180 Note that axiomatic specifications are only appropriate when
181 declaring a new logical system; axiomatic specifications are
182 restricted to global theory contexts. Normal applications should
183 only use definitional mechanisms!
185 \item [@{command "definition"}~@{text "c \<WHERE> eq"}] produces an
186 internal definition @{text "c \<equiv> t"} according to the specification
187 given as @{text eq}, which is then turned into a proven fact. The
188 given proposition may deviate from internal meta-level equality
189 according to the rewrite rules declared as @{attribute defn} by the
190 object-logic. This usually covers object-level equality @{text "x =
191 y"} and equivalence @{text "A \<leftrightarrow> B"}. End-users normally need not
192 change the @{attribute defn} setup.
194 Definitions may be presented with explicit arguments on the LHS, as
195 well as additional conditions, e.g.\ @{text "f x y = t"} instead of
196 @{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an
197 unrestricted @{text "g \<equiv> \<lambda>x y. u"}.
199 \item [@{command "abbreviation"}~@{text "c \<WHERE> eq"}] introduces
200 a syntactic constant which is associated with a certain term
201 according to the meta-level equality @{text eq}.
203 Abbreviations participate in the usual type-inference process, but
204 are expanded before the logic ever sees them. Pretty printing of
205 terms involves higher-order rewriting with rules stemming from
206 reverted abbreviations. This needs some care to avoid overlapping
207 or looping syntactic replacements!
209 The optional @{text mode} specification restricts output to a
210 particular print mode; using ``@{text input}'' here achieves the
211 effect of one-way abbreviations. The mode may also include an
212 ``@{keyword "output"}'' qualifier that affects the concrete syntax
213 declared for abbreviations, cf.\ @{command "syntax"} in
214 \secref{sec:syn-trans}.
216 \item [@{command "print_abbrevs"}] prints all constant abbreviations
217 of the current context.
219 \item [@{command "notation"}~@{text "c (mx)"}] associates mixfix
220 syntax with an existing constant or fixed variable. This is a
221 robust interface to the underlying @{command "syntax"} primitive
222 (\secref{sec:syn-trans}). Type declaration and internal syntactic
223 representation of the given entity is retrieved from the context.
225 \item [@{command "no_notation"}] is similar to @{command
226 "notation"}, but removes the specified syntax annotation from the
231 All of these specifications support local theory targets (cf.\
232 \secref{sec:target}).
236 section {* Generic declarations *}
239 Arbitrary operations on the background context may be wrapped-up as
240 generic declaration elements. Since the underlying concept of local
241 theories may be subject to later re-interpretation, there is an
242 additional dependency on a morphism that tells the difference of the
243 original declaration context wrt.\ the application context
244 encountered later on. A fact declaration is an important special
245 case: it consists of a theorem which is applied to the context by
246 means of an attribute.
248 \begin{matharray}{rcl}
249 @{command_def "declaration"} & : & \isarkeep{local{\dsh}theory} \\
250 @{command_def "declare"} & : & \isarkeep{local{\dsh}theory} \\
254 'declaration' target? text
256 'declare' target? (thmrefs + 'and')
262 \item [@{command "declaration"}~@{text d}] adds the declaration
263 function @{text d} of ML type @{ML_type declaration}, to the current
264 local theory under construction. In later application contexts, the
265 function is transformed according to the morphisms being involved in
266 the interpretation hierarchy.
268 \item [@{command "declare"}~@{text thms}] declares theorems to the
269 current local theory context. No theorem binding is involved here,
270 unlike @{command "theorems"} or @{command "lemmas"} (cf.\
271 \secref{sec:axms-thms}), so @{command "declare"} only has the effect
272 of applying attributes as included in the theorem specification.
278 section {* Locales \label{sec:locale} *}
281 Locales are named local contexts, consisting of a list of
282 declaration elements that are modeled after the Isar proof context
283 commands (cf.\ \secref{sec:proof-context}).
287 subsection {* Locale specifications *}
290 \begin{matharray}{rcl}
291 @{command_def "locale"} & : & \isartrans{theory}{local{\dsh}theory} \\
292 @{command_def "print_locale"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
293 @{command_def "print_locales"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
294 @{method_def intro_locales} & : & \isarmeth \\
295 @{method_def unfold_locales} & : & \isarmeth \\
298 \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
299 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
300 \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
302 'locale' name ('=' localeexpr)? 'begin'?
304 'print\_locale' '!'? localeexpr
306 localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
309 contextexpr: nameref | '(' contextexpr ')' |
310 (contextexpr (name mixfix? +)) | (contextexpr + '+')
312 contextelem: fixes | constrains | assumes | defines | notes
314 fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
316 constrains: 'constrains' (name '::' type + 'and')
318 assumes: 'assumes' (thmdecl? props + 'and')
320 defines: 'defines' (thmdecl? prop proppat? + 'and')
322 notes: 'notes' (thmdef? thmrefs + 'and')
324 includes: 'includes' contextexpr
330 \item [@{command "locale"}~@{text "loc = import + body"}] defines a
331 new locale @{text loc} as a context consisting of a certain view of
332 existing locales (@{text import}) plus some additional elements
333 (@{text body}). Both @{text import} and @{text body} are optional;
334 the degenerate form @{command "locale"}~@{text loc} defines an empty
335 locale, which may still be useful to collect declarations of facts
336 later on. Type-inference on locale expressions automatically takes
337 care of the most general typing that the combined context elements
340 The @{text import} consists of a structured context expression,
341 consisting of references to existing locales, renamed contexts, or
342 merged contexts. Renaming uses positional notation: @{text "c
343 x\<^sub>1 \<dots> x\<^sub>n"} means that (a prefix of) the fixed
344 parameters of context @{text c} are named @{text "x\<^sub>1, \<dots>,
345 x\<^sub>n"}; a ``@{text _}'' (underscore) means to skip that
346 position. Renaming by default deletes concrete syntax, but new
347 syntax may by specified with a mixfix annotation. An exeption of
348 this rule is the special syntax declared with ``@{text
349 "(\<STRUCTURE>)"}'' (see below), which is neither deleted nor can it
350 be changed. Merging proceeds from left-to-right, suppressing any
351 duplicates stemming from different paths through the import
354 The @{text body} consists of basic context elements, further context
355 expressions may be included as well.
359 \item [@{element "fixes"}~@{text "x :: \<tau> (mx)"}] declares a local
360 parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
361 are optional). The special syntax declaration ``@{text
362 "(\<STRUCTURE>)"}'' means that @{text x} may be referenced
363 implicitly in this context.
365 \item [@{element "constrains"}~@{text "x :: \<tau>"}] introduces a type
366 constraint @{text \<tau>} on the local parameter @{text x}.
368 \item [@{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}]
369 introduces local premises, similar to @{command "assume"} within a
370 proof (cf.\ \secref{sec:proof-context}).
372 \item [@{element "defines"}~@{text "a: x \<equiv> t"}] defines a previously
373 declared parameter. This is similar to @{command "def"} within a
374 proof (cf.\ \secref{sec:proof-context}), but @{element "defines"}
375 takes an equational proposition instead of variable-term pair. The
376 left-hand side of the equation may have additional arguments, e.g.\
377 ``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''.
379 \item [@{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
380 reconsiders facts within a local context. Most notably, this may
381 include arbitrary declarations in any attribute specifications
382 included here, e.g.\ a local @{attribute simp} rule.
384 The initial @{text import} specification of a locale
385 expression maintains a dynamic relation to the locales being
386 referenced (benefiting from any later fact declarations in the
391 Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given
392 in the syntax of @{element "assumes"} and @{element "defines"} above
393 are illegal in locale definitions. In the long goal format of
394 \secref{sec:goals}, term bindings may be included as expected,
397 \medskip By default, locale specifications are ``closed up'' by
398 turning the given text into a predicate definition @{text
399 loc_axioms} and deriving the original assumptions as local lemmas
400 (modulo local definitions). The predicate statement covers only the
401 newly specified assumptions, omitting the content of included locale
402 expressions. The full cumulative view is only provided on export,
403 involving another predicate @{text loc} that refers to the complete
406 In any case, the predicate arguments are those locale parameters
407 that actually occur in the respective piece of text. Also note that
408 these predicates operate at the meta-level in theory, but the locale
409 packages attempts to internalize statements according to the
410 object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and
411 @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
412 \secref{sec:object-logic}). Separate introduction rules @{text
413 loc_axioms.intro} and @{text loc.intro} are provided as well.
415 \item [@{command "print_locale"}~@{text "import + body"}] prints the
416 specified locale expression in a flattened form. The notable
417 special case @{command "print_locale"}~@{text loc} just prints the
418 contents of the named locale, but keep in mind that type-inference
419 will normalize type variables according to the usual alphabetical
420 order. The command omits @{element "notes"} elements by default.
421 Use @{command "print_locale"}@{text "!"} to get them included.
423 \item [@{command "print_locales"}] prints the names of all locales
424 of the current theory.
426 \item [@{method intro_locales} and @{method unfold_locales}]
427 repeatedly expand all introduction rules of locale predicates of the
428 theory. While @{method intro_locales} only applies the @{text
429 loc.intro} introduction rules and therefore does not decend to
430 assumptions, @{method unfold_locales} is more aggressive and applies
431 @{text loc_axioms.intro} as well. Both methods are aware of locale
432 specifications entailed by the context, both from target statements,
433 and from interpretations (see below). New goals that are entailed
434 by the current context are discharged automatically.
440 subsection {* Interpretation of locales *}
443 Locale expressions (more precisely, \emph{context expressions}) may
444 be instantiated, and the instantiated facts added to the current
445 context. This requires a proof of the instantiated specification
446 and is called \emph{locale interpretation}. Interpretation is
447 possible in theories and locales (command @{command
448 "interpretation"}) and also within a proof body (command @{command
451 \begin{matharray}{rcl}
452 @{command_def "interpretation"} & : & \isartrans{theory}{proof(prove)} \\
453 @{command_def "interpret"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
454 @{command_def "print_interps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
457 \indexouternonterm{interp}
459 'interpretation' (interp | name ('<' | subseteq) contextexpr)
463 'print\_interps' '!'? name
465 instantiation: ('[' (inst+) ']')?
467 interp: (name ':')? \\ (contextexpr instantiation |
468 name instantiation 'where' (thmdecl? prop + 'and'))
474 \item [@{command "interpretation"}~@{text "expr insts \<WHERE> eqns"}]
476 The first form of @{command "interpretation"} interprets @{text
477 expr} in the theory. The instantiation is given as a list of terms
478 @{text insts} and is positional. All parameters must receive an
479 instantiation term --- with the exception of defined parameters.
480 These are, if omitted, derived from the defining equation and other
481 instantiations. Use ``@{text _}'' to omit an instantiation term.
483 The command generates proof obligations for the instantiated
484 specifications (assumes and defines elements). Once these are
485 discharged by the user, instantiated facts are added to the theory
486 in a post-processing phase.
488 Additional equations, which are unfolded in facts during
489 post-processing, may be given after the keyword @{keyword "where"}.
490 This is useful for interpreting concepts introduced through
491 definition specification elements. The equations must be proved.
492 Note that if equations are present, the context expression is
493 restricted to a locale name.
495 The command is aware of interpretations already active in the
496 theory, but does not simplify the goal automatically. In order to
497 simplify the proof obligations use methods @{method intro_locales}
498 or @{method unfold_locales}. Post-processing is not applied to
499 facts of interpretations that are already active. This avoids
500 duplication of interpreted facts, in particular. Note that, in the
501 case of a locale with import, parts of the interpretation may
502 already be active. The command will only process facts for new
505 The context expression may be preceded by a name, which takes effect
506 in the post-processing of facts. It is used to prefix fact names,
507 for example to avoid accidental hiding of other facts.
509 Adding facts to locales has the effect of adding interpreted facts
510 to the theory for all active interpretations also. That is,
511 interpretations dynamically participate in any facts added to
514 \item [@{command "interpretation"}~@{text "name \<subseteq> expr"}]
516 This form of the command interprets @{text expr} in the locale
517 @{text name}. It requires a proof that the specification of @{text
518 name} implies the specification of @{text expr}. As in the
519 localized version of the theorem command, the proof is in the
520 context of @{text name}. After the proof obligation has been
521 dischared, the facts of @{text expr} become part of locale @{text
522 name} as \emph{derived} context elements and are available when the
523 context @{text name} is subsequently entered. Note that, like
524 import, this is dynamic: facts added to a locale part of @{text
525 expr} after interpretation become also available in @{text name}.
526 Like facts of renamed context elements, facts obtained by
527 interpretation may be accessed by prefixing with the parameter
528 renaming (where the parameters are separated by ``@{text _}'').
530 Unlike interpretation in theories, instantiation is confined to the
531 renaming of parameters, which may be specified as part of the
532 context expression @{text expr}. Using defined parameters in @{text
533 name} one may achieve an effect similar to instantiation, though.
535 Only specification fragments of @{text expr} that are not already
536 part of @{text name} (be it imported, derived or a derived fragment
537 of the import) are considered by interpretation. This enables
538 circular interpretations.
540 If interpretations of @{text name} exist in the current theory, the
541 command adds interpretations for @{text expr} as well, with the same
542 prefix and attributes, although only for fragments of @{text expr}
543 that are not interpreted in the theory already.
545 \item [@{command "interpret"}~@{text "expr insts \<WHERE> eqns"}]
546 interprets @{text expr} in the proof context and is otherwise
547 similar to interpretation in theories.
549 \item [@{command "print_interps"}~@{text loc}] prints the
550 interpretations of a particular locale @{text loc} that are active
551 in the current context, either theory or proof context. The
552 exclamation point argument triggers printing of \emph{witness}
553 theorems justifying interpretations. These are normally omitted
559 Since attributes are applied to interpreted theorems,
560 interpretation may modify the context of common proof tools, e.g.\
561 the Simplifier or Classical Reasoner. Since the behavior of such
562 automated reasoning tools is \emph{not} stable under
563 interpretation morphisms, manual declarations might have to be
568 An interpretation in a theory may subsume previous
569 interpretations. This happens if the same specification fragment
570 is interpreted twice and the instantiation of the second
571 interpretation is more general than the interpretation of the
572 first. A warning is issued, since it is likely that these could
573 have been generalized in the first place. The locale package does
574 not attempt to remove subsumed interpretations.
579 section {* Classes \label{sec:class} *}
582 A class is a particular locale with \emph{exactly one} type variable
583 @{text \<alpha>}. Beyond the underlying locale, a corresponding type class
584 is established which is interpreted logically as axiomatic type
585 class \cite{Wenzel:1997:TPHOL} whose logical content are the
586 assumptions of the locale. Thus, classes provide the full
587 generality of locales combined with the commodity of type classes
588 (notably type-inference). See \cite{isabelle-classes} for a short
591 \begin{matharray}{rcl}
592 @{command_def "class"} & : & \isartrans{theory}{local{\dsh}theory} \\
593 @{command_def "instantiation"} & : & \isartrans{theory}{local{\dsh}theory} \\
594 @{command_def "instance"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
595 @{command_def "subclass"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
596 @{command_def "print_classes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
597 @{method_def intro_classes} & : & \isarmeth \\
601 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
604 'instantiation' (nameref + 'and') '::' arity 'begin'
608 'subclass' target? nameref
613 superclassexpr: nameref | (nameref '+' superclassexpr)
619 \item [@{command "class"}~@{text "c = superclasses + body"}] defines
620 a new class @{text c}, inheriting from @{text superclasses}. This
621 introduces a locale @{text c} with import of all locales @{text
624 Any @{element "fixes"} in @{text body} are lifted to the global
625 theory level (\emph{class operations} @{text "f\<^sub>1, \<dots>,
626 f\<^sub>n"} of class @{text c}), mapping the local type parameter
627 @{text \<alpha>} to a schematic type variable @{text "?\<alpha> :: c"}.
629 Likewise, @{element "assumes"} in @{text body} are also lifted,
630 mapping each local parameter @{text "f :: \<tau>[\<alpha>]"} to its
631 corresponding global constant @{text "f :: \<tau>[?\<alpha> :: c]"}. The
632 corresponding introduction rule is provided as @{text
633 c_class_axioms.intro}. This rule should be rarely needed directly
634 --- the @{method intro_classes} method takes care of the details of
635 class membership proofs.
637 \item [@{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>,
638 s\<^sub>n) s \<BEGIN>"}] opens a theory target (cf.\
639 \secref{sec:target}) which allows to specify class operations @{text
640 "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding to sort @{text s} at the
641 particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1, \<dots>,
642 \<alpha>\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command
643 in the target body poses a goal stating these type arities. The
644 target is concluded by an @{command_ref (local) "end"} command.
646 Note that a list of simultaneous type constructors may be given;
647 this corresponds nicely to mutual recursive type definitions, e.g.\
650 \item [@{command "instance"}] in an instantiation target body sets
651 up a goal stating the type arities claimed at the opening @{command
652 "instantiation"}. The proof would usually proceed by @{method
653 intro_classes}, and then establish the characteristic theorems of
654 the type classes involved. After finishing the proof, the
655 background theory will be augmented by the proven type arities.
657 \item [@{command "subclass"}~@{text c}] in a class context for class
658 @{text d} sets up a goal stating that class @{text c} is logically
659 contained in class @{text d}. After finishing the proof, class
660 @{text d} is proven to be subclass @{text c} and the locale @{text
661 c} is interpreted into @{text d} simultaneously.
663 \item [@{command "print_classes"}] prints all classes in the current
666 \item [@{method intro_classes}] repeatedly expands all class
667 introduction rules of this theory. Note that this method usually
668 needs not be named explicitly, as it is already included in the
669 default proof step (e.g.\ of @{command "proof"}). In particular,
670 instantiation of trivial (syntactic) classes may be performed by a
671 single ``@{command ".."}'' proof step.
677 subsection {* The class target *}
682 A named context may refer to a locale (cf.\ \secref{sec:target}).
683 If this locale is also a class @{text c}, apart from the common
684 locale target behaviour the following happens.
688 \item Local constant declarations @{text "g[\<alpha>]"} referring to the
689 local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"}
690 are accompanied by theory-level constants @{text "g[?\<alpha> :: c]"}
691 referring to theory-level class operations @{text "f[?\<alpha> :: c]"}.
693 \item Local theorem bindings are lifted as are assumptions.
695 \item Local syntax refers to local operations @{text "g[\<alpha>]"} and
696 global operations @{text "g[?\<alpha> :: c]"} uniformly. Type inference
697 resolves ambiguities. In rare cases, manual type annotations are
704 subsection {* Old-style axiomatic type classes \label{sec:axclass} *}
707 \begin{matharray}{rcl}
708 @{command_def "axclass"} & : & \isartrans{theory}{theory} \\
709 @{command_def "instance"} & : & \isartrans{theory}{proof(prove)} \\
712 Axiomatic type classes are Isabelle/Pure's primitive
713 \emph{definitional} interface to type classes. For practical
714 applications, you should consider using classes
715 (cf.~\secref{sec:classes}) which provide high level interface.
718 'axclass' classdecl (axmdecl prop +)
720 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
726 \item [@{command "axclass"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n
727 axms"}] defines an axiomatic type class as the intersection of
728 existing classes, with additional axioms holding. Class axioms may
729 not contain more than one type variable. The class axioms (with
730 implicit sort constraints added) are bound to the given names.
731 Furthermore a class introduction rule is generated (being bound as
732 @{text c_class.intro}); this rule is employed by method @{method
733 intro_classes} to support instantiation proofs of this class.
735 The ``class axioms'' are stored as theorems according to the given
736 name specifications, adding @{text "c_class"} as name space prefix;
737 the same facts are also stored collectively as @{text
740 \item [@{command "instance"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} and
741 @{command "instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n) s"}]
742 setup a goal stating a class relation or type arity. The proof
743 would usually proceed by @{method intro_classes}, and then establish
744 the characteristic theorems of the type classes involved. After
745 finishing the proof, the theory will be augmented by a type
746 signature declaration corresponding to the resulting theorem.
752 section {* Unrestricted overloading *}
755 Isabelle/Pure's definitional schemes support certain forms of
756 overloading (see \secref{sec:consts}). At most occassions
757 overloading will be used in a Haskell-like fashion together with
758 type classes by means of @{command "instantiation"} (see
759 \secref{sec:class}). Sometimes low-level overloading is desirable.
760 The @{command "overloading"} target provides a convenient view for
763 \begin{matharray}{rcl}
764 @{command_def "overloading"} & : & \isartrans{theory}{local{\dsh}theory} \\
769 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
774 \item [@{command "overloading"}~@{text "x\<^sub>1 \<equiv> c\<^sub>1 ::
775 \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n \<BEGIN>"}]
776 opens a theory target (cf.\ \secref{sec:target}) which allows to
777 specify constants with overloaded definitions. These are identified
778 by an explicitly given mapping from variable names @{text
779 "x\<^sub>i"} to constants @{text "c\<^sub>i"} at particular type
780 instances. The definitions themselves are established using common
781 specification tools, using the names @{text "x\<^sub>i"} as
782 reference to the corresponding constants. The target is concluded
783 by @{command (local) "end"}.
785 A @{text "(unchecked)"} option disables global dependency checks for
786 the corresponding definition, which is occasionally useful for
787 exotic overloading. It is at the discretion of the user to avoid
788 malformed theory specifications!
794 section {* Incorporating ML code \label{sec:ML} *}
797 \begin{matharray}{rcl}
798 @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
799 @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
800 @{command_def "ML_prf"} & : & \isarkeep{proof} \\
801 @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
802 @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
803 @{command_def "setup"} & : & \isartrans{theory}{theory} \\
804 @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\
810 ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
812 'method\_setup' name '=' text text
818 \item [@{command "use"}~@{text "file"}] reads and executes ML
819 commands from @{text "file"}. The current theory context is passed
820 down to the ML toplevel and may be modified, using @{ML
821 "Context.>>"} or derived ML commands. The file name is checked with
822 the @{keyword_ref "uses"} dependency declaration given in the theory
823 header (see also \secref{sec:begin-thy}).
825 Top-level ML bindings are stored within the (global or local) theory
828 \item [@{command "ML"}~@{text "text"}] is similar to @{command
829 "use"}, but executes ML commands directly from the given @{text
830 "text"}. Top-level ML bindings are stored within the (global or
831 local) theory context.
833 \item [@{command "ML_prf"}] is analogous to @{command "ML"} but
834 works within a proof context.
836 Top-level ML bindings are stored within the proof context in a
837 purely sequential fashion, disregarding the nested proof structure.
838 ML bindings introduced by @{command "ML_prf"} are discarded at the
841 \item [@{command "ML_val"} and @{command "ML_command"}] are
842 diagnostic versions of @{command "ML"}, which means that the context
843 may not be updated. @{command "ML_val"} echos the bindings produced
844 at the ML toplevel, but @{command "ML_command"} is silent.
846 \item [@{command "setup"}~@{text "text"}] changes the current theory
847 context by applying @{text "text"}, which refers to an ML expression
848 of type @{ML_type "theory -> theory"}. This enables to initialize
849 any object-logic specific tools and packages written in ML, for
852 \item [@{command "method_setup"}~@{text "name = text description"}]
853 defines a proof method in the current theory. The given @{text
854 "text"} has to be an ML expression of type @{ML_type "Args.src ->
855 Proof.context -> Proof.method"}. Parsing concrete method syntax
856 from @{ML_type Args.src} input can be quite tedious in general. The
857 following simple examples are for methods without any explicit
858 arguments, or a list of theorems, respectively.
860 %FIXME proper antiquotations
863 Method.no_args (Method.METHOD (fn facts => foobar_tac))
864 Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
865 Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
866 Method.thms_ctxt_args (fn thms => fn ctxt =>
867 Method.METHOD (fn facts => foobar_tac))
871 Note that mere tactic emulations may ignore the @{text facts}
872 parameter above. Proper proof methods would do something
873 appropriate with the list of current facts, though. Single-rule
874 methods usually do strict forward-chaining (e.g.\ by using @{ML
875 Drule.multi_resolves}), while automatic ones just insert the facts
876 using @{ML Method.insert_tac} before applying the main tactic.
882 section {* Primitive specification elements *}
884 subsection {* Type classes and sorts \label{sec:classes} *}
887 \begin{matharray}{rcll}
888 @{command_def "classes"} & : & \isartrans{theory}{theory} \\
889 @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
890 @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\
891 @{command_def "class_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
895 'classes' (classdecl +)
897 'classrel' (nameref ('<' | subseteq) nameref + 'and')
905 \item [@{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"}]
906 declares class @{text c} to be a subclass of existing classes @{text
907 "c\<^sub>1, \<dots>, c\<^sub>n"}. Cyclic class structures are not permitted.
909 \item [@{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}] states
910 subclass relations between existing classes @{text "c\<^sub>1"} and
911 @{text "c\<^sub>2"}. This is done axiomatically! The @{command_ref
912 "instance"} command (see \secref{sec:axclass}) provides a way to
913 introduce proven class relations.
915 \item [@{command "defaultsort"}~@{text s}] makes sort @{text s} the
916 new default sort for any type variables given without sort
917 constraints. Usually, the default sort would be only changed when
918 defining a new object-logic.
920 \item [@{command "class_deps"}] visualizes the subclass relation,
921 using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
927 subsection {* Types and type abbreviations \label{sec:types-pure} *}
930 \begin{matharray}{rcll}
931 @{command_def "types"} & : & \isartrans{theory}{theory} \\
932 @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\
933 @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\
934 @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
938 'types' (typespec '=' type infix? +)
940 'typedecl' typespec infix?
942 'nonterminals' (name +)
944 'arities' (nameref '::' arity +)
950 \item [@{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}]
951 introduces \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}
952 for existing type @{text "\<tau>"}. Unlike actual type definitions, as
953 are available in Isabelle/HOL for example, type synonyms are just
954 purely syntactic abbreviations without any logical significance.
955 Internally, type synonyms are fully expanded.
957 \item [@{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}]
958 declares a new type constructor @{text t}, intended as an actual
959 logical type (of the object-logic, if available).
961 \item [@{command "nonterminals"}~@{text c}] declares type
962 constructors @{text c} (without arguments) to act as purely
963 syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
964 syntax of terms or types.
966 \item [@{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)
967 s"}] augments Isabelle's order-sorted signature of types by new type
968 constructor arities. This is done axiomatically! The @{command_ref
969 "instance"} command (see \S\ref{sec:axclass}) provides a way to
970 introduce proven type arities.
976 subsection {* Constants and definitions \label{sec:consts} *}
979 Definitions essentially express abbreviations within the logic. The
980 simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
981 c} is a newly declared constant. Isabelle also allows derived forms
982 where the arguments of @{text c} appear on the left, abbreviating a
983 prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
984 written more conveniently as @{text "c x y \<equiv> t"}. Moreover,
985 definitions may be weakened by adding arbitrary pre-conditions:
986 @{text "A \<Longrightarrow> c x y \<equiv> t"}.
988 \medskip The built-in well-formedness conditions for definitional
993 \item Arguments (on the left-hand side) must be distinct variables.
995 \item All variables on the right-hand side must also appear on the
998 \item All type variables on the right-hand side must also appear on
999 the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
1000 \<alpha> list)"} for example.
1002 \item The definition must not be recursive. Most object-logics
1003 provide definitional principles that can be used to express
1008 Overloading means that a constant being declared as @{text "c :: \<alpha>
1009 decl"} may be defined separately on type instances @{text "c ::
1010 (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
1011 t}. The right-hand side may mention overloaded constants
1012 recursively at type instances corresponding to the immediate
1013 argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
1014 specification patterns impose global constraints on all occurrences,
1015 e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
1016 corresponding occurrences on some right-hand side need to be an
1017 instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
1019 \begin{matharray}{rcl}
1020 @{command_def "consts"} & : & \isartrans{theory}{theory} \\
1021 @{command_def "defs"} & : & \isartrans{theory}{theory} \\
1022 @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\
1026 'consts' ((name '::' type mixfix?) +)
1028 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
1033 'constdefs' structs? (constdecl? constdef +)
1036 structs: '(' 'structure' (vars + 'and') ')'
1038 constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
1040 constdef: thmdecl? prop
1046 \item [@{command "consts"}~@{text "c :: \<sigma>"}] declares constant
1047 @{text c} to have any instance of type scheme @{text \<sigma>}. The
1048 optional mixfix annotations may attach concrete syntax to the
1051 \item [@{command "defs"}~@{text "name: eqn"}] introduces @{text eqn}
1052 as a definitional axiom for some existing constant.
1054 The @{text "(unchecked)"} option disables global dependency checks
1055 for this definition, which is occasionally useful for exotic
1056 overloading. It is at the discretion of the user to avoid malformed
1057 theory specifications!
1059 The @{text "(overloaded)"} option declares definitions to be
1060 potentially overloaded. Unless this option is given, a warning
1061 message would be issued for any definitional equation with a more
1062 special type than that of the corresponding constant declaration.
1064 \item [@{command "constdefs"}] provides a streamlined combination of
1065 constants declarations and definitions: type-inference takes care of
1066 the most general typing of the given specification (the optional
1067 type constraint may refer to type-inference dummies ``@{text
1068 _}'' as usual). The resulting type declaration needs to agree with
1069 that of the specification; overloading is \emph{not} supported here!
1071 The constant name may be omitted altogether, if neither type nor
1072 syntax declarations are given. The canonical name of the
1073 definitional axiom for constant @{text c} will be @{text c_def},
1074 unless specified otherwise. Also note that the given list of
1075 specifications is processed in a strictly sequential manner, with
1076 type-checking being performed independently.
1078 An optional initial context of @{text "(structure)"} declarations
1079 admits use of indexed syntax, using the special symbol @{verbatim
1080 "\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is
1081 particularly useful with locales (see also \S\ref{sec:locale}).
1087 section {* Axioms and theorems \label{sec:axms-thms} *}
1090 \begin{matharray}{rcll}
1091 @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
1092 @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\
1093 @{command_def "theorems"} & : & \isarkeep{local{\dsh}theory} \\
1097 'axioms' (axmdecl prop +)
1099 ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
1105 \item [@{command "axioms"}~@{text "a: \<phi>"}] introduces arbitrary
1106 statements as axioms of the meta-logic. In fact, axioms are
1107 ``axiomatic theorems'', and may be referred later just as any other
1110 Axioms are usually only introduced when declaring new logical
1111 systems. Everyday work is typically done the hard way, with proper
1112 definitions and proven theorems.
1114 \item [@{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
1115 retrieves and stores existing facts in the theory context, or the
1116 specified target context (see also \secref{sec:target}). Typical
1117 applications would also involve attributes, to declare Simplifier
1120 \item [@{command "theorems"}] is essentially the same as @{command
1121 "lemmas"}, but marks the result as a different kind of facts.
1127 section {* Oracles *}
1130 \begin{matharray}{rcl}
1131 @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
1134 The oracle interface promotes a given ML function @{ML_text "'a -> cterm"}
1135 to @{ML_text "'a -> thm"}. This acts like an infinitary
1136 specification of axioms -- there is no internal check of the
1137 correctness of the results! The inference kernel records oracle
1138 invocations within the internal derivation object of theorems, and
1139 the pretty printer attaches ``@{text "[!]"}'' to indicate results
1140 that are not fully checked by Isabelle inferences.
1143 'oracle' name '=' text
1149 \item [@{command "oracle"}~@{text "name = text"}] turns the given ML
1150 expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
1151 ML function of type @{ML_text "'a -> thm"}, which is bound to the
1152 global identifier @{ML_text name}.
1158 section {* Name spaces *}
1161 \begin{matharray}{rcl}
1162 @{command_def "global"} & : & \isartrans{theory}{theory} \\
1163 @{command_def "local"} & : & \isartrans{theory}{theory} \\
1164 @{command_def "hide"} & : & \isartrans{theory}{theory} \\
1168 'hide' ('(open)')? name (nameref + )
1172 Isabelle organizes any kind of name declarations (of types,
1173 constants, theorems etc.) by separate hierarchically structured name
1174 spaces. Normally the user does not have to control the behavior of
1175 name spaces by hand, yet the following commands provide some way to
1180 \item [@{command "global"} and @{command "local"}] change the
1181 current name declaration mode. Initially, theories start in
1182 @{command "local"} mode, causing all names to be automatically
1183 qualified by the theory name. Changing this to @{command "global"}
1184 causes all names to be declared without the theory prefix, until
1185 @{command "local"} is declared again.
1187 Note that global names are prone to get hidden accidently later,
1188 when qualified names of the same base name are introduced.
1190 \item [@{command "hide"}~@{text "space names"}] fully removes
1191 declarations from a given name space (which may be @{text "class"},
1192 @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text
1193 "(open)"} option, only the base name is hidden. Global
1194 (unqualified) names may never be hidden.
1196 Note that hiding name space accesses has no impact on logical
1197 declarations -- they remain valid internally. Entities that are no
1198 longer accessible to the user are printed with the special qualifier
1199 ``@{text "??"}'' prefixed to the full internal name.
1205 section {* Syntax and translations \label{sec:syn-trans} *}
1208 \begin{matharray}{rcl}
1209 @{command_def "syntax"} & : & \isartrans{theory}{theory} \\
1210 @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\
1211 @{command_def "translations"} & : & \isartrans{theory}{theory} \\
1212 @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\
1216 ('syntax' | 'no\_syntax') mode? (constdecl +)
1218 ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
1221 mode: ('(' ( name | 'output' | name 'output' ) ')')
1223 transpat: ('(' nameref ')')? string
1229 \item [@{command "syntax"}~@{text "(mode) decls"}] is similar to
1230 @{command "consts"}~@{text decls}, except that the actual logical
1231 signature extension is omitted. Thus the context free grammar of
1232 Isabelle's inner syntax may be augmented in arbitrary ways,
1233 independently of the logic. The @{text mode} argument refers to the
1234 print mode that the grammar rules belong; unless the @{keyword_ref
1235 "output"} indicator is given, all productions are added both to the
1236 input and output grammar.
1238 \item [@{command "no_syntax"}~@{text "(mode) decls"}] removes
1239 grammar declarations (and translations) resulting from @{text
1240 decls}, which are interpreted in the same manner as for @{command
1243 \item [@{command "translations"}~@{text rules}] specifies syntactic
1244 translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
1245 parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
1246 Translation patterns may be prefixed by the syntactic category to be
1247 used for parsing; the default is @{text logic}.
1249 \item [@{command "no_translations"}~@{text rules}] removes syntactic
1250 translation rules, which are interpreted in the same manner as for
1251 @{command "translations"} above.
1257 section {* Syntax translation functions *}
1260 \begin{matharray}{rcl}
1261 @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\
1262 @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\
1263 @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
1264 @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
1265 @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
1269 ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
1270 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
1274 Syntax translation functions written in ML admit almost arbitrary
1275 manipulations of Isabelle's inner syntax. Any of the above commands
1276 have a single \railqtok{text} argument that refers to an ML
1277 expression of appropriate type, which are as follows by default:
1279 %FIXME proper antiquotations
1281 val parse_ast_translation : (string * (ast list -> ast)) list
1282 val parse_translation : (string * (term list -> term)) list
1283 val print_translation : (string * (term list -> term)) list
1284 val typed_print_translation :
1285 (string * (bool -> typ -> term list -> term)) list
1286 val print_ast_translation : (string * (ast list -> ast)) list
1289 If the @{text "(advanced)"} option is given, the corresponding
1290 translation functions may depend on the current theory or proof
1291 context. This allows to implement advanced syntax mechanisms, as
1292 translations functions may refer to specific theory declarations or
1293 auxiliary proof data.
1295 See also \cite[\S8]{isabelle-ref} for more information on the
1296 general concept of syntax transformations in Isabelle.
1298 %FIXME proper antiquotations
1300 val parse_ast_translation:
1301 (string * (Proof.context -> ast list -> ast)) list
1302 val parse_translation:
1303 (string * (Proof.context -> term list -> term)) list
1304 val print_translation:
1305 (string * (Proof.context -> term list -> term)) list
1306 val typed_print_translation:
1307 (string * (Proof.context -> bool -> typ -> term list -> term)) list
1308 val print_ast_translation:
1309 (string * (Proof.context -> ast list -> ast)) list