1 (* Title: Doc/Datatypes/Datatypes.thy
2 Author: Jasmin Blanchette, TU Muenchen
3 Author: Lorenz Panny, TU Muenchen
4 Author: Andrei Popescu, TU Muenchen
5 Author: Dmitriy Traytel, TU Muenchen
7 Tutorial for (co)datatype definitions with the new package.
11 imports Setup "~~/src/HOL/Library/Simps_Case_Conv"
14 section {* Introduction
15 \label{sec:introduction} *}
18 The 2013 edition of Isabelle introduced a new definitional package for freely
19 generated datatypes and codatatypes. The datatype support is similar to that
20 provided by the earlier package due to Berghofer and Wenzel
21 \cite{Berghofer-Wenzel:1999:TPHOL}, documented in the Isar reference manual
22 \cite{isabelle-isar-ref}; indeed, replacing the keyword \keyw{datatype} by
23 @{command datatype_new} is usually all that is needed to port existing theories
24 to use the new package.
26 Perhaps the main advantage of the new package is that it supports recursion
27 through a large class of non-datatypes, such as finite sets:
30 datatype_new 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s (lbl\<^sub>f\<^sub>s: 'a) (sub\<^sub>f\<^sub>s: "'a tree\<^sub>f\<^sub>s fset")
34 Another strong point is the support for local definitions:
39 datatype_new flag = Less | Eq | Greater
44 Furthermore, the package provides a lot of convenience, including automatically
45 generated discriminators, selectors, and relators as well as a wealth of
46 properties about them.
48 In addition to inductive datatypes, the new package supports coinductive
49 datatypes, or \emph{codatatypes}, which allow infinite values. For example, the
50 following command introduces the type of lazy lists, which comprises both finite
58 codatatype (*<*)(in early) (*>*)'a llist = LNil | LCons 'a "'a llist"
62 Mixed inductive--coinductive recursion is possible via nesting. Compare the
63 following four Rose tree examples:
66 datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
67 datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
68 codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
69 codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
72 The first two tree types allow only paths of finite length, whereas the last two
73 allow infinite paths. Orthogonally, the nodes in the first and third types have
74 finitely many direct subtrees, whereas those of the second and fourth may have
77 To use the package, it is necessary to import the @{theory BNF} theory, which
78 can be precompiled into the \texttt{HOL-BNF} image. The following commands show
79 how to launch jEdit/PIDE with the image loaded and how to build the image
80 without launching jEdit:
85 \ \ \ \ \texttt{isabelle jedit -l HOL-BNF} \\
87 \hbox{}\ \ \ \ \texttt{isabelle build -b HOL-BNF}
91 The package, like its predecessor, fully adheres to the LCF philosophy
92 \cite{mgordon79}: The characteristic theorems associated with the specified
93 (co)datatypes are derived rather than introduced axiomatically.%
94 \footnote{If the @{text quick_and_dirty} option is enabled, some of the
95 internal constructions and most of the internal proof obligations are skipped.}
96 The package's metatheory is described in a pair of papers
97 \cite{traytel-et-al-2012,blanchette-et-al-wit}. The central notion is that of a
98 \emph{bounded natural functor} (BNF)---a well-behaved type constructor for which
99 nested (co)recursion is supported.
101 This tutorial is organized as follows:
104 \setlength{\itemsep}{0pt}
106 \item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
107 describes how to specify datatypes using the @{command datatype_new} command.
109 \item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
110 Functions,'' describes how to specify recursive functions using
111 @{command primrec_new}, \keyw{fun}, and \keyw{function}.
113 \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
114 describes how to specify codatatypes using the @{command codatatype} command.
116 \item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive
117 Functions,'' describes how to specify corecursive functions using the
118 @{command primcorec} and @{command primcorecursive} commands.
120 \item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
121 Bounded Natural Functors,'' explains how to use the @{command bnf} command
122 to register arbitrary type constructors as BNFs.
125 \ref{sec:deriving-destructors-and-theorems-for-free-constructors},
126 ``Deriving Destructors and Theorems for Free Constructors,'' explains how to
127 use the command @{command wrap_free_constructors} to derive destructor constants
128 and theorems for freely generated types, as performed internally by @{command
129 datatype_new} and @{command codatatype}.
131 %\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
132 %describes the package's programmatic interface.
134 %\item Section \ref{sec:interoperability}, ``Interoperability,''
135 %is concerned with the packages' interaction with other Isabelle packages and
136 %tools, such as the code generator and the counterexample generators.
138 %\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
139 %Limitations,'' concludes with known open issues at the time of writing.
144 \setbox\boxA=\hbox{\texttt{NOSPAM}}
146 \newcommand\authoremaili{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
147 in.\allowbreak tum.\allowbreak de}}
148 \newcommand\authoremailii{\texttt{lore{\color{white}NOSPAM}\kern-\wd\boxA{}nz.panny@\allowbreak
149 \allowbreak tum.\allowbreak de}}
150 \newcommand\authoremailiii{\texttt{pope{\color{white}NOSPAM}\kern-\wd\boxA{}scua@\allowbreak
151 in.\allowbreak tum.\allowbreak de}}
152 \newcommand\authoremailiv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak
153 in.\allowbreak tum.\allowbreak de}}
155 The commands @{command datatype_new} and @{command primrec_new} are expected to
156 replace \keyw{datatype} and \keyw{primrec} in a future release. Authors of new
157 theories are encouraged to use the new commands, and maintainers of older
158 theories may want to consider upgrading.
160 Comments and bug reports concerning either the tool or this tutorial should be
161 directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
166 section {* Defining Datatypes
167 \label{sec:defining-datatypes} *}
170 Datatypes can be specified using the @{command datatype_new} command.
174 subsection {* Introductory Examples
175 \label{ssec:datatype-introductory-examples} *}
178 Datatypes are illustrated through concrete examples featuring different flavors
179 of recursion. More examples can be found in the directory
180 \verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|.
183 subsubsection {* Nonrecursive Types
184 \label{sssec:datatype-nonrecursive-types} *}
187 Datatypes are introduced by specifying the desired names and argument types for
188 their constructors. \emph{Enumeration} types are the simplest form of datatype.
189 All their constructors are nullary:
192 datatype_new trool = Truue | Faalse | Perhaaps
196 Here, @{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}.
198 Polymorphic types are possible, such as the following option type, modeled after
199 its homologue from the @{theory Option} theory:
205 datatype_new 'a option = None | Some 'a
209 The constructors are @{text "None :: 'a option"} and
210 @{text "Some :: 'a \<Rightarrow> 'a option"}.
212 The next example has three type parameters:
215 datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c
220 @{text "Triple :: 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a, 'b, 'c) triple"}.
221 Unlike in Standard ML, curried constructors are supported. The uncurried variant
225 datatype_new ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
229 Occurrences of nonatomic types on the right-hand side of the equal sign must be
230 enclosed in double quotes, as is customary in Isabelle.
234 subsubsection {* Simple Recursion
235 \label{sssec:datatype-simple-recursion} *}
238 Natural numbers are the simplest example of a recursive type:
241 datatype_new nat = Zero | Suc nat
245 Lists were shown in the introduction. Terminated lists are a variant that
246 stores a value of type @{typ 'b} at the very end:
249 datatype_new (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
252 subsubsection {* Mutual Recursion
253 \label{sssec:datatype-mutual-recursion} *}
256 \emph{Mutually recursive} types are introduced simultaneously and may refer to
257 each other. The example below introduces a pair of types for even and odd
261 datatype_new even_nat = Even_Zero | Even_Suc odd_nat
262 and odd_nat = Odd_Suc even_nat
266 Arithmetic expressions are defined via terms, terms via factors, and factors via
270 datatype_new ('a, 'b) exp =
271 Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
273 Factor "('a, 'b) fct" | Prod "('a, 'b) fct" "('a, 'b) trm"
275 Const 'a | Var 'b | Expr "('a, 'b) exp"
278 subsubsection {* Nested Recursion
279 \label{sssec:datatype-nested-recursion} *}
282 \emph{Nested recursion} occurs when recursive occurrences of a type appear under
283 a type constructor. The introduction showed some examples of trees with nesting
284 through lists. A more complex example, that reuses our @{type option} type,
288 datatype_new 'a btree =
289 BNode 'a "'a btree option" "'a btree option"
293 Not all nestings are admissible. For example, this command will fail:
296 datatype_new 'a wrong = W1 | W2 (*<*)'a
297 typ (*>*)"'a wrong \<Rightarrow> 'a"
301 The issue is that the function arrow @{text "\<Rightarrow>"} allows recursion
302 only through its right-hand side. This issue is inherited by polymorphic
303 datatypes defined in terms of~@{text "\<Rightarrow>"}:
306 datatype_new ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
307 datatype_new 'a also_wrong = W1 | W2 (*<*)'a
308 typ (*>*)"('a also_wrong, 'a) fn"
315 datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
319 In general, type constructors @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
320 allow recursion on a subset of their type arguments @{text 'a\<^sub>1}, \ldots,
321 @{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
322 type arguments are called \emph{dead}. In @{typ "'a \<Rightarrow> 'b"} and
323 @{typ "('a, 'b) fn"}, the type variable @{typ 'a} is dead and @{typ 'b} is live.
325 Type constructors must be registered as BNFs to have live arguments. This is
326 done automatically for datatypes and codatatypes introduced by the @{command
327 datatype_new} and @{command codatatype} commands.
328 Section~\ref{sec:registering-bounded-natural-functors} explains how to register
329 arbitrary type constructors as BNFs.
331 Here is another example that fails:
334 datatype_new 'a pow_list = PNil 'a (*<*)'a
335 datatype_new 'a pow_list' = PNil' 'a (*>*)| PCons "('a * 'a) pow_list"
339 This one features a different flavor of nesting, where the recursive call in the
340 type specification occurs around (rather than inside) another type constructor.
343 subsubsection {* Auxiliary Constants and Properties
344 \label{sssec:datatype-auxiliary-constants-and-properties} *}
347 The @{command datatype_new} command introduces various constants in addition to
348 the constructors. With each datatype are associated set functions, a map
349 function, a relator, discriminators, and selectors, all of which can be given
350 custom names. In the example below, the familiar names @{text null}, @{text hd},
351 @{text tl}, @{text set}, @{text map}, and @{text list_all2}, override the
352 default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2},
353 @{text set_list}, @{text map_list}, and @{text rel_list}:
358 "[x, xs]" == "x # [xs]"
366 hide_const Nil Cons hd tl set map list_all2
370 datatype_new (set: 'a) list (map: map rel: list_all2) =
371 null: Nil (defaults tl: Nil)
372 | Cons (hd: 'a) (tl: "'a list")
377 \begin{tabular}{@ {}ll@ {}}
379 @{text "Nil \<Colon> 'a list"} \\
381 @{text "Cons \<Colon> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"} \\
383 @{text "null \<Colon> 'a list \<Rightarrow> bool"} \\
385 @{text "hd \<Colon> 'a list \<Rightarrow> 'a"} \\
387 @{text "tl \<Colon> 'a list \<Rightarrow> 'a list"} \\
389 @{text "set \<Colon> 'a list \<Rightarrow> 'a set"} \\
391 @{text "map \<Colon> ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \\
393 @{text "list_all2 \<Colon> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"}
396 The discriminator @{const null} and the selectors @{const hd} and @{const tl}
397 are characterized as follows:
399 \[@{thm list.collapse(1)[of xs, no_vars]}
400 \qquad @{thm list.collapse(2)[of xs, no_vars]}\]
402 For two-constructor datatypes, a single discriminator constant is sufficient.
403 The discriminator associated with @{const Cons} is simply
404 @{term "\<lambda>xs. \<not> null xs"}.
406 The @{text defaults} clause following the @{const Nil} constructor specifies a
407 default value for selectors associated with other constructors. Here, it is used
408 to ensure that the tail of the empty list is itself (instead of being left
411 Because @{const Nil} is nullary, it is also possible to use
412 @{term "\<lambda>xs. xs = Nil"} as a discriminator. This is specified by
413 entering ``@{text "="}'' instead of the identifier @{const null}. Although this
414 may look appealing, the mixture of constructors and selectors in the
415 characteristic theorems can lead Isabelle's automation to switch between the
416 constructor and the destructor view in surprising ways.
418 The usual mixfix syntax annotations are available for both types and
419 constructors. For example:
425 datatype_new ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
427 text {* \blankline *}
429 datatype_new (set: 'a) list (map: map rel: list_all2) =
431 | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
435 Incidentally, this is how the traditional syntax can be set up:
438 syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
440 text {* \blankline *}
443 "[x, xs]" == "x # [xs]"
447 subsection {* Command Syntax
448 \label{ssec:datatype-command-syntax} *}
451 subsubsection {* \keyw{datatype\_new}
452 \label{sssec:datatype-new} *}
455 \begin{matharray}{rcl}
456 @{command_def "datatype_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
460 @@{command datatype_new} target? @{syntax dt_options}? \\
461 (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
463 @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
466 The syntactic entity \synt{target} can be used to specify a local
467 context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
468 manual \cite{isabelle-isar-ref}.
470 The optional target is optionally followed by datatype-specific options:
473 \setlength{\itemsep}{0pt}
476 The @{text "no_discs_sels"} option indicates that no discriminators or selectors
480 The @{text "no_code"} option indicates that the datatype should not be
481 registered for code generation.
484 The @{text "rep_compat"} option indicates that the generated names should
485 contain optional (and normally not displayed) ``@{text "new."}'' components to
486 prevent clashes with a later call to \keyw{rep\_datatype}. See
487 Section~\ref{ssec:datatype-compatibility-issues} for details.
490 The left-hand sides of the datatype equations specify the name of the type to
491 define, its type parameters, and additional information:
494 @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
496 @{syntax_def tyargs}: typefree | '(' ((name ':')? typefree + ',') ')'
498 @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
502 The syntactic entity \synt{name} denotes an identifier, \synt{typefree}
503 denotes fixed type variable (@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix}
504 denotes the usual parenthesized mixfix notation. They are documented in the Isar
505 reference manual \cite{isabelle-isar-ref}.
507 The optional names preceding the type variables allow to override the default
508 names of the set functions (@{text set1_t}, \ldots, @{text setM_t}).
509 Inside a mutually recursive specification, all defined datatypes must
510 mention exactly the same type variables in the same order.
513 @{syntax_def ctor}: (name ':')? name (@{syntax ctor_arg} * ) \\
514 @{syntax dt_sel_defaults}? mixfix?
520 The main constituents of a constructor specification are the name of the
521 constructor and the list of its argument types. An optional discriminator name
522 can be supplied at the front to override the default name
523 (@{text t.is_C\<^sub>j}).
526 @{syntax_def ctor_arg}: type | '(' name ':' type ')'
532 In addition to the type of a constructor argument, it is possible to specify a
533 name for the corresponding selector to override the default name
534 (@{text un_C\<^sub>ji}). The same selector names can be reused for several
535 constructors as long as they share the same type.
538 @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')'
543 @{text "C \<Colon> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<sigma>"},
544 default values can be specified for any selector
545 @{text "un_D \<Colon> \<sigma> \<Rightarrow> \<tau>"}
546 associated with other constructors. The specified default value must be of type
547 @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<tau>"}
548 (i.e., it may depend on @{text C}'s arguments).
552 subsubsection {* \keyw{datatype\_new\_compat}
553 \label{sssec:datatype-new-compat} *}
556 \begin{matharray}{rcl}
557 @{command_def "datatype_new_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
561 @@{command datatype_new_compat} names
565 The old datatype package provides some functionality that is not yet replicated
569 \setlength{\itemsep}{0pt}
571 \item It is integrated with \keyw{fun} and \keyw{function}
572 \cite{isabelle-function}, Nitpick \cite{isabelle-nitpick}, Quickcheck,
575 \item It is extended by various add-ons, notably to produce instances of the
576 @{const size} function.
580 New-style datatypes can in most cases be registered as old-style datatypes using
581 @{command datatype_new_compat}. The \textit{names} argument is a space-separated
582 list of type names that are mutually recursive. For example:
585 datatype_new_compat even_nat odd_nat
587 text {* \blankline *}
589 thm even_nat_odd_nat.size
591 text {* \blankline *}
593 ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *}
596 A few remarks concern nested recursive datatypes only:
599 \setlength{\itemsep}{0pt}
601 \item The old-style, nested-as-mutual induction rule, iterator theorems, and
602 recursor theorems are generated under their usual names but with ``@{text
603 "compat_"}'' prefixed (e.g., @{text compat_tree.induct}).
605 \item All types through which recursion takes place must be new-style datatypes
606 or the function type. In principle, it should be possible to support old-style
607 datatypes as well, but the command does not support this yet (and there is
608 currently no way to register old-style datatypes as new-style datatypes).
610 \item The recursor produced for types that recurse through functions has a
611 different signature than with the old package. This makes it impossible to use
612 the old \keyw{primrec} command.
615 An alternative to @{command datatype_new_compat} is to use the old package's
616 \keyw{rep\_datatype} command. The associated proof obligations must then be
621 subsection {* Generated Constants
622 \label{ssec:datatype-generated-constants} *}
625 Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
626 with $m > 0$ live type variables and $n$ constructors
627 @{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the
628 following auxiliary constants are introduced:
631 \setlength{\itemsep}{0pt}
633 \item \relax{Case combinator}: @{text t.case_t} (rendered using the familiar
634 @{text case}--@{text of} syntax)
636 \item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
637 @{text "t.is_C\<^sub>n"}
639 \item \relax{Selectors}:
640 @{text t.un_C\<^sub>11}$, \ldots, @{text t.un_C\<^sub>1k\<^sub>1}, \\
641 \phantom{\relax{Selectors:}} \quad\vdots \\
642 \phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
644 \item \relax{Set functions} (or \relax{natural transformations}):
645 @{text set1_t}, \ldots, @{text t.setm_t}
647 \item \relax{Map function} (or \relax{functorial action}): @{text t.map_t}
649 \item \relax{Relator}: @{text t.rel_t}
651 \item \relax{Iterator}: @{text t.fold_t}
653 \item \relax{Recursor}: @{text t.rec_t}
658 The case combinator, discriminators, and selectors are collectively called
659 \emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
660 names and is normally hidden.
664 subsection {* Generated Theorems
665 \label{ssec:datatype-generated-theorems} *}
668 The characteristic theorems generated by @{command datatype_new} are grouped in
669 three broad categories:
672 \setlength{\itemsep}{0pt}
674 \item The \emph{free constructor theorems} are properties about the constructors
675 and destructors that can be derived for any freely generated type. Internally,
676 the derivation is performed by @{command wrap_free_constructors}.
678 \item The \emph{functorial theorems} are properties of datatypes related to
681 \item The \emph{inductive theorems} are properties of datatypes related to
682 their inductive nature.
687 The full list of named theorems can be obtained as usual by entering the
688 command \keyw{print\_theorems} immediately after the datatype definition.
689 This list normally excludes low-level theorems that reveal internal
690 constructions. To make these accessible, add the line
693 declare [[bnf_note_all]]
695 declare [[bnf_note_all = false]]
700 to the top of the theory file.
703 subsubsection {* Free Constructor Theorems
704 \label{sssec:free-constructor-theorems} *}
711 The free constructor theorems are partitioned in three subgroups. The first
712 subgroup of properties is concerned with the constructors. They are listed below
713 for @{typ "'a list"}:
718 \item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\rm:] ~ \\
719 @{thm list.inject[no_vars]}
721 \item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\rm:] ~ \\
722 @{thm list.distinct(1)[no_vars]} \\
723 @{thm list.distinct(2)[no_vars]}
725 \item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
726 @{thm list.exhaust[no_vars]}
728 \item[@{text "t."}\hthm{nchotomy}\rm:] ~ \\
729 @{thm list.nchotomy[no_vars]}
735 In addition, these nameless theorems are registered as safe elimination rules:
740 \item[@{text "t."}\hthm{distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rm:] ~ \\
741 @{thm list.distinct(1)[THEN notE, elim!, no_vars]} \\
742 @{thm list.distinct(2)[THEN notE, elim!, no_vars]}
748 The next subgroup is concerned with the case combinator:
753 \item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\
754 @{thm list.case(1)[no_vars]} \\
755 @{thm list.case(2)[no_vars]}
757 \item[@{text "t."}\hthm{case\_cong}\rm:] ~ \\
758 @{thm list.case_cong[no_vars]}
760 \item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\rm:] ~ \\
761 @{thm list.weak_case_cong[no_vars]}
763 \item[@{text "t."}\hthm{split}\rm:] ~ \\
764 @{thm list.split[no_vars]}
766 \item[@{text "t."}\hthm{split\_asm}\rm:] ~ \\
767 @{thm list.split_asm[no_vars]}
769 \item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]
775 The third subgroup revolves around discriminators and selectors:
780 \item[@{text "t."}\hthm{disc} @{text "[simp]"}\rm:] ~ \\
781 @{thm list.disc(1)[no_vars]} \\
782 @{thm list.disc(2)[no_vars]}
784 \item[@{text "t."}\hthm{discI}\rm:] ~ \\
785 @{thm list.discI(1)[no_vars]} \\
786 @{thm list.discI(2)[no_vars]}
788 \item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
789 @{thm list.sel(1)[no_vars]} \\
790 @{thm list.sel(2)[no_vars]}
792 \item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
793 @{thm list.collapse(1)[no_vars]} \\
794 @{thm list.collapse(2)[no_vars]}
796 \item[@{text "t."}\hthm{disc\_exclude} @{text "[dest]"}\rm:] ~ \\
797 These properties are missing for @{typ "'a list"} because there is only one
798 proper discriminator. Had the datatype been introduced with a second
799 discriminator called @{const nonnull}, they would have read thusly: \\[\jot]
800 @{prop "null list \<Longrightarrow> \<not> nonnull list"} \\
801 @{prop "nonnull list \<Longrightarrow> \<not> null list"}
803 \item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
804 @{thm list.disc_exhaust[no_vars]}
806 \item[@{text "t."}\hthm{sel\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
807 @{thm list.sel_exhaust[no_vars]}
809 \item[@{text "t."}\hthm{expand}\rm:] ~ \\
810 @{thm list.expand[no_vars]}
812 \item[@{text "t."}\hthm{sel\_split}\rm:] ~ \\
813 @{thm list.sel_split[no_vars]}
815 \item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\
816 @{thm list.sel_split_asm[no_vars]}
818 \item[@{text "t."}\hthm{case\_eq\_if}\rm:] ~ \\
819 @{thm list.case_eq_if[no_vars]}
825 In addition, equational versions of @{text t.disc} are registered with the @{text "[code]"}
830 subsubsection {* Functorial Theorems
831 \label{sssec:functorial-theorems} *}
834 The functorial theorems are partitioned in two subgroups. The first subgroup
835 consists of properties involving the constructors and either a set function, the
836 map function, or the relator:
841 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
842 @{thm list.set(1)[no_vars]} \\
843 @{thm list.set(2)[no_vars]}
845 \item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
846 @{thm list.map(1)[no_vars]} \\
847 @{thm list.map(2)[no_vars]}
849 \item[@{text "t."}\hthm{rel\_inject} @{text "[simp]"}\rm:] ~ \\
850 @{thm list.rel_inject(1)[no_vars]} \\
851 @{thm list.rel_inject(2)[no_vars]}
853 \item[@{text "t."}\hthm{rel\_distinct} @{text "[simp]"}\rm:] ~ \\
854 @{thm list.rel_distinct(1)[no_vars]} \\
855 @{thm list.rel_distinct(2)[no_vars]}
861 In addition, equational versions of @{text t.rel_inject} and @{text
862 rel_distinct} are registered with the @{text "[code]"} attribute.
864 The second subgroup consists of more abstract properties of the set functions,
865 the map function, and the relator:
870 \item[@{text "t."}\hthm{map\_comp}\rm:] ~ \\
871 @{thm list.map_cong0[no_vars]}
873 \item[@{text "t."}\hthm{map\_cong} @{text "[fundef_cong]"}\rm:] ~ \\
874 @{thm list.map_cong[no_vars]}
876 \item[@{text "t."}\hthm{map\_id}\rm:] ~ \\
877 @{thm list.map_id[no_vars]}
879 \item[@{text "t."}\hthm{rel\_compp}\rm:] ~ \\
880 @{thm list.rel_compp[no_vars]}
882 \item[@{text "t."}\hthm{rel\_conversep}\rm:] ~ \\
883 @{thm list.rel_conversep[no_vars]}
885 \item[@{text "t."}\hthm{rel\_eq}\rm:] ~ \\
886 @{thm list.rel_eq[no_vars]}
888 \item[@{text "t."}\hthm{rel\_flip}\rm:] ~ \\
889 @{thm list.rel_flip[no_vars]}
891 \item[@{text "t."}\hthm{rel\_mono}\rm:] ~ \\
892 @{thm list.rel_mono[no_vars]}
894 \item[@{text "t."}\hthm{set\_map}\rm:] ~ \\
895 @{thm list.set_map[no_vars]}
902 subsubsection {* Inductive Theorems
903 \label{sssec:inductive-theorems} *}
906 The inductive theorems are as follows:
911 \item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
912 @{thm list.induct[no_vars]}
914 \item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
915 Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
916 prove $m$ properties simultaneously.
918 \item[@{text "t."}\hthm{fold} @{text "[simp, code]"}\rm:] ~ \\
919 @{thm list.fold(1)[no_vars]} \\
920 @{thm list.fold(2)[no_vars]}
922 \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
923 @{thm list.rec(1)[no_vars]} \\
924 @{thm list.rec(2)[no_vars]}
930 For convenience, @{command datatype_new} also provides the following collection:
935 \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\
936 @{text t.rel_distinct} @{text t.set}
943 subsection {* Compatibility Issues
944 \label{ssec:datatype-compatibility-issues} *}
947 The command @{command datatype_new} has been designed to be highly compatible
948 with the old \keyw{datatype}, to ease migration. There are nonetheless a few
949 incompatibilities that may arise when porting to the new package:
952 \setlength{\itemsep}{0pt}
954 \item \emph{The Standard ML interfaces are different.} Tools and extensions
955 written to call the old ML interfaces will need to be adapted to the new
956 interfaces. Little has been done so far in this direction. Whenever possible, it
957 is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype}
958 to register new-style datatypes as old-style datatypes.
960 \item \emph{The constants @{text t_case} and @{text t_rec} are now called
961 @{text case_t} and @{text rec_t}.}
963 \item \emph{The recursor @{text rec_t} has a different signature for nested
964 recursive datatypes.} In the old package, nested recursion through non-functions
965 was internally reduced to mutual recursion. This reduction was visible in the
966 type of the recursor, used by \keyw{primrec}. Recursion through functions was
967 handled specially. In the new package, nested recursion (for functions and
968 non-functions) is handled in a more modular fashion. The old-style recursor can
969 be generated on demand using @{command primrec_new}, as explained in
970 Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
973 \item \emph{Accordingly, the induction rule is different for nested recursive
974 datatypes.} Again, the old-style induction rule can be generated on demand using
975 @{command primrec_new}, as explained in
976 Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
979 \item \emph{The internal constructions are completely different.} Proof texts
980 that unfold the definition of constants introduced by \keyw{datatype} will be
983 \item \emph{A few theorems have different names.}
984 The properties @{text t.cases} and @{text t.recs} have been renamed
985 @{text t.case} and @{text t.rec}. For non-mutually recursive datatypes,
986 @{text t.inducts} is available as @{text t.induct}.
987 For $m > 1$ mutually recursive datatypes,
988 @{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
989 @{text "t\<^sub>i.induct"}.
991 \item \emph{The @{text t.simps} collection has been extended.}
992 Previously available theorems are available at the same index.
994 \item \emph{Variables in generated properties have different names.} This is
995 rarely an issue, except in proof texts that refer to variable names in the
996 @{text "[where \<dots>]"} attribute. The solution is to use the more robust
997 @{text "[of \<dots>]"} syntax.
1000 In the other direction, there is currently no way to register old-style
1001 datatypes as new-style datatypes. If the goal is to define new-style datatypes
1002 with nested recursion through old-style datatypes, the old-style
1003 datatypes can be registered as a BNF
1004 (Section~\ref{sec:registering-bounded-natural-functors}). If the goal is
1005 to derive discriminators and selectors, this can be achieved using @{command
1006 wrap_free_constructors}
1007 (Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
1011 section {* Defining Recursive Functions
1012 \label{sec:defining-recursive-functions} *}
1015 Recursive functions over datatypes can be specified using the @{command
1016 primrec_new} command, which supports primitive recursion, or using the more
1017 general \keyw{fun} and \keyw{function} commands. Here, the focus is on @{command
1018 primrec_new}; the other two commands are described in a separate tutorial
1019 \cite{isabelle-function}.
1021 %%% TODO: partial_function
1025 subsection {* Introductory Examples
1026 \label{ssec:primrec-introductory-examples} *}
1029 Primitive recursion is illustrated through concrete examples based on the
1030 datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
1031 examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|.
1035 subsubsection {* Nonrecursive Types
1036 \label{sssec:primrec-nonrecursive-types} *}
1039 Primitive recursion removes one layer of constructors on the left-hand side in
1040 each equation. For example:
1043 primrec_new bool_of_trool :: "trool \<Rightarrow> bool" where
1044 "bool_of_trool Faalse \<longleftrightarrow> False" |
1045 "bool_of_trool Truue \<longleftrightarrow> True"
1047 text {* \blankline *}
1049 primrec_new the_list :: "'a option \<Rightarrow> 'a list" where
1050 "the_list None = []" |
1051 "the_list (Some a) = [a]"
1053 text {* \blankline *}
1055 primrec_new the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
1056 "the_default d None = d" |
1057 "the_default _ (Some a) = a"
1059 text {* \blankline *}
1061 primrec_new mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
1062 "mirrror (Triple a b c) = Triple c b a"
1066 The equations can be specified in any order, and it is acceptable to leave out
1067 some cases, which are then unspecified. Pattern matching on the left-hand side
1068 is restricted to a single datatype, which must correspond to the same argument
1073 subsubsection {* Simple Recursion
1074 \label{sssec:primrec-simple-recursion} *}
1077 For simple recursive types, recursive calls on a constructor argument are
1078 allowed on the right-hand side:
1081 primrec_new replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
1082 "replicate Zero _ = []" |
1083 "replicate (Suc n) x = x # replicate n x"
1085 text {* \blankline *}
1087 primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
1090 Zero \<Rightarrow> x
1091 | Suc j' \<Rightarrow> at xs j')"
1093 text {* \blankline *}
1095 primrec_new (*<*)(in early) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
1096 "tfold _ (TNil y) = y" |
1097 "tfold f (TCons x xs) = f x (tfold f xs)"
1101 Pattern matching is only available for the argument on which the recursion takes
1102 place. Fortunately, it is easy to generate pattern-maching equations using the
1103 \keyw{simps\_of\_case} command provided by the theory
1104 \verb|~~/src/HOL/Library/Simps_Case_Conv|.
1107 simps_of_case at_simps: at.simps
1110 This generates the lemma collection @{thm [source] at_simps}:
1112 \[@{thm at_simps(1)[no_vars]}
1113 \qquad @{thm at_simps(2)[no_vars]}\]
1115 The next example is defined using \keyw{fun} to escape the syntactic
1116 restrictions imposed on primitive recursive functions. The
1117 @{command datatype_new_compat} command is needed to register new-style datatypes
1118 for use with \keyw{fun} and \keyw{function}
1119 (Section~\ref{sssec:datatype-new-compat}):
1122 datatype_new_compat nat
1124 text {* \blankline *}
1126 fun at_least_two :: "nat \<Rightarrow> bool" where
1127 "at_least_two (Suc (Suc _)) \<longleftrightarrow> True" |
1128 "at_least_two _ \<longleftrightarrow> False"
1131 subsubsection {* Mutual Recursion
1132 \label{sssec:primrec-mutual-recursion} *}
1135 The syntax for mutually recursive functions over mutually recursive datatypes
1140 nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
1141 nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
1143 "nat_of_even_nat Even_Zero = Zero" |
1144 "nat_of_even_nat (Even_Suc n) = Suc (nat_of_odd_nat n)" |
1145 "nat_of_odd_nat (Odd_Suc n) = Suc (nat_of_even_nat n)"
1147 text {* \blankline *}
1150 eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
1151 eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and
1152 eval\<^sub>f :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) fct \<Rightarrow> int"
1154 "eval\<^sub>e \<gamma> \<xi> (Term t) = eval\<^sub>t \<gamma> \<xi> t" |
1155 "eval\<^sub>e \<gamma> \<xi> (Sum t e) = eval\<^sub>t \<gamma> \<xi> t + eval\<^sub>e \<gamma> \<xi> e" |
1156 "eval\<^sub>t \<gamma> \<xi> (Factor f) = eval\<^sub>f \<gamma> \<xi> f" |
1157 "eval\<^sub>t \<gamma> \<xi> (Prod f t) = eval\<^sub>f \<gamma> \<xi> f + eval\<^sub>t \<gamma> \<xi> t" |
1158 "eval\<^sub>f \<gamma> _ (Const a) = \<gamma> a" |
1159 "eval\<^sub>f _ \<xi> (Var b) = \<xi> b" |
1160 "eval\<^sub>f \<gamma> \<xi> (Expr e) = eval\<^sub>e \<gamma> \<xi> e"
1164 Mutual recursion is possible within a single type, using \keyw{fun}:
1168 even :: "nat \<Rightarrow> bool" and
1169 odd :: "nat \<Rightarrow> bool"
1171 "even Zero = True" |
1172 "even (Suc n) = odd n" |
1173 "odd Zero = False" |
1174 "odd (Suc n) = even n"
1177 subsubsection {* Nested Recursion
1178 \label{sssec:primrec-nested-recursion} *}
1181 In a departure from the old datatype package, nested recursion is normally
1182 handled via the map functions of the nesting type constructors. For example,
1183 recursive calls are lifted to lists using @{const map}:
1187 datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f (lbl\<^sub>f\<^sub>f: 'a) (sub\<^sub>f\<^sub>f: "'a tree\<^sub>f\<^sub>f list")
1189 primrec_new at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
1190 "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
1193 | j # js' \<Rightarrow> at (map (\<lambda>t. at\<^sub>f\<^sub>f t js') ts) j)"
1197 The next example features recursion through the @{text option} type. Although
1198 @{text option} is not a new-style datatype, it is registered as a BNF with the
1199 map function @{const map_option}:
1202 primrec_new (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
1203 "sum_btree (BNode a lt rt) =
1204 a + the_default 0 (map_option sum_btree lt) +
1205 the_default 0 (map_option sum_btree rt)"
1209 The same principle applies for arbitrary type constructors through which
1210 recursion is possible. Notably, the map function for the function type
1211 (@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
1214 primrec_new (*<*)(in early) (*>*)relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
1215 "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
1216 "relabel_ft f (FTNode g) = FTNode (relabel_ft f \<circ> g)"
1220 For convenience, recursion through functions can also be expressed using
1221 $\lambda$-abstractions and function application rather than through composition.
1225 primrec_new relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
1226 "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
1227 "relabel_ft f (FTNode g) = FTNode (\<lambda>x. relabel_ft f (g x))"
1229 text {* \blankline *}
1231 primrec_new subtree_ft :: "'a \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
1232 "subtree_ft x (FTNode g) = g x"
1236 For recursion through curried $n$-ary functions, $n$ applications of
1237 @{term "op \<circ>"} are necessary. The examples below illustrate the case where
1241 datatype_new 'a ftree2 = FTLeaf2 'a | FTNode2 "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2"
1243 text {* \blankline *}
1245 primrec_new (*<*)(in early) (*>*)relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
1246 "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)" |
1247 "relabel_ft2 f (FTNode2 g) = FTNode2 (op \<circ> (op \<circ> (relabel_ft2 f)) g)"
1249 text {* \blankline *}
1251 primrec_new relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
1252 "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)" |
1253 "relabel_ft2 f (FTNode2 g) = FTNode2 (\<lambda>x y. relabel_ft2 f (g x y))"
1255 text {* \blankline *}
1257 primrec_new subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
1258 "subtree_ft2 x y (FTNode2 g) = g x y"
1261 subsubsection {* Nested-as-Mutual Recursion
1262 \label{sssec:primrec-nested-as-mutual-recursion} *}
1269 For compatibility with the old package, but also because it is sometimes
1270 convenient in its own right, it is possible to treat nested recursive datatypes
1271 as mutually recursive ones if the recursion takes place though new-style
1272 datatypes. For example:
1276 at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" and
1277 ats\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a"
1279 "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
1282 | j # js' \<Rightarrow> ats\<^sub>f\<^sub>f ts j js')" |
1283 "ats\<^sub>f\<^sub>f (t # ts) j =
1285 Zero \<Rightarrow> at\<^sub>f\<^sub>f t
1286 | Suc j' \<Rightarrow> ats\<^sub>f\<^sub>f ts j')"
1290 Appropriate induction rules are generated as
1291 @{thm [source] at\<^sub>f\<^sub>f.induct},
1292 @{thm [source] ats\<^sub>f\<^sub>f.induct}, and
1293 @{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}. The
1294 induction rules and the underlying recursors are generated on a per-need basis
1295 and are kept in a cache to speed up subsequent definitions.
1297 Here is a second example:
1301 sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" and
1302 sum_btree_option :: "'a btree option \<Rightarrow> 'a"
1304 "sum_btree (BNode a lt rt) =
1305 a + sum_btree_option lt + sum_btree_option rt" |
1306 "sum_btree_option None = 0" |
1307 "sum_btree_option (Some t) = sum_btree t"
1310 % * can pretend a nested type is mutually recursive (if purely inductive)
1311 % * avoids the higher-order map
1314 % * this can always be avoided;
1315 % * e.g. in our previous example, we first mapped the recursive
1316 % calls, then we used a generic at function to retrieve the result
1318 % * there's no hard-and-fast rule of when to use one or the other,
1319 % just like there's no rule when to use fold and when to use
1322 % * higher-order approach, considering nesting as nesting, is more
1323 % compositional -- e.g. we saw how we could reuse an existing polymorphic
1324 % at or the_default, whereas @{const ats\<^sub>f\<^sub>f} is much more specific
1327 % * is perhaps less intuitive, because it requires higher-order thinking
1328 % * may seem inefficient, and indeed with the code generator the
1329 % mutually recursive version might be nicer
1330 % * is somewhat indirect -- must apply a map first, then compute a result
1332 % * the auxiliary functions like @{const ats\<^sub>f\<^sub>f} are sometimes useful in own right
1334 % * impact on automation unclear
1342 subsection {* Command Syntax
1343 \label{ssec:primrec-command-syntax} *}
1346 subsubsection {* \keyw{primrec\_new}
1347 \label{sssec:primrec-new} *}
1350 \begin{matharray}{rcl}
1351 @{command_def "primrec_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
1355 @@{command primrec_new} target? fixes \\ @'where' (@{syntax pr_equation} + '|')
1357 @{syntax_def pr_equation}: thmdecl? prop
1363 subsection {* Generated Theorems
1364 \label{ssec:primrec-generated-theorems} *}
1367 % * synthesized nonrecursive definition
1368 % * user specification is rederived from it, exactly as entered
1372 % * without some needless induction hypotheses if not used
1379 subsection {* Recursive Default Values for Selectors
1380 \label{ssec:primrec-recursive-default-values-for-selectors} *}
1383 A datatype selector @{text un_D} can have a default value for each constructor
1384 on which it is not otherwise specified. Occasionally, it is useful to have the
1385 default value be defined recursively. This produces a chicken-and-egg situation
1386 that may seem unsolvable, because the datatype is not introduced yet at the
1387 moment when the selectors are introduced. Of course, we can always define the
1388 selectors manually afterward, but we then have to state and prove all the
1389 characteristic theorems ourselves instead of letting the package do it.
1391 Fortunately, there is a fairly elegant workaround that relies on overloading and
1392 that avoids the tedium of manual derivations:
1395 \setlength{\itemsep}{0pt}
1398 Introduce a fully unspecified constant @{text "un_D\<^sub>0 \<Colon> 'a"} using
1402 Define the datatype, specifying @{text "un_D\<^sub>0"} as the selector's default
1406 Define the behavior of @{text "un_D\<^sub>0"} on values of the newly introduced
1407 datatype using the \keyw{overloading} command.
1410 Derive the desired equation on @{text un_D} from the characteristic equations
1411 for @{text "un_D\<^sub>0"}.
1415 The following example illustrates this procedure:
1418 consts termi\<^sub>0 :: 'a
1420 text {* \blankline *}
1422 datatype_new ('a, 'b) tlist =
1423 TNil (termi: 'b) (defaults ttl: TNil)
1424 | TCons (thd: 'a) (ttl : "('a, 'b) tlist") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs")
1426 text {* \blankline *}
1429 termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist \<Rightarrow> 'b"
1431 primrec_new termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
1432 "termi\<^sub>0 (TNil y) = y" |
1433 "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
1436 text {* \blankline *}
1438 lemma terminal_TCons[simp]: "termi (TCons x xs) = termi xs"
1442 subsection {* Compatibility Issues
1443 \label{ssec:primrec-compatibility-issues} *}
1446 The command @{command primrec_new} has been designed to be highly compatible
1447 with the old \keyw{primrec}, to ease migration. There is nonetheless at least
1448 one incompatibility that may arise when porting to the new package:
1451 \setlength{\itemsep}{0pt}
1453 \item \emph{Some theorems have different names.}
1454 For $m > 1$ mutually recursive functions,
1455 @{text "f\<^sub>1_\<dots>_f\<^sub>m.simps"} has been broken down into separate
1456 subcollections @{text "f\<^sub>i.simps"}.
1461 section {* Defining Codatatypes
1462 \label{sec:defining-codatatypes} *}
1465 Codatatypes can be specified using the @{command codatatype} command. The
1466 command is first illustrated through concrete examples featuring different
1467 flavors of corecursion. More examples can be found in the directory
1468 \verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|. The
1469 \emph{Archive of Formal Proofs} also includes some useful codatatypes, notably
1470 for lazy lists \cite{lochbihler-2010}.
1474 subsection {* Introductory Examples
1475 \label{ssec:codatatype-introductory-examples} *}
1478 subsubsection {* Simple Corecursion
1479 \label{sssec:codatatype-simple-corecursion} *}
1482 Noncorecursive codatatypes coincide with the corresponding datatypes, so they
1483 are useless in practice. \emph{Corecursive codatatypes} have the same syntax
1484 as recursive datatypes, except for the command name. For example, here is the
1485 definition of lazy lists:
1488 codatatype (lset: 'a) llist (map: lmap rel: llist_all2) =
1489 lnull: LNil (defaults ltl: LNil)
1490 | LCons (lhd: 'a) (ltl: "'a llist")
1494 Lazy lists can be infinite, such as @{text "LCons 0 (LCons 0 (\<dots>))"} and
1495 @{text "LCons 0 (LCons 1 (LCons 2 (\<dots>)))"}. Here is a related type, that of
1499 codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
1500 SCons (shd: 'a) (stl: "'a stream")
1504 Another interesting type that can
1505 be defined as a codatatype is that of the extended natural numbers:
1508 codatatype enat = EZero | ESuc enat
1512 This type has exactly one infinite element, @{text "ESuc (ESuc (ESuc (\<dots>)))"},
1513 that represents $\infty$. In addition, it has finite values of the form
1514 @{text "ESuc (\<dots> (ESuc EZero)\<dots>)"}.
1516 Here is an example with many constructors:
1519 codatatype 'a process =
1521 | Skip (cont: "'a process")
1522 | Action (prefix: 'a) (cont: "'a process")
1523 | Choice (left: "'a process") (right: "'a process")
1527 Notice that the @{const cont} selector is associated with both @{const Skip}
1528 and @{const Action}.
1532 subsubsection {* Mutual Corecursion
1533 \label{sssec:codatatype-mutual-corecursion} *}
1537 The example below introduces a pair of \emph{mutually corecursive} types:
1540 codatatype even_enat = Even_EZero | Even_ESuc odd_enat
1541 and odd_enat = Odd_ESuc even_enat
1544 subsubsection {* Nested Corecursion
1545 \label{sssec:codatatype-nested-corecursion} *}
1549 The next examples feature \emph{nested corecursion}:
1552 codatatype 'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i (lbl\<^sub>i\<^sub>i: 'a) (sub\<^sub>i\<^sub>i: "'a tree\<^sub>i\<^sub>i llist")
1554 text {* \blankline *}
1556 codatatype 'a tree\<^sub>i\<^sub>s = Node\<^sub>i\<^sub>s (lbl\<^sub>i\<^sub>s: 'a) (sub\<^sub>i\<^sub>s: "'a tree\<^sub>i\<^sub>s fset")
1558 text {* \blankline *}
1560 codatatype 'a state_machine =
1561 State_Machine (accept: bool) (trans: "'a \<Rightarrow> 'a state_machine")
1564 subsection {* Command Syntax
1565 \label{ssec:codatatype-command-syntax} *}
1568 subsubsection {* \keyw{codatatype}
1569 \label{sssec:codatatype} *}
1572 \begin{matharray}{rcl}
1573 @{command_def "codatatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
1577 @@{command codatatype} target? \\
1578 (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
1582 Definitions of codatatypes have almost exactly the same syntax as for datatypes
1583 (Section~\ref{ssec:datatype-command-syntax}). The @{text "no_discs_sels"} option
1584 is not available, because destructors are a crucial notion for codatatypes.
1588 subsection {* Generated Constants
1589 \label{ssec:codatatype-generated-constants} *}
1592 Given a codatatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
1593 with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
1594 \ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
1595 datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
1596 iterator and the recursor are replaced by dual concepts:
1599 \setlength{\itemsep}{0pt}
1601 \item \relax{Coiterator}: @{text unfold_t}
1603 \item \relax{Corecursor}: @{text corec_t}
1609 subsection {* Generated Theorems
1610 \label{ssec:codatatype-generated-theorems} *}
1613 The characteristic theorems generated by @{command codatatype} are grouped in
1614 three broad categories:
1617 \setlength{\itemsep}{0pt}
1619 \item The \emph{free constructor theorems} are properties about the constructors
1620 and destructors that can be derived for any freely generated type.
1622 \item The \emph{functorial theorems} are properties of datatypes related to
1625 \item The \emph{coinductive theorems} are properties of datatypes related to
1626 their coinductive nature.
1630 The first two categories are exactly as for datatypes and are described in
1632 \ref{sssec:free-constructor-theorems}~and~\ref{sssec:functorial-theorems}.
1636 subsubsection {* Coinductive Theorems
1637 \label{sssec:coinductive-theorems} *}
1640 The coinductive theorems are listed below for @{typ "'a llist"}:
1645 \item[\begin{tabular}{@ {}l@ {}}
1646 @{text "t."}\hthm{coinduct} @{text "[coinduct t, consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
1647 \phantom{@{text "t."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
1649 @{thm llist.coinduct[no_vars]}
1651 \item[\begin{tabular}{@ {}l@ {}}
1652 @{text "t."}\hthm{strong\_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
1653 \phantom{@{text "t."}\hthm{strong\_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
1655 @{thm llist.strong_coinduct[no_vars]}
1657 \item[\begin{tabular}{@ {}l@ {}}
1658 @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m, case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"} \\
1659 @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong\_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
1660 \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong\_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
1662 Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be
1663 used to prove $m$ properties simultaneously.
1665 \item[@{text "t."}\hthm{unfold}\rm:] ~ \\
1666 @{thm llist.unfold(1)[no_vars]} \\
1667 @{thm llist.unfold(2)[no_vars]}
1669 \item[@{text "t."}\hthm{corec}\rm:] ~ \\
1670 @{thm llist.corec(1)[no_vars]} \\
1671 @{thm llist.corec(2)[no_vars]}
1673 \item[@{text "t."}\hthm{disc\_unfold}\rm:] ~ \\
1674 @{thm llist.disc_unfold(1)[no_vars]} \\
1675 @{thm llist.disc_unfold(2)[no_vars]}
1677 \item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\
1678 @{thm llist.disc_corec(1)[no_vars]} \\
1679 @{thm llist.disc_corec(2)[no_vars]}
1681 \item[@{text "t."}\hthm{disc\_unfold\_iff} @{text "[simp]"}\rm:] ~ \\
1682 @{thm llist.disc_unfold_iff(1)[no_vars]} \\
1683 @{thm llist.disc_unfold_iff(2)[no_vars]}
1685 \item[@{text "t."}\hthm{disc\_corec\_iff} @{text "[simp]"}\rm:] ~ \\
1686 @{thm llist.disc_corec_iff(1)[no_vars]} \\
1687 @{thm llist.disc_corec_iff(2)[no_vars]}
1689 \item[@{text "t."}\hthm{sel\_unfold} @{text "[simp]"}\rm:] ~ \\
1690 @{thm llist.sel_unfold(1)[no_vars]} \\
1691 @{thm llist.sel_unfold(2)[no_vars]}
1693 \item[@{text "t."}\hthm{sel\_corec} @{text "[simp]"}\rm:] ~ \\
1694 @{thm llist.sel_corec(1)[no_vars]} \\
1695 @{thm llist.sel_corec(2)[no_vars]}
1701 For convenience, @{command codatatype} also provides the following collection:
1706 \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec} @{text t.disc_corec_iff}] ~ \\
1707 @{text t.sel_corec} @{text t.disc_unfold} @{text t.disc_unfold_iff} @{text t.sel_unfold} @{text t.map} \\
1708 @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
1715 section {* Defining Corecursive Functions
1716 \label{sec:defining-corecursive-functions} *}
1719 Corecursive functions can be specified using the @{command primcorec} and
1720 \keyw{prim\-corec\-ursive} commands, which support primitive corecursion, or
1721 using the more general \keyw{partial\_function} command. Here, the focus is on
1722 the first two. More examples can be found in the directory
1723 \verb|~~/src/HOL/BNF/Examples|.
1725 Whereas recursive functions consume datatypes one constructor at a time,
1726 corecursive functions construct codatatypes one constructor at a time.
1727 Partly reflecting a lack of agreement among proponents of coalgebraic methods,
1728 Isabelle supports three competing syntaxes for specifying a function $f$:
1731 \setlength{\itemsep}{0pt}
1733 \abovedisplayskip=.5\abovedisplayskip
1734 \belowdisplayskip=.5\belowdisplayskip
1736 \item The \emph{destructor view} specifies $f$ by implications of the form
1737 \[@{text "\<dots> \<Longrightarrow> is_C\<^sub>j (f x\<^sub>1 \<dots> x\<^sub>n)"}\] and
1738 equations of the form
1739 \[@{text "un_C\<^sub>ji (f x\<^sub>1 \<dots> x\<^sub>n) = \<dots>"}\]
1740 This style is popular in the coalgebraic literature.
1742 \item The \emph{constructor view} specifies $f$ by equations of the form
1743 \[@{text "\<dots> \<Longrightarrow> f x\<^sub>1 \<dots> x\<^sub>n = C\<^sub>j \<dots>"}\]
1744 This style is often more concise than the previous one.
1746 \item The \emph{code view} specifies $f$ by a single equation of the form
1747 \[@{text "f x\<^sub>1 \<dots> x\<^sub>n = \<dots>"}\]
1748 with restrictions on the format of the right-hand side. Lazy functional
1749 programming languages such as Haskell support a generalized version of this
1753 All three styles are available as input syntax. Whichever syntax is chosen,
1754 characteristic theorems for all three styles are generated.
1756 %%% TODO: partial_function? E.g. for defining tail recursive function on lazy
1757 %%% lists (cf. terminal0 in TLList.thy)
1761 subsection {* Introductory Examples
1762 \label{ssec:primcorec-introductory-examples} *}
1765 Primitive corecursion is illustrated through concrete examples based on the
1766 codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
1767 examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|. The code
1768 view is favored in the examples below. Sections
1769 \ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
1770 present the same examples expressed using the constructor and destructor views.
1773 subsubsection {* Simple Corecursion
1774 \label{sssec:primcorec-simple-corecursion} *}
1777 Following the code view, corecursive calls are allowed on the right-hand side as
1778 long as they occur under a constructor, which itself appears either directly to
1779 the right of the equal sign or in a conditional expression:
1782 primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
1783 "literate g x = LCons x (literate g (g x))"
1785 text {* \blankline *}
1787 primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
1788 "siterate g x = SCons x (siterate g (g x))"
1792 The constructor ensures that progress is made---i.e., the function is
1793 \emph{productive}. The above functions compute the infinite lazy list or stream
1794 @{text "[x, g x, g (g x), \<dots>]"}. Productivity guarantees that prefixes
1795 @{text "[x, g x, g (g x), \<dots>, (g ^^ k) x]"} of arbitrary finite length
1796 @{text k} can be computed by unfolding the code equation a finite number of
1799 Corecursive functions construct codatatype values, but nothing prevents them
1800 from also consuming such values. The following function drops every second
1801 element in a stream:
1804 primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
1805 "every_snd s = SCons (shd s) (stl (stl s))"
1809 Constructs such as @{text "let"}---@{text "in"}, @{text
1810 "if"}---@{text "then"}---@{text "else"}, and @{text "case"}---@{text "of"} may
1811 appear around constructors that guard corecursive calls:
1814 primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
1817 LNil \<Rightarrow> ys
1818 | LCons x xs' \<Rightarrow> LCons x (lappend xs' ys))"
1822 Pattern matching is not supported by @{command primcorec}. Fortunately, it is
1823 easy to generate pattern-maching equations using the \keyw{simps\_of\_case}
1824 command provided by the theory \verb|~~/src/HOL/Library/Simps_Case_Conv|.
1827 simps_of_case lappend_simps: lappend.code
1830 This generates the lemma collection @{thm [source] lappend_simps}:
1832 \[@{thm lappend_simps(1)[no_vars]}
1833 \qquad @{thm lappend_simps(2)[no_vars]}\]
1835 Corecursion is useful to specify not only functions but also infinite objects:
1838 primcorec infty :: enat where
1839 "infty = ESuc infty"
1843 The example below constructs a pseudorandom process value. It takes a stream of
1844 actions (@{text s}), a pseudorandom function generator (@{text f}), and a
1845 pseudorandom seed (@{text n}):
1849 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
1851 "random_process s f n =
1852 (if n mod 4 = 0 then
1854 else if n mod 4 = 1 then
1855 Skip (random_process s f (f n))
1856 else if n mod 4 = 2 then
1857 Action (shd s) (random_process (stl s) f (f n))
1859 Choice (random_process (every_snd s) (f \<circ> f) (f n))
1860 (random_process (every_snd (stl s)) (f \<circ> f) (f (f n))))"
1864 The main disadvantage of the code view is that the conditions are tested
1865 sequentially. This is visible in the generated theorems. The constructor and
1866 destructor views offer nonsequential alternatives.
1870 subsubsection {* Mutual Corecursion
1871 \label{sssec:primcorec-mutual-corecursion} *}
1874 The syntax for mutually corecursive functions over mutually corecursive
1875 datatypes is unsurprising:
1879 even_infty :: even_enat and
1880 odd_infty :: odd_enat
1882 "even_infty = Even_ESuc odd_infty" |
1883 "odd_infty = Odd_ESuc even_infty"
1886 subsubsection {* Nested Corecursion
1887 \label{sssec:primcorec-nested-corecursion} *}
1890 The next pair of examples generalize the @{const literate} and @{const siterate}
1891 functions (Section~\ref{sssec:primcorec-nested-corecursion}) to possibly
1892 infinite trees in which subnodes are organized either as a lazy list (@{text
1893 tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}). They rely on the map functions of
1894 the nesting type constructors to lift the corecursive calls:
1897 primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
1898 "iterate\<^sub>i\<^sub>i g x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i g) (g x))"
1900 text {* \blankline *}
1902 primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
1903 "iterate\<^sub>i\<^sub>s g x = Node\<^sub>i\<^sub>s x (fimage (iterate\<^sub>i\<^sub>s g) (g x))"
1907 Both examples follow the usual format for constructor arguments associated
1908 with nested recursive occurrences of the datatype. Consider
1909 @{const iterate\<^sub>i\<^sub>i}. The term @{term "g x"} constructs an @{typ "'a llist"}
1910 value, which is turned into an @{typ "'a tree\<^sub>i\<^sub>i llist"} value using
1913 This format may sometimes feel artificial. The following function constructs
1914 a tree with a single, infinite branch from a stream:
1917 primcorec tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
1918 "tree\<^sub>i\<^sub>i_of_stream s =
1919 Node\<^sub>i\<^sub>i (shd s) (lmap tree\<^sub>i\<^sub>i_of_stream (LCons (stl s) LNil))"
1923 Fortunately, it is easy to prove the following lemma, where the corecursive call
1924 is moved inside the lazy list constructor, thereby eliminating the need for
1928 lemma tree\<^sub>i\<^sub>i_of_stream_alt:
1929 "tree\<^sub>i\<^sub>i_of_stream s = Node\<^sub>i\<^sub>i (shd s) (LCons (tree\<^sub>i\<^sub>i_of_stream (stl s)) LNil)"
1930 by (subst tree\<^sub>i\<^sub>i_of_stream.code) simp
1933 The next example illustrates corecursion through functions, which is a bit
1934 special. Deterministic finite automata (DFAs) are traditionally defined as
1935 5-tuples @{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,
1936 @{text \<Sigma>} is a finite alphabet, @{text \<delta>} is a transition function, @{text q\<^sub>0}
1937 is an initial state, and @{text F} is a set of final states. The following
1938 function translates a DFA into a @{type state_machine}:
1942 (*<*)(in early) (*>*)sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
1944 "sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (sm_of_dfa \<delta> F \<circ> \<delta> q)"
1948 The map function for the function type (@{text \<Rightarrow>}) is composition
1949 (@{text "op \<circ>"}). For convenience, corecursion through functions can
1950 also be expressed using $\lambda$-abstractions and function application rather
1951 than through composition. For example:
1955 sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
1957 "sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (\<lambda>a. sm_of_dfa \<delta> F (\<delta> q a))"
1959 text {* \blankline *}
1961 primcorec empty_sm :: "'a state_machine" where
1962 "empty_sm = State_Machine False (\<lambda>_. empty_sm)"
1964 text {* \blankline *}
1966 primcorec not_sm :: "'a state_machine \<Rightarrow> 'a state_machine" where
1967 "not_sm M = State_Machine (\<not> accept M) (\<lambda>a. not_sm (trans M a))"
1969 text {* \blankline *}
1972 or_sm :: "'a state_machine \<Rightarrow> 'a state_machine \<Rightarrow> 'a state_machine"
1974 "or_sm M N = State_Machine (accept M \<or> accept N)
1975 (\<lambda>a. or_sm (trans M a) (trans N a))"
1979 For recursion through curried $n$-ary functions, $n$ applications of
1980 @{term "op \<circ>"} are necessary. The examples below illustrate the case where
1984 codatatype ('a, 'b) state_machine2 =
1985 State_Machine2 (accept2: bool) (trans2: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) state_machine2")
1987 text {* \blankline *}
1990 (*<*)(in early) (*>*)sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) state_machine2"
1992 "sm2_of_dfa \<delta> F q = State_Machine2 (q \<in> F) (op \<circ> (op \<circ> (sm2_of_dfa \<delta> F)) (\<delta> q))"
1994 text {* \blankline *}
1997 sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) state_machine2"
1999 "sm2_of_dfa \<delta> F q = State_Machine2 (q \<in> F) (\<lambda>a b. sm2_of_dfa \<delta> F (\<delta> q a b))"
2002 subsubsection {* Nested-as-Mutual Corecursion
2003 \label{sssec:primcorec-nested-as-mutual-corecursion} *}
2006 Just as it is possible to recurse over nested recursive datatypes as if they
2007 were mutually recursive
2008 (Section~\ref{sssec:primrec-nested-as-mutual-recursion}), it is possible to
2009 pretend that nested codatatypes are mutually corecursive. For example:
2017 iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" and
2018 iterates\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a llist \<Rightarrow> 'a tree\<^sub>i\<^sub>i llist"
2020 "iterate\<^sub>i\<^sub>i g x = Node\<^sub>i\<^sub>i x (iterates\<^sub>i\<^sub>i g (g x))" |
2021 "iterates\<^sub>i\<^sub>i g xs =
2023 LNil \<Rightarrow> LNil
2024 | LCons x xs' \<Rightarrow> LCons (iterate\<^sub>i\<^sub>i g x) (iterates\<^sub>i\<^sub>i g xs'))"
2028 Coinduction rules are generated as
2029 @{thm [source] iterate\<^sub>i\<^sub>i.coinduct},
2030 @{thm [source] iterates\<^sub>i\<^sub>i.coinduct}, and
2031 @{thm [source] iterate\<^sub>i\<^sub>i_iterates\<^sub>i\<^sub>i.coinduct}
2032 and analogously for @{text strong_coinduct}. These rules and the
2033 underlying corecursors are generated on a per-need basis and are kept in a cache
2034 to speed up subsequent definitions.
2042 subsubsection {* Constructor View
2043 \label{ssec:primrec-constructor-view} *}
2051 The constructor view is similar to the code view, but there is one separate
2052 conditional equation per constructor rather than a single unconditional
2053 equation. Examples that rely on a single constructor, such as @{const literate}
2054 and @{const siterate}, are identical in both styles.
2056 Here is an example where there is a difference:
2059 primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
2060 "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lappend xs ys = LNil" |
2061 "_ \<Longrightarrow> lappend xs ys = LCons (lhd (if lnull xs then ys else xs))
2062 (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
2066 With the constructor view, we must distinguish between the @{const LNil} and
2067 the @{const LCons} case. The condition for @{const LCons} is
2068 left implicit, as the negation of that for @{const LNil}.
2070 For this example, the constructor view is slighlty more involved than the
2071 code equation. Recall the code view version presented in
2072 Section~\ref{sssec:primcorec-simple-corecursion}.
2073 % TODO: \[{thm code_view.lappend.code}\]
2074 The constructor view requires us to analyze the second argument (@{term ys}).
2075 The code equation generated from the constructor view also suffers from this.
2076 % TODO: \[{thm lappend.code}\]
2078 In contrast, the next example is arguably more naturally expressed in the
2083 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
2085 "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail" |
2086 "n mod 4 = 1 \<Longrightarrow>
2087 random_process s f n = Skip (random_process s f (f n))" |
2088 "n mod 4 = 2 \<Longrightarrow>
2089 random_process s f n = Action (shd s) (random_process (stl s) f (f n))" |
2090 "n mod 4 = 3 \<Longrightarrow>
2091 random_process s f n = Choice (random_process (every_snd s) f (f n))
2092 (random_process (every_snd (stl s)) f (f n))"
2099 Since there is no sequentiality, we can apply the equation for @{const Choice}
2100 without having first to discharge @{term "n mod (4\<Colon>int) \<noteq> 0"},
2101 @{term "n mod (4\<Colon>int) \<noteq> 1"}, and
2102 @{term "n mod (4\<Colon>int) \<noteq> 2"}.
2103 The price to pay for this elegance is that we must discharge exclusivity proof
2104 obligations, one for each pair of conditions
2105 @{term "(n mod (4\<Colon>int) = i, n mod (4\<Colon>int) = j)"}
2106 with @{term "i < j"}. If we prefer not to discharge any obligations, we can
2107 enable the @{text "sequential"} option. This pushes the problem to the users of
2108 the generated properties.
2109 %Here are more examples to conclude:
2113 subsubsection {* Destructor View
2114 \label{ssec:primrec-destructor-view} *}
2122 The destructor view is in many respects dual to the constructor view. Conditions
2123 determine which constructor to choose, and these conditions are interpreted
2124 sequentially or not depending on the @{text "sequential"} option.
2125 Consider the following examples:
2128 primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
2129 "\<not> lnull (literate _ x)" |
2130 "lhd (literate _ x) = x" |
2131 "ltl (literate g x) = literate g (g x)"
2133 text {* \blankline *}
2135 primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
2136 "shd (siterate _ x) = x" |
2137 "stl (siterate g x) = siterate g (g x)"
2139 text {* \blankline *}
2141 primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
2142 "shd (every_snd s) = shd s" |
2143 "stl (every_snd s) = stl (stl s)"
2147 The first formula in the @{const literate} specification indicates which
2148 constructor to choose. For @{const siterate} and @{const every_snd}, no such
2149 formula is necessary, since the type has only one constructor. The last two
2150 formulas are equations specifying the value of the result for the relevant
2151 selectors. Corecursive calls appear directly to the right of the equal sign.
2152 Their arguments are unrestricted.
2154 The next example shows how to specify functions that rely on more than one
2158 primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
2159 "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
2160 "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
2161 "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
2165 For a codatatype with $n$ constructors, it is sufficient to specify $n - 1$
2166 discriminator formulas. The command will then assume that the remaining
2167 constructor should be taken otherwise. This can be made explicit by adding
2176 primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
2177 "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
2179 "_ \<Longrightarrow> \<not> lnull (lappend xs ys)"
2181 "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
2182 "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
2187 to the specification. The generated selector theorems are conditional.
2189 The next example illustrates how to cope with selectors defined for several
2194 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
2196 "n mod 4 = 0 \<Longrightarrow> is_Fail (random_process s f n)" |
2197 "n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)" |
2198 "n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)" |
2199 "n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)" |
2200 "cont (random_process s f n) = random_process s f (f n)" of Skip |
2201 "prefix (random_process s f n) = shd s" |
2202 "cont (random_process s f n) = random_process (stl s) f (f n)" of Action |
2203 "left (random_process s f n) = random_process (every_snd s) f (f n)" |
2204 "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)"
2208 Using the @{text "of"} keyword, different equations are specified for @{const
2209 cont} depending on which constructor is selected.
2211 Here are more examples to conclude:
2215 even_infty :: even_enat and
2216 odd_infty :: odd_enat
2218 "\<not> is_Even_EZero even_infty" |
2219 "un_Even_ESuc even_infty = odd_infty" |
2220 "un_Odd_ESuc odd_infty = even_infty"
2222 text {* \blankline *}
2224 primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
2225 "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i g x) = x" |
2226 "sub\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i g x) = lmap (iterate\<^sub>i\<^sub>i g) (g x)"
2232 subsection {* Command Syntax
2233 \label{ssec:primcorec-command-syntax} *}
2236 subsubsection {* \keyw{primcorec} and \keyw{primcorecursive}
2237 \label{sssec:primcorecursive-and-primcorec} *}
2240 \begin{matharray}{rcl}
2241 @{command_def "primcorec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
2242 @{command_def "primcorecursive"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
2246 (@@{command primcorec} | @@{command primcorecursive}) target? \\ @{syntax pcr_option}? fixes @'where'
2247 (@{syntax pcr_formula} + '|')
2249 @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')'
2251 @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
2254 The optional target is optionally followed by a corecursion-specific option:
2257 \setlength{\itemsep}{0pt}
2260 The @{text "sequential"} option indicates that the conditions in specifications
2261 expressed using the constructor or destructor view are to be interpreted
2265 The @{text "exhaustive"} option indicates that the conditions in specifications
2266 expressed using the constructor or destructor view cover all possible cases.
2270 The @{command primcorec} command is an abbreviation for @{command primcorecursive} with
2271 @{text "by auto?"} to discharge any emerging proof obligations.
2276 subsection {* Generated Theorems
2277 \label{ssec:primcorec-generated-theorems} *}
2282 subsection {* Recursive Default Values for Selectors
2283 \label{ssec:primcorec-recursive-default-values-for-selectors} *}
2286 partial_function to the rescue
2291 section {* Registering Bounded Natural Functors
2292 \label{sec:registering-bounded-natural-functors} *}
2295 The (co)datatype package can be set up to allow nested recursion through
2296 arbitrary type constructors, as long as they adhere to the BNF requirements and
2297 are registered as BNFs.
2302 subsection {* Introductory Example
2303 \label{ssec:bnf-introductory-example} *}
2306 More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and
2307 \verb|~~/src/HOL/BNF/More_BNFs.thy|.
2309 %Mention distinction between live and dead type arguments;
2310 % * and existence of map, set for those
2316 subsection {* Command Syntax
2317 \label{ssec:bnf-command-syntax} *}
2320 subsubsection {* \keyw{bnf}
2321 \label{sssec:bnf} *}
2324 \begin{matharray}{rcl}
2325 @{command_def "bnf"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
2329 @@{command bnf} target? (name ':')? typ \\
2330 'map:' term ('sets:' (term +))? 'bd:' term \\
2331 ('wits:' (term +))? ('rel:' term)?
2336 subsubsection {* \keyw{bnf\_decl}
2337 \label{sssec:bnf-decl} *}
2340 %%% TODO: use command_def once the command is available
2341 \begin{matharray}{rcl}
2342 @{text "bnf_decl"} & : & @{text "local_theory \<rightarrow> local_theory"}
2346 @@{command bnf_decl} target? @{syntax dt_name}
2348 @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
2350 @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')'
2352 @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
2355 Declares a fresh type and fresh constants (map, set, relator, cardinal bound)
2356 and asserts the bnf properties for these constants as axioms. Additionally,
2357 type arguments may be marked as dead (by using @{syntax "-"} instead of a name for the
2358 set function)---this is the only difference of @{syntax dt_name} compared to
2359 the syntax used by the @{command datatype_new}/@{command codatatype} commands.
2361 The axioms are sound, since one there exists a bnf of any given arity.
2365 subsubsection {* \keyw{print\_bnfs}
2366 \label{sssec:print-bnfs} *}
2369 \begin{matharray}{rcl}
2370 @{command_def "print_bnfs"} & : & @{text "local_theory \<rightarrow>"}
2374 @@{command print_bnfs}
2379 section {* Deriving Destructors and Theorems for Free Constructors
2380 \label{sec:deriving-destructors-and-theorems-for-free-constructors} *}
2383 The derivation of convenience theorems for types equipped with free constructors,
2384 as performed internally by @{command datatype_new} and @{command codatatype},
2385 is available as a stand-alone command called @{command wrap_free_constructors}.
2387 % * need for this is rare but may arise if you want e.g. to add destructors to
2388 % a type not introduced by ...
2390 % * also useful for compatibility with old package, e.g. add destructors to
2391 % old \keyw{datatype}
2393 % * @{command wrap_free_constructors}
2394 % * @{text "no_discs_sels"}, @{text "no_code"}, @{text "rep_compat"}
2395 % * hack to have both co and nonco view via locale (cf. ext nats)
2402 subsection {* Introductory Example
2403 \label{ssec:ctors-introductory-example} *}
2407 subsection {* Command Syntax
2408 \label{ssec:ctors-command-syntax} *}
2411 subsubsection {* \keyw{wrap\_free\_constructors}
2412 \label{sssec:wrap-free-constructors} *}
2415 \begin{matharray}{rcl}
2416 @{command_def "wrap_free_constructors"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
2420 @@{command wrap_free_constructors} target? @{syntax dt_options} \\
2421 term_list name @{syntax wfc_discs_sels}?
2423 @{syntax_def wfc_discs_sels}: name_list (name_list_list name_term_list_list? )?
2425 @{syntax_def name_term}: (name ':' term)
2427 X_list: '[' (X + ',') ']'
2430 % options: no_discs_sels no_code rep_compat
2433 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
2438 section {* Standard ML Interface
2439 \label{sec:standard-ml-interface} *}
2442 The package's programmatic interface.
2448 section {* Interoperability
2449 \label{sec:interoperability} *}
2452 The package's interaction with other Isabelle packages and tools, such as the
2453 code generator and the counterexample generators.
2457 subsection {* Transfer and Lifting
2458 \label{ssec:transfer-and-lifting} *}
2461 subsection {* Code Generator
2462 \label{ssec:code-generator} *}
2465 subsection {* Quickcheck
2466 \label{ssec:quickcheck} *}
2469 subsection {* Nitpick
2470 \label{ssec:nitpick} *}
2473 subsection {* Nominal Isabelle
2474 \label{ssec:nominal-isabelle} *}
2479 section {* Known Bugs and Limitations
2480 \label{sec:known-bugs-and-limitations} *}
2483 Known open issues of the package.
2487 %* primcorecursive and primcorec is unfinished
2489 %* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
2491 %* issues with HOL-Proofs?
2493 %* partial documentation
2495 %* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
2496 % (for @{command datatype_new_compat} and prim(co)rec)
2498 % * a fortiori, no way to register same type as both data- and codatatype
2500 %* no recursion through unused arguments (unlike with the old package)
2502 %* in a locale, cannot use locally fixed types (because of limitation in typedef)?
2504 % *names of variables suboptimal
2510 \section*{Acknowledgment}
2512 Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
2513 (co)datatype package. Andreas Lochbihler provided lots of comments on earlier
2514 versions of the package, especially for the coinductive part. Brian Huffman
2515 suggested major simplifications to the internal constructions, much of which has
2516 yet to be implemented. Florian Haftmann and Christian Urban provided general
2517 advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder
2518 found an elegant proof to eliminate one of the BNF assumptions. Andreas
2519 Lochbihler and Christian Sternagel suggested many textual improvements to this