honor user-specified set function names
authorblanchet
Wed Apr 24 13:16:20 2013 +0200 (2013-04-24)
changeset 517577babcb61aa5c
parent 51756 b0bae7bd236c
child 51758 55963309557b
honor user-specified set function names
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_fp.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_util.ML
src/HOL/BNF/Tools/bnf_wrap.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 13:16:20 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 13:16:20 2013 +0200
     1.3 @@ -261,7 +261,7 @@
     1.4          (maps wit_thms_of_bnf inners);
     1.5  
     1.6      val (bnf', lthy') =
     1.7 -      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss))
     1.8 +      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) []
     1.9          (((((b, mapx), sets), bd), wits), SOME rel) lthy;
    1.10    in
    1.11      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.12 @@ -359,7 +359,7 @@
    1.13      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.14  
    1.15      val (bnf', lthy') =
    1.16 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds))
    1.17 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) []
    1.18          (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.19    in
    1.20      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.21 @@ -443,7 +443,7 @@
    1.22      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.23  
    1.24      val (bnf', lthy') =
    1.25 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds)
    1.26 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) []
    1.27          (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.28  
    1.29    in
    1.30 @@ -520,7 +520,7 @@
    1.31      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.32  
    1.33      val (bnf', lthy') =
    1.34 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds)
    1.35 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) []
    1.36          (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.37    in
    1.38      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.39 @@ -662,7 +662,7 @@
    1.40  
    1.41      fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
    1.42  
    1.43 -    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
    1.44 +    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads) []
    1.45        (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
    1.46    in
    1.47      ((bnf', deads), lthy')
     2.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 13:16:20 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 13:16:20 2013 +0200
     2.3 @@ -92,7 +92,7 @@
     2.4    val print_bnfs: Proof.context -> unit
     2.5    val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
     2.6      ({prems: thm list, context: Proof.context} -> tactic) list ->
     2.7 -    ({prems: thm list, context: Proof.context} -> tactic) -> typ list option ->
     2.8 +    ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding list ->
     2.9      ((((binding * term) * term list) * term) * term list) * term option -> local_theory ->
    2.10      BNF * local_theory
    2.11  end;
    2.12 @@ -535,7 +535,7 @@
    2.13  
    2.14  (* Define new BNFs *)
    2.15  
    2.16 -fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt
    2.17 +fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt set_bs
    2.18    (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy =
    2.19    let
    2.20      val fact_policy = mk_fact_policy no_defs_lthy;
    2.21 @@ -587,15 +587,23 @@
    2.22      val map_bind_def = (fn () => Binding.suffix_name ("_" ^ mapN) b, map_rhs);
    2.23      val set_binds_defs =
    2.24        let
    2.25 -        val bs = if live = 1 then [fn () => Binding.suffix_name ("_" ^ setN) b]
    2.26 -          else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_setN i) b) (1 upto live)
    2.27 -      in map2 pair bs set_rhss end;
    2.28 +        fun set_name i get_b =
    2.29 +          (case try (nth set_bs) (i - 1) of
    2.30 +            SOME b => if Binding.is_empty b then get_b else K b
    2.31 +          | NONE => get_b);
    2.32 +        val bs =
    2.33 +          if live = 1 then
    2.34 +            [set_name 1 (fn () => Binding.suffix_name ("_" ^ setN) b)]
    2.35 +          else
    2.36 +            map (fn i => set_name i (fn () => Binding.suffix_name ("_" ^ mk_setN i) b))
    2.37 +              (1 upto live);
    2.38 +      in bs ~~ set_rhss end;
    2.39      val bd_bind_def = (fn () => Binding.suffix_name ("_" ^ bdN) b, bd_rhs);
    2.40      val wit_binds_defs =
    2.41        let
    2.42          val bs = if nwits = 1 then [fn () => Binding.suffix_name ("_" ^ witN) b]
    2.43            else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_witN i) b) (1 upto nwits);
    2.44 -      in map2 pair bs wit_rhss end;
    2.45 +      in bs ~~ wit_rhss end;
    2.46  
    2.47      val (((((bnf_map_term, raw_map_def),
    2.48        (bnf_set_terms, raw_set_defs)),
    2.49 @@ -1178,7 +1186,7 @@
    2.50                      (map_wpullN, [#map_wpull axioms]),
    2.51                      (set_naturalN, #set_natural axioms),
    2.52                      (set_bdN, #set_bd axioms)] @
    2.53 -                    map2 pair witNs wit_thms
    2.54 +                    (witNs ~~ wit_thms)
    2.55                      |> map (fn (thmN, thms) =>
    2.56                        ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
    2.57                        [(thms, [])]));
    2.58 @@ -1246,13 +1254,13 @@
    2.59      map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
    2.60        goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs)
    2.61      |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
    2.62 -  end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
    2.63 +  end) ooo prepare_def const_policy fact_policy qualify (K I) Ds;
    2.64  
    2.65  val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
    2.66    Proof.unfolding ([[(defs, [])]])
    2.67      (Proof.theorem NONE (snd o register_bnf key oo after_qed)
    2.68        (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
    2.69 -  prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE;
    2.70 +  prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE [];
    2.71  
    2.72  fun print_bnfs ctxt =
    2.73    let
     3.1 --- a/src/HOL/BNF/Tools/bnf_fp.ML	Wed Apr 24 13:16:20 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp.ML	Wed Apr 24 13:16:20 2013 +0200
     3.3 @@ -142,10 +142,10 @@
     3.4  
     3.5    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
     3.6  
     3.7 -  val fp_bnf: (mixfix list -> (string * sort) list option -> binding list ->
     3.8 +  val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list list ->
     3.9      typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
    3.10 -    binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
    3.11 -    local_theory -> BNF_Def.BNF list * 'a
    3.12 +    binding list -> mixfix list -> binding list list -> (string * sort) list ->
    3.13 +    ((string * sort) * typ) list -> local_theory -> BNF_Def.BNF list * 'a
    3.14  end;
    3.15  
    3.16  structure BNF_FP : BNF_FP =
    3.17 @@ -390,7 +390,7 @@
    3.18    | fp_sort lhss (SOME resBs) Ass =
    3.19      (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
    3.20  
    3.21 -fun mk_fp_bnf timer construct_fp resBs bs sort lhss bnfs deadss livess unfold_set lthy =
    3.22 +fun mk_fp_bnf timer construct_fp resBs bs set_bss sort lhss bnfs deadss livess unfold_set lthy =
    3.23    let
    3.24      val name = mk_common_name (map Binding.name_of bs);
    3.25      fun qualify i =
    3.26 @@ -418,14 +418,14 @@
    3.27  
    3.28      val timer = time (timer "Normalization & sealing of BNFs");
    3.29  
    3.30 -    val res = construct_fp resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
    3.31 +    val res = construct_fp resBs bs set_bss (map TFree resDs, deadss) bnfs'' lthy'';
    3.32  
    3.33      val timer = time (timer "FP construction in total");
    3.34    in
    3.35      timer; (bnfs'', res)
    3.36    end;
    3.37  
    3.38 -fun fp_bnf construct_fp bs mixfixes resBs eqs lthy =
    3.39 +fun fp_bnf construct_fp bs mixfixes set_bss resBs eqs lthy =
    3.40    let
    3.41      val timer = time (Timer.startRealTimer ());
    3.42      val (lhss, rhss) = split_list eqs;
    3.43 @@ -435,7 +435,8 @@
    3.44        (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
    3.45          (empty_unfolds, lthy));
    3.46    in
    3.47 -    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold_set lthy'
    3.48 +    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs set_bss sort lhss bnfs Dss Ass
    3.49 +      unfold_set lthy'
    3.50    end;
    3.51  
    3.52  end;
     4.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 13:16:20 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 13:16:20 2013 +0200
     4.3 @@ -8,14 +8,16 @@
     4.4  signature BNF_FP_DEF_SUGAR =
     4.5  sig
     4.6    val datatypes: bool ->
     4.7 -    (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
     4.8 -      BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
     4.9 +    (mixfix list -> (string * sort) list option -> binding list -> binding list list ->
    4.10 +      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    4.11 +      BNF_FP.fp_result * local_theory) ->
    4.12      (bool * bool) * (((((binding * typ) * sort) list * binding) * mixfix) * ((((binding * binding) *
    4.13        (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
    4.14      local_theory -> local_theory
    4.15    val parse_datatype_cmd: bool ->
    4.16 -    (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
    4.17 -      BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
    4.18 +    (mixfix list -> (string * sort) list option -> binding list -> binding list list ->
    4.19 +      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    4.20 +      BNF_FP.fp_result * local_theory) ->
    4.21      (local_theory -> local_theory) parser
    4.22  end;
    4.23  
    4.24 @@ -163,6 +165,7 @@
    4.25      val Ass0 = map (map prepare_type_arg o type_args_constrained_of) specs;
    4.26      val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
    4.27      val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
    4.28 +    val set_bss = map (map (fst o fst) o type_args_constrained_of) specs;
    4.29  
    4.30      val (((Bs0, Cs), Xs), no_defs_lthy) =
    4.31        no_defs_lthy0
    4.32 @@ -237,7 +240,7 @@
    4.33      val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
    4.34             fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
    4.35             fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
    4.36 -      fp_bnf construct_fp fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
    4.37 +      fp_bnf construct_fp fp_bs mixfixes set_bss (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
    4.38  
    4.39      val timer = time (Timer.startRealTimer ());
    4.40  
     5.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 13:16:20 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 13:16:20 2013 +0200
     5.3 @@ -10,7 +10,8 @@
     5.4  signature BNF_GFP =
     5.5  sig
     5.6    val construct_gfp: mixfix list -> (string * sort) list option -> binding list ->
     5.7 -    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory
     5.8 +    binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     5.9 +    BNF_FP.fp_result * local_theory
    5.10  end;
    5.11  
    5.12  structure BNF_GFP : BNF_GFP =
    5.13 @@ -54,7 +55,7 @@
    5.14       ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
    5.15  
    5.16  (*all BNFs have the same lives*)
    5.17 -fun construct_gfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
    5.18 +fun construct_gfp mixfixes resBs bs set_bss (resDs, Dss) bnfs lthy =
    5.19    let
    5.20      val timer = time (Timer.startRealTimer ());
    5.21  
    5.22 @@ -2894,11 +2895,12 @@
    5.23          val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs);
    5.24  
    5.25          val (Jbnfs, lthy) =
    5.26 -          fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn (thms, wits) => fn lthy =>
    5.27 -            bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads)
    5.28 +          fold_map7 (fn tacs => fn b => fn set_bs => fn mapx => fn sets => fn T =>
    5.29 +              fn (thms, wits) => fn lthy =>
    5.30 +            bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) set_bs
    5.31                (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
    5.32              |> register_bnf (Local_Theory.full_name lthy b))
    5.33 -          tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
    5.34 +          tacss bs set_bss fs_maps setss_by_bnf Ts all_witss lthy;
    5.35  
    5.36          val fold_maps = fold_thms lthy (map (fn bnf =>
    5.37            mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs);
     6.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 13:16:20 2013 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 13:16:20 2013 +0200
     6.3 @@ -9,7 +9,8 @@
     6.4  signature BNF_LFP =
     6.5  sig
     6.6    val construct_lfp: mixfix list -> (string * sort) list option -> binding list ->
     6.7 -    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory
     6.8 +    binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     6.9 +    BNF_FP.fp_result * local_theory
    6.10  end;
    6.11  
    6.12  structure BNF_LFP : BNF_LFP =
    6.13 @@ -25,7 +26,7 @@
    6.14  open BNF_LFP_Tactics
    6.15  
    6.16  (*all BNFs have the same lives*)
    6.17 -fun construct_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
    6.18 +fun construct_lfp mixfixes resBs bs set_bss (resDs, Dss) bnfs lthy =
    6.19    let
    6.20      val timer = time (Timer.startRealTimer ());
    6.21  
    6.22 @@ -1733,11 +1734,12 @@
    6.23          fun wit_tac _ = mk_wit_tac n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
    6.24  
    6.25          val (Ibnfs, lthy) =
    6.26 -          fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn wits => fn lthy =>
    6.27 -            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads)
    6.28 +          fold_map7 (fn tacs => fn b => fn set_bs => fn mapx => fn sets => fn T => fn wits =>
    6.29 +              fn lthy =>
    6.30 +            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) set_bs
    6.31                (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
    6.32              |> register_bnf (Local_Theory.full_name lthy b))
    6.33 -          tacss bs fs_maps setss_by_bnf Ts ctor_witss lthy;
    6.34 +          tacss bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
    6.35  
    6.36          val fold_maps = fold_thms lthy (map (fn bnf =>
    6.37            mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Ibnfs);
     7.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 13:16:20 2013 +0200
     7.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 13:16:20 2013 +0200
     7.3 @@ -43,6 +43,7 @@
     7.4    val splice: 'a list -> 'a list -> 'a list
     7.5    val transpose: 'a list list -> 'a list list
     7.6    val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
     7.7 +  val pad_list: 'a -> int -> 'a list -> 'a list
     7.8  
     7.9    val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
    7.10    val mk_TFrees: int -> Proof.context -> typ list * Proof.context
    7.11 @@ -616,6 +617,8 @@
    7.12        map (f false) negs @ [f true pos]
    7.13      end;
    7.14  
    7.15 +fun pad_list x n xs = xs @ replicate (n - length xs) x;
    7.16 +
    7.17  fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
    7.18  
    7.19  fun is_triv_implies thm =
     8.1 --- a/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Apr 24 13:16:20 2013 +0200
     8.2 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Apr 24 13:16:20 2013 +0200
     8.3 @@ -65,8 +65,6 @@
     8.4  val safe_elim_attrs = @{attributes [elim!]};
     8.5  val simp_attrs = @{attributes [simp]};
     8.6  
     8.7 -fun pad_list x n xs = xs @ replicate (n - length xs) x;
     8.8 -
     8.9  fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys)));
    8.10  
    8.11  fun mk_half_pairss' _ ([], []) = []