7 chapter {* Isabelle/HOL \label{ch:hol} *}
9 section {* Primitive types \label{sec:hol-typedef} *}
12 \begin{matharray}{rcl}
13 @{command_def (HOL) "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
14 @{command_def (HOL) "typedef"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
18 'typedecl' typespec infix?
20 'typedef' altname? abstype '=' repset
23 altname: '(' (name | 'open' | 'open' name) ')'
25 abstype: typespec infix?
27 repset: term ('morphisms' name name)?
33 \item @{command (HOL) "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} is similar
34 to the original @{command "typedecl"} of Isabelle/Pure (see
35 \secref{sec:types-pure}), but also declares type arity @{text "t ::
36 (type, \<dots>, type) type"}, making @{text t} an actual HOL type
37 constructor. %FIXME check, update
39 \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} sets up
40 a goal stating non-emptiness of the set @{text A}. After finishing
41 the proof, the theory will be augmented by a Gordon/HOL-style type
42 definition, which establishes a bijection between the representing
43 set @{text A} and the new type @{text t}.
45 Technically, @{command (HOL) "typedef"} defines both a type @{text
46 t} and a set (term constant) of the same name (an alternative base
47 name may be given in parentheses). The injection from type to set
48 is called @{text Rep_t}, its inverse @{text Abs_t} (this may be
49 changed via an explicit @{keyword (HOL) "morphisms"} declaration).
51 Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text
52 Abs_t_inverse} provide the most basic characterization as a
53 corresponding injection/surjection pair (in both directions). Rules
54 @{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly
55 more convenient view on the injectivity part, suitable for automated
56 proof tools (e.g.\ in @{attribute simp} or @{attribute iff}
57 declarations). Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and
58 @{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views
59 on surjectivity; these are already declared as set or type rules for
60 the generic @{method cases} and @{method induct} methods.
62 An alternative name may be specified in parentheses; the default is
63 to use @{text t} as indicated before. The ``@{text "(open)"}''
64 declaration suppresses a separate constant definition for the
69 Note that raw type declarations are rarely used in practice; the
70 main application is with experimental (or even axiomatic!) theory
71 fragments. Instead of primitive HOL type definitions, user-level
72 theories usually refer to higher-level packages such as @{command
73 (HOL) "record"} (see \secref{sec:hol-record}) or @{command (HOL)
74 "datatype"} (see \secref{sec:hol-datatype}).
78 section {* Adhoc tuples *}
81 \begin{matharray}{rcl}
82 @{attribute (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\
86 'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))
92 \item @{attribute (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots>
93 \<AND> q\<^sub>1 \<dots> q\<^sub>n"} puts expressions of low-level tuple types into
94 canonical form as specified by the arguments given; the @{text i}-th
95 collection of arguments refers to occurrences in premise @{text i}
96 of the rule. The ``@{text "(complete)"}'' option causes \emph{all}
97 arguments in function applications to be represented canonically
98 according to their tuple type structure.
100 Note that these operations tend to invent funny names for new local
101 parameters to be introduced.
107 section {* Records \label{sec:hol-record} *}
110 In principle, records merely generalize the concept of tuples, where
111 components may be addressed by labels instead of just position. The
112 logical infrastructure of records in Isabelle/HOL is slightly more
113 advanced, though, supporting truly extensible record schemes. This
114 admits operations that are polymorphic with respect to record
115 extension, yielding ``object-oriented'' effects like (single)
116 inheritance. See also \cite{NaraschewskiW-TPHOLs98} for more
117 details on object-oriented verification and record subtyping in HOL.
121 subsection {* Basic concepts *}
124 Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records
125 at the level of terms and types. The notation is as follows:
128 \begin{tabular}{l|l|l}
129 & record terms & record types \\ \hline
130 fixed & @{text "\<lparr>x = a, y = b\<rparr>"} & @{text "\<lparr>x :: A, y :: B\<rparr>"} \\
131 schematic & @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} &
132 @{text "\<lparr>x :: A, y :: B, \<dots> :: M\<rparr>"} \\
136 \noindent The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text
139 A fixed record @{text "\<lparr>x = a, y = b\<rparr>"} has field @{text x} of value
140 @{text a} and field @{text y} of value @{text b}. The corresponding
141 type is @{text "\<lparr>x :: A, y :: B\<rparr>"}, assuming that @{text "a :: A"}
142 and @{text "b :: B"}.
144 A record scheme like @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} contains fields
145 @{text x} and @{text y} as before, but also possibly further fields
146 as indicated by the ``@{text "\<dots>"}'' notation (which is actually part
147 of the syntax). The improper field ``@{text "\<dots>"}'' of a record
148 scheme is called the \emph{more part}. Logically it is just a free
149 variable, which is occasionally referred to as ``row variable'' in
150 the literature. The more part of a record scheme may be
151 instantiated by zero or more further components. For example, the
152 previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z =
153 c, \<dots> = m'\<rparr>"}, where @{text m'} refers to a different more part.
154 Fixed records are special instances of record schemes, where
155 ``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"}
156 element. In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation
157 for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}.
159 \medskip Two key observations make extensible records in a simply
160 typed language like HOL work out:
164 \item the more part is internalized, as a free term or type
167 \item field names are externalized, they cannot be accessed within
168 the logic as first-class values.
172 \medskip In Isabelle/HOL record types have to be defined explicitly,
173 fixing their field names and types, and their (optional) parent
174 record. Afterwards, records may be formed using above syntax, while
175 obeying the canonical order of fields as given by their declaration.
176 The record package provides several standard operations like
177 selectors and updates. The common setup for various generic proof
178 tools enable succinct reasoning patterns. See also the Isabelle/HOL
179 tutorial \cite{isabelle-hol-book} for further instructions on using
184 subsection {* Record specifications *}
187 \begin{matharray}{rcl}
188 @{command_def (HOL) "record"} & : & @{text "theory \<rightarrow> theory"} \\
192 'record' typespec '=' (type '+')? (constdecl +)
198 \item @{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1
199 \<dots> c\<^sub>n :: \<sigma>\<^sub>n"} defines extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"},
200 derived from the optional parent record @{text "\<tau>"} by adding new
201 field components @{text "c\<^sub>i :: \<sigma>\<^sub>i"} etc.
203 The type variables of @{text "\<tau>"} and @{text "\<sigma>\<^sub>i"} need to be
204 covered by the (distinct) parameters @{text "\<alpha>\<^sub>1, \<dots>,
205 \<alpha>\<^sub>m"}. Type constructor @{text t} has to be new, while @{text
206 \<tau>} needs to specify an instance of an existing record type. At
207 least one new field @{text "c\<^sub>i"} has to be specified.
208 Basically, field names need to belong to a unique record. This is
209 not a real restriction in practice, since fields are qualified by
210 the record name internally.
212 The parent record specification @{text \<tau>} is optional; if omitted
213 @{text t} becomes a root record. The hierarchy of all records
214 declared within a theory context forms a forest structure, i.e.\ a
215 set of trees starting with a root record each. There is no way to
216 merge multiple parent records!
218 For convenience, @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} is made a
219 type abbreviation for the fixed record type @{text "\<lparr>c\<^sub>1 ::
220 \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"}, likewise is @{text
221 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>) t_scheme"} made an abbreviation for
222 @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> ::
229 subsection {* Record operations *}
232 Any record definition of the form presented above produces certain
233 standard operations. Selectors and updates are provided for any
234 field, including the improper one ``@{text more}''. There are also
235 cumulative record constructor functions. To simplify the
236 presentation below, we assume for now that @{text "(\<alpha>\<^sub>1, \<dots>,
237 \<alpha>\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 ::
238 \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"}.
240 \medskip \textbf{Selectors} and \textbf{updates} are available for
241 any field (including ``@{text more}''):
243 \begin{matharray}{lll}
244 @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
245 @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
248 There is special syntax for application of updates: @{text "r\<lparr>x :=
249 a\<rparr>"} abbreviates term @{text "x_update a r"}. Further notation for
250 repeated updates is also available: @{text "r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z :=
251 c\<rparr>"} may be written @{text "r\<lparr>x := a, y := b, z := c\<rparr>"}. Note that
252 because of postfix notation the order of fields shown here is
253 reverse than in the actual term. Since repeated updates are just
254 function applications, fields may be freely permuted in @{text "\<lparr>x
255 := a, y := b, z := c\<rparr>"}, as far as logical equality is concerned.
256 Thus commutativity of independent updates can be proven within the
257 logic for any two fields, but not as a general theorem.
259 \medskip The \textbf{make} operation provides a cumulative record
260 constructor function:
262 \begin{matharray}{lll}
263 @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
266 \medskip We now reconsider the case of non-root records, which are
267 derived of some parent. In general, the latter may depend on
268 another parent as well, resulting in a list of \emph{ancestor
269 records}. Appending the lists of fields of all ancestors results in
270 a certain field prefix. The record package automatically takes care
271 of this by lifting operations over this context of ancestor fields.
272 Assuming that @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} has ancestor
273 fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"},
274 the above record operations will get the following types:
278 @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
279 @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow>
280 \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
281 \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
282 @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>
283 \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
287 \noindent Some further operations address the extension aspect of a
288 derived record scheme specifically: @{text "t.fields"} produces a
289 record fragment consisting of exactly the new fields introduced here
290 (the result may serve as a more part elsewhere); @{text "t.extend"}
291 takes a fixed record and adds a given more part; @{text
292 "t.truncate"} restricts a record scheme to a fixed record.
296 @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
297 @{text "t.extend"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow>
298 \<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
299 @{text "t.truncate"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
303 \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide
308 subsection {* Derived rules and proof tools *}
311 The record package proves several results internally, declaring
312 these facts to appropriate proof tools. This enables users to
313 reason about record structures quite conveniently. Assume that
314 @{text t} is a record type as specified above.
318 \item Standard conversions for selectors or updates applied to
319 record constructor terms are made part of the default Simplifier
320 context; thus proofs by reduction of basic operations merely require
321 the @{method simp} method without further arguments. These rules
322 are available as @{text "t.simps"}, too.
324 \item Selectors applied to updated records are automatically reduced
325 by an internal simplification procedure, which is also part of the
326 standard Simplifier setup.
328 \item Inject equations of a form analogous to @{prop "(x, y) = (x',
329 y') \<equiv> x = x' \<and> y = y'"} are declared to the Simplifier and Classical
330 Reasoner as @{attribute iff} rules. These rules are available as
333 \item The introduction rule for record equality analogous to @{text
334 "x r = x r' \<Longrightarrow> y r = y r' \<dots> \<Longrightarrow> r = r'"} is declared to the Simplifier,
335 and as the basic rule context as ``@{attribute intro}@{text "?"}''.
336 The rule is called @{text "t.equality"}.
338 \item Representations of arbitrary record expressions as canonical
339 constructor terms are provided both in @{method cases} and @{method
340 induct} format (cf.\ the generic proof methods of the same name,
341 \secref{sec:cases-induct}). Several variations are available, for
342 fixed records, record schemes, more parts etc.
344 The generic proof methods are sufficiently smart to pick the most
345 sensible rule according to the type of the indicated record
346 expression: users just need to apply something like ``@{text "(cases
347 r)"}'' to a certain proof problem.
349 \item The derived record operations @{text "t.make"}, @{text
350 "t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not}
351 treated automatically, but usually need to be expanded by hand,
352 using the collective fact @{text "t.defs"}.
358 section {* Datatypes \label{sec:hol-datatype} *}
361 \begin{matharray}{rcl}
362 @{command_def (HOL) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
363 @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
367 'datatype' (dtspec + 'and')
369 'rep\_datatype' ('(' (name +) ')')? (term +)
372 dtspec: parname? typespec infix? '=' (cons + '|')
374 cons: name (type *) mixfix?
379 \item @{command (HOL) "datatype"} defines inductive datatypes in
382 \item @{command (HOL) "rep_datatype"} represents existing types as
383 inductive ones, generating the standard infrastructure of derived
384 concepts (primitive recursion etc.).
388 The induction and exhaustion theorems generated provide case names
389 according to the constructors involved, while parameters are named
390 after the types (see also \secref{sec:cases-induct}).
392 See \cite{isabelle-HOL} for more details on datatypes, but beware of
393 the old-style theory syntax being used there! Apart from proper
394 proof methods for case-analysis and induction, there are also
395 emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
396 induct_tac} available, see \secref{sec:hol-induct-tac}; these admit
397 to refer directly to the internal structure of subgoals (including
398 internally bound parameters).
402 section {* Recursive functions \label{sec:recursion} *}
405 \begin{matharray}{rcl}
406 @{command_def (HOL) "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
407 @{command_def (HOL) "fun"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
408 @{command_def (HOL) "function"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
409 @{command_def (HOL) "termination"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
413 'primrec' target? fixes 'where' equations
415 equations: (thmdecl? prop + '|')
417 ('fun' | 'function') target? functionopts? fixes 'where' clauses
419 clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
421 functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
423 'termination' ( term )?
428 \item @{command (HOL) "primrec"} defines primitive recursive
429 functions over datatypes, see also \cite{isabelle-HOL}.
431 \item @{command (HOL) "function"} defines functions by general
432 wellfounded recursion. A detailed description with examples can be
433 found in \cite{isabelle-function}. The function is specified by a
434 set of (possibly conditional) recursive equations with arbitrary
435 pattern matching. The command generates proof obligations for the
436 completeness and the compatibility of patterns.
438 The defined function is considered partial, and the resulting
439 simplification rules (named @{text "f.psimps"}) and induction rule
440 (named @{text "f.pinduct"}) are guarded by a generated domain
441 predicate @{text "f_dom"}. The @{command (HOL) "termination"}
442 command can then be used to establish that the function is total.
444 \item @{command (HOL) "fun"} is a shorthand notation for ``@{command
445 (HOL) "function"}~@{text "(sequential)"}, followed by automated
446 proof attempts regarding pattern matching and termination. See
447 \cite{isabelle-function} for further details.
449 \item @{command (HOL) "termination"}~@{text f} commences a
450 termination proof for the previously defined function @{text f}. If
451 this is omitted, the command refers to the most recent function
452 definition. After the proof is closed, the recursive equations and
453 the induction principle is established.
459 Recursive definitions introduced by the @{command (HOL) "function"}
461 reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text
462 "c.induct"} (where @{text c} is the name of the function definition)
463 refers to a specific induction rule, with parameters named according
464 to the user-specified equations.
465 For the @{command (HOL) "primrec"} the induction principle coincides
466 with structural recursion on the datatype the recursion is carried
468 Case names of @{command (HOL)
469 "primrec"} are that of the datatypes involved, while those of
470 @{command (HOL) "function"} are numbered (starting from 1).
472 The equations provided by these packages may be referred later as
473 theorem list @{text "f.simps"}, where @{text f} is the (collective)
474 name of the functions defined. Individual equations may be named
477 The @{command (HOL) "function"} command accepts the following
482 \item @{text sequential} enables a preprocessor which disambiguates
483 overlapping patterns by making them mutually disjoint. Earlier
484 equations take precedence over later ones. This allows to give the
485 specification in a format very similar to functional programming.
486 Note that the resulting simplification and induction rules
487 correspond to the transformed specification, not the one given
488 originally. This usually means that each equation given by the user
489 may result in several theroems. Also note that this automatic
490 transformation only works for ML-style datatype patterns.
492 \item @{text domintros} enables the automated generation of
493 introduction rules for the domain predicate. While mostly not
494 needed, they can be helpful in some proofs about partial functions.
496 \item @{text tailrec} generates the unconstrained recursive
497 equations even without a termination proof, provided that the
498 function is tail-recursive. This currently only works
500 \item @{text "default d"} allows to specify a default value for a
501 (partial) function, which will ensure that @{text "f x = d x"}
502 whenever @{text "x \<notin> f_dom"}.
508 subsection {* Proof methods related to recursive definitions *}
511 \begin{matharray}{rcl}
512 @{method_def (HOL) pat_completeness} & : & @{text method} \\
513 @{method_def (HOL) relation} & : & @{text method} \\
514 @{method_def (HOL) lexicographic_order} & : & @{text method} \\
520 'lexicographic\_order' (clasimpmod *)
526 \item @{method (HOL) pat_completeness} is a specialized method to
527 solve goals regarding the completeness of pattern matching, as
528 required by the @{command (HOL) "function"} package (cf.\
529 \cite{isabelle-function}).
531 \item @{method (HOL) relation}~@{text R} introduces a termination
532 proof using the relation @{text R}. The resulting proof state will
533 contain goals expressing that @{text R} is wellfounded, and that the
534 arguments of recursive calls decrease with respect to @{text R}.
535 Usually, this method is used as the initial proof step of manual
538 \item @{method (HOL) "lexicographic_order"} attempts a fully
539 automated termination proof by searching for a lexicographic
540 combination of size measures on the arguments of the function. The
541 method accepts the same arguments as the @{method auto} method,
542 which it uses internally to prove local descents. The same context
543 modifiers as for @{method auto} are accepted, see
544 \secref{sec:clasimp}.
546 In case of failure, extensive information is printed, which can help
547 to analyse the situation (cf.\ \cite{isabelle-function}).
553 subsection {* Old-style recursive function definitions (TFL) *}
556 The old TFL commands @{command (HOL) "recdef"} and @{command (HOL)
557 "recdef_tc"} for defining recursive are mostly obsolete; @{command
558 (HOL) "function"} or @{command (HOL) "fun"} should be used instead.
560 \begin{matharray}{rcl}
561 @{command_def (HOL) "recdef"} & : & @{text "theory \<rightarrow> theory)"} \\
562 @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
566 'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
570 hints: '(' 'hints' (recdefmod *) ')'
572 recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
574 tc: nameref ('(' nat ')')?
580 \item @{command (HOL) "recdef"} defines general well-founded
581 recursive functions (using the TFL package), see also
582 \cite{isabelle-HOL}. The ``@{text "(permissive)"}'' option tells
583 TFL to recover from failed proof attempts, returning unfinished
584 results. The @{text recdef_simp}, @{text recdef_cong}, and @{text
585 recdef_wf} hints refer to auxiliary rules to be used in the internal
586 automated proof process of TFL. Additional @{syntax clasimpmod}
587 declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
588 context of the Simplifier (cf.\ \secref{sec:simplifier}) and
589 Classical reasoner (cf.\ \secref{sec:classical}).
591 \item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the
592 proof for leftover termination condition number @{text i} (default
593 1) as generated by a @{command (HOL) "recdef"} definition of
596 Note that in most cases, @{command (HOL) "recdef"} is able to finish
597 its internal proofs without manual intervention.
601 \medskip Hints for @{command (HOL) "recdef"} may be also declared
602 globally, using the following attributes.
604 \begin{matharray}{rcl}
605 @{attribute_def (HOL) recdef_simp} & : & @{text attribute} \\
606 @{attribute_def (HOL) recdef_cong} & : & @{text attribute} \\
607 @{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\
611 ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
617 section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}
620 An \textbf{inductive definition} specifies the least predicate (or
621 set) @{text R} closed under given rules: applying a rule to elements
622 of @{text R} yields a result within @{text R}. For example, a
623 structural operational semantics is an inductive definition of an
626 Dually, a \textbf{coinductive definition} specifies the greatest
627 predicate~/ set @{text R} that is consistent with given rules: every
628 element of @{text R} can be seen as arising by applying a rule to
629 elements of @{text R}. An important example is using bisimulation
630 relations to formalise equivalence of processes and infinite data
633 \medskip The HOL package is related to the ZF one, which is
634 described in a separate paper,\footnote{It appeared in CADE
635 \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
636 which you should refer to in case of difficulties. The package is
637 simpler than that of ZF thanks to implicit type-checking in HOL.
638 The types of the (co)inductive predicates (or sets) determine the
639 domain of the fixedpoint definition, and the package does not have
640 to use inference rules for type-checking.
642 \begin{matharray}{rcl}
643 @{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
644 @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
645 @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
646 @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
647 @{attribute_def (HOL) mono} & : & @{text attribute} \\
651 ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
652 ('where' clauses)? ('monos' thmrefs)?
654 clauses: (thmdecl? prop + '|')
656 'mono' (() | 'add' | 'del')
662 \item @{command (HOL) "inductive"} and @{command (HOL)
663 "coinductive"} define (co)inductive predicates from the
664 introduction rules given in the @{keyword "where"} part. The
665 optional @{keyword "for"} part contains a list of parameters of the
666 (co)inductive predicates that remain fixed throughout the
667 definition. The optional @{keyword "monos"} section contains
668 \emph{monotonicity theorems}, which are required for each operator
669 applied to a recursive set in the introduction rules. There
670 \emph{must} be a theorem of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"},
671 for each premise @{text "M R\<^sub>i t"} in an introduction rule!
673 \item @{command (HOL) "inductive_set"} and @{command (HOL)
674 "coinductive_set"} are wrappers for to the previous commands,
675 allowing the definition of (co)inductive sets.
677 \item @{attribute (HOL) mono} declares monotonicity rules. These
678 rule are involved in the automated monotonicity proof of @{command
685 subsection {* Derived rules *}
688 Each (co)inductive definition @{text R} adds definitions to the
689 theory and also proves some theorems:
693 \item @{text R.intros} is the list of introduction rules as proven
694 theorems, for the recursive predicates (or sets). The rules are
695 also available individually, using the names given them in the
698 \item @{text R.cases} is the case analysis (or elimination) rule;
700 \item @{text R.induct} or @{text R.coinduct} is the (co)induction
705 When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are
706 defined simultaneously, the list of introduction rules is called
707 @{text "R\<^sub>1_\<dots>_R\<^sub>n.intros"}, the case analysis rules are
708 called @{text "R\<^sub>1.cases, \<dots>, R\<^sub>n.cases"}, and the list
709 of mutual induction rules is called @{text
710 "R\<^sub>1_\<dots>_R\<^sub>n.inducts"}.
714 subsection {* Monotonicity theorems *}
717 Each theory contains a default set of theorems that are used in
718 monotonicity proofs. New rules can be added to this set via the
719 @{attribute (HOL) mono} attribute. The HOL theory @{text Inductive}
720 shows how this is done. In general, the following monotonicity
721 theorems may be added:
725 \item Theorems of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"}, for proving
726 monotonicity of inductive definitions whose introduction rules have
727 premises involving terms such as @{text "M R\<^sub>i t"}.
729 \item Monotonicity theorems for logical operators, which are of the
730 general form @{text "(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>"}. For example, in
731 the case of the operator @{text "\<or>"}, the corresponding theorem is
733 \infer{@{text "P\<^sub>1 \<or> P\<^sub>2 \<longrightarrow> Q\<^sub>1 \<or> Q\<^sub>2"}}{@{text "P\<^sub>1 \<longrightarrow> Q\<^sub>1"} & @{text "P\<^sub>2 \<longrightarrow> Q\<^sub>2"}}
736 \item De Morgan style equations for reasoning about the ``polarity''
739 @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad
740 @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}
743 \item Equations for reducing complex operators to more primitive
744 ones whose monotonicity can easily be proved, e.g.
746 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad
747 @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}
752 %FIXME: Example of an inductive definition
756 section {* Arithmetic proof support *}
759 \begin{matharray}{rcl}
760 @{method_def (HOL) arith} & : & @{text method} \\
761 @{attribute_def (HOL) arith_split} & : & @{text attribute} \\
764 The @{method (HOL) arith} method decides linear arithmetic problems
765 (on types @{text nat}, @{text int}, @{text real}). Any current
766 facts are inserted into the goal before running the procedure.
768 The @{attribute (HOL) arith_split} attribute declares case split
769 rules to be expanded before the arithmetic procedure is invoked.
771 Note that a simpler (but faster) version of arithmetic reasoning is
772 already performed by the Simplifier.
776 section {* Invoking automated reasoning tools -- The Sledgehammer *}
779 Isabelle/HOL includes a generic \emph{ATP manager} that allows
780 external automated reasoning tools to crunch a pending goal.
781 Supported provers include E\footnote{\url{http://www.eprover.org}},
782 SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire.
783 There is also a wrapper to invoke provers remotely via the
784 SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}}
787 The problem passed to external provers consists of the goal together
788 with a smart selection of lemmas from the current theory context.
789 The result of a successful proof search is some source text that
790 usually reconstructs the proof within Isabelle, without requiring
791 external provers again. The Metis
792 prover\footnote{\url{http://www.gilith.com/software/metis/}} that is
793 integrated into Isabelle/HOL is being used here.
795 In this mode of operation, heavy means of automated reasoning are
796 used as a strong relevance filter, while the main proof checking
797 works via explicit inferences going through the Isabelle kernel.
798 Moreover, rechecking Isabelle proof texts with already specified
799 auxiliary facts is much faster than performing fully automated
800 search over and over again.
802 \begin{matharray}{rcl}
803 @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
804 @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
805 @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
806 @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
807 @{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
808 @{method_def (HOL) metis} & : & @{text method} \\
812 'sledgehammer' (nameref *)
814 'atp\_messages' ('(' nat ')')?
822 \item @{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \<dots> prover\<^sub>n"}
823 invokes the specified automated theorem provers on the first
824 subgoal. Provers are run in parallel, the first successful result
825 is displayed, and the other attempts are terminated.
827 Provers are defined in the theory context, see also @{command (HOL)
828 print_atps}. If no provers are given as arguments to @{command
829 (HOL) sledgehammer}, the system refers to the default defined as
830 ``ATP provers'' preference by the user interface.
832 There are additional preferences for timeout (default: 60 seconds),
833 and the maximum number of independent prover processes (default: 5);
834 excessive provers are automatically terminated.
836 \item @{command (HOL) print_atps} prints the list of automated
837 theorem provers available to the @{command (HOL) sledgehammer}
840 \item @{command (HOL) atp_info} prints information about presently
841 running provers, including elapsed runtime, and the remaining time
844 \item @{command (HOL) atp_kill} terminates all presently running
847 \item @{command (HOL) atp_messages} displays recent messages issued
848 by automated theorem provers. This allows to examine results that
849 might have got lost due to the asynchronous nature of default
850 @{command (HOL) sledgehammer} output. An optional message limit may
851 be specified (default 5).
853 \item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover
854 with the given facts. Metis is an automated proof tool of medium
855 strength, but is fully integrated into Isabelle/HOL, with explicit
856 inferences going through the kernel. Thus its results are
857 guaranteed to be ``correct by construction''.
859 Note that all facts used with Metis need to be specified as explicit
860 arguments. There are no rule declarations as for other Isabelle
861 provers, like @{method blast} or @{method fast}.
867 section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *}
870 The following tools of Isabelle/HOL support cases analysis and
871 induction in unstructured tactic scripts; see also
872 \secref{sec:cases-induct} for proper Isar versions of similar ideas.
874 \begin{matharray}{rcl}
875 @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & @{text method} \\
876 @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\
877 @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\
878 @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
882 'case\_tac' goalspec? term rule?
884 'induct\_tac' goalspec? (insts * 'and') rule?
886 'ind\_cases' (prop +) ('for' (name +)) ?
888 'inductive\_cases' (thmdecl? (prop +) + 'and')
891 rule: ('rule' ':' thmref)
897 \item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit
898 to reason about inductive types. Rules are selected according to
899 the declarations by the @{attribute cases} and @{attribute induct}
900 attributes, cf.\ \secref{sec:cases-induct}. The @{command (HOL)
901 datatype} package already takes care of this.
903 These unstructured tactics feature both goal addressing and dynamic
904 instantiation. Note that named rule cases are \emph{not} provided
905 as would be by the proper @{method cases} and @{method induct} proof
906 methods (see \secref{sec:cases-induct}). Unlike the @{method
907 induct} method, @{method induct_tac} does not handle structured rule
908 statements, only the compact object-logic conclusion of the subgoal
911 \item @{method (HOL) ind_cases} and @{command (HOL)
912 "inductive_cases"} provide an interface to the internal @{ML_text
913 mk_cases} operation. Rules are simplified in an unrestricted
916 While @{method (HOL) ind_cases} is a proof method to apply the
917 result immediately as elimination rules, @{command (HOL)
918 "inductive_cases"} provides case split theorems at the theory level
919 for later use. The @{keyword "for"} argument of the @{method (HOL)
920 ind_cases} method allows to specify a list of variables that should
921 be generalized before applying the resulting rule.
927 section {* Executable code *}
930 Isabelle/Pure provides two generic frameworks to support code
931 generation from executable specifications. Isabelle/HOL
932 instantiates these mechanisms in a way that is amenable to end-user
935 One framework generates code from both functional and relational
936 programs to SML. See \cite{isabelle-HOL} for further information
937 (this actually covers the new-style theory format as well).
939 \begin{matharray}{rcl}
940 @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
941 @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
942 @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
943 @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
944 @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
945 @{attribute_def (HOL) code} & : & @{text attribute} \\
952 ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
953 ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
954 'contains' ( ( name '=' term ) + | term + )
957 modespec: '(' ( name * ) ')'
960 'consts\_code' (codespec +)
963 codespec: const template attachment ?
966 'types\_code' (tycodespec +)
969 tycodespec: name template attachment ?
975 template: '(' string ')'
978 attachment: 'attach' modespec ? verblbrace text verbrbrace
987 \item @{command (HOL) "value"}~@{text t} evaluates and prints a term
988 using the code generator.
992 \medskip The other framework generates code from functional programs
993 (including overloading using type classes) to SML \cite{SML}, OCaml
994 \cite{OCaml} and Haskell \cite{haskell-revised-report}.
995 Conceptually, code generation is split up in three steps:
996 \emph{selection} of code theorems, \emph{translation} into an
997 abstract executable view and \emph{serialization} to a specific
998 \emph{target language}. See \cite{isabelle-codegen} for an
999 introduction on how to use it.
1001 \begin{matharray}{rcl}
1002 @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1003 @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1004 @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1005 @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
1006 @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
1007 @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
1008 @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
1009 @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
1010 @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
1011 @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
1012 @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
1013 @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
1014 @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
1015 @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1016 @{attribute_def (HOL) code} & : & @{text attribute} \\
1020 'export\_code' ( constexpr + ) ? \\
1021 ( ( 'in' target ( 'module\_name' string ) ? \\
1022 ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
1025 'code\_thms' ( constexpr + ) ?
1028 'code\_deps' ( constexpr + ) ?
1034 constexpr: ( const | 'name.*' | '*' )
1037 typeconstructor: nameref
1043 target: 'OCaml' | 'SML' | 'Haskell'
1046 'code\_datatype' const +
1049 'code\_const' (const + 'and') \\
1050 ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1053 'code\_type' (typeconstructor + 'and') \\
1054 ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1057 'code\_class' (class + 'and') \\
1058 ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
1061 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
1062 ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
1065 'code\_monad' const const target
1068 'code\_reserved' target ( string + )
1071 'code\_include' target ( string ( string | '-') )
1074 'code\_modulename' target ( ( string string ) + )
1077 'code\_abort' ( const + )
1080 syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
1083 'code' ( 'inline' ) ? ( 'del' ) ?
1089 \item @{command (HOL) "export_code"} is the canonical interface for
1090 generating and serializing code: for a given list of constants, code
1091 is generated for the specified target languages. Abstract code is
1092 cached incrementally. If no constant is given, the currently cached
1093 code is serialized. If no serialization instruction is given, only
1094 abstract code is cached.
1096 Constants may be specified by giving them literally, referring to
1097 all executable contants within a certain theory by giving @{text
1098 "name.*"}, or referring to \emph{all} executable constants currently
1099 available by giving @{text "*"}.
1101 By default, for each involved theory one corresponding name space
1102 module is generated. Alternativly, a module name may be specified
1103 after the @{keyword "module_name"} keyword; then \emph{all} code is
1104 placed in this module.
1106 For \emph{SML} and \emph{OCaml}, the file specification refers to a
1107 single file; for \emph{Haskell}, it refers to a whole directory,
1108 where code is generated in multiple files reflecting the module
1109 hierarchy. The file specification ``@{text "-"}'' denotes standard
1110 output. For \emph{SML}, omitting the file specification compiles
1111 code internally in the context of the current ML session.
1113 Serializers take an optional list of arguments in parentheses. For
1114 \emph{Haskell} a module name prefix may be given using the ``@{text
1115 "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim
1116 "deriving (Read, Show)"}'' clause to each appropriate datatype
1119 \item @{command (HOL) "code_thms"} prints a list of theorems
1120 representing the corresponding program containing all given
1121 constants; if no constants are given, the currently cached code
1122 theorems are printed.
1124 \item @{command (HOL) "code_deps"} visualizes dependencies of
1125 theorems representing the corresponding program containing all given
1126 constants; if no constants are given, the currently cached code
1127 theorems are visualized.
1129 \item @{command (HOL) "code_datatype"} specifies a constructor set
1132 \item @{command (HOL) "code_const"} associates a list of constants
1133 with target-specific serializations; omitting a serialization
1134 deletes an existing serialization.
1136 \item @{command (HOL) "code_type"} associates a list of type
1137 constructors with target-specific serializations; omitting a
1138 serialization deletes an existing serialization.
1140 \item @{command (HOL) "code_class"} associates a list of classes
1141 with target-specific class names; omitting a serialization deletes
1142 an existing serialization. This applies only to \emph{Haskell}.
1144 \item @{command (HOL) "code_instance"} declares a list of type
1145 constructor / class instance relations as ``already present'' for a
1146 given target. Omitting a ``@{text "-"}'' deletes an existing
1147 ``already present'' declaration. This applies only to
1150 \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
1151 to generate monadic code for Haskell.
1153 \item @{command (HOL) "code_reserved"} declares a list of names as
1154 reserved for a given target, preventing it to be shadowed by any
1157 \item @{command (HOL) "code_include"} adds arbitrary named content
1158 (``include'') to generated code. A ``@{text "-"}'' as last argument
1159 will remove an already added ``include''.
1161 \item @{command (HOL) "code_modulename"} declares aliasings from one
1162 module name onto another.
1164 \item @{command (HOL) "code_abort"} declares constants which are not
1165 required to have a definition by means of defining equations; if
1166 needed these are implemented by program abort instead.
1168 \item @{attribute (HOL) code} explicitly selects (or with option
1169 ``@{text "del"}'' deselects) a defining equation for code
1170 generation. Usually packages introducing defining equations provide
1171 a reasonable default setup for selection.
1173 \item @{attribute (HOL) code}~@{text inline} declares (or with
1174 option ``@{text "del"}'' removes) inlining theorems which are
1175 applied as rewrite rules to any defining equation during
1178 \item @{command (HOL) "print_codesetup"} gives an overview on
1179 selected defining equations, code generator datatypes and
1186 section {* Definition by specification \label{sec:hol-specification} *}
1189 \begin{matharray}{rcl}
1190 @{command_def (HOL) "specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
1191 @{command_def (HOL) "ax_specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
1195 ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
1197 decl: ((name ':')? term '(' 'overloaded' ')'?)
1202 \item @{command (HOL) "specification"}~@{text "decls \<phi>"} sets up a
1203 goal stating the existence of terms with the properties specified to
1204 hold for the constants given in @{text decls}. After finishing the
1205 proof, the theory will be augmented with definitions for the given
1206 constants, as well as with theorems stating the properties for these
1209 \item @{command (HOL) "ax_specification"}~@{text "decls \<phi>"} sets up
1210 a goal stating the existence of terms with the properties specified
1211 to hold for the constants given in @{text decls}. After finishing
1212 the proof, the theory will be augmented with axioms expressing the
1213 properties given in the first place.
1215 \item @{text decl} declares a constant to be defined by the
1216 specification given. The definition for the constant @{text c} is
1217 bound to the name @{text c_def} unless a theorem name is given in
1218 the declaration. Overloaded constants should be declared as such.
1222 Whether to use @{command (HOL) "specification"} or @{command (HOL)
1223 "ax_specification"} is to some extent a matter of style. @{command
1224 (HOL) "specification"} introduces no new axioms, and so by
1225 construction cannot introduce inconsistencies, whereas @{command
1226 (HOL) "ax_specification"} does introduce axioms, but only after the
1227 user has explicitly proven it to be safe. A practical issue must be
1228 considered, though: After introducing two constants with the same
1229 properties using @{command (HOL) "specification"}, one can prove
1230 that the two constants are, in fact, equal. If this might be a
1231 problem, one should use @{command (HOL) "ax_specification"}.