more explicit syntax for defining a bnf

--- a/src/Doc/Datatypes/Datatypes.thy	Wed Nov 13 09:37:00 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Nov 13 10:53:36 2013 +0100
@@ -2280,10 +2280,9 @@
 \end{matharray}
 
 @{rail "
-  @@{command bnf} target? (name ':')? term \\
-    term_list term term_list? term?
-  ;
-  X_list: '[' (X + ',') ']'
+  @@{command bnf} target? (name ':')? typ \\
+    'map:' term ('sets:' (term +))? 'bd:' term \\
+    ('wits:' (term +))? ('rel:' term)?
 "}
 *}
 
@@ -2364,6 +2363,8 @@
   @{syntax_def wfc_discs_sels}: name_list (name_list_list name_term_list_list? )?
   ;
   @{syntax_def name_term}: (name ':' term)
+  ;
+  X_list: '[' (X + ',') ']'
 "}
 
 % options: no_discs_sels rep_compat

--- a/src/HOL/BNF/BNF_Def.thy	Wed Nov 13 09:37:00 2013 +0100
+++ b/src/HOL/BNF/BNF_Def.thy	Wed Nov 13 10:53:36 2013 +0100
@@ -202,5 +202,4 @@
 ML_file "Tools/bnf_def_tactics.ML"
 ML_file "Tools/bnf_def.ML"
 
-
 end

--- a/src/HOL/BNF/Basic_BNFs.thy	Wed Nov 13 09:37:00 2013 +0100
+++ b/src/HOL/BNF/Basic_BNFs.thy	Wed Nov 13 10:53:36 2013 +0100
@@ -27,14 +27,20 @@
 lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Grp B1 f1 OO (Grp B2 f2)\<inverse>\<inverse> \<le> (Grp A p1)\<inverse>\<inverse> OO Grp A p2"
   unfolding wpull_def Grp_def by auto
 
-bnf ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq"
-  "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+bnf ID: 'a
+  map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+  sets: "\<lambda>x. {x}"
+  bd: natLeq
+  rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
 apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
 done
 
-bnf DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
+bnf DEADID: 'a
+  map: "id :: 'a \<Rightarrow> 'a"
+  bd: "natLeq +c |UNIV :: 'a set|"
+  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
 by (auto simp add: wpull_Grp_def Grp_def
   card_order_csum natLeq_card_order card_of_card_order_on
   cinfinite_csum natLeq_cinfinite)
@@ -47,7 +53,12 @@
 
 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
 
-bnf sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
+bnf "'a + 'b"
+  map: sum_map
+  sets: setl setr
+  bd: natLeq
+  wits: Inl Inr
+  rel: sum_rel
 proof -
   show "sum_map id id = id" by (rule sum_map.id)
 next
@@ -147,7 +158,11 @@
 
 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
 
-bnf map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. natLeq" prod_rel
+bnf "'a \<times> 'b"
+  map: map_pair
+  sets: fsts snds
+  bd: natLeq
+  rel: prod_rel
 proof (unfold prod_set_defs)
   show "map_pair id id = id" by (rule map_pair.id)
 next
@@ -230,8 +245,11 @@
   ultimately show ?thesis using card_of_ordLeq by fast
 qed
 
-bnf "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
-  "fun_rel op ="
+bnf "'a \<Rightarrow> 'b"
+  map: "op \<circ>"
+  sets: range
+  bd: "natLeq +c |UNIV :: 'a set|"
+  rel: "fun_rel op ="
 proof
   fix f show "id \<circ> f = id f" by simp
 next

--- a/src/HOL/BNF/More_BNFs.thy	Wed Nov 13 09:37:00 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Wed Nov 13 10:53:36 2013 +0100
@@ -21,7 +21,12 @@
 lemma option_rec_conv_option_case: "option_rec = option_case"
 by (simp add: fun_eq_iff split: option.split)
 
-bnf Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"] option_rel
+bnf "'a option"
+  map: Option.map
+  sets: Option.set
+  bd: natLeq 
+  wits: None
+  rel: option_rel
 proof -
   show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
 next
@@ -94,7 +99,11 @@
     (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
 qed
 
-bnf map [set] "\<lambda>_::'a list. natLeq" ["[]"]
+bnf "'a list"
+  map: map
+  sets: set
+  bd: natLeq
+  wits: Nil
 proof -
   show "map id = id" by (rule List.map.id)
 next
@@ -214,7 +223,12 @@
      using X' Y1 Y2 by (auto simp: X'eq intro!: exI[of _ "x"]) (transfer, blast)+
 qed
 
-bnf fimage [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
+bnf "'a fset"
+  map: fimage
+  sets: fset 
+  bd: natLeq
+  wits: "{||}"
+  rel: fset_rel
 apply -
           apply transfer' apply simp
          apply transfer' apply force
@@ -300,7 +314,12 @@
     by transfer force
 qed
 
-bnf cimage [rcset] "\<lambda>_::'a cset. natLeq" ["cempty"] cset_rel
+bnf "'a cset"
+  map: cimage
+  sets: rcset
+  bd: natLeq
+  wits: "cempty"
+  rel: cset_rel
 proof -
   show "cimage id = id" by transfer' simp
 next
@@ -874,7 +893,11 @@
   by transfer
     (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
 
-bnf mmap [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
+bnf "'a multiset"
+  map: mmap
+  sets: set_of 
+  bd: natLeq
+  wits: "{#}"
 by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
   intro: mmap_cong wpull_mmap)
 

--- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Nov 13 09:37:00 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Nov 13 10:53:36 2013 +0100
@@ -147,7 +147,7 @@
     val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1);
 
     (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
-    val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
+    val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd;
 
     fun map_id0_tac _ =
       mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
@@ -257,7 +257,7 @@
 
     val (bnf', lthy') =
       bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
-        Binding.empty [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
+        Binding.empty [] ((((((b, CCA), mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -351,7 +351,7 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
-        Binding.empty [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+        Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -433,7 +433,7 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
-        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+        [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -506,7 +506,7 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
-        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+        [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -643,7 +643,7 @@
     val (bnf', lthy') =
       bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)
         Binding.empty Binding.empty []
-        (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
+        ((((((b, T), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   in
     ((bnf', deads), lthy')
   end;

--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Nov 13 09:37:00 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Nov 13 10:53:36 2013 +0100
@@ -105,7 +105,7 @@
     ({prems: thm list, context: Proof.context} -> tactic) list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
     binding -> binding list ->
-    ((((binding * term) * term list) * term) * term list) * term option ->
+    (((((binding * typ) * term) * term list) * term) * term list) * term option ->
     local_theory -> bnf * local_theory
 end;
 
@@ -651,18 +651,18 @@
 
 (* Define new BNFs *)
 
-fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b rel_b set_bs
-  (((((raw_bnf_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy =
+fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs
+  ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
+  no_defs_lthy =
   let
     val fact_policy = mk_fact_policy no_defs_lthy;
     val bnf_b = qualify raw_bnf_b;
     val live = length raw_sets;
 
+    val bnf_rhs_T = prep_typ no_defs_lthy raw_bnf_T;
     val map_rhs = prep_term no_defs_lthy raw_map;
     val set_rhss = map (prep_term no_defs_lthy) raw_sets;
-    val (bd_rhsT, bd_rhs) = (case prep_term no_defs_lthy raw_bd_Abs of
-      Abs (_, T, t) => (T, t)
-    | _ => error "Bad bound constant");
+    val bd_rhs = prep_term no_defs_lthy raw_bd;
 
     fun err T =
       error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
@@ -670,9 +670,9 @@
 
     val (bnf_b, key) =
       if Binding.eq_name (bnf_b, Binding.empty) then
-        (case bd_rhsT of
+        (case bnf_rhs_T of
           Type (C, Ts) => if forall (can dest_TFree) Ts
-            then (Binding.qualified_name C, C) else err bd_rhsT
+            then (Binding.qualified_name C, C) else err bnf_rhs_T
         | T => err T)
       else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
 
@@ -745,9 +745,9 @@
     val CA_params = map TVar (Term.add_tvarsT CA []);
 
     val bnf_sets = map2 (normalize_set CA_params) alphas (map (Morphism.term phi) bnf_set_terms);
-    val bdT = Morphism.typ phi bd_rhsT;
+    val bnf_T = Morphism.typ phi bnf_rhs_T;
     val bnf_bd =
-      Term.subst_TVars (Term.add_tvar_namesT bdT [] ~~ CA_params) (Morphism.term phi bnf_bd_term);
+      Term.subst_TVars (Term.add_tvar_namesT bnf_T [] ~~ CA_params) (Morphism.term phi bnf_bd_term);
 
     (*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*)
     val deads = (case Ds_opt of
@@ -1334,7 +1334,7 @@
     map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
       goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs)
     |> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
-  end) oo prepare_def const_policy fact_policy qualify (K I) Ds map_b rel_b set_bs;
+  end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs;
 
 val bnf_cmd = (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
   let
@@ -1353,7 +1353,7 @@
     Proof.unfolding ([[(defs, [])]])
       (Proof.theorem NONE (snd o register_bnf key oo after_qed mk_wit_thms)
         (map (single o rpair []) goals @ nontriv_wit_goals) lthy)
-  end) oo prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE
+  end) oo prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_typ Syntax.read_term NONE
     Binding.empty Binding.empty [];
 
 fun print_bnfs ctxt =
@@ -1389,11 +1389,14 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "bnf"}
     "register a type as a bounded natural functor"
-    ((parse_opt_binding_colon -- Parse.term --
-       (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
-       (Scan.option ((@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}))
-         >> the_default []) --
-       Scan.option Parse.term)
+    (parse_opt_binding_colon -- Parse.typ --|
+       (Parse.reserved "map" -- @{keyword ":"}) -- Parse.term --
+       (Scan.option ((Parse.reserved "sets" -- @{keyword ":"}) |--
+         Scan.repeat1 (Scan.unless (Parse.reserved "bd") Parse.term)) >> the_default []) --|
+       (Parse.reserved "bd" -- @{keyword ":"}) -- Parse.term --
+       (Scan.option ((Parse.reserved "wits" -- @{keyword ":"}) |--
+         Scan.repeat1 (Scan.unless (Parse.reserved "rel") Parse.term)) >> the_default []) --
+       Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term)
        >> bnf_cmd);
 
 end;

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Nov 13 09:37:00 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Nov 13 10:53:36 2013 +0100
@@ -2678,7 +2678,7 @@
               fn T => fn (thms, wits) => fn lthy =>
             bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) map_b
               rel_b set_bs
-              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
+              ((((((b, T), fold_rev Term.absfree fs' mapx), sets), bd), wits), NONE) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy;
 

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Nov 13 09:37:00 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Nov 13 10:53:36 2013 +0100
@@ -1749,7 +1749,7 @@
               fn T => fn wits => fn lthy =>
             bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads)
               map_b rel_b set_bs
-              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
+              ((((((b, T), fold_rev Term.absfree fs' mapx), sets), bd), wits), NONE)
               lthy
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;