rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
authordesharna
Mon Oct 06 13:38:13 2014 +0200 (2014-10-06)
changeset 58579b7bc5ba2f3fb
parent 58578 9ff8ca957c02
child 58580 8ee2d984caa8
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:37:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:38:13 2014 +0200
     1.3 @@ -1935,7 +1935,7 @@
     1.4      val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
     1.5               dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
     1.6               ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
     1.7 -             xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms,
     1.8 +             xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_induct_thms,
     1.9               xtor_co_rec_transfer_thms, ...},
    1.10             lthy)) =
    1.11        fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
    1.12 @@ -2195,7 +2195,7 @@
    1.13              let
    1.14                val ((rel_induct_thms, common_rel_induct_thm), rel_induct_attrs) =
    1.15                  derive_rel_induct_thms_for_types lthy fpTs As Bs ctrss ctr_Tsss
    1.16 -                  (map #exhaust ctr_sugars) rel_xtor_co_induct_thm ctr_defss ctor_injects
    1.17 +                  (map #exhaust ctr_sugars) xtor_rel_co_induct ctr_defss ctor_injects
    1.18                    pre_rel_defs abs_inverses live_nesting_rel_eqs;
    1.19              in
    1.20                ((map single rel_induct_thms, single common_rel_induct_thm),
    1.21 @@ -2299,7 +2299,7 @@
    1.22                val ((rel_coinduct_thms, common_rel_coinduct_thm),
    1.23                     (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
    1.24                  derive_rel_coinduct_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses
    1.25 -                  abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm
    1.26 +                  abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss xtor_rel_co_induct
    1.27                    live_nesting_rel_eqs;
    1.28              in
    1.29                ((map single rel_coinduct_thms, single common_rel_coinduct_thm),
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:37:38 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:38:13 2014 +0200
     2.3 @@ -164,7 +164,7 @@
     2.4      val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
     2.5  
     2.6      val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
     2.7 -    val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
     2.8 +    val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct)
     2.9        |> map (unfold_thms lthy (id_apply :: rel_unfolds));
    2.10  
    2.11      val rel_defs = map rel_def_of_bnf bnfs;
    2.12 @@ -185,8 +185,8 @@
    2.13      val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
    2.14      val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;
    2.15  
    2.16 -    val rel_xtor_co_induct_thm =
    2.17 -      mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
    2.18 +    val xtor_rel_co_induct =
    2.19 +      mk_xtor_rel_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
    2.20          xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs
    2.21            rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
    2.22          lthy;
    2.23 @@ -208,7 +208,7 @@
    2.24              fun mk_type_copy_thms thm = map (curry op RS thm)
    2.25                @{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
    2.26            in
    2.27 -            cterm_instantiate_pos cts rel_xtor_co_induct_thm
    2.28 +            cterm_instantiate_pos cts xtor_rel_co_induct
    2.29              |> singleton (Proof_Context.export names_lthy lthy)
    2.30              |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @
    2.31                  fp_or_nesting_rel_eqs)
    2.32 @@ -225,7 +225,7 @@
    2.33            let
    2.34              val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
    2.35            in
    2.36 -            cterm_instantiate_pos cts rel_xtor_co_induct_thm
    2.37 +            cterm_instantiate_pos cts xtor_rel_co_induct
    2.38              |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
    2.39                  fp_or_nesting_rel_eqs)
    2.40              |> funpow (2 * n) (fn thm => thm RS spec)
    2.41 @@ -476,7 +476,7 @@
    2.42          xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
    2.43          xtor_co_rec_thms = xtor_co_rec_thms,
    2.44          xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
    2.45 -        rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
    2.46 +        xtor_rel_co_induct = xtor_rel_co_induct,
    2.47          dtor_set_induct_thms = [],
    2.48          xtor_co_rec_transfer_thms = []}
    2.49         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 13:37:38 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 13:38:13 2014 +0200
     3.3 @@ -26,7 +26,7 @@
     3.4       xtor_rel_thms: thm list,
     3.5       xtor_co_rec_thms: thm list,
     3.6       xtor_co_rec_o_maps: thm list,
     3.7 -     rel_xtor_co_induct_thm: thm,
     3.8 +     xtor_rel_co_induct: thm,
     3.9       dtor_set_induct_thms: thm list,
    3.10       xtor_co_rec_transfer_thms: thm list}
    3.11  
    3.12 @@ -176,7 +176,7 @@
    3.13    val mk_sum_Cinfinite: thm list -> thm
    3.14    val mk_sum_card_order: thm list -> thm
    3.15  
    3.16 -  val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
    3.17 +  val mk_xtor_rel_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
    3.18      term list -> term list -> term list -> term list -> term list ->
    3.19      ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
    3.20    val mk_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
    3.21 @@ -218,13 +218,13 @@
    3.22     xtor_rel_thms: thm list,
    3.23     xtor_co_rec_thms: thm list,
    3.24     xtor_co_rec_o_maps: thm list,
    3.25 -   rel_xtor_co_induct_thm: thm,
    3.26 +   xtor_rel_co_induct: thm,
    3.27     dtor_set_induct_thms: thm list,
    3.28     xtor_co_rec_transfer_thms: thm list};
    3.29  
    3.30  fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
    3.31      dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
    3.32 -    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, rel_xtor_co_induct_thm,
    3.33 +    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct,
    3.34      dtor_set_induct_thms, xtor_co_rec_transfer_thms} =
    3.35    {Ts = map (Morphism.typ phi) Ts,
    3.36     bnfs = map (morph_bnf phi) bnfs,
    3.37 @@ -241,7 +241,7 @@
    3.38     xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
    3.39     xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
    3.40     xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
    3.41 -   rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
    3.42 +   xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct,
    3.43     dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms,
    3.44     xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_rec_transfer_thms};
    3.45  
    3.46 @@ -500,7 +500,7 @@
    3.47  fun mk_sum_card_order [thm] = thm
    3.48    | mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
    3.49  
    3.50 -fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
    3.51 +fun mk_xtor_rel_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
    3.52    let
    3.53      val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
    3.54      val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
     4.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 13:37:38 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 13:38:13 2014 +0200
     4.3 @@ -1659,7 +1659,7 @@
     4.4      val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
     4.5  
     4.6      fun mk_Jrel_DEADID_coinduct_thm () =
     4.7 -      mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
     4.8 +      mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
     4.9          Jzs Jz's dtors dtor's (fn {context = ctxt, prems} =>
    4.10            (unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
    4.11            REPEAT_DETERM (rtac allI 1) THEN rtac (dtor_coinduct_thm OF prems) 1)) lthy;
    4.12 @@ -2255,7 +2255,7 @@
    4.13          end;
    4.14  
    4.15        val Jrel_coinduct_thm =
    4.16 -        mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
    4.17 +        mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
    4.18            Jrel_coinduct_tac lthy;
    4.19  
    4.20          val le_Jrel_OO_thm =
    4.21 @@ -2541,7 +2541,7 @@
    4.22         ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
    4.23         xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
    4.24         xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
    4.25 -       xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
    4.26 +       xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_rel_co_induct = Jrel_coinduct_thm,
    4.27         dtor_set_induct_thms = dtor_Jset_induct_thms,
    4.28         xtor_co_rec_transfer_thms = dtor_corec_transfer_thms};
    4.29    in
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:37:38 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:38:13 2014 +0200
     5.3 @@ -1766,7 +1766,7 @@
     5.4      val Irels = if m = 0 then map HOLogic.eq_const Ts
     5.5        else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
     5.6      val Irel_induct_thm =
     5.7 -      mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
     5.8 +      mk_xtor_rel_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
     5.9          (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
    5.10             ctor_Irel_thms rel_mono_strong0s) lthy;
    5.11  
    5.12 @@ -1828,7 +1828,7 @@
    5.13         ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
    5.14         xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
    5.15         xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
    5.16 -       xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
    5.17 +       xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, xtor_rel_co_induct = Irel_induct_thm,
    5.18         dtor_set_induct_thms = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms};
    5.19    in
    5.20      timer; (fp_res, lthy')
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:37:38 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:38:13 2014 +0200
     6.3 @@ -46,7 +46,7 @@
     6.4     xtor_rel_thms = [xtor_rel],
     6.5     xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
     6.6     xtor_co_rec_o_maps = [ctor_rec_o_map],
     6.7 -   rel_xtor_co_induct_thm = xtor_rel_induct,
     6.8 +   xtor_rel_co_induct = xtor_rel_induct,
     6.9     dtor_set_induct_thms = [],
    6.10     xtor_co_rec_transfer_thms = []};
    6.11