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 {* Coercive subtyping *}
1289 \begin{matharray}{rcl}
1290 @{attribute_def (HOL) coercion} & : & @{text attribute} \\
1291 @{attribute_def (HOL) coercion_enabled} & : & @{text attribute} \\
1292 @{attribute_def (HOL) coercion_map} & : & @{text attribute} \\
1296 @@{attribute (HOL) coercion} (@{syntax term})?
1300 @@{attribute (HOL) coercion_map} (@{syntax term})?
1304 Coercive subtyping allows the user to omit explicit type conversions,
1305 also called \emph{coercions}. Type inference will add them as
1306 necessary when parsing a term. See
1307 \cite{traytel-berghofer-nipkow-2011} for details.
1311 \item @{attribute (HOL) "coercion"}~@{text "f"} registers a new
1312 coercion function @{text "f :: \<sigma>\<^isub>1 \<Rightarrow>
1313 \<sigma>\<^isub>2"} where @{text "\<sigma>\<^isub>1"} and @{text
1314 "\<sigma>\<^isub>2"} are nullary type constructors. Coercions are
1315 composed by the inference algorithm if needed. Note that the type
1316 inference algorithm is complete only if the registered coercions form
1320 \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a new
1321 map function to lift coercions through type constructors. The function
1322 @{text "map"} must conform to the following type pattern
1324 \begin{matharray}{lll}
1325 @{text "map"} & @{text "::"} &
1326 @{text "f\<^isub>1 \<Rightarrow> \<dots> \<Rightarrow> f\<^isub>n \<Rightarrow> (\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n) t \<Rightarrow> (\<beta>\<^isub>1, \<dots>, \<beta>\<^isub>n) t"} \\
1329 where @{text "t"} is a type constructor and @{text "f\<^isub>i"} is of
1330 type @{text "\<alpha>\<^isub>i \<Rightarrow> \<beta>\<^isub>i"} or
1331 @{text "\<beta>\<^isub>i \<Rightarrow> \<alpha>\<^isub>i"}.
1332 Registering a map function overwrites any existing map function for
1333 this particular type constructor.
1336 \item @{attribute (HOL) "coercion_enabled"} enables the coercion
1337 inference algorithm.
1343 section {* Arithmetic proof support *}
1346 \begin{matharray}{rcl}
1347 @{method_def (HOL) arith} & : & @{text method} \\
1348 @{attribute_def (HOL) arith} & : & @{text attribute} \\
1349 @{attribute_def (HOL) arith_split} & : & @{text attribute} \\
1352 The @{method (HOL) arith} method decides linear arithmetic problems
1353 (on types @{text nat}, @{text int}, @{text real}). Any current
1354 facts are inserted into the goal before running the procedure.
1356 The @{attribute (HOL) arith} attribute declares facts that are
1357 always supplied to the arithmetic provers implicitly.
1359 The @{attribute (HOL) arith_split} attribute declares case split
1360 rules to be expanded before @{method (HOL) arith} is invoked.
1362 Note that a simpler (but faster) arithmetic prover is
1363 already invoked by the Simplifier.
1367 section {* Intuitionistic proof search *}
1370 \begin{matharray}{rcl}
1371 @{method_def (HOL) iprover} & : & @{text method} \\
1375 @@{method (HOL) iprover} ( @{syntax rulemod} * )
1378 The @{method (HOL) iprover} method performs intuitionistic proof
1379 search, depending on specifically declared rules from the context,
1380 or given as explicit arguments. Chained facts are inserted into the
1381 goal before commencing proof search.
1383 Rules need to be classified as @{attribute (Pure) intro},
1384 @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
1385 ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
1386 applied aggressively (without considering back-tracking later).
1387 Rules declared with ``@{text "?"}'' are ignored in proof search (the
1388 single-step @{method (Pure) rule} method still observes these). An
1389 explicit weight annotation may be given as well; otherwise the
1390 number of rule premises will be taken into account here.
1393 section {* Model Elimination and Resolution *}
1396 \begin{matharray}{rcl}
1397 @{method_def (HOL) "meson"} & : & @{text method} \\
1398 @{method_def (HOL) "metis"} & : & @{text method} \\
1402 @@{method (HOL) meson} @{syntax thmrefs}?
1405 @@{method (HOL) metis} ( '(' ('partial_types' | 'full_types' | 'no_types'
1406 | @{syntax name}) ')' )? @{syntax thmrefs}?
1409 The @{method (HOL) meson} method implements Loveland's model elimination
1410 procedure \cite{loveland-78}. See @{file "~~/src/HOL/ex/Meson_Test.thy"} for
1413 The @{method (HOL) metis} method combines ordered resolution and ordered
1414 paramodulation to find first-order (or mildly higher-order) proofs. The first
1415 optional argument specifies a type encoding; see the Sledgehammer manual
1416 \cite{isabelle-sledgehammer} for details. The @{file
1417 "~~/src/HOL/Metis_Examples"} directory contains several small theories
1418 developed to a large extent using Metis.
1421 section {* Coherent Logic *}
1424 \begin{matharray}{rcl}
1425 @{method_def (HOL) "coherent"} & : & @{text method} \\
1429 @@{method (HOL) coherent} @{syntax thmrefs}?
1432 The @{method (HOL) coherent} method solves problems of
1433 \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
1434 applications in confluence theory, lattice theory and projective
1435 geometry. See @{file "~~/src/HOL/ex/Coherent.thy"} for some
1440 section {* Proving propositions *}
1443 In addition to the standard proof methods, a number of diagnosis
1444 tools search for proofs and provide an Isar proof snippet on success.
1445 These tools are available via the following commands.
1447 \begin{matharray}{rcl}
1448 @{command_def (HOL) "solve_direct"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1449 @{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1450 @{command_def (HOL) "try_methods"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1451 @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1452 @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \<rightarrow> theory"}
1456 @@{command (HOL) try}
1459 @@{command (HOL) try_methods} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
1463 @@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?
1466 @@{command (HOL) sledgehammer_params} ( ( '[' args ']' ) ? )
1469 args: ( @{syntax name} '=' value + ',' )
1472 facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'
1474 "} % FIXME check args "value"
1478 \item @{command (HOL) "solve_direct"} checks whether the current subgoals can
1479 be solved directly by an existing theorem. Duplicate lemmas can be detected
1482 \item @{command (HOL) "try_methods"} attempts to prove a subgoal using a combination
1483 of standard proof methods (@{text auto}, @{text simp}, @{text blast}, etc.).
1484 Additional facts supplied via @{text "simp:"}, @{text "intro:"},
1485 @{text "elim:"}, and @{text "dest:"} are passed to the appropriate proof
1488 \item @{command (HOL) "try"} attempts to prove or disprove a subgoal
1489 using a combination of provers and disprovers (@{text "solve_direct"},
1490 @{text "quickcheck"}, @{text "try_methods"}, @{text "sledgehammer"},
1493 \item @{command (HOL) "sledgehammer"} attempts to prove a subgoal using external
1494 automatic provers (resolution provers and SMT solvers). See the Sledgehammer
1495 manual \cite{isabelle-sledgehammer} for details.
1497 \item @{command (HOL) "sledgehammer_params"} changes
1498 @{command (HOL) "sledgehammer"} configuration options persistently.
1504 section {* Checking and refuting propositions *}
1507 Identifying incorrect propositions usually involves evaluation of
1508 particular assignments and systematic counterexample search. This
1509 is supported by the following commands.
1511 \begin{matharray}{rcl}
1512 @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1513 @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1514 @{command_def (HOL) "refute"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1515 @{command_def (HOL) "nitpick"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1516 @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"} \\
1517 @{command_def (HOL) "refute_params"} & : & @{text "theory \<rightarrow> theory"} \\
1518 @{command_def (HOL) "nitpick_params"} & : & @{text "theory \<rightarrow> theory"}
1522 @@{command (HOL) value} ( '[' name ']' )? modes? @{syntax term}
1525 (@@{command (HOL) quickcheck} | @@{command (HOL) refute} | @@{command (HOL) nitpick})
1526 ( '[' args ']' )? @{syntax nat}?
1529 (@@{command (HOL) quickcheck_params} | @@{command (HOL) refute_params} |
1530 @@{command (HOL) nitpick_params}) ( '[' args ']' )?
1533 modes: '(' (@{syntax name} +) ')'
1536 args: ( @{syntax name} '=' value + ',' )
1538 "} % FIXME check "value"
1542 \item @{command (HOL) "value"}~@{text t} evaluates and prints a
1543 term; optionally @{text modes} can be specified, which are
1544 appended to the current print mode; see \secref{sec:print-modes}.
1545 Internally, the evaluation is performed by registered evaluators,
1546 which are invoked sequentially until a result is returned.
1547 Alternatively a specific evaluator can be selected using square
1548 brackets; typical evaluators use the current set of code equations
1549 to normalize and include @{text simp} for fully symbolic
1550 evaluation using the simplifier, @{text nbe} for
1551 \emph{normalization by evaluation} and \emph{code} for code
1554 \item @{command (HOL) "quickcheck"} tests the current goal for
1555 counterexamples using a series of assignments for its
1556 free variables; by default the first subgoal is tested, an other
1557 can be selected explicitly using an optional goal index.
1558 Assignments can be chosen exhausting the search space upto a given
1559 size, or using a fixed number of random assignments in the search space,
1560 or exploring the search space symbolically using narrowing.
1561 By default, quickcheck uses exhaustive testing.
1562 A number of configuration options are supported for
1563 @{command (HOL) "quickcheck"}, notably:
1567 \item[@{text tester}] specifies which testing approach to apply.
1568 There are three testers, @{text exhaustive},
1569 @{text random}, and @{text narrowing}.
1570 An unknown configuration option is treated as an argument to tester,
1571 making @{text "tester ="} optional.
1572 When multiple testers are given, these are applied in parallel.
1573 If no tester is specified, quickcheck uses the testers that are
1574 set active, i.e., configurations
1575 @{text quickcheck_exhaustive_active}, @{text quickcheck_random_active},
1576 @{text quickcheck_narrowing_active} are set to true.
1577 \item[@{text size}] specifies the maximum size of the search space
1578 for assignment values.
1580 \item[@{text eval}] takes a term or a list of terms and evaluates
1581 these terms under the variable assignment found by quickcheck.
1583 \item[@{text iterations}] sets how many sets of assignments are
1584 generated for each particular size.
1586 \item[@{text no_assms}] specifies whether assumptions in
1587 structured proofs should be ignored.
1589 \item[@{text timeout}] sets the time limit in seconds.
1591 \item[@{text default_type}] sets the type(s) generally used to
1592 instantiate type variables.
1594 \item[@{text report}] if set quickcheck reports how many tests
1595 fulfilled the preconditions.
1597 \item[@{text quiet}] if not set quickcheck informs about the
1598 current size for assignment values.
1600 \item[@{text expect}] can be used to check if the user's
1601 expectation was met (@{text no_expectation}, @{text
1602 no_counterexample}, or @{text counterexample}).
1606 These option can be given within square brackets.
1608 \item @{command (HOL) "quickcheck_params"} changes
1609 @{command (HOL) "quickcheck"} configuration options persistently.
1611 \item @{command (HOL) "refute"} tests the current goal for
1612 counterexamples using a reduction to SAT. The following configuration
1613 options are supported:
1617 \item[@{text minsize}] specifies the minimum size (cardinality) of the
1618 models to search for.
1620 \item[@{text maxsize}] specifies the maximum size (cardinality) of the
1621 models to search for. Nonpositive values mean $\infty$.
1623 \item[@{text maxvars}] specifies the maximum number of Boolean variables
1624 to use when transforming the term into a propositional formula.
1625 Nonpositive values mean $\infty$.
1627 \item[@{text satsolver}] specifies the SAT solver to use.
1629 \item[@{text no_assms}] specifies whether assumptions in
1630 structured proofs should be ignored.
1632 \item[@{text maxtime}] sets the time limit in seconds.
1634 \item[@{text expect}] can be used to check if the user's
1635 expectation was met (@{text genuine}, @{text potential},
1636 @{text none}, or @{text unknown}).
1640 These option can be given within square brackets.
1642 \item @{command (HOL) "refute_params"} changes
1643 @{command (HOL) "refute"} configuration options persistently.
1645 \item @{command (HOL) "nitpick"} tests the current goal for counterexamples
1646 using a reduction to first-order relational logic. See the Nitpick manual
1647 \cite{isabelle-nitpick} for details.
1649 \item @{command (HOL) "nitpick_params"} changes
1650 @{command (HOL) "nitpick"} configuration options persistently.
1656 section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *}
1659 The following tools of Isabelle/HOL support cases analysis and
1660 induction in unstructured tactic scripts; see also
1661 \secref{sec:cases-induct} for proper Isar versions of similar ideas.
1663 \begin{matharray}{rcl}
1664 @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & @{text method} \\
1665 @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\
1666 @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\
1667 @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1671 @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?
1673 @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
1675 @@{method (HOL) ind_cases} (@{syntax prop}+) (@'for' (@{syntax name}+))?
1677 @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
1680 rule: 'rule' ':' @{syntax thmref}
1685 \item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit
1686 to reason about inductive types. Rules are selected according to
1687 the declarations by the @{attribute cases} and @{attribute induct}
1688 attributes, cf.\ \secref{sec:cases-induct}. The @{command (HOL)
1689 datatype} package already takes care of this.
1691 These unstructured tactics feature both goal addressing and dynamic
1692 instantiation. Note that named rule cases are \emph{not} provided
1693 as would be by the proper @{method cases} and @{method induct} proof
1694 methods (see \secref{sec:cases-induct}). Unlike the @{method
1695 induct} method, @{method induct_tac} does not handle structured rule
1696 statements, only the compact object-logic conclusion of the subgoal
1699 \item @{method (HOL) ind_cases} and @{command (HOL)
1700 "inductive_cases"} provide an interface to the internal @{ML_text
1701 mk_cases} operation. Rules are simplified in an unrestricted
1704 While @{method (HOL) ind_cases} is a proof method to apply the
1705 result immediately as elimination rules, @{command (HOL)
1706 "inductive_cases"} provides case split theorems at the theory level
1707 for later use. The @{keyword "for"} argument of the @{method (HOL)
1708 ind_cases} method allows to specify a list of variables that should
1709 be generalized before applying the resulting rule.
1715 section {* Executable code *}
1717 text {* For validation purposes, it is often useful to \emph{execute}
1718 specifications. In principle, execution could be simulated by
1719 Isabelle's inference kernel, i.e. by a combination of resolution and
1720 simplification. Unfortunately, this approach is rather inefficient.
1721 A more efficient way of executing specifications is to translate
1722 them into a functional programming language such as ML.
1724 Isabelle provides two generic frameworks to support code generation
1725 from executable specifications. Isabelle/HOL instantiates these
1726 mechanisms in a way that is amenable to end-user applications.
1730 subsection {* The new code generator (F. Haftmann) *}
1732 text {* This framework generates code from functional programs
1733 (including overloading using type classes) to SML \cite{SML}, OCaml
1734 \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
1735 \cite{scala-overview-tech-report}. Conceptually, code generation is
1736 split up in three steps: \emph{selection} of code theorems,
1737 \emph{translation} into an abstract executable view and
1738 \emph{serialization} to a specific \emph{target language}.
1739 Inductive specifications can be executed using the predicate
1740 compiler which operates within HOL. See \cite{isabelle-codegen} for
1743 \begin{matharray}{rcl}
1744 @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1745 @{attribute_def (HOL) code} & : & @{text attribute} \\
1746 @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
1747 @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
1748 @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1749 @{attribute_def (HOL) code_inline} & : & @{text attribute} \\
1750 @{attribute_def (HOL) code_post} & : & @{text attribute} \\
1751 @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1752 @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1753 @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1754 @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
1755 @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
1756 @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
1757 @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
1758 @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
1759 @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
1760 @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
1761 @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
1762 @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"}
1766 @@{command (HOL) export_code} ( constexpr + ) \\
1767 ( ( @'in' target ( @'module_name' @{syntax string} ) ? \\
1768 ( @'file' ( @{syntax string} | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
1771 const: @{syntax term}
1774 constexpr: ( const | 'name._' | '_' )
1777 typeconstructor: @{syntax nameref}
1780 class: @{syntax nameref}
1783 target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
1786 @@{attribute (HOL) code} ( 'del' | 'abstype' | 'abstract' )?
1789 @@{command (HOL) code_abort} ( const + )
1792 @@{command (HOL) code_datatype} ( const + )
1795 @@{attribute (HOL) code_inline} ( 'del' ) ?
1798 @@{attribute (HOL) code_post} ( 'del' ) ?
1801 @@{command (HOL) code_thms} ( constexpr + ) ?
1804 @@{command (HOL) code_deps} ( constexpr + ) ?
1807 @@{command (HOL) code_const} (const + @'and') \\
1808 ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
1811 @@{command (HOL) code_type} (typeconstructor + @'and') \\
1812 ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
1815 @@{command (HOL) code_class} (class + @'and') \\
1816 ( ( '(' target \\ ( @{syntax string} ? + @'and' ) ')' ) + )
1819 @@{command (HOL) code_instance} (( typeconstructor '::' class ) + @'and') \\
1820 ( ( '(' target ( '-' ? + @'and' ) ')' ) + )
1823 @@{command (HOL) code_reserved} target ( @{syntax string} + )
1826 @@{command (HOL) code_monad} const const target
1829 @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
1832 @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )
1835 @@{command (HOL) code_reflect} @{syntax string} \\
1836 ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \\
1837 ( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?
1840 syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
1845 \item @{command (HOL) "export_code"} generates code for a given list
1846 of constants in the specified target language(s). If no
1847 serialization instruction is given, only abstract code is generated
1850 Constants may be specified by giving them literally, referring to
1851 all executable contants within a certain theory by giving @{text
1852 "name.*"}, or referring to \emph{all} executable constants currently
1853 available by giving @{text "*"}.
1855 By default, for each involved theory one corresponding name space
1856 module is generated. Alternativly, a module name may be specified
1857 after the @{keyword "module_name"} keyword; then \emph{all} code is
1858 placed in this module.
1860 For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
1861 refers to a single file; for \emph{Haskell}, it refers to a whole
1862 directory, where code is generated in multiple files reflecting the
1863 module hierarchy. Omitting the file specification denotes standard
1866 Serializers take an optional list of arguments in parentheses. For
1867 \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
1868 explicit module signatures.
1870 For \emph{Haskell} a module name prefix may be given using the
1871 ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
1872 ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
1873 datatype declaration.
1875 \item @{attribute (HOL) code} explicitly selects (or with option
1876 ``@{text "del"}'' deselects) a code equation for code generation.
1877 Usually packages introducing code equations provide a reasonable
1878 default setup for selection. Variants @{text "code abstype"} and
1879 @{text "code abstract"} declare abstract datatype certificates or
1880 code equations on abstract datatype representations respectively.
1882 \item @{command (HOL) "code_abort"} declares constants which are not
1883 required to have a definition by means of code equations; if needed
1884 these are implemented by program abort instead.
1886 \item @{command (HOL) "code_datatype"} specifies a constructor set
1889 \item @{command (HOL) "print_codesetup"} gives an overview on
1890 selected code equations and code generator datatypes.
1892 \item @{attribute (HOL) code_inline} declares (or with option
1893 ``@{text "del"}'' removes) inlining theorems which are applied as
1894 rewrite rules to any code equation during preprocessing.
1896 \item @{attribute (HOL) code_post} declares (or with option ``@{text
1897 "del"}'' removes) theorems which are applied as rewrite rules to any
1898 result of an evaluation.
1900 \item @{command (HOL) "print_codeproc"} prints the setup of the code
1901 generator preprocessor.
1903 \item @{command (HOL) "code_thms"} prints a list of theorems
1904 representing the corresponding program containing all given
1905 constants after preprocessing.
1907 \item @{command (HOL) "code_deps"} visualizes dependencies of
1908 theorems representing the corresponding program containing all given
1909 constants after preprocessing.
1911 \item @{command (HOL) "code_const"} associates a list of constants
1912 with target-specific serializations; omitting a serialization
1913 deletes an existing serialization.
1915 \item @{command (HOL) "code_type"} associates a list of type
1916 constructors with target-specific serializations; omitting a
1917 serialization deletes an existing serialization.
1919 \item @{command (HOL) "code_class"} associates a list of classes
1920 with target-specific class names; omitting a serialization deletes
1921 an existing serialization. This applies only to \emph{Haskell}.
1923 \item @{command (HOL) "code_instance"} declares a list of type
1924 constructor / class instance relations as ``already present'' for a
1925 given target. Omitting a ``@{text "-"}'' deletes an existing
1926 ``already present'' declaration. This applies only to
1929 \item @{command (HOL) "code_reserved"} declares a list of names as
1930 reserved for a given target, preventing it to be shadowed by any
1933 \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
1934 to generate monadic code for Haskell.
1936 \item @{command (HOL) "code_include"} adds arbitrary named content
1937 (``include'') to generated code. A ``@{text "-"}'' as last argument
1938 will remove an already added ``include''.
1940 \item @{command (HOL) "code_modulename"} declares aliasings from one
1941 module name onto another.
1943 \item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
1944 argument compiles code into the system runtime environment and
1945 modifies the code generator setup that future invocations of system
1946 runtime code generation referring to one of the ``@{text
1947 "datatypes"}'' or ``@{text "functions"}'' entities use these precompiled
1948 entities. With a ``@{text "file"}'' argument, the corresponding code
1949 is generated into that specified file without modifying the code
1956 subsection {* The old code generator (S. Berghofer) *}
1958 text {* This framework generates code from both functional and
1959 relational programs to SML, as explained below.
1961 \begin{matharray}{rcl}
1962 @{command_def "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
1963 @{command_def "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
1964 @{command_def "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
1965 @{command_def "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
1966 @{attribute_def code} & : & @{text attribute} \\
1970 ( @@{command code_module} | @@{command code_library} ) modespec? @{syntax name}? \\
1971 ( @'file' name ) ? ( @'imports' ( @{syntax name} + ) ) ? \\
1972 @'contains' ( ( @{syntax name} '=' @{syntax term} ) + | @{syntax term} + )
1975 modespec: '(' ( @{syntax name} * ) ')'
1978 @@{command (HOL) consts_code} (codespec +)
1981 codespec: const template attachment ?
1984 @@{command (HOL) types_code} (tycodespec +)
1987 tycodespec: @{syntax name} template attachment ?
1990 const: @{syntax term}
1993 template: '(' @{syntax string} ')'
1996 attachment: 'attach' modespec? '{' @{syntax text} '}'
1999 @@{attribute code} name?
2004 subsubsection {* Invoking the code generator *}
2006 text {* The code generator is invoked via the @{command code_module}
2007 and @{command code_library} commands, which correspond to
2008 \emph{incremental} and \emph{modular} code generation, respectively.
2012 \item [Modular] For each theory, an ML structure is generated,
2013 containing the code generated from the constants defined in this
2016 \item [Incremental] All the generated code is emitted into the same
2017 structure. This structure may import code from previously generated
2018 structures, which can be specified via @{keyword "imports"}.
2019 Moreover, the generated structure may also be referred to in later
2020 invocations of the code generator.
2024 After the @{command code_module} and @{command code_library}
2025 keywords, the user may specify an optional list of ``modes'' in
2026 parentheses. These can be used to instruct the code generator to
2027 emit additional code for special purposes, e.g.\ functions for
2028 converting elements of generated datatypes to Isabelle terms, or
2029 test data generators. The list of modes is followed by a module
2030 name. The module name is optional for modular code generation, but
2031 must be specified for incremental code generation.
2033 The code can either be written to a file, in which case a file name
2034 has to be specified after the @{keyword "file"} keyword, or be loaded
2035 directly into Isabelle's ML environment. In the latter case, the
2036 @{command ML} theory command can be used to inspect the results
2037 interactively, for example.
2039 The terms from which to generate code can be specified after the
2040 @{keyword "contains"} keyword, either as a list of bindings, or just
2041 as a list of terms. In the latter case, the code generator just
2042 produces code for all constants and types occuring in the term, but
2043 does not bind the compiled terms to ML identifiers.
2049 contains test = "foldl op + (0 :: int) [1, 2, 3, 4, 5]"
2051 text {* \noindent This binds the result of compiling the given term to
2052 the ML identifier @{ML Test.test}. *}
2054 ML {* @{assert} (Test.test = 15) *}
2057 subsubsection {* Configuring the code generator *}
2059 text {* When generating code for a complex term, the code generator
2060 recursively calls itself for all subterms. When it arrives at a
2061 constant, the default strategy of the code generator is to look up
2062 its definition and try to generate code for it. Constants which
2063 have no definitions that are immediately executable, may be
2064 associated with a piece of ML code manually using the @{command_ref
2065 consts_code} command. It takes a list whose elements consist of a
2066 constant (given in usual term syntax -- an explicit type constraint
2067 accounts for overloading), and a mixfix template describing the ML
2068 code. The latter is very much the same as the mixfix templates used
2069 when declaring new constants. The most notable difference is that
2070 terms may be included in the ML template using antiquotation
2071 brackets @{verbatim "{"}@{verbatim "*"}~@{text "..."}~@{verbatim
2072 "*"}@{verbatim "}"}.
2074 A similar mechanism is available for types: @{command_ref
2075 types_code} associates type constructors with specific ML code.
2077 For example, the following declarations copied from @{file
2078 "~~/src/HOL/Product_Type.thy"} describe how the product type of
2079 Isabelle/HOL should be compiled to ML. *}
2081 typedecl ('a, 'b) prod
2082 consts Pair :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) prod"
2084 types_code prod ("(_ */ _)")
2085 consts_code Pair ("(_,/ _)")
2087 text {* Sometimes, the code associated with a constant or type may
2088 need to refer to auxiliary functions, which have to be emitted when
2089 the constant is used. Code for such auxiliary functions can be
2090 declared using @{keyword "attach"}. For example, the @{const wfrec}
2091 function can be implemented as follows:
2094 consts_code wfrec ("\<module>wfrec?") (* FIXME !? *)
2095 attach {* fun wfrec f x = f (wfrec f) x *}
2097 text {* If the code containing a call to @{const wfrec} resides in an
2098 ML structure different from the one containing the function
2099 definition attached to @{const wfrec}, the name of the ML structure
2100 (followed by a ``@{text "."}'') is inserted in place of ``@{text
2101 "\<module>"}'' in the above template. The ``@{text "?"}'' means that
2102 the code generator should ignore the first argument of @{const
2103 wfrec}, i.e.\ the termination relation, which is usually not
2106 \medskip Another possibility of configuring the code generator is to
2107 register theorems to be used for code generation. Theorems can be
2108 registered via the @{attribute code} attribute. It takes an optional
2109 name as an argument, which indicates the format of the
2110 theorem. Currently supported formats are equations (this is the
2111 default when no name is specified) and horn clauses (this is
2112 indicated by the name \texttt{ind}). The left-hand sides of
2113 equations may only contain constructors and distinct variables,
2114 whereas horn clauses must have the same format as introduction rules
2115 of inductive definitions.
2117 The following example specifies three equations from which to
2118 generate code for @{term "op <"} on natural numbers (see also
2119 @{"file" "~~/src/HOL/Nat.thy"}). *}
2121 lemma [code]: "(Suc m < Suc n) = (m < n)"
2122 and [code]: "((n::nat) < 0) = False"
2123 and [code]: "(0 < Suc n) = True" by simp_all
2126 subsubsection {* Specific HOL code generators *}
2128 text {* The basic code generator framework offered by Isabelle/Pure
2129 has already been extended with additional code generators for
2130 specific HOL constructs. These include datatypes, recursive
2131 functions and inductive relations. The code generator for inductive
2132 relations can handle expressions of the form @{text "(t\<^sub>1, \<dots>, t\<^sub>n) \<in>
2133 r"}, where @{text "r"} is an inductively defined relation. If at
2134 least one of the @{text "t\<^sub>i"} is a dummy pattern ``@{text "_"}'',
2135 the above expression evaluates to a sequence of possible answers. If
2136 all of the @{text "t\<^sub>i"} are proper terms, the expression evaluates
2139 The following example demonstrates this for beta-reduction on lambda
2140 terms (see also @{"file" "~~/src/HOL/Proofs/Lambda/Lambda.thy"}).
2145 | App dB dB (infixl "\<degree>" 200)
2148 primrec lift :: "dB \<Rightarrow> nat \<Rightarrow> dB"
2150 "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
2151 | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
2152 | "lift (Abs s) k = Abs (lift s (k + 1))"
2154 primrec subst :: "dB \<Rightarrow> dB \<Rightarrow> nat \<Rightarrow> dB" ("_[_'/_]" [300, 0, 0] 300)
2157 (if k < i then Var (i - 1) else if i = k then s else Var i)"
2158 | "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
2159 | "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
2161 inductive beta :: "dB \<Rightarrow> dB \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
2163 beta: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
2164 | appL: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
2165 | appR: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
2166 | abs: "s \<rightarrow>\<^sub>\<beta> t \<Longrightarrow> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
2170 test1 = "Abs (Var 0) \<degree> Var 0 \<rightarrow>\<^sub>\<beta> Var 0"
2171 test2 = "Abs (Abs (Var 0 \<degree> Var 0) \<degree> (Abs (Var 0) \<degree> Var 0)) \<rightarrow>\<^sub>\<beta> _"
2174 In the above example, @{ML Test.test1} evaluates to a boolean,
2175 whereas @{ML Test.test2} is a lazy sequence whose elements can be
2176 inspected separately.
2179 ML {* @{assert} Test.test1 *}
2180 ML {* val results = DSeq.list_of Test.test2 *}
2181 ML {* @{assert} (length results = 2) *}
2184 \medskip The theory underlying the HOL code generator is described
2185 more detailed in \cite{Berghofer-Nipkow:2002}. More examples that
2186 illustrate the usage of the code generator can be found e.g.\ in
2187 @{"file" "~~/src/HOL/MicroJava/J/JListExample.thy"} and @{"file"
2188 "~~/src/HOL/MicroJava/JVM/JVMListExample.thy"}.
2192 section {* Definition by specification \label{sec:hol-specification} *}
2195 \begin{matharray}{rcl}
2196 @{command_def (HOL) "specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
2197 @{command_def (HOL) "ax_specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
2201 (@@{command (HOL) specification} | @@{command (HOL) ax_specification})
2202 '(' (decl +) ')' \\ (@{syntax thmdecl}? @{syntax prop} +)
2204 decl: ((@{syntax name} ':')? @{syntax term} '(' @'overloaded' ')'?)
2209 \item @{command (HOL) "specification"}~@{text "decls \<phi>"} sets up a
2210 goal stating the existence of terms with the properties specified to
2211 hold for the constants given in @{text decls}. After finishing the
2212 proof, the theory will be augmented with definitions for the given
2213 constants, as well as with theorems stating the properties for these
2216 \item @{command (HOL) "ax_specification"}~@{text "decls \<phi>"} sets up
2217 a goal stating the existence of terms with the properties specified
2218 to hold for the constants given in @{text decls}. After finishing
2219 the proof, the theory will be augmented with axioms expressing the
2220 properties given in the first place.
2222 \item @{text decl} declares a constant to be defined by the
2223 specification given. The definition for the constant @{text c} is
2224 bound to the name @{text c_def} unless a theorem name is given in
2225 the declaration. Overloaded constants should be declared as such.
2229 Whether to use @{command (HOL) "specification"} or @{command (HOL)
2230 "ax_specification"} is to some extent a matter of style. @{command
2231 (HOL) "specification"} introduces no new axioms, and so by
2232 construction cannot introduce inconsistencies, whereas @{command
2233 (HOL) "ax_specification"} does introduce axioms, but only after the
2234 user has explicitly proven it to be safe. A practical issue must be
2235 considered, though: After introducing two constants with the same
2236 properties using @{command (HOL) "specification"}, one can prove
2237 that the two constants are, in fact, equal. If this might be a
2238 problem, one should use @{command (HOL) "ax_specification"}.