# HG changeset patch # User blanchet # Date 1409814163 -7200 # Node ID 95397823f39eb0c93798020adf8e7d51ae93454f # Parent 2de7b0313de33f40f64db906d42ac5ee081d3a4d moved code around diff -r 2de7b0313de3 -r 95397823f39e src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 04 09:02:43 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 04 09:02:43 2014 +0200 @@ -8,13 +8,40 @@ signature BNF_FP_DEF_SUGAR = sig - val fp_sugar_of: Proof.context -> string -> BNF_FP_Util.fp_sugar option - val fp_sugar_of_global: theory -> string -> BNF_FP_Util.fp_sugar option - val fp_sugars_of: Proof.context -> BNF_FP_Util.fp_sugar list - val fp_sugars_of_global: theory -> BNF_FP_Util.fp_sugar list - val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list -> theory -> theory) -> - (BNF_FP_Util.fp_sugar list -> local_theory -> local_theory)-> theory -> theory - val register_fp_sugars: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory + type fp_sugar = + {T: typ, + BT: typ, + X: typ, + fp: BNF_Util.fp_kind, + fp_res_index: int, + fp_res: BNF_FP_Util.fp_result, + pre_bnf: BNF_Def.bnf, + absT_info: BNF_Comp.absT_info, + fp_nesting_bnfs: BNF_Def.bnf list, + live_nesting_bnfs: BNF_Def.bnf list, + ctrXs_Tss: typ list list, + ctr_defs: thm list, + ctr_sugar: Ctr_Sugar.ctr_sugar, + co_rec: term, + co_rec_def: thm, + maps: thm list, + common_co_inducts: thm list, + co_inducts: thm list, + co_rec_thms: thm list, + co_rec_discs: thm list, + co_rec_selss: thm list list, + rel_injects: thm list, + rel_distincts: thm list}; + + val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar + val transfer_fp_sugar: theory -> fp_sugar -> fp_sugar + val fp_sugar_of: Proof.context -> string -> fp_sugar option + val fp_sugar_of_global: theory -> string -> fp_sugar option + val fp_sugars_of: Proof.context -> fp_sugar list + val fp_sugars_of_global: theory -> fp_sugar list + val fp_sugar_interpretation: (fp_sugar list -> theory -> theory) -> + (fp_sugar list -> local_theory -> local_theory)-> theory -> theory + val register_fp_sugars: fp_sugar list -> local_theory -> local_theory val co_induct_of: 'a list -> 'a val strong_co_induct_of: 'a list -> 'a @@ -111,6 +138,60 @@ val set_inductN = "set_induct"; val set_selN = "set_sel"; +type fp_sugar = + {T: typ, + BT: typ, + X: typ, + fp: fp_kind, + fp_res_index: int, + fp_res: fp_result, + pre_bnf: bnf, + absT_info: absT_info, + fp_nesting_bnfs: bnf list, + live_nesting_bnfs: bnf list, + ctrXs_Tss: typ list list, + ctr_defs: thm list, + ctr_sugar: Ctr_Sugar.ctr_sugar, + co_rec: term, + co_rec_def: thm, + maps: thm list, + common_co_inducts: thm list, + co_inducts: thm list, + co_rec_thms: thm list, + co_rec_discs: thm list, + co_rec_selss: thm list list, + rel_injects: thm list, + rel_distincts: thm list}; + +fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs, + live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts, + co_inducts, co_rec_thms, co_rec_discs, co_rec_selss, rel_injects, rel_distincts} : fp_sugar) = + {T = Morphism.typ phi T, + BT = Morphism.typ phi BT, + X = Morphism.typ phi X, + fp = fp, + fp_res = morph_fp_result phi fp_res, + fp_res_index = fp_res_index, + pre_bnf = morph_bnf phi pre_bnf, + absT_info = morph_absT_info phi absT_info, + fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs, + live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs, + ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss, + ctr_defs = map (Morphism.thm phi) ctr_defs, + ctr_sugar = morph_ctr_sugar phi ctr_sugar, + co_rec = Morphism.term phi co_rec, + co_rec_def = Morphism.thm phi co_rec_def, + maps = map (Morphism.thm phi) maps, + common_co_inducts = map (Morphism.thm phi) common_co_inducts, + co_inducts = map (Morphism.thm phi) co_inducts, + co_rec_thms = map (Morphism.thm phi) co_rec_thms, + co_rec_discs = map (Morphism.thm phi) co_rec_discs, + co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss, + rel_injects = map (Morphism.thm phi) rel_injects, + rel_distincts = map (Morphism.thm phi) rel_distincts}; + +val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism; + structure Data = Generic_Data ( type T = fp_sugar Symtab.table; @@ -119,30 +200,6 @@ fun merge data : T = Symtab.merge (K true) data; ); -fun zipping_map f = - let - fun zmap _ [] = [] - | zmap xs (y :: ys) = f (xs, y, ys) :: zmap (xs @ [y]) ys - in zmap [] end; - - -fun choose_binary_fun fs AB = - find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs; -fun build_binary_fun_app fs t u = - Option.map (rapp u o rapp t) (choose_binary_fun fs (fastype_of t, fastype_of u)); - -fun build_the_rel rel_table ctxt Rs Ts A B = - build_rel rel_table ctxt Ts (the o choose_binary_fun Rs) (A, B); -fun build_rel_app ctxt Rs Ts t u = - build_the_rel [] ctxt Rs Ts (fastype_of t) (fastype_of u) $ t $ u; - -fun mk_parametricity_goal ctxt Rs t u = - let val prem = build_the_rel [] ctxt Rs [] (fastype_of t) (fastype_of u) in - HOLogic.mk_Trueprop (prem $ t $ u) - end; - -val name_of_set = name_of_const "set"; - fun fp_sugar_of_generic context = Option.map (transfer_fp_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context) @@ -216,6 +273,29 @@ map (fn (base, full) => if member (op =) dups base then underscore full else base) ps end; +fun zipper_map f = + let + fun zed _ [] = [] + | zed xs (y :: ys) = f (xs, y, ys) :: zed (xs @ [y]) ys + in zed [] end; + +fun choose_binary_fun fs AB = + find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs; +fun build_binary_fun_app fs t u = + Option.map (rapp u o rapp t) (choose_binary_fun fs (fastype_of t, fastype_of u)); + +fun build_the_rel rel_table ctxt Rs Ts A B = + build_rel rel_table ctxt Ts (the o choose_binary_fun Rs) (A, B); +fun build_rel_app ctxt Rs Ts t u = + build_the_rel [] ctxt Rs Ts (fastype_of t) (fastype_of u) $ t $ u; + +fun mk_parametricity_goal ctxt Rs t u = + let val prem = build_the_rel [] ctxt Rs [] (fastype_of t) (fastype_of u) in + HOLogic.mk_Trueprop (prem $ t $ u) + end; + +val name_of_set = name_of_const "set"; + val mp_conj = @{thm mp_conj}; val fundefcong_attrs = @{attributes [fundef_cong]}; @@ -1547,7 +1627,7 @@ val (args, names_lthy) = mk_Frees "z" (binder_types (fastype_of ctr)) names_lthy; in - flat (zipping_map (fn (prev_args, arg, next_args) => + flat (zipper_map (fn (prev_args, arg, next_args) => let val (args_with_elem, args_without_elem) = if fastype_of arg = A then diff -r 2de7b0313de3 -r 95397823f39e src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Sep 04 09:02:43 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Sep 04 09:02:43 2014 +0200 @@ -8,7 +8,7 @@ signature BNF_FP_N2M = sig val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list -> - BNF_FP_Util.fp_sugar list -> binding list -> (string * sort) list -> + BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory end; diff -r 2de7b0313de3 -r 95397823f39e src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Sep 04 09:02:43 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Sep 04 09:02:43 2014 +0200 @@ -12,13 +12,13 @@ val dest_map: Proof.context -> string -> term -> term * term list val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list -> - term list list list list -> BNF_FP_Util.fp_sugar list -> local_theory -> - (BNF_FP_Util.fp_sugar list + term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory -> + (BNF_FP_Def_Sugar.fp_sugar list * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) * local_theory val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> term list -> (term * term list list) list list -> local_theory -> - (typ list * int list * BNF_FP_Util.fp_sugar list + (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) * local_theory end; diff -r 2de7b0313de3 -r 95397823f39e src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 04 09:02:43 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 04 09:02:43 2014 +0200 @@ -30,34 +30,6 @@ val morph_fp_result: morphism -> fp_result -> fp_result - type fp_sugar = - {T: typ, - BT: typ, - X: typ, - fp: BNF_Util.fp_kind, - fp_res_index: int, - fp_res: fp_result, - pre_bnf: BNF_Def.bnf, - absT_info: BNF_Comp.absT_info, - fp_nesting_bnfs: BNF_Def.bnf list, - live_nesting_bnfs: BNF_Def.bnf list, - ctrXs_Tss: typ list list, - ctr_defs: thm list, - ctr_sugar: Ctr_Sugar.ctr_sugar, - co_rec: term, - co_rec_def: thm, - maps: thm list, - common_co_inducts: thm list, - co_inducts: thm list, - co_rec_thms: thm list, - co_rec_discs: thm list, - co_rec_selss: thm list list, - rel_injects: thm list, - rel_distincts: thm list}; - - val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar - val transfer_fp_sugar: theory -> fp_sugar -> fp_sugar - val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list @@ -265,60 +237,6 @@ rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm, dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms}; (* No idea of what this is doing... *) -type fp_sugar = - {T: typ, - BT: typ, - X: typ, - fp: fp_kind, - fp_res_index: int, - fp_res: fp_result, - pre_bnf: bnf, - absT_info: absT_info, - fp_nesting_bnfs: bnf list, - live_nesting_bnfs: bnf list, - ctrXs_Tss: typ list list, - ctr_defs: thm list, - ctr_sugar: Ctr_Sugar.ctr_sugar, - co_rec: term, - co_rec_def: thm, - maps: thm list, - common_co_inducts: thm list, - co_inducts: thm list, - co_rec_thms: thm list, - co_rec_discs: thm list, - co_rec_selss: thm list list, - rel_injects: thm list, - rel_distincts: thm list}; - -fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs, - live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts, - co_inducts, co_rec_thms, co_rec_discs, co_rec_selss, rel_injects, rel_distincts} : fp_sugar) = - {T = Morphism.typ phi T, - BT = Morphism.typ phi BT, - X = Morphism.typ phi X, - fp = fp, - fp_res = morph_fp_result phi fp_res, - fp_res_index = fp_res_index, - pre_bnf = morph_bnf phi pre_bnf, - absT_info = morph_absT_info phi absT_info, - fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs, - live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs, - ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss, - ctr_defs = map (Morphism.thm phi) ctr_defs, - ctr_sugar = morph_ctr_sugar phi ctr_sugar, - co_rec = Morphism.term phi co_rec, - co_rec_def = Morphism.thm phi co_rec_def, - maps = map (Morphism.thm phi) maps, - common_co_inducts = map (Morphism.thm phi) common_co_inducts, - co_inducts = map (Morphism.thm phi) co_inducts, - co_rec_thms = map (Morphism.thm phi) co_rec_thms, - co_rec_discs = map (Morphism.thm phi) co_rec_discs, - co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss, - rel_injects = map (Morphism.thm phi) rel_injects, - rel_distincts = map (Morphism.thm phi) rel_distincts}; - -val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism; - fun time ctxt timer msg = (if Config.get ctxt bnf_timing then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ "ms") diff -r 2de7b0313de3 -r 95397823f39e src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 04 09:02:43 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 04 09:02:43 2014 +0200 @@ -19,7 +19,6 @@ open BNF_Util open BNF_Tactics open BNF_Def -open BNF_FP_Util open BNF_FP_Def_Sugar val size_N = "size_" @@ -63,7 +62,7 @@ fun mk_unabs_def_unused_0 n = funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong); -val rec_o_map_simp_thms = +val rec_o_map_simps = @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod BNF_Composition.id_bnf_comp_def}; @@ -73,15 +72,15 @@ HEADGOAL (rtac (ctor_rec_o_map RS trans) THEN' CONVERSION Thm.eta_long_conversion THEN' asm_simp_tac (ss_only (pre_map_defs @ - distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simp_thms) + distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simps) ctxt)); -val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]}; +val size_o_map_simps = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]}; fun mk_size_o_map_tac ctxt size_def rec_o_map inj_maps size_maps = unfold_thms_tac ctxt [size_def] THEN HEADGOAL (rtac (rec_o_map RS trans) THEN' - asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simp_thms) ctxt)) THEN + asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simps) ctxt)) THEN IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl)); fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,