# HG changeset patch
# User blanchet
# Date 1366802180 -7200
# Node ID 7babcb61aa5c04b418fd7f2c07d63263d2de14e2
# Parent  b0bae7bd236c95573b292bad38a977dd9a1d8bc6
honor user-specified set function names

diff -r b0bae7bd236c -r 7babcb61aa5c 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:20 2013 +0200
@@ -261,7 +261,7 @@
         (maps wit_thms_of_bnf inners);
 
     val (bnf', lthy') =
-      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss))
+      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) []
         (((((b, mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
@@ -359,7 +359,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 (killedAs @ Ds))
+      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;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
@@ -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) []
         (((((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) []
         (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
@@ -662,7 +662,7 @@
 
     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) []
       (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   in
     ((bnf', deads), lthy')
diff -r b0bae7bd236c -r 7babcb61aa5c 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:20 2013 +0200
@@ -92,7 +92,7 @@
   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 ->
+    ({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
 end;
@@ -535,7 +535,7 @@
 
 (* Define new BNFs *)
 
-fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt
+fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt 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;
@@ -587,15 +587,23 @@
     val map_bind_def = (fn () => Binding.suffix_name ("_" ^ mapN) b, map_rhs);
     val set_binds_defs =
       let
-        val bs = if live = 1 then [fn () => Binding.suffix_name ("_" ^ setN) b]
-          else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_setN i) b) (1 upto live)
-      in map2 pair bs set_rhss end;
+        fun set_name i get_b =
+          (case try (nth set_bs) (i - 1) of
+            SOME b => if Binding.is_empty b then get_b else K b
+          | NONE => get_b);
+        val bs =
+          if live = 1 then
+            [set_name 1 (fn () => Binding.suffix_name ("_" ^ setN) b)]
+          else
+            map (fn i => set_name i (fn () => Binding.suffix_name ("_" ^ mk_setN i) b))
+              (1 upto live);
+      in bs ~~ set_rhss end;
     val bd_bind_def = (fn () => Binding.suffix_name ("_" ^ bdN) b, bd_rhs);
     val wit_binds_defs =
       let
         val bs = if nwits = 1 then [fn () => Binding.suffix_name ("_" ^ witN) b]
           else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_witN i) b) (1 upto nwits);
-      in map2 pair bs wit_rhss end;
+      in bs ~~ wit_rhss end;
 
     val (((((bnf_map_term, raw_map_def),
       (bnf_set_terms, raw_set_defs)),
@@ -1178,7 +1186,7 @@
                     (map_wpullN, [#map_wpull axioms]),
                     (set_naturalN, #set_natural axioms),
                     (set_bdN, #set_bd axioms)] @
-                    map2 pair witNs wit_thms
+                    (witNs ~~ wit_thms)
                     |> map (fn (thmN, thms) =>
                       ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
                       [(thms, [])]));
@@ -1246,13 +1254,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) oo prepare_def const_policy fact_policy qualify (K I) Ds;
+  end) ooo 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 [];
 
 fun print_bnfs ctxt =
   let
diff -r b0bae7bd236c -r 7babcb61aa5c 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:20 2013 +0200
@@ -142,10 +142,10 @@
 
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
-  val fp_bnf: (mixfix list -> (string * sort) list option -> binding 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 -> (string * sort) list -> ((string * sort) * typ) list ->
-    local_theory -> BNF_Def.BNF list * 'a
+    binding list -> mixfix list -> binding list list -> (string * sort) list ->
+    ((string * sort) * typ) list -> local_theory -> BNF_Def.BNF list * 'a
 end;
 
 structure BNF_FP : BNF_FP =
@@ -390,7 +390,7 @@
   | 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 sort lhss bnfs deadss livess unfold_set lthy =
+fun mk_fp_bnf timer construct_fp resBs 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 +418,14 @@
 
     val timer = time (timer "Normalization & sealing of BNFs");
 
-    val res = construct_fp resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
+    val res = construct_fp resBs 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 resBs eqs lthy =
+fun fp_bnf construct_fp bs mixfixes set_bss resBs eqs lthy =
   let
     val timer = time (Timer.startRealTimer ());
     val (lhss, rhss) = split_list eqs;
@@ -435,7 +435,8 @@
       (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 sort lhss bnfs Dss Ass unfold_set lthy'
+    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs set_bss sort lhss bnfs Dss Ass
+      unfold_set lthy'
   end;
 
 end;
diff -r b0bae7bd236c -r 7babcb61aa5c 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:20 2013 +0200
@@ -8,14 +8,16 @@
 signature BNF_FP_DEF_SUGAR =
 sig
   val datatypes: bool ->
-    (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
-      BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
+    (mixfix list -> (string * sort) list option -> 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 ->
     local_theory -> local_theory
   val parse_datatype_cmd: bool ->
-    (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
-      BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
+    (mixfix list -> (string * sort) list option -> 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;
 
@@ -163,6 +165,7 @@
     val Ass0 = map (map prepare_type_arg o type_args_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 (((Bs0, Cs), Xs), no_defs_lthy) =
       no_defs_lthy0
@@ -237,7 +240,7 @@
     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 (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
+      fp_bnf construct_fp fp_bs mixfixes set_bss (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
 
     val timer = time (Timer.startRealTimer ());
 
diff -r b0bae7bd236c -r 7babcb61aa5c 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:20 2013 +0200
@@ -10,7 +10,8 @@
 signature BNF_GFP =
 sig
   val construct_gfp: mixfix list -> (string * sort) list option -> binding list ->
-    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory
+    binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
+    BNF_FP.fp_result * local_theory
 end;
 
 structure BNF_GFP : BNF_GFP =
@@ -54,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 (resDs, Dss) bnfs lthy =
+fun construct_gfp mixfixes resBs bs set_bss (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
@@ -2894,11 +2895,12 @@
         val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Jbnfs, lthy) =
-          fold_map6 (fn tacs => fn b => 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)
+          fold_map7 (fn tacs => fn 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
             |> register_bnf (Local_Theory.full_name lthy b))
-          tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
+          tacss 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 b0bae7bd236c -r 7babcb61aa5c 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:20 2013 +0200
@@ -9,7 +9,8 @@
 signature BNF_LFP =
 sig
   val construct_lfp: mixfix list -> (string * sort) list option -> binding list ->
-    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory
+    binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
+    BNF_FP.fp_result * local_theory
 end;
 
 structure BNF_LFP : BNF_LFP =
@@ -25,7 +26,7 @@
 open BNF_LFP_Tactics
 
 (*all BNFs have the same lives*)
-fun construct_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
+fun construct_lfp mixfixes resBs bs set_bss (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
@@ -1733,11 +1734,12 @@
         fun wit_tac _ = mk_wit_tac n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Ibnfs, lthy) =
-          fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn wits => fn lthy =>
-            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads)
+          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
               (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
-          tacss bs fs_maps setss_by_bnf Ts ctor_witss lthy;
+          tacss 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 b0bae7bd236c -r 7babcb61aa5c 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:20 2013 +0200
@@ -43,6 +43,7 @@
   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
+  val pad_list: 'a -> int -> 'a list -> 'a list
 
   val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
   val mk_TFrees: int -> Proof.context -> typ list * Proof.context
@@ -616,6 +617,8 @@
       map (f false) negs @ [f true pos]
     end;
 
+fun pad_list x n xs = xs @ replicate (n - length xs) x;
+
 fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
 
 fun is_triv_implies thm =
diff -r b0bae7bd236c -r 7babcb61aa5c src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Apr 24 13:16:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Apr 24 13:16:20 2013 +0200
@@ -65,8 +65,6 @@
 val safe_elim_attrs = @{attributes [elim!]};
 val simp_attrs = @{attributes [simp]};
 
-fun pad_list x n xs = xs @ replicate (n - length xs) x;
-
 fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys)));
 
 fun mk_half_pairss' _ ([], []) = []