# HG changeset patch # User desharna # Date 1412595493 -7200 # Node ID b7bc5ba2f3fb952c2fdb642162e295616bbcb302 # Parent 9ff8ca957c02574f36d83475fdcf84644b9e2382 rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct' diff -r 9ff8ca957c02 -r b7bc5ba2f3fb src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:37:38 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:38:13 2014 +0200 @@ -1935,7 +1935,7 @@ val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, - xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms, + xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_induct_thms, xtor_co_rec_transfer_thms, ...}, lthy)) = fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) @@ -2195,7 +2195,7 @@ let val ((rel_induct_thms, common_rel_induct_thm), rel_induct_attrs) = derive_rel_induct_thms_for_types lthy fpTs As Bs ctrss ctr_Tsss - (map #exhaust ctr_sugars) rel_xtor_co_induct_thm ctr_defss ctor_injects + (map #exhaust ctr_sugars) xtor_rel_co_induct ctr_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs; in ((map single rel_induct_thms, single common_rel_induct_thm), @@ -2299,7 +2299,7 @@ val ((rel_coinduct_thms, common_rel_coinduct_thm), (rel_coinduct_attrs, common_rel_coinduct_attrs)) = derive_rel_coinduct_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses - abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm + abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss xtor_rel_co_induct live_nesting_rel_eqs; in ((map single rel_coinduct_thms, single common_rel_coinduct_thm), diff -r 9ff8ca957c02 -r b7bc5ba2f3fb src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:37:38 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:38:13 2014 +0200 @@ -164,7 +164,7 @@ val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs; val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs; - val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #rel_xtor_co_induct_thm) + val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct) |> map (unfold_thms lthy (id_apply :: rel_unfolds)); val rel_defs = map rel_def_of_bnf bnfs; @@ -185,8 +185,8 @@ val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs); val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs; - val rel_xtor_co_induct_thm = - mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys + val xtor_rel_co_induct = + mk_xtor_rel_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos) lthy; @@ -208,7 +208,7 @@ fun mk_type_copy_thms thm = map (curry op RS thm) @{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs}; in - cterm_instantiate_pos cts rel_xtor_co_induct_thm + cterm_instantiate_pos cts xtor_rel_co_induct |> singleton (Proof_Context.export names_lthy lthy) |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ fp_or_nesting_rel_eqs) @@ -225,7 +225,7 @@ let val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As); in - cterm_instantiate_pos cts rel_xtor_co_induct_thm + cterm_instantiate_pos cts xtor_rel_co_induct |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ fp_or_nesting_rel_eqs) |> funpow (2 * n) (fn thm => thm RS spec) @@ -476,7 +476,7 @@ xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*), xtor_co_rec_thms = xtor_co_rec_thms, xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*), - rel_xtor_co_induct_thm = rel_xtor_co_induct_thm, + xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_induct_thms = [], xtor_co_rec_transfer_thms = []} |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy)))); diff -r 9ff8ca957c02 -r b7bc5ba2f3fb src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:37:38 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:38:13 2014 +0200 @@ -26,7 +26,7 @@ xtor_rel_thms: thm list, xtor_co_rec_thms: thm list, xtor_co_rec_o_maps: thm list, - rel_xtor_co_induct_thm: thm, + xtor_rel_co_induct: thm, dtor_set_induct_thms: thm list, xtor_co_rec_transfer_thms: thm list} @@ -176,7 +176,7 @@ val mk_sum_Cinfinite: thm list -> thm val mk_sum_card_order: thm list -> thm - val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list -> + val mk_xtor_rel_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm val mk_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list -> @@ -218,13 +218,13 @@ xtor_rel_thms: thm list, xtor_co_rec_thms: thm list, xtor_co_rec_o_maps: thm list, - rel_xtor_co_induct_thm: thm, + xtor_rel_co_induct: thm, dtor_set_induct_thms: thm list, xtor_co_rec_transfer_thms: thm list}; fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, - xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, rel_xtor_co_induct_thm, + xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct, dtor_set_induct_thms, xtor_co_rec_transfer_thms} = {Ts = map (Morphism.typ phi) Ts, bnfs = map (morph_bnf phi) bnfs, @@ -241,7 +241,7 @@ xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps, - rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm, + xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct, dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms, xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_rec_transfer_thms}; @@ -500,7 +500,7 @@ fun mk_sum_card_order [thm] = thm | mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms]; -fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy = +fun mk_xtor_rel_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy = let val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels; val relphis = map (fn rel => Term.list_comb (rel, phis)) rels; diff -r 9ff8ca957c02 -r b7bc5ba2f3fb src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:37:38 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:38:13 2014 +0200 @@ -1659,7 +1659,7 @@ val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; fun mk_Jrel_DEADID_coinduct_thm () = - mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis + mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis Jzs Jz's dtors dtor's (fn {context = ctxt, prems} => (unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN REPEAT_DETERM (rtac allI 1) THEN rtac (dtor_coinduct_thm OF prems) 1)) lthy; @@ -2255,7 +2255,7 @@ end; val Jrel_coinduct_thm = - mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's + mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's Jrel_coinduct_tac lthy; val le_Jrel_OO_thm = @@ -2541,7 +2541,7 @@ ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss', xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms, - xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm, + xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_rel_co_induct = Jrel_coinduct_thm, dtor_set_induct_thms = dtor_Jset_induct_thms, xtor_co_rec_transfer_thms = dtor_corec_transfer_thms}; in diff -r 9ff8ca957c02 -r b7bc5ba2f3fb src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:37:38 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:38:13 2014 +0200 @@ -1766,7 +1766,7 @@ val Irels = if m = 0 then map HOLogic.eq_const Ts else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; val Irel_induct_thm = - mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's + mk_xtor_rel_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks ctor_Irel_thms rel_mono_strong0s) lthy; @@ -1828,7 +1828,7 @@ ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss', xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms, - xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm, + xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, xtor_rel_co_induct = Irel_induct_thm, dtor_set_induct_thms = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms}; in timer; (fp_res, lthy') diff -r 9ff8ca957c02 -r b7bc5ba2f3fb src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:37:38 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:38:13 2014 +0200 @@ -46,7 +46,7 @@ xtor_rel_thms = [xtor_rel], xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}], xtor_co_rec_o_maps = [ctor_rec_o_map], - rel_xtor_co_induct_thm = xtor_rel_induct, + xtor_rel_co_induct = xtor_rel_induct, dtor_set_induct_thms = [], xtor_co_rec_transfer_thms = []};