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.
13 "primcorec_notyet" :: thy_decl
17 (* FIXME: Temporary setup until "primcorec" and "primcorecursive" are fully implemented. *)
19 fun add_dummy_cmd _ _ lthy = lthy;
21 val _ = Outer_Syntax.local_theory @{command_spec "primcorec_notyet"} ""
22 (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd);
27 section {* Introduction
28 \label{sec:introduction} *}
31 The 2013 edition of Isabelle introduced a new definitional package for freely
32 generated datatypes and codatatypes. The datatype support is similar to that
33 provided by the earlier package due to Berghofer and Wenzel
34 \cite{Berghofer-Wenzel:1999:TPHOL}, documented in the Isar reference manual
35 \cite{isabelle-isar-ref}; indeed, replacing the keyword \keyw{datatype} by
36 @{command datatype_new} is usually all that is needed to port existing theories
37 to use the new package.
39 Perhaps the main advantage of the new package is that it supports recursion
40 through a large class of non-datatypes, such as finite sets:
43 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")
47 Another strong point is the support for local definitions:
52 datatype_new flag = Less | Eq | Greater
57 The package also provides some convenience, notably automatically generated
58 discriminators and selectors.
60 In addition to plain inductive datatypes, the new package supports coinductive
61 datatypes, or \emph{codatatypes}, which may have infinite values. For example,
62 the following command introduces the type of lazy lists, which comprises both
63 finite and infinite values:
69 codatatype (*<*)(in early) (*>*)'a llist = LNil | LCons 'a "'a llist"
73 Mixed inductive--coinductive recursion is possible via nesting. Compare the
74 following four Rose tree examples:
77 datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
78 datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
79 codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
80 codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
83 The first two tree types allow only finite branches, whereas the last two allow
84 branches of infinite length. Orthogonally, the nodes in the first and third
85 types have finite branching, whereas those of the second and fourth may have
86 infinitely many direct subtrees.
88 To use the package, it is necessary to import the @{theory BNF} theory, which
89 can be precompiled into the \texttt{HOL-BNF} image. The following commands show
90 how to launch jEdit/PIDE with the image loaded and how to build the image
91 without launching jEdit:
96 \ \ \ \ \texttt{isabelle jedit -l HOL-BNF} \\
98 \hbox{}\ \ \ \ \texttt{isabelle build -b HOL-BNF}
102 The package, like its predecessor, fully adheres to the LCF philosophy
103 \cite{mgordon79}: The characteristic theorems associated with the specified
104 (co)datatypes are derived rather than introduced axiomatically.%
105 \footnote{If the @{text quick_and_dirty} option is enabled, some of the
106 internal constructions and most of the internal proof obligations are skipped.}
107 The package's metatheory is described in a pair of papers
108 \cite{traytel-et-al-2012,blanchette-et-al-wit}. The central notion is that of a
109 \emph{bounded natural functor} (BNF)---a well-behaved type constructor for which
110 nested (co)recursion is supported.
112 This tutorial is organized as follows:
115 \setlength{\itemsep}{0pt}
117 \item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
118 describes how to specify datatypes using the @{command datatype_new} command.
120 \item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
121 Functions,'' describes how to specify recursive functions using
122 @{command primrec_new}, \keyw{fun}, and \keyw{function}.
124 \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
125 describes how to specify codatatypes using the @{command codatatype} command.
127 \item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive
128 Functions,'' describes how to specify corecursive functions using the
129 @{command primcorec} and @{command primcorecursive} commands.
131 \item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
132 Bounded Natural Functors,'' explains how to use the @{command bnf} command
133 to register arbitrary type constructors as BNFs.
136 \ref{sec:deriving-destructors-and-theorems-for-free-constructors},
137 ``Deriving Destructors and Theorems for Free Constructors,'' explains how to
138 use the command @{command wrap_free_constructors} to derive destructor constants
139 and theorems for freely generated types, as performed internally by @{command
140 datatype_new} and @{command codatatype}.
142 %\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
143 %describes the package's programmatic interface.
145 %\item Section \ref{sec:interoperability}, ``Interoperability,''
146 %is concerned with the packages' interaction with other Isabelle packages and
147 %tools, such as the code generator and the counterexample generators.
149 %\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
150 %Limitations,'' concludes with known open issues at the time of writing.
155 \setbox\boxA=\hbox{\texttt{nospam}}
157 \newcommand\authoremaili{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
158 in.\allowbreak tum.\allowbreak de}}
159 \newcommand\authoremailii{\texttt{lore{\color{white}nospam}\kern-\wd\boxA{}nz.panny@\allowbreak
160 \allowbreak tum.\allowbreak de}}
161 \newcommand\authoremailiii{\texttt{pope{\color{white}nospam}\kern-\wd\boxA{}scua@\allowbreak
162 in.\allowbreak tum.\allowbreak de}}
163 \newcommand\authoremailiv{\texttt{tray{\color{white}nospam}\kern-\wd\boxA{}tel@\allowbreak
164 in.\allowbreak tum.\allowbreak de}}
166 The commands @{command datatype_new} and @{command primrec_new} are expected to
167 displace \keyw{datatype} and \keyw{primrec} in a future release. Authors of new
168 theories are encouraged to use the new commands, and maintainers of older
169 theories may want to consider upgrading.
171 Comments and bug reports concerning either the tool or this tutorial should be
172 directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
177 \textbf{Warning:}\enskip This tutorial and the package it describes are under
178 construction. Please apologise for their appearance. Should you have suggestions
179 or comments regarding either, please let the authors know.
184 section {* Defining Datatypes
185 \label{sec:defining-datatypes} *}
188 Datatypes can be specified using the @{command datatype_new} command.
192 subsection {* Introductory Examples
193 \label{ssec:datatype-introductory-examples} *}
196 Datatypes are illustrated through concrete examples featuring different flavors
197 of recursion. More examples can be found in the directory
198 \verb|~~/src/HOL/BNF/Examples|.
201 subsubsection {* Nonrecursive Types
202 \label{sssec:datatype-nonrecursive-types} *}
205 Datatypes are introduced by specifying the desired names and argument types for
206 their constructors. \emph{Enumeration} types are the simplest form of datatype.
207 All their constructors are nullary:
210 datatype_new trool = Truue | Faalse | Perhaaps
214 Here, @{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}.
216 Polymorphic types are possible, such as the following option type, modeled after
217 its homologue from the @{theory Option} theory:
223 datatype_new 'a option = None | Some 'a
227 The constructors are @{text "None :: 'a option"} and
228 @{text "Some :: 'a \<Rightarrow> 'a option"}.
230 The next example has three type parameters:
233 datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c
238 @{text "Triple :: 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a, 'b, 'c) triple"}.
239 Unlike in Standard ML, curried constructors are supported. The uncurried variant
243 datatype_new ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
246 subsubsection {* Simple Recursion
247 \label{sssec:datatype-simple-recursion} *}
250 Natural numbers are the simplest example of a recursive type:
253 datatype_new nat = Zero | Suc nat
257 Lists were shown in the introduction. Terminated lists are a variant:
260 datatype_new (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
264 Occurrences of nonatomic types on the right-hand side of the equal sign must be
265 enclosed in double quotes, as is customary in Isabelle.
269 subsubsection {* Mutual Recursion
270 \label{sssec:datatype-mutual-recursion} *}
273 \emph{Mutually recursive} types are introduced simultaneously and may refer to
274 each other. The example below introduces a pair of types for even and odd
278 datatype_new even_nat = Even_Zero | Even_Suc odd_nat
279 and odd_nat = Odd_Suc even_nat
283 Arithmetic expressions are defined via terms, terms via factors, and factors via
287 datatype_new ('a, 'b) exp =
288 Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
290 Factor "('a, 'b) fct" | Prod "('a, 'b) fct" "('a, 'b) trm"
292 Const 'a | Var 'b | Expr "('a, 'b) exp"
295 subsubsection {* Nested Recursion
296 \label{sssec:datatype-nested-recursion} *}
299 \emph{Nested recursion} occurs when recursive occurrences of a type appear under
300 a type constructor. The introduction showed some examples of trees with nesting
301 through lists. A more complex example, that reuses our @{type option} type,
305 datatype_new 'a btree =
306 BNode 'a "'a btree option" "'a btree option"
310 Not all nestings are admissible. For example, this command will fail:
313 datatype_new 'a wrong = Wrong (*<*)'a
314 typ (*>*)"'a wrong \<Rightarrow> 'a"
318 The issue is that the function arrow @{text "\<Rightarrow>"} allows recursion
319 only through its right-hand side. This issue is inherited by polymorphic
320 datatypes defined in terms of~@{text "\<Rightarrow>"}:
323 datatype_new ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
324 datatype_new 'a also_wrong = Also_Wrong (*<*)'a
325 typ (*>*)"('a also_wrong, 'a) fn"
332 datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
336 In general, type constructors @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
337 allow recursion on a subset of their type arguments @{text 'a\<^sub>1}, \ldots,
338 @{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
339 type arguments are called \emph{dead}. In @{typ "'a \<Rightarrow> 'b"} and
340 @{typ "('a, 'b) fn"}, the type variable @{typ 'a} is dead and @{typ 'b} is live.
342 Type constructors must be registered as BNFs to have live arguments. This is
343 done automatically for datatypes and codatatypes introduced by the @{command
344 datatype_new} and @{command codatatype} commands.
345 Section~\ref{sec:registering-bounded-natural-functors} explains how to register
346 arbitrary type constructors as BNFs.
350 subsubsection {* Custom Names and Syntaxes
351 \label{sssec:datatype-custom-names-and-syntaxes} *}
354 The @{command datatype_new} command introduces various constants in addition to
355 the constructors. With each datatype are associated set functions, a map
356 function, a relator, discriminators, and selectors, all of which can be given
357 custom names. In the example below, the traditional names
358 @{text set}, @{text map}, @{text list_all2}, @{text null}, @{text hd}, and
359 @{text tl} override the default names @{text list_set}, @{text list_map}, @{text
360 list_rel}, @{text is_Nil}, @{text un_Cons1}, and @{text un_Cons2}:
365 "[x, xs]" == "x # [xs]"
373 hide_const Nil Cons hd tl set map list_all2 list_case list_rec
377 datatype_new (set: 'a) list (map: map rel: list_all2) =
378 null: Nil (defaults tl: Nil)
379 | Cons (hd: 'a) (tl: "'a list")
383 The command introduces a discriminator @{const null} and a pair of selectors
384 @{const hd} and @{const tl} characterized as follows:
386 \[@{thm list.collapse(1)[of xs, no_vars]}
387 \qquad @{thm list.collapse(2)[of xs, no_vars]}\]
389 For two-constructor datatypes, a single discriminator constant suffices. The
390 discriminator associated with @{const Cons} is simply
391 @{term "\<lambda>xs. \<not> null xs"}.
393 The @{text defaults} clause following the @{const Nil} constructor specifies a
394 default value for selectors associated with other constructors. Here, it is used
395 to ensure that the tail of the empty list is itself (instead of being left
398 Because @{const Nil} is nullary, it is also possible to use
399 @{term "\<lambda>xs. xs = Nil"} as a discriminator. This is specified by
400 entering ``@{text "="}'' instead of the identifier @{const null}. Although this
401 may look appealing, the mixture of constructors and selectors in the
402 characteristic theorems can lead Isabelle's automation to switch between the
403 constructor and the destructor view in surprising ways.
405 The usual mixfix syntaxes are available for both types and constructors. For
412 datatype_new ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
414 text {* \blankline *}
416 datatype_new (set: 'a) list (map: map rel: list_all2) =
418 | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
422 Incidentally, this is how the traditional syntaxes can be set up:
425 syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
427 text {* \blankline *}
430 "[x, xs]" == "x # [xs]"
434 subsection {* Command Syntax
435 \label{ssec:datatype-command-syntax} *}
438 subsubsection {* \keyw{datatype\_new}
439 \label{sssec:datatype-new} *}
442 \begin{matharray}{rcl}
443 @{command_def "datatype_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
447 @@{command datatype_new} target? @{syntax dt_options}? \\
448 (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
450 @{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'
453 The syntactic quantity \synt{target} can be used to specify a local
454 context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
455 manual \cite{isabelle-isar-ref}.
457 The optional target is optionally followed by datatype-specific options:
460 \setlength{\itemsep}{0pt}
463 The @{text "no_discs_sels"} option indicates that no discriminators or selectors
467 The @{text "rep_compat"} option indicates that the generated names should
468 contain optional (and normally not displayed) ``@{text "new."}'' components to
469 prevent clashes with a later call to \keyw{rep\_datatype}. See
470 Section~\ref{ssec:datatype-compatibility-issues} for details.
473 The left-hand sides of the datatype equations specify the name of the type to
474 define, its type parameters, and additional information:
477 @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
479 @{syntax_def tyargs}: typefree | '(' ((name ':')? typefree + ',') ')'
481 @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
485 The syntactic quantity \synt{name} denotes an identifier, \synt{typefree}
486 denotes fixed type variable (@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix}
487 denotes the usual parenthesized mixfix notation. They are documented in the Isar
488 reference manual \cite{isabelle-isar-ref}.
490 The optional names preceding the type variables allow to override the default
491 names of the set functions (@{text t_set1}, \ldots, @{text t_setM}).
492 Inside a mutually recursive specification, all defined datatypes must
493 mention exactly the same type variables in the same order.
496 @{syntax_def ctor}: (name ':')? name (@{syntax ctor_arg} * ) \\
497 @{syntax dt_sel_defaults}? mixfix?
503 The main constituents of a constructor specification is the name of the
504 constructor and the list of its argument types. An optional discriminator name
505 can be supplied at the front to override the default name
506 (@{text t.is_C\<^sub>j}).
509 @{syntax_def ctor_arg}: type | '(' name ':' type ')'
515 In addition to the type of a constructor argument, it is possible to specify a
516 name for the corresponding selector to override the default name
517 (@{text un_C\<^sub>ji}). The same selector names can be reused for several
518 constructors as long as they share the same type.
521 @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')'
526 @{text "C \<Colon> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<sigma>"},
527 default values can be specified for any selector
528 @{text "un_D \<Colon> \<sigma> \<Rightarrow> \<tau>"}
529 associated with other constructors. The specified default value must be of type
530 @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<tau>"}
531 (i.e., it may depends on @{text C}'s arguments).
535 subsubsection {* \keyw{datatype\_new\_compat}
536 \label{sssec:datatype-new-compat} *}
539 \begin{matharray}{rcl}
540 @{command_def "datatype_new_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
544 @@{command datatype_new_compat} names
548 The old datatype package provides some functionality that is not yet replicated
552 \setlength{\itemsep}{0pt}
554 \item It is integrated with \keyw{fun} and \keyw{function}
555 \cite{isabelle-function}, Nitpick \cite{isabelle-nitpick}, Quickcheck,
558 \item It is extended by various add-ons, notably to produce instances of the
559 @{const size} function.
563 New-style datatypes can in most case be registered as old-style datatypes using
564 @{command datatype_new_compat}. The \textit{names} argument is a space-separated
565 list of type names that are mutually recursive. For example:
568 datatype_new_compat even_nat odd_nat
570 text {* \blankline *}
572 thm even_nat_odd_nat.size
574 text {* \blankline *}
576 ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *}
579 A few remarks concern nested recursive datatypes only:
582 \setlength{\itemsep}{0pt}
584 \item The old-style, nested-as-mutual induction rule, iterator theorems, and
585 recursor theorems are generated under their usual names but with ``@{text
586 "compat_"}'' prefixed (e.g., @{text compat_tree.induct}).
588 \item All types through which recursion takes place must be new-style datatypes
589 or the function type. In principle, it should be possible to support old-style
590 datatypes as well, but the command does not support this yet (and there is
591 currently no way to register old-style datatypes as new-style datatypes).
594 An alternative to @{command datatype_new_compat} is to use the old package's
595 \keyw{rep\_datatype} command. The associated proof obligations must then be
600 subsection {* Generated Constants
601 \label{ssec:datatype-generated-constants} *}
604 Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
605 with $m > 0$ live type variables and $n$ constructors
606 @{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the
607 following auxiliary constants are introduced:
610 \setlength{\itemsep}{0pt}
612 \item \relax{Case combinator}: @{text t_case} (rendered using the familiar
613 @{text case}--@{text of} syntax)
615 \item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
616 @{text "t.is_C\<^sub>n"}
618 \item \relax{Selectors}:
619 @{text t.un_C\<^sub>11}$, \ldots, @{text t.un_C\<^sub>1k\<^sub>1}, \\
620 \phantom{\relax{Selectors:}} \quad\vdots \\
621 \phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
623 \item \relax{Set functions} (or \relax{natural transformations}):
624 @{text t_set1}, \ldots, @{text t_setm}
626 \item \relax{Map function} (or \relax{functorial action}): @{text t_map}
628 \item \relax{Relator}: @{text t_rel}
630 \item \relax{Iterator}: @{text t_fold}
632 \item \relax{Recursor}: @{text t_rec}
637 The case combinator, discriminators, and selectors are collectively called
638 \emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
639 name and is normally hidden.
643 subsection {* Generated Theorems
644 \label{ssec:datatype-generated-theorems} *}
647 The characteristic theorems generated by @{command datatype_new} are grouped in
648 three broad categories:
651 \setlength{\itemsep}{0pt}
653 \item The \emph{free constructor theorems} are properties about the constructors
654 and destructors that can be derived for any freely generated type. Internally,
655 the derivation is performed by @{command wrap_free_constructors}.
657 \item The \emph{functorial theorems} are properties of datatypes related to
660 \item The \emph{inductive theorems} are properties of datatypes related to
661 their inductive nature.
666 The full list of named theorems can be obtained as usual by entering the
667 command \keyw{print\_theorems} immediately after the datatype definition.
668 This list normally excludes low-level theorems that reveal internal
669 constructions. To make these accessible, add the line
672 declare [[bnf_note_all]]
674 declare [[bnf_note_all = false]]
679 to the top of the theory file.
682 subsubsection {* Free Constructor Theorems
683 \label{sssec:free-constructor-theorems} *}
690 The first subgroup of properties are concerned with the constructors.
691 They are listed below for @{typ "'a list"}:
696 \item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\rm:] ~ \\
697 @{thm list.inject[no_vars]}
699 \item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\rm:] ~ \\
700 @{thm list.distinct(1)[no_vars]} \\
701 @{thm list.distinct(2)[no_vars]}
703 \item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
704 @{thm list.exhaust[no_vars]}
706 \item[@{text "t."}\hthm{nchotomy}\rm:] ~ \\
707 @{thm list.nchotomy[no_vars]}
713 In addition, these nameless theorems are registered as safe elimination rules:
718 \item[@{text "t."}\hthm{list.distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rm:] ~ \\
719 @{thm list.distinct(1)[THEN notE, elim!, no_vars]} \\
720 @{thm list.distinct(2)[THEN notE, elim!, no_vars]}
726 The next subgroup is concerned with the case combinator:
731 \item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\
732 @{thm list.case(1)[no_vars]} \\
733 @{thm list.case(2)[no_vars]}
735 \item[@{text "t."}\hthm{case\_cong}\rm:] ~ \\
736 @{thm list.case_cong[no_vars]}
738 \item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\rm:] ~ \\
739 @{thm list.weak_case_cong[no_vars]}
741 \item[@{text "t."}\hthm{split}\rm:] ~ \\
742 @{thm list.split[no_vars]}
744 \item[@{text "t."}\hthm{split\_asm}\rm:] ~ \\
745 @{thm list.split_asm[no_vars]}
747 \item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]
753 The third and last subgroup revolves around discriminators and selectors:
758 \item[@{text "t."}\hthm{disc} @{text "[simp]"}\rm:] ~ \\
759 @{thm list.disc(1)[no_vars]} \\
760 @{thm list.disc(2)[no_vars]}
762 \item[@{text "t."}\hthm{discI}\rm:] ~ \\
763 @{thm list.discI(1)[no_vars]} \\
764 @{thm list.discI(2)[no_vars]}
766 \item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
767 @{thm list.sel(1)[no_vars]} \\
768 @{thm list.sel(2)[no_vars]}
770 \item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
771 @{thm list.collapse(1)[no_vars]} \\
772 @{thm list.collapse(2)[no_vars]}
774 \item[@{text "t."}\hthm{disc\_exclude}\rm:] ~ \\
775 These properties are missing for @{typ "'a list"} because there is only one
776 proper discriminator. Had the datatype been introduced with a second
777 discriminator called @{const is_Cons}, they would have read thusly: \\[\jot]
778 @{prop "null list \<Longrightarrow> \<not> is_Cons list"} \\
779 @{prop "is_Cons list \<Longrightarrow> \<not> null list"}
781 \item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
782 @{thm list.disc_exhaust[no_vars]}
784 \item[@{text "t."}\hthm{expand}\rm:] ~ \\
785 @{thm list.expand[no_vars]}
787 \item[@{text "t."}\hthm{case\_conv}\rm:] ~ \\
788 @{thm list.case_conv[no_vars]}
795 subsubsection {* Functorial Theorems
796 \label{sssec:functorial-theorems} *}
799 The BNF-related theorem are as follows:
804 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
805 @{thm list.set(1)[no_vars]} \\
806 @{thm list.set(2)[no_vars]}
808 \item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
809 @{thm list.map(1)[no_vars]} \\
810 @{thm list.map(2)[no_vars]}
812 \item[@{text "t."}\hthm{rel\_inject} @{text "[simp, code]"}\rm:] ~ \\
813 @{thm list.rel_inject(1)[no_vars]} \\
814 @{thm list.rel_inject(2)[no_vars]}
816 \item[@{text "t."}\hthm{rel\_distinct} @{text "[simp, code]"}\rm:] ~ \\
817 @{thm list.rel_distinct(1)[no_vars]} \\
818 @{thm list.rel_distinct(2)[no_vars]}
825 subsubsection {* Inductive Theorems
826 \label{sssec:inductive-theorems} *}
829 The inductive theorems are as follows:
834 \item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
835 @{thm list.induct[no_vars]}
837 \item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
838 Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
839 prove $m$ properties simultaneously.
841 \item[@{text "t."}\hthm{fold} @{text "[simp, code]"}\rm:] ~ \\
842 @{thm list.fold(1)[no_vars]} \\
843 @{thm list.fold(2)[no_vars]}
845 \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
846 @{thm list.rec(1)[no_vars]} \\
847 @{thm list.rec(2)[no_vars]}
853 For convenience, @{command datatype_new} also provides the following collection:
858 \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}] ~ \\
859 @{text t.rel_distinct} @{text t.set}
866 subsection {* Compatibility Issues
867 \label{ssec:datatype-compatibility-issues} *}
870 The command @{command datatype_new} was designed to be highly compatible with
871 \keyw{datatype}, to ease migration. There are nonetheless a number of
872 incompatibilities that may arise when porting to the new package:
875 \setlength{\itemsep}{0pt}
877 \item \emph{The Standard ML interfaces are different.} Tools and extensions
878 written to call the old ML interfaces will need to be adapted to the new
879 interfaces. Little has been done so far in this direction. Whenever possible, it
880 is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype}
881 to register new-style datatypes as old-style datatypes.
883 \item \emph{The recursor @{text "t_rec"} has a different signature for nested
884 recursive datatypes.} In the old package, nested recursion was internally
885 reduced to mutual recursion. This reduction was visible in the type of the
886 recursor, used by \keyw{primrec}. In the new package, nested recursion is
887 handled in a more modular fashion. The old-style recursor can be generated on
888 demand using @{command primrec_new}, as explained in
889 Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
892 \item \emph{Accordingly, the induction principle is different for nested
893 recursive datatypes.} Again, the old-style induction principle can be generated
894 on demand using @{command primrec_new}, as explained in
895 Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
898 \item \emph{The internal constructions are completely different.} Proofs texts
899 that unfold the definition of constants introduced by \keyw{datatype} will be
902 \item \emph{A few theorems have different names.}
903 The properties @{text t.cases} and @{text t.recs} have been renamed to
904 @{text t.case} and @{text t.rec}. For non-mutually recursive datatypes,
905 @{text t.inducts} is available as @{text t.induct}.
906 For $m > 1$ mutually recursive datatypes,
907 @{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed to
908 @{text "t\<^sub>i.induct"}.
910 \item \emph{The @{text t.simps} collection has been extended.}
911 Previously available theorems are available at the same index.
913 \item \emph{Variables in generated properties have different names.} This is
914 rarely an issue, except in proof texts that refer to variable names in the
915 @{text "[where \<dots>]"} attribute. The solution is to use the more robust
916 @{text "[of \<dots>]"} syntax.
919 In the other direction, there is currently no way to register old-style
920 datatypes as new-style datatypes. If the goal is to define new-style datatypes
921 with nested recursion through old-style datatypes, the old-style
922 datatypes can be registered as a BNF
923 (Section~\ref{sec:registering-bounded-natural-functors}). If the goal is
924 to derive discriminators and selectors, this can be achieved using @{command
925 wrap_free_constructors}
926 (Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
930 section {* Defining Recursive Functions
931 \label{sec:defining-recursive-functions} *}
934 Recursive functions over datatypes can be specified using @{command
935 primrec_new}, which supports primitive recursion, or using the more general
936 \keyw{fun} and \keyw{function} commands. Here, the focus is on @{command
937 primrec_new}; the other two commands are described in a separate tutorial
938 \cite{isabelle-function}.
940 %%% TODO: partial_function
944 subsection {* Introductory Examples
945 \label{ssec:primrec-introductory-examples} *}
948 Primitive recursion is illustrated through concrete examples based on the
949 datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
950 examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|.
954 subsubsection {* Nonrecursive Types
955 \label{sssec:primrec-nonrecursive-types} *}
958 Primitive recursion removes one layer of constructors on the left-hand side in
959 each equation. For example:
962 primrec_new bool_of_trool :: "trool \<Rightarrow> bool" where
963 "bool_of_trool Faalse \<longleftrightarrow> False" |
964 "bool_of_trool Truue \<longleftrightarrow> True"
966 text {* \blankline *}
968 primrec_new the_list :: "'a option \<Rightarrow> 'a list" where
969 "the_list None = []" |
970 "the_list (Some a) = [a]"
972 text {* \blankline *}
974 primrec_new the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
975 "the_default d None = d" |
976 "the_default _ (Some a) = a"
978 text {* \blankline *}
980 primrec_new mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
981 "mirrror (Triple a b c) = Triple c b a"
985 The equations can be specified in any order, and it is acceptable to leave out
986 some cases, which are then unspecified. Pattern matching on the left-hand side
987 is restricted to a single datatype, which must correspond to the same argument
992 subsubsection {* Simple Recursion
993 \label{sssec:primrec-simple-recursion} *}
996 For simple recursive types, recursive calls on a constructor argument are
997 allowed on the right-hand side:
1000 primrec_new replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
1001 "replicate Zero _ = []" |
1002 "replicate (Suc n) x = x # replicate n x"
1004 text {* \blankline *}
1006 primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
1009 Zero \<Rightarrow> x
1010 | Suc j' \<Rightarrow> at xs j')"
1012 text {* \blankline *}
1014 primrec_new (*<*)(in early) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
1015 "tfold _ (TNil y) = y" |
1016 "tfold f (TCons x xs) = f x (tfold f xs)"
1020 The next example is not primitive recursive, but it can be defined easily using
1021 \keyw{fun}. The @{command datatype_new_compat} command is needed to register
1022 new-style datatypes for use with \keyw{fun} and \keyw{function}
1023 (Section~\ref{sssec:datatype-new-compat}):
1026 datatype_new_compat nat
1028 text {* \blankline *}
1030 fun at_least_two :: "nat \<Rightarrow> bool" where
1031 "at_least_two (Suc (Suc _)) \<longleftrightarrow> True" |
1032 "at_least_two _ \<longleftrightarrow> False"
1035 subsubsection {* Mutual Recursion
1036 \label{sssec:primrec-mutual-recursion} *}
1039 The syntax for mutually recursive functions over mutually recursive datatypes
1044 nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
1045 nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
1047 "nat_of_even_nat Even_Zero = Zero" |
1048 "nat_of_even_nat (Even_Suc n) = Suc (nat_of_odd_nat n)" |
1049 "nat_of_odd_nat (Odd_Suc n) = Suc (nat_of_even_nat n)"
1051 text {* \blankline *}
1054 eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
1055 eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and
1056 eval\<^sub>f :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) fct \<Rightarrow> int"
1058 "eval\<^sub>e \<gamma> \<xi> (Term t) = eval\<^sub>t \<gamma> \<xi> t" |
1059 "eval\<^sub>e \<gamma> \<xi> (Sum t e) = eval\<^sub>t \<gamma> \<xi> t + eval\<^sub>e \<gamma> \<xi> e" |
1060 "eval\<^sub>t \<gamma> \<xi> (Factor f) = eval\<^sub>f \<gamma> \<xi> f" |
1061 "eval\<^sub>t \<gamma> \<xi> (Prod f t) = eval\<^sub>f \<gamma> \<xi> f + eval\<^sub>t \<gamma> \<xi> t" |
1062 "eval\<^sub>f \<gamma> _ (Const a) = \<gamma> a" |
1063 "eval\<^sub>f _ \<xi> (Var b) = \<xi> b" |
1064 "eval\<^sub>f \<gamma> \<xi> (Expr e) = eval\<^sub>e \<gamma> \<xi> e"
1068 Mutual recursion is possible within a single type, using \keyw{fun}:
1072 even :: "nat \<Rightarrow> bool" and
1073 odd :: "nat \<Rightarrow> bool"
1075 "even Zero = True" |
1076 "even (Suc n) = odd n" |
1077 "odd Zero = False" |
1078 "odd (Suc n) = even n"
1081 subsubsection {* Nested Recursion
1082 \label{sssec:primrec-nested-recursion} *}
1085 In a departure from the old datatype package, nested recursion is normally
1086 handled via the map functions of the nesting type constructors. For example,
1087 recursive calls are lifted to lists using @{const map}:
1091 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")
1093 primrec_new at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
1094 "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
1097 | j # js' \<Rightarrow> at (map (\<lambda>t. at\<^sub>f\<^sub>f t js') ts) j)"
1101 The next example features recursion through the @{text option} type. Although
1102 @{text option} is not a new-style datatype, it is registered as a BNF with the
1103 map function @{const option_map}:
1106 primrec_new (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
1107 "sum_btree (BNode a lt rt) =
1108 a + the_default 0 (option_map sum_btree lt) +
1109 the_default 0 (option_map sum_btree rt)"
1113 The same principle applies for arbitrary type constructors through which
1114 recursion is possible. Notably, the map function for the function type
1115 (@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
1118 primrec_new ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
1119 "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
1120 "ftree_map f (FTNode g) = FTNode (ftree_map f \<circ> g)"
1124 (No such function is defined by the package because @{typ 'a} is dead in
1125 @{typ "'a ftree"}, but we can easily do it ourselves.)
1129 subsubsection {* Nested-as-Mutual Recursion
1130 \label{sssec:primrec-nested-as-mutual-recursion} *}
1137 For compatibility with the old package, but also because it is sometimes
1138 convenient in its own right, it is possible to treat nested recursive datatypes
1139 as mutually recursive ones if the recursion takes place though new-style
1140 datatypes. For example:
1144 at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" and
1145 ats\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a"
1147 "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
1150 | j # js' \<Rightarrow> ats\<^sub>f\<^sub>f ts j js')" |
1151 "ats\<^sub>f\<^sub>f (t # ts) j =
1153 Zero \<Rightarrow> at\<^sub>f\<^sub>f t
1154 | Suc j' \<Rightarrow> ats\<^sub>f\<^sub>f ts j')"
1158 Appropriate induction principles are generated under the names
1159 @{thm [source] "at\<^sub>f\<^sub>f.induct"},
1160 @{thm [source] "ats\<^sub>f\<^sub>f.induct"}, and
1161 @{thm [source] "at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct"}.
1163 %%% TODO: Add recursors.
1165 Here is a second example:
1169 sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" and
1170 sum_btree_option :: "'a btree option \<Rightarrow> 'a"
1172 "sum_btree (BNode a lt rt) =
1173 a + sum_btree_option lt + sum_btree_option rt" |
1174 "sum_btree_option None = 0" |
1175 "sum_btree_option (Some t) = sum_btree t"
1178 % * can pretend a nested type is mutually recursive (if purely inductive)
1179 % * avoids the higher-order map
1182 % * this can always be avoided;
1183 % * e.g. in our previous example, we first mapped the recursive
1184 % calls, then we used a generic at function to retrieve the result
1186 % * there's no hard-and-fast rule of when to use one or the other,
1187 % just like there's no rule when to use fold and when to use
1190 % * higher-order approach, considering nesting as nesting, is more
1191 % compositional -- e.g. we saw how we could reuse an existing polymorphic
1192 % at or the_default, whereas @{const ats\<^sub>f\<^sub>f} is much more specific
1195 % * is perhaps less intuitive, because it requires higher-order thinking
1196 % * may seem inefficient, and indeed with the code generator the
1197 % mutually recursive version might be nicer
1198 % * is somewhat indirect -- must apply a map first, then compute a result
1200 % * the auxiliary functions like @{const ats\<^sub>f\<^sub>f} are sometimes useful in own right
1202 % * impact on automation unclear
1210 subsection {* Command Syntax
1211 \label{ssec:primrec-command-syntax} *}
1214 subsubsection {* \keyw{primrec\_new}
1215 \label{sssec:primrec-new} *}
1218 \begin{matharray}{rcl}
1219 @{command_def "primrec_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
1223 @@{command primrec_new} target? fixes \\ @'where' (@{syntax pr_equation} + '|')
1225 @{syntax_def pr_equation}: thmdecl? prop
1231 subsection {* Generated Theorems
1232 \label{ssec:primrec-generated-theorems} *}
1235 % * synthesized nonrecursive definition
1236 % * user specification is rederived from it, exactly as entered
1240 % * without some needless induction hypotheses if not used
1247 subsection {* Recursive Default Values for Selectors
1248 \label{ssec:primrec-recursive-default-values-for-selectors} *}
1251 A datatype selector @{text un_D} can have a default value for each constructor
1252 on which it is not otherwise specified. Occasionally, it is useful to have the
1253 default value be defined recursively. This produces a chicken-and-egg situation
1254 that may seem unsolvable, because the datatype is not introduced yet at the
1255 moment when the selectors are introduced. Of course, we can always define the
1256 selectors manually afterward, but we then have to state and prove all the
1257 characteristic theorems ourselves instead of letting the package do it.
1259 Fortunately, there is a fairly elegant workaround that relies on overloading and
1260 that avoids the tedium of manual derivations:
1263 \setlength{\itemsep}{0pt}
1266 Introduce a fully unspecified constant @{text "un_D\<^sub>0 \<Colon> 'a"} using
1270 Define the datatype, specifying @{text "un_D\<^sub>0"} as the selector's default
1274 Define the behavior of @{text "un_D\<^sub>0"} on values of the newly introduced
1275 datatype using the \keyw{overloading} command.
1278 Derive the desired equation on @{text un_D} from the characteristic equations
1279 for @{text "un_D\<^sub>0"}.
1283 The following example illustrates this procedure:
1286 consts termi\<^sub>0 :: 'a
1288 text {* \blankline *}
1290 datatype_new ('a, 'b) tlist =
1291 TNil (termi: 'b) (defaults ttl: TNil)
1292 | TCons (thd: 'a) (ttl : "('a, 'b) tlist") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs")
1294 text {* \blankline *}
1297 termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist \<Rightarrow> 'b"
1299 primrec_new termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
1300 "termi\<^sub>0 (TNil y) = y" |
1301 "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
1304 text {* \blankline *}
1306 lemma terminal_TCons[simp]: "termi (TCons x xs) = termi xs"
1311 subsection {* Compatibility Issues
1312 \label{ssec:primrec-compatibility-issues} *}
1315 % * different induction in nested case
1316 % * solution: define nested-as-mutual functions with primrec,
1317 % and look at .induct
1319 % * different induction and recursor in nested case
1320 % * only matters to low-level users; they can define a dummy function to force
1321 % generation of mutualized recursor
1326 section {* Defining Codatatypes
1327 \label{sec:defining-codatatypes} *}
1330 Codatatypes can be specified using the @{command codatatype} command. The
1331 command is first illustrated through concrete examples featuring different
1332 flavors of corecursion. More examples can be found in the directory
1333 \verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs} also
1334 includes some useful codatatypes, notably for lazy lists \cite{lochbihler-2010}.
1338 subsection {* Introductory Examples
1339 \label{ssec:codatatype-introductory-examples} *}
1342 subsubsection {* Simple Corecursion
1343 \label{sssec:codatatype-simple-corecursion} *}
1346 Noncorecursive codatatypes coincide with the corresponding datatypes, so
1347 they have no practical uses. \emph{Corecursive codatatypes} have the same syntax
1348 as recursive datatypes, except for the command name. For example, here is the
1349 definition of lazy lists:
1352 codatatype (lset: 'a) llist (map: lmap rel: llist_all2) =
1353 lnull: LNil (defaults ltl: LNil)
1354 | LCons (lhd: 'a) (ltl: "'a llist")
1358 Lazy lists can be infinite, such as @{text "LCons 0 (LCons 0 (\<dots>))"} and
1359 @{text "LCons 0 (LCons 1 (LCons 2 (\<dots>)))"}. Here is a related type, that of
1363 codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
1364 SCons (shd: 'a) (stl: "'a stream")
1368 Another interesting type that can
1369 be defined as a codatatype is that of the extended natural numbers:
1372 codatatype enat = EZero | ESuc enat
1376 This type has exactly one infinite element, @{text "ESuc (ESuc (ESuc (\<dots>)))"},
1377 that represents $\infty$. In addition, it has finite values of the form
1378 @{text "ESuc (\<dots> (ESuc EZero)\<dots>)"}.
1380 Here is an example with many constructors:
1383 codatatype 'a process =
1385 | Skip (cont: "'a process")
1386 | Action (prefix: 'a) (cont: "'a process")
1387 | Choice (left: "'a process") (right: "'a process")
1391 Notice that the @{const cont} selector is associated with both @{const Skip}
1392 and @{const Choice}.
1396 subsubsection {* Mutual Corecursion
1397 \label{sssec:codatatype-mutual-corecursion} *}
1401 The example below introduces a pair of \emph{mutually corecursive} types:
1404 codatatype even_enat = Even_EZero | Even_ESuc odd_enat
1405 and odd_enat = Odd_ESuc even_enat
1408 subsubsection {* Nested Corecursion
1409 \label{sssec:codatatype-nested-corecursion} *}
1413 The next examples feature \emph{nested corecursion}:
1416 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")
1418 text {* \blankline *}
1420 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")
1422 text {* \blankline *}
1424 codatatype 'a state_machine =
1425 State_Machine (accept: bool) (trans: "'a \<Rightarrow> 'a state_machine")
1428 subsection {* Command Syntax
1429 \label{ssec:codatatype-command-syntax} *}
1432 subsubsection {* \keyw{codatatype}
1433 \label{sssec:codatatype} *}
1436 \begin{matharray}{rcl}
1437 @{command_def "codatatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
1441 @@{command codatatype} target? \\
1442 (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
1446 Definitions of codatatypes have almost exactly the same syntax as for datatypes
1447 (Section~\ref{ssec:datatype-command-syntax}). The @{text "no_discs_sels"} option
1448 is not available, because destructors are a crucial notion for codatatypes.
1452 subsection {* Generated Constants
1453 \label{ssec:codatatype-generated-constants} *}
1456 Given a codatatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
1457 with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
1458 \ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
1459 datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
1460 iterator and the recursor are replaced by dual concepts:
1463 \setlength{\itemsep}{0pt}
1465 \item \relax{Coiterator}: @{text t_unfold}
1467 \item \relax{Corecursor}: @{text t_corec}
1473 subsection {* Generated Theorems
1474 \label{ssec:codatatype-generated-theorems} *}
1477 The characteristic theorems generated by @{command codatatype} are grouped in
1478 three broad categories:
1481 \setlength{\itemsep}{0pt}
1483 \item The \emph{free constructor theorems} are properties about the constructors
1484 and destructors that can be derived for any freely generated type.
1486 \item The \emph{functorial theorems} are properties of datatypes related to
1489 \item The \emph{coinductive theorems} are properties of datatypes related to
1490 their coinductive nature.
1494 The first two categories are exactly as for datatypes and are described in
1496 \ref{sssec:free-constructor-theorems}~and~\ref{sssec:functorial-theorems}.
1500 subsubsection {* Coinductive Theorems
1501 \label{sssec:coinductive-theorems} *}
1504 The coinductive theorems are as follows:
1509 \item[\begin{tabular}{@ {}l@ {}}
1510 @{text "t."}\hthm{coinduct} @{text "[coinduct t, consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
1511 \phantom{@{text "t."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
1513 @{thm llist.coinduct[no_vars]}
1515 \item[\begin{tabular}{@ {}l@ {}}
1516 @{text "t."}\hthm{strong\_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
1517 \phantom{@{text "t."}\hthm{strong\_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
1519 @{thm llist.strong_coinduct[no_vars]}
1521 \item[\begin{tabular}{@ {}l@ {}}
1522 @{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]"} \\
1523 @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong\_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
1524 \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong\_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
1526 Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be
1527 used to prove $m$ properties simultaneously.
1529 \item[@{text "t."}\hthm{unfold} \rm(@{text "[simp]"})\rm:] ~ \\
1530 @{thm llist.unfold(1)[no_vars]} \\
1531 @{thm llist.unfold(2)[no_vars]}
1533 \item[@{text "t."}\hthm{corec} (@{text "[simp]"})\rm:] ~ \\
1534 @{thm llist.corec(1)[no_vars]} \\
1535 @{thm llist.corec(2)[no_vars]}
1537 \item[@{text "t."}\hthm{disc\_unfold}\rm:] ~ \\
1538 @{thm llist.disc_unfold(1)[no_vars]} \\
1539 @{thm llist.disc_unfold(2)[no_vars]}
1541 \item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\
1542 @{thm llist.disc_corec(1)[no_vars]} \\
1543 @{thm llist.disc_corec(2)[no_vars]}
1545 \item[@{text "t."}\hthm{disc\_unfold\_iff} @{text "[simp]"}\rm:] ~ \\
1546 @{thm llist.disc_unfold_iff(1)[no_vars]} \\
1547 @{thm llist.disc_unfold_iff(2)[no_vars]}
1549 \item[@{text "t."}\hthm{disc\_corec\_iff} @{text "[simp]"}\rm:] ~ \\
1550 @{thm llist.disc_corec_iff(1)[no_vars]} \\
1551 @{thm llist.disc_corec_iff(2)[no_vars]}
1553 \item[@{text "t."}\hthm{sel\_unfold} @{text "[simp]"}\rm:] ~ \\
1554 @{thm llist.sel_unfold(1)[no_vars]} \\
1555 @{thm llist.sel_unfold(2)[no_vars]}
1557 \item[@{text "t."}\hthm{sel\_corec} @{text "[simp]"}\rm:] ~ \\
1558 @{thm llist.sel_corec(1)[no_vars]} \\
1559 @{thm llist.sel_corec(2)[no_vars]}
1565 For convenience, @{command codatatype} also provides the following collection:
1570 \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec}$^*$ @{text t.disc_corec}] ~ \\
1571 @{text t.disc_corec_iff} @{text t.sel_corec} @{text t.unfold}$^*$ @{text t.disc_unfold} @{text t.disc_unfold_iff} ~ \\
1572 @{text t.sel_unfold} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
1579 section {* Defining Corecursive Functions
1580 \label{sec:defining-corecursive-functions} *}
1583 Corecursive functions can be specified using @{command primcorec} and
1584 @{command primcorecursive}, which support primitive corecursion, or using the
1585 more general \keyw{partial\_function} command. Here, the focus is on
1586 the former two. More examples can be found in the directory
1587 \verb|~~/src/HOL/BNF/Examples|.
1589 Whereas recursive functions consume datatypes one constructor at a time,
1590 corecursive functions construct codatatypes one constructor at a time.
1591 Partly reflecting a lack of agreement among proponents of coalgebraic methods,
1592 Isabelle supports three competing syntaxes for specifying a function $f$:
1595 \setlength{\itemsep}{0pt}
1597 \abovedisplayskip=.5\abovedisplayskip
1598 \belowdisplayskip=.5\belowdisplayskip
1600 \item The \emph{destructor view} specifies $f$ by implications of the form
1601 \[@{text "\<dots> \<Longrightarrow> is_C\<^sub>j (f x\<^sub>1 \<dots> x\<^sub>n)"}\] and
1602 equations of the form
1603 \[@{text "un_C\<^sub>ji (f x\<^sub>1 \<dots> x\<^sub>n) = \<dots>"}\]
1604 This style is popular in the coalgebraic literature.
1606 \item The \emph{constructor view} specifies $f$ by equations of the form
1607 \[@{text "\<dots> \<Longrightarrow> f x\<^sub>1 \<dots> x\<^sub>n = C \<dots>"}\]
1608 This style is often more concise than the previous one.
1610 \item The \emph{code view} specifies $f$ by a single equation of the form
1611 \[@{text "f x\<^sub>1 \<dots> x\<^sub>n = \<dots>"}\]
1612 with restrictions on the format of the right-hand side. Lazy functional
1613 programming languages such as Haskell support a generalized version of this
1617 All three styles are available as input syntax. Whichever syntax is chosen,
1618 characteristic theorems for all three styles are generated.
1622 \textbf{Warning:}\enskip The @{command primcorec} and @{command primcorecursive}
1623 commands are under development. Some of the functionality described here is
1624 vaporware. An alternative is to define corecursive functions directly using the
1625 generated @{text t_unfold} or @{text t_corec} combinators.
1628 %%% TODO: partial_function? E.g. for defining tail recursive function on lazy
1629 %%% lists (cf. terminal0 in TLList.thy)
1633 subsection {* Introductory Examples
1634 \label{ssec:primcorec-introductory-examples} *}
1637 Primitive corecursion is illustrated through concrete examples based on the
1638 codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
1639 examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|. The code
1640 view is favored in the examples below. Sections
1641 \ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
1642 present the same examples expressed using the constructor and destructor views.
1650 subsubsection {* Simple Corecursion
1651 \label{sssec:primcorec-simple-corecursion} *}
1654 Following the code view, corecursive calls are allowed on the right-hand side as
1655 long as they occur under a constructor, which itself appears either directly to
1656 the right of the equal sign or in a conditional expression:
1659 primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
1660 "literate f x = LCons x (literate f (f x))"
1662 text {* \blankline *}
1664 primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
1665 "siterate f x = SCons x (siterate f (f x))"
1669 The constructor ensures that progress is made---i.e., the function is
1670 \emph{productive}. The above functions compute the infinite lazy list or stream
1671 @{text "[x, f x, f (f x), \<dots>]"}. Productivity guarantees that prefixes
1672 @{text "[x, f x, f (f x), \<dots>, (f ^^ k) x]"} of arbitrary finite length
1673 @{text k} can be computed by unfolding the code equation a finite number of
1674 times. The period (\keyw{.}) at the end of the commands discharge the zero proof
1677 Corecursive functions construct codatatype values, but nothing prevents them
1678 from also consuming such values. The following function drops ever second
1679 element in a stream:
1682 primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
1683 "every_snd s = SCons (shd s) (stl (stl s))"
1687 Constructs such as @{text "let"}---@{text "in"}, @{text
1688 "if"}---@{text "then"}---@{text "else"}, and @{text "case"}---@{text "of"} may
1689 appear around constructors that guard corecursive calls:
1692 primcorec_notyet lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
1695 LNil \<Rightarrow> ys
1696 | LCons x xs' \<Rightarrow> LCons x (lappend xs' ys))"
1700 Corecursion is useful to specify not only functions but also infinite objects:
1703 primcorec infty :: enat where
1704 "infty = ESuc infty"
1708 The example below constructs a pseudorandom process value. It takes a stream of
1709 actions (@{text s}), a pseudorandom function generator (@{text f}), and a
1710 pseudorandom seed (@{text n}):
1714 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
1716 "random_process s f n =
1717 (if n mod 4 = 0 then
1719 else if n mod 4 = 1 then
1720 Skip (random_process s f (f n))
1721 else if n mod 4 = 2 then
1722 Action (shd s) (random_process (stl s) f (f n))
1724 Choice (random_process (every_snd s) (f \<circ> f) (f n))
1725 (random_process (every_snd (stl s)) (f \<circ> f) (f (f n))))"
1729 The main disadvantage of the code view is that the conditions are tested
1730 sequentially. This is visible in the generated theorems. The constructor and
1731 destructor views offer nonsequential alternatives.
1735 subsubsection {* Mutual Corecursion
1736 \label{sssec:primcorec-mutual-corecursion} *}
1739 The syntax for mutually corecursive functions over mutually corecursive
1740 datatypes is unsurprising:
1744 even_infty :: even_enat and
1745 odd_infty :: odd_enat
1747 "even_infty = Even_ESuc odd_infty" |
1748 "odd_infty = Odd_ESuc even_infty"
1751 subsubsection {* Nested Corecursion
1752 \label{sssec:primcorec-nested-corecursion} *}
1755 The next pair of examples generalize the @{const literate} and @{const siterate}
1756 functions (Section~\ref{sssec:primcorec-nested-corecursion}) to possibly
1757 infinite trees in which subnodes are organized either as a lazy list (@{text
1758 tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}):
1761 primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
1762 "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i f) (f x))"
1764 text {* \blankline *}
1766 primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
1767 "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fmap (iterate\<^sub>i\<^sub>s f) (f x))"
1771 Deterministic finite automata (DFAs) are usually defined as 5-tuples
1772 @{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,
1773 @{text \<Sigma>} is a finite alphabet, @{text \<delta>} is a transition function, @{text q\<^sub>0}
1774 is an initial state, and @{text F} is a set of final states. The following
1775 function translates a DFA into a @{type state_machine}:
1778 primcorec (*<*)(in early) (*>*)
1779 sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
1781 "sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (sm_of_dfa \<delta> F o \<delta> q)"
1785 The map function for the function type (@{text \<Rightarrow>}) is composition
1786 (@{text "op \<circ>"}). For convenience, corecursion through functions can be
1787 expressed using @{text \<lambda>}-expressions and function application rather
1788 than composition. For example:
1792 sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
1794 "sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (sm_of_dfa \<delta> F o \<delta> q)"
1796 text {* \blankline *}
1798 primcorec empty_sm :: "'a state_machine" where
1799 "empty_sm = State_Machine False (\<lambda>_. empty_sm)"
1801 text {* \blankline *}
1803 primcorec not_sm :: "'a state_machine \<Rightarrow> 'a state_machine" where
1804 "not_sm M = State_Machine (\<not> accept M) (\<lambda>a. not_sm (trans M a))"
1806 text {* \blankline *}
1809 or_sm :: "'a state_machine \<Rightarrow> 'a state_machine \<Rightarrow> 'a state_machine"
1812 State_Machine (accept M \<or> accept N)
1813 (\<lambda>a. or_sm (trans M a) (trans N a))"
1816 subsubsection {* Nested-as-Mutual Corecursion
1817 \label{sssec:primcorec-nested-as-mutual-corecursion} *}
1820 Just as it is possible to recurse over nested recursive datatypes as if they
1821 were mutually recursive
1822 (Section~\ref{sssec:primrec-nested-as-mutual-recursion}), it is possible to
1823 pretend that nested codatatypes are mutually corecursive. For example:
1827 iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" and
1828 iterates\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a llist \<Rightarrow> 'a tree\<^sub>i\<^sub>i llist"
1830 "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (iterates\<^sub>i\<^sub>i f (f x))" |
1831 "iterates\<^sub>i\<^sub>i f xs =
1833 LNil \<Rightarrow> LNil
1834 | LCons x xs' \<Rightarrow> LCons (iterate\<^sub>i\<^sub>i f x) (iterates\<^sub>i\<^sub>i f xs'))"
1840 subsubsection {* Constructor View
1841 \label{ssec:primrec-constructor-view} *}
1844 locale ctr_view = code_view
1849 The constructor view is similar to the code view, but there is one separate
1850 conditional equation per constructor rather than a single unconditional
1851 equation. Examples that rely on a single constructor, such as @{const literate}
1852 and @{const siterate}, are identical in both styles.
1854 Here is an example where there is a difference:
1857 primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
1858 "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lappend xs ys = LNil" |
1859 "_ \<Longrightarrow> lappend xs ys = LCons (lhd (if lnull xs then ys else xs))
1860 (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
1864 With the constructor view, we must distinguish between the @{const LNil} and
1865 the @{const LCons} case. The condition for @{const LCons} is
1866 left implicit, as the negation of that for @{const LNil}.
1868 For this example, the constructor view is slighlty more involved than the
1869 code equation. Recall the code view version presented in
1870 Section~\ref{sssec:primcorec-simple-corecursion}.
1871 % TODO: \[{thm code_view.lappend.code}\]
1872 The constructor view requires us to analyze the second argument (@{term ys}).
1873 The code equation generated from the constructor view also suffers from this.
1874 % TODO: \[{thm lappend.code}\]
1876 In contrast, the next example is arguably more naturally expressed in the
1881 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
1883 "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail" |
1884 "n mod 4 = 1 \<Longrightarrow>
1885 random_process s f n = Skip (random_process s f (f n))" |
1886 "n mod 4 = 2 \<Longrightarrow>
1887 random_process s f n = Action (shd s) (random_process (stl s) f (f n))" |
1888 "n mod 4 = 3 \<Longrightarrow>
1889 random_process s f n = Choice (random_process (every_snd s) f (f n))
1890 (random_process (every_snd (stl s)) f (f n))"
1897 Since there is no sequentiality, we can apply the equation for @{const Choice}
1898 without having first to discharge @{term "n mod (4\<Colon>int) \<noteq> 0"},
1899 @{term "n mod (4\<Colon>int) \<noteq> 1"}, and
1900 @{term "n mod (4\<Colon>int) \<noteq> 2"}.
1901 The price to pay for this elegance is that we must discharge exclusivity proof
1902 obligations, one for each pair of conditions
1903 @{term "(n mod (4\<Colon>int) = i, n mod (4\<Colon>int) = j)"}
1904 with @{term "i < j"}. If we prefer not to discharge any obligations, we can
1905 enable the @{text "sequential"} option. This pushes the problem to the users of
1906 the generated properties.
1907 %Here are more examples to conclude:
1911 subsubsection {* Destructor View
1912 \label{ssec:primrec-destructor-view} *}
1920 The destructor view is in many respects dual to the constructor view. Conditions
1921 determine which constructor to choose, and these conditions are interpreted
1922 sequentially or not depending on the @{text "sequential"} option.
1923 Consider the following examples:
1926 primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
1927 "\<not> lnull (literate _ x)" |
1928 "lhd (literate _ x) = x" |
1929 "ltl (literate f x) = literate f (f x)"
1931 text {* \blankline *}
1933 primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
1934 "shd (siterate _ x) = x" |
1935 "stl (siterate f x) = siterate f (f x)"
1937 text {* \blankline *}
1939 primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
1940 "shd (every_snd s) = shd s" |
1941 "stl (every_snd s) = stl (stl s)"
1945 The first formula in the @{const literate} specification indicates which
1946 constructor to choose. For @{const siterate} and @{const every_snd}, no such
1947 formula is necessary, since the type has only one constructor. The last two
1948 formulas are equations specifying the value of the result for the relevant
1949 selectors. Corecursive calls appear directly to the right of the equal sign.
1950 Their arguments are unrestricted.
1952 The next example shows how to specify functions that rely on more than one
1956 primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
1957 "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
1958 "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
1959 "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
1963 For a codatatype with $n$ constructors, it is sufficient to specify $n - 1$
1964 discriminator formulas. The command will then assume that the remaining
1965 constructor should be taken otherwise. This can be made explicit by adding
1971 primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
1972 "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
1974 "_ \<Longrightarrow> \<not> lnull (lappend xs ys)"
1976 "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
1977 "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
1979 context dest_view begin
1984 to the specification. The generated selector theorems are conditional.
1986 The next example illustrates how to cope with selectors defined for several
1991 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
1993 "n mod 4 = 0 \<Longrightarrow> is_Fail (random_process s f n)" |
1994 "n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)" |
1995 "n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)" |
1996 "n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)" |
1997 "cont (random_process s f n) = random_process s f (f n)" of Skip |
1998 "prefix (random_process s f n) = shd s" |
1999 "cont (random_process s f n) = random_process (stl s) f (f n)" of Action |
2000 "left (random_process s f n) = random_process (every_snd s) f (f n)" |
2001 "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)"
2005 Using the @{text "of"} keyword, different equations are specified for @{const
2006 cont} depending on which constructor is selected.
2008 Here are more examples to conclude:
2012 even_infty :: even_enat and
2013 odd_infty :: odd_enat
2015 "\<not> is_Even_EZero even_infty" |
2016 "un_Even_ESuc even_infty = odd_infty" |
2017 "un_Odd_ESuc odd_infty = even_infty"
2019 text {* \blankline *}
2021 primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
2022 "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = x" |
2023 "sub\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = lmap (iterate\<^sub>i\<^sub>i f) (f x)"
2029 subsection {* Command Syntax
2030 \label{ssec:primcorec-command-syntax} *}
2033 subsubsection {* \keyw{primcorec} and \keyw{primcorecursive}
2034 \label{sssec:primcorecursive-and-primcorec} *}
2037 \begin{matharray}{rcl}
2038 @{command_def "primcorec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
2039 @{command_def "primcorecursive"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
2043 (@@{command primcorec} | @@{command primcorecursive}) target? \\ @{syntax pcr_option}? fixes @'where'
2044 (@{syntax pcr_formula} + '|')
2046 @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')'
2048 @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
2051 The optional target is optionally followed by a corecursion-specific option:
2054 \setlength{\itemsep}{0pt}
2057 The @{text "sequential"} option indicates that the conditions in specifications
2058 expressed using the constructor or destructor view are to be interpreted
2062 The @{text "exhaustive"} option indicates that the conditions in specifications
2063 expressed using the constructor or destructor view cover all possible cases.
2067 The @{command primcorec} command is an abbreviation for @{command primcorecursive} with
2068 @{text "by auto?"} to discharge any emerging proof obligations.
2073 subsection {* Generated Theorems
2074 \label{ssec:primcorec-generated-theorems} *}
2079 subsection {* Recursive Default Values for Selectors
2080 \label{ssec:primcorec-recursive-default-values-for-selectors} *}
2083 partial_function to the rescue
2088 section {* Registering Bounded Natural Functors
2089 \label{sec:registering-bounded-natural-functors} *}
2092 The (co)datatype package can be set up to allow nested recursion through
2093 arbitrary type constructors, as long as they adhere to the BNF requirements and
2094 are registered as BNFs.
2099 subsection {* Introductory Example
2100 \label{ssec:bnf-introductory-example} *}
2103 More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and
2104 \verb|~~/src/HOL/BNF/More_BNFs.thy|.
2106 %Mention distinction between live and dead type arguments;
2107 % * and existence of map, set for those
2113 subsection {* Command Syntax
2114 \label{ssec:bnf-command-syntax} *}
2117 subsubsection {* \keyw{bnf}
2118 \label{sssec:bnf} *}
2121 \begin{matharray}{rcl}
2122 @{command_def "bnf"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
2126 @@{command bnf} target? (name ':')? term \\
2127 term_list term term_list term?
2129 X_list: '[' (X + ',') ']'
2134 subsubsection {* \keyw{print\_bnfs}
2135 \label{sssec:print-bnfs} *}
2138 \begin{matharray}{rcl}
2139 @{command_def "print_bnfs"} & : & @{text "local_theory \<rightarrow>"}
2143 @@{command print_bnfs}
2148 section {* Deriving Destructors and Theorems for Free Constructors
2149 \label{sec:deriving-destructors-and-theorems-for-free-constructors} *}
2152 The derivation of convenience theorems for types equipped with free constructors,
2153 as performed internally by @{command datatype_new} and @{command codatatype},
2154 is available as a stand-alone command called @{command wrap_free_constructors}.
2156 % * need for this is rare but may arise if you want e.g. to add destructors to
2157 % a type not introduced by ...
2159 % * also useful for compatibility with old package, e.g. add destructors to
2160 % old \keyw{datatype}
2162 % * @{command wrap_free_constructors}
2163 % * @{text "no_discs_sels"}, @{text "rep_compat"}
2164 % * hack to have both co and nonco view via locale (cf. ext nats)
2169 subsection {* Introductory Example
2170 \label{ssec:ctors-introductory-example} *}
2174 subsection {* Command Syntax
2175 \label{ssec:ctors-command-syntax} *}
2178 subsubsection {* \keyw{wrap\_free\_constructors}
2179 \label{sssec:wrap-free-constructors} *}
2182 \begin{matharray}{rcl}
2183 @{command_def "wrap_free_constructors"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
2187 @@{command wrap_free_constructors} target? @{syntax dt_options} \\
2188 term_list name @{syntax fc_discs_sels}?
2190 @{syntax_def fc_discs_sels}: name_list (name_list_list name_term_list_list? )?
2192 @{syntax_def name_term}: (name ':' term)
2195 % options: no_discs_sels rep_compat
2197 % X_list is as for BNF
2200 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
2205 section {* Standard ML Interface
2206 \label{sec:standard-ml-interface} *}
2209 The package's programmatic interface.
2215 section {* Interoperability
2216 \label{sec:interoperability} *}
2219 The package's interaction with other Isabelle packages and tools, such as the
2220 code generator and the counterexample generators.
2224 subsection {* Transfer and Lifting
2225 \label{ssec:transfer-and-lifting} *}
2228 subsection {* Code Generator
2229 \label{ssec:code-generator} *}
2232 subsection {* Quickcheck
2233 \label{ssec:quickcheck} *}
2236 subsection {* Nitpick
2237 \label{ssec:nitpick} *}
2240 subsection {* Nominal Isabelle
2241 \label{ssec:nominal-isabelle} *}
2246 section {* Known Bugs and Limitations
2247 \label{sec:known-bugs-and-limitations} *}
2250 Known open issues of the package.
2254 %* primcorecursive and primcorec is unfinished
2256 %* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
2258 %* issues with HOL-Proofs?
2260 %* partial documentation
2262 %* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
2263 % (for @{command datatype_new_compat} and prim(co)rec)
2265 % * a fortiori, no way to register same type as both data- and codatatype
2267 %* no recursion through unused arguments (unlike with the old package)
2269 %* in a locale, cannot use locally fixed types (because of limitation in typedef)?
2271 % *names of variables suboptimal
2276 section {* Acknowledgments
2277 \label{sec:acknowledgments} *}
2280 Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
2281 (co)datatype package. Andreas Lochbihler provided lots of comments on earlier
2282 versions of the package, especially for the coinductive part. Brian Huffman
2283 suggested major simplifications to the internal constructions, much of which has
2284 yet to be implemented. Florian Haftmann and Christian Urban provided general
2285 advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder
2286 suggested an elegant proof to eliminate one of the BNF assumptions.