# HG changeset patch # User blanchet # Date 1398241407 -7200 # Node ID 1f9ab71d43a5b467ff6b1e4b0249cbf646e9e597 # Parent 16e1fa9d094fd3627c786f06319de2934811b75d no need to make 'size' generation an interpretation -- overkill diff -r 16e1fa9d094f -r 1f9ab71d43a5 src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/BNF_FP_Base.thy Wed Apr 23 10:23:27 2014 +0200 @@ -163,11 +163,58 @@ lemma vimage2p_comp: "vimage2p (f1 \ f2) (g1 \ g2) = vimage2p f2 g2 \ vimage2p f1 g1" unfolding fun_eq_iff vimage2p_def o_apply by simp +lemma fun_cong_unused_0: "f = (\x. g) \ f (\x. 0) = g" + by (erule arg_cong) + +lemma snd_o_convol: "(snd \ (\x. (f x, g x))) = g" + by (rule ext) simp + +lemma inj_on_convol_id: "inj_on (\x. (x, f x)) X" + unfolding inj_on_def by simp + +lemma case_prod_app: "case_prod f x y = case_prod (\l r. f l r y) x" + by (case_tac x) simp + +lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \ f) (r \ g) x" + by (case_tac x) simp+ + +lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\l r. h (f l) (g r)) x" + by (case_tac x) simp+ + +lemma prod_inj_map: "inj f \ inj g \ inj (map_prod f g)" + by (simp add: inj_on_def) + + ML_file "Tools/BNF/bnf_fp_util.ML" ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" +ML_file "Tools/BNF/bnf_lfp_size.ML" ML_file "Tools/BNF/bnf_fp_def_sugar.ML" ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" ML_file "Tools/BNF/bnf_fp_n2m.ML" ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML" +ML_file "Tools/Function/size.ML" +setup Size.setup + +lemma size_bool[code]: "size (b\bool) = 0" + by (cases b) auto + +lemma nat_size[simp, code]: "size (n\nat) = n" + by (induct n) simp_all + +declare prod.size[no_atp] + +lemma sum_size_o_map: "sum_size g1 g2 \ map_sum f1 f2 = sum_size (g1 \ f1) (g2 \ f2)" + by (rule ext) (case_tac x, auto) + +lemma prod_size_o_map: "prod_size g1 g2 \ map_prod f1 f2 = prod_size (g1 \ f1) (g2 \ f2)" + by (rule ext) auto + +setup {* +BNF_LFP_Size.register_size @{type_name sum} @{const_name sum_size} @{thms sum.size} + @{thms sum_size_o_map} +#> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size} + @{thms prod_size_o_map} +*} + end diff -r 16e1fa9d094f -r 1f9ab71d43a5 src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:27 2014 +0200 @@ -186,61 +186,14 @@ lemma ssubst_Pair_rhs: "\(r, s) \ R; s' = s\ \ (r, s') \ R" by (rule ssubst) -lemma fun_cong_unused_0: "f = (\x. g) \ f (\x. 0) = g" - by (erule arg_cong) - -lemma snd_o_convol: "(snd \ (\x. (f x, g x))) = g" - by (rule ext) simp - -lemma inj_on_convol_id: "inj_on (\x. (x, f x)) X" - unfolding inj_on_def by simp - -lemma case_prod_app: "case_prod f x y = case_prod (\l r. f l r y) x" - by (case_tac x) simp - -lemma case_sum_o_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \ f) (r \ g) x" - by (case_tac x) simp+ - -lemma case_prod_o_map_prod: "case_prod h (map_prod f g x) = case_prod (\l r. h (f l) (g r)) x" - by (case_tac x) simp+ - -lemma prod_inj_map: "inj f \ inj g \ inj (map_prod f g)" - by (simp add: inj_on_def) - ML_file "Tools/BNF/bnf_lfp_util.ML" ML_file "Tools/BNF/bnf_lfp_tactics.ML" ML_file "Tools/BNF/bnf_lfp.ML" ML_file "Tools/BNF/bnf_lfp_compat.ML" ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" - -subsection {* Size of a datatype value *} - -ML_file "Tools/BNF/bnf_lfp_size.ML" -ML_file "Tools/Function/size.ML" -setup Size.setup - -lemma size_bool[code]: "size (b\bool) = 0" - by (cases b) auto - -lemma nat_size[simp, code]: "size (n\nat) = n" - by (induct n) simp_all - -declare prod.size[no_atp] - -lemma sum_size_o_map: "sum_size g1 g2 \ map_sum f1 f2 = sum_size (g1 \ f1) (g2 \ f2)" - by (rule ext) (case_tac x, auto) - -lemma prod_size_o_map: "prod_size g1 g2 \ map_prod f1 f2 = prod_size (g1 \ f1) (g2 \ f2)" - by (rule ext) auto - -setup {* -BNF_LFP_Size.register_size @{type_name sum} @{const_name sum_size} @{thms sum.size} - @{thms sum_size_o_map} -#> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size} - @{thms prod_size_o_map} -*} - hide_fact (open) id_transfer +datatype_new 'a x = X 'a + end diff -r 16e1fa9d094f -r 1f9ab71d43a5 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 10:23:27 2014 +0200 @@ -7,37 +7,10 @@ signature BNF_FP_DEF_SUGAR = sig - 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, - nested_bnfs: BNF_Def.bnf list, - 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, - disc_co_recs: thm list, - sel_co_recss: thm list list, - rel_injects: thm list, - rel_distincts: thm list}; - - val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar - val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar - val fp_sugar_of: Proof.context -> string -> fp_sugar option - val fp_sugars_of: Proof.context -> fp_sugar list - val fp_sugar_interpretation: (fp_sugar list -> theory -> theory) -> theory -> theory - val register_fp_sugars: fp_sugar list -> local_theory -> local_theory + val fp_sugar_of: Proof.context -> string -> BNF_FP_Util.fp_sugar option + val fp_sugars_of: Proof.context -> BNF_FP_Util.fp_sugar list + val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list -> theory -> theory) -> theory -> theory + val register_fp_sugars: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory val co_induct_of: 'a list -> 'a val strong_co_induct_of: 'a list -> 'a @@ -121,63 +94,10 @@ open BNF_Def open BNF_FP_Util open BNF_FP_Def_Sugar_Tactics +open BNF_LFP_Size val EqN = "Eq_"; -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, - nested_bnfs: bnf list, - 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, - disc_co_recs: thm list, - sel_co_recss: 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, nested_bnfs, - nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts, - co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, 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, - nested_bnfs = map (morph_bnf phi) nested_bnfs, - nesting_bnfs = map (morph_bnf phi) 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, - disc_co_recs = map (Morphism.thm phi) disc_co_recs, - sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss, - 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 o Proof_Context.theory_of; - structure Data = Generic_Data ( type T = fp_sugar Symtab.table; @@ -211,11 +131,12 @@ val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path; -fun register_fp_sugars fp_sugars = +fun register_fp_sugars (fp_sugars as {fp, ...} :: _) = fold (fn fp_sugar as {T = Type (s, _), ...} => Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar)))) fp_sugars + #> Local_Theory.background_theory (generate_lfp_size fp_sugars) #> Local_Theory.background_theory (FP_Sugar_Interpretation.data fp_sugars); fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res diff -r 16e1fa9d094f -r 1f9ab71d43a5 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 23 10:23:27 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_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list -> + BNF_FP_Util.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 16e1fa9d094f -r 1f9ab71d43a5 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Apr 23 10:23:27 2014 +0200 @@ -11,13 +11,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_Def_Sugar.fp_sugar list -> local_theory -> - (BNF_FP_Def_Sugar.fp_sugar list + term list list list list -> BNF_FP_Util.fp_sugar list -> local_theory -> + (BNF_FP_Util.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_Def_Sugar.fp_sugar list + (typ list * int list * BNF_FP_Util.fp_sugar list * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) * local_theory end; diff -r 16e1fa9d094f -r 1f9ab71d43a5 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Apr 23 10:23:27 2014 +0200 @@ -28,6 +28,34 @@ 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, + nested_bnfs: BNF_Def.bnf list, + 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, + disc_co_recs: thm list, + sel_co_recss: thm list list, + rel_injects: thm list, + rel_distincts: thm list}; + + val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar + val transfer_fp_sugar: Proof.context -> 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 @@ -184,6 +212,7 @@ structure BNF_FP_Util : BNF_FP_UTIL = struct +open Ctr_Sugar open BNF_Comp open BNF_Def open BNF_Util @@ -226,6 +255,60 @@ xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm}; +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, + nested_bnfs: bnf list, + 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, + disc_co_recs: thm list, + sel_co_recss: 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, nested_bnfs, + nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts, + co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, 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, + nested_bnfs = map (morph_bnf phi) nested_bnfs, + nesting_bnfs = map (morph_bnf phi) 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, + disc_co_recs = map (Morphism.thm phi) disc_co_recs, + sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss, + 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 o Proof_Context.theory_of; + 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 16e1fa9d094f -r 1f9ab71d43a5 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:27 2014 +0200 @@ -9,6 +9,7 @@ sig val register_size: string -> string -> thm list -> thm list -> theory -> theory val lookup_size: theory -> string -> (string * (thm list * thm list)) option + val generate_lfp_size: BNF_FP_Util.fp_sugar list -> theory -> theory end; structure BNF_LFP_Size : BNF_LFP_SIZE = @@ -17,7 +18,7 @@ open BNF_Util open BNF_Tactics open BNF_Def -open BNF_FP_Def_Sugar +open BNF_FP_Util val size_N = "size_" @@ -53,8 +54,7 @@ funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong); val rec_o_map_simp_thms = - @{thms o_def id_apply case_prod_app case_sum_o_map_sum case_prod_o_map_prod - BNF_Comp.id_bnf_comp_def}; + @{thms o_def id_apply case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def}; fun mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map = unfold_thms_tac ctxt [rec_def] THEN @@ -71,7 +71,7 @@ asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simp_thms) ctxt)) THEN IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl)); -fun generate_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP, +fun generate_lfp_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP, fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs, nesting_bnfs, ...} : fp_sugar) :: _) thy = let @@ -335,8 +335,6 @@ Symtab.update_new (T_name, (size_name, (size_simps, flat size_o_map_thmss)))) T_names size_names) end - | generate_size _ thy = thy; - -val _ = Theory.setup (fp_sugar_interpretation generate_size); + | generate_lfp_size _ thy = thy; end;