# HG changeset patch # User blanchet # Date 1367490902 -7200 # Node ID 09d24ea3f140bb593ee3719590e649e15dbd4ed5 # Parent 7a08fe1e19b159616e8ee29314d428fdbfdc9a35 rationalized data structure diff -r 7a08fe1e19b1 -r 09d24ea3f140 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu May 02 11:58:18 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu May 02 12:35:02 2013 +0200 @@ -8,7 +8,8 @@ signature BNF_FP_DEF_SUGAR = sig type fp_sugar = - {lfp: bool, + {T: typ, + lfp: bool, index: int, pre_bnfs: BNF_Def.bnf list, fp_res: BNF_FP_Util.fp_result, @@ -73,7 +74,8 @@ val EqN = "Eq_"; type fp_sugar = - {lfp: bool, + {T: typ, + lfp: bool, index: int, pre_bnfs: bnf list, fp_res: fp_result, @@ -83,13 +85,13 @@ un_fold_thmss: thm list list, co_rec_thmss: thm list list}; -fun eq_fp_sugar ({lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, - {lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = - lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); +fun eq_fp_sugar ({T = T1, lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, + {T = T2, lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = + T1 = T2 andalso lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); -fun morph_fp_sugar phi {lfp, index, pre_bnfs, fp_res, ctr_sugars, un_folds, co_recs, un_fold_thmss, - co_rec_thmss} = - {lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, +fun morph_fp_sugar phi {T, lfp, index, pre_bnfs, fp_res, ctr_sugars, un_folds, co_recs, + un_fold_thmss, co_rec_thmss} = + {T = Morphism.typ phi T, lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, fp_res = morph_fp_result phi fp_res, ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, un_folds = map (Morphism.term phi) un_folds, co_recs = map (Morphism.term phi) co_recs, un_fold_thmss = map (map (Morphism.thm phi)) un_fold_thmss, @@ -109,13 +111,13 @@ Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); -fun register_fp_sugars lfp pre_bnfs (fp_res as {ctors, ...}) ctr_sugars un_folds co_recs +fun register_fp_sugars lfp pre_bnfs (fp_res as {Ts, ...}) ctr_sugars un_folds co_recs un_fold_thmss co_rec_thmss lthy = (0, lthy) - |> fold (fn ctor => fn (kk, lthy) => (kk + 1, - register_fp_sugar (fp_name_of_ctor ctor) {lfp = lfp, index = kk, - pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_sugars = ctr_sugars, un_folds = un_folds, - co_recs = co_recs, un_fold_thmss = un_fold_thmss, co_rec_thmss = co_rec_thmss} lthy)) ctors + |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, + register_fp_sugar s {T = T, lfp = lfp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res, + ctr_sugars = ctr_sugars, un_folds = un_folds, co_recs = co_recs, + un_fold_thmss = un_fold_thmss, co_rec_thmss = co_rec_thmss} lthy)) Ts |> snd; (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) @@ -904,7 +906,7 @@ val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss, - rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms}, lthy)) = + rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms, ...}, lthy)) = fp_bnf construct_fp fp_bs mixfixes map_bs rel_bs set_bss (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0; @@ -1315,7 +1317,7 @@ end; fun derive_and_note_coinduct_unfold_corec_thms_for_types - ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)), + ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)), (unfolds, corecs, unfold_defs, corec_defs)), lthy) = let val ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms, diff -r 7a08fe1e19b1 -r 09d24ea3f140 src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 02 11:58:18 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 02 12:35:02 2013 +0200 @@ -9,7 +9,8 @@ signature BNF_FP_UTIL = sig type fp_result = - {bnfs: BNF_Def.bnf list, + {Ts: typ list, + bnfs: BNF_Def.bnf list, ctors: term list, dtors: term list, folds: term list, @@ -25,7 +26,6 @@ fold_thms: thm list, rec_thms: thm list} - val fp_name_of_ctor: term -> string val morph_fp_result: morphism -> fp_result -> fp_result val eq_fp_result: fp_result * fp_result -> bool @@ -179,7 +179,8 @@ open BNF_Util type fp_result = - {bnfs: BNF_Def.bnf list, + {Ts: typ list, + bnfs: BNF_Def.bnf list, ctors: term list, dtors: term list, folds: term list, @@ -195,11 +196,10 @@ fold_thms: thm list, rec_thms: thm list}; -val fp_name_of_ctor = fst o dest_Type o range_type o fastype_of; - -fun morph_fp_result phi {bnfs, ctors, dtors, folds, recs, induct, strong_induct, dtor_ctors, +fun morph_fp_result phi {Ts, bnfs, ctors, dtors, folds, recs, induct, strong_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, fold_thms, rec_thms} = - {bnfs = map (morph_bnf phi) bnfs, + {Ts = map (Morphism.typ phi) Ts, + bnfs = map (morph_bnf phi) bnfs, ctors = map (Morphism.term phi) ctors, dtors = map (Morphism.term phi) dtors, folds = map (Morphism.term phi) folds, diff -r 7a08fe1e19b1 -r 09d24ea3f140 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu May 02 11:58:18 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu May 02 12:35:02 2013 +0200 @@ -3029,7 +3029,7 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - ({bnfs = Jbnfs, ctors = ctors, dtors = dtors, folds = unfolds, recs = corecs, + ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, folds = unfolds, recs = corecs, induct = dtor_coinduct_thm, strong_induct = dtor_strong_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_dtor_map_thms, set_thmss = folded_dtor_set_thmss', diff -r 7a08fe1e19b1 -r 09d24ea3f140 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu May 02 11:58:18 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu May 02 12:35:02 2013 +0200 @@ -1852,7 +1852,7 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - ({bnfs = Ibnfs, ctors = ctors, dtors = dtors, folds = folds, recs = recs, + ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, folds = folds, recs = recs, induct = ctor_induct_thm, strong_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms, set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, fold_thms = ctor_fold_thms,