# HG changeset patch # User blanchet # Date 1459343810 -7200 # Node ID d4b7d128ec5ad166557228eb6c204878fb3e42e6 # Parent 7fde2461f9ef0515cca38e1152c6e7800221eb7d more 'corec' docs diff -r 7fde2461f9ef -r d4b7d128ec5a src/Doc/Corec/Corec.thy --- a/src/Doc/Corec/Corec.thy Tue Mar 29 23:45:28 2016 +0200 +++ b/src/Doc/Corec/Corec.thy Wed Mar 30 15:16:50 2016 +0200 @@ -20,19 +20,104 @@ \label{sec:introduction}\ text \ -... -@{cite "isabelle-datatypes"} +Isabelle's (co)datatype package @{cite "isabelle-datatypes"} offers a convenient +syntax for introducing codatatypes. For example, the type of (infinite) streams +can be defined as follows (cf. @{file "~~/src/HOL/Library/Stream.thy"}): +\ + + codatatype 'a stream = + SCons (shd: 'a) (stl: "'a stream") + +text \ +\noindent +The (co)datatype package also provides two commands, \keyw{primcorec} and +\keyw{prim\-corec\-ur\-sive}, for defining primitively corecursive functions. + +This tutorial presents a definitional package for functions beyond +primitive corecursion. It describes @{command corec} and related commands:\ +@{command corecursive}, @{command friend_of_corec}, and @{command coinduction_upto}. +It also covers the @{method corec_unique} proof method. +The package is not part of @{theory Main}; it is located in +@{file "~~/src/HOL/Library/BNF_Corec.thy"}. -* friend -* up to +The @{command corec} command generalizes \keyw{primcorec} in three main +respects. First, it allows multiple constructors around corecursive calls, where +\keyw{primcorec} expects exactly one. For example: +\ + + corec oneTwos :: "nat stream" where + "oneTwos = SCons 1 (SCons 2 oneTwos)" + +text \ +Second, @{command corec} allows other functions than constructors to appear in +the corecursive call context (i.e., around any self-calls on the right-hand side +of the equation). The requirement on these functions is that they must be +\emph{friendly}. Intuitively, a function is friendly if it needs to destruct +at most one constructor of input to produce one constructor of output. +We can register functions as friendly using the @{command friend_of_corec} +command, or by passing the @{text friend} option to @{command corec}. The +friendliness check relies on an internal syntactic check in combination with +a parametricity subgoal, which must be discharged manually (typically using +@{method transfer_prover}). + +Third, @{command corec} allows self-calls that are not guarded by a constructor, +as long as these calls occur in a friendly context (a context consisting +exclusively of friendly functions) and can be shown to be terminating +(well founded). The mixture of recursive and corecursive calls in a single +function can be quite useful in practice. -* versioning +Internally, the package synthesizes corecursors that take into account the +possible call contexts. The corecursor is accompanined by a corresponding, +equally general coinduction principle. The corecursor and the coinduction +principle grow in expressiveness as we interact with it. In process algebra +terminology, corecursion and coinduction take place \emph{up to} friendly +contexts. -BNF +The package fully adheres to the LCF philosophy @{cite mgordon79}: The +characteristic theorems associated with the specified corecursive functions are +derived rather than introduced axiomatically.% +\footnote{However, most of the internal proof obligations are omitted if the +@{text quick_and_dirty} option is enabled.} +The package is described in a pair of scientific papers +@{cite "blanchette-et-al-2015-fouco" and "blanchette-et-al-2016-fouco2"}. Some +of the text and examples below originate from there. + +This tutorial is organized as follows: + +\begin{itemize} +\setlength{\itemsep}{0pt} + +\item Section \ref{sec:introductory-examples}, ``Introductory Examples,'' +describes how to specify corecursive functions and to reason about them. -link to papers +\item Section \ref{sec:command-syntax}, ``Command Syntax,'' describes the syntax +of the commands offered by the package. + +\item Section \ref{sec:generated-theorems}, ``Generated Theorems,'' lists the +theorems produced by the package's commands. + +\item Section \ref{sec:proof-method}, ``Proof Method,'' briefly describes the +@{method corec_unique} proof method. + +\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and +Limitations,'' concludes with known open issues. +\end{itemize} -* plugins (code) +Although it is more powerful than \keyw{primcorec} in many respects, +@{command corec} suffers from a number of limitations. Most notably, it does +not support mutually corecursive codatatypes, and it is less efficient than +\keyw{primcorec} because it needs to dynamically synthesize corecursors and +corresponding coinduction principles to accommodate the friends. + +\newbox\boxA +\setbox\boxA=\hbox{\texttt{NOSPAM}} + +\newcommand\authoremaili{\texttt{jasmin.blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak +gmail.\allowbreak com}} + +Comments and bug reports concerning either the package or this tutorial should +be directed to the first author at \authoremaili{} or to the +\texttt{cl-isabelle-users} mailing list. \ @@ -40,6 +125,9 @@ \label{sec:introductory-examples}\ text \ +The package is illustrated through concrete examples featuring different flavors +of corecursion. More examples can be found in the directory +@{file "~~/src/HOL/Corec_Examples"}. \ @@ -48,29 +136,8 @@ text \ The case studies by Rutten~@{cite rutten05} and Hinze~@{cite hinze10} on stream -calculi serve as our starting point. Streams can be defined as follows -(cf. @{file "~~/src/HOL/Library/Stream.thy"}): -\ - - codatatype 'a stream = - SCons (shd: 'a) (stl: "'a stream") - -text \ -The @{command corec} command makes it possible to define functions where the -corecursive call occurs under two or more constructors: -\ - - corec oneTwos :: "nat stream" where - "oneTwos = SCons 1 (SCons 2 oneTwos)" - -thm oneTwos.cong_intros - -text \ -\noindent -This is already beyond the syntactic fragment supported by \keyw{primcorec}. - -The following definition of pointwise sum can be performed with either -\keyw{primcorec} or @{command corec}: +calculi serve as our starting point. The following definition of pointwise sum +can be performed with either \keyw{primcorec} or @{command corec}: \ primcorec ssum :: "('a :: plus) stream \ 'a stream \ 'a stream" where @@ -92,9 +159,11 @@ text \ \noindent -The command emits two subgoals. The first one corresponds to the equation we -specified and is trivial to discharge. The second one is a parametricity subgoal -and can usually be discharged using the @{text transfer_prover} proof method. +The command emits two subgoals. The first subgoal corresponds to the equation we +specified and is trivial to discharge. The second subgoal is a parametricity +property that captures the the requirement that the function may destruct at +most one constructor of input to produce one constructor of output. This subgoal +can usually be discharged using the @{text transfer_prover} proof method. After registering @{const ssum} as a friend, we can use it in the corecursive call context, either inside or outside the constructor guard: @@ -136,11 +205,13 @@ corec factA :: "nat stream" where "factA = (let zs = SCons 1 factA in sprod zs zs)" +text \\blankline\ + corec factB :: "nat stream" where "factB = sexp (SCons 0 factB)" text \ -The arguments of friendly operations can be of complex types involving the +The arguments of friendly functions can be of complex types involving the target codatatype. The following example defines the supremum of a finite set of streams by primitive corecursion and registers it as friendly: \ @@ -150,13 +221,14 @@ text \ \noindent -In general, the arguments may be any BNF, with the restriction that the target -codatatype (@{typ "nat stream"}) may occur only in a live position of the BNF. -For this reason, the following operation, on unbounded sets, cannot be -registered as a friend: +In general, the arguments may be any bounded natural functor (BNF) +@{cite "isabelle-datatypes"}, with the restriction that the target codatatype +(@{typ "nat stream"}) may occur only in a \emph{live} position of the BNF. For +this reason, the following function, on unbounded sets, cannot be registered as +a friend: \ - corec ssup :: "nat stream set \ nat stream" where + primcorec ssup :: "nat stream set \ nat stream" where "ssup X = SCons (Sup (image shd X)) (ssup (image stl X))" @@ -176,25 +248,25 @@ We first define the pointwise sum of two trees analogously to @{const ssum}: \ - corec (friend) tplus :: "('a :: plus) tree \ 'a tree \ 'a tree" where - "tplus t u = - Node (lab t + lab u) (map (\(t', u'). tplus t' u') (zip (sub t) (sub u)))" + corec (friend) tsum :: "('a :: plus) tree \ 'a tree \ 'a tree" where + "tsum t u = + Node (lab t + lab u) (map (\(t', u'). tsum t' u') (zip (sub t) (sub u)))" text \ \noindent Here, @{const map} is the standard map function on lists, and @{const zip} -converts two parallel lists into a list of pairs. The @{const tplus} function is +converts two parallel lists into a list of pairs. The @{const tsum} function is primitively corecursive. Instead of @{text "corec (friend)"}, we could also have used \keyw{primcorec} and @{command friend_of_corec}, as we did for @{const ssum}. -Once @{const tplus} is registered as friendly, we can use it in the corecursive -call context: +Once @{const tsum} is registered as friendly, we can use it in the corecursive +call context of another function: \ corec (friend) ttimes :: "('a :: {plus,times}) tree \ 'a tree \ 'a tree" where "ttimes t u = Node (lab t * lab u) - (map (\(t', u'). tplus (ttimes t u') (ttimes t' u)) (zip (sub t) (sub u)))" + (map (\(t', u'). tsum (ttimes t u') (ttimes t' u)) (zip (sub t) (sub u)))" text \ All the syntactic convenience provided by \keyw{primcorec} is also supported by @@ -241,12 +313,10 @@ It is often convenient to let a corecursive function perform some finite computation before producing a constructor. With mixed recursion--corecursion, a finite number of unguarded recursive calls perform this calculation before -reaching a guarded corecursive call. - -Intuitively, the unguarded recursive call can be unfolded to arbitrary finite -depth, ultimately yielding a purely corecursive definition. An example is the -@{term primes} function from Di Gianantonio and Miculan -@{cite "di-gianantonio-miculan-2003"}: +reaching a guarded corecursive call. Intuitively, the unguarded recursive call +can be unfolded to arbitrary finite depth, ultimately yielding a purely +corecursive definition. An example is the @{term primes} function from Di +Gianantonio and Miculan @{cite "di-gianantonio-miculan-2003"}: \ corecursive primes :: "nat \ nat \ nat stream" where @@ -266,17 +336,17 @@ The @{command corecursive} command is a variant of @{command corec} that allows us to specify a termination argument for any unguarded self-call. -When called with @{term "m = 1"} and @{term "n = 2"}, the @{const primes} +When called with @{text "m = 1"} and @{text "n = 2"}, the @{const primes} function computes the stream of prime numbers. The unguarded call in the @{text else} branch increments @{term n} until it is coprime to the first argument @{term m} (i.e., the greatest common divisor of @{term m} and -@{term n} is @{term 1}). +@{term n} is @{text 1}). For any positive integers @{term m} and @{term n}, the numbers @{term m} and -@{term "m * n + 1"} are coprime, yielding an upper bound on the number of times +@{text "m * n + 1"} are coprime, yielding an upper bound on the number of times @{term n} is increased. Hence, the function will take the @{text else} branch at most finitely often before taking the then branch and producing one constructor. -There is a slight complication when @{term "m = 0 \ n > 1"}: Without the first +There is a slight complication when @{text "m = 0 \ n > 1"}: Without the first disjunct in the @{text "if"} condition, the function could stall. (This corner case was overlooked in the original example @{cite "di-gianantonio-miculan-2003"}.) @@ -290,6 +360,8 @@ (if n > 0 then ssum (catalan (n - 1)) (SCons 0 (catalan (n + 1))) else SCons 1 (catalan 1))" +text \\blankline\ + corec collatz :: "nat \ nat stream" where "collatz n = (if even n \ n > 0 then collatz (n div 2) else SCons n (collatz (3 * n + 1)))" @@ -304,8 +376,8 @@ \label{ssec:self-friendship}\ text \ -Paradoxically, the package allows us to simultaneously define a function and use -it as its own friend, as in the following definition of a ``skewed product'': +The package allows us to simultaneously define a function and use it as its own +friend, as in the following definition of a ``skewed product'': \ corec (friend) @@ -346,16 +418,18 @@ The coinduction up-to principle after registering @{const sskew} as friendly is available as @{thm [source] sskew.coinduct} and as one of the components of -the collection @{thm [source] stream.coinduct_upto}: +the theorem collection @{thm [source] stream.coinduct_upto}: % \begin{indentblock} -@{thm sfsup.coinduct[no_vars]} +@{thm sskew.coinduct[no_vars]} \end{indentblock} % This rule is almost identical to structural coinduction, except that the -corecursive application of @{term R} is replaced by -@{term "stream.v5.congclp R"}. The @{const stream.v5.congclp} predicate is -equipped with the following introduction rules: +corecursive application of @{term R} is generalized to +@{term "stream.v5.congclp R"}. + +The @{const stream.v5.congclp} predicate is equipped with the following +introduction rules: \begin{indentblock} \begin{description} @@ -394,6 +468,11 @@ because @{const sexp} has a more restrictive result type than @{const sskew} (@{typ "nat stream"} vs. @{typ "('a :: {plus,times}) stream"}. +The version numbers, here @{text v5}, distinguish the different congruence +closures generated for a given codatatype as more friends are registered. As +much as possible, it is recommended to avoid referring to them in proof +documents. + Since the package maintains a set of incomparable corecursors, there is also a set of associated coinduction principles and a set of sets of introduction rules. A technically subtle point is to make Isabelle choose the right rules in @@ -416,12 +495,16 @@ TNil (terminal: 'b) | TCons (thd: 'a) (ttl: "('a, 'b) tllist") +text \\blankline\ + corec (friend) square_elems :: "(nat, 'b) tllist \ (nat, 'b) tllist" where "square_elems xs = (case xs of TNil z \ TNil z | TCons y ys \ TCons (y ^^ 2) (square_elems ys))" +text \\blankline\ + corec (friend) square_terminal :: "('a, int) tllist \ ('a, int) tllist" where "square_terminal xs = (case xs of @@ -447,7 +530,7 @@ @{const square_elems}, and @{const square_terminal}. \end{itemize} % -To generate it, without having to define a new function with @{command corec}, +To generate it without having to define a new function with @{command corec}, we can use the following command: \ @@ -455,9 +538,15 @@ text \ \noindent -This produces the theorems @{thm [source] nat_int_tllist.coinduct_upto} and -@{thm [source] nat_int_tllist.cong_intros} (as well as the individually named -introduction rules) and extends @{thm [source] tllist.coinduct_upto} and +This produces the theorems +% +\begin{indentblock} +@{thm [source] nat_int_tllist.coinduct_upto} \\ +@{thm [source] nat_int_tllist.cong_intros} +\end{indentblock} +% +(as well as the individually named introduction rules) and extends +the dynamic collections @{thm [source] tllist.coinduct_upto} and @{thm [source] tllist.cong_intros}. \ @@ -469,12 +558,12 @@ It is sometimes possible to achieve better automation by using a more specialized proof method than coinduction. Uniqueness principles maintain a good balance between expressiveness and automation. They exploit the property that a -corecursive specification is the unique solution to a fixpoint equation. +corecursive definition is the unique solution to a fixpoint equation. The @{command corec}, @{command corecursive}, and @{command friend_of_corec} commands generate a property @{text f.unique} about the function of interest @{term f} that can be used to prove that any function that satisfies -@{term f}'s corecursive specification must be equal to @{term f}. For example: +@{term f}'s corecursive specification must be equal to~@{term f}. For example: \[@{thm ssum.unique[no_vars]}\] The uniqueness principles are not restricted to functions defined using @@ -485,11 +574,11 @@ \[@{term "(\x. f x = H x f) \ f x = t x"}\] into \[@{term "\x. t x = H x t"}\] -The higher-order functional @{term H} must be such that the equation -@{term "f x = H x f"} would be a valid @{command corec} specification---but -without nested self-calls or unguarded calls. Thus, @{method corec_unique} -proves uniqueness of @{term t} with respect to the given fixpoint equation -regardless of how @{term t} was defined. For example: +The higher-order functional @{term H} must be such that @{term "f x = H x f"} +would be a valid @{command corec} specification, but without nested self-calls +or unguarded (recursive) calls. Thus, @{method corec_unique} proves uniqueness +of @{term t} with respect to the given corecursive equation regardless of how +@{term t} was defined. For example: \ lemma @@ -506,12 +595,22 @@ by simp qed +text \ +The proof method relies on some theorems generated by the package. If no function +over a given codatatype has been defined using @{command corec} or +@{command corecursive} or registered as friendly using @{command friend_of_corec}, +the theorems will not be available yet. In such cases, the theorems can be +explicitly generated using the command +\ + + coinduction_upto stream: "'a stream" + section \Command Syntax \label{sec:command-syntax}\ subsection \\keyw{corec} and \keyw{corecursive} - \label{ssec:corec-and-corecursive}\ + \label{ssec:corec-and-corecursive-syntax}\ text \ \begin{matharray}{rcl} @@ -556,14 +655,14 @@ @{text "[transfer_rule]"} attribute is set on the generated theorem. \end{itemize} -The @{command corec} command is an abbreviation for @{command corecursive} with -@{text "apply transfer_prover"} or @{text "apply lexicographic_order"} to -discharge any emerging proof obligations. +The @{command corec} command is an abbreviation for @{command corecursive} +with appropriate applications of @{method transfer_prover} and +@{method lexicographic_order} to discharge any emerging proof obligations. \ subsection \\keyw{friend_of_corec} - \label{ssec:friend-of-corec}\ + \label{ssec:friend-of-corec-syntax}\ text \ \begin{matharray}{rcl} @@ -606,7 +705,7 @@ subsection \\keyw{coinduction_upto} - \label{ssec:coinduction-upto}\ + \label{ssec:coinduction-upto-syntax}\ text \ \begin{matharray}{rcl} @@ -633,47 +732,150 @@ \label{sec:generated-theorems}\ text \ -... +The full list of named theorems generated by the package can be obtained by +issuing the command \keyw{print_theorems} immediately after the datatype definition. +This list excludes low-level theorems that reveal internal constructions. To +make these accessible, add the line +\ + + declare [[bnf_internals]] +(*<*) + declare [[bnf_internals = false]] +(*>*) + +text \ +In addition to the theorem listed below for each command provided by the +package, all commands update the dynamic theorem collections + +\begin{indentblock} +\begin{description} + +\item[@{text "t."}\hthm{coinduct_upto}] + +\item[@{text "t."}\hthm{cong_intros}] + +\end{description} +\end{indentblock} +% +for the corresponding codatatype @{text t} so that they always contain the most +powerful coinduction up-to principles derived so far. \ subsection \\keyw{corec} and \keyw{corecursive} - \label{ssec:corec-and-corecursive}\ + \label{ssec:corec-and-corecursive-theorems}\ text \ -... +For a function @{term f} over codatatype @{text t}, the @{command corec} and +@{command corecursive} commands generate the following properties (listed for +@{const sexp}, cf. Section~\ref{ssec:simple-corecursion}): + +\begin{indentblock} +\begin{description} + +\item[@{text "f."}\hthm{code} @{text "[code]"}\rm:] ~ \\ +@{thm sexp.code[no_vars]} \\ +The @{text "[code]"} attribute is set by the @{text code} plugin +@{cite "isabelle-datatypes"}. + +\item[@{text "f."}\hthm{coinduct} @{text "[consumes 1, case_names t, case_conclusion D\<^sub>1 \ + D\<^sub>n]"}\rm:] ~ \\ +@{thm sexp.coinduct[no_vars]} + +\item[@{text "f."}\hthm{cong_intros}\rm:] ~ \\ +@{thm sexp.cong_intros[no_vars]} + +\item[@{text "f."}\hthm{unique}\rm:] ~ \\ +@{thm sexp.unique[no_vars]} \\ +This property is not generated for mixed recursive--corecursive definitions. + +\item[@{text "f."}\hthm{inner_induct}\rm:] ~ \\ +This property is only generated for mixed recursive--corecursive definitions. +For @{const primes} (Section~\ref{ssec:mixed-recursion-corecursion}, it reads as +follows: \\[\jot] +@{thm primes.inner_induct[no_vars]} + +\end{description} +\end{indentblock} + +\noindent +The individual rules making up @{text "f.cong_intros"} are available as + +\begin{indentblock} +\begin{description} + +\item[@{text "f."}\hthm{cong_base}] + +\item[@{text "f."}\hthm{cong_refl}] + +\item[@{text "f."}\hthm{cong_sym}] + +\item[@{text "f."}\hthm{cong_trans}] + +\item[@{text "f."}\hthm{cong_C\textsubscript{1}}, \ldots, @{text "f."}\hthm{cong_C\textsubscript{\textit{n}}}] ~ \\ +where @{text "C\<^sub>1"}, @{text "\"}, @{text "C\<^sub>n"} are @{text t}'s +constructors + +\item[@{text "f."}\hthm{cong_f\textsubscript{1}}, \ldots, @{text "f."}\hthm{cong_f\textsubscript{\textit{m}}}] ~ \\ +where @{text "f\<^sub>1"}, @{text "\"}, @{text "f\<^sub>m"} are the available +friends for @{text t} + +\end{description} +\end{indentblock} \ subsection \\keyw{friend_of_corec} - \label{ssec:friend-of-corec}\ + \label{ssec:friend-of-corec-theorems}\ text \ -... +The @{command friend_of_corec} command generates the same theorems as +@{command corec} and @{command corecursive}, except that it adds an optional +@{text "friend."} component to the names to prevent potential clashes (e.g., +@{text "f.friend.code"}). \ subsection \\keyw{coinduction_upto} - \label{ssec:coinduction-upto}\ + \label{ssec:coinduction-upto-theorems}\ text \ -... +The @{command coinduction_upto} command generates the following properties +(listed for @{text nat_int_tllist}): + +\begin{indentblock} +\begin{description} + +\item[\begin{tabular}{@ {}l@ {}} + @{text "t."}\hthm{coinduct_upto} @{text "[consumes 1, case_names t,"} \\ + \phantom{@{text "t."}\hthm{coinduct_upto} @{text "["}}@{text "case_conclusion D\<^sub>1 \ + D\<^sub>n]"}\rm: +\end{tabular}] ~ \\ +@{thm nat_int_tllist.coinduct_upto[no_vars]} + +\item[@{text "t."}\hthm{cong_intros}\rm:] ~ \\ +@{thm nat_int_tllist.cong_intros[no_vars]} + +\end{description} +\end{indentblock} + +\noindent +The individual rules making up @{text "t.cong_intros"} are available +separately as @{text "t.cong_base"}, @{text "t.cong_refl"}, etc.\ +(Section~\ref{ssec:corec-and-corecursive-theorems}). \ section \Proof Method \label{sec:proof-method}\ -text \ -... -\ - - subsection \\textit{corec_unique} \label{ssec:corec-unique}\ text \ -... +The @{method corec_unique} proof method can be used to prove the uniqueness of +a corecursive specification. See Section~\ref{ssec:uniqueness-reasoning} for +details. \ @@ -688,14 +890,27 @@ \setlength{\itemsep}{0pt} \item -\emph{TODO.} TODO. +\emph{Mutually corecursive codatatypes are not supported.} + +\item +\emph{The signature of friend functions may not depend on type variables beyond +those that appear in the codatatype.} + +\item +\emph{The internal tactics may fail on legal inputs.} - * no mutual types - * limitation on type of friend - * unfinished tactics - * polymorphism of corecUU_transfer - * alternative views - * plugins +\item +\emph{The @{text transfer} option is not implemented yet.} + +\item +\emph{The constructor and destructor views offered by {\upshape\keyw{primcorec}} +are not supported by @{command corec} and @{command corecursive}.} + +\item +\emph{There is no mechanism for registering custom plugins.} + +\item +\emph{The package does not interact well with locales.} \end{enumerate} \ diff -r 7fde2461f9ef -r d4b7d128ec5a src/Doc/Corec/document/root.tex --- a/src/Doc/Corec/document/root.tex Tue Mar 29 23:45:28 2016 +0200 +++ b/src/Doc/Corec/document/root.tex Wed Mar 30 15:16:50 2016 +0200 @@ -77,7 +77,7 @@ This tutorial describes the definitional package for nonprimitively corecursive functions in Isabelle/HOL. The following commands are provided: \keyw{corec}, \keyw{corecursive}, \keyw{friend\_of\_corec}, and \keyw{coinduction\_\allowbreak upto}. -They supplement \keyw{codatatype}, \keyw{primcorec}, and \keyw{primcorecursive}, which +They supplement \keyw{codatatype}, \keyw{primcorec}, and \keyw{primco\-rec\-ur\-sive}, which define codatatypes and primitively corecursive functions. \end{abstract} \end{sloppy} diff -r 7fde2461f9ef -r d4b7d128ec5a src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Mar 29 23:45:28 2016 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Mar 30 15:16:50 2016 +0200 @@ -86,7 +86,7 @@ \footnote{However, some of the internal constructions and most of the internal proof obligations are omitted if the @{text quick_and_dirty} option is enabled.} -The package is described in a number of papers +The package is described in a number of scientific papers @{cite "traytel-et-al-2012" and "blanchette-et-al-2014-impl" and "panny-et-al-2014" and "blanchette-et-al-2015-wit"}. The central notion is that of a \emph{bounded natural functor} (BNF)---a @@ -103,7 +103,7 @@ \item Section \ref{sec:defining-primitively-recursive-functions}, ``Defining Primitively Recursive Functions,'' describes how to specify functions using @{command primrec}. (A separate tutorial @{cite "isabelle-function"} -describes the more general \keyw{fun} and \keyw{function} commands.) +describes the more powerful \keyw{fun} and \keyw{function} commands.) \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,'' describes how to specify codatatypes using the @{command codatatype} command. @@ -111,7 +111,9 @@ \item Section \ref{sec:defining-primitively-corecursive-functions}, ``Defining Primitively Corecursive Functions,'' describes how to specify functions using the @{command primcorec} and -@{command primcorecursive} commands. +@{command primcorecursive} commands. (A separate tutorial +@{cite "isabelle-corec"} describes the more powerful \keyw{corec} and +\keyw{corecursive} commands.) \item Section \ref{sec:registering-bounded-natural-functors}, ``Registering Bounded Natural Functors,'' explains how to use the @{command bnf} command @@ -132,17 +134,17 @@ as the code generator, Transfer, Lifting, and Quickcheck. \item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and -Limitations,'' concludes with known open issues at the time of writing. +Limitations,'' concludes with known open issues. \end{itemize} \newbox\boxA \setbox\boxA=\hbox{\texttt{NOSPAM}} -\newcommand\authoremaili{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak -in.\allowbreak tum.\allowbreak de}} +\newcommand\authoremaili{\texttt{jasmin.blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak +gmail.\allowbreak com}} 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 second author at \authoremaili{} or to the \texttt{cl-isabelle-users} mailing list. \ @@ -161,7 +163,7 @@ text \ Datatypes are illustrated through concrete examples featuring different flavors of recursion. More examples can be found in the directory -@{file "~~/src/HOL/Datatype_Examples"} +@{file "~~/src/HOL/Datatype_Examples"}. \ @@ -687,12 +689,11 @@ \end{itemize} \noindent -The full list of named theorems can be obtained as usual by entering the -command \keyw{print_theorems} immediately after the datatype definition. -This list includes theorems produced by plugins -(Section~\ref{sec:selecting-plugins}), but normally excludes low-level -theorems that reveal internal constructions. To make these accessible, add -the line +The full list of named theorems can be obtained by issuing the command +\keyw{print_theorems} immediately after the datatype definition. This list +includes theorems produced by plugins (Section~\ref{sec:selecting-plugins}), +but normally excludes low-level theorems that reveal internal constructions. +To make these accessible, add the line \ declare [[bnf_internals]] @@ -700,11 +701,6 @@ declare [[bnf_internals = false]] (*>*) -text \ -\noindent -to the top of the theory file. -\ - subsubsection \Free Constructor Theorems \label{sssec:free-constructor-theorems}\ @@ -812,7 +808,7 @@ \item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\ These properties are missing for @{typ "'a list"} because there is only one proper discriminator. If the datatype had been introduced with a second -discriminator called @{const nonnull}, they would have read thusly: \\[\jot] +discriminator called @{const nonnull}, they would have read as follows: \\[\jot] @{prop "null list \ \ nonnull list"} \\ @{prop "nonnull list \ \ null list"} @@ -1143,7 +1139,7 @@ text \ The theory @{file "~~/src/HOL/Library/Countable.thy"} provides a -proof method called @{text countable_datatype} that can be used to prove the +proof method called @{method countable_datatype} that can be used to prove the countability of many datatypes, building on the countability of the types appearing in their definitions and of any type arguments. For example: \ @@ -2037,11 +2033,12 @@ Corecursive functions can be specified using the @{command primcorec} and \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"}. +\keyw{corec} and \keyw{corecursive} commands, and techniques based on domains +and topologies @{cite "lochbihler-hoelzl-2014"}. In this tutorial, the focus is +on @{command primcorec} and @{command primcorecursive}; \keyw{corec} and +\keyw{corecursive} are described in a separate tutorial +@{cite "isabelle-corec"}. More examples can be found in the directories +@{file "~~/src/HOL/Datatype_Examples"} and @{file "~~/src/HOL/Corec_Examples"}. Whereas recursive functions consume datatypes one constructor at a time, corecursive functions construct codatatypes one constructor at a time. diff -r 7fde2461f9ef -r d4b7d128ec5a src/Doc/manual.bib --- a/src/Doc/manual.bib Tue Mar 29 23:45:28 2016 +0200 +++ b/src/Doc/manual.bib Wed Mar 30 15:16:50 2016 +0200 @@ -333,6 +333,12 @@ note = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}} } +@manual{isabelle-corec, + author = {Jasmin Christian Blanchette and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel}, + title = {Defining Nonprimitively Corecursive Functions in {Isabelle\slash HOL}}, + institution = {TU Munich}, + note = {\url{http://isabelle.in.tum.de/doc/corec.pdf}}} + @inproceedings{blanchette-nipkow-2010, title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder", author = "Jasmin Christian Blanchette and Tobias Nipkow", @@ -352,11 +358,11 @@ publisher = {Springer} } -@inproceedings{blanchette-et-al-2015-corec, +@inproceedings{blanchette-et-al-2015-fouco, author = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel}, - title = {Foundational extensible corecursion: a proof assistant perspective}, + title = {Foundational extensible corecursion: A proof assistant perspective}, booktitle = {20th {ACM} {SIGPLAN} International Conference on Functional Programming, {ICFP} 2015}, pages = {192--204}, @@ -366,6 +372,15 @@ publisher = {{ACM}}, } +@misc{blanchette-et-al-2016-fouco2, + author = {Jasmin Christian Blanchette and + Andreas Lochbihler and + Andrei Popescu and + Dmitriy Traytel}, + title = {Productivity for free: Friendly Corecursion for {Isabelle\slash HOL}}, + howpublished = "\url{http://www21.in.tum.de/~blanchet/fouco2.pdf}", + year = 2016} + @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",