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 replace \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 forgive 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"
247 Occurrences of nonatomic types on the right-hand side of the equal sign must be
248 enclosed in double quotes, as is customary in Isabelle.
252 subsubsection {* Simple Recursion
253 \label{sssec:datatype-simple-recursion} *}
256 Natural numbers are the simplest example of a recursive type:
259 datatype_new nat = Zero | Suc nat
263 Lists were shown in the introduction. Terminated lists are a variant:
266 datatype_new (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
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 syntax annotations are available for both types and
406 constructors. For example:
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 syntax 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 entity \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 entity \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 are 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 depend 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 cases 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 is 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} @{text "[dest]"}\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 nonnull}, they would have read thusly: \\[\jot]
778 @{prop "null list \<Longrightarrow> \<not> nonnull list"} \\
779 @{prop "nonnull 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{sel\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
785 @{thm list.sel_exhaust[no_vars]}
787 \item[@{text "t."}\hthm{expand}\rm:] ~ \\
788 @{thm list.expand[no_vars]}
790 \item[@{text "t."}\hthm{sel\_split}\rm:] ~ \\
791 @{thm list.sel_split[no_vars]}
793 \item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\
794 @{thm list.sel_split_asm[no_vars]}
796 \item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\
797 @{thm list.case_conv_if[no_vars]}
804 subsubsection {* Functorial Theorems
805 \label{sssec:functorial-theorems} *}
808 The BNF-related theorem are as follows:
813 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
814 @{thm list.set(1)[no_vars]} \\
815 @{thm list.set(2)[no_vars]}
817 \item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
818 @{thm list.map(1)[no_vars]} \\
819 @{thm list.map(2)[no_vars]}
821 \item[@{text "t."}\hthm{rel\_inject} @{text "[simp, code]"}\rm:] ~ \\
822 @{thm list.rel_inject(1)[no_vars]} \\
823 @{thm list.rel_inject(2)[no_vars]}
825 \item[@{text "t."}\hthm{rel\_distinct} @{text "[simp, code]"}\rm:] ~ \\
826 @{thm list.rel_distinct(1)[no_vars]} \\
827 @{thm list.rel_distinct(2)[no_vars]}
834 subsubsection {* Inductive Theorems
835 \label{sssec:inductive-theorems} *}
838 The inductive theorems are as follows:
843 \item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
844 @{thm list.induct[no_vars]}
846 \item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
847 Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
848 prove $m$ properties simultaneously.
850 \item[@{text "t."}\hthm{fold} @{text "[simp, code]"}\rm:] ~ \\
851 @{thm list.fold(1)[no_vars]} \\
852 @{thm list.fold(2)[no_vars]}
854 \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
855 @{thm list.rec(1)[no_vars]} \\
856 @{thm list.rec(2)[no_vars]}
862 For convenience, @{command datatype_new} also provides the following collection:
867 \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}] ~ \\
868 @{text t.rel_distinct} @{text t.set}
875 subsection {* Compatibility Issues
876 \label{ssec:datatype-compatibility-issues} *}
879 The command @{command datatype_new} has been designed to be highly compatible
880 with the old \keyw{datatype}, to ease migration. There are nonetheless a few
881 incompatibilities that may arise when porting to the new package:
884 \setlength{\itemsep}{0pt}
886 \item \emph{The Standard ML interfaces are different.} Tools and extensions
887 written to call the old ML interfaces will need to be adapted to the new
888 interfaces. Little has been done so far in this direction. Whenever possible, it
889 is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype}
890 to register new-style datatypes as old-style datatypes.
892 \item \emph{The recursor @{text "t_rec"} has a different signature for nested
893 recursive datatypes.} In the old package, nested recursion was internally
894 reduced to mutual recursion. This reduction was visible in the type of the
895 recursor, used by \keyw{primrec}. In the new package, nested recursion is
896 handled in a more modular fashion. The old-style recursor can be generated on
897 demand using @{command primrec_new}, as explained in
898 Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
901 \item \emph{Accordingly, the induction principle is different for nested
902 recursive datatypes.} Again, the old-style induction principle can be generated
903 on demand using @{command primrec_new}, as explained in
904 Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
907 \item \emph{The internal constructions are completely different.} Proof texts
908 that unfold the definition of constants introduced by \keyw{datatype} will be
911 \item \emph{A few theorems have different names.}
912 The properties @{text t.cases} and @{text t.recs} have been renamed
913 @{text t.case} and @{text t.rec}. For non-mutually recursive datatypes,
914 @{text t.inducts} is available as @{text t.induct}.
915 For $m > 1$ mutually recursive datatypes,
916 @{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
917 @{text "t\<^sub>i.induct"}.
919 \item \emph{The @{text t.simps} collection has been extended.}
920 Previously available theorems are available at the same index.
922 \item \emph{Variables in generated properties have different names.} This is
923 rarely an issue, except in proof texts that refer to variable names in the
924 @{text "[where \<dots>]"} attribute. The solution is to use the more robust
925 @{text "[of \<dots>]"} syntax.
928 In the other direction, there is currently no way to register old-style
929 datatypes as new-style datatypes. If the goal is to define new-style datatypes
930 with nested recursion through old-style datatypes, the old-style
931 datatypes can be registered as a BNF
932 (Section~\ref{sec:registering-bounded-natural-functors}). If the goal is
933 to derive discriminators and selectors, this can be achieved using @{command
934 wrap_free_constructors}
935 (Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
939 section {* Defining Recursive Functions
940 \label{sec:defining-recursive-functions} *}
943 Recursive functions over datatypes can be specified using @{command
944 primrec_new}, which supports primitive recursion, or using the more general
945 \keyw{fun} and \keyw{function} commands. Here, the focus is on @{command
946 primrec_new}; the other two commands are described in a separate tutorial
947 \cite{isabelle-function}.
949 %%% TODO: partial_function
953 subsection {* Introductory Examples
954 \label{ssec:primrec-introductory-examples} *}
957 Primitive recursion is illustrated through concrete examples based on the
958 datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
959 examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|.
963 subsubsection {* Nonrecursive Types
964 \label{sssec:primrec-nonrecursive-types} *}
967 Primitive recursion removes one layer of constructors on the left-hand side in
968 each equation. For example:
971 primrec_new bool_of_trool :: "trool \<Rightarrow> bool" where
972 "bool_of_trool Faalse \<longleftrightarrow> False" |
973 "bool_of_trool Truue \<longleftrightarrow> True"
975 text {* \blankline *}
977 primrec_new the_list :: "'a option \<Rightarrow> 'a list" where
978 "the_list None = []" |
979 "the_list (Some a) = [a]"
981 text {* \blankline *}
983 primrec_new the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
984 "the_default d None = d" |
985 "the_default _ (Some a) = a"
987 text {* \blankline *}
989 primrec_new mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
990 "mirrror (Triple a b c) = Triple c b a"
994 The equations can be specified in any order, and it is acceptable to leave out
995 some cases, which are then unspecified. Pattern matching on the left-hand side
996 is restricted to a single datatype, which must correspond to the same argument
1001 subsubsection {* Simple Recursion
1002 \label{sssec:primrec-simple-recursion} *}
1005 For simple recursive types, recursive calls on a constructor argument are
1006 allowed on the right-hand side:
1009 primrec_new replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
1010 "replicate Zero _ = []" |
1011 "replicate (Suc n) x = x # replicate n x"
1013 text {* \blankline *}
1015 primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
1018 Zero \<Rightarrow> x
1019 | Suc j' \<Rightarrow> at xs j')"
1021 text {* \blankline *}
1023 primrec_new (*<*)(in early) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
1024 "tfold _ (TNil y) = y" |
1025 "tfold f (TCons x xs) = f x (tfold f xs)"
1029 The next example is not primitive recursive, but it can be defined easily using
1030 \keyw{fun}. The @{command datatype_new_compat} command is needed to register
1031 new-style datatypes for use with \keyw{fun} and \keyw{function}
1032 (Section~\ref{sssec:datatype-new-compat}):
1035 datatype_new_compat nat
1037 text {* \blankline *}
1039 fun at_least_two :: "nat \<Rightarrow> bool" where
1040 "at_least_two (Suc (Suc _)) \<longleftrightarrow> True" |
1041 "at_least_two _ \<longleftrightarrow> False"
1044 subsubsection {* Mutual Recursion
1045 \label{sssec:primrec-mutual-recursion} *}
1048 The syntax for mutually recursive functions over mutually recursive datatypes
1053 nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
1054 nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
1056 "nat_of_even_nat Even_Zero = Zero" |
1057 "nat_of_even_nat (Even_Suc n) = Suc (nat_of_odd_nat n)" |
1058 "nat_of_odd_nat (Odd_Suc n) = Suc (nat_of_even_nat n)"
1060 text {* \blankline *}
1063 eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
1064 eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and
1065 eval\<^sub>f :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) fct \<Rightarrow> int"
1067 "eval\<^sub>e \<gamma> \<xi> (Term t) = eval\<^sub>t \<gamma> \<xi> t" |
1068 "eval\<^sub>e \<gamma> \<xi> (Sum t e) = eval\<^sub>t \<gamma> \<xi> t + eval\<^sub>e \<gamma> \<xi> e" |
1069 "eval\<^sub>t \<gamma> \<xi> (Factor f) = eval\<^sub>f \<gamma> \<xi> f" |
1070 "eval\<^sub>t \<gamma> \<xi> (Prod f t) = eval\<^sub>f \<gamma> \<xi> f + eval\<^sub>t \<gamma> \<xi> t" |
1071 "eval\<^sub>f \<gamma> _ (Const a) = \<gamma> a" |
1072 "eval\<^sub>f _ \<xi> (Var b) = \<xi> b" |
1073 "eval\<^sub>f \<gamma> \<xi> (Expr e) = eval\<^sub>e \<gamma> \<xi> e"
1077 Mutual recursion is possible within a single type, using \keyw{fun}:
1081 even :: "nat \<Rightarrow> bool" and
1082 odd :: "nat \<Rightarrow> bool"
1084 "even Zero = True" |
1085 "even (Suc n) = odd n" |
1086 "odd Zero = False" |
1087 "odd (Suc n) = even n"
1090 subsubsection {* Nested Recursion
1091 \label{sssec:primrec-nested-recursion} *}
1094 In a departure from the old datatype package, nested recursion is normally
1095 handled via the map functions of the nesting type constructors. For example,
1096 recursive calls are lifted to lists using @{const map}:
1100 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")
1102 primrec_new at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
1103 "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
1106 | j # js' \<Rightarrow> at (map (\<lambda>t. at\<^sub>f\<^sub>f t js') ts) j)"
1110 The next example features recursion through the @{text option} type. Although
1111 @{text option} is not a new-style datatype, it is registered as a BNF with the
1112 map function @{const option_map}:
1115 primrec_new (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
1116 "sum_btree (BNode a lt rt) =
1117 a + the_default 0 (option_map sum_btree lt) +
1118 the_default 0 (option_map sum_btree rt)"
1122 The same principle applies for arbitrary type constructors through which
1123 recursion is possible. Notably, the map function for the function type
1124 (@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
1127 primrec_new (*<*)(in early) (*>*)ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
1128 "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
1129 "ftree_map f (FTNode g) = FTNode (ftree_map f \<circ> g)"
1133 (No such map function is defined by the package because the type
1134 variable @{typ 'a} is dead in @{typ "'a ftree"}.)
1136 Using \keyw{fun} or \keyw{function}, recursion through functions can be
1137 expressed using $\lambda$-expressions and function application rather
1138 than through composition. For example:
1141 datatype_new_compat ftree
1143 text {* \blankline *}
1145 function ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
1146 "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
1147 "ftree_map f (FTNode g) = FTNode (\<lambda>x. ftree_map f (g x))"
1148 by auto (metis ftree.exhaust)
1151 subsubsection {* Nested-as-Mutual Recursion
1152 \label{sssec:primrec-nested-as-mutual-recursion} *}
1159 For compatibility with the old package, but also because it is sometimes
1160 convenient in its own right, it is possible to treat nested recursive datatypes
1161 as mutually recursive ones if the recursion takes place though new-style
1162 datatypes. For example:
1166 at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" and
1167 ats\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a"
1169 "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
1172 | j # js' \<Rightarrow> ats\<^sub>f\<^sub>f ts j js')" |
1173 "ats\<^sub>f\<^sub>f (t # ts) j =
1175 Zero \<Rightarrow> at\<^sub>f\<^sub>f t
1176 | Suc j' \<Rightarrow> ats\<^sub>f\<^sub>f ts j')"
1180 Appropriate induction principles are generated under the names
1181 @{thm [source] at\<^sub>f\<^sub>f.induct},
1182 @{thm [source] ats\<^sub>f\<^sub>f.induct}, and
1183 @{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}.
1185 %%% TODO: Add recursors.
1187 Here is a second example:
1191 sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" and
1192 sum_btree_option :: "'a btree option \<Rightarrow> 'a"
1194 "sum_btree (BNode a lt rt) =
1195 a + sum_btree_option lt + sum_btree_option rt" |
1196 "sum_btree_option None = 0" |
1197 "sum_btree_option (Some t) = sum_btree t"
1200 % * can pretend a nested type is mutually recursive (if purely inductive)
1201 % * avoids the higher-order map
1204 % * this can always be avoided;
1205 % * e.g. in our previous example, we first mapped the recursive
1206 % calls, then we used a generic at function to retrieve the result
1208 % * there's no hard-and-fast rule of when to use one or the other,
1209 % just like there's no rule when to use fold and when to use
1212 % * higher-order approach, considering nesting as nesting, is more
1213 % compositional -- e.g. we saw how we could reuse an existing polymorphic
1214 % at or the_default, whereas @{const ats\<^sub>f\<^sub>f} is much more specific
1217 % * is perhaps less intuitive, because it requires higher-order thinking
1218 % * may seem inefficient, and indeed with the code generator the
1219 % mutually recursive version might be nicer
1220 % * is somewhat indirect -- must apply a map first, then compute a result
1222 % * the auxiliary functions like @{const ats\<^sub>f\<^sub>f} are sometimes useful in own right
1224 % * impact on automation unclear
1232 subsection {* Command Syntax
1233 \label{ssec:primrec-command-syntax} *}
1236 subsubsection {* \keyw{primrec\_new}
1237 \label{sssec:primrec-new} *}
1240 \begin{matharray}{rcl}
1241 @{command_def "primrec_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
1245 @@{command primrec_new} target? fixes \\ @'where' (@{syntax pr_equation} + '|')
1247 @{syntax_def pr_equation}: thmdecl? prop
1253 subsection {* Generated Theorems
1254 \label{ssec:primrec-generated-theorems} *}
1257 % * synthesized nonrecursive definition
1258 % * user specification is rederived from it, exactly as entered
1262 % * without some needless induction hypotheses if not used
1269 subsection {* Recursive Default Values for Selectors
1270 \label{ssec:primrec-recursive-default-values-for-selectors} *}
1273 A datatype selector @{text un_D} can have a default value for each constructor
1274 on which it is not otherwise specified. Occasionally, it is useful to have the
1275 default value be defined recursively. This produces a chicken-and-egg situation
1276 that may seem unsolvable, because the datatype is not introduced yet at the
1277 moment when the selectors are introduced. Of course, we can always define the
1278 selectors manually afterward, but we then have to state and prove all the
1279 characteristic theorems ourselves instead of letting the package do it.
1281 Fortunately, there is a fairly elegant workaround that relies on overloading and
1282 that avoids the tedium of manual derivations:
1285 \setlength{\itemsep}{0pt}
1288 Introduce a fully unspecified constant @{text "un_D\<^sub>0 \<Colon> 'a"} using
1292 Define the datatype, specifying @{text "un_D\<^sub>0"} as the selector's default
1296 Define the behavior of @{text "un_D\<^sub>0"} on values of the newly introduced
1297 datatype using the \keyw{overloading} command.
1300 Derive the desired equation on @{text un_D} from the characteristic equations
1301 for @{text "un_D\<^sub>0"}.
1305 The following example illustrates this procedure:
1308 consts termi\<^sub>0 :: 'a
1310 text {* \blankline *}
1312 datatype_new ('a, 'b) tlist =
1313 TNil (termi: 'b) (defaults ttl: TNil)
1314 | TCons (thd: 'a) (ttl : "('a, 'b) tlist") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs")
1316 text {* \blankline *}
1319 termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist \<Rightarrow> 'b"
1321 primrec_new termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
1322 "termi\<^sub>0 (TNil y) = y" |
1323 "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
1326 text {* \blankline *}
1328 lemma terminal_TCons[simp]: "termi (TCons x xs) = termi xs"
1332 subsection {* Compatibility Issues
1333 \label{ssec:primrec-compatibility-issues} *}
1336 The command @{command primrec_new} has been designed to be highly compatible
1337 with the old \keyw{primrec}, to ease migration. There is nonetheless at least
1338 one incompatibility that may arise when porting to the new package:
1341 \setlength{\itemsep}{0pt}
1343 \item \emph{Theorems sometimes have different names.}
1344 For $m > 1$ mutually recursive functions,
1345 @{text "f\<^sub>1_\<dots>_f\<^sub>m.simps"} has been broken down into separate
1346 subcollections @{text "f\<^sub>i.simps"}.
1351 section {* Defining Codatatypes
1352 \label{sec:defining-codatatypes} *}
1355 Codatatypes can be specified using the @{command codatatype} command. The
1356 command is first illustrated through concrete examples featuring different
1357 flavors of corecursion. More examples can be found in the directory
1358 \verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|. The
1359 \emph{Archive of Formal Proofs} also includes some useful codatatypes, notably
1360 for lazy lists \cite{lochbihler-2010}.
1364 subsection {* Introductory Examples
1365 \label{ssec:codatatype-introductory-examples} *}
1368 subsubsection {* Simple Corecursion
1369 \label{sssec:codatatype-simple-corecursion} *}
1372 Noncorecursive codatatypes coincide with the corresponding datatypes, so they
1373 are useless in practice. \emph{Corecursive codatatypes} have the same syntax
1374 as recursive datatypes, except for the command name. For example, here is the
1375 definition of lazy lists:
1378 codatatype (lset: 'a) llist (map: lmap rel: llist_all2) =
1379 lnull: LNil (defaults ltl: LNil)
1380 | LCons (lhd: 'a) (ltl: "'a llist")
1384 Lazy lists can be infinite, such as @{text "LCons 0 (LCons 0 (\<dots>))"} and
1385 @{text "LCons 0 (LCons 1 (LCons 2 (\<dots>)))"}. Here is a related type, that of
1389 codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
1390 SCons (shd: 'a) (stl: "'a stream")
1394 Another interesting type that can
1395 be defined as a codatatype is that of the extended natural numbers:
1398 codatatype enat = EZero | ESuc enat
1402 This type has exactly one infinite element, @{text "ESuc (ESuc (ESuc (\<dots>)))"},
1403 that represents $\infty$. In addition, it has finite values of the form
1404 @{text "ESuc (\<dots> (ESuc EZero)\<dots>)"}.
1406 Here is an example with many constructors:
1409 codatatype 'a process =
1411 | Skip (cont: "'a process")
1412 | Action (prefix: 'a) (cont: "'a process")
1413 | Choice (left: "'a process") (right: "'a process")
1417 Notice that the @{const cont} selector is associated with both @{const Skip}
1418 and @{const Choice}.
1422 subsubsection {* Mutual Corecursion
1423 \label{sssec:codatatype-mutual-corecursion} *}
1427 The example below introduces a pair of \emph{mutually corecursive} types:
1430 codatatype even_enat = Even_EZero | Even_ESuc odd_enat
1431 and odd_enat = Odd_ESuc even_enat
1434 subsubsection {* Nested Corecursion
1435 \label{sssec:codatatype-nested-corecursion} *}
1439 The next examples feature \emph{nested corecursion}:
1442 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")
1444 text {* \blankline *}
1446 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")
1448 text {* \blankline *}
1450 codatatype 'a state_machine =
1451 State_Machine (accept: bool) (trans: "'a \<Rightarrow> 'a state_machine")
1454 subsection {* Command Syntax
1455 \label{ssec:codatatype-command-syntax} *}
1458 subsubsection {* \keyw{codatatype}
1459 \label{sssec:codatatype} *}
1462 \begin{matharray}{rcl}
1463 @{command_def "codatatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
1467 @@{command codatatype} target? \\
1468 (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
1472 Definitions of codatatypes have almost exactly the same syntax as for datatypes
1473 (Section~\ref{ssec:datatype-command-syntax}). The @{text "no_discs_sels"} option
1474 is not available, because destructors are a crucial notion for codatatypes.
1478 subsection {* Generated Constants
1479 \label{ssec:codatatype-generated-constants} *}
1482 Given a codatatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
1483 with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
1484 \ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
1485 datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
1486 iterator and the recursor are replaced by dual concepts:
1489 \setlength{\itemsep}{0pt}
1491 \item \relax{Coiterator}: @{text t_unfold}
1493 \item \relax{Corecursor}: @{text t_corec}
1499 subsection {* Generated Theorems
1500 \label{ssec:codatatype-generated-theorems} *}
1503 The characteristic theorems generated by @{command codatatype} are grouped in
1504 three broad categories:
1507 \setlength{\itemsep}{0pt}
1509 \item The \emph{free constructor theorems} are properties about the constructors
1510 and destructors that can be derived for any freely generated type.
1512 \item The \emph{functorial theorems} are properties of datatypes related to
1515 \item The \emph{coinductive theorems} are properties of datatypes related to
1516 their coinductive nature.
1520 The first two categories are exactly as for datatypes and are described in
1522 \ref{sssec:free-constructor-theorems}~and~\ref{sssec:functorial-theorems}.
1526 subsubsection {* Coinductive Theorems
1527 \label{sssec:coinductive-theorems} *}
1530 The coinductive theorems are listed below for @{typ "'a llist"}:
1535 \item[\begin{tabular}{@ {}l@ {}}
1536 @{text "t."}\hthm{coinduct} @{text "[coinduct t, consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
1537 \phantom{@{text "t."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
1539 @{thm llist.coinduct[no_vars]}
1541 \item[\begin{tabular}{@ {}l@ {}}
1542 @{text "t."}\hthm{strong\_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
1543 \phantom{@{text "t."}\hthm{strong\_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
1545 @{thm llist.strong_coinduct[no_vars]}
1547 \item[\begin{tabular}{@ {}l@ {}}
1548 @{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]"} \\
1549 @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong\_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
1550 \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong\_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
1552 Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be
1553 used to prove $m$ properties simultaneously.
1555 \item[@{text "t."}\hthm{unfold}\rm:] ~ \\
1556 @{thm llist.unfold(1)[no_vars]} \\
1557 @{thm llist.unfold(2)[no_vars]}
1559 \item[@{text "t."}\hthm{corec}\rm:] ~ \\
1560 @{thm llist.corec(1)[no_vars]} \\
1561 @{thm llist.corec(2)[no_vars]}
1563 \item[@{text "t."}\hthm{disc\_unfold}\rm:] ~ \\
1564 @{thm llist.disc_unfold(1)[no_vars]} \\
1565 @{thm llist.disc_unfold(2)[no_vars]}
1567 \item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\
1568 @{thm llist.disc_corec(1)[no_vars]} \\
1569 @{thm llist.disc_corec(2)[no_vars]}
1571 \item[@{text "t."}\hthm{disc\_unfold\_iff} @{text "[simp]"}\rm:] ~ \\
1572 @{thm llist.disc_unfold_iff(1)[no_vars]} \\
1573 @{thm llist.disc_unfold_iff(2)[no_vars]}
1575 \item[@{text "t."}\hthm{disc\_corec\_iff} @{text "[simp]"}\rm:] ~ \\
1576 @{thm llist.disc_corec_iff(1)[no_vars]} \\
1577 @{thm llist.disc_corec_iff(2)[no_vars]}
1579 \item[@{text "t."}\hthm{sel\_unfold} @{text "[simp]"}\rm:] ~ \\
1580 @{thm llist.sel_unfold(1)[no_vars]} \\
1581 @{thm llist.sel_unfold(2)[no_vars]}
1583 \item[@{text "t."}\hthm{sel\_corec} @{text "[simp]"}\rm:] ~ \\
1584 @{thm llist.sel_corec(1)[no_vars]} \\
1585 @{thm llist.sel_corec(2)[no_vars]}
1591 For convenience, @{command codatatype} also provides the following collection:
1596 \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec} @{text t.disc_corec_iff}] ~ \\
1597 @{text t.sel_corec} @{text t.disc_unfold} @{text t.disc_unfold_iff} @{text t.sel_unfold} @{text t.map} \\
1598 @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
1605 section {* Defining Corecursive Functions
1606 \label{sec:defining-corecursive-functions} *}
1609 Corecursive functions can be specified using @{command primcorec} and
1610 @{command primcorecursive}, which support primitive corecursion, or using the
1611 more general \keyw{partial\_function} command. Here, the focus is on
1612 the former two. More examples can be found in the directory
1613 \verb|~~/src/HOL/BNF/Examples|.
1615 Whereas recursive functions consume datatypes one constructor at a time,
1616 corecursive functions construct codatatypes one constructor at a time.
1617 Partly reflecting a lack of agreement among proponents of coalgebraic methods,
1618 Isabelle supports three competing syntaxes for specifying a function $f$:
1621 \setlength{\itemsep}{0pt}
1623 \abovedisplayskip=.5\abovedisplayskip
1624 \belowdisplayskip=.5\belowdisplayskip
1626 \item The \emph{destructor view} specifies $f$ by implications of the form
1627 \[@{text "\<dots> \<Longrightarrow> is_C\<^sub>j (f x\<^sub>1 \<dots> x\<^sub>n)"}\] and
1628 equations of the form
1629 \[@{text "un_C\<^sub>ji (f x\<^sub>1 \<dots> x\<^sub>n) = \<dots>"}\]
1630 This style is popular in the coalgebraic literature.
1632 \item The \emph{constructor view} specifies $f$ by equations of the form
1633 \[@{text "\<dots> \<Longrightarrow> f x\<^sub>1 \<dots> x\<^sub>n = C \<dots>"}\]
1634 This style is often more concise than the previous one.
1636 \item The \emph{code view} specifies $f$ by a single equation of the form
1637 \[@{text "f x\<^sub>1 \<dots> x\<^sub>n = \<dots>"}\]
1638 with restrictions on the format of the right-hand side. Lazy functional
1639 programming languages such as Haskell support a generalized version of this
1643 All three styles are available as input syntax. Whichever syntax is chosen,
1644 characteristic theorems for all three styles are generated.
1648 \textbf{Warning:}\enskip The @{command primcorec} and @{command primcorecursive}
1649 commands are under development. Some of the functionality described here is
1650 vaporware. An alternative is to define corecursive functions directly using the
1651 generated @{text t_unfold} or @{text t_corec} combinators.
1654 %%% TODO: partial_function? E.g. for defining tail recursive function on lazy
1655 %%% lists (cf. terminal0 in TLList.thy)
1659 subsection {* Introductory Examples
1660 \label{ssec:primcorec-introductory-examples} *}
1663 Primitive corecursion is illustrated through concrete examples based on the
1664 codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
1665 examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|. The code
1666 view is favored in the examples below. Sections
1667 \ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
1668 present the same examples expressed using the constructor and destructor views.
1676 subsubsection {* Simple Corecursion
1677 \label{sssec:primcorec-simple-corecursion} *}
1680 Following the code view, corecursive calls are allowed on the right-hand side as
1681 long as they occur under a constructor, which itself appears either directly to
1682 the right of the equal sign or in a conditional expression:
1685 primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
1686 "literate f x = LCons x (literate f (f x))"
1688 text {* \blankline *}
1690 primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
1691 "siterate f x = SCons x (siterate f (f x))"
1695 The constructor ensures that progress is made---i.e., the function is
1696 \emph{productive}. The above functions compute the infinite lazy list or stream
1697 @{text "[x, f x, f (f x), \<dots>]"}. Productivity guarantees that prefixes
1698 @{text "[x, f x, f (f x), \<dots>, (f ^^ k) x]"} of arbitrary finite length
1699 @{text k} can be computed by unfolding the code equation a finite number of
1702 Corecursive functions construct codatatype values, but nothing prevents them
1703 from also consuming such values. The following function drops every second
1704 element in a stream:
1707 primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
1708 "every_snd s = SCons (shd s) (stl (stl s))"
1712 Constructs such as @{text "let"}---@{text "in"}, @{text
1713 "if"}---@{text "then"}---@{text "else"}, and @{text "case"}---@{text "of"} may
1714 appear around constructors that guard corecursive calls:
1717 primcorec_notyet lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
1720 LNil \<Rightarrow> ys
1721 | LCons x xs' \<Rightarrow> LCons x (lappend xs' ys))"
1725 Corecursion is useful to specify not only functions but also infinite objects:
1728 primcorec infty :: enat where
1729 "infty = ESuc infty"
1733 The example below constructs a pseudorandom process value. It takes a stream of
1734 actions (@{text s}), a pseudorandom function generator (@{text f}), and a
1735 pseudorandom seed (@{text n}):
1739 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
1741 "random_process s f n =
1742 (if n mod 4 = 0 then
1744 else if n mod 4 = 1 then
1745 Skip (random_process s f (f n))
1746 else if n mod 4 = 2 then
1747 Action (shd s) (random_process (stl s) f (f n))
1749 Choice (random_process (every_snd s) (f \<circ> f) (f n))
1750 (random_process (every_snd (stl s)) (f \<circ> f) (f (f n))))"
1754 The main disadvantage of the code view is that the conditions are tested
1755 sequentially. This is visible in the generated theorems. The constructor and
1756 destructor views offer nonsequential alternatives.
1760 subsubsection {* Mutual Corecursion
1761 \label{sssec:primcorec-mutual-corecursion} *}
1764 The syntax for mutually corecursive functions over mutually corecursive
1765 datatypes is unsurprising:
1769 even_infty :: even_enat and
1770 odd_infty :: odd_enat
1772 "even_infty = Even_ESuc odd_infty" |
1773 "odd_infty = Odd_ESuc even_infty"
1776 subsubsection {* Nested Corecursion
1777 \label{sssec:primcorec-nested-corecursion} *}
1780 The next pair of examples generalize the @{const literate} and @{const siterate}
1781 functions (Section~\ref{sssec:primcorec-nested-corecursion}) to possibly
1782 infinite trees in which subnodes are organized either as a lazy list (@{text
1783 tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}):
1786 primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
1787 "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i f) (f x))"
1789 text {* \blankline *}
1791 primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
1792 "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fimage (iterate\<^sub>i\<^sub>s f) (f x))"
1796 Deterministic finite automata (DFAs) are traditionally defined as 5-tuples
1797 @{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,
1798 @{text \<Sigma>} is a finite alphabet, @{text \<delta>} is a transition function, @{text q\<^sub>0}
1799 is an initial state, and @{text F} is a set of final states. The following
1800 function translates a DFA into a @{type state_machine}:
1803 primcorec (*<*)(in early) (*>*)
1804 sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
1806 "sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (sm_of_dfa \<delta> F o \<delta> q)"
1810 The map function for the function type (@{text \<Rightarrow>}) is composition
1811 (@{text "op \<circ>"}). For convenience, corecursion through functions can be
1812 expressed using $\lambda$-expressions and function application rather
1813 than through composition. For example:
1817 sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
1819 "sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (sm_of_dfa \<delta> F o \<delta> q)"
1821 text {* \blankline *}
1823 primcorec empty_sm :: "'a state_machine" where
1824 "empty_sm = State_Machine False (\<lambda>_. empty_sm)"
1826 text {* \blankline *}
1828 primcorec not_sm :: "'a state_machine \<Rightarrow> 'a state_machine" where
1829 "not_sm M = State_Machine (\<not> accept M) (\<lambda>a. not_sm (trans M a))"
1831 text {* \blankline *}
1834 or_sm :: "'a state_machine \<Rightarrow> 'a state_machine \<Rightarrow> 'a state_machine"
1837 State_Machine (accept M \<or> accept N)
1838 (\<lambda>a. or_sm (trans M a) (trans N a))"
1841 subsubsection {* Nested-as-Mutual Corecursion
1842 \label{sssec:primcorec-nested-as-mutual-corecursion} *}
1845 Just as it is possible to recurse over nested recursive datatypes as if they
1846 were mutually recursive
1847 (Section~\ref{sssec:primrec-nested-as-mutual-recursion}), it is possible to
1848 pretend that nested codatatypes are mutually corecursive. For example:
1852 iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" and
1853 iterates\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a llist \<Rightarrow> 'a tree\<^sub>i\<^sub>i llist"
1855 "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (iterates\<^sub>i\<^sub>i f (f x))" |
1856 "iterates\<^sub>i\<^sub>i f xs =
1858 LNil \<Rightarrow> LNil
1859 | LCons x xs' \<Rightarrow> LCons (iterate\<^sub>i\<^sub>i f x) (iterates\<^sub>i\<^sub>i f xs'))"
1865 subsubsection {* Constructor View
1866 \label{ssec:primrec-constructor-view} *}
1869 locale ctr_view = code_view
1874 The constructor view is similar to the code view, but there is one separate
1875 conditional equation per constructor rather than a single unconditional
1876 equation. Examples that rely on a single constructor, such as @{const literate}
1877 and @{const siterate}, are identical in both styles.
1879 Here is an example where there is a difference:
1882 primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
1883 "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lappend xs ys = LNil" |
1884 "_ \<Longrightarrow> lappend xs ys = LCons (lhd (if lnull xs then ys else xs))
1885 (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
1889 With the constructor view, we must distinguish between the @{const LNil} and
1890 the @{const LCons} case. The condition for @{const LCons} is
1891 left implicit, as the negation of that for @{const LNil}.
1893 For this example, the constructor view is slighlty more involved than the
1894 code equation. Recall the code view version presented in
1895 Section~\ref{sssec:primcorec-simple-corecursion}.
1896 % TODO: \[{thm code_view.lappend.code}\]
1897 The constructor view requires us to analyze the second argument (@{term ys}).
1898 The code equation generated from the constructor view also suffers from this.
1899 % TODO: \[{thm lappend.code}\]
1901 In contrast, the next example is arguably more naturally expressed in the
1906 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
1908 "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail" |
1909 "n mod 4 = 1 \<Longrightarrow>
1910 random_process s f n = Skip (random_process s f (f n))" |
1911 "n mod 4 = 2 \<Longrightarrow>
1912 random_process s f n = Action (shd s) (random_process (stl s) f (f n))" |
1913 "n mod 4 = 3 \<Longrightarrow>
1914 random_process s f n = Choice (random_process (every_snd s) f (f n))
1915 (random_process (every_snd (stl s)) f (f n))"
1922 Since there is no sequentiality, we can apply the equation for @{const Choice}
1923 without having first to discharge @{term "n mod (4\<Colon>int) \<noteq> 0"},
1924 @{term "n mod (4\<Colon>int) \<noteq> 1"}, and
1925 @{term "n mod (4\<Colon>int) \<noteq> 2"}.
1926 The price to pay for this elegance is that we must discharge exclusivity proof
1927 obligations, one for each pair of conditions
1928 @{term "(n mod (4\<Colon>int) = i, n mod (4\<Colon>int) = j)"}
1929 with @{term "i < j"}. If we prefer not to discharge any obligations, we can
1930 enable the @{text "sequential"} option. This pushes the problem to the users of
1931 the generated properties.
1932 %Here are more examples to conclude:
1936 subsubsection {* Destructor View
1937 \label{ssec:primrec-destructor-view} *}
1945 The destructor view is in many respects dual to the constructor view. Conditions
1946 determine which constructor to choose, and these conditions are interpreted
1947 sequentially or not depending on the @{text "sequential"} option.
1948 Consider the following examples:
1951 primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
1952 "\<not> lnull (literate _ x)" |
1953 "lhd (literate _ x) = x" |
1954 "ltl (literate f x) = literate f (f x)"
1956 text {* \blankline *}
1958 primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
1959 "shd (siterate _ x) = x" |
1960 "stl (siterate f x) = siterate f (f x)"
1962 text {* \blankline *}
1964 primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
1965 "shd (every_snd s) = shd s" |
1966 "stl (every_snd s) = stl (stl s)"
1970 The first formula in the @{const literate} specification indicates which
1971 constructor to choose. For @{const siterate} and @{const every_snd}, no such
1972 formula is necessary, since the type has only one constructor. The last two
1973 formulas are equations specifying the value of the result for the relevant
1974 selectors. Corecursive calls appear directly to the right of the equal sign.
1975 Their arguments are unrestricted.
1977 The next example shows how to specify functions that rely on more than one
1981 primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
1982 "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
1983 "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
1984 "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
1988 For a codatatype with $n$ constructors, it is sufficient to specify $n - 1$
1989 discriminator formulas. The command will then assume that the remaining
1990 constructor should be taken otherwise. This can be made explicit by adding
1996 primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
1997 "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
1999 "_ \<Longrightarrow> \<not> lnull (lappend xs ys)"
2001 "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
2002 "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
2004 context dest_view begin
2009 to the specification. The generated selector theorems are conditional.
2011 The next example illustrates how to cope with selectors defined for several
2016 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
2018 "n mod 4 = 0 \<Longrightarrow> is_Fail (random_process s f n)" |
2019 "n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)" |
2020 "n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)" |
2021 "n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)" |
2022 "cont (random_process s f n) = random_process s f (f n)" of Skip |
2023 "prefix (random_process s f n) = shd s" |
2024 "cont (random_process s f n) = random_process (stl s) f (f n)" of Action |
2025 "left (random_process s f n) = random_process (every_snd s) f (f n)" |
2026 "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)"
2030 Using the @{text "of"} keyword, different equations are specified for @{const
2031 cont} depending on which constructor is selected.
2033 Here are more examples to conclude:
2037 even_infty :: even_enat and
2038 odd_infty :: odd_enat
2040 "\<not> is_Even_EZero even_infty" |
2041 "un_Even_ESuc even_infty = odd_infty" |
2042 "un_Odd_ESuc odd_infty = even_infty"
2044 text {* \blankline *}
2046 primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
2047 "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = x" |
2048 "sub\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = lmap (iterate\<^sub>i\<^sub>i f) (f x)"
2054 subsection {* Command Syntax
2055 \label{ssec:primcorec-command-syntax} *}
2058 subsubsection {* \keyw{primcorec} and \keyw{primcorecursive}
2059 \label{sssec:primcorecursive-and-primcorec} *}
2062 \begin{matharray}{rcl}
2063 @{command_def "primcorec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
2064 @{command_def "primcorecursive"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
2068 (@@{command primcorec} | @@{command primcorecursive}) target? \\ @{syntax pcr_option}? fixes @'where'
2069 (@{syntax pcr_formula} + '|')
2071 @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')'
2073 @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
2076 The optional target is optionally followed by a corecursion-specific option:
2079 \setlength{\itemsep}{0pt}
2082 The @{text "sequential"} option indicates that the conditions in specifications
2083 expressed using the constructor or destructor view are to be interpreted
2087 The @{text "exhaustive"} option indicates that the conditions in specifications
2088 expressed using the constructor or destructor view cover all possible cases.
2092 The @{command primcorec} command is an abbreviation for @{command primcorecursive} with
2093 @{text "by auto?"} to discharge any emerging proof obligations.
2098 subsection {* Generated Theorems
2099 \label{ssec:primcorec-generated-theorems} *}
2104 subsection {* Recursive Default Values for Selectors
2105 \label{ssec:primcorec-recursive-default-values-for-selectors} *}
2108 partial_function to the rescue
2113 section {* Registering Bounded Natural Functors
2114 \label{sec:registering-bounded-natural-functors} *}
2117 The (co)datatype package can be set up to allow nested recursion through
2118 arbitrary type constructors, as long as they adhere to the BNF requirements and
2119 are registered as BNFs.
2124 subsection {* Introductory Example
2125 \label{ssec:bnf-introductory-example} *}
2128 More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and
2129 \verb|~~/src/HOL/BNF/More_BNFs.thy|.
2131 %Mention distinction between live and dead type arguments;
2132 % * and existence of map, set for those
2138 subsection {* Command Syntax
2139 \label{ssec:bnf-command-syntax} *}
2142 subsubsection {* \keyw{bnf}
2143 \label{sssec:bnf} *}
2146 \begin{matharray}{rcl}
2147 @{command_def "bnf"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
2151 @@{command bnf} target? (name ':')? term \\
2152 term_list term term_list term?
2154 X_list: '[' (X + ',') ']'
2159 subsubsection {* \keyw{print\_bnfs}
2160 \label{sssec:print-bnfs} *}
2163 \begin{matharray}{rcl}
2164 @{command_def "print_bnfs"} & : & @{text "local_theory \<rightarrow>"}
2168 @@{command print_bnfs}
2173 section {* Deriving Destructors and Theorems for Free Constructors
2174 \label{sec:deriving-destructors-and-theorems-for-free-constructors} *}
2177 The derivation of convenience theorems for types equipped with free constructors,
2178 as performed internally by @{command datatype_new} and @{command codatatype},
2179 is available as a stand-alone command called @{command wrap_free_constructors}.
2181 % * need for this is rare but may arise if you want e.g. to add destructors to
2182 % a type not introduced by ...
2184 % * also useful for compatibility with old package, e.g. add destructors to
2185 % old \keyw{datatype}
2187 % * @{command wrap_free_constructors}
2188 % * @{text "no_discs_sels"}, @{text "rep_compat"}
2189 % * hack to have both co and nonco view via locale (cf. ext nats)
2194 subsection {* Introductory Example
2195 \label{ssec:ctors-introductory-example} *}
2199 subsection {* Command Syntax
2200 \label{ssec:ctors-command-syntax} *}
2203 subsubsection {* \keyw{wrap\_free\_constructors}
2204 \label{sssec:wrap-free-constructors} *}
2207 \begin{matharray}{rcl}
2208 @{command_def "wrap_free_constructors"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
2212 @@{command wrap_free_constructors} target? @{syntax dt_options} \\
2213 term_list name @{syntax wfc_discs_sels}?
2215 @{syntax_def wfc_discs_sels}: name_list (name_list_list name_term_list_list? )?
2217 @{syntax_def name_term}: (name ':' term)
2220 % options: no_discs_sels rep_compat
2222 % X_list is as for BNF
2225 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
2230 section {* Standard ML Interface
2231 \label{sec:standard-ml-interface} *}
2234 The package's programmatic interface.
2240 section {* Interoperability
2241 \label{sec:interoperability} *}
2244 The package's interaction with other Isabelle packages and tools, such as the
2245 code generator and the counterexample generators.
2249 subsection {* Transfer and Lifting
2250 \label{ssec:transfer-and-lifting} *}
2253 subsection {* Code Generator
2254 \label{ssec:code-generator} *}
2257 subsection {* Quickcheck
2258 \label{ssec:quickcheck} *}
2261 subsection {* Nitpick
2262 \label{ssec:nitpick} *}
2265 subsection {* Nominal Isabelle
2266 \label{ssec:nominal-isabelle} *}
2271 section {* Known Bugs and Limitations
2272 \label{sec:known-bugs-and-limitations} *}
2275 Known open issues of the package.
2279 %* primcorecursive and primcorec is unfinished
2281 %* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
2283 %* issues with HOL-Proofs?
2285 %* partial documentation
2287 %* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
2288 % (for @{command datatype_new_compat} and prim(co)rec)
2290 % * a fortiori, no way to register same type as both data- and codatatype
2292 %* no recursion through unused arguments (unlike with the old package)
2294 %* in a locale, cannot use locally fixed types (because of limitation in typedef)?
2296 % *names of variables suboptimal
2302 \section*{Acknowledgment}
2304 Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
2305 (co)datatype package. Andreas Lochbihler provided lots of comments on earlier
2306 versions of the package, especially for the coinductive part. Brian Huffman
2307 suggested major simplifications to the internal constructions, much of which has
2308 yet to be implemented. Florian Haftmann and Christian Urban provided general
2309 advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder
2310 found an elegant proof to eliminate one of the BNF assumptions. Christian
2311 Sternagel suggested many textual improvements to this tutorial.