# HG changeset patch # User blanchet # Date 1392307885 -3600 # Node ID 3f4efd7d950dc0b3c04dc55f4687e982143759b7 # Parent 1cd927ca8296fc87c64313ce645a80bbd80094b1 added a bit of documentation for the different commands diff -r 1cd927ca8296 -r 3f4efd7d950d src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Thu Feb 13 17:11:11 2014 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Feb 13 17:11:25 2014 +0100 @@ -476,10 +476,13 @@ \medskip \noindent +The @{command datatype_new} command introduces a set of mutually recursive +datatypes specified by their constructors. + The syntactic entity \synt{target} can be used to specify a local context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference manual \cite{isabelle-isar-ref}. -% + The optional target is potentially followed by datatype-specific options: \begin{itemize} @@ -1367,6 +1370,21 @@ ; @{syntax_def pr_equation}: thmdecl? prop \} + +\medskip + +\noindent +The @{command primrec_new} command introduces a set of mutually recursive +functions over a datatype. + +The syntactic entity \synt{target} can be used to specify a local context, +\synt{fixes} is a list of names with optional type signatures, \synt{thmdecl} +is an optional name for the formula that follows, and \synt{prop} is a HOL +proposition. They are is documented in the Isar reference manual +\cite{isabelle-isar-ref}. + +%%% TODO: elaborate on format of the equations +%%% TODO: elaborate on mutual and nested-to-mutual *} @@ -2251,8 +2269,7 @@ @{rail \ (@@{command primcorec} | @@{command primcorecursive}) target? \ - @{syntax pcr_option}? fixes @'where' - (@{syntax pcr_formula} + '|') + @{syntax pcr_option}? fixes @'where' (@{syntax pcr_formula} + '|') ; @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')' ; @@ -2262,6 +2279,15 @@ \medskip \noindent +The @{command primcorec} command introduces a set of mutually corecursive +functions over a codatatype. + +The syntactic entity \synt{target} can be used to specify a local context, +\synt{fixes} is a list of names with optional type signatures, \synt{thmdecl} +is an optional name for the formula that follows, and \synt{prop} is a HOL +proposition. They are is documented in the Isar reference manual +\cite{isabelle-isar-ref}. + The optional target is potentially followed by a corecursion-specific option: \begin{itemize} @@ -2280,6 +2306,9 @@ \noindent The @{command primcorec} command is an abbreviation for @{command primcorecursive} with @{text "by auto?"} to discharge any emerging proof obligations. + +%%% TODO: elaborate on format of the propositions +%%% TODO: elaborate on mutual and nested-to-mutual *} @@ -2479,6 +2508,18 @@ 'map:' term ('sets:' (term +))? 'bd:' term \ ('wits:' (term +))? ('rel:' term)? \} + +\medskip + +\noindent +The @{command bnf} command registers an existing type as a bounded natural +functor (BNF). The type must be equipped with an appropriate map function +(functorial action). In addition, custom set functions, relators, and +nonemptiness witnesses can be specified; otherwise, default versions are used. + +The syntactic entity \synt{target} can be used to specify a local +context---e.g., @{text "(in linorder)"}. It is documented in the Isar +reference manual \cite{isabelle-isar-ref}. *} @@ -2508,12 +2549,17 @@ \noindent The @{command bnf_decl} command declares a new type and associated constants (map, set, relator, and cardinal bound) and asserts the BNF properties for -these constants as axioms. Type arguments are live by default; they can be -marked as dead by entering ``-'' (hyphen) instead of an identifier for the -corresponding set function. Witnesses can be specified by their types. -Otherwise, the syntax of @{command bnf_decl} is -identical to the left-hand side of a @{command datatype_new} or @{command -codatatype} definition. +these constants as axioms. + +The syntactic entity \synt{target} can be used to specify a local +context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference +manual \cite{isabelle-isar-ref}. + +Type arguments are live by default; they can be marked as dead by entering +``-'' (hyphen) instead of an identifier for the corresponding set function. +Witnesses can be specified by their types. Otherwise, the syntax of +@{command bnf_decl} is identical to the left-hand side of a +@{command datatype_new} or @{command codatatype} definition. The command is useful to reason abstractly about BNFs. The axioms are safe because there exists BNFs of arbitrary large arities. Applications must import @@ -2589,9 +2635,18 @@ \medskip +\noindent +The @{command free_constructors} command generates destructor constants for +freely constructed types as well as properties about constructors and +destructors. It also registers the constants and theorems in a data structure +that is queried by various tools (e.g., \keyw{function}). + +The syntactic entity \synt{target} can be used to specify a local +context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference +manual \cite{isabelle-isar-ref}. + % options: no_discs_sels no_code -\noindent Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems. For technical reasons, the @{text "[fundef_cong]"} attribute is not set on the generated @{text case_cong} theorem. It can be added manually using