# 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, \<dots>, '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, \<dots>, '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 \<Longrightarrow> \<not> nonnull list"} \\
 @{prop "nonnull list \<Longrightarrow> \<not> 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 \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
+    primrec (*<*)(in early) (transfer) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> '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 \<dots> 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_\<dots>_f\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> 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 \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
+    primcorec (*<*)(transfer) (*>*)literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> '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\<Colon>int) \<noteq> 0"},
 @{term "n mod (4\<Colon>int) \<noteq> 1"}, and
 @{term "n mod (4\<Colon>int) \<noteq> 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\<Colon>int) = i, n mod (4\<Colon>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 \<dots> t\<^sub>m,"} \\
+  \phantom{@{text "f."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
+  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 \<dots> t\<^sub>m,"} \\
+  \phantom{@{text "f."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
+  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_\<dots>_f\<^sub>m."}\hthm{coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
+  \phantom{@{text "f."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
+  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_\<dots>_f\<^sub>m."}\hthm{coinduct_strong} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
+  \phantom{@{text "f."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
+  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 \<Rightarrow> ('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 \<Rightarrow> ('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