moved code around
authorblanchet
Thu Sep 04 09:02:43 2014 +0200 (2014-09-04)
changeset 5818095397823f39e
parent 58179 2de7b0313de3
child 58181 6d527272f7b2
moved code around
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 04 09:02:43 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 04 09:02:43 2014 +0200
     1.3 @@ -8,13 +8,40 @@
     1.4  
     1.5  signature BNF_FP_DEF_SUGAR =
     1.6  sig
     1.7 -  val fp_sugar_of: Proof.context -> string -> BNF_FP_Util.fp_sugar option
     1.8 -  val fp_sugar_of_global: theory -> string -> BNF_FP_Util.fp_sugar option
     1.9 -  val fp_sugars_of: Proof.context -> BNF_FP_Util.fp_sugar list
    1.10 -  val fp_sugars_of_global: theory -> BNF_FP_Util.fp_sugar list
    1.11 -  val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list -> theory -> theory) ->
    1.12 -    (BNF_FP_Util.fp_sugar list -> local_theory -> local_theory)-> theory -> theory
    1.13 -  val register_fp_sugars: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory
    1.14 +  type fp_sugar =
    1.15 +    {T: typ,
    1.16 +     BT: typ,
    1.17 +     X: typ,
    1.18 +     fp: BNF_Util.fp_kind,
    1.19 +     fp_res_index: int,
    1.20 +     fp_res: BNF_FP_Util.fp_result,
    1.21 +     pre_bnf: BNF_Def.bnf,
    1.22 +     absT_info: BNF_Comp.absT_info,
    1.23 +     fp_nesting_bnfs: BNF_Def.bnf list,
    1.24 +     live_nesting_bnfs: BNF_Def.bnf list,
    1.25 +     ctrXs_Tss: typ list list,
    1.26 +     ctr_defs: thm list,
    1.27 +     ctr_sugar: Ctr_Sugar.ctr_sugar,
    1.28 +     co_rec: term,
    1.29 +     co_rec_def: thm,
    1.30 +     maps: thm list,
    1.31 +     common_co_inducts: thm list,
    1.32 +     co_inducts: thm list,
    1.33 +     co_rec_thms: thm list,
    1.34 +     co_rec_discs: thm list,
    1.35 +     co_rec_selss: thm list list,
    1.36 +     rel_injects: thm list,
    1.37 +     rel_distincts: thm list};
    1.38 +
    1.39 +  val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
    1.40 +  val transfer_fp_sugar: theory -> fp_sugar -> fp_sugar
    1.41 +  val fp_sugar_of: Proof.context -> string -> fp_sugar option
    1.42 +  val fp_sugar_of_global: theory -> string -> fp_sugar option
    1.43 +  val fp_sugars_of: Proof.context -> fp_sugar list
    1.44 +  val fp_sugars_of_global: theory -> fp_sugar list
    1.45 +  val fp_sugar_interpretation: (fp_sugar list -> theory -> theory) ->
    1.46 +    (fp_sugar list -> local_theory -> local_theory)-> theory -> theory
    1.47 +  val register_fp_sugars: fp_sugar list -> local_theory -> local_theory
    1.48  
    1.49    val co_induct_of: 'a list -> 'a
    1.50    val strong_co_induct_of: 'a list -> 'a
    1.51 @@ -111,6 +138,60 @@
    1.52  val set_inductN = "set_induct";
    1.53  val set_selN = "set_sel";
    1.54  
    1.55 +type fp_sugar =
    1.56 +  {T: typ,
    1.57 +   BT: typ,
    1.58 +   X: typ,
    1.59 +   fp: fp_kind,
    1.60 +   fp_res_index: int,
    1.61 +   fp_res: fp_result,
    1.62 +   pre_bnf: bnf,
    1.63 +   absT_info: absT_info,
    1.64 +   fp_nesting_bnfs: bnf list,
    1.65 +   live_nesting_bnfs: bnf list,
    1.66 +   ctrXs_Tss: typ list list,
    1.67 +   ctr_defs: thm list,
    1.68 +   ctr_sugar: Ctr_Sugar.ctr_sugar,
    1.69 +   co_rec: term,
    1.70 +   co_rec_def: thm,
    1.71 +   maps: thm list,
    1.72 +   common_co_inducts: thm list,
    1.73 +   co_inducts: thm list,
    1.74 +   co_rec_thms: thm list,
    1.75 +   co_rec_discs: thm list,
    1.76 +   co_rec_selss: thm list list,
    1.77 +   rel_injects: thm list,
    1.78 +   rel_distincts: thm list};
    1.79 +
    1.80 +fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
    1.81 +    live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
    1.82 +    co_inducts, co_rec_thms, co_rec_discs, co_rec_selss, rel_injects, rel_distincts} : fp_sugar) =
    1.83 +  {T = Morphism.typ phi T,
    1.84 +   BT = Morphism.typ phi BT,
    1.85 +   X = Morphism.typ phi X,
    1.86 +   fp = fp,
    1.87 +   fp_res = morph_fp_result phi fp_res,
    1.88 +   fp_res_index = fp_res_index,
    1.89 +   pre_bnf = morph_bnf phi pre_bnf,
    1.90 +   absT_info = morph_absT_info phi absT_info,
    1.91 +   fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs,
    1.92 +   live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
    1.93 +   ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
    1.94 +   ctr_defs = map (Morphism.thm phi) ctr_defs,
    1.95 +   ctr_sugar = morph_ctr_sugar phi ctr_sugar,
    1.96 +   co_rec = Morphism.term phi co_rec,
    1.97 +   co_rec_def = Morphism.thm phi co_rec_def,
    1.98 +   maps = map (Morphism.thm phi) maps,
    1.99 +   common_co_inducts = map (Morphism.thm phi) common_co_inducts,
   1.100 +   co_inducts = map (Morphism.thm phi) co_inducts,
   1.101 +   co_rec_thms = map (Morphism.thm phi) co_rec_thms,
   1.102 +   co_rec_discs = map (Morphism.thm phi) co_rec_discs,
   1.103 +   co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss,
   1.104 +   rel_injects = map (Morphism.thm phi) rel_injects,
   1.105 +   rel_distincts = map (Morphism.thm phi) rel_distincts};
   1.106 +
   1.107 +val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism;
   1.108 +
   1.109  structure Data = Generic_Data
   1.110  (
   1.111    type T = fp_sugar Symtab.table;
   1.112 @@ -119,30 +200,6 @@
   1.113    fun merge data : T = Symtab.merge (K true) data;
   1.114  );
   1.115  
   1.116 -fun zipping_map f =
   1.117 -  let
   1.118 -    fun zmap _ [] = []
   1.119 -      | zmap xs (y :: ys) = f (xs, y, ys) :: zmap (xs @ [y]) ys
   1.120 -  in zmap [] end;
   1.121 -
   1.122 -
   1.123 -fun choose_binary_fun fs AB =
   1.124 -  find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs;
   1.125 -fun build_binary_fun_app fs t u =
   1.126 -  Option.map (rapp u o rapp t) (choose_binary_fun fs (fastype_of t, fastype_of u));
   1.127 -
   1.128 -fun build_the_rel rel_table ctxt Rs Ts A B =
   1.129 -  build_rel rel_table ctxt Ts (the o choose_binary_fun Rs) (A, B);
   1.130 -fun build_rel_app ctxt Rs Ts t u =
   1.131 -  build_the_rel [] ctxt Rs Ts (fastype_of t) (fastype_of u) $ t $ u;
   1.132 -
   1.133 -fun mk_parametricity_goal ctxt Rs t u =
   1.134 -  let val prem = build_the_rel [] ctxt Rs [] (fastype_of t) (fastype_of u) in
   1.135 -    HOLogic.mk_Trueprop (prem $ t $ u)
   1.136 -  end;
   1.137 -
   1.138 -val name_of_set = name_of_const "set";
   1.139 -
   1.140  fun fp_sugar_of_generic context =
   1.141    Option.map (transfer_fp_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context)
   1.142  
   1.143 @@ -216,6 +273,29 @@
   1.144      map (fn (base, full) => if member (op =) dups base then underscore full else base) ps
   1.145    end;
   1.146  
   1.147 +fun zipper_map f =
   1.148 +  let
   1.149 +    fun zed _ [] = []
   1.150 +      | zed xs (y :: ys) = f (xs, y, ys) :: zed (xs @ [y]) ys
   1.151 +  in zed [] end;
   1.152 +
   1.153 +fun choose_binary_fun fs AB =
   1.154 +  find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs;
   1.155 +fun build_binary_fun_app fs t u =
   1.156 +  Option.map (rapp u o rapp t) (choose_binary_fun fs (fastype_of t, fastype_of u));
   1.157 +
   1.158 +fun build_the_rel rel_table ctxt Rs Ts A B =
   1.159 +  build_rel rel_table ctxt Ts (the o choose_binary_fun Rs) (A, B);
   1.160 +fun build_rel_app ctxt Rs Ts t u =
   1.161 +  build_the_rel [] ctxt Rs Ts (fastype_of t) (fastype_of u) $ t $ u;
   1.162 +
   1.163 +fun mk_parametricity_goal ctxt Rs t u =
   1.164 +  let val prem = build_the_rel [] ctxt Rs [] (fastype_of t) (fastype_of u) in
   1.165 +    HOLogic.mk_Trueprop (prem $ t $ u)
   1.166 +  end;
   1.167 +
   1.168 +val name_of_set = name_of_const "set";
   1.169 +
   1.170  val mp_conj = @{thm mp_conj};
   1.171  
   1.172  val fundefcong_attrs = @{attributes [fundef_cong]};
   1.173 @@ -1547,7 +1627,7 @@
   1.174                                  val (args, names_lthy) =
   1.175                                    mk_Frees "z" (binder_types (fastype_of ctr)) names_lthy;
   1.176                                in
   1.177 -                                flat (zipping_map (fn (prev_args, arg, next_args) =>
   1.178 +                                flat (zipper_map (fn (prev_args, arg, next_args) =>
   1.179                                    let
   1.180                                      val (args_with_elem, args_without_elem) =
   1.181                                        if fastype_of arg = A then
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 04 09:02:43 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 04 09:02:43 2014 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  signature BNF_FP_N2M =
     2.5  sig
     2.6    val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
     2.7 -    BNF_FP_Util.fp_sugar list -> binding list -> (string * sort) list ->
     2.8 +    BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list ->
     2.9      typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
    2.10      BNF_FP_Util.fp_result * local_theory
    2.11  end;
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Thu Sep 04 09:02:43 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Thu Sep 04 09:02:43 2014 +0200
     3.3 @@ -12,13 +12,13 @@
     3.4    val dest_map: Proof.context -> string -> term -> term * term list
     3.5  
     3.6    val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
     3.7 -    term list list list list -> BNF_FP_Util.fp_sugar list -> local_theory ->
     3.8 -    (BNF_FP_Util.fp_sugar list
     3.9 +    term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
    3.10 +    (BNF_FP_Def_Sugar.fp_sugar list
    3.11       * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    3.12      * local_theory
    3.13    val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
    3.14      (term * term list list) list list -> local_theory ->
    3.15 -    (typ list * int list * BNF_FP_Util.fp_sugar list
    3.16 +    (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
    3.17       * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    3.18      * local_theory
    3.19  end;
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 04 09:02:43 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 04 09:02:43 2014 +0200
     4.3 @@ -30,34 +30,6 @@
     4.4  
     4.5    val morph_fp_result: morphism -> fp_result -> fp_result
     4.6  
     4.7 -  type fp_sugar =
     4.8 -    {T: typ,
     4.9 -     BT: typ,
    4.10 -     X: typ,
    4.11 -     fp: BNF_Util.fp_kind,
    4.12 -     fp_res_index: int,
    4.13 -     fp_res: fp_result,
    4.14 -     pre_bnf: BNF_Def.bnf,
    4.15 -     absT_info: BNF_Comp.absT_info,
    4.16 -     fp_nesting_bnfs: BNF_Def.bnf list,
    4.17 -     live_nesting_bnfs: BNF_Def.bnf list,
    4.18 -     ctrXs_Tss: typ list list,
    4.19 -     ctr_defs: thm list,
    4.20 -     ctr_sugar: Ctr_Sugar.ctr_sugar,
    4.21 -     co_rec: term,
    4.22 -     co_rec_def: thm,
    4.23 -     maps: thm list,
    4.24 -     common_co_inducts: thm list,
    4.25 -     co_inducts: thm list,
    4.26 -     co_rec_thms: thm list,
    4.27 -     co_rec_discs: thm list,
    4.28 -     co_rec_selss: thm list list,
    4.29 -     rel_injects: thm list,
    4.30 -     rel_distincts: thm list};
    4.31 -
    4.32 -  val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
    4.33 -  val transfer_fp_sugar: theory -> fp_sugar -> fp_sugar
    4.34 -
    4.35    val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
    4.36  
    4.37    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
    4.38 @@ -265,60 +237,6 @@
    4.39     rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
    4.40     dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms}; (* No idea of what this is doing... *)
    4.41  
    4.42 -type fp_sugar =
    4.43 -  {T: typ,
    4.44 -   BT: typ,
    4.45 -   X: typ,
    4.46 -   fp: fp_kind,
    4.47 -   fp_res_index: int,
    4.48 -   fp_res: fp_result,
    4.49 -   pre_bnf: bnf,
    4.50 -   absT_info: absT_info,
    4.51 -   fp_nesting_bnfs: bnf list,
    4.52 -   live_nesting_bnfs: bnf list,
    4.53 -   ctrXs_Tss: typ list list,
    4.54 -   ctr_defs: thm list,
    4.55 -   ctr_sugar: Ctr_Sugar.ctr_sugar,
    4.56 -   co_rec: term,
    4.57 -   co_rec_def: thm,
    4.58 -   maps: thm list,
    4.59 -   common_co_inducts: thm list,
    4.60 -   co_inducts: thm list,
    4.61 -   co_rec_thms: thm list,
    4.62 -   co_rec_discs: thm list,
    4.63 -   co_rec_selss: thm list list,
    4.64 -   rel_injects: thm list,
    4.65 -   rel_distincts: thm list};
    4.66 -
    4.67 -fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
    4.68 -    live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
    4.69 -    co_inducts, co_rec_thms, co_rec_discs, co_rec_selss, rel_injects, rel_distincts} : fp_sugar) =
    4.70 -  {T = Morphism.typ phi T,
    4.71 -   BT = Morphism.typ phi BT,
    4.72 -   X = Morphism.typ phi X,
    4.73 -   fp = fp,
    4.74 -   fp_res = morph_fp_result phi fp_res,
    4.75 -   fp_res_index = fp_res_index,
    4.76 -   pre_bnf = morph_bnf phi pre_bnf,
    4.77 -   absT_info = morph_absT_info phi absT_info,
    4.78 -   fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs,
    4.79 -   live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
    4.80 -   ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
    4.81 -   ctr_defs = map (Morphism.thm phi) ctr_defs,
    4.82 -   ctr_sugar = morph_ctr_sugar phi ctr_sugar,
    4.83 -   co_rec = Morphism.term phi co_rec,
    4.84 -   co_rec_def = Morphism.thm phi co_rec_def,
    4.85 -   maps = map (Morphism.thm phi) maps,
    4.86 -   common_co_inducts = map (Morphism.thm phi) common_co_inducts,
    4.87 -   co_inducts = map (Morphism.thm phi) co_inducts,
    4.88 -   co_rec_thms = map (Morphism.thm phi) co_rec_thms,
    4.89 -   co_rec_discs = map (Morphism.thm phi) co_rec_discs,
    4.90 -   co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss,
    4.91 -   rel_injects = map (Morphism.thm phi) rel_injects,
    4.92 -   rel_distincts = map (Morphism.thm phi) rel_distincts};
    4.93 -
    4.94 -val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism;
    4.95 -
    4.96  fun time ctxt timer msg = (if Config.get ctxt bnf_timing
    4.97    then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
    4.98      "ms")
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Sep 04 09:02:43 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Sep 04 09:02:43 2014 +0200
     5.3 @@ -19,7 +19,6 @@
     5.4  open BNF_Util
     5.5  open BNF_Tactics
     5.6  open BNF_Def
     5.7 -open BNF_FP_Util
     5.8  open BNF_FP_Def_Sugar
     5.9  
    5.10  val size_N = "size_"
    5.11 @@ -63,7 +62,7 @@
    5.12  fun mk_unabs_def_unused_0 n =
    5.13    funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong);
    5.14  
    5.15 -val rec_o_map_simp_thms =
    5.16 +val rec_o_map_simps =
    5.17    @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod
    5.18        BNF_Composition.id_bnf_comp_def};
    5.19  
    5.20 @@ -73,15 +72,15 @@
    5.21    HEADGOAL (rtac (ctor_rec_o_map RS trans) THEN'
    5.22      CONVERSION Thm.eta_long_conversion THEN'
    5.23      asm_simp_tac (ss_only (pre_map_defs @
    5.24 -        distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simp_thms)
    5.25 +        distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simps)
    5.26        ctxt));
    5.27  
    5.28 -val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
    5.29 +val size_o_map_simps = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
    5.30  
    5.31  fun mk_size_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
    5.32    unfold_thms_tac ctxt [size_def] THEN
    5.33    HEADGOAL (rtac (rec_o_map RS trans) THEN'
    5.34 -    asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simp_thms) ctxt)) THEN
    5.35 +    asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simps) ctxt)) THEN
    5.36    IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
    5.37  
    5.38  fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,