# HG changeset patch # User blanchet # Date 1449263944 -3600 # Node ID 1e4caf2beb5d8668c38d13947704c3f2f1fe5e0b # Parent 0ccb1eaa2184a10909df0b5ab8e0969efe374cba tuned docs diff -r 0ccb1eaa2184 -r 1e4caf2beb5d src/Doc/Datatypes/Datatypes.thy --- 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, \, '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 \ nat) \ \ \ ('a\<^sub>m \ nat) \ u \ 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} *} diff -r 0ccb1eaa2184 -r 1e4caf2beb5d src/Doc/manual.bib --- 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},