--- a/src/Doc/Datatypes/Datatypes.thy Fri Aug 02 22:46:54 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Aug 02 22:54:28 2013 +0200
@@ -6,15 +6,24 @@
theory Datatypes
imports Setup
+keywords
+ "primrec_new" :: thy_decl and
+ "primcorec" :: thy_decl
begin
-(*
-text {*
+(*<*)
+(* FIXME: Evil setup until "primrec_new" and "primcorec" are in place. *)
+ML_command {*
+fun add_dummy_cmd _ _ lthy = lthy;
- primrec_new <fixes>
+val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"} ""
+ (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd);
+val _ = Outer_Syntax.local_theory @{command_spec "primcorec"} ""
+ (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd);
*}
-*)
+(*>*)
+
section {* Introduction
\label{sec:introduction} *}
@@ -24,52 +33,56 @@
and codatatypes. The datatype support is similar to that provided by the earlier
package due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL},
documented in the Isar reference manual \cite{isabelle-isar-ref};
-indeed, replacing @{command datatype} by @{command datatype_new} is usually
-sufficient to port existing specifications to the new package. What makes the
-new package attractive is that it supports definitions with recursion through a
-large class of non-datatypes, notably finite sets:
+indeed, replacing the keyword @{command datatype} by @{command datatype_new} is
+usually all that is needed to port existing theories to use the new package.
+
+Perhaps the main advantage of the new package is that it supports recursion
+through a large class of non-datatypes, comprising finite sets:
*}
- datatype_new 'a treeFS = TreeFS 'a "'a treeFS fset"
+ datatype_new 'a treeFS = NodeFS 'a "'a treeFS fset"
text {*
\noindent
-Another advantage of the new package is that it supports local definitions:
+Another strong point is that the package supports local definitions:
*}
context linorder
begin
- datatype_new flag = Less | Eq | Greater
+ datatype_new flag = Less | Eq | Greater
end
text {*
\noindent
-Finally, the package also provides some convenience, notably automatically
-generated destructors.
+The package also provides some convenience, notably automatically generated
+destructors (discriminators and selectors).
-The command @{command datatype_new} is expected to displace @{command datatype} in a future
-release. Authors of new theories are encouraged to use @{command datatype_new}, and
-maintainers of older theories may want to consider upgrading in the coming months.
-
-The package also provides codatatypes (or ``coinductive datatypes''), which may
-have infinite values. The following command introduces a codatatype of infinite
-streams:
+In addition to plain inductive datatypes, the package supports coinductive
+datatypes, or \emph{codatatypes}, which may have infinite values. For example,
+the following command introduces the type of lazy lists:
*}
- codatatype 'a stream = Stream 'a "'a stream"
+ codatatype 'a llist = LNil | LCons 'a "'a llist"
text {*
\noindent
-Mixed inductive--coinductive recursion is possible via nesting.
-Compare the following four examples:
+Mixed inductive--coinductive recursion is possible via nesting. Compare the
+following four examples:
+
+%%% TODO: Avoid 0
*}
- datatype_new 'a treeFF = TreeFF 'a "'a treeFF list"
- datatype_new 'a treeFI = TreeFI 'a "'a treeFF stream"
- codatatype 'a treeIF = TreeIF 'a "'a treeFF list"
- codatatype 'a treeII = TreeII 'a "'a treeFF stream"
+ datatype_new 'a treeFF0 = NodeFF 'a "'a treeFF0 list"
+ datatype_new 'a treeFI0 = NodeFI 'a "'a treeFI0 llist"
+ codatatype 'a treeIF0 = NodeIF 'a "'a treeIF0 list"
+ codatatype 'a treeII0 = NodeII 'a "'a treeII0 llist"
text {*
+The first two tree types allow only finite branches, whereas the last two allow
+infinite branches. Orthogonally, the nodes in the first and third types have
+finite branching, whereas those of the second and fourth may have infinitely
+many direct subtrees.
+
To use the package, it is necessary to import the @{theory BNF} theory, which
can be precompiled as the \textit{HOL-BNF} image. The following commands show
how to launch jEdit/PIDE with the image loaded and how to build the image
@@ -87,14 +100,11 @@
The package, like its predecessor, fully adheres to the LCF philosophy
\cite{mgordon79}: The characteristic theorems associated with the specified
(co)datatypes are derived rather than introduced axiomatically.%
-\footnote{Nonetheless, if the \textit{quick\_and\_dirty} option is enabled, some
-of the internal constructions and most of the internal proof obligations are
-skipped.}
+\footnote{If the \textit{quick\_and\_dirty} option is enabled, some of the
+internal constructions and most of the internal proof obligations are skipped.}
The package's metatheory is described in a pair of papers
\cite{traytel-et-al-2012,blanchette-et-al-wit}.
-*}
-text {*
This tutorial is organized as follows:
\begin{itemize}
@@ -145,14 +155,17 @@
\newcommand\authoremailiii{\texttt{tray{\color{white}nospam}\kern-\wd\boxA{}tel@\allowbreak
in.\allowbreak tum.\allowbreak de}}
-\noindent
-Comments and bug reports concerning either
-the tool or the manual should be directed to the authors at
-\authoremaili, \authoremailii, and \authoremailiii.
+The command @{command datatype_new} is expected to displace @{command datatype}
+in a future release. Authors of new theories are encouraged to use
+@{command datatype_new}, and maintainers of older theories may want to consider
+upgrading in the coming months.
+
+Comments and bug reports concerning either the tool or this tutorial should be
+directed to the authors at \authoremaili, \authoremailii, and \authoremailiii.
\begin{framed}
\noindent
-\textbf{Warning:} This document is under heavy construction. Please apologise
+\textbf{Warning:} This tutorial is under heavy construction. Please apologise
for its appearance and come back in a few months. If you have ideas regarding
material that should be included, please let the authors know.
\end{framed}
@@ -167,11 +180,15 @@
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|.
+
+ * libraries include many useful datatypes, e.g. list, option, etc., as well
+ as operations on these;
+ see e.g. ``What's in Main'' \cite{xxx}
*}
-subsection {* Introductory Examples
- \label{ssec:datatype-introductory-examples} *}
+subsection {* Examples
+ \label{ssec:datatype-examples} *}
subsubsection {* Nonrecursive Types *}
@@ -203,6 +220,16 @@
datatype_new nat = Zero | Suc nat
text {*
+Setup to be able to write @{term 0} instead of @{const Zero}:
+*}
+
+ instantiation nat :: zero
+ begin
+ definition "0 = Zero"
+ instance ..
+ end
+
+text {*
lists were shown in the introduction
terminated lists are a variant:
@@ -224,19 +251,19 @@
Simple example: distinction between even and odd natural numbers:
*}
- datatype_new even_nat = Zero | Even_Suc odd_nat
- and odd_nat = Odd_Suc even_nat
+ datatype_new enat = EZero | ESuc onat
+ and onat = OSuc enat
text {*
More complex, and more realistic, example:
*}
- datatype_new ('a, 'b) expr =
- Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) expr"
+ datatype_new ('a, 'b) exp =
+ Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
and ('a, 'b) trm =
- Factor "('a, 'b) fact" | Prod "('a, 'b) fact" "('a, 'b) trm"
- and ('a, 'b) fact =
- Const 'a | Var 'b | Sub_Expr "('a, 'b) expr"
+ Factor "('a, 'b) fct" | Prod "('a, 'b) fct" "('a, 'b) trm"
+ and ('a, 'b) fct =
+ Const 'a | Var 'b | Expr "('a, 'b) exp"
subsubsection {* Nested Recursion *}
@@ -246,20 +273,16 @@
The introduction showed some examples of trees with nesting through lists.
-More complex example, which reuses our maybe and triple types:
+More complex example, which reuses our maybe:
*}
- datatype_new 'a triple_tree =
- Triple_Tree "('a triple_tree maybe, bool, 'a triple_tree maybe) triple"
+ datatype_new 'a btree =
+ BNode 'a "'a btree maybe" "'a btree maybe"
text {*
Recursion may not be arbitrary; e.g. impossible to define
*}
-(*
- datatype_new 'a foo = Foo (*<*) datatype_new 'a bar = Bar "'a foo \<Rightarrow> 'a foo"
-*)
-
datatype_new 'a evil = Evil (*<*)'a
typ (*>*)"'a evil \<Rightarrow> 'a evil"
@@ -307,20 +330,32 @@
The set functions, map function, relator, discriminators, and selectors can be
given custom names, as in the example below:
+
+%%% FIXME: get rid of 0 below
*}
-(*<*)hide_const Nil Cons hd tl(*>*)
- datatype_new (set: 'a) list (map: map rel: list_all2) =
+(*<*)
+ no_translations
+ "[x, xs]" == "x # [xs]"
+ "[x]" == "x # []"
+
+ no_notation
+ Nil ("[]") and
+ Cons (infixr "#" 65)
+
+ hide_const Nil Cons hd tl map
+(*>*)
+ datatype_new (set0: 'a) list0 (map: map0 rel: list0_all2) =
null: Nil (defaults tl: Nil)
- | Cons (hd: 'a) (tl: "'a list")
+ | Cons (hd: 'a) (tl: "'a list0")
text {*
\noindent
The command introduces a discriminator @{const null} and a pair of selectors
@{const hd} and @{const tl} characterized as follows:
%
-\[@{thm list.collapse(1)[of xs, no_vars]}
- \qquad @{thm list.collapse(2)[of xs, no_vars]}\]
+\[@{thm list0.collapse(1)[of xs, no_vars]}
+ \qquad @{thm list0.collapse(2)[of xs, no_vars]}\]
%
For two-constructor datatypes, a single discriminator constant suffices. The
discriminator associated with @{const Cons} is simply @{text "\<not> null"}.
@@ -348,13 +383,26 @@
datatype_new ('a, 'b) prod (infixr "*" 20) =
Pair 'a 'b
- datatype_new (set_: 'a) list_ =
+(*<*)
+ hide_const Nil Cons hd tl
+(*>*)
+ datatype_new (set: 'a) list (map: map rel: list_all2) =
null: Nil ("[]")
- | Cons (hd: 'a) (tl: "'a list_") (infixr "#" 65)
+ | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
+
+text {*
+Incidentally, this is how the traditional syntaxes are set up in @{theory List}:
+*}
+
+ syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
+
+ translations
+ "[x, xs]" == "x # [xs]"
+ "[x]" == "x # []"
-subsection {* General Syntax
- \label{ssec:datatype-general-syntax} *}
+subsection {* Syntax
+ \label{ssec:datatype-syntax} *}
text {*
Datatype definitions have the following general syntax:
@@ -410,7 +458,7 @@
specify exactly the same type variables in the same order.
@{rail "
- @{syntax_def ctor}: (@{syntax name} ':')? @{syntax name} (@{syntax ctor_arg} *) \\
+ @{syntax_def ctor}: (@{syntax name} ':')? @{syntax name} (@{syntax ctor_arg} * ) \\
@{syntax sel_defaults}? @{syntax mixfix}?
"}
@@ -444,8 +492,8 @@
(i.e., it may dependend on @{text C}'s arguments).
*}
-subsection {* Characteristic Theorems
- \label{ssec:datatype-characteristic-theorems} *}
+subsection {* Generated Theorems
+ \label{ssec:datatype-generated-theorems} *}
text {*
* free ctor theorems
@@ -520,33 +568,208 @@
More examples in \verb|~~/src/HOL/BNF/Examples|.
*}
-subsection {* Introductory Examples
- \label{ssec:primrec-introductory-examples} *}
+subsection {* Examples
+ \label{ssec:primrec-examples} *}
subsubsection {* Nonrecursive Types *}
+text {*
+ * simple (depth 1) pattern matching on the left-hand side
+*}
+
+ primrec_new bool_of_trool :: "trool \<Rightarrow> bool" where
+ "real_of_trool Faalse = False" |
+ "real_of_trool Truue = 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:
+*}
+
+ primrec_new list_of_maybe :: "'a maybe \<Rightarrow> 'a list" where
+ "list_of_maybe Nothing = []" |
+ "list_of_maybe (Just a) = [a]"
+
+ primrec_new maybe_def :: "'a \<Rightarrow> 'a maybe \<Rightarrow> 'a" where
+ "maybe_def d Nothing = d" |
+ "maybe_def _ (Just a) = a"
+
+ primrec_new mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
+ "mirrror (Triple a b c) = Triple c b a"
+
subsubsection {* Simple Recursion *}
+text {*
+again, simple pattern matching on left-hand side, but possibility
+to call a function recursively on an argument to a constructor:
+*}
+
+ primrec_new replicate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ "rep 0 _ = []" |
+ "rep (Suc n) a = a # rep n a"
+
+text {*
+we don't like the confusing name @{const nth}:
+*}
+
+ primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
+ "at (a # as) j =
+ (case j of
+ 0 \<Rightarrow> a
+ | Suc j' \<Rightarrow> at as j')"
+
+ 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)"
+
subsubsection {* Mutual Recursion *}
+text {*
+E.g., converting even/odd naturals to plain old naturals:
+*}
+
+ primrec_new
+ nat_of_enat :: "enat \<Rightarrow> nat" and
+ nat_of_onat :: "onat => nat"
+ where
+ "nat_of_enat EZero = 0" |
+ "nat_of_enat (ESuc n) = Suc (nat_of_onat n)" |
+ "nat_of_onat (OSuc n) = Suc (nat_of_enat n)"
+
+text {*
+Mutual recursion is even possible within a single type, an innovation over the
+old package:
+*}
+
+ primrec_new
+ even :: "nat \<Rightarrow> bool" and
+ odd :: "nat \<Rightarrow> bool"
+ where
+ "even 0 = True" |
+ "even (Suc n) = odd n" |
+ "odd 0 = False" |
+ "odd (Suc n) = even n"
+
+text {*
+More elaborate:
+*}
+
+ primrec_new
+ eval\<^sub>e :: "('a, 'b) exp \<Rightarrow> real" and
+ eval\<^sub>t :: "('a, 'b) trm \<Rightarrow> real" and
+ eval\<^sub>f :: "('a, 'b) fct \<Rightarrow> real"
+ where
+ "eval\<^sub>e \<gamma> \<xi> (Term t) = eval\<^sub>t \<gamma> \<xi> t" |
+ "eval\<^sub>e \<gamma> \<xi> (Sum t e) = eval\<^sub>t \<gamma> \<xi> t + eval\<^sub>e \<gamma> \<xi> e" |
+ "eval\<^sub>t \<gamma> \<xi> (Factor f) = eval\<^sub>f \<gamma> \<xi> f)" |
+ "eval\<^sub>t \<gamma> \<xi> (Prod f t) = eval\<^sub>f \<gamma> \<xi> f + eval\<^sub>t \<gamma> \<xi> t" |
+ "eval\<^sub>f \<gamma> _ (Const a) = \<gamma> a" |
+ "eval\<^sub>f _ \<xi> (Var b) = \<xi> b" |
+ "eval\<^sub>f \<gamma> \<xi> (Expr e) = eval\<^sub>e \<gamma> \<xi> e"
+
subsubsection {* Nested Recursion *}
+(*<*)
+ datatype_new 'a treeFF = NodeFF 'a "'a treeFF list"
+ datatype_new 'a treeFI = NodeFI 'a "'a treeFI llist"
+(*>*)
+ primrec_new atFF0 :: "'a treeFF \<Rightarrow> nat list \<Rightarrow> 'a" where
+ "atFF0 (NodeFF a ts) js =
+ (case js of
+ [] \<Rightarrow> a
+ | j # js' \<Rightarrow> at (map (\<lambda>t. atFF0 t js') ts) j)"
+
+ primrec_new atFI :: "'a treeFI \<Rightarrow> nat list \<Rightarrow> 'a" where
+ "atFF (NodeFI a ts) js =
+ (case js of
+ [] \<Rightarrow> a
+ | j # js' \<Rightarrow> at (llist_map (\<lambda>t. atFF t js') ts) j)"
+
+ primrec_new sum_btree :: "('a\<Colon>plus) btree \<Rightarrow> 'a" where
+ "sum_btree (BNode a lt rt) =
+ a + maybe_def 0 (maybe_map sum_btree lt) +
+ maybe_def 0 (maybe_map sum_btree rt)"
+
subsubsection {* Nested-as-Mutual Recursion *}
+text {*
+ * can pretend a nested type is mutually recursive
+ * avoids the higher-order map
+ * e.g.
+*}
-subsection {* General Syntax
- \label{ssec:primrec-general-syntax} *}
+ primrec_new
+ at_treeFF :: "'a treeFF \<Rightarrow> nat list \<Rightarrow> 'a" and
+ at_treesFF :: "'a treeFF list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a"
+ where
+ "at_treeFF (NodeFF a ts) js =
+ (case js of
+ [] \<Rightarrow> a
+ | j # js' \<Rightarrow> at_treesFF ts j js')" |
+ "at_treesFF (t # ts) j =
+ (case j of
+ 0 \<Rightarrow> at_treeFF t
+ | Suc j' \<Rightarrow> at_treesFF ts j')"
+
+ primrec_new
+ sum_btree :: "('a\<Colon>plus) btree \<Rightarrow> 'a" and
+ sum_btree_maybe :: "('a\<Colon>plus) btree maybe \<Rightarrow> 'a"
+ where
+ "sum_btree (BNode a lt rt) =
+ a + sum_btree_maybe lt + sum_btree_maybe rt" |
+ "sum_btree_maybe Nothing = 0" |
+ "sum_btree_maybe (Just t) = sum_btree t"
text {*
+ * 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
+ * there's no hard-and-fast rule of when to use one or the other,
+ just like there's no rule when to use fold and when to use
+ primrec_new
+
+ * higher-order approach, considering nesting as nesting, is more
+ compositional -- e.g. we saw how we could reuse an existing polymorphic
+ at or maybe_def, whereas at_treesFF is much more specific
+
+ * but:
+ * is perhaps less intuitive, because it requires higher-order thinking
+ * may seem inefficient, and indeed with the code generator the
+ mutually recursive version might be nicer
+ * is somewhat indirect -- must apply a map first, then compute a result
+ (cannot mix)
+ * the auxiliary functions like at_treesFF are sometimes useful in own right
+
+ * impact on automation unclear
*}
-subsection {* Characteristic Theorems
- \label{ssec:primrec-characteristic-theorems} *}
+
+subsection {* Syntax
+ \label{ssec:primrec-syntax} *}
+
+text {*
+Primitive recursive functions have the following general syntax:
+
+@{rail "
+ @@{command primrec_new} @{syntax target}? @{syntax \"fixes\"} \\ @'where'
+ (@{syntax primrec_equation} + '|')
+ ;
+ @{syntax_def primrec_equation}: @{syntax thmdecl}? @{syntax prop}
+"}
+*}
+
+
+subsection {* Generated Theorems
+ \label{ssec:primrec-generated-theorems} *}
text {*
* synthesized nonrecursive definition
@@ -559,8 +782,8 @@
* mutualized
*}
-subsection {* Recursive Default Values
- \label{ssec:recursive-default-values} *}
+subsection {* Recursive Default Values for Selectors
+ \label{ssec:recursive-default-values-for-selectors} *}
text {*
A datatype selector @{text un_D} can have a default value for each constructor
@@ -603,19 +826,22 @@
| TCons (thd: 'a) (ttl : "('a, 'b) tlist_") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs")
(*<*)
+ (* FIXME: remove hack once "primrec_new" is in place *)
rep_datatype TNil TCons
by (erule tlist_.induct, assumption) auto
(*>*)
-
overloading
termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist_ \<Rightarrow> 'b"
begin
-
-(*<*)(*FIXME: use primrec_new and avoid rep_datatype*)(*>*)
+(*<*)
+ (* FIXME: remove hack once "primrec_new" is in place *)
fun 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"
-
+(*>*)
+ 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"
end
lemma terminal_TCons[simp]: "termi (TCons x xs) = termi xs"
@@ -642,29 +868,32 @@
text {*
This section describes how to specify codatatypes using the @{command codatatype}
command.
+
+ * libraries include some useful codatatypes, notably lazy lists;
+ see the ``Coinductive'' AFP entry \cite{xxx} for an elaborate library
*}
-subsection {* Introductory Examples
- \label{ssec:codatatype-introductory-examples} *}
+subsection {* Examples
+ \label{ssec:codatatype-examples} *}
text {*
More examples in \verb|~~/src/HOL/BNF/Examples|.
*}
-subsection {* General Syntax
- \label{ssec:codatatype-general-syntax} *}
+subsection {* Syntax
+ \label{ssec:codatatype-syntax} *}
text {*
Definitions of codatatypes have almost exactly the same syntax as for datatypes
-(Section~\ref{ssec:datatype-general-syntax}), with two exceptions: The command
-is called @{command codatatype}; the \keyw{no\_dests} option is not
-available, because destructors are a central notion for codatatypes.
+(Section~\ref{ssec:datatype-syntax}), with two exceptions: The command is called
+@{command codatatype}; the \keyw{no\_dests} option is not available, because
+destructors are a central notion for codatatypes.
*}
-subsection {* Characteristic Theorems
- \label{ssec:codatatype-characteristic-theorems} *}
+subsection {* Generated Theorems
+ \label{ssec:codatatype-generated-theorems} *}
section {* Defining Corecursive Functions
@@ -679,23 +908,35 @@
*}
-subsection {* Introductory Examples
- \label{ssec:primcorec-introductory-examples} *}
+subsection {* Examples
+ \label{ssec:primcorec-examples} *}
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}).
+codatatypes (Section~\ref{ssec:recursive-default-values-for-selectors}).
*}
-subsection {* General Syntax
- \label{ssec:primcorec-general-syntax} *}
+subsection {* Syntax
+ \label{ssec:primcorec-syntax} *}
+
+text {*
+Primitive corecrusvie definitions have the following general syntax:
+
+@{rail "
+ @@{command primcorec} @{syntax target}? @{syntax \"fixes\"} \\ @'where'
+ (@{syntax primcorec_formula} + '|')
+ ;
+ @{syntax_def primcorec_formula}: @{syntax thmdecl}? @{syntax prop}
+ (@'of' (@{syntax term} * ))?
+"}
+*}
-subsection {* Characteristic Theorems
- \label{ssec:primcorec-characteristic-theorems} *}
+subsection {* Generated Theorems
+ \label{ssec:primcorec-generated-theorems} *}
section {* Registering Bounded Natural Functors
@@ -711,8 +952,8 @@
*}
-subsection {* Introductory Example
- \label{ssec:bnf-introductory-examples} *}
+subsection {* Example
+ \label{ssec:bnf-examples} *}
text {*
More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and
@@ -723,8 +964,8 @@
*}
-subsection {* General Syntax
- \label{ssec:bnf-general-syntax} *}
+subsection {* Syntax
+ \label{ssec:bnf-syntax} *}
section {* Generating Free Constructor Theorems
@@ -745,16 +986,16 @@
*}
-subsection {* Introductory Example
- \label{ssec:ctors-introductory-examples} *}
+subsection {* Example
+ \label{ssec:ctors-examples} *}
-subsection {* General Syntax
- \label{ssec:ctors-general-syntax} *}
+subsection {* Syntax
+ \label{ssec:ctors-syntax} *}
-subsection {* Characteristic Theorems
- \label{ssec:ctors-characteristic-theorems} *}
+subsection {* Generated Theorems
+ \label{ssec:ctors-generated-theorems} *}
section {* Standard ML Interface
--- a/src/Doc/Datatypes/document/root.tex Fri Aug 02 22:46:54 2013 +0200
+++ b/src/Doc/Datatypes/document/root.tex Fri Aug 02 22:54:28 2013 +0200
@@ -23,8 +23,8 @@
\renewcommand{\isacharunderscore}{\mbox{\_}}
\renewcommand{\isacharunderscorekeyword}{\mbox{\_}}
\renewcommand{\isachardoublequote}{\mbox{\upshape{``}}}
-\renewcommand{\isachardoublequoteopen}{\mbox{\upshape{``}\,}}
-\renewcommand{\isachardoublequoteclose}{\mbox{\,\upshape{''}}}
+\renewcommand{\isachardoublequoteopen}{\mbox{\upshape{``}\kern.05ex}}
+\renewcommand{\isachardoublequoteclose}{\/\kern.1ex\mbox{\upshape{''}}}
\hyphenation{isa-belle}
--- a/src/Doc/ProgProve/Bool_nat_list.thy Fri Aug 02 22:46:54 2013 +0200
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Fri Aug 02 22:54:28 2013 +0200
@@ -416,18 +416,31 @@
\fi
%
+From now on lists are always the predefined lists.
+
+
\subsection{Exercises}
\begin{exercise}
-Define your own addition, multiplication, and exponentiation functions on type
-@{typ nat}. Prove as many of the standard equational laws as possible, e.g.\
-associativity, commutativity and distributivity.
+Start from the definition of @{const add} given above.
+Prove it is associative (@{prop"add (add m n) p = add m (add n p)"})
+and commutative (@{prop"add m n = add n m"}). Define a recursive function
+@{text double} @{text"::"} @{typ"nat \<Rightarrow> nat"} and prove that @{prop"double m = add m m"}.
\end{exercise}
\begin{exercise}
-Define your own sorting function on the predefined lists.
-Prove that the result is sorted and that every element occurs as many times
-in the output as in the input.
+Define a function @{text"count ::"} @{typ"'a \<Rightarrow> 'a list \<Rightarrow> nat"}
+that counts the number of occurrences of an element in a list. Prove
+@{prop"count x xs \<le> length xs"}.
+\end{exercise}
+
+\begin{exercise}
+Define a recursive function @{text "snoc ::"} @{typ"'a list \<Rightarrow> 'a \<Rightarrow> 'a list"}
+that appends an element to the end of a list. Do not use the predefined append
+operator @{text"@"}. With the help of @{text snoc} define a recursive function
+@{text "reverse ::"} @{typ"'a list \<Rightarrow> 'a list"} that reverses a list. Do not
+use the predefined function @{const rev}.
+Prove @{prop"reverse(reverse xs) = xs"}.
\end{exercise}
*}
(*<*)
--- a/src/HOL/BNF/Examples/Misc_Data.thy Fri Aug 02 22:46:54 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Data.thy Fri Aug 02 22:54:28 2013 +0200
@@ -154,6 +154,7 @@
datatype_new 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
+datatype_new 'a deadfoo = C "'a \<Rightarrow> 'a + 'a"
datatype_new 'a dead_foo = A
datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
--- a/src/HOL/BNF/Tools/bnf_def.ML Fri Aug 02 22:46:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Fri Aug 02 22:54:28 2013 +0200
@@ -1107,7 +1107,7 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
- (mk_rel_mono_tac rel_OO_Grps (Lazy.force in_mono))
+ (K (mk_rel_mono_tac rel_OO_Grps (Lazy.force in_mono)))
|> Thm.close_derivation
end;
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Fri Aug 02 22:46:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Fri Aug 02 22:54:28 2013 +0200
@@ -25,7 +25,7 @@
val mk_rel_conversep_tac: thm -> thm -> tactic
val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_rel_mono_tac: thm list -> thm -> tactic
val mk_rel_mono_strong_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_map_transfer_tac: thm -> thm -> thm list -> thm -> thm ->
@@ -42,6 +42,7 @@
open BNF_Tactics
val ord_eq_le_trans = @{thm ord_eq_le_trans};
+val ord_le_eq_trans = @{thm ord_le_eq_trans};
val conversep_shift = @{thm conversep_le_swap} RS iffD1;
fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
@@ -85,12 +86,13 @@
{context = ctxt, prems = _} =
let
val n = length set_maps;
+ val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans);
in
if null set_maps then
unfold_thms_tac ctxt ((map_id RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
rtac @{thm Grp_UNIV_idI[OF refl]} 1
- else unfold_thms_tac ctxt rel_OO_Grps THEN
- EVERY' [rtac @{thm antisym}, rtac @{thm predicate2I},
+ else
+ EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
REPEAT_DETERM o
eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
@@ -122,20 +124,28 @@
rtac @{thm equalityI}, rtac subset_UNIV, rtac subsetI, rtac CollectI,
CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id])) 1;
-fun mk_rel_mono_tac rel_OO_Grps in_mono {context = ctxt, prems = _} =
- unfold_thms_tac ctxt rel_OO_Grps THEN
- EVERY' [rtac @{thm relcompp_mono}, rtac @{thm iffD2[OF conversep_mono]},
+fun mk_rel_mono_tac rel_OO_Grps in_mono =
+ let
+ val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
+ else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
+ rtac (hd rel_OO_Grps RS sym RSN (2, ord_le_eq_trans));
+ in
+ EVERY' [rel_OO_Grps_tac, rtac @{thm relcompp_mono}, rtac @{thm iffD2[OF conversep_mono]},
rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono},
- rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1;
+ rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1
+ end;
fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
+ val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
+ else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
+ rtac (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans));
in
if null set_maps then rtac (rel_eq RS @{thm leq_conversepI}) 1
- else unfold_thms_tac ctxt (rel_OO_Grps) THEN
- EVERY' [rtac @{thm predicate2I},
+ else
+ EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I},
REPEAT_DETERM o
eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
hyp_subst_tac ctxt, rtac @{thm conversepI}, rtac @{thm relcomppI}, rtac @{thm conversepI},
@@ -151,17 +161,21 @@
rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
-fun mk_rel_OO_tac rel_OO_Grs rel_eq map_cong0 map_wppull map_comp set_maps
+fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
fun in_tac nthO_in = rtac CollectI THEN'
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps;
+ val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
+ else rtac (hd rel_OO_Grps RS trans) THEN'
+ rtac (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN
+ (2, trans));
in
if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1
- else unfold_thms_tac ctxt rel_OO_Grs THEN
- EVERY' [rtac @{thm antisym}, rtac @{thm predicate2I},
+ else
+ EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
REPEAT_DETERM o
eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
hyp_subst_tac ctxt,
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Aug 02 22:46:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Aug 02 22:54:28 2013 +0200
@@ -23,7 +23,8 @@
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
- xtor_co_iter_thmss: thm list list}
+ xtor_co_iter_thmss: thm list list,
+ rel_co_induct_thm: thm}
val morph_fp_result: morphism -> fp_result -> fp_result
val eq_fp_result: fp_result * fp_result -> bool
@@ -203,10 +204,12 @@
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
- xtor_co_iter_thmss: thm list list};
+ xtor_co_iter_thmss: thm list list,
+ rel_co_induct_thm: thm};
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_inducts, dtor_ctors,
- ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss} =
+ ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss,
+ rel_co_induct_thm} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
@@ -219,7 +222,8 @@
xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
- xtor_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss};
+ xtor_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss,
+ rel_co_induct_thm = Morphism.thm phi rel_co_induct_thm};
fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
eq_list eq_bnf (bnfs1, bnfs2);
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Aug 02 22:46:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Aug 02 22:54:28 2013 +0200
@@ -2920,7 +2920,8 @@
ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss',
xtor_rel_thms = dtor_Jrel_thms,
- xtor_co_iter_thmss = transpose [ctor_dtor_unfold_thms, ctor_dtor_corec_thms]},
+ xtor_co_iter_thmss = transpose [ctor_dtor_unfold_thms, ctor_dtor_corec_thms],
+ rel_co_induct_thm = Jrel_coinduct_thm},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Aug 02 22:46:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Aug 02 22:54:28 2013 +0200
@@ -1847,7 +1847,8 @@
xtor_co_inducts = [ctor_induct_thm], dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
ctor_injects = ctor_inject_thms, xtor_map_thms = folded_ctor_map_thms,
xtor_set_thmss = folded_ctor_set_thmss', xtor_rel_thms = ctor_Irel_thms,
- xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms]},
+ xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms],
+ rel_co_induct_thm = Irel_induct_thm},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;