# HG changeset patch # User blanchet # Date 1393847300 -3600 # Node ID fa3a1ec69a1bc55be24362f362d70154d23987f0 # Parent b458558cbcc2ad1020119796d2a3b441960211e8 rationalize internals diff -r b458558cbcc2 -r fa3a1ec69a1b src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:20 2014 +0100 @@ -265,6 +265,7 @@ hide_fact (open) id_transfer datatype_new 'a F = F 'a +datatype_compat F primrec f where "f (F x) = x" diff -r b458558cbcc2 -r fa3a1ec69a1b src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 12:48:20 2014 +0100 @@ -20,13 +20,13 @@ ctrXs_Tss: typ list list, ctr_defs: thm list, ctr_sugar: Ctr_Sugar.ctr_sugar, - co_iters: term list, + co_rec: term, maps: thm list, common_co_inducts: thm list, co_inducts: thm list, - co_iter_thmss: thm list list, - disc_co_iterss: thm list list, - sel_co_itersss: thm list list list}; + co_rec_thms: thm list, + disc_co_recs: thm list, + sel_co_recss: thm list list}; val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar @@ -131,17 +131,17 @@ ctrXs_Tss: typ list list, ctr_defs: thm list, ctr_sugar: Ctr_Sugar.ctr_sugar, - co_iters: term list, + co_rec: term, maps: thm list, common_co_inducts: thm list, co_inducts: thm list, - co_iter_thmss: thm list list, - disc_co_iterss: thm list list, - sel_co_itersss: thm list list list}; + co_rec_thms: thm list, + disc_co_recs: thm list, + sel_co_recss: thm list list}; fun morph_fp_sugar phi ({T, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs, - nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, - co_iter_thmss, disc_co_iterss, sel_co_itersss} : fp_sugar) = + nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, maps, common_co_inducts, co_inducts, + co_rec_thms, disc_co_recs, sel_co_recss} : fp_sugar) = {T = Morphism.typ phi T, X = Morphism.typ phi X, fp = fp, @@ -154,13 +154,13 @@ 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_iters = map (Morphism.term phi) co_iters, + co_rec = Morphism.term phi co_rec, 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_iter_thmss = map (map (Morphism.thm phi)) co_iter_thmss, - disc_co_iterss = map (map (Morphism.thm phi)) disc_co_iterss, - sel_co_itersss = map (map (map (Morphism.thm phi))) sel_co_itersss}; + 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}; val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of; @@ -190,17 +190,17 @@ (fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar))); fun register_fp_sugars Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) - ctrXs_Tsss ctr_defss ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss - disc_co_itersss sel_co_iterssss lthy = + ctrXs_Tsss ctr_defss ctr_sugars co_recs mapss common_co_inducts co_inductss co_rec_thmss + disc_co_recss sel_co_recsss lthy = (0, lthy) |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, register_fp_sugar s {T = T, 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, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, - ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk, maps = nth mapss kk, + ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, maps = nth mapss kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk, - co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk, - sel_co_itersss = nth sel_co_iterssss kk} + co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk, + sel_co_recss = nth sel_co_recsss kk} lthy)) Ts |> snd; @@ -1364,9 +1364,9 @@ val induct_type_attr = Attrib.internal o K o Induct.induct_type; - val (iterss', rec_thmss') = - if iterss = [[]] then ([map #casex ctr_sugars], map #case_thms ctr_sugars) - else (iterss, rec_thmss); + val (recs, rec_thmss') = + if iterss = [[]] then (map #casex ctr_sugars, map #case_thms ctr_sugars) + else (map the_single iterss, rec_thmss); val simp_thmss = map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injects rel_distincts setss; @@ -1388,8 +1388,8 @@ I) |> Local_Theory.notes (common_notes @ notes) |> snd |> register_fp_sugars Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res - ctrXs_Tsss ctr_defss ctr_sugars iterss' mapss [induct_thm] (map single induct_thms) - (map single rec_thmss') (replicate nn []) (replicate nn []) + ctrXs_Tsss ctr_defss ctr_sugars recs mapss [induct_thm] (map single induct_thms) + rec_thmss' (replicate nn []) (replicate nn []) end; fun derive_note_coinduct_coiters_thms_for_types @@ -1446,9 +1446,9 @@ |> add_spec_rules co_rec_of sel_corec_thmss corec_thmss |> Local_Theory.notes (common_notes @ notes) |> snd |> register_fp_sugars Xs Greatest_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res - ctrXs_Tsss ctr_defss ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm] - (transpose [coinduct_thms, strong_coinduct_thms]) (map single corec_thmss) - (map single disc_corec_thmss) (map single sel_corec_thmsss) + ctrXs_Tsss ctr_defss ctr_sugars (map the_single coiterss) mapss + [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms]) + corec_thmss disc_corec_thmss sel_corec_thmsss end; val lthy'' = lthy' diff -r b458558cbcc2 -r fa3a1ec69a1b src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 12:48:20 2014 +0100 @@ -274,19 +274,20 @@ val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0; - fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_iters maps + fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec maps co_inducts co_rec_thms disc_corec_thms sel_corec_thmss = {T = T, X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, - ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_iters = co_iters, + ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec, maps = maps, common_co_inducts = common_co_inducts, co_inducts = co_inducts, - co_iter_thmss = [co_rec_thms], disc_co_iterss = [disc_corec_thms], - sel_co_itersss = [sel_corec_thmss]} + co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms, + sel_co_recss = sel_corec_thmss} |> morph_fp_sugar phi; val target_fp_sugars = map14 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars - co_iterss mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss sel_corec_thmsss; + (map the_single co_iterss) mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss + sel_corec_thmsss; val n2m_sugar = (target_fp_sugars, fp_sugar_thms); in diff -r b458558cbcc2 -r fa3a1ec69a1b src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Mar 03 12:48:20 2014 +0100 @@ -374,7 +374,7 @@ let val thy = Proof_Context.theory_of lthy0; - val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, co_iters = coiter1 :: _, + val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, co_rec = corec, common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) = nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0; @@ -394,7 +394,7 @@ val perm_Ts = map #T perm_fp_sugars; val perm_Xs = map #X perm_fp_sugars; - val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o #co_iters) perm_fp_sugars; + val perm_Cs = map (domain_type o body_fun_type o fastype_of o #co_rec) perm_fp_sugars; val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs); fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)] @@ -454,27 +454,22 @@ end; fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} - : ctr_sugar) p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss sel_coitersss = - let - val p_ios = map SOME p_is @ [NONE]; - val corec_thms = co_rec_of coiter_thmss; - val disc_corecs = co_rec_of disc_coiterss; - val sel_corecss = co_rec_of sel_coitersss; - in + : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms disc_corecs sel_corecss = + let val p_ios = map SOME p_is @ [NONE] in map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss disc_excludesss collapses corec_thms disc_corecs sel_corecss end; - fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_iters = coiters, - co_iter_thmss = coiter_thmss, disc_co_iterss = disc_coiterss, - sel_co_itersss = sel_coitersss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = - {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of coiters), + fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_rec = corec, + co_rec_thms = corec_thms, disc_co_recs = disc_corecs, + sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = + {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts, nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs, nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs, nested_map_comps = map map_comp_of_bnf nested_bnfs, - ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss - sel_coitersss}; + ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs + sel_corecss}; in ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts, co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms, diff -r b458558cbcc2 -r fa3a1ec69a1b src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Mar 03 12:48:20 2014 +0100 @@ -146,8 +146,8 @@ (kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0)); val descr = map3 mk_typ_descr kkssss Tparentss ctrss0; - val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars; - val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars; + val recs = map (fst o dest_Const o #co_rec) fp_sugars; + val rec_thms = maps #co_rec_thms fp_sugars; fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) = diff -r b458558cbcc2 -r fa3a1ec69a1b src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Mar 03 12:48:20 2014 +0100 @@ -21,10 +21,10 @@ fun 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_defs, ctr_sugar, co_iters = iters, - co_iter_thmss = iter_thmss, ...} : fp_sugar) = +fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_rec = recx, + co_rec_thms = rec_thms, ...} : fp_sugar) = {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs, - ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss}; + ctr_sugar = ctr_sugar, recx = recx, rec_thms = rec_thms}; fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 = let @@ -35,7 +35,7 @@ val Ts = map #T fp_sugars; val Xs = map #X fp_sugars; - val Cs = map (body_type o fastype_of o co_rec_of o #co_iters) fp_sugars; + val Cs = map (body_type o fastype_of o #co_rec) fp_sugars; val Xs_TCs = Xs ~~ (Ts ~~ Cs); fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)]