diff -r 35890e80f480 -r cf34abe28209 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Feb 06 18:31:43 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Feb 06 23:42:36 2014 +0100
@@ -11,6 +11,7 @@
 imports
   Setup
   "~~/src/HOL/Library/BNF_Decl"
+  "~~/src/HOL/Library/Cardinal_Notations"
   "~~/src/HOL/Library/FSet"
   "~~/src/HOL/Library/Simps_Case_Conv"
 begin
@@ -298,9 +299,9 @@
 datatypes defined in terms of~@{text "\<Rightarrow>"}:
 *}
 
-    datatype_new ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
+    datatype_new ('a, 'b) fun_copy = Fun "'a \<Rightarrow> 'b"
     datatype_new 'a also_wrong = W1 | W2 (*<*)'a
-    typ (*>*)"('a also_wrong, 'a) fn"
+    typ (*>*)"('a also_wrong, 'a) fun_copy"
 
 text {*
 \noindent
@@ -322,7 +323,8 @@
 allow recursion on a subset of their type arguments @{text 'a\<^sub>1}, \ldots,
 @{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
 type arguments are called \emph{dead}. In @{typ "'a \<Rightarrow> 'b"} and
-@{typ "('a, 'b) fn"}, the type variable @{typ 'a} is dead and @{typ 'b} is live.
+@{typ "('a, 'b) fun_copy"}, the type variable @{typ 'a} is dead and
+@{typ 'b} is live.
 
 Type constructors must be registered as BNFs to have live arguments. This is
 done automatically for datatypes and codatatypes introduced by the @{command
@@ -1559,8 +1561,7 @@
 
 text {* \blankline *}
 
-    codatatype 'a state_machine =
-      State_Machine (accept: bool) (trans: "'a \<Rightarrow> 'a state_machine")
+    codatatype 'a sm = SM (accept: bool) (trans: "'a \<Rightarrow> 'a sm")
 
 
 subsection {* Command Syntax
@@ -1927,7 +1928,8 @@
 *}
 
     primcorec (*<*)(in late) (*>*)tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
-      "tree\<^sub>i\<^sub>i_of_stream s = Node\<^sub>i\<^sub>i (shd s) (LCons (tree\<^sub>i\<^sub>i_of_stream (stl s)) LNil)"
+      "tree\<^sub>i\<^sub>i_of_stream s =
+         Node\<^sub>i\<^sub>i (shd s) (LCons (tree\<^sub>i\<^sub>i_of_stream (stl s)) LNil)"
 
 text {*
 The next example illustrates corecursion through functions, which is a bit
@@ -1935,13 +1937,11 @@
 5-tuples @{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,
 @{text \<Sigma>} is a finite alphabet, @{text \<delta>} is a transition function, @{text q\<^sub>0}
 is an initial state, and @{text F} is a set of final states. The following
-function translates a DFA into a @{type state_machine}:
+function translates a DFA into a state machine:
 *}
 
-    primcorec
-      (*<*)(in early) (*>*)sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
-    where
-      "sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (sm_of_dfa \<delta> F \<circ> \<delta> q)"
+    primcorec (*<*)(in early) (*>*)sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a sm" where
+      "sm_of_dfa \<delta> F q = SM (q \<in> F) (sm_of_dfa \<delta> F \<circ> \<delta> q)"
 
 text {*
 \noindent
@@ -1951,28 +1951,24 @@
 than through composition. For example:
 *}
 
-    primcorec
-      sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
-    where
-      "sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (\<lambda>a. sm_of_dfa \<delta> F (\<delta> q a))"
+    primcorec sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a sm" where
+      "sm_of_dfa \<delta> F q = SM (q \<in> F) (\<lambda>a. sm_of_dfa \<delta> F (\<delta> q a))"
 
 text {* \blankline *}
 
-    primcorec empty_sm :: "'a state_machine" where
-      "empty_sm = State_Machine False (\<lambda>_. empty_sm)"
+    primcorec empty_sm :: "'a sm" where
+      "empty_sm = SM False (\<lambda>_. empty_sm)"
 
 text {* \blankline *}
 
-    primcorec not_sm :: "'a state_machine \<Rightarrow> 'a state_machine" where
-      "not_sm M = State_Machine (\<not> accept M) (\<lambda>a. not_sm (trans M a))"
+    primcorec not_sm :: "'a sm \<Rightarrow> 'a sm" where
+      "not_sm M = SM (\<not> accept M) (\<lambda>a. not_sm (trans M a))"
 
 text {* \blankline *}
 
-    primcorec
-      or_sm :: "'a state_machine \<Rightarrow> 'a state_machine \<Rightarrow> 'a state_machine"
-    where
-      "or_sm M N = State_Machine (accept M \<or> accept N)
-         (\<lambda>a. or_sm (trans M a) (trans N a))"
+    primcorec or_sm :: "'a sm \<Rightarrow> 'a sm \<Rightarrow> 'a sm" where
+      "or_sm M N =
+         SM (accept M \<or> accept N) (\<lambda>a. or_sm (trans M a) (trans N a))"
 
 text {*
 \noindent
@@ -1981,22 +1977,22 @@
 $n = 2$:
 *}
 
-    codatatype ('a, 'b) state_machine2 =
-      State_Machine2 (accept2: bool) (trans2: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) state_machine2")
+    codatatype ('a, 'b) sm2 =
+      SM2 (accept2: bool) (trans2: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) sm2")
 
 text {* \blankline *}
 
     primcorec
-      (*<*)(in early) (*>*)sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) state_machine2"
+      (*<*)(in early) (*>*)sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) sm2"
     where
-      "sm2_of_dfa \<delta> F q = State_Machine2 (q \<in> F) (op \<circ> (op \<circ> (sm2_of_dfa \<delta> F)) (\<delta> q))"
+      "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) (op \<circ> (op \<circ> (sm2_of_dfa \<delta> F)) (\<delta> q))"
 
 text {* \blankline *}
 
     primcorec
-      sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) state_machine2"
+      sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) sm2"
     where
-      "sm2_of_dfa \<delta> F q = State_Machine2 (q \<in> F) (\<lambda>a b. sm2_of_dfa \<delta> F (\<delta> q a b))"
+      "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) (\<lambda>a b. sm2_of_dfa \<delta> F (\<delta> q a b))"
 
 
 subsubsection {* Nested-as-Mutual Corecursion
@@ -2175,12 +2171,10 @@
 
     primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
       "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
+      "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
+      "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)" |
 (*>*)
       "_ \<Longrightarrow> \<not> lnull (lappend xs ys)"
-(*<*) |
-      "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
-      "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
-(*>*)
 
 text {*
 \noindent
@@ -2294,25 +2288,168 @@
 
 text {*
 The (co)datatype package can be set up to allow nested recursion through
-arbitrary type constructors, as long as they adhere to the BNF requirements and
-are registered as BNFs.
+arbitrary type constructors, as long as they adhere to the BNF requirements
+and are registered as BNFs. It is also possible to declare a BNF abstractly
+without specifying its internal structure.
 *}
 
 
-(*
-subsection {* Introductory Example
-  \label{ssec:bnf-introductory-example} *}
+subsection {* Bounded Natural Functors
+  \label{ssec:bounded-natural-functors} *}
+
+text {*
+Bounded natural functors (BNFs) are a semantic criterion for where
+(co)re\-cur\-sion may appear on the right-hand side of an equation
+\cite{traytel-et-al-2012,blanchette-et-al-wit}.
+
+An $n$-ary BNF is a type constructor equipped with a map function
+(functorial action), $n$ set functions (natural transformations),
+and an infinite cardinal bound that satisfy certain properties.
+For example, @{typ "'a llist"} is a unary BNF.
+Its relator @{text "llist_all2 \<Colon>
+  ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow>
+  'a llist \<Rightarrow> 'b llist \<Rightarrow> bool"}
+extends binary predicates over elements to binary predicates over parallel
+lazy lists. The cardinal bound limits the number of elements returned by the
+set function; it may not depend on the cardinality of @{typ 'a}.
+
+The type constructors introduced by @{command datatype_new} and
+@{command codatatype} are automatically registered as BNFs. In addition, a
+number of old-style datatypes and non-free types are preregistered.
+
+Given an $n$-ary BNF, the $n$ type variables associated with set functions,
+and on which the map function acts, are \emph{live}; any other variables are
+\emph{dead}. Nested (co)recursion can only take place through live variables.
+*}
+
+
+subsection {* Introductory Examples
+  \label{ssec:bnf-introductory-examples} *}
 
 text {*
-More examples in \verb|~~/src/HOL/Basic_BNFs.thy|,
-\verb|~~/src/HOL/Library/FSet.thy|, and
-\verb|~~/src/HOL/Library/Multiset.thy|.
-
-%Mention distinction between live and dead type arguments;
-%  * and existence of map, set for those
-%mention =>.
+The example below shows how to register a type as a BNF using the @{command bnf}
+command. Some of the proof obligations are best viewed with the theory
+@{theory Cardinal_Notations}, located in \verb|~~/src/HOL/Library|,
+imported.
+
+The type is simply a copy of the function space @{typ "'d \<Rightarrow> 'a"}, where @{typ 'a}
+is live and @{typ 'd} is dead. We introduce it together with its map function,
+set function, and relator.
 *}
-*)
+
+    typedef ('d, 'a) fn = "UNIV \<Colon> ('d \<Rightarrow> 'a) set"
+    by simp
+
+text {* \blankline *}
+
+    lemmas Abs_Rep_thms[simp] =
+      Abs_fn_inverse[OF UNIV_I] Rep_fn_inverse
+
+text {* \blankline *}
+
+    definition map_fn :: "('a \<Rightarrow> 'b) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn" where
+      "map_fn f F = Abs_fn (\<lambda>x. f (Rep_fn F x))"
+
+text {* \blankline *}
+
+    definition set_fn :: "('d, 'a) fn \<Rightarrow> 'a set" where
+      "set_fn F = range (Rep_fn F)"
+
+text {* \blankline *}
+
+    definition
+      rel_fn :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn \<Rightarrow> bool"
+    where
+      "rel_fn R F G = fun_rel (op =) R (Rep_fn F) (Rep_fn G)"
+
+text {* \blankline *}
+
+    axiomatization where cheat: "P"
+
+text {* \blankline *}
+
+    bnf "('d, 'a) fn"
+      map: map_fn
+      sets: set_fn
+      bd: "natLeq +c |UNIV :: 'd set|"
+      rel: rel_fn
+    proof -
+      show "map_fn id = id"
+        by (auto simp add: map_fn_def[abs_def] id_comp)
+    next
+      fix F G show "map_fn (G \<circ> F) = map_fn G \<circ> map_fn F"
+        by (simp add: map_fn_def[abs_def] comp_def[abs_def])
+    next
+      fix F f g
+      assume "\<And>x. x \<in> set_fn F \<Longrightarrow> f x = g x"
+      thus "map_fn f F = map_fn g F"
+        by (auto simp add: map_fn_def set_fn_def)
+    next
+      fix f show "set_fn \<circ> map_fn f = op ` f \<circ> set_fn"
+        by (auto simp add: set_fn_def map_fn_def comp_def)
+    next
+      show "card_order (natLeq +c |UNIV \<Colon> 'd set| )"
+        apply (rule card_order_csum)
+        apply (rule natLeq_card_order)
+        by (rule card_of_card_order_on)
+    next
+      show "cinfinite (natLeq +c |UNIV \<Colon> 'd set| )"
+        apply (rule cinfinite_csum)
+        apply (rule disjI1)
+        by (rule natLeq_cinfinite)
+    next
+      fix F :: "('d, 'a) fn"
+      have "|set_fn F| \<le>o |UNIV \<Colon> 'd set|" (is "_ \<le>o ?U")
+        unfolding set_fn_def by (rule card_of_image)
+      also have "?U \<le>o natLeq +c ?U"
+        by (rule ordLeq_csum2) (rule card_of_Card_order)
+      finally show "|set_fn F| \<le>o natLeq +c |UNIV \<Colon> 'd set|" .
+    next
+      fix R S
+      show "rel_fn R OO rel_fn S \<le> rel_fn (R OO S)"
+        by (auto simp add: rel_fn_def[abs_def] fun_rel_def)
+    next
+      fix R
+      show "rel_fn R =
+            (BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
+             BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
+        unfolding set_fn_def rel_fn_def[abs_def] fun_rel_def Grp_def
+          fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
+        by (rule cheat)
+    qed
+
+text {* \blankline *}
+
+    print_theorems
+    print_bnfs
+
+text {*
+\noindent
+Using \keyw{print\_theorems} and @{keyword print_bnfs}, we can contemplate and
+show the world what we have achieved.
+
+This particular example does not need any nonemptiness witness, because the
+one generated by default is good enough, but in general this would be
+necessary. See \verb|~~/src/HOL/Basic_BNFs.thy|,
+\verb|~~/src/HOL/Library/FSet.thy|, and \verb|~~/src/HOL/Library/Multiset.thy|
+for further examples of BNF registration, some of which feature custom
+witnesses.
+
+The next example declares a BNF axiomatically. The @{command bnf_decl} command
+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.
+*}
+
+    bnf_decl (setA: 'a, setB: 'b, setC: 'c) F [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
+
+text {* \blankline *}
+
+    print_theorems
+    print_bnfs
 
 
 subsection {* Command Syntax
@@ -2339,28 +2476,37 @@
   \label{sssec:bnf-decl} *}
 
 text {*
-%%% TODO: use command_def once the command is available
 \begin{matharray}{rcl}
-  @{text "bnf_decl"} & : & @{text "local_theory \<rightarrow> local_theory"}
+  @{command_def "bnf_decl"} & : & @{text "local_theory \<rightarrow> local_theory"}
 \end{matharray}
 
 @{rail \<open>
   @@{command bnf_decl} target? @{syntax dt_name}
   ;
-  @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
+  @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? \<newline>
+    @{syntax wit_types}? mixfix?
   ;
   @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')'
   ;
   @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
+  ;
+  @{syntax_def wit_types}: '[' 'wits' ':' types ']'
 \<close>}
 
-Declares a fresh type and fresh constants (map, set, relator, cardinal bound)
-and asserts the bnf properties for these constants as axioms. Additionally,
-type arguments may be marked as dead (by using @{syntax "-"} instead of a name for the
-set function)---this is the only difference of @{syntax dt_name} compared to
-the syntax used by the @{command datatype_new}/@{command codatatype} commands.
-
-The axioms are sound, since one there exists a bnf of any given arity.
+\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 \texttt{-} (hyphen) instead of a name 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
+the theory @{theory BNF_Decl}, located in the directory
+\verb|~~/src/HOL/Library|, to use this functionality.
 *}