--- a/src/Doc/Datatypes/Datatypes.thy Fri Sep 13 11:16:13 2013 -0700
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 13 21:55:33 2013 +0200
@@ -51,7 +51,11 @@
finite and infinite values:
*}
- codatatype 'a llist (*<*)(map: lmap) (*>*)= LNil | LCons 'a "'a llist"
+(*<*)
+ locale dummy_llist
+ begin
+(*>*)
+ codatatype 'a llist = LNil | LCons 'a "'a llist"
text {*
\noindent
@@ -59,10 +63,6 @@
following four Rose tree examples:
*}
-(*<*)
- locale dummy_tree
- begin
-(*>*)
datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
datatype_new 'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
codatatype 'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
@@ -177,17 +177,19 @@
\label{sec:defining-datatypes} *}
text {*
-This section describes how to specify datatypes using the @{command
-datatype_new} command. The command is first illustrated through concrete
-examples featuring different flavors of recursion. More examples can be found in
-the directory \verb|~~/src/HOL/BNF/Examples|.
+Datatypes can be specified using the @{command datatype_new} command. The
+command is first illustrated through concrete examples featuring different
+flavors of recursion. More examples can be found in the directory
+\verb|~~/src/HOL/BNF/Examples|.
*}
subsection {* Introductory Examples
\label{ssec:datatype-introductory-examples} *}
-subsubsection {* Nonrecursive Types *}
+
+subsubsection {* Nonrecursive Types
+ \label{sssec:datatype-nonrecursive-types} *}
text {*
Datatypes are introduced by specifying the desired names and argument types for
@@ -231,17 +233,14 @@
datatype_new ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
-subsubsection {* Simple Recursion *}
+subsubsection {* Simple Recursion
+ \label{sssec:datatype-simple-recursion} *}
text {*
Natural numbers are the simplest example of a recursive type:
*}
datatype_new nat = Zero | Suc nat
-(*<*)
- (* FIXME: remove once "datatype_new" is integrated with "fun" *)
- datatype_new_compat nat
-(*>*)
text {*
\noindent
@@ -264,7 +263,8 @@
*}
-subsubsection {* Mutual Recursion *}
+subsubsection {* Mutual Recursion
+ \label{sssec:datatype-mutual-recursion} *}
text {*
\emph{Mutually recursive} types are introduced simultaneously and may refer to
@@ -272,8 +272,8 @@
natural numbers:
*}
- datatype_new enat = EZero | ESuc onat
- and onat = OSuc enat
+ datatype_new even_nat = Even_Zero | Even_Suc odd_nat
+ and odd_nat = Odd_Suc even_nat
text {*
\noindent
@@ -289,7 +289,8 @@
Const 'a | Var 'b | Expr "('a, 'b) exp"
-subsubsection {* Nested Recursion *}
+subsubsection {* Nested Recursion
+ \label{sssec:datatype-nested-recursion} *}
text {*
\emph{Nested recursion} occurs when recursive occurrences of a type appear under
@@ -322,6 +323,13 @@
text {*
\noindent
+This is legal:
+*}
+
+ datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
+
+text {*
+\noindent
In general, type constructors @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
allow recursion on a subset of their type arguments @{text 'a\<^sub>1}, \ldots,
@{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
@@ -336,7 +344,8 @@
*}
-subsubsection {* Custom Names and Syntaxes *}
+subsubsection {* Custom Names and Syntaxes
+ \label{sssec:datatype-custom-names-and-syntaxes} *}
text {*
The @{command datatype_new} command introduces various constants in addition to
@@ -424,7 +433,8 @@
\label{ssec:datatype-command-syntax} *}
-subsubsection {* \keyw{datatype\_new} *}
+subsubsection {* \keyw{datatype\_new}
+ \label{sssec:datatype-new} *}
text {*
Datatype definitions have the following general syntax:
@@ -433,7 +443,7 @@
@@{command_def datatype_new} target? @{syntax dt_options}? \\
(@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
;
- @{syntax_def dt_options}: '(' ((@'no_discs_sels' | @'rep_compat') + ',') ')'
+ @{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'
"}
The syntactic quantity \synt{target} can be used to specify a local
@@ -446,11 +456,11 @@
\setlength{\itemsep}{0pt}
\item
-The \keyw{no\_discs\_sels} option indicates that no discriminators or selectors
+The @{text "no_discs_sels"} option indicates that no discriminators or selectors
should be generated.
\item
-The \keyw{rep\_compat} option indicates that the names generated by the
+The @{text "rep_compat"} option indicates that the names generated by the
package should contain optional (and normally not displayed) ``@{text "new."}''
components to prevent clashes with a later call to \keyw{rep\_datatype}. See
Section~\ref{ssec:datatype-compatibility-issues} for details.
@@ -504,7 +514,7 @@
constructors as long as they share the same type.
@{rail "
- @{syntax_def dt_sel_defaults}: '(' @'defaults' (name ':' term +) ')'
+ @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')'
"}
\noindent
@@ -518,12 +528,49 @@
*}
-subsubsection {* \keyw{datatype\_new\_compat} *}
+subsubsection {* \keyw{datatype\_new\_compat}
+ \label{sssec:datatype-new-compat} *}
text {*
+The old datatype package provides some functionality that is not yet replicated
+in the new package:
+
+\begin{itemize}
+\item It is integrated with \keyw{fun} and \keyw{function}
+\cite{isabelle-function}, Nitpick \cite{isabelle-nitpick}, Quickcheck,
+and other packages.
+
+\item It is extended by various add-ons, notably to produce instances of the
+@{const size} function.
+\end{itemize}
+
+\noindent
+New-style datatypes can in most case be registered as old-style datatypes using
+the command
+
@{rail "
- @@{command_def datatype_new_compat} types
+ @@{command_def datatype_new_compat} names
"}
+
+\noindent
+where the \textit{names} argument is simply a space-separated list of type names
+that are mutually recursive. For example:
+*}
+
+ datatype_new_compat even_nat odd_nat
+
+text {* \blankline *}
+
+ thm even_nat_odd_nat.size
+
+text {* \blankline *}
+
+ ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *}
+
+text {*
+For nested recursive datatypes, all types through which recursion takes place
+must be new-style datatypes. In principle, it should be possible to support
+old-style datatypes as well, but the command does not support this yet.
*}
@@ -531,7 +578,7 @@
\label{ssec:datatype-generated-constants} *}
text {*
-Given a type @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
+Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
with $m > 0$ live type variables and $n$ constructors
@{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the
following auxiliary constants are introduced:
@@ -575,7 +622,7 @@
text {*
The characteristic theorems generated by @{command datatype_new} are grouped in
-two broad categories:
+three broad categories:
\begin{itemize}
\item The \emph{free constructor theorems} are properties about the constructors
@@ -607,7 +654,8 @@
to the top of the theory file.
*}
-subsubsection {* Free Constructor Theorems *}
+subsubsection {* Free Constructor Theorems
+ \label{sssec:free-constructor-theorems} *}
(*<*)
consts is_Cons :: 'a
@@ -620,42 +668,55 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\rmfamily:] ~ \\
@{thm list.inject[no_vars]}
-\item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\rmfamily:] ~ \\
@{thm list.distinct(1)[no_vars]} \\
@{thm list.distinct(2)[no_vars]}
-\item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
@{thm list.exhaust[no_vars]}
-\item[@{text "t."}\hthm{nchotomy}\upshape:] ~ \\
+\item[@{text "t."}\hthm{nchotomy}\rmfamily:] ~ \\
@{thm list.nchotomy[no_vars]}
\end{description}
\end{indentblock}
\noindent
+In addition, these nameless theorems are registered as safe elimination rules:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{list.distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rmfamily:] ~ \\
+@{thm list.distinct(1)[THEN notE, elim!, no_vars]} \\
+@{thm list.distinct(2)[THEN notE, elim!, no_vars]}
+
+\end{description}
+\end{indentblock}
+
+\noindent
The next subgroup is concerned with the case combinator:
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{case} @{text "[simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{case} @{text "[simp]"}\rmfamily:] ~ \\
@{thm list.case(1)[no_vars]} \\
@{thm list.case(2)[no_vars]}
-\item[@{text "t."}\hthm{case\_cong}\upshape:] ~ \\
+\item[@{text "t."}\hthm{case\_cong}\rmfamily:] ~ \\
@{thm list.case_cong[no_vars]}
-\item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\rmfamily:] ~ \\
@{thm list.weak_case_cong[no_vars]}
-\item[@{text "t."}\hthm{split}\upshape:] ~ \\
+\item[@{text "t."}\hthm{split}\rmfamily:] ~ \\
@{thm list.split[no_vars]}
-\item[@{text "t."}\hthm{split\_asm}\upshape:] ~ \\
+\item[@{text "t."}\hthm{split\_asm}\rmfamily:] ~ \\
@{thm list.split_asm[no_vars]}
\item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]
@@ -669,32 +730,32 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{discs} @{text "[simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{discs} @{text "[simp]"}\rmfamily:] ~ \\
@{thm list.discs(1)[no_vars]} \\
@{thm list.discs(2)[no_vars]}
-\item[@{text "t."}\hthm{sels} @{text "[simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{sels} @{text "[simp]"}\rmfamily:] ~ \\
@{thm list.sels(1)[no_vars]} \\
@{thm list.sels(2)[no_vars]}
-\item[@{text "t."}\hthm{collapse} @{text "[simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rmfamily:] ~ \\
@{thm list.collapse(1)[no_vars]} \\
@{thm list.collapse(2)[no_vars]}
-\item[@{text "t."}\hthm{disc\_exclude}\upshape:] ~ \\
+\item[@{text "t."}\hthm{disc\_exclude}\rmfamily:] ~ \\
These properties are missing for @{typ "'a list"} because there is only one
proper discriminator. Had the datatype been introduced with a second
discriminator called @{const is_Cons}, they would have read thusly: \\[\jot]
@{prop "null list \<Longrightarrow> \<not> is_Cons list"} \\
@{prop "is_Cons list \<Longrightarrow> \<not> null list"}
-\item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
@{thm list.disc_exhaust[no_vars]}
-\item[@{text "t."}\hthm{expand}\upshape:] ~ \\
+\item[@{text "t."}\hthm{expand}\rmfamily:] ~ \\
@{thm list.expand[no_vars]}
-\item[@{text "t."}\hthm{case\_conv}\upshape:] ~ \\
+\item[@{text "t."}\hthm{case\_conv}\rmfamily:] ~ \\
@{thm list.case_conv[no_vars]}
\end{description}
@@ -702,27 +763,28 @@
*}
-subsubsection {* Functorial Theorems *}
+subsubsection {* Functorial Theorems
+ \label{sssec:functorial-theorems} *}
text {*
-The BNF-related theorem are listed below:
+The BNF-related theorem are as follows:
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{sets} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{sets} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.sets(1)[no_vars]} \\
@{thm list.sets(2)[no_vars]}
-\item[@{text "t."}\hthm{map} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{map} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.map(1)[no_vars]} \\
@{thm list.map(2)[no_vars]}
-\item[@{text "t."}\hthm{rel\_inject} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{rel\_inject} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.rel_inject(1)[no_vars]} \\
@{thm list.rel_inject(2)[no_vars]}
-\item[@{text "t."}\hthm{rel\_distinct} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{rel\_distinct} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.rel_distinct(1)[no_vars]} \\
@{thm list.rel_distinct(2)[no_vars]}
@@ -731,26 +793,27 @@
*}
-subsubsection {* Inductive Theorems *}
+subsubsection {* Inductive Theorems
+ \label{sssec:inductive-theorems} *}
text {*
-The inductive theorems are listed below:
+The inductive theorems are as follows:
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
@{thm list.induct[no_vars]}
-\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
+\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
prove $m$ properties simultaneously.
-\item[@{text "t."}\hthm{fold} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{fold} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.fold(1)[no_vars]} \\
@{thm list.fold(2)[no_vars]}
-\item[@{text "t."}\hthm{rec} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{rec} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.rec(1)[no_vars]} \\
@{thm list.rec(2)[no_vars]}
@@ -793,7 +856,7 @@
% Nitpick
% * provide exactly the same theorems with the same names (compatibility)
% * option 1
-% * \keyw{rep\_compat}
+% * @{text "rep_compat"}
% * \keyw{rep\_datatype}
% * has some limitations
% * mutually recursive datatypes? (fails with rep_datatype?)
@@ -818,65 +881,72 @@
text {*
This describes how to specify recursive functions over datatypes specified using
@{command datatype_new}. The focus in on the @{command primrec_new} command,
-which supports primitive recursion. A few examples feature the \keyw{fun} and
-\keyw{function} commands, described in a separate tutorial
-\cite{isabelle-function}.
+which supports primitive recursion. More examples can be found in
+\verb|~~/src/HOL/BNF/Examples|.
-%%% TODO: partial_function?
+%%% TODO: partial_function
*}
-text {*
-More examples in \verb|~~/src/HOL/BNF/Examples|.
-*}
subsection {* Introductory Examples
\label{ssec:primrec-introductory-examples} *}
-subsubsection {* Nonrecursive Types *}
+
+subsubsection {* Nonrecursive Types
+ \label{sssec:primrec-nonrecursive-types} *}
text {*
-% * simple (depth 1) pattern matching on the left-hand side
+Primitive recursion removes one layer of constructors on the left-hand side in
+each equation. For example:
*}
primrec_new bool_of_trool :: "trool \<Rightarrow> bool" where
- "bool_of_trool Faalse = False" |
- "bool_of_trool Truue = True"
+ "bool_of_trool Faalse \<longleftrightarrow> False" |
+ "bool_of_trool Truue \<longleftrightarrow> True"
-text {*
-% * OK to specify the cases in a different order
-% * OK to leave out some case (but get a warning -- maybe we need a "quiet"
-% or "silent" flag?)
-% * case is then unspecified
-
-More examples:
-*}
+text {* \blankline *}
primrec_new the_list :: "'a option \<Rightarrow> 'a list" where
"the_list None = []" |
"the_list (Some a) = [a]"
+text {* \blankline *}
+
primrec_new the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
"the_default d None = d" |
"the_default _ (Some a) = a"
+text {* \blankline *}
+
primrec_new mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
"mirrror (Triple a b c) = Triple c b a"
+text {*
+\noindent
+The equations can be specified in any order, and it is acceptable to leave out
+some cases, which are then unspecified. Pattern matching on the left-hand side
+is restricted to a single datatype, which must correspond to the same argument
+in all equations.
+*}
-subsubsection {* Simple Recursion *}
+
+subsubsection {* Simple Recursion
+ \label{sssec:primrec-simple-recursion} *}
text {*
-again, simple pattern matching on left-hand side, but possibility
-to call a function recursively on an argument to a constructor:
+For simple recursive types, recursive calls on a constructor argument are
+allowed on the right-hand side:
*}
+(*<*)
+ context dummy_tlist
+ begin
+(*>*)
primrec_new replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
"replicate Zero _ = []" |
"replicate (Suc n) a = a # replicate n a"
-text {*
-we don't like the confusing name @{const nth}:
-*}
+text {* \blankline *}
primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
"at (a # as) j =
@@ -884,10 +954,8 @@
Zero \<Rightarrow> a
| Suc j' \<Rightarrow> at as j')"
-(*<*)
- context dummy_tlist
- begin
-(*>*)
+text {* \blankline *}
+
primrec_new tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
"tfold _ (TNil b) = b" |
"tfold f (TCons a as) = f a (tfold f as)"
@@ -896,39 +964,37 @@
(*>*)
text {*
-Show one example where fun is needed.
+\noindent
+The next example is not primitive recursive, but it can be defined easily using
+@{command fun}. The @{command datatype_new_compat} command is needed to register
+new-style datatypes for use with @{command fun} and @{command function}
+(Section~\ref{sssec:datatype-new-compat}):
*}
-subsubsection {* Mutual Recursion *}
+ datatype_new_compat nat
+
+text {* \blankline *}
+
+ fun at_least_two :: "nat \<Rightarrow> bool" where
+ "at_least_two (Suc (Suc _)) \<longleftrightarrow> True" |
+ "at_least_two _ \<longleftrightarrow> False"
+
+
+subsubsection {* Mutual Recursion
+ \label{sssec:primrec-mutual-recursion} *}
text {*
-E.g., converting even/odd naturals to plain old naturals:
+The syntax for mutually recursive functions over mutually recursive datatypes
+is straightforward:
*}
primrec_new
- nat_of_enat :: "enat \<Rightarrow> nat" and
- nat_of_onat :: "onat => nat"
+ nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
+ nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
where
- "nat_of_enat EZero = Zero" |
- "nat_of_enat (ESuc n) = Suc (nat_of_onat n)" |
- "nat_of_onat (OSuc n) = Suc (nat_of_enat n)"
-
-text {*
-Mutual recursion is be possible within a single type, but currently only using fun:
-*}
-
- fun
- even :: "nat \<Rightarrow> bool" and
- odd :: "nat \<Rightarrow> bool"
- where
- "even Zero = True" |
- "even (Suc n) = odd n" |
- "odd Zero = False" |
- "odd (Suc n) = even n"
-
-text {*
-More elaborate example that works with primrec_new:
-*}
+ "nat_of_even_nat Even_Zero = Zero" |
+ "nat_of_even_nat (Even_Suc n) = Suc (nat_of_odd_nat n)" |
+ "nat_of_odd_nat (Odd_Suc n) = Suc (nat_of_even_nat n)"
primrec_new
eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
@@ -943,26 +1009,54 @@
"eval\<^sub>f _ \<xi> (Var b) = \<xi> b" |
"eval\<^sub>f \<gamma> \<xi> (Expr e) = eval\<^sub>e \<gamma> \<xi> e"
+text {*
+\noindent
+Mutual recursion is be possible within a single type, using @{command fun}:
+*}
-subsubsection {* Nested Recursion *}
+ fun
+ even :: "nat \<Rightarrow> bool" and
+ odd :: "nat \<Rightarrow> bool"
+ where
+ "even Zero = True" |
+ "even (Suc n) = odd n" |
+ "odd Zero = False" |
+ "odd (Suc n) = even n"
+
+
+subsubsection {* Nested Recursion
+ \label{sssec:primrec-nested-recursion} *}
+
+text {*
+In a departure from the old datatype package, nested recursion is normally
+handled via the map functions of the nesting type constructors. For example,
+recursive calls are lifted to lists using @{const map}:
+*}
(*<*)
datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
- datatype_new 'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
+
+ context dummy_tlist
+ begin
(*>*)
primrec_new at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
"at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
(case js of
[] \<Rightarrow> a
| j # js' \<Rightarrow> at (map (\<lambda>t. at\<^sub>f\<^sub>f t js') ts) j)"
+(*<*)
+ end
+(*>*)
text {*
-Explain @{const lmap}.
+The next example features recursion through the @{text option} type. Although
+@{text option} is not a new-style datatype, it is registered as a BNF with the
+map function @{const option_map}:
*}
(*<*)
locale sum_btree_nested
- begin
+ begin
(*>*)
primrec_new sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
"sum_btree (BNode a lt rt) =
@@ -973,15 +1067,31 @@
(*>*)
text {*
-Show example with function composition (ftree).
+\noindent
+The same principle applies for arbitrary type constructors through which
+recursion is possible. Notably, the map function for the function type
+(@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
*}
-subsubsection {* Nested-as-Mutual Recursion *}
+ primrec_new ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
+ "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
+ "ftree_map f (FTNode g) = FTNode (ftree_map f \<circ> g)"
text {*
-% * can pretend a nested type is mutually recursive (if purely inductive)
-% * avoids the higher-order map
-% * e.g.
+\noindent
+(No such function is defined by the package because @{typ 'a} is dead in
+@{typ "'a ftree"}, but we can easily do it ourselves.)
+*}
+
+
+subsubsection {* Nested-as-Mutual Recursion
+ \label{sssec:datatype-nested-as-mutual-recursion} *}
+
+text {*
+For compatibility with the old package, but also because it is sometimes
+convenient in its own right, it is possible to treat nested recursive datatypes
+as mutually recursive ones if the recursion takes place though new-style
+datatypes. For example:
*}
primrec_new
@@ -997,6 +1107,8 @@
Zero \<Rightarrow> at_tree\<^sub>f\<^sub>f t
| Suc j' \<Rightarrow> at_trees\<^sub>f\<^sub>f ts j')"
+text {* \blankline *}
+
primrec_new
sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" and
sum_btree_option :: "'a btree option \<Rightarrow> 'a"
@@ -1007,6 +1119,11 @@
"sum_btree_option (Some t) = sum_btree t"
text {*
+
+% * can pretend a nested type is mutually recursive (if purely inductive)
+% * avoids the higher-order map
+% * e.g.
+
% * this can always be avoided;
% * e.g. in our previous example, we first mapped the recursive
% calls, then we used a generic at function to retrieve the result
@@ -1036,7 +1153,8 @@
\label{ssec:primrec-command-syntax} *}
-subsubsection {* \keyw{primrec\_new} *}
+subsubsection {* \keyw{primrec\_new}
+ \label{sssec:primrec-new} *}
text {*
Primitive recursive functions have the following general syntax:
@@ -1068,13 +1186,13 @@
subsection {* Recursive Default Values for Selectors
- \label{ssec:recursive-default-values-for-selectors} *}
+ \label{ssec:primrec-recursive-default-values-for-selectors} *}
text {*
A datatype selector @{text un_D} can have a default value for each constructor
on which it is not otherwise specified. Occasionally, it is useful to have the
default value be defined recursively. This produces a chicken-and-egg situation
-that appears unsolvable, because the datatype is not introduced yet at the
+that may seem unsolvable, because the datatype is not introduced yet at the
moment when the selectors are introduced. Of course, we can always define the
selectors manually afterward, but we then have to state and prove all the
characteristic theorems ourselves instead of letting the package do it.
@@ -1120,8 +1238,8 @@
termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist \<Rightarrow> 'b"
begin
primrec_new termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
- "termi\<^sub>0 (TNil y) = y" |
- "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
+ "termi\<^sub>0 (TNil y) = y" |
+ "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
end
text {* \blankline *}
@@ -1150,57 +1268,193 @@
\label{sec:defining-codatatypes} *}
text {*
-This section describes how to specify codatatypes using the @{command
-codatatype} command. The command is first illustrated through concrete examples
-featuring different flavors of corecursion. More examples can be found in the
-directory \verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs}
-also includes some useful codatatypes, notably for lazy lists
-\cite{lochbihler-2010}.
+Codatatypes can be specified using the @{command codatatype} command. The
+command is first illustrated through concrete examples featuring different
+flavors of corecursion. More examples can be found in the directory
+\verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs} also
+includes some useful codatatypes, notably for lazy lists \cite{lochbihler-2010}.
*}
-(*
subsection {* Introductory Examples
\label{ssec:codatatype-introductory-examples} *}
+
+subsubsection {* Simple Corecursion
+ \label{sssec:codatatype-simple-corecursion} *}
+
text {*
-More examples in \verb|~~/src/HOL/BNF/Examples|.
+Noncorecursive codatatypes coincide with the corresponding datatypes, so
+they have no practical uses. \emph{Corecursive codatatypes} have the same syntax
+as recursive datatypes, except for the command name. For example, here is the
+definition of lazy lists:
+*}
+
+ codatatype (lset: 'a) llist (map: lmap rel: llist_all2) =
+ lnull: LNil (defaults ltl: LNil)
+ | LCons (lhd: 'a) (ltl: "'a llist")
+
+text {*
+\noindent
+Lazy lists can be infinite, such as @{text "LCons 0 (LCons 0 (\<dots>))"} and
+@{text "LCons 0 (LCons 1 (LCons 2 (\<dots>)))"}. Another interesting type that can
+be defined as a codatatype is that of the extended natural numbers:
+*}
+
+ codatatype enat = EZero | ESuc nat
+
+text {*
+\noindent
+This type has exactly one infinite element, @{text "ESuc (ESuc (ESuc (\<dots>)))"},
+that represents $\infty$. In addition, it has finite values of the form
+@{text "ESuc (\<dots> (ESuc EZero)\<dots>)"}.
*}
-*)
+
+
+subsubsection {* Mutual Corecursion
+ \label{sssec:codatatype-mutual-corecursion} *}
+
+text {*
+\noindent
+The example below introduces a pair of \emph{mutually corecursive} types:
+*}
+
+ codatatype even_enat = Even_EZero | Even_ESuc odd_enat
+ and odd_enat = Odd_ESuc even_enat
+
+
+subsubsection {* Nested Corecursion
+ \label{sssec:codatatype-nested-corecursion} *}
+
+text {*
+\noindent
+The next two examples feature \emph{nested corecursion}:
+*}
+
+ codatatype 'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
+ codatatype 'a tree\<^sub>i\<^sub>s = Node\<^sub>i\<^sub>s 'a "'a tree\<^sub>i\<^sub>s fset"
subsection {* Command Syntax
\label{ssec:codatatype-command-syntax} *}
-subsubsection {* \keyw{codatatype} *}
+subsubsection {* \keyw{codatatype}
+ \label{sssec:codatatype} *}
text {*
Definitions of codatatypes have almost exactly the same syntax as for datatypes
(Section~\ref{ssec:datatype-command-syntax}), with two exceptions: The command
-is called @{command codatatype}; the \keyw{no\_discs\_sels} option is not
-available, because destructors are a central notion for codatatypes.
+is called @{command codatatype}. The @{text "no_discs_sels"} option is not
+available, because destructors are a crucial notion for codatatypes.
+*}
+
+
+subsection {* Generated Constants
+ \label{ssec:codatatype-generated-constants} *}
+
+text {*
+Given a codatatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
+with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
+\ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
+datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
+iterator and the recursor are replaced by dual concepts:
+
+\begin{itemize}
+\setlength{\itemsep}{0pt}
+
+\item \relax{Coiterator}: @{text t_unfold}
+
+\item \relax{Corecursor}: @{text t_corec}
+
+\end{itemize}
+*}
+
+
+subsection {* Generated Theorems
+ \label{ssec:codatatype-generated-theorems} *}
+
+text {*
+The characteristic theorems generated by @{command codatatype} are grouped in
+three broad categories:
+
+\begin{itemize}
+\item The \emph{free constructor theorems} are properties about the constructors
+and destructors that can be derived for any freely generated type.
+
+\item The \emph{functorial theorems} are properties of datatypes related to
+their BNF nature.
+
+\item The \emph{coinductive theorems} are properties of datatypes related to
+their coinductive nature.
+\end{itemize}
+
+\noindent
+The first two categories are exactly as for datatypes and are described in
+Sections \ref{ssec:free-constructor-theorems}~and~\ref{ssec:functorial-theorems}.
*}
-(*
-subsection {* Generated Constants
- \label{ssec:codatatype-generated-constants} *}
-*)
+subsubsection {* Coinductive Theorems
+ \label{sssec:coinductive-theorems} *}
+
+text {*
+The coinductive theorems are as follows:
+
+% [(coinductN, map single coinduct_thms,
+% fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
+% (corecN, corec_thmss, K coiter_attrs),
+% (disc_corecN, disc_corec_thmss, K disc_coiter_attrs),
+% (disc_corec_iffN, disc_corec_iff_thmss, K disc_coiter_iff_attrs),
+% (disc_unfoldN, disc_unfold_thmss, K disc_coiter_attrs),
+% (disc_unfold_iffN, disc_unfold_iff_thmss, K disc_coiter_iff_attrs),
+% (sel_corecN, sel_corec_thmss, K sel_coiter_attrs),
+% (sel_unfoldN, sel_unfold_thmss, K sel_coiter_attrs),
+% (simpsN, simp_thmss, K []),
+% (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
+% (unfoldN, unfold_thmss, K coiter_attrs)]
+% |> massage_multi_notes;
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{coinduct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
+@{thm llist.coinduct[no_vars]}
+\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
+Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
+prove $m$ properties simultaneously.
-(*
-subsection {* Generated Theorems
- \label{ssec:codatatype-generated-theorems} *}
-*)
+\item[@{text "t."}\hthm{unfold} @{text "[code]"}\rmfamily:] ~ \\
+@{thm llist.unfold(1)[no_vars]} \\
+@{thm llist.unfold(2)[no_vars]}
+
+\item[@{text "t."}\hthm{corec} @{text "[code]"}\rmfamily:] ~ \\
+@{thm llist.corec(1)[no_vars]} \\
+@{thm llist.corec(2)[no_vars]}
+
+\end{description}
+\end{indentblock}
+
+\noindent
+For convenience, @{command codatatype} also provides the following collection:
+
+\begin{indentblock}
+\begin{description}
+
+\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}] ~ \\
+@{text t.rel_distinct} @{text t.sets}
+
+\end{description}
+\end{indentblock}
+*}
section {* Defining Corecursive Functions
\label{sec:defining-corecursive-functions} *}
text {*
-This section describes how to specify corecursive functions using the
-@{command primcorec} command.
+Corecursive functions can be specified using the @{command primcorec} command.
%%% TODO: partial_function? E.g. for defining tail recursive function on lazy
%%% lists (cf. terminal0 in TLList.thy)
@@ -1213,9 +1467,6 @@
text {*
More examples in \verb|~~/src/HOL/BNF/Examples|.
-
-Also, for default values, the same trick as for datatypes is possible for
-codatatypes (Section~\ref{ssec:recursive-default-values-for-selectors}).
*}
*)
@@ -1224,7 +1475,8 @@
\label{ssec:primcorec-command-syntax} *}
-subsubsection {* \keyw{primcorec} *}
+subsubsection {* \keyw{primcorec}
+ \label{sssec:primcorec} *}
text {*
Primitive corecursive definitions have the following general syntax:
@@ -1244,13 +1496,23 @@
*)
+(*
+subsection {* Recursive Default Values for Selectors
+ \label{ssec:primcorec-recursive-default-values-for-selectors} *}
+
+text {*
+partial_function to the rescue
+*}
+*)
+
+
section {* Registering Bounded Natural Functors
\label{sec:registering-bounded-natural-functors} *}
text {*
-This section explains how to set up the (co)datatype package to allow nested
-recursion through custom well-behaved type constructors. The key concept is that
-of a bounded natural functor (BNF).
+The (co)datatype package can be set up to allow nested recursion through custom
+well-behaved type constructors. The key concept is that of a bounded natural
+functor (BNF).
*}
@@ -1274,7 +1536,8 @@
\label{ssec:bnf-command-syntax} *}
-subsubsection {* \keyw{bnf} *}
+subsubsection {* \keyw{bnf}
+ \label{sssec:bnf} *}
text {*
@{rail "
@@ -1286,7 +1549,8 @@
*}
-subsubsection {* \keyw{print\_bnfs} *}
+subsubsection {* \keyw{print\_bnfs}
+ \label{sssec:print-bnfs} *}
text {*
@{command print_bnfs}
@@ -1297,8 +1561,9 @@
\label{sec:deriving-destructors-and-theorems-for-free-constructors} *}
text {*
-This section explains how to derive convenience theorems for free constructors,
-as performed internally by @{command datatype_new} and @{command codatatype}.
+The derivation of convenience theorems for types equipped with free constructors,
+as performed internally by @{command datatype_new} and @{command codatatype},
+is available as a stand-alone command called @{command wrap_free_constructors}.
% * need for this is rare but may arise if you want e.g. to add destructors to
% a type not introduced by ...
@@ -1307,7 +1572,7 @@
% old \keyw{datatype}
%
% * @{command wrap_free_constructors}
-% * \keyw{no\_discs\_sels}, \keyw{rep\_compat}
+% * @{text "no_discs_sels"}, @{text "rep_compat"}
% * hack to have both co and nonco view via locale (cf. ext nats)
*}
@@ -1322,7 +1587,8 @@
\label{ssec:ctors-command-syntax} *}
-subsubsection {* \keyw{wrap\_free\_constructors} *}
+subsubsection {* \keyw{wrap\_free\_constructors}
+ \label{sssec:wrap-free-constructors} *}
text {*
Free constructor wrapping has the following general syntax:
@@ -1349,7 +1615,7 @@
\label{sec:standard-ml-interface} *}
text {*
-This section describes the package's programmatic interface.
+The package's programmatic interface.
*}
*)
@@ -1359,9 +1625,8 @@
\label{sec:interoperability} *}
text {*
-This section is concerned with the packages' interaction with other Isabelle
-packages and tools, such as the code generator and the counterexample
-generators.
+The package's interaction with other Isabelle packages and tools, such as the
+code generator and the counterexample generators.
*}
@@ -1391,7 +1656,7 @@
\label{sec:known-bugs-and-limitations} *}
text {*
-This section lists known open issues of the package.
+Known open issues of the package.
*}
text {*