command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it

--- a/src/HOL/BNF/BNF.thy	Wed Nov 27 11:08:55 2013 +0100
+++ b/src/HOL/BNF/BNF.thy	Wed Nov 27 15:08:18 2013 +0100
@@ -10,7 +10,7 @@
 header {* Bounded Natural Functors for (Co)datatypes *}
 
 theory BNF
-imports Countable_Set_Type BNF_LFP BNF_GFP
+imports Countable_Set_Type BNF_LFP BNF_GFP BNF_Decl
 begin
 
 hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/BNF_Decl.thy	Wed Nov 27 15:08:18 2013 +0100
@@ -0,0 +1,18 @@
+(*  Title:      HOL/BNF/BNF_Decl.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Copyright   2013
+
+Axiomatic declaration of bounded natural functors.
+*)
+
+header {* Axiomatic declaration of Bounded Natural Functors *}
+
+theory BNF_Decl
+imports BNF_Def
+keywords
+  "bnf_decl" :: thy_decl
+begin
+
+ML_file "Tools/bnf_decl.ML"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Tools/bnf_decl.ML	Wed Nov 27 15:08:18 2013 +0100
@@ -0,0 +1,96 @@
+(*  Title:      HOL/BNF/Tools/bnf_decl.ML
+    Author:     Dmitriy Traytel, TU Muenchen
+    Copyright   2013
+
+Axiomatic declaration of bounded natural functors.
+*)
+
+signature BNF_DECL =
+sig
+  val bnf_decl: (binding option * (typ * sort)) list -> binding -> mixfix -> binding -> binding ->
+    local_theory -> BNF_Def.bnf * local_theory
+end
+
+structure BNF_Decl : BNF_DECL =
+struct
+
+open BNF_Util
+open BNF_Def
+
+fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb lthy =
+  let
+   fun prepare_type_arg (set_opt, (ty, c)) =
+      let val s = fst (dest_TFree (prepare_typ lthy ty)) in
+        (set_opt, (s, prepare_constraint lthy c))
+      end;
+    val ((user_setbs, vars), raw_vars') =
+      map prepare_type_arg raw_vars
+      |> `split_list
+      |>> apfst (map_filter I);
+    val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars';
+
+    fun mk_b name user_b =
+      (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
+      |> Binding.qualify false (Binding.name_of b);
+    val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy;
+    val (bd_type_Tname, lthy) =
+      Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy;
+    val T = Type (Tname, map TFree vars);
+    val bd_type_T = Type (bd_type_Tname, map TFree deads);
+    val lives = map TFree (filter_out (member (op =) deads) vars);
+    val live = length lives;
+    val _ = "Trying to declare a BNF with no live variables" |> null lives ? error;
+    val (lives', _) = BNF_Util.mk_TFrees (length lives)
+      (fold Variable.declare_typ (map TFree vars) lthy);
+    val T' = Term.typ_subst_atomic (lives ~~ lives') T;
+    val mapT = map2 (curry op -->) lives lives' ---> T --> T';
+    val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
+    val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
+    val mapb = mk_b BNF_Def.mapN user_mapb;
+    val bdb = mk_b "bd" Binding.empty;
+    val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs
+      (if live = 1 then [0] else 1 upto live);
+    val lthy = Local_Theory.background_theory
+      (Sign.add_consts_i ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
+        map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs))
+      lthy;
+    val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
+    val Fsets = map2 (fn setb => fn setT =>
+      Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
+    val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
+    val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
+      prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads))
+      user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), []), NONE) lthy;
+
+    fun mk_wits_tac set_maps = K (TRYALL Goal.conjunction_tac) THEN' the triv_tac_opt set_maps;
+    val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
+    fun mk_wit_thms set_maps =
+      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
+        |> Conjunction.elim_balanced (length wit_goals)
+        |> map2 (Conjunction.elim_balanced o length) wit_goalss
+        |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
+
+    val ((_, [thms]), (lthy_old, lthy)) = Local_Theory.background_theory_result
+      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), goals)]) lthy
+      ||> `Local_Theory.restore;
+    val phi = Proof_Context.export_morphism lthy_old lthy;
+  in
+    BNF_Def.register_bnf key (after_qed mk_wit_thms (map single  (Morphism.fact phi thms)) lthy)
+  end;
+
+val bnf_decl = prepare_decl (K I) (K I);
+
+fun read_constraint _ NONE = HOLogic.typeS
+  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
+
+val bnf_decl_cmd = prepare_decl read_constraint Syntax.parse_typ;
+
+val parse_bnf_decl =
+  parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- Parse.opt_mixfix;
+
+val _ =
+  Outer_Syntax.local_theory @{command_spec "bnf_decl"} "bnf declaration"
+    (parse_bnf_decl >> 
+      (fn (((bsTs, b), (mapb, relb)), mx) => bnf_decl_cmd bsTs b mx mapb relb #> snd));
+
+end;

--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Nov 27 11:08:55 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Nov 27 15:08:18 2013 +0100
@@ -101,6 +101,15 @@
     Proof.context
 
   val print_bnfs: Proof.context -> unit
+  val prepare_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
+    (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option ->
+    binding -> binding -> binding list ->
+    (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
+    string * term list *
+    ((thm list -> {context: Proof.context, prems: thm list} -> tactic) option * term list list) *
+    ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
+    local_theory * thm list
+
   val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
     ({prems: thm list, context: Proof.context} -> tactic) list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Nov 27 11:08:55 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Nov 27 15:08:18 2013 +0100
@@ -1515,24 +1515,13 @@
 
 val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained;
 
+(*FIXME: use parse_type_args_named_constrained from BNF_Util and thus 
+  allow users to kill certain arguments of a (co)datatype*)
 val parse_type_args_named_constrained =
   parse_type_arg_constrained >> (single o pair Binding.empty) ||
   @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
   Scan.succeed [];
 
-val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- parse_binding;
-
-val no_map_rel = (Binding.empty, Binding.empty);
-
-fun extract_map_rel ("map", b) = apfst (K b)
-  | extract_map_rel ("rel", b) = apsnd (K b)
-  | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")");
-
-val parse_map_rel_bindings =
-  @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"}
-    >> (fn ps => fold extract_map_rel ps no_map_rel) ||
-  Scan.succeed no_map_rel;
-
 val parse_ctr_spec =
   parse_opt_binding_colon -- parse_binding -- Scan.repeat parse_ctr_arg --
   Scan.optional parse_defaults [] -- Parse.opt_mixfix;

--- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Nov 27 11:08:55 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Nov 27 15:08:18 2013 +0100
@@ -136,6 +136,8 @@
 
   val parse_binding_colon: binding parser
   val parse_opt_binding_colon: binding parser
+  val parse_type_args_named_constrained: (binding option * (string * string option)) list parser
+  val parse_map_rel_bindings: (binding * binding) parser
 
   val typedef: binding * (string * sort) list * mixfix -> term ->
     (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
@@ -253,6 +255,32 @@
 val parse_binding_colon = parse_binding --| @{keyword ":"};
 val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
 
+val parse_type_arg_constrained =
+  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
+
+val parse_type_arg_named_constrained =
+   (Parse.minus --| @{keyword ":"} >> K NONE || parse_opt_binding_colon >> SOME) --
+   parse_type_arg_constrained;
+
+val parse_type_args_named_constrained =
+  parse_type_arg_constrained >> (single o pair (SOME Binding.empty)) ||
+  @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
+  Scan.succeed [];
+
+val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- parse_binding;
+
+val no_map_rel = (Binding.empty, Binding.empty);
+
+fun extract_map_rel ("map", b) = apfst (K b)
+  | extract_map_rel ("rel", b) = apsnd (K b)
+  | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")");
+
+val parse_map_rel_bindings =
+  @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"}
+    >> (fn ps => fold extract_map_rel ps no_map_rel) ||
+  Scan.succeed no_map_rel;
+
+
 (*TODO: is this really different from Typedef.add_typedef_global?*)
 fun typedef (b, Ts, mx) set opt_morphs tac lthy =
   let