# HG changeset patch
# User blanchet
# Date 1366802181 -7200
# Node ID 55963309557b67080230ca7a14a5a745986200a4
# Parent  7babcb61aa5c04b418fd7f2c07d63263d2de14e2
honor user-specified name for map function

diff -r 7babcb61aa5c -r 55963309557b src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 13:16:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 13:16:21 2013 +0200
@@ -261,8 +261,8 @@
         (maps wit_thms_of_bnf inners);
 
     val (bnf', lthy') =
-      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) []
-        (((((b, mapx), sets), bd), wits), SOME rel) lthy;
+      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
+        [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -359,8 +359,8 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) []
-        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
+        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -443,7 +443,7 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) []
+      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
         (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
 
   in
@@ -520,7 +520,7 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) []
+      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
         (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
@@ -662,7 +662,8 @@
 
     fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
 
-    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads) []
+    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
+      Binding.empty []
       (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   in
     ((bnf', deads), lthy')
diff -r 7babcb61aa5c -r 55963309557b src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 13:16:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 13:16:21 2013 +0200
@@ -92,9 +92,9 @@
   val print_bnfs: Proof.context -> unit
   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 list ->
-    ((((binding * term) * term list) * term) * term list) * term option -> local_theory ->
-    BNF * local_theory
+    ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
+    binding list -> ((((binding * term) * term list) * term) * term list) * term option ->
+    local_theory -> BNF * local_theory
 end;
 
 structure BNF_Def : BNF_DEF =
@@ -535,7 +535,7 @@
 
 (* Define new BNFs *)
 
-fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt set_bs
+fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b set_bs
   (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy =
   let
     val fact_policy = mk_fact_policy no_defs_lthy;
@@ -584,7 +584,9 @@
     fun maybe_restore lthy_old lthy =
       lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;
 
-    val map_bind_def = (fn () => Binding.suffix_name ("_" ^ mapN) b, map_rhs);
+    val map_bind_def =
+      (fn () => if Binding.is_empty map_b then Binding.suffix_name ("_" ^ mapN) b else map_b,
+       map_rhs);
     val set_binds_defs =
       let
         fun set_name i get_b =
@@ -1254,13 +1256,13 @@
     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 (map single thms @ wit_thms) lthy)
-  end) ooo prepare_def const_policy fact_policy qualify (K I) Ds;
+  end) oooo prepare_def const_policy fact_policy qualify (K I) Ds;
 
 val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
   Proof.unfolding ([[(defs, [])]])
     (Proof.theorem NONE (snd o register_bnf key oo after_qed)
       (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
-  prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE [];
+  prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE Binding.empty [];
 
 fun print_bnfs ctxt =
   let
diff -r 7babcb61aa5c -r 55963309557b src/HOL/BNF/Tools/bnf_fp.ML
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Wed Apr 24 13:16:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Wed Apr 24 13:16:21 2013 +0200
@@ -142,9 +142,9 @@
 
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
-  val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list list ->
-    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
-    binding list -> mixfix list -> binding list list -> (string * sort) list ->
+  val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list ->
+      binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
+    binding list -> mixfix list -> binding list -> binding list list -> (string * sort) list ->
     ((string * sort) * typ) list -> local_theory -> BNF_Def.BNF list * 'a
 end;
 
@@ -390,7 +390,8 @@
   | fp_sort lhss (SOME resBs) Ass =
     (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
 
-fun mk_fp_bnf timer construct_fp resBs bs set_bss sort lhss bnfs deadss livess unfold_set lthy =
+fun mk_fp_bnf timer construct_fp resBs bs map_bs set_bss sort lhss bnfs deadss livess unfold_set
+    lthy =
   let
     val name = mk_common_name (map Binding.name_of bs);
     fun qualify i =
@@ -418,14 +419,14 @@
 
     val timer = time (timer "Normalization & sealing of BNFs");
 
-    val res = construct_fp resBs bs set_bss (map TFree resDs, deadss) bnfs'' lthy'';
+    val res = construct_fp resBs bs map_bs set_bss (map TFree resDs, deadss) bnfs'' lthy'';
 
     val timer = time (timer "FP construction in total");
   in
     timer; (bnfs'', res)
   end;
 
-fun fp_bnf construct_fp bs mixfixes set_bss resBs eqs lthy =
+fun fp_bnf construct_fp bs mixfixes map_bs set_bss resBs eqs lthy =
   let
     val timer = time (Timer.startRealTimer ());
     val (lhss, rhss) = split_list eqs;
@@ -435,7 +436,7 @@
       (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
         (empty_unfolds, lthy));
   in
-    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs set_bss sort lhss bnfs Dss Ass
+    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs map_bs set_bss sort lhss bnfs Dss Ass
       unfold_set lthy'
   end;
 
diff -r 7babcb61aa5c -r 55963309557b src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 13:16:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 13:16:21 2013 +0200
@@ -8,15 +8,16 @@
 signature BNF_FP_DEF_SUGAR =
 sig
   val datatypes: bool ->
-    (mixfix list -> (string * sort) list option -> binding list -> binding list list ->
-      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
+    (mixfix list -> (string * sort) list option -> binding list -> binding list ->
+      binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
       BNF_FP.fp_result * local_theory) ->
-    (bool * bool) * (((((binding * typ) * sort) list * binding) * mixfix) * ((((binding * binding) *
-      (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
+    (bool * bool) * ((((binding * (binding * (typ * sort)) list) * binding) * mixfix) *
+      ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
+        mixfix) list) list ->
     local_theory -> local_theory
   val parse_datatype_cmd: bool ->
-    (mixfix list -> (string * sort) list option -> binding list -> binding list list ->
-      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
+    (mixfix list -> (string * sort) list option -> binding list -> binding list ->
+      binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
       BNF_FP.fp_result * local_theory) ->
     (local_theory -> local_theory) parser
 end;
@@ -129,7 +130,8 @@
   reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
   handle THM _ => thm;
 
-fun type_args_constrained_of (((cAs, _), _), _) = cAs;
+fun map_binding_of ((((b, _), _), _), _) = b;
+fun type_args_named_constrained_of ((((_, ncAs), _), _), _) = ncAs;
 fun type_binding_of (((_, b), _), _) = b;
 fun mixfix_of ((_, mx), _) = mx;
 fun ctr_specs_of (_, ctr_specs) = ctr_specs;
@@ -156,16 +158,17 @@
     val fp_bs = map type_binding_of specs;
     val fp_b_names = map Binding.name_of fp_bs;
     val fp_common_name = mk_common_name fp_b_names;
+    val map_bs = map map_binding_of specs;
 
-    fun prepare_type_arg ((_, ty), c) =
+    fun prepare_type_arg (_, (ty, c)) =
       let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
         TFree (s, prepare_constraint no_defs_lthy0 c)
       end;
 
-    val Ass0 = map (map prepare_type_arg o type_args_constrained_of) specs;
+    val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of) specs;
     val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
     val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
-    val set_bss = map (map (fst o fst) o type_args_constrained_of) specs;
+    val set_bss = map (map fst o type_args_named_constrained_of) specs;
 
     val (((Bs0, Cs), Xs), no_defs_lthy) =
       no_defs_lthy0
@@ -180,7 +183,8 @@
       locale and shadows an existing global type*)
     val fake_thy =
       Theory.copy #> fold (fn spec => perhaps (try (Sign.add_type no_defs_lthy
-        (type_binding_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs;
+          (type_binding_of spec, length (type_args_named_constrained_of spec), mixfix_of spec))))
+        specs;
     val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;
 
     fun mk_fake_T b =
@@ -240,7 +244,8 @@
     val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
            fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
            fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
-      fp_bnf construct_fp fp_bs mixfixes set_bss (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
+      fp_bnf construct_fp fp_bs mixfixes map_bs set_bss (map dest_TFree unsorted_As) fp_eqs
+        no_defs_lthy0;
 
     val timer = time (Timer.startRealTimer ());
 
@@ -1181,21 +1186,21 @@
 val parse_defaults =
   @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
 
-(* Identical to unexported function of the same name in "Pure/Isar/parse.ML" *)
-fun parse_type_arguments arg =
-  arg >> single || @{keyword "("} |-- Parse.!!! (Parse.list1 arg --| @{keyword ")"}) ||
+val parse_type_arg_constrained =
+  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort)
+
+val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained
+
+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_type_arg_constrained =
-  parse_opt_binding_colon -- Parse.type_ident --
-  Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort)
-
-val parse_type_args_constrained = parse_type_arguments parse_type_arg_constrained;
-
 val parse_single_spec =
-  parse_type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
-  (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon -- Parse.binding --
-    Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] -- Parse.opt_mixfix));
+  parse_opt_binding_colon -- parse_type_args_named_constrained -- Parse.binding --
+  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon --
+      Parse.binding -- Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] --
+    Parse.opt_mixfix));
 
 val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
 
diff -r 7babcb61aa5c -r 55963309557b src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 13:16:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 13:16:21 2013 +0200
@@ -9,7 +9,7 @@
 
 signature BNF_GFP =
 sig
-  val construct_gfp: mixfix list -> (string * sort) list option -> binding list ->
+  val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
     binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     BNF_FP.fp_result * local_theory
 end;
@@ -55,7 +55,7 @@
      ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
 
 (*all BNFs have the same lives*)
-fun construct_gfp mixfixes resBs bs set_bss (resDs, Dss) bnfs lthy =
+fun construct_gfp mixfixes resBs bs map_bs set_bss (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
@@ -2895,12 +2895,13 @@
         val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Jbnfs, lthy) =
-          fold_map7 (fn tacs => fn b => fn set_bs => fn mapx => fn sets => fn T =>
+          fold_map8 (fn tacs => fn b => fn map_b => fn set_bs => fn mapx => fn sets => fn T =>
               fn (thms, wits) => fn lthy =>
-            bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) set_bs
-              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
+            bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) map_b
+              set_bs (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
+              lthy
             |> register_bnf (Local_Theory.full_name lthy b))
-          tacss bs set_bss fs_maps setss_by_bnf Ts all_witss lthy;
+          tacss bs map_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy;
 
         val fold_maps = fold_thms lthy (map (fn bnf =>
           mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs);
diff -r 7babcb61aa5c -r 55963309557b src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 13:16:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 13:16:21 2013 +0200
@@ -8,7 +8,7 @@
 
 signature BNF_LFP =
 sig
-  val construct_lfp: mixfix list -> (string * sort) list option -> binding list ->
+  val construct_lfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
     binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     BNF_FP.fp_result * local_theory
 end;
@@ -26,7 +26,7 @@
 open BNF_LFP_Tactics
 
 (*all BNFs have the same lives*)
-fun construct_lfp mixfixes resBs bs set_bss (resDs, Dss) bnfs lthy =
+fun construct_lfp mixfixes resBs bs map_bs set_bss (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
@@ -1734,12 +1734,12 @@
         fun wit_tac _ = mk_wit_tac n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Ibnfs, lthy) =
-          fold_map7 (fn tacs => fn b => fn set_bs => fn mapx => fn sets => fn T => fn wits =>
-              fn lthy =>
-            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) set_bs
+          fold_map8 (fn tacs => fn b => fn map_b => fn set_bs => fn mapx => fn sets => fn T =>
+              fn wits => fn lthy =>
+            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) map_b set_bs
               (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
-          tacss bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
+          tacss bs map_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
 
         val fold_maps = fold_thms lthy (map (fn bnf =>
           mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Ibnfs);
diff -r 7babcb61aa5c -r 55963309557b src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 13:16:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 13:16:21 2013 +0200
@@ -40,6 +40,9 @@
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g
   val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h
+  val fold_map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j * 'i) ->
+    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i ->
+    'j list * 'i
   val splice: 'a list -> 'a list -> 'a list
   val transpose: 'a list list -> 'a list list
   val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
@@ -273,6 +276,23 @@
     in (x :: xs, acc'') end
   | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
+fun fold_map7 _ [] [] [] [] [] [] [] acc = ([], acc)
+  | fold_map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) acc =
+    let
+      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 acc;
+      val (xs, acc'') = fold_map7 f x1s x2s x3s x4s x5s x6s x7s acc';
+    in (x :: xs, acc'') end
+  | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
+fun fold_map8 _ [] [] [] [] [] [] [] [] acc = ([], acc)
+  | fold_map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+      acc =
+    let
+      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 acc;
+      val (xs, acc'') = fold_map8 f x1s x2s x3s x4s x5s x6s x7s x8s acc';
+    in (x :: xs, acc'') end
+  | fold_map8 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
 (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);