--- a/src/Doc/Datatypes/Datatypes.thy Fri Dec 04 21:39:38 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Dec 04 22:19:04 2015 +0100
@@ -134,7 +134,6 @@
Limitations,'' concludes with known open issues at the time of writing.
\end{itemize}
-
\newbox\boxA
\setbox\boxA=\hbox{\texttt{NOSPAM}}
@@ -142,7 +141,7 @@
in.\allowbreak tum.\allowbreak de}}
Comments and bug reports concerning either the package or this tutorial should
-be directed to the first author at \authoremaili or to the
+be directed to the first author at \authoremaili{} or to the
\texttt{cl-isabelle-users} mailing list.
*}
@@ -1967,9 +1966,12 @@
text {*
Corecursive functions can be specified using the @{command primcorec} and
-\keyw{prim\-corec\-ursive} commands, which support primitive corecursion, or
-using the more general \keyw{partial_function} command. In this tutorial, the
-focus is on the first two. More examples can be found in %the directory
+\keyw{prim\-corec\-ursive} commands, which support primitive corecursion.
+Other approaches include the more general \keyw{partial_function} command, the
+forthcoming \keyw{corec} command @{cite "blanchette-et-al-2015-corec"}, and
+techniques based on domains and topologies @{cite "lochbihler-hoelzl-2014"}.
+In this tutorial, the focus is on @{command primcorec} and
+@{command primcorecursive}. More examples can be found in the directory
@{file "~~/src/HOL/Datatype_Examples"}.
Whereas recursive functions consume datatypes one constructor at a time,
@@ -3136,6 +3138,11 @@
datatype (plugins del: code "quickcheck") color = Red | Black
+text {*
+Beyond the standard plugins, the \emph{Archive of Formal Proofs} includes a
+\keyw{derive} command that derives class instances of datatypes
+@{cite "sternagel-thiemann-2015"}.
+*}
subsection {* Code Generator
\label{ssec:code-generator} *}
@@ -3218,7 +3225,8 @@
@{text "'a\<^sub>1, \<dots>, 'a\<^sub>m"}, by default @{text u} values are given a size of 0. This
can be improved upon by registering a custom size function of type
@{text "('a\<^sub>1 \<Rightarrow> nat) \<Rightarrow> \<dots> \<Rightarrow> ('a\<^sub>m \<Rightarrow> nat) \<Rightarrow> u \<Rightarrow> nat"} using
-@{ML BNF_LFP_Size.register_size} or @{ML BNF_LFP_Size.register_size_global}. See
+the ML function @{ML BNF_LFP_Size.register_size} or
+@{ML BNF_LFP_Size.register_size_global}. See theory
@{file "~~/src/HOL/Library/Multiset.thy"} for an example.
*}
@@ -3271,12 +3279,17 @@
For (co)datatypes with at least one live type argument, the plugin sets the
@{text "[transfer_rule]"} attribute on the following (co)datatypes properties:
-@{text "t.case_transfer"}, @{text "t.sel_transfer"}, @{text "t.ctr_transfer"},
-@{text "t.disc_transfer"}, @{text "t.rec_transfer"}, and @{text
-"t.corec_transfer"}. For (co)datatypes that further have \emph{no dead type
-arguments}, the plugin sets @{text "[transfer_rule]"} on
-@{text "t.set_transfer"}, @{text "t.map_transfer"}, and
-@{text "t.rel_transfer"}.
+@{text "t.case_"}\allowbreak @{text "transfer"},
+@{text "t.sel_"}\allowbreak @{text "transfer"},
+@{text "t.ctr_"}\allowbreak @{text "transfer"},
+@{text "t.disc_"}\allowbreak @{text "transfer"},
+@{text "t.rec_"}\allowbreak @{text "transfer"}, and
+@{text "t.corec_"}\allowbreak @{text "transfer"}.
+For (co)datatypes that further have \emph{no dead type arguments}, the plugin
+sets @{text "[transfer_rule]"} on
+@{text "t.set_"}\allowbreak @{text "transfer"},
+@{text "t.map_"}\allowbreak @{text "transfer"}, and
+@{text "t.rel_"}\allowbreak @{text "transfer"}.
For @{command primrec}, @{command primcorec}, and @{command primcorecursive},
the plugin implements the generation of the @{text "f.transfer"} property,
@@ -3382,7 +3395,7 @@
\item
\emph{The compatibility layer sometimes produces induction principles with a
-slightly different shape than the old package.}
+slightly different ordering of the premises than the old package.}
\end{enumerate}
*}
--- a/src/Doc/manual.bib Fri Dec 04 21:39:38 2015 +0100
+++ b/src/Doc/manual.bib Fri Dec 04 22:19:04 2015 +0100
@@ -337,7 +337,7 @@
Andrei Popescu and
Dmitriy Traytel},
title = {Witnessing (Co)datatypes},
- booktitle = {{ESOP} 2015},
+ booktitle = {24th European Symposium on Programming, {ESOP} 2015},
pages = {359--382},
year = {2015},
editor = {Jan Vitek},
@@ -346,6 +346,20 @@
publisher = {Springer}
}
+@inproceedings{blanchette-et-al-2015-corec,
+ author = {Jasmin Christian Blanchette and
+ Andrei Popescu and
+ Dmitriy Traytel},
+ title = {Foundational extensible corecursion: a proof assistant perspective},
+ booktitle = {20th {ACM} {SIGPLAN} International Conference on
+ Functional Programming, {ICFP} 2015},
+ pages = {192--204},
+ year = {2015},
+ editor = {Kathleen Fisher and
+ John H. Reppy},
+ publisher = {{ACM}},
+}
+
@inproceedings{blanchette-et-al-2014-impl,
author = "Jasmin Christian Blanchette and Johannes H{\"o}lzl
and Andreas Lochbihler and Lorenz Panny and Andrei Popescu and Dmitriy Traytel",
@@ -353,8 +367,8 @@
year = 2014,
publisher = "Springer",
editor = "Gerwin Klein and Ruben Gamboa",
- booktitle = "ITP 2014",
- series = "LNCS",
+ booktitle = {5th International Conference on Interactive Theorem Proving, ITP 2014},
+ series = LNCS,
volume = 8558,
pages = "93--110"
}
@@ -710,7 +724,8 @@
title = {Edinburgh {LCF}: A Mechanised Logic of Computation},
year = 1979,
publisher = {Springer},
- series = {LNCS 78}}
+ series = LNCS,
+ volume = 78}
@inproceedings{Gunter-HOL92,author={Elsa L. Gunter},
title={Why we can't have {SML} style datatype declarations in {HOL}},
@@ -1038,6 +1053,22 @@
month = "Feb.",
year = 2010}
+@inproceedings{lochbihler-hoelzl-2014,
+ author = {Andreas Lochbihler and
+ Johannes H{\"{o}}lzl},
+ title = {Recursive Functions on Lazy Lists via Domains and Topologies},
+ booktitle = {Interactive Theorem Proving --- 5th International Conference, {ITP}
+ 2014},
+ pages = {341--357},
+ year = {2014},
+ editor = {Gerwin Klein and
+ Ruben Gamboa},
+ series = LNCS,
+ volume = {8558},
+ publisher = {Springer},
+ year = {2014}
+}
+
@book{loveland-78,
author = "D. W. Loveland",
title = "Automated Theorem Proving: A Logical Basis",
@@ -1706,6 +1737,15 @@
pages = "341--355",
crossref = {cade12}}
+@incollection{sternagel-thiemann-2015,
+ title = "Deriving Class Instances for Datatypes",
+ author = "Christian Sternagel and Ren\'e Thiemann",
+ booktitle = "The Archive of Formal Proofs",
+ editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
+ publisher = "\url{http://afp.sourceforge.net/entries/Deriving.shtml}",
+ month = "March",
+ year = 2015}
+
@book{suppes72,
author = {Patrick Suppes},
title = {Axiomatic Set Theory},
@@ -1820,7 +1860,7 @@
Logic---{C}ategory Theory Applied to Theorem Proving},
year = {2012},
pages = {596--605},
- booktitle = {LICS 2012},
+ booktitle = {27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012},
publisher = {IEEE}
}
@@ -2013,8 +2053,7 @@
@inproceedings{Wenzel:2014:ITP-PIDE,
author = {Makarius Wenzel},
title = {Asynchronous User Interaction and Tool Integration in {Isabelle/PIDE}},
- booktitle = {Interactive Theorem Proving --- 5th International Conference,
- ITP 2014, Vienna, Austria},
+ booktitle = {5th International Conference on Interactive Theorem Proving, ITP 2014},
editor = {Gerwin Klein and Ruben Gamboa},
year = {2014},
publisher = {Springer},