5 chapter {* Isabelle/HOL \label{ch:hol} *}
7 section {* Higher-Order Logic *}
9 text {* Isabelle/HOL is based on Higher-Order Logic, a polymorphic
10 version of Church's Simple Theory of Types. HOL can be best
11 understood as a simply-typed version of classical set theory. The
12 logic was first implemented in Gordon's HOL system
13 \cite{mgordon-hol}. It extends Church's original logic
14 \cite{church40} by explicit type variables (naive polymorphism) and
15 a sound axiomatization scheme for new types based on subsets of
18 Andrews's book \cite{andrews86} is a full description of the
19 original Church-style higher-order logic, with proofs of correctness
20 and completeness wrt.\ certain set-theoretic interpretations. The
21 particular extensions of Gordon-style HOL are explained semantically
22 in two chapters of the 1993 HOL book \cite{pitts93}.
24 Experience with HOL over decades has demonstrated that higher-order
25 logic is widely applicable in many areas of mathematics and computer
26 science. In a sense, Higher-Order Logic is simpler than First-Order
27 Logic, because there are fewer restrictions and special cases. Note
28 that HOL is \emph{weaker} than FOL with axioms for ZF set theory,
29 which is traditionally considered the standard foundation of regular
30 mathematics, but for most applications this does not matter. If you
31 prefer ML to Lisp, you will probably prefer HOL to ZF.
33 \medskip The syntax of HOL follows @{text "\<lambda>"}-calculus and
34 functional programming. Function application is curried. To apply
35 the function @{text f} of type @{text "\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"} to the
36 arguments @{text a} and @{text b} in HOL, you simply write @{text "f
37 a b"} (as in ML or Haskell). There is no ``apply'' operator; the
38 existing application of the Pure @{text "\<lambda>"}-calculus is re-used.
39 Note that in HOL @{text "f (a, b)"} means ``@{text "f"} applied to
40 the pair @{text "(a, b)"} (which is notation for @{text "Pair a
41 b"}). The latter typically introduces extra formal efforts that can
42 be avoided by currying functions by default. Explicit tuples are as
43 infrequent in HOL formalizations as in good ML or Haskell programs.
45 \medskip Isabelle/HOL has a distinct feel, compared to other
46 object-logics like Isabelle/ZF. It identifies object-level types
47 with meta-level types, taking advantage of the default
48 type-inference mechanism of Isabelle/Pure. HOL fully identifies
49 object-level functions with meta-level functions, with native
50 abstraction and application.
52 These identifications allow Isabelle to support HOL particularly
53 nicely, but they also mean that HOL requires some sophistication
54 from the user. In particular, an understanding of Hindley-Milner
55 type-inference with type-classes, which are both used extensively in
56 the standard libraries and applications. Beginners can set
57 @{attribute show_types} or even @{attribute show_sorts} to get more
58 explicit information about the result of type-inference. *}
61 section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}
63 text {* An \emph{inductive definition} specifies the least predicate
64 or set @{text R} closed under given rules: applying a rule to
65 elements of @{text R} yields a result within @{text R}. For
66 example, a structural operational semantics is an inductive
67 definition of an evaluation relation.
69 Dually, a \emph{coinductive definition} specifies the greatest
70 predicate or set @{text R} that is consistent with given rules:
71 every element of @{text R} can be seen as arising by applying a rule
72 to elements of @{text R}. An important example is using
73 bisimulation relations to formalise equivalence of processes and
74 infinite data structures.
76 Both inductive and coinductive definitions are based on the
77 Knaster-Tarski fixed-point theorem for complete lattices. The
78 collection of introduction rules given by the user determines a
79 functor on subsets of set-theoretic relations. The required
80 monotonicity of the recursion scheme is proven as a prerequisite to
81 the fixed-point definition and the resulting consequences. This
82 works by pushing inclusion through logical connectives and any other
83 operator that might be wrapped around recursive occurrences of the
84 defined relation: there must be a monotonicity theorem of the form
85 @{text "A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B"}, for each premise @{text "\<M> R t"} in an
86 introduction rule. The default rule declarations of Isabelle/HOL
87 already take care of most common situations.
89 \begin{matharray}{rcl}
90 @{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
91 @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
92 @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
93 @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
94 @{attribute_def (HOL) mono} & : & @{text attribute} \\
98 (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
99 @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
101 @{syntax \"fixes\"} (@'for' @{syntax \"fixes\"})? (@'where' clauses)? \\
102 (@'monos' @{syntax thmrefs})?
104 clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
106 @@{attribute (HOL) mono} (() | 'add' | 'del')
111 \item @{command (HOL) "inductive"} and @{command (HOL)
112 "coinductive"} define (co)inductive predicates from the introduction
115 The propositions given as @{text "clauses"} in the @{keyword
116 "where"} part are either rules of the usual @{text "\<And>/\<Longrightarrow>"} format
117 (with arbitrary nesting), or equalities using @{text "\<equiv>"}. The
118 latter specifies extra-logical abbreviations in the sense of
119 @{command_ref abbreviation}. Introducing abstract syntax
120 simultaneously with the actual introduction rules is occasionally
121 useful for complex specifications.
123 The optional @{keyword "for"} part contains a list of parameters of
124 the (co)inductive predicates that remain fixed throughout the
125 definition, in contrast to arguments of the relation that may vary
126 in each occurrence within the given @{text "clauses"}.
128 The optional @{keyword "monos"} declaration contains additional
129 \emph{monotonicity theorems}, which are required for each operator
130 applied to a recursive set in the introduction rules.
132 \item @{command (HOL) "inductive_set"} and @{command (HOL)
133 "coinductive_set"} are wrappers for to the previous commands for
134 native HOL predicates. This allows to define (co)inductive sets,
135 where multiple arguments are simulated via tuples.
137 \item @{attribute (HOL) mono} declares monotonicity rules in the
138 context. These rule are involved in the automated monotonicity
139 proof of the above inductive and coinductive definitions.
145 subsection {* Derived rules *}
147 text {* A (co)inductive definition of @{text R} provides the following
152 \item @{text R.intros} is the list of introduction rules as proven
153 theorems, for the recursive predicates (or sets). The rules are
154 also available individually, using the names given them in the
157 \item @{text R.cases} is the case analysis (or elimination) rule;
159 \item @{text R.induct} or @{text R.coinduct} is the (co)induction
164 When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are
165 defined simultaneously, the list of introduction rules is called
166 @{text "R\<^sub>1_\<dots>_R\<^sub>n.intros"}, the case analysis rules are
167 called @{text "R\<^sub>1.cases, \<dots>, R\<^sub>n.cases"}, and the list
168 of mutual induction rules is called @{text
169 "R\<^sub>1_\<dots>_R\<^sub>n.inducts"}.
173 subsection {* Monotonicity theorems *}
175 text {* The context maintains a default set of theorems that are used
176 in monotonicity proofs. New rules can be declared via the
177 @{attribute (HOL) mono} attribute. See the main Isabelle/HOL
178 sources for some examples. The general format of such monotonicity
179 theorems is as follows:
183 \item Theorems of the form @{text "A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B"}, for proving
184 monotonicity of inductive definitions whose introduction rules have
185 premises involving terms such as @{text "\<M> R t"}.
187 \item Monotonicity theorems for logical operators, which are of the
188 general form @{text "(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>"}. For example, in
189 the case of the operator @{text "\<or>"}, the corresponding theorem is
191 \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"}}
194 \item De Morgan style equations for reasoning about the ``polarity''
197 @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad
198 @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}
201 \item Equations for reducing complex operators to more primitive
202 ones whose monotonicity can easily be proved, e.g.
204 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad
205 @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}
211 subsubsection {* Examples *}
213 text {* The finite powerset operator can be defined inductively like this: *}
215 inductive_set Fin :: "'a set \<Rightarrow> 'a set set" for A :: "'a set"
217 empty: "{} \<in> Fin A"
218 | insert: "a \<in> A \<Longrightarrow> B \<in> Fin A \<Longrightarrow> insert a B \<in> Fin A"
220 text {* The accessible part of a relation is defined as follows: *}
222 inductive acc :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
223 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
224 where acc: "(\<And>y. y \<prec> x \<Longrightarrow> acc r y) \<Longrightarrow> acc r x"
226 text {* Common logical connectives can be easily characterized as
227 non-recursive inductive definitions with parameters, but without
230 inductive AND for A B :: bool
231 where "A \<Longrightarrow> B \<Longrightarrow> AND A B"
233 inductive OR for A B :: bool
234 where "A \<Longrightarrow> OR A B"
235 | "B \<Longrightarrow> OR A B"
237 inductive EXISTS for B :: "'a \<Rightarrow> bool"
238 where "B a \<Longrightarrow> EXISTS B"
240 text {* Here the @{text "cases"} or @{text "induct"} rules produced by
241 the @{command inductive} package coincide with the expected
242 elimination rules for Natural Deduction. Already in the original
243 article by Gerhard Gentzen \cite{Gentzen:1935} there is a hint that
244 each connective can be characterized by its introductions, and the
245 elimination can be constructed systematically. *}
248 section {* Recursive functions \label{sec:recursion} *}
251 \begin{matharray}{rcl}
252 @{command_def (HOL) "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
253 @{command_def (HOL) "fun"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
254 @{command_def (HOL) "function"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
255 @{command_def (HOL) "termination"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
259 @@{command (HOL) primrec} @{syntax target}? @{syntax \"fixes\"} @'where' equations
261 (@@{command (HOL) fun} | @@{command (HOL) function}) @{syntax target}? functionopts?
262 @{syntax \"fixes\"} \\ @'where' equations
265 equations: (@{syntax thmdecl}? @{syntax prop} + '|')
267 functionopts: '(' (('sequential' | 'domintros') + ',') ')'
269 @@{command (HOL) termination} @{syntax term}?
274 \item @{command (HOL) "primrec"} defines primitive recursive
275 functions over datatypes (see also @{command_ref (HOL) datatype} and
276 @{command_ref (HOL) rep_datatype}). The given @{text equations}
277 specify reduction rules that are produced by instantiating the
278 generic combinator for primitive recursion that is available for
281 Each equation needs to be of the form:
283 @{text [display] "f x\<^sub>1 \<dots> x\<^sub>m (C y\<^sub>1 \<dots> y\<^sub>k) z\<^sub>1 \<dots> z\<^sub>n = rhs"}
285 such that @{text C} is a datatype constructor, @{text rhs} contains
286 only the free variables on the left-hand side (or from the context),
287 and all recursive occurrences of @{text "f"} in @{text "rhs"} are of
288 the form @{text "f \<dots> y\<^sub>i \<dots>"} for some @{text i}. At most one
289 reduction rule for each constructor can be given. The order does
290 not matter. For missing constructors, the function is defined to
291 return a default value, but this equation is made difficult to
294 The reduction rules are declared as @{attribute simp} by default,
295 which enables standard proof methods like @{method simp} and
296 @{method auto} to normalize expressions of @{text "f"} applied to
297 datatype constructions, by simulating symbolic computation via
300 \item @{command (HOL) "function"} defines functions by general
301 wellfounded recursion. A detailed description with examples can be
302 found in \cite{isabelle-function}. The function is specified by a
303 set of (possibly conditional) recursive equations with arbitrary
304 pattern matching. The command generates proof obligations for the
305 completeness and the compatibility of patterns.
307 The defined function is considered partial, and the resulting
308 simplification rules (named @{text "f.psimps"}) and induction rule
309 (named @{text "f.pinduct"}) are guarded by a generated domain
310 predicate @{text "f_dom"}. The @{command (HOL) "termination"}
311 command can then be used to establish that the function is total.
313 \item @{command (HOL) "fun"} is a shorthand notation for ``@{command
314 (HOL) "function"}~@{text "(sequential)"}, followed by automated
315 proof attempts regarding pattern matching and termination. See
316 \cite{isabelle-function} for further details.
318 \item @{command (HOL) "termination"}~@{text f} commences a
319 termination proof for the previously defined function @{text f}. If
320 this is omitted, the command refers to the most recent function
321 definition. After the proof is closed, the recursive equations and
322 the induction principle is established.
326 Recursive definitions introduced by the @{command (HOL) "function"}
327 command accommodate reasoning by induction (cf.\ @{method induct}):
328 rule @{text "f.induct"} refers to a specific induction rule, with
329 parameters named according to the user-specified equations. Cases
330 are numbered starting from 1. For @{command (HOL) "primrec"}, the
331 induction principle coincides with structural recursion on the
332 datatype where the recursion is carried out.
334 The equations provided by these packages may be referred later as
335 theorem list @{text "f.simps"}, where @{text f} is the (collective)
336 name of the functions defined. Individual equations may be named
339 The @{command (HOL) "function"} command accepts the following
344 \item @{text sequential} enables a preprocessor which disambiguates
345 overlapping patterns by making them mutually disjoint. Earlier
346 equations take precedence over later ones. This allows to give the
347 specification in a format very similar to functional programming.
348 Note that the resulting simplification and induction rules
349 correspond to the transformed specification, not the one given
350 originally. This usually means that each equation given by the user
351 may result in several theorems. Also note that this automatic
352 transformation only works for ML-style datatype patterns.
354 \item @{text domintros} enables the automated generation of
355 introduction rules for the domain predicate. While mostly not
356 needed, they can be helpful in some proofs about partial functions.
361 subsubsection {* Example: evaluation of expressions *}
363 text {* Subsequently, we define mutual datatypes for arithmetic and
364 boolean expressions, and use @{command primrec} for evaluation
365 functions that follow the same recursive structure. *}
368 IF "'a bexp" "'a aexp" "'a aexp"
369 | Sum "'a aexp" "'a aexp"
370 | Diff "'a aexp" "'a aexp"
374 Less "'a aexp" "'a aexp"
375 | And "'a bexp" "'a bexp"
379 text {* \medskip Evaluation of arithmetic and boolean expressions *}
381 primrec evala :: "('a \<Rightarrow> nat) \<Rightarrow> 'a aexp \<Rightarrow> nat"
382 and evalb :: "('a \<Rightarrow> nat) \<Rightarrow> 'a bexp \<Rightarrow> bool"
384 "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
385 | "evala env (Sum a1 a2) = evala env a1 + evala env a2"
386 | "evala env (Diff a1 a2) = evala env a1 - evala env a2"
387 | "evala env (Var v) = env v"
388 | "evala env (Num n) = n"
389 | "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
390 | "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
391 | "evalb env (Neg b) = (\<not> evalb env b)"
393 text {* Since the value of an expression depends on the value of its
394 variables, the functions @{const evala} and @{const evalb} take an
395 additional parameter, an \emph{environment} that maps variables to
398 \medskip Substitution on expressions can be defined similarly. The
399 mapping @{text f} of type @{typ "'a \<Rightarrow> 'a aexp"} given as a
400 parameter is lifted canonically on the types @{typ "'a aexp"} and
401 @{typ "'a bexp"}, respectively.
404 primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
405 and substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp"
407 "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
408 | "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
409 | "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
410 | "substa f (Var v) = f v"
411 | "substa f (Num n) = Num n"
412 | "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
413 | "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
414 | "substb f (Neg b) = Neg (substb f b)"
416 text {* In textbooks about semantics one often finds substitution
417 theorems, which express the relationship between substitution and
418 evaluation. For @{typ "'a aexp"} and @{typ "'a bexp"}, we can prove
419 such a theorem by mutual induction, followed by simplification.
423 "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
424 "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
425 by (induct a and b) simp_all
428 "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
429 "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
430 by (induct a and b) simp_all
433 subsubsection {* Example: a substitution function for terms *}
435 text {* Functions on datatypes with nested recursion are also defined
436 by mutual primitive recursion. *}
438 datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
440 text {* A substitution function on type @{typ "('a, 'b) term"} can be
441 defined as follows, by working simultaneously on @{typ "('a, 'b)
444 primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term" and
445 subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
447 "subst_term f (Var a) = f a"
448 | "subst_term f (App b ts) = App b (subst_term_list f ts)"
449 | "subst_term_list f [] = []"
450 | "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
452 text {* The recursion scheme follows the structure of the unfolded
453 definition of type @{typ "('a, 'b) term"}. To prove properties of this
454 substitution function, mutual induction is needed:
457 lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)" and
458 "subst_term_list (subst_term f1 \<circ> f2) ts = subst_term_list f1 (subst_term_list f2 ts)"
459 by (induct t and ts) simp_all
462 subsubsection {* Example: a map function for infinitely branching trees *}
464 text {* Defining functions on infinitely branching datatypes by
465 primitive recursion is just as easy.
468 datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
470 primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
472 "map_tree f (Atom a) = Atom (f a)"
473 | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
475 text {* Note that all occurrences of functions such as @{text ts}
476 above must be applied to an argument. In particular, @{term
477 "map_tree f \<circ> ts"} is not allowed here. *}
479 text {* Here is a simple composition lemma for @{term map_tree}: *}
481 lemma "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
482 by (induct t) simp_all
485 subsection {* Proof methods related to recursive definitions *}
488 \begin{matharray}{rcl}
489 @{method_def (HOL) pat_completeness} & : & @{text method} \\
490 @{method_def (HOL) relation} & : & @{text method} \\
491 @{method_def (HOL) lexicographic_order} & : & @{text method} \\
492 @{method_def (HOL) size_change} & : & @{text method} \\
496 @@{method (HOL) relation} @{syntax term}
498 @@{method (HOL) lexicographic_order} (@{syntax clasimpmod} * )
500 @@{method (HOL) size_change} ( orders (@{syntax clasimpmod} * ) )
502 orders: ( 'max' | 'min' | 'ms' ) *
507 \item @{method (HOL) pat_completeness} is a specialized method to
508 solve goals regarding the completeness of pattern matching, as
509 required by the @{command (HOL) "function"} package (cf.\
510 \cite{isabelle-function}).
512 \item @{method (HOL) relation}~@{text R} introduces a termination
513 proof using the relation @{text R}. The resulting proof state will
514 contain goals expressing that @{text R} is wellfounded, and that the
515 arguments of recursive calls decrease with respect to @{text R}.
516 Usually, this method is used as the initial proof step of manual
519 \item @{method (HOL) "lexicographic_order"} attempts a fully
520 automated termination proof by searching for a lexicographic
521 combination of size measures on the arguments of the function. The
522 method accepts the same arguments as the @{method auto} method,
523 which it uses internally to prove local descents. The @{syntax
524 clasimpmod} modifiers are accepted (as for @{method auto}).
526 In case of failure, extensive information is printed, which can help
527 to analyse the situation (cf.\ \cite{isabelle-function}).
529 \item @{method (HOL) "size_change"} also works on termination goals,
530 using a variation of the size-change principle, together with a
531 graph decomposition technique (see \cite{krauss_phd} for details).
532 Three kinds of orders are used internally: @{text max}, @{text min},
533 and @{text ms} (multiset), which is only available when the theory
534 @{text Multiset} is loaded. When no order kinds are given, they are
535 tried in order. The search for a termination proof uses SAT solving
538 For local descent proofs, the @{syntax clasimpmod} modifiers are
539 accepted (as for @{method auto}).
545 subsection {* Functions with explicit partiality *}
548 \begin{matharray}{rcl}
549 @{command_def (HOL) "partial_function"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
550 @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\
554 @@{command (HOL) partial_function} @{syntax target}?
555 '(' @{syntax nameref} ')' @{syntax \"fixes\"} \\
556 @'where' @{syntax thmdecl}? @{syntax prop}
561 \item @{command (HOL) "partial_function"}~@{text "(mode)"} defines
562 recursive functions based on fixpoints in complete partial
563 orders. No termination proof is required from the user or
564 constructed internally. Instead, the possibility of non-termination
565 is modelled explicitly in the result type, which contains an
566 explicit bottom element.
568 Pattern matching and mutual recursion are currently not supported.
569 Thus, the specification consists of a single function described by a
570 single recursive equation.
572 There are no fixed syntactic restrictions on the body of the
573 function, but the induced functional must be provably monotonic
574 wrt.\ the underlying order. The monotonicitity proof is performed
575 internally, and the definition is rejected when it fails. The proof
576 can be influenced by declaring hints using the
577 @{attribute (HOL) partial_function_mono} attribute.
579 The mandatory @{text mode} argument specifies the mode of operation
580 of the command, which directly corresponds to a complete partial
581 order on the result type. By default, the following modes are
585 \item @{text option} defines functions that map into the @{type
586 option} type. Here, the value @{term None} is used to model a
587 non-terminating computation. Monotonicity requires that if @{term
588 None} is returned by a recursive call, then the overall result
589 must also be @{term None}. This is best achieved through the use of
590 the monadic operator @{const "Option.bind"}.
592 \item @{text tailrec} defines functions with an arbitrary result
593 type and uses the slightly degenerated partial order where @{term
594 "undefined"} is the bottom element. Now, monotonicity requires that
595 if @{term undefined} is returned by a recursive call, then the
596 overall result must also be @{term undefined}. In practice, this is
597 only satisfied when each recursive call is a tail call, whose result
598 is directly returned. Thus, this mode of operation allows the
599 definition of arbitrary tail-recursive functions.
602 Experienced users may define new modes by instantiating the locale
603 @{const "partial_function_definitions"} appropriately.
605 \item @{attribute (HOL) partial_function_mono} declares rules for
606 use in the internal monononicity proofs of partial function
614 subsection {* Old-style recursive function definitions (TFL) *}
617 The old TFL commands @{command (HOL) "recdef"} and @{command (HOL)
618 "recdef_tc"} for defining recursive are mostly obsolete; @{command
619 (HOL) "function"} or @{command (HOL) "fun"} should be used instead.
621 \begin{matharray}{rcl}
622 @{command_def (HOL) "recdef"} & : & @{text "theory \<rightarrow> theory)"} \\
623 @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
627 @@{command (HOL) recdef} ('(' @'permissive' ')')? \\
628 @{syntax name} @{syntax term} (@{syntax prop} +) hints?
630 recdeftc @{syntax thmdecl}? tc
632 hints: '(' @'hints' ( recdefmod * ) ')'
634 recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf')
635 (() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod}
637 tc: @{syntax nameref} ('(' @{syntax nat} ')')?
642 \item @{command (HOL) "recdef"} defines general well-founded
643 recursive functions (using the TFL package), see also
644 \cite{isabelle-HOL}. The ``@{text "(permissive)"}'' option tells
645 TFL to recover from failed proof attempts, returning unfinished
646 results. The @{text recdef_simp}, @{text recdef_cong}, and @{text
647 recdef_wf} hints refer to auxiliary rules to be used in the internal
648 automated proof process of TFL. Additional @{syntax clasimpmod}
649 declarations may be given to tune the context of the Simplifier
650 (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\
651 \secref{sec:classical}).
653 \item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the
654 proof for leftover termination condition number @{text i} (default
655 1) as generated by a @{command (HOL) "recdef"} definition of
658 Note that in most cases, @{command (HOL) "recdef"} is able to finish
659 its internal proofs without manual intervention.
663 \medskip Hints for @{command (HOL) "recdef"} may be also declared
664 globally, using the following attributes.
666 \begin{matharray}{rcl}
667 @{attribute_def (HOL) recdef_simp} & : & @{text attribute} \\
668 @{attribute_def (HOL) recdef_cong} & : & @{text attribute} \\
669 @{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\
673 (@@{attribute (HOL) recdef_simp} | @@{attribute (HOL) recdef_cong} |
674 @@{attribute (HOL) recdef_wf}) (() | 'add' | 'del')
679 section {* Datatypes \label{sec:hol-datatype} *}
682 \begin{matharray}{rcl}
683 @{command_def (HOL) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
684 @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
688 @@{command (HOL) datatype} (spec + @'and')
690 @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
693 spec: @{syntax parname}? @{syntax typespec} @{syntax mixfix}? '=' (cons + '|')
695 cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
700 \item @{command (HOL) "datatype"} defines inductive datatypes in
703 \item @{command (HOL) "rep_datatype"} represents existing types as
706 For foundational reasons, some basic types such as @{typ nat}, @{typ
707 "'a \<times> 'b"}, @{typ "'a + 'b"}, @{typ bool} and @{typ unit} are
708 introduced by more primitive means using @{command_ref typedef}. To
709 recover the rich infrastructure of @{command datatype} (e.g.\ rules
710 for @{method cases} and @{method induct} and the primitive recursion
711 combinators), such types may be represented as actual datatypes
712 later. This is done by specifying the constructors of the desired
713 type, and giving a proof of the induction rule, distinctness and
714 injectivity of constructors.
716 For example, see @{file "~~/src/HOL/Sum_Type.thy"} for the
717 representation of the primitive sum type as fully-featured datatype.
721 The generated rules for @{method induct} and @{method cases} provide
722 case names according to the given constructors, while parameters are
723 named after the types (see also \secref{sec:cases-induct}).
725 See \cite{isabelle-HOL} for more details on datatypes, but beware of
726 the old-style theory syntax being used there! Apart from proper
727 proof methods for case-analysis and induction, there are also
728 emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
729 induct_tac} available, see \secref{sec:hol-induct-tac}; these admit
730 to refer directly to the internal structure of subgoals (including
731 internally bound parameters).
735 subsubsection {* Examples *}
737 text {* We define a type of finite sequences, with slightly different
738 names than the existing @{typ "'a list"} that is already in @{theory
741 datatype 'a seq = Empty | Seq 'a "'a seq"
743 text {* We can now prove some simple lemma by structural induction: *}
745 lemma "Seq x xs \<noteq> xs"
746 proof (induct xs arbitrary: x)
748 txt {* This case can be proved using the simplifier: the freeness
749 properties of the datatype are already declared as @{attribute
751 show "Seq x Empty \<noteq> Empty"
755 txt {* The step case is proved similarly. *}
756 show "Seq x (Seq y ys) \<noteq> Seq y ys"
757 using `Seq y ys \<noteq> ys` by simp
760 text {* Here is a more succinct version of the same proof: *}
762 lemma "Seq x xs \<noteq> xs"
763 by (induct xs arbitrary: x) simp_all
766 section {* Records \label{sec:hol-record} *}
769 In principle, records merely generalize the concept of tuples, where
770 components may be addressed by labels instead of just position. The
771 logical infrastructure of records in Isabelle/HOL is slightly more
772 advanced, though, supporting truly extensible record schemes. This
773 admits operations that are polymorphic with respect to record
774 extension, yielding ``object-oriented'' effects like (single)
775 inheritance. See also \cite{NaraschewskiW-TPHOLs98} for more
776 details on object-oriented verification and record subtyping in HOL.
780 subsection {* Basic concepts *}
783 Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records
784 at the level of terms and types. The notation is as follows:
787 \begin{tabular}{l|l|l}
788 & record terms & record types \\ \hline
789 fixed & @{text "\<lparr>x = a, y = b\<rparr>"} & @{text "\<lparr>x :: A, y :: B\<rparr>"} \\
790 schematic & @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} &
791 @{text "\<lparr>x :: A, y :: B, \<dots> :: M\<rparr>"} \\
795 \noindent The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text
798 A fixed record @{text "\<lparr>x = a, y = b\<rparr>"} has field @{text x} of value
799 @{text a} and field @{text y} of value @{text b}. The corresponding
800 type is @{text "\<lparr>x :: A, y :: B\<rparr>"}, assuming that @{text "a :: A"}
801 and @{text "b :: B"}.
803 A record scheme like @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} contains fields
804 @{text x} and @{text y} as before, but also possibly further fields
805 as indicated by the ``@{text "\<dots>"}'' notation (which is actually part
806 of the syntax). The improper field ``@{text "\<dots>"}'' of a record
807 scheme is called the \emph{more part}. Logically it is just a free
808 variable, which is occasionally referred to as ``row variable'' in
809 the literature. The more part of a record scheme may be
810 instantiated by zero or more further components. For example, the
811 previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z =
812 c, \<dots> = m'\<rparr>"}, where @{text m'} refers to a different more part.
813 Fixed records are special instances of record schemes, where
814 ``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"}
815 element. In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation
816 for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}.
818 \medskip Two key observations make extensible records in a simply
819 typed language like HOL work out:
823 \item the more part is internalized, as a free term or type
826 \item field names are externalized, they cannot be accessed within
827 the logic as first-class values.
831 \medskip In Isabelle/HOL record types have to be defined explicitly,
832 fixing their field names and types, and their (optional) parent
833 record. Afterwards, records may be formed using above syntax, while
834 obeying the canonical order of fields as given by their declaration.
835 The record package provides several standard operations like
836 selectors and updates. The common setup for various generic proof
837 tools enable succinct reasoning patterns. See also the Isabelle/HOL
838 tutorial \cite{isabelle-hol-book} for further instructions on using
843 subsection {* Record specifications *}
846 \begin{matharray}{rcl}
847 @{command_def (HOL) "record"} & : & @{text "theory \<rightarrow> theory"} \\
851 @@{command (HOL) record} @{syntax typespec_sorts} '=' \\
852 (@{syntax type} '+')? (@{syntax constdecl} +)
857 \item @{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1
858 \<dots> c\<^sub>n :: \<sigma>\<^sub>n"} defines extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"},
859 derived from the optional parent record @{text "\<tau>"} by adding new
860 field components @{text "c\<^sub>i :: \<sigma>\<^sub>i"} etc.
862 The type variables of @{text "\<tau>"} and @{text "\<sigma>\<^sub>i"} need to be
863 covered by the (distinct) parameters @{text "\<alpha>\<^sub>1, \<dots>,
864 \<alpha>\<^sub>m"}. Type constructor @{text t} has to be new, while @{text
865 \<tau>} needs to specify an instance of an existing record type. At
866 least one new field @{text "c\<^sub>i"} has to be specified.
867 Basically, field names need to belong to a unique record. This is
868 not a real restriction in practice, since fields are qualified by
869 the record name internally.
871 The parent record specification @{text \<tau>} is optional; if omitted
872 @{text t} becomes a root record. The hierarchy of all records
873 declared within a theory context forms a forest structure, i.e.\ a
874 set of trees starting with a root record each. There is no way to
875 merge multiple parent records!
877 For convenience, @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} is made a
878 type abbreviation for the fixed record type @{text "\<lparr>c\<^sub>1 ::
879 \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"}, likewise is @{text
880 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>) t_scheme"} made an abbreviation for
881 @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> ::
888 subsection {* Record operations *}
891 Any record definition of the form presented above produces certain
892 standard operations. Selectors and updates are provided for any
893 field, including the improper one ``@{text more}''. There are also
894 cumulative record constructor functions. To simplify the
895 presentation below, we assume for now that @{text "(\<alpha>\<^sub>1, \<dots>,
896 \<alpha>\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 ::
897 \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"}.
899 \medskip \textbf{Selectors} and \textbf{updates} are available for
900 any field (including ``@{text more}''):
902 \begin{matharray}{lll}
903 @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
904 @{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>"} \\
907 There is special syntax for application of updates: @{text "r\<lparr>x :=
908 a\<rparr>"} abbreviates term @{text "x_update a r"}. Further notation for
909 repeated updates is also available: @{text "r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z :=
910 c\<rparr>"} may be written @{text "r\<lparr>x := a, y := b, z := c\<rparr>"}. Note that
911 because of postfix notation the order of fields shown here is
912 reverse than in the actual term. Since repeated updates are just
913 function applications, fields may be freely permuted in @{text "\<lparr>x
914 := a, y := b, z := c\<rparr>"}, as far as logical equality is concerned.
915 Thus commutativity of independent updates can be proven within the
916 logic for any two fields, but not as a general theorem.
918 \medskip The \textbf{make} operation provides a cumulative record
919 constructor function:
921 \begin{matharray}{lll}
922 @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
925 \medskip We now reconsider the case of non-root records, which are
926 derived of some parent. In general, the latter may depend on
927 another parent as well, resulting in a list of \emph{ancestor
928 records}. Appending the lists of fields of all ancestors results in
929 a certain field prefix. The record package automatically takes care
930 of this by lifting operations over this context of ancestor fields.
931 Assuming that @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} has ancestor
932 fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"},
933 the above record operations will get the following types:
937 @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
938 @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow>
939 \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
940 \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
941 @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>
942 \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
946 \noindent Some further operations address the extension aspect of a
947 derived record scheme specifically: @{text "t.fields"} produces a
948 record fragment consisting of exactly the new fields introduced here
949 (the result may serve as a more part elsewhere); @{text "t.extend"}
950 takes a fixed record and adds a given more part; @{text
951 "t.truncate"} restricts a record scheme to a fixed record.
955 @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
956 @{text "t.extend"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow>
957 \<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
958 @{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>"} \\
962 \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide
967 subsection {* Derived rules and proof tools *}
970 The record package proves several results internally, declaring
971 these facts to appropriate proof tools. This enables users to
972 reason about record structures quite conveniently. Assume that
973 @{text t} is a record type as specified above.
977 \item Standard conversions for selectors or updates applied to
978 record constructor terms are made part of the default Simplifier
979 context; thus proofs by reduction of basic operations merely require
980 the @{method simp} method without further arguments. These rules
981 are available as @{text "t.simps"}, too.
983 \item Selectors applied to updated records are automatically reduced
984 by an internal simplification procedure, which is also part of the
985 standard Simplifier setup.
987 \item Inject equations of a form analogous to @{prop "(x, y) = (x',
988 y') \<equiv> x = x' \<and> y = y'"} are declared to the Simplifier and Classical
989 Reasoner as @{attribute iff} rules. These rules are available as
992 \item The introduction rule for record equality analogous to @{text
993 "x r = x r' \<Longrightarrow> y r = y r' \<dots> \<Longrightarrow> r = r'"} is declared to the Simplifier,
994 and as the basic rule context as ``@{attribute intro}@{text "?"}''.
995 The rule is called @{text "t.equality"}.
997 \item Representations of arbitrary record expressions as canonical
998 constructor terms are provided both in @{method cases} and @{method
999 induct} format (cf.\ the generic proof methods of the same name,
1000 \secref{sec:cases-induct}). Several variations are available, for
1001 fixed records, record schemes, more parts etc.
1003 The generic proof methods are sufficiently smart to pick the most
1004 sensible rule according to the type of the indicated record
1005 expression: users just need to apply something like ``@{text "(cases
1006 r)"}'' to a certain proof problem.
1008 \item The derived record operations @{text "t.make"}, @{text
1009 "t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not}
1010 treated automatically, but usually need to be expanded by hand,
1011 using the collective fact @{text "t.defs"}.
1017 subsubsection {* Examples *}
1019 text {* See @{file "~~/src/HOL/ex/Records.thy"}, for example. *}
1022 section {* Adhoc tuples *}
1025 \begin{matharray}{rcl}
1026 @{attribute_def (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\
1030 @@{attribute (HOL) split_format} ('(' 'complete' ')')?
1035 \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes
1036 arguments in function applications to be represented canonically
1037 according to their tuple type structure.
1039 Note that this operation tends to invent funny names for new local
1040 parameters introduced.
1046 section {* Typedef axiomatization \label{sec:hol-typedef} *}
1048 text {* A Gordon/HOL-style type definition is a certain axiom scheme
1049 that identifies a new type with a subset of an existing type. More
1050 precisely, the new type is defined by exhibiting an existing type
1051 @{text \<tau>}, a set @{text "A :: \<tau> set"}, and a theorem that proves
1052 @{prop "\<exists>x. x \<in> A"}. Thus @{text A} is a non-empty subset of @{text
1053 \<tau>}, and the new type denotes this subset. New functions are
1054 postulated that establish an isomorphism between the new type and
1055 the subset. In general, the type @{text \<tau>} may involve type
1056 variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} which means that the type definition
1057 produces a type constructor @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} depending on
1058 those type arguments.
1060 The axiomatization can be considered a ``definition'' in the sense
1061 of the particular set-theoretic interpretation of HOL
1062 \cite{pitts93}, where the universe of types is required to be
1063 downwards-closed wrt.\ arbitrary non-empty subsets. Thus genuinely
1064 new types introduced by @{command "typedef"} stay within the range
1065 of HOL models by construction. Note that @{command_ref
1066 type_synonym} from Isabelle/Pure merely introduces syntactic
1067 abbreviations, without any logical significance.
1069 \begin{matharray}{rcl}
1070 @{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
1074 @@{command (HOL) typedef} alt_name? abs_type '=' rep_set
1077 alt_name: '(' (@{syntax name} | @'open' | @'open' @{syntax name}) ')'
1079 abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
1081 rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
1086 \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}
1087 axiomatizes a type definition in the background theory of the
1088 current context, depending on a non-emptiness result of the set
1089 @{text A} that needs to be proven here. The set @{text A} may
1090 contain type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} as specified on the LHS,
1091 but no term variables.
1093 Even though a local theory specification, the newly introduced type
1094 constructor cannot depend on parameters or assumptions of the
1095 context: this is structurally impossible in HOL. In contrast, the
1096 non-emptiness proof may use local assumptions in unusual situations,
1097 which could result in different interpretations in target contexts:
1098 the meaning of the bijection between the representing set @{text A}
1099 and the new type @{text t} may then change in different application
1102 By default, @{command (HOL) "typedef"} defines both a type
1103 constructor @{text t} for the new type, and a term constant @{text
1104 t} for the representing set within the old type. Use the ``@{text
1105 "(open)"}'' option to suppress a separate constant definition
1106 altogether. The injection from type to set is called @{text Rep_t},
1107 its inverse @{text Abs_t}, unless explicit @{keyword (HOL)
1108 "morphisms"} specification provides alternative names.
1110 The core axiomatization uses the locale predicate @{const
1111 type_definition} as defined in Isabelle/HOL. Various basic
1112 consequences of that are instantiated accordingly, re-using the
1113 locale facts with names derived from the new type constructor. Thus
1114 the generic @{thm type_definition.Rep} is turned into the specific
1115 @{text "Rep_t"}, for example.
1117 Theorems @{thm type_definition.Rep}, @{thm
1118 type_definition.Rep_inverse}, and @{thm type_definition.Abs_inverse}
1119 provide the most basic characterization as a corresponding
1120 injection/surjection pair (in both directions). The derived rules
1121 @{thm type_definition.Rep_inject} and @{thm
1122 type_definition.Abs_inject} provide a more convenient version of
1123 injectivity, suitable for automated proof tools (e.g.\ in
1124 declarations involving @{attribute simp} or @{attribute iff}).
1125 Furthermore, the rules @{thm type_definition.Rep_cases}~/ @{thm
1126 type_definition.Rep_induct}, and @{thm type_definition.Abs_cases}~/
1127 @{thm type_definition.Abs_induct} provide alternative views on
1128 surjectivity. These rules are already declared as set or type rules
1129 for the generic @{method cases} and @{method induct} methods,
1132 An alternative name for the set definition (and other derived
1133 entities) may be specified in parentheses; the default is to use
1139 If you introduce a new type axiomatically, i.e.\ via @{command_ref
1140 typedecl} and @{command_ref axiomatization}, the minimum requirement
1141 is that it has a non-empty model, to avoid immediate collapse of the
1142 HOL logic. Moreover, one needs to demonstrate that the
1143 interpretation of such free-form axiomatizations can coexist with
1144 that of the regular @{command_def typedef} scheme, and any extension
1145 that other people might have introduced elsewhere (e.g.\ in HOLCF
1146 \cite{MuellerNvOS99}).
1150 subsubsection {* Examples *}
1152 text {* Type definitions permit the introduction of abstract data
1153 types in a safe way, namely by providing models based on already
1154 existing types. Given some abstract axiomatic description @{text P}
1155 of a type, this involves two steps:
1159 \item Find an appropriate type @{text \<tau>} and subset @{text A} which
1160 has the desired properties @{text P}, and make a type definition
1161 based on this representation.
1163 \item Prove that @{text P} holds for @{text \<tau>} by lifting @{text P}
1164 from the representation.
1168 You can later forget about the representation and work solely in
1169 terms of the abstract properties @{text P}.
1171 \medskip The following trivial example pulls a three-element type
1172 into existence within the formal logical environment of HOL. *}
1174 typedef three = "{(True, True), (True, False), (False, True)}"
1177 definition "One = Abs_three (True, True)"
1178 definition "Two = Abs_three (True, False)"
1179 definition "Three = Abs_three (False, True)"
1181 lemma three_distinct: "One \<noteq> Two" "One \<noteq> Three" "Two \<noteq> Three"
1182 by (simp_all add: One_def Two_def Three_def Abs_three_inject three_def)
1185 fixes x :: three obtains "x = One" | "x = Two" | "x = Three"
1186 by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject three_def)
1188 text {* Note that such trivial constructions are better done with
1189 derived specification mechanisms such as @{command datatype}: *}
1191 datatype three' = One' | Two' | Three'
1193 text {* This avoids re-doing basic definitions and proofs from the
1194 primitive @{command typedef} above. *}
1197 section {* Functorial structure of types *}
1200 \begin{matharray}{rcl}
1201 @{command_def (HOL) "enriched_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
1205 @@{command (HOL) enriched_type} (@{syntax name} ':')? @{syntax term}
1211 \item @{command (HOL) "enriched_type"}~@{text "prefix: m"} allows to
1212 prove and register properties about the functorial structure of type
1213 constructors. These properties then can be used by other packages
1214 to deal with those type constructors in certain type constructions.
1215 Characteristic theorems are noted in the current local theory. By
1216 default, they are prefixed with the base name of the type
1217 constructor, an explicit prefix can be given alternatively.
1219 The given term @{text "m"} is considered as \emph{mapper} for the
1220 corresponding type constructor and must conform to the following
1223 \begin{matharray}{lll}
1224 @{text "m"} & @{text "::"} &
1225 @{text "\<sigma>\<^isub>1 \<Rightarrow> \<dots> \<sigma>\<^isub>k \<Rightarrow> (\<^vec>\<alpha>\<^isub>n) t \<Rightarrow> (\<^vec>\<beta>\<^isub>n) t"} \\
1228 \noindent where @{text t} is the type constructor, @{text
1229 "\<^vec>\<alpha>\<^isub>n"} and @{text "\<^vec>\<beta>\<^isub>n"} are distinct
1230 type variables free in the local theory and @{text "\<sigma>\<^isub>1"},
1231 \ldots, @{text "\<sigma>\<^isub>k"} is a subsequence of @{text "\<alpha>\<^isub>1 \<Rightarrow>
1232 \<beta>\<^isub>1"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<alpha>\<^isub>1"}, \ldots,
1233 @{text "\<alpha>\<^isub>n \<Rightarrow> \<beta>\<^isub>n"}, @{text "\<beta>\<^isub>n \<Rightarrow>
1234 \<alpha>\<^isub>n"}.
1239 section {* Quotient types *}
1242 The quotient package defines a new quotient type given a raw type
1243 and a partial equivalence relation.
1244 It also includes automation for transporting definitions and theorems.
1245 It can automatically produce definitions and theorems on the quotient type,
1246 given the corresponding constants and facts on the raw type.
1248 \begin{matharray}{rcl}
1249 @{command_def (HOL) "quotient_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
1250 @{command_def (HOL) "quotient_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
1251 @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
1252 @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
1253 @{command_def (HOL) "print_quotconsts"} & : & @{text "context \<rightarrow>"}\\
1257 @@{command (HOL) quotient_type} (spec + @'and');
1259 spec: @{syntax typespec} @{syntax mixfix}? '=' \\
1260 @{syntax type} '/' ('partial' ':')? @{syntax term};
1264 @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \\
1265 @{syntax term} 'is' @{syntax term};
1267 constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
1272 \item @{command (HOL) "quotient_type"} defines quotient types.
1274 \item @{command (HOL) "quotient_definition"} defines a constant on the quotient type.
1276 \item @{command (HOL) "print_quotmaps"} prints quotient map functions.
1278 \item @{command (HOL) "print_quotients"} prints quotients.
1280 \item @{command (HOL) "print_quotconsts"} prints quotient constants.
1286 section {* Arithmetic proof support *}
1289 \begin{matharray}{rcl}
1290 @{method_def (HOL) arith} & : & @{text method} \\
1291 @{attribute_def (HOL) arith} & : & @{text attribute} \\
1292 @{attribute_def (HOL) arith_split} & : & @{text attribute} \\
1295 The @{method (HOL) arith} method decides linear arithmetic problems
1296 (on types @{text nat}, @{text int}, @{text real}). Any current
1297 facts are inserted into the goal before running the procedure.
1299 The @{attribute (HOL) arith} attribute declares facts that are
1300 always supplied to the arithmetic provers implicitly.
1302 The @{attribute (HOL) arith_split} attribute declares case split
1303 rules to be expanded before @{method (HOL) arith} is invoked.
1305 Note that a simpler (but faster) arithmetic prover is
1306 already invoked by the Simplifier.
1310 section {* Intuitionistic proof search *}
1313 \begin{matharray}{rcl}
1314 @{method_def (HOL) iprover} & : & @{text method} \\
1318 @@{method (HOL) iprover} ( @{syntax rulemod} * )
1321 The @{method (HOL) iprover} method performs intuitionistic proof
1322 search, depending on specifically declared rules from the context,
1323 or given as explicit arguments. Chained facts are inserted into the
1324 goal before commencing proof search.
1326 Rules need to be classified as @{attribute (Pure) intro},
1327 @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
1328 ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
1329 applied aggressively (without considering back-tracking later).
1330 Rules declared with ``@{text "?"}'' are ignored in proof search (the
1331 single-step @{method (Pure) rule} method still observes these). An
1332 explicit weight annotation may be given as well; otherwise the
1333 number of rule premises will be taken into account here.
1336 section {* Model Elimination and Resolution *}
1339 \begin{matharray}{rcl}
1340 @{method_def (HOL) "meson"} & : & @{text method} \\
1341 @{method_def (HOL) "metis"} & : & @{text method} \\
1345 @@{method (HOL) meson} @{syntax thmrefs}?
1348 @@{method (HOL) metis} ( '(' ('partial_types' | 'full_types' | 'no_types'
1349 | @{syntax name}) ')' )? @{syntax thmrefs}?
1352 The @{method (HOL) meson} method implements Loveland's model elimination
1353 procedure \cite{loveland-78}. See @{file "~~/src/HOL/ex/Meson_Test.thy"} for
1356 The @{method (HOL) metis} method combines ordered resolution and ordered
1357 paramodulation to find first-order (or mildly higher-order) proofs. The first
1358 optional argument specifies a type encoding; see the Sledgehammer manual
1359 \cite{isabelle-sledgehammer} for details. The @{file
1360 "~~/src/HOL/Metis_Examples"} directory contains several small theories
1361 developed to a large extent using Metis.
1364 section {* Coherent Logic *}
1367 \begin{matharray}{rcl}
1368 @{method_def (HOL) "coherent"} & : & @{text method} \\
1372 @@{method (HOL) coherent} @{syntax thmrefs}?
1375 The @{method (HOL) coherent} method solves problems of
1376 \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
1377 applications in confluence theory, lattice theory and projective
1378 geometry. See @{file "~~/src/HOL/ex/Coherent.thy"} for some
1383 section {* Proving propositions *}
1386 In addition to the standard proof methods, a number of diagnosis
1387 tools search for proofs and provide an Isar proof snippet on success.
1388 These tools are available via the following commands.
1390 \begin{matharray}{rcl}
1391 @{command_def (HOL) "solve_direct"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1392 @{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1393 @{command_def (HOL) "try_methods"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1394 @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1395 @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \<rightarrow> theory"}
1399 @@{command (HOL) try}
1402 @@{command (HOL) try_methods} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
1406 @@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?
1409 @@{command (HOL) sledgehammer_params} ( ( '[' args ']' ) ? )
1412 args: ( @{syntax name} '=' value + ',' )
1415 facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'
1417 "} % FIXME check args "value"
1421 \item @{command (HOL) "solve_direct"} checks whether the current subgoals can
1422 be solved directly by an existing theorem. Duplicate lemmas can be detected
1425 \item @{command (HOL) "try_methods"} attempts to prove a subgoal using a combination
1426 of standard proof methods (@{text auto}, @{text simp}, @{text blast}, etc.).
1427 Additional facts supplied via @{text "simp:"}, @{text "intro:"},
1428 @{text "elim:"}, and @{text "dest:"} are passed to the appropriate proof
1431 \item @{command (HOL) "try"} attempts to prove or disprove a subgoal
1432 using a combination of provers and disprovers (@{text "solve_direct"},
1433 @{text "quickcheck"}, @{text "try_methods"}, @{text "sledgehammer"},
1436 \item @{command (HOL) "sledgehammer"} attempts to prove a subgoal using external
1437 automatic provers (resolution provers and SMT solvers). See the Sledgehammer
1438 manual \cite{isabelle-sledgehammer} for details.
1440 \item @{command (HOL) "sledgehammer_params"} changes
1441 @{command (HOL) "sledgehammer"} configuration options persistently.
1447 section {* Checking and refuting propositions *}
1450 Identifying incorrect propositions usually involves evaluation of
1451 particular assignments and systematic counterexample search. This
1452 is supported by the following commands.
1454 \begin{matharray}{rcl}
1455 @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1456 @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1457 @{command_def (HOL) "refute"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1458 @{command_def (HOL) "nitpick"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1459 @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"} \\
1460 @{command_def (HOL) "refute_params"} & : & @{text "theory \<rightarrow> theory"} \\
1461 @{command_def (HOL) "nitpick_params"} & : & @{text "theory \<rightarrow> theory"}
1465 @@{command (HOL) value} ( '[' name ']' )? modes? @{syntax term}
1468 (@@{command (HOL) quickcheck} | @@{command (HOL) refute} | @@{command (HOL) nitpick})
1469 ( '[' args ']' )? @{syntax nat}?
1472 (@@{command (HOL) quickcheck_params} | @@{command (HOL) refute_params} |
1473 @@{command (HOL) nitpick_params}) ( '[' args ']' )?
1476 modes: '(' (@{syntax name} +) ')'
1479 args: ( @{syntax name} '=' value + ',' )
1481 "} % FIXME check "value"
1485 \item @{command (HOL) "value"}~@{text t} evaluates and prints a
1486 term; optionally @{text modes} can be specified, which are
1487 appended to the current print mode; see \secref{sec:print-modes}.
1488 Internally, the evaluation is performed by registered evaluators,
1489 which are invoked sequentially until a result is returned.
1490 Alternatively a specific evaluator can be selected using square
1491 brackets; typical evaluators use the current set of code equations
1492 to normalize and include @{text simp} for fully symbolic
1493 evaluation using the simplifier, @{text nbe} for
1494 \emph{normalization by evaluation} and \emph{code} for code
1497 \item @{command (HOL) "quickcheck"} tests the current goal for
1498 counterexamples using a series of assignments for its
1499 free variables; by default the first subgoal is tested, an other
1500 can be selected explicitly using an optional goal index.
1501 Assignments can be chosen exhausting the search space upto a given
1502 size, or using a fixed number of random assignments in the search space,
1503 or exploring the search space symbolically using narrowing.
1504 By default, quickcheck uses exhaustive testing.
1505 A number of configuration options are supported for
1506 @{command (HOL) "quickcheck"}, notably:
1510 \item[@{text tester}] specifies which testing approach to apply.
1511 There are three testers, @{text exhaustive},
1512 @{text random}, and @{text narrowing}.
1513 An unknown configuration option is treated as an argument to tester,
1514 making @{text "tester ="} optional.
1515 When multiple testers are given, these are applied in parallel.
1516 If no tester is specified, quickcheck uses the testers that are
1517 set active, i.e., configurations
1518 @{text quickcheck_exhaustive_active}, @{text quickcheck_random_active},
1519 @{text quickcheck_narrowing_active} are set to true.
1520 \item[@{text size}] specifies the maximum size of the search space
1521 for assignment values.
1523 \item[@{text eval}] takes a term or a list of terms and evaluates
1524 these terms under the variable assignment found by quickcheck.
1526 \item[@{text iterations}] sets how many sets of assignments are
1527 generated for each particular size.
1529 \item[@{text no_assms}] specifies whether assumptions in
1530 structured proofs should be ignored.
1532 \item[@{text timeout}] sets the time limit in seconds.
1534 \item[@{text default_type}] sets the type(s) generally used to
1535 instantiate type variables.
1537 \item[@{text report}] if set quickcheck reports how many tests
1538 fulfilled the preconditions.
1540 \item[@{text quiet}] if not set quickcheck informs about the
1541 current size for assignment values.
1543 \item[@{text expect}] can be used to check if the user's
1544 expectation was met (@{text no_expectation}, @{text
1545 no_counterexample}, or @{text counterexample}).
1549 These option can be given within square brackets.
1551 \item @{command (HOL) "quickcheck_params"} changes
1552 @{command (HOL) "quickcheck"} configuration options persistently.
1554 \item @{command (HOL) "refute"} tests the current goal for
1555 counterexamples using a reduction to SAT. The following configuration
1556 options are supported:
1560 \item[@{text minsize}] specifies the minimum size (cardinality) of the
1561 models to search for.
1563 \item[@{text maxsize}] specifies the maximum size (cardinality) of the
1564 models to search for. Nonpositive values mean $\infty$.
1566 \item[@{text maxvars}] specifies the maximum number of Boolean variables
1567 to use when transforming the term into a propositional formula.
1568 Nonpositive values mean $\infty$.
1570 \item[@{text satsolver}] specifies the SAT solver to use.
1572 \item[@{text no_assms}] specifies whether assumptions in
1573 structured proofs should be ignored.
1575 \item[@{text maxtime}] sets the time limit in seconds.
1577 \item[@{text expect}] can be used to check if the user's
1578 expectation was met (@{text genuine}, @{text potential},
1579 @{text none}, or @{text unknown}).
1583 These option can be given within square brackets.
1585 \item @{command (HOL) "refute_params"} changes
1586 @{command (HOL) "refute"} configuration options persistently.
1588 \item @{command (HOL) "nitpick"} tests the current goal for counterexamples
1589 using a reduction to first-order relational logic. See the Nitpick manual
1590 \cite{isabelle-nitpick} for details.
1592 \item @{command (HOL) "nitpick_params"} changes
1593 @{command (HOL) "nitpick"} configuration options persistently.
1599 section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *}
1602 The following tools of Isabelle/HOL support cases analysis and
1603 induction in unstructured tactic scripts; see also
1604 \secref{sec:cases-induct} for proper Isar versions of similar ideas.
1606 \begin{matharray}{rcl}
1607 @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & @{text method} \\
1608 @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\
1609 @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\
1610 @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1614 @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?
1616 @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
1618 @@{method (HOL) ind_cases} (@{syntax prop}+) (@'for' (@{syntax name}+))?
1620 @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
1623 rule: 'rule' ':' @{syntax thmref}
1628 \item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit
1629 to reason about inductive types. Rules are selected according to
1630 the declarations by the @{attribute cases} and @{attribute induct}
1631 attributes, cf.\ \secref{sec:cases-induct}. The @{command (HOL)
1632 datatype} package already takes care of this.
1634 These unstructured tactics feature both goal addressing and dynamic
1635 instantiation. Note that named rule cases are \emph{not} provided
1636 as would be by the proper @{method cases} and @{method induct} proof
1637 methods (see \secref{sec:cases-induct}). Unlike the @{method
1638 induct} method, @{method induct_tac} does not handle structured rule
1639 statements, only the compact object-logic conclusion of the subgoal
1642 \item @{method (HOL) ind_cases} and @{command (HOL)
1643 "inductive_cases"} provide an interface to the internal @{ML_text
1644 mk_cases} operation. Rules are simplified in an unrestricted
1647 While @{method (HOL) ind_cases} is a proof method to apply the
1648 result immediately as elimination rules, @{command (HOL)
1649 "inductive_cases"} provides case split theorems at the theory level
1650 for later use. The @{keyword "for"} argument of the @{method (HOL)
1651 ind_cases} method allows to specify a list of variables that should
1652 be generalized before applying the resulting rule.
1658 section {* Executable code *}
1660 text {* For validation purposes, it is often useful to \emph{execute}
1661 specifications. In principle, execution could be simulated by
1662 Isabelle's inference kernel, i.e. by a combination of resolution and
1663 simplification. Unfortunately, this approach is rather inefficient.
1664 A more efficient way of executing specifications is to translate
1665 them into a functional programming language such as ML.
1667 Isabelle provides two generic frameworks to support code generation
1668 from executable specifications. Isabelle/HOL instantiates these
1669 mechanisms in a way that is amenable to end-user applications.
1673 subsection {* The new code generator (F. Haftmann) *}
1675 text {* This framework generates code from functional programs
1676 (including overloading using type classes) to SML \cite{SML}, OCaml
1677 \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
1678 \cite{scala-overview-tech-report}. Conceptually, code generation is
1679 split up in three steps: \emph{selection} of code theorems,
1680 \emph{translation} into an abstract executable view and
1681 \emph{serialization} to a specific \emph{target language}.
1682 Inductive specifications can be executed using the predicate
1683 compiler which operates within HOL. See \cite{isabelle-codegen} for
1686 \begin{matharray}{rcl}
1687 @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1688 @{attribute_def (HOL) code} & : & @{text attribute} \\
1689 @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
1690 @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
1691 @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1692 @{attribute_def (HOL) code_inline} & : & @{text attribute} \\
1693 @{attribute_def (HOL) code_post} & : & @{text attribute} \\
1694 @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1695 @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1696 @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1697 @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
1698 @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
1699 @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
1700 @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
1701 @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
1702 @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
1703 @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
1704 @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
1705 @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"}
1709 @@{command (HOL) export_code} ( constexpr + ) \\
1710 ( ( @'in' target ( @'module_name' @{syntax string} ) ? \\
1711 ( @'file' ( @{syntax string} | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
1714 const: @{syntax term}
1717 constexpr: ( const | 'name._' | '_' )
1720 typeconstructor: @{syntax nameref}
1723 class: @{syntax nameref}
1726 target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
1729 @@{attribute (HOL) code} ( 'del' | 'abstype' | 'abstract' )?
1732 @@{command (HOL) code_abort} ( const + )
1735 @@{command (HOL) code_datatype} ( const + )
1738 @@{attribute (HOL) code_inline} ( 'del' ) ?
1741 @@{attribute (HOL) code_post} ( 'del' ) ?
1744 @@{command (HOL) code_thms} ( constexpr + ) ?
1747 @@{command (HOL) code_deps} ( constexpr + ) ?
1750 @@{command (HOL) code_const} (const + @'and') \\
1751 ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
1754 @@{command (HOL) code_type} (typeconstructor + @'and') \\
1755 ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
1758 @@{command (HOL) code_class} (class + @'and') \\
1759 ( ( '(' target \\ ( @{syntax string} ? + @'and' ) ')' ) + )
1762 @@{command (HOL) code_instance} (( typeconstructor '::' class ) + @'and') \\
1763 ( ( '(' target ( '-' ? + @'and' ) ')' ) + )
1766 @@{command (HOL) code_reserved} target ( @{syntax string} + )
1769 @@{command (HOL) code_monad} const const target
1772 @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
1775 @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )
1778 @@{command (HOL) code_reflect} @{syntax string} \\
1779 ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \\
1780 ( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?
1783 syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
1788 \item @{command (HOL) "export_code"} generates code for a given list
1789 of constants in the specified target language(s). If no
1790 serialization instruction is given, only abstract code is generated
1793 Constants may be specified by giving them literally, referring to
1794 all executable contants within a certain theory by giving @{text
1795 "name.*"}, or referring to \emph{all} executable constants currently
1796 available by giving @{text "*"}.
1798 By default, for each involved theory one corresponding name space
1799 module is generated. Alternativly, a module name may be specified
1800 after the @{keyword "module_name"} keyword; then \emph{all} code is
1801 placed in this module.
1803 For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
1804 refers to a single file; for \emph{Haskell}, it refers to a whole
1805 directory, where code is generated in multiple files reflecting the
1806 module hierarchy. Omitting the file specification denotes standard
1809 Serializers take an optional list of arguments in parentheses. For
1810 \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
1811 explicit module signatures.
1813 For \emph{Haskell} a module name prefix may be given using the
1814 ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
1815 ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
1816 datatype declaration.
1818 \item @{attribute (HOL) code} explicitly selects (or with option
1819 ``@{text "del"}'' deselects) a code equation for code generation.
1820 Usually packages introducing code equations provide a reasonable
1821 default setup for selection. Variants @{text "code abstype"} and
1822 @{text "code abstract"} declare abstract datatype certificates or
1823 code equations on abstract datatype representations respectively.
1825 \item @{command (HOL) "code_abort"} declares constants which are not
1826 required to have a definition by means of code equations; if needed
1827 these are implemented by program abort instead.
1829 \item @{command (HOL) "code_datatype"} specifies a constructor set
1832 \item @{command (HOL) "print_codesetup"} gives an overview on
1833 selected code equations and code generator datatypes.
1835 \item @{attribute (HOL) code_inline} declares (or with option
1836 ``@{text "del"}'' removes) inlining theorems which are applied as
1837 rewrite rules to any code equation during preprocessing.
1839 \item @{attribute (HOL) code_post} declares (or with option ``@{text
1840 "del"}'' removes) theorems which are applied as rewrite rules to any
1841 result of an evaluation.
1843 \item @{command (HOL) "print_codeproc"} prints the setup of the code
1844 generator preprocessor.
1846 \item @{command (HOL) "code_thms"} prints a list of theorems
1847 representing the corresponding program containing all given
1848 constants after preprocessing.
1850 \item @{command (HOL) "code_deps"} visualizes dependencies of
1851 theorems representing the corresponding program containing all given
1852 constants after preprocessing.
1854 \item @{command (HOL) "code_const"} associates a list of constants
1855 with target-specific serializations; omitting a serialization
1856 deletes an existing serialization.
1858 \item @{command (HOL) "code_type"} associates a list of type
1859 constructors with target-specific serializations; omitting a
1860 serialization deletes an existing serialization.
1862 \item @{command (HOL) "code_class"} associates a list of classes
1863 with target-specific class names; omitting a serialization deletes
1864 an existing serialization. This applies only to \emph{Haskell}.
1866 \item @{command (HOL) "code_instance"} declares a list of type
1867 constructor / class instance relations as ``already present'' for a
1868 given target. Omitting a ``@{text "-"}'' deletes an existing
1869 ``already present'' declaration. This applies only to
1872 \item @{command (HOL) "code_reserved"} declares a list of names as
1873 reserved for a given target, preventing it to be shadowed by any
1876 \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
1877 to generate monadic code for Haskell.
1879 \item @{command (HOL) "code_include"} adds arbitrary named content
1880 (``include'') to generated code. A ``@{text "-"}'' as last argument
1881 will remove an already added ``include''.
1883 \item @{command (HOL) "code_modulename"} declares aliasings from one
1884 module name onto another.
1886 \item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
1887 argument compiles code into the system runtime environment and
1888 modifies the code generator setup that future invocations of system
1889 runtime code generation referring to one of the ``@{text
1890 "datatypes"}'' or ``@{text "functions"}'' entities use these precompiled
1891 entities. With a ``@{text "file"}'' argument, the corresponding code
1892 is generated into that specified file without modifying the code
1899 subsection {* The old code generator (S. Berghofer) *}
1901 text {* This framework generates code from both functional and
1902 relational programs to SML, as explained below.
1904 \begin{matharray}{rcl}
1905 @{command_def "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
1906 @{command_def "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
1907 @{command_def "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
1908 @{command_def "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
1909 @{attribute_def code} & : & @{text attribute} \\
1913 ( @@{command code_module} | @@{command code_library} ) modespec? @{syntax name}? \\
1914 ( @'file' name ) ? ( @'imports' ( @{syntax name} + ) ) ? \\
1915 @'contains' ( ( @{syntax name} '=' @{syntax term} ) + | @{syntax term} + )
1918 modespec: '(' ( @{syntax name} * ) ')'
1921 @@{command (HOL) consts_code} (codespec +)
1924 codespec: const template attachment ?
1927 @@{command (HOL) types_code} (tycodespec +)
1930 tycodespec: @{syntax name} template attachment ?
1933 const: @{syntax term}
1936 template: '(' @{syntax string} ')'
1939 attachment: 'attach' modespec? '{' @{syntax text} '}'
1942 @@{attribute code} name?
1947 subsubsection {* Invoking the code generator *}
1949 text {* The code generator is invoked via the @{command code_module}
1950 and @{command code_library} commands, which correspond to
1951 \emph{incremental} and \emph{modular} code generation, respectively.
1955 \item [Modular] For each theory, an ML structure is generated,
1956 containing the code generated from the constants defined in this
1959 \item [Incremental] All the generated code is emitted into the same
1960 structure. This structure may import code from previously generated
1961 structures, which can be specified via @{keyword "imports"}.
1962 Moreover, the generated structure may also be referred to in later
1963 invocations of the code generator.
1967 After the @{command code_module} and @{command code_library}
1968 keywords, the user may specify an optional list of ``modes'' in
1969 parentheses. These can be used to instruct the code generator to
1970 emit additional code for special purposes, e.g.\ functions for
1971 converting elements of generated datatypes to Isabelle terms, or
1972 test data generators. The list of modes is followed by a module
1973 name. The module name is optional for modular code generation, but
1974 must be specified for incremental code generation.
1976 The code can either be written to a file, in which case a file name
1977 has to be specified after the @{keyword "file"} keyword, or be loaded
1978 directly into Isabelle's ML environment. In the latter case, the
1979 @{command ML} theory command can be used to inspect the results
1980 interactively, for example.
1982 The terms from which to generate code can be specified after the
1983 @{keyword "contains"} keyword, either as a list of bindings, or just
1984 as a list of terms. In the latter case, the code generator just
1985 produces code for all constants and types occuring in the term, but
1986 does not bind the compiled terms to ML identifiers.
1992 contains test = "foldl op + (0 :: int) [1, 2, 3, 4, 5]"
1994 text {* \noindent This binds the result of compiling the given term to
1995 the ML identifier @{ML Test.test}. *}
1997 ML {* @{assert} (Test.test = 15) *}
2000 subsubsection {* Configuring the code generator *}
2002 text {* When generating code for a complex term, the code generator
2003 recursively calls itself for all subterms. When it arrives at a
2004 constant, the default strategy of the code generator is to look up
2005 its definition and try to generate code for it. Constants which
2006 have no definitions that are immediately executable, may be
2007 associated with a piece of ML code manually using the @{command_ref
2008 consts_code} command. It takes a list whose elements consist of a
2009 constant (given in usual term syntax -- an explicit type constraint
2010 accounts for overloading), and a mixfix template describing the ML
2011 code. The latter is very much the same as the mixfix templates used
2012 when declaring new constants. The most notable difference is that
2013 terms may be included in the ML template using antiquotation
2014 brackets @{verbatim "{"}@{verbatim "*"}~@{text "..."}~@{verbatim
2015 "*"}@{verbatim "}"}.
2017 A similar mechanism is available for types: @{command_ref
2018 types_code} associates type constructors with specific ML code.
2020 For example, the following declarations copied from @{file
2021 "~~/src/HOL/Product_Type.thy"} describe how the product type of
2022 Isabelle/HOL should be compiled to ML. *}
2024 typedecl ('a, 'b) prod
2025 consts Pair :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) prod"
2027 types_code prod ("(_ */ _)")
2028 consts_code Pair ("(_,/ _)")
2030 text {* Sometimes, the code associated with a constant or type may
2031 need to refer to auxiliary functions, which have to be emitted when
2032 the constant is used. Code for such auxiliary functions can be
2033 declared using @{keyword "attach"}. For example, the @{const wfrec}
2034 function can be implemented as follows:
2037 consts_code wfrec ("\<module>wfrec?") (* FIXME !? *)
2038 attach {* fun wfrec f x = f (wfrec f) x *}
2040 text {* If the code containing a call to @{const wfrec} resides in an
2041 ML structure different from the one containing the function
2042 definition attached to @{const wfrec}, the name of the ML structure
2043 (followed by a ``@{text "."}'') is inserted in place of ``@{text
2044 "\<module>"}'' in the above template. The ``@{text "?"}'' means that
2045 the code generator should ignore the first argument of @{const
2046 wfrec}, i.e.\ the termination relation, which is usually not
2049 \medskip Another possibility of configuring the code generator is to
2050 register theorems to be used for code generation. Theorems can be
2051 registered via the @{attribute code} attribute. It takes an optional
2052 name as an argument, which indicates the format of the
2053 theorem. Currently supported formats are equations (this is the
2054 default when no name is specified) and horn clauses (this is
2055 indicated by the name \texttt{ind}). The left-hand sides of
2056 equations may only contain constructors and distinct variables,
2057 whereas horn clauses must have the same format as introduction rules
2058 of inductive definitions.
2060 The following example specifies three equations from which to
2061 generate code for @{term "op <"} on natural numbers (see also
2062 @{"file" "~~/src/HOL/Nat.thy"}). *}
2064 lemma [code]: "(Suc m < Suc n) = (m < n)"
2065 and [code]: "((n::nat) < 0) = False"
2066 and [code]: "(0 < Suc n) = True" by simp_all
2069 subsubsection {* Specific HOL code generators *}
2071 text {* The basic code generator framework offered by Isabelle/Pure
2072 has already been extended with additional code generators for
2073 specific HOL constructs. These include datatypes, recursive
2074 functions and inductive relations. The code generator for inductive
2075 relations can handle expressions of the form @{text "(t\<^sub>1, \<dots>, t\<^sub>n) \<in>
2076 r"}, where @{text "r"} is an inductively defined relation. If at
2077 least one of the @{text "t\<^sub>i"} is a dummy pattern ``@{text "_"}'',
2078 the above expression evaluates to a sequence of possible answers. If
2079 all of the @{text "t\<^sub>i"} are proper terms, the expression evaluates
2082 The following example demonstrates this for beta-reduction on lambda
2083 terms (see also @{"file" "~~/src/HOL/Proofs/Lambda/Lambda.thy"}).
2088 | App dB dB (infixl "\<degree>" 200)
2091 primrec lift :: "dB \<Rightarrow> nat \<Rightarrow> dB"
2093 "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
2094 | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
2095 | "lift (Abs s) k = Abs (lift s (k + 1))"
2097 primrec subst :: "dB \<Rightarrow> dB \<Rightarrow> nat \<Rightarrow> dB" ("_[_'/_]" [300, 0, 0] 300)
2100 (if k < i then Var (i - 1) else if i = k then s else Var i)"
2101 | "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
2102 | "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
2104 inductive beta :: "dB \<Rightarrow> dB \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
2106 beta: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
2107 | appL: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
2108 | appR: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
2109 | abs: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
2113 test1 = "Abs (Var 0) \<degree> Var 0 \<rightarrow>\<^sub>\<beta> Var 0"
2114 test2 = "Abs (Abs (Var 0 \<degree> Var 0) \<degree> (Abs (Var 0) \<degree> Var 0)) \<rightarrow>\<^sub>\<beta> _"
2117 In the above example, @{ML Test.test1} evaluates to a boolean,
2118 whereas @{ML Test.test2} is a lazy sequence whose elements can be
2119 inspected separately.
2122 ML {* @{assert} Test.test1 *}
2123 ML {* val results = DSeq.list_of Test.test2 *}
2124 ML {* @{assert} (length results = 2) *}
2127 \medskip The theory underlying the HOL code generator is described
2128 more detailed in \cite{Berghofer-Nipkow:2002}. More examples that
2129 illustrate the usage of the code generator can be found e.g.\ in
2130 @{"file" "~~/src/HOL/MicroJava/J/JListExample.thy"} and @{"file"
2131 "~~/src/HOL/MicroJava/JVM/JVMListExample.thy"}.
2135 section {* Definition by specification \label{sec:hol-specification} *}
2138 \begin{matharray}{rcl}
2139 @{command_def (HOL) "specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
2140 @{command_def (HOL) "ax_specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
2144 (@@{command (HOL) specification} | @@{command (HOL) ax_specification})
2145 '(' (decl +) ')' \\ (@{syntax thmdecl}? @{syntax prop} +)
2147 decl: ((@{syntax name} ':')? @{syntax term} '(' @'overloaded' ')'?)
2152 \item @{command (HOL) "specification"}~@{text "decls \<phi>"} sets up a
2153 goal stating the existence of terms with the properties specified to
2154 hold for the constants given in @{text decls}. After finishing the
2155 proof, the theory will be augmented with definitions for the given
2156 constants, as well as with theorems stating the properties for these
2159 \item @{command (HOL) "ax_specification"}~@{text "decls \<phi>"} sets up
2160 a goal stating the existence of terms with the properties specified
2161 to hold for the constants given in @{text decls}. After finishing
2162 the proof, the theory will be augmented with axioms expressing the
2163 properties given in the first place.
2165 \item @{text decl} declares a constant to be defined by the
2166 specification given. The definition for the constant @{text c} is
2167 bound to the name @{text c_def} unless a theorem name is given in
2168 the declaration. Overloaded constants should be declared as such.
2172 Whether to use @{command (HOL) "specification"} or @{command (HOL)
2173 "ax_specification"} is to some extent a matter of style. @{command
2174 (HOL) "specification"} introduces no new axioms, and so by
2175 construction cannot introduce inconsistencies, whereas @{command
2176 (HOL) "ax_specification"} does introduce axioms, but only after the
2177 user has explicitly proven it to be safe. A practical issue must be
2178 considered, though: After introducing two constants with the same
2179 properties using @{command (HOL) "specification"}, one can prove
2180 that the two constants are, in fact, equal. If this might be a
2181 problem, one should use @{command (HOL) "ax_specification"}.