# HG changeset patch # User desharna # Date 1411735314 -7200 # Node ID a88eb33058f753094cdb673ff20985a96b0d8295 # Parent f70bffabd7cfcb39f995d506cf2223cb32774bff refactor fp_sugar move theorems diff -r f70bffabd7cf -r a88eb33058f7 src/HOL/Library/bnf_lfp_countable.ML --- a/src/HOL/Library/bnf_lfp_countable.ML Fri Sep 26 14:41:15 2014 +0200 +++ b/src/HOL/Library/bnf_lfp_countable.ML Fri Sep 26 14:41:54 2014 +0200 @@ -152,7 +152,7 @@ val fp_sugars as {fp_nesting_bnfs, common_co_inducts = induct :: _, ...} :: _ = map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0; - val ctr_sugars = map #ctr_sugar fp_sugars; + val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars; val ctrss0 = map #ctrs ctr_sugars; val ns = map length ctrss0; diff -r f70bffabd7cf -r a88eb33058f7 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 14:41:15 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 14:41:54 2014 +0200 @@ -8,7 +8,10 @@ signature BNF_FP_DEF_SUGAR = sig - type fp_ctr_sugar = {} + type fp_ctr_sugar = + {ctrXs_Tss: typ list list, + ctr_defs: thm list, + ctr_sugar: Ctr_Sugar.ctr_sugar} type fp_bnf_sugar = {rel_injects: thm list, @@ -31,9 +34,6 @@ 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, @@ -160,7 +160,10 @@ val set_inductN = "set_induct"; val set_selN = "set_sel"; -type fp_ctr_sugar = {} +type fp_ctr_sugar = + {ctrXs_Tss: typ list list, + ctr_defs: thm list, + ctr_sugar: Ctr_Sugar.ctr_sugar} type fp_bnf_sugar = {rel_injects: thm list, @@ -183,9 +186,6 @@ 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, @@ -205,9 +205,14 @@ co_rec_discs = map (Morphism.thm phi) co_rec_discs, co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss} +fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar} : fp_ctr_sugar) = + {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} + 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, - fp_ctr_sugar, fp_bnf_sugar, fp_co_induct_sugar} : fp_sugar) = + live_nesting_bnfs, co_rec, co_rec_def, maps, common_co_inducts, fp_ctr_sugar, fp_bnf_sugar, + fp_co_induct_sugar} : fp_sugar) = {T = Morphism.typ phi T, BT = Morphism.typ phi BT, X = Morphism.typ phi X, @@ -218,14 +223,11 @@ 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, - fp_ctr_sugar = fp_ctr_sugar, + fp_ctr_sugar = morph_fp_ctr_sugar phi fp_ctr_sugar, fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar, fp_co_induct_sugar = morph_fp_co_induct_sugar phi fp_co_induct_sugar}; @@ -286,10 +288,12 @@ {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs, - ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk, maps = nth mapss kk, common_co_inducts = common_co_inducts, - fp_ctr_sugar = {}, + fp_ctr_sugar = + {ctrXs_Tss = nth ctrXs_Tsss kk, + ctr_defs = nth ctr_defss kk, + ctr_sugar = nth ctr_sugars kk}, fp_bnf_sugar = {rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk}, diff -r f70bffabd7cf -r a88eb33058f7 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:41:15 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:41:54 2014 +0200 @@ -136,7 +136,7 @@ val nn = length fpTs; val kks = 0 upto nn - 1; - fun target_ctr_sugar_of_fp_sugar fpT ({T, ctr_sugar, ...} : fp_sugar) = + fun target_ctr_sugar_of_fp_sugar fpT ({T, fp_ctr_sugar = {ctr_sugar, ...}, ...} : fp_sugar) = let val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) []; val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho); @@ -144,7 +144,7 @@ morph_ctr_sugar phi ctr_sugar end; - val ctr_defss = map #ctr_defs fp_sugars0; + val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0; val mapss = map #maps fp_sugars0; val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0; @@ -296,10 +296,12 @@ ({fp_bnf_sugar = {rel_injects, rel_distincts, ...}, ...} : fp_sugar) = {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs, - live_nesting_bnfs = live_nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, - ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps, + live_nesting_bnfs = live_nesting_bnfs, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps, common_co_inducts = common_co_inducts, - fp_ctr_sugar = {}, + fp_ctr_sugar = + {ctrXs_Tss = ctrXs_Tss, + ctr_defs = ctr_defs, + ctr_sugar = ctr_sugar}, fp_bnf_sugar = {rel_injects = rel_injects, rel_distincts = rel_distincts}, @@ -457,7 +459,8 @@ val perm_callssss0 = permute callssss0; val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts; - val perm_callssss = map2 (indexify_callsss o #ctrs o #ctr_sugar) perm_fp_sugars0 perm_callssss0; + val perm_callssss = + map2 (indexify_callsss o #ctrs o #ctr_sugar o #fp_ctr_sugar) perm_fp_sugars0 perm_callssss0; val ((perm_fp_sugars, fp_sugar_thms), lthy) = if length perm_Tss = 1 then diff -r f70bffabd7cf -r a88eb33058f7 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 14:41:15 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 14:41:54 2014 +0200 @@ -420,7 +420,8 @@ val perm_indices = map #fp_res_index perm_fp_sugars; val perm_fpTs = map #T perm_fp_sugars; - val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars; + val perm_ctrXs_Tsss' = + map (repair_nullary_single_ctr o #ctrXs_Tss o #fp_ctr_sugar) perm_fp_sugars; val nn0 = length res_Ts; val nn = length perm_fpTs; @@ -495,7 +496,7 @@ distinct_discsss collapses corec_thms corec_discs corec_selss end; - fun mk_spec ({T, ctr_sugar as {exhaust_discs, sel_defs, ...}, co_rec = corec, + fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...}, co_rec = corec, fp_co_induct_sugar = {co_rec_thms = corec_thms, co_rec_discs = corec_discs, co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = {corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, exhaust_discs = exhaust_discs, diff -r f70bffabd7cf -r a88eb33058f7 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:41:15 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:41:54 2014 +0200 @@ -76,14 +76,14 @@ absT_info = trivial_absT_info_of fpT, fp_nesting_bnfs = [], live_nesting_bnfs = [], - ctrXs_Tss = ctr_Tss, - ctr_defs = @{thms Inl_def_alt Inr_def_alt}, - ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]}, maps = @{thms map_sum.simps}, common_co_inducts = @{thms sum.induct}, - fp_ctr_sugar = {}, + fp_ctr_sugar = + {ctrXs_Tss = ctr_Tss, + ctr_defs = @{thms Inl_def_alt Inr_def_alt}, + ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name}, fp_bnf_sugar = {rel_injects = @{thms rel_sum_simps(1,4)}, rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}}, @@ -120,14 +120,14 @@ absT_info = trivial_absT_info_of fpT, fp_nesting_bnfs = [], live_nesting_bnfs = [], - ctrXs_Tss = [ctr_Ts], - ctr_defs = @{thms Pair_def_alt}, - ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]}, maps = @{thms map_prod_simp}, common_co_inducts = @{thms prod.induct}, - fp_ctr_sugar = {}, + fp_ctr_sugar = + {ctrXs_Tss = [ctr_Ts], + ctr_defs = @{thms Pair_def_alt}, + ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name}, fp_bnf_sugar = {rel_injects = @{thms rel_prod_apply}, rel_distincts = []}, diff -r f70bffabd7cf -r a88eb33058f7 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Sep 26 14:41:15 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Sep 26 14:41:54 2014 +0200 @@ -236,7 +236,7 @@ fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) = (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs)); - val fp_ctr_sugars = map (#ctr_sugar o checked_fp_sugar_of) fpT_names; + val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar o checked_fp_sugar_of) fpT_names; val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars; val all_infos = Old_Datatype_Data.get_all thy; val (orig_descr' :: nested_descrs) = @@ -290,11 +290,12 @@ else ((fp_sugars, (NONE, NONE)), lthy); - fun mk_ctr_of ({ctr_sugar = {ctrs, ...}, ...} : fp_sugar) (Type (_, Ts)) = map (mk_ctr Ts) ctrs; + fun mk_ctr_of ({fp_ctr_sugar = {ctr_sugar = {ctrs, ...}, ...}, ...} : fp_sugar) (Type (_, Ts)) = + map (mk_ctr Ts) ctrs; val substAT = Term.typ_subst_atomic (var_As ~~ As); val Xs' = map #X fp_sugars'; - val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss) fp_sugars'; + val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss o #fp_ctr_sugar) fp_sugars'; val ctrss' = map2 mk_ctr_of fp_sugars' fpTs'; val {common_co_inducts = induct :: _, ...} :: _ = fp_sugars'; val inducts = map (hd o #co_inducts o #fp_co_induct_sugar) fp_sugars'; @@ -317,8 +318,9 @@ val rec'_names = map (fst o dest_Const) recs'; val rec'_thms = flat rec'_thmss; - fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects, - distincts, case_thms, case_cong, case_cong_weak, split, split_asm, ...}, ...} : fp_sugar) = + fun mk_info (kk, {T = Type (T_name0, _), fp_ctr_sugar = {ctr_sugar = {casex, exhaust, nchotomy, + injects, distincts, case_thms, case_cong, case_cong_weak, split, + split_asm, ...}, ...}, ...} : fp_sugar) = (T_name0, {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct', inducts = inducts', exhaust = exhaust, nchotomy = nchotomy, rec_names = rec'_names, diff -r f70bffabd7cf -r a88eb33058f7 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Sep 26 14:41:15 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Sep 26 14:41:54 2014 +0200 @@ -24,7 +24,7 @@ | is_new_datatype ctxt s = (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false); -fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_sugar, co_rec = recx, +fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...}, co_rec = recx, fp_co_induct_sugar = {co_rec_thms = rec_thms, ...}, ...} : fp_sugar) = {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, recx = recx, rec_thms = rec_thms}; @@ -51,7 +51,7 @@ SOME (T, C) => [T, C] | NONE => [U]); - val ctrXs_Tsss = map #ctrXs_Tss fp_sugars; + val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) fp_sugars; val fun_arg_Tssss = map (map (map zip_XrecT)) ctrXs_Tsss; val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; diff -r f70bffabd7cf -r a88eb33058f7 src/HOL/Tools/SMT/smt_datatypes.ML --- a/src/HOL/Tools/SMT/smt_datatypes.ML Fri Sep 26 14:41:15 2014 +0200 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML Fri Sep 26 14:41:54 2014 +0200 @@ -71,13 +71,13 @@ | info :: _ => (map (pair (hd fps)) (get_typedef_decl info T Ts), ctxt)) in (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of - SOME {fp, fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} => + SOME {fp, fp_res = {Ts = fp_Ts, ...}, fp_ctr_sugar = {ctr_sugar, ...}, ...} => if member (op =) fps fp then let val ns = map (fst o dest_Type) fp_Ts val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns val Xs = map #X mutual_fp_sugars - val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars + val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) mutual_fp_sugars (* Datatypes nested through datatypes and codatatypes nested through codatatypes are allowed. So are mutually (co)recursive (co)datatypes. *)