# HG changeset patch # User blanchet # Date 1420490885 -3600 # Node ID d418ac9727f2c47db149bab9e5eb7fe16a1a2a5f # Parent 5ca195783da869c5c12f111655a662a1ae6c4a97 docs diff -r 5ca195783da8 -r d418ac9727f2 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Jan 05 21:24:14 2015 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Jan 05 21:48:05 2015 +0100 @@ -342,15 +342,15 @@ *} -subsubsection {* Auxiliary Constants and Properties - \label{sssec:datatype-auxiliary-constants-and-properties} *} +subsubsection {* Auxiliary Constants + \label{sssec:datatype-auxiliary-constants} *} text {* The @{command datatype} command introduces various constants in addition to the constructors. With each datatype are associated set functions, a map function, a relator, discriminators, and selectors, all of which can be given custom names. In the example below, the familiar names @{text null}, @{text hd}, -@{text tl}, @{text set}, @{text map}, and @{text list_all2}, override the +@{text tl}, @{text set}, @{text map}, and @{text list_all2} override the default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2}, @{text set_list}, @{text map_list}, and @{text rel_list}: *} @@ -367,7 +367,8 @@ hide_type list hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list pred_list - context early begin + context early + begin (*>*) datatype (set: 'a) list = null: Nil @@ -624,10 +625,9 @@ \label{ssec:datatype-generated-constants} *} text {* -Given a datatype @{text "('a\<^sub>1, \, 'a\<^sub>m) t"} -with $m > 0$ live type variables and $n$ constructors -@{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the -following auxiliary constants are introduced: +Given a datatype @{text "('a\<^sub>1, \, 'a\<^sub>m) t"} with $m > 0$ live type variables +and $n$ constructors @{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the following +auxiliary constants are introduced: \medskip @@ -756,8 +756,8 @@ \item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.case(1)[no_vars]} \\ @{thm list.case(2)[no_vars]} \\ -(The @{text "[code]"} attribute is set by the @{text code} plugin, -Section~\ref{ssec:code-generator}.) +The @{text "[code]"} attribute is set by the @{text code} plugin +(Section~\ref{ssec:code-generator}). \item[@{text "t."}\hthm{case_cong} @{text "[fundef_cong]"}\rm:] ~ \\ @{thm list.case_cong[no_vars]} @@ -796,19 +796,19 @@ \item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.sel(1)[no_vars]} \\ @{thm list.sel(2)[no_vars]} \\ -(The @{text "[code]"} attribute is set by the @{text code} plugin, -Section~\ref{ssec:code-generator}.) +The @{text "[code]"} attribute is set by the @{text code} plugin +(Section~\ref{ssec:code-generator}). \item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\ @{thm list.collapse(1)[no_vars]} \\ @{thm list.collapse(2)[no_vars]} \\ -(The @{text "[simp]"} attribute is exceptionally omitted for datatypes equipped +The @{text "[simp]"} attribute is exceptionally omitted for datatypes equipped with a single nullary constructor, because a property of the form -@{prop "x = C"} is not suitable as a simplification rule.) +@{prop "x = C"} is not suitable as a simplification rule. \item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\ These properties are missing for @{typ "'a list"} because there is only one -proper discriminator. Had the datatype been introduced with a second +proper discriminator. If the datatype had been introduced with a second discriminator called @{const nonnull}, they would have read thusly: \\[\jot] @{prop "null list \ \ nonnull list"} \\ @{prop "nonnull list \ \ null list"} @@ -842,8 +842,8 @@ \noindent In addition, equational versions of @{text t.disc} are registered with the -@{text "[code]"} attribute. (The @{text "[code]"} attribute is set by the -@{text code} plugin, Section~\ref{ssec:code-generator}.) +@{text "[code]"} attribute. The @{text "[code]"} attribute is set by the +@{text code} plugin (Section~\ref{ssec:code-generator}). *} @@ -860,32 +860,32 @@ \item[@{text "t."}\hthm{case_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm list.case_transfer[no_vars]} \\ -(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin, -Section~\ref{ssec:transfer}.) +The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin +(Section~\ref{ssec:transfer}). \item[@{text "t."}\hthm{sel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ This property is missing for @{typ "'a list"} because there is no common selector to all constructors. \\ -(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin, -Section~\ref{ssec:transfer}.) +The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin +(Section~\ref{ssec:transfer}). \item[@{text "t."}\hthm{ctr_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm list.ctr_transfer(1)[no_vars]} \\ @{thm list.ctr_transfer(2)[no_vars]} \\ -(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin, -Section~\ref{ssec:transfer}.) +The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin +(Section~\ref{ssec:transfer}). \item[@{text "t."}\hthm{disc_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm list.disc_transfer(1)[no_vars]} \\ @{thm list.disc_transfer(2)[no_vars]} \\ -(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin, -Section~\ref{ssec:transfer}.) +The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin +(Section~\ref{ssec:transfer}). \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.set(1)[no_vars]} \\ @{thm list.set(2)[no_vars]} \\ -(The @{text "[code]"} attribute is set by the @{text code} plugin, -Section~\ref{ssec:code-generator}.) +The @{text "[code]"} attribute is set by the @{text code} plugin +(Section~\ref{ssec:code-generator}). \item[@{text "t."}\hthm{set_cases} @{text "[consumes 1, cases set: set\<^sub>i_t]"}\rm:] ~ \\ @{thm list.set_cases[no_vars]} @@ -900,8 +900,8 @@ \item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.map(1)[no_vars]} \\ @{thm list.map(2)[no_vars]} \\ -(The @{text "[code]"} attribute is set by the @{text code} plugin, -Section~\ref{ssec:code-generator}.) +The @{text "[code]"} attribute is set by the @{text code} plugin +(Section~\ref{ssec:code-generator}). \item[@{text "t."}\hthm{map_disc_iff} @{text "[simp]"}\rm:] ~ \\ @{thm list.map_disc_iff[no_vars]} @@ -932,9 +932,9 @@ \noindent In addition, equational versions of @{text t.rel_inject} and @{text -rel_distinct} are registered with the @{text "[code]"} attribute. (The -@{text "[code]"} attribute is set by the @{text code} plugin, -Section~\ref{ssec:code-generator}.) +rel_distinct} are registered with the @{text "[code]"} attribute. The +@{text "[code]"} attribute is set by the @{text code} plugin +(Section~\ref{ssec:code-generator}). The second subgroup consists of more abstract properties of the set functions, the map function, and the relator: @@ -953,8 +953,8 @@ \item[@{text "t."}\hthm{set_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm list.set_transfer[no_vars]} \\ -(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin, -Section~\ref{ssec:transfer}.) +The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin +(Section~\ref{ssec:transfer}). \item[@{text "t."}\hthm{map_cong0}\rm:] ~ \\ @{thm list.map_cong0[no_vars]} @@ -976,13 +976,13 @@ \item[@{text "t."}\hthm{map_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm list.map_transfer[no_vars]} \\ -(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin, -Section~\ref{ssec:transfer}.) +The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin +(Section~\ref{ssec:transfer}). \item[@{text "t."}\hthm{rel_compp} @{text "[relator_distr]"}\rm:] ~ \\ @{thm list.rel_compp[no_vars]} \\ -(The @{text "[relator_distr]"} attribute is set by the @{text lifting} plugin, -Section~\ref{ssec:lifting}.) +The @{text "[relator_distr]"} attribute is set by the @{text lifting} plugin +(Section~\ref{ssec:lifting}). \item[@{text "t."}\hthm{rel_conversep}\rm:] ~ \\ @{thm list.rel_conversep[no_vars]} @@ -999,13 +999,13 @@ \item[@{text "t."}\hthm{rel_mono} @{text "[mono, relator_mono]"}\rm:] ~ \\ @{thm list.rel_mono[no_vars]} \\ -(The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin, -Section~\ref{ssec:lifting}.) +The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin +(Section~\ref{ssec:lifting}). \item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm list.rel_transfer[no_vars]} \\ -(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin, -Section~\ref{ssec:transfer}.) +The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin +(Section~\ref{ssec:transfer}). \end{description} \end{indentblock} @@ -1037,16 +1037,16 @@ \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.rec(1)[no_vars]} \\ @{thm list.rec(2)[no_vars]} \\ -(The @{text "[code]"} attribute is set by the @{text code} plugin, -Section~\ref{ssec:code-generator}.) +The @{text "[code]"} attribute is set by the @{text code} plugin +(Section~\ref{ssec:code-generator}). \item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\ @{thm list.rec_o_map[no_vars]} \item[@{text "t."}\hthm{rec_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm list.rec_transfer[no_vars]} \\ -(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin, -Section~\ref{ssec:transfer}.) +The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin +(Section~\ref{ssec:transfer}). \end{description} \end{indentblock} @@ -1057,7 +1057,7 @@ \begin{indentblock} \begin{description} -\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.map} @{text t.rel_inject}] ~ \\ +\item[@{text "t."}\hthm{simps}] = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.map} @{text t.rel_inject} \\ @{text t.rel_distinct} @{text t.set} \end{description} @@ -1228,7 +1228,7 @@ text {* \blankline *} - primrec (*<*)(in early) (*>*)tfold :: "('a \ 'b \ 'b) \ ('a, 'b) tlist \ 'b" where + primrec (*<*)(in early) (transfer) (*>*)tfold :: "('a \ 'b \ 'b) \ ('a, 'b) tlist \ 'b" where "tfold _ (TNil y) = y" | "tfold f (TCons x xs) = f x (tfold f xs)" @@ -1398,7 +1398,8 @@ \label{sssec:primrec-nested-as-mutual-recursion} *} (*<*) - locale n2m begin + locale n2m + begin (*>*) text {* @@ -1532,21 +1533,50 @@ *} -(* subsection {* Generated Theorems \label{ssec:primrec-generated-theorems} *} +(*<*) + context early + begin +(*>*) + text {* -% * synthesized nonrecursive definition -% * user specification is rederived from it, exactly as entered -% -% * induct -% * mutualized -% * without some needless induction hypotheses if not used -% * rec -% * mutualized +The @{command primrec} command generates the following properties (listed +for @{const tfold}): + +\begin{indentblock} +\begin{description} + +\item[@{text "f."}\hthm{simps} @{text "[simp, code]"}\rm:] ~ \\ +@{thm tfold.simps(1)[no_vars]} \\ +@{thm tfold.simps(2)[no_vars]} \\ +The @{text "[code]"} attribute is set by the @{text code} plugin +(Section~\ref{ssec:code-generator}). + +\item[@{text "f."}\hthm{transfer} @{text "[transfer_rule]"}\rm:] ~ \\ +@{thm tfold.transfer[no_vars]} \\ +This theorem is generated by the @{text transfer} plugin +(Section~\ref{ssec:transfer}) for functions declared with the @{text transfer} +option enabled. + +\item[@{text "f."}\hthm{induct} @{text "[case_names C\<^sub>1 \ C\<^sub>n]"}\rm:] ~ \\ +This induction rule is generated for nested-as-mutual recursive functions +(Section~\ref{sssec:primrec-nested-as-mutual-recursion}). + +\item[@{text "f\<^sub>1_\_f\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \ C\<^sub>n]"}\rm:] ~ \\ +This induction rule is generated for nested-as-mutual recursive functions +(Section~\ref{sssec:primrec-nested-as-mutual-recursion}). Given $m > 1$ mutually +recursive functions, this rule can be used to prove $m$ properties +simultaneously. + +\end{description} +\end{indentblock} *} -*) + +(*<*) + end +(*>*) subsection {* Recursive Default Values for Selectors @@ -1870,8 +1900,8 @@ \item[@{text "t."}\hthm{corec_code} @{text "[code]"}\rm:] ~ \\ @{thm llist.corec_code[no_vars]} \\ -(The @{text "[code]"} attribute is set by the @{text code} plugin, -Section~\ref{ssec:code-generator}.) +The @{text "[code]"} attribute is set by the @{text code} plugin +(Section~\ref{ssec:code-generator}). \item[@{text "t."}\hthm{corec_disc}\rm:] ~ \\ @{thm llist.corec_disc(1)[no_vars]} \\ @@ -1890,8 +1920,8 @@ \item[@{text "t."}\hthm{corec_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm llist.corec_transfer[no_vars]} \\ -(The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin, -Section~\ref{ssec:transfer}.) +The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin +(Section~\ref{ssec:transfer}). \end{description} \end{indentblock} @@ -1902,7 +1932,7 @@ \begin{indentblock} \begin{description} -\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec_disc_iff}] @{text t.corec_sel} ~ \\ +\item[@{text "t."}\hthm{simps}] = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec_disc_iff} @{text t.corec_sel} \\ @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set} \end{description} @@ -1978,7 +2008,7 @@ the right of the equal sign or in a conditional expression: *} - primcorec literate :: "('a \ 'a) \ 'a \ 'a llist" where + primcorec (*<*)(transfer) (*>*)literate :: "('a \ 'a) \ 'a \ 'a llist" where "literate g x = LCons x (literate g (g x))" text {* \blankline *} @@ -2296,7 +2326,7 @@ without having first to discharge @{term "n mod (4\int) \ 0"}, @{term "n mod (4\int) \ 1"}, and @{term "n mod (4\int) \ 2"}. -The price to pay for this elegance is that we must discharge exclusivity proof +The price to pay for this elegance is that we must discharge exclusiveness proof obligations, one for each pair of conditions @{term "(n mod (4\int) = i, n mod (4\int) = j)"} with @{term "i < j"}. If we prefer not to discharge any obligations, we can @@ -2473,6 +2503,7 @@ \item The @{text exhaustive} option indicates that the conditions in specifications expressed using the constructor or destructor view cover all possible cases. +This generally gives rise to an additional proof obligation. \item The @{text transfer} option indicates that an unconditional transfer rule @@ -2489,10 +2520,101 @@ *} -(* subsection {* Generated Theorems \label{ssec:primcorec-generated-theorems} *} -*) + +text {* +The @{command primcorec} and @{command primcorecursive} commands generate the +following properties (listed for @{const literate}): + +\begin{indentblock} +\begin{description} + +\item[@{text "f."}\hthm{code} @{text "[code]"}\rm:] ~ \\ +@{thm literate.code[no_vars]} \\ +The @{text "[code]"} attribute is set by the @{text code} plugin +(Section~\ref{ssec:code-generator}). + +\item[@{text "f."}\hthm{ctr}\rm:] ~ \\ +@{thm literate.ctr[no_vars]} + +\item[@{text "f."}\hthm{disc} @{text "[simp, code]"}\rm:] ~ \\ +@{thm literate.disc[no_vars]} \\ +The @{text "[code]"} attribute is set by the @{text code} plugin +(Section~\ref{ssec:code-generator}). The @{text "[simp]"} attribute is set only +for functions for which @{text f.disc_iff} is not available. + +\item[@{text "f."}\hthm{disc_iff} @{text "[simp]"}\rm:] ~ \\ +@{thm literate.disc_iff[no_vars]} \\ +This property is generated only for functions declared with the +@{text exhaustive} option or whose conditions are trivially exhaustive. + +\item[@{text "f."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\ +@{thm literate.disc[no_vars]} \\ +The @{text "[code]"} attribute is set by the @{text code} plugin +(Section~\ref{ssec:code-generator}). + +\item[@{text "f."}\hthm{exclude}\rm:] ~ \\ +These properties are missing for @{const literate} because no exclusiveness +proof obligations arose. In general, the properties correspond to the +discharged proof obligations. + +\item[@{text "f."}\hthm{exhaust}\rm:] ~ \\ +This property is missing for @{const literate} because no exhaustiveness +proof obligation arose. In general, the property correspond to the discharged +proof obligation. + +\item[\begin{tabular}{@ {}l@ {}} + @{text "f."}\hthm{coinduct} @{text "[consumes m, case_names t\<^sub>1 \ t\<^sub>m,"} \\ + \phantom{@{text "f."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \ + D\<^sub>n]"}\rm: +\end{tabular}] ~ \\ +This coinduction rule is generated for nested-as-mutual corecursive functions +(Section~\ref{sssec:primcorec-nested-as-mutual-corecursion}). + +\item[\begin{tabular}{@ {}l@ {}} + @{text "f."}\hthm{coinduct_strong} @{text "[consumes m, case_names t\<^sub>1 \ t\<^sub>m,"} \\ + \phantom{@{text "f."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \ + D\<^sub>n]"}\rm: +\end{tabular}] ~ \\ +This coinduction rule is generated for nested-as-mutual corecursive functions +(Section~\ref{sssec:primcorec-nested-as-mutual-corecursion}). + +\item[\begin{tabular}{@ {}l@ {}} + @{text "f\<^sub>1_\_f\<^sub>m."}\hthm{coinduct} @{text "[case_names t\<^sub>1 \ t\<^sub>m,"} \\ + \phantom{@{text "f."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \ + D\<^sub>n]"}\rm: +\end{tabular}] ~ \\ +This coinduction rule is generated for nested-as-mutual corecursive functions +(Section~\ref{sssec:primcorec-nested-as-mutual-corecursion}). Given $m > 1$ +mutually corecursive functions, this rule can be used to prove $m$ properties +simultaneously. + +\item[\begin{tabular}{@ {}l@ {}} + @{text "f\<^sub>1_\_f\<^sub>m."}\hthm{coinduct_strong} @{text "[case_names t\<^sub>1 \ t\<^sub>m,"} \\ + \phantom{@{text "f."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \ + D\<^sub>n]"}\rm: +\end{tabular}] ~ \\ +This coinduction rule is generated for nested-as-mutual corecursive functions +(Section~\ref{sssec:primcorec-nested-as-mutual-corecursion}). Given $m > 1$ +mutually corecursive functions, this rule can be used to prove $m$ properties +simultaneously. + +\end{description} +\end{indentblock} + +\noindent +For convenience, @{command primcorec} and @{command primcorecursive} also +provide the following collection: + +\begin{indentblock} +\begin{description} + +\item[@{text "f."}\hthm{simps}] = @{text f.disc_iff} (or @{text f.disc}) @{text t.sel} + +\end{description} +\end{indentblock} +*} (* @@ -2652,10 +2774,9 @@ reasoning abstractly about an arbitrary BNF. The @{command bnf_axiomatization} command below introduces a type @{text "('a, 'b, 'c) F"}, three set constants, a map function, a relator, and a nonemptiness witness that depends only on -@{typ 'a}. (The type @{text "'a \ ('a, 'b, 'c) F"} of -the witness can be read as an implication: If we have a witness for @{typ 'a}, -we can construct a witness for @{text "('a, 'b, 'c) F"}.) The BNF -properties are postulated as axioms. +@{typ 'a}. The type @{text "'a \ ('a, 'b, 'c) F"} of the witness can be read +as an implication: Given a witness for @{typ 'a}, we can construct a witness for +@{text "('a, 'b, 'c) F"}. The BNF properties are postulated as axioms. *} bnf_axiomatization (setA: 'a, setB: 'b, setC: 'c) F