rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
authordesharna
Mon Oct 06 13:37:38 2014 +0200 (2014-10-06)
changeset 585789ff8ca957c02
parent 58577 15337ad05370
child 58579 b7bc5ba2f3fb
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
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
src/HOL/Tools/BNF/bnf_lfp_size.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:36:48 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:37:38 2014 +0200
     1.3 @@ -388,7 +388,7 @@
     1.4  
     1.5      val co_recs = map (Morphism.term phi) raw_co_recs;
     1.6  
     1.7 -    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms
     1.8 +    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_maps
     1.9        |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
    1.10  
    1.11      val xtor_co_rec_thms =
    1.12 @@ -475,7 +475,7 @@
    1.13          xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
    1.14          xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
    1.15          xtor_co_rec_thms = xtor_co_rec_thms,
    1.16 -        xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
    1.17 +        xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
    1.18          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
    1.19          dtor_set_induct_thms = [],
    1.20          xtor_co_rec_transfer_thms = []}
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 13:36:48 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 13:37:38 2014 +0200
     2.3 @@ -25,7 +25,7 @@
     2.4       xtor_set_thmss: thm list list,
     2.5       xtor_rel_thms: thm list,
     2.6       xtor_co_rec_thms: thm list,
     2.7 -     xtor_co_rec_o_map_thms: thm list,
     2.8 +     xtor_co_rec_o_maps: thm list,
     2.9       rel_xtor_co_induct_thm: thm,
    2.10       dtor_set_induct_thms: thm list,
    2.11       xtor_co_rec_transfer_thms: thm list}
    2.12 @@ -217,14 +217,14 @@
    2.13     xtor_set_thmss: thm list list,
    2.14     xtor_rel_thms: thm list,
    2.15     xtor_co_rec_thms: thm list,
    2.16 -   xtor_co_rec_o_map_thms: thm list,
    2.17 +   xtor_co_rec_o_maps: thm list,
    2.18     rel_xtor_co_induct_thm: thm,
    2.19     dtor_set_induct_thms: thm list,
    2.20     xtor_co_rec_transfer_thms: thm list};
    2.21  
    2.22  fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
    2.23      dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
    2.24 -    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm,
    2.25 +    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, rel_xtor_co_induct_thm,
    2.26      dtor_set_induct_thms, xtor_co_rec_transfer_thms} =
    2.27    {Ts = map (Morphism.typ phi) Ts,
    2.28     bnfs = map (morph_bnf phi) bnfs,
    2.29 @@ -240,7 +240,7 @@
    2.30     xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
    2.31     xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
    2.32     xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
    2.33 -   xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
    2.34 +   xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
    2.35     rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
    2.36     dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms,
    2.37     xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_rec_transfer_thms};
     3.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 13:36:48 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 13:37:38 2014 +0200
     3.3 @@ -2541,7 +2541,7 @@
     3.4         ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
     3.5         xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
     3.6         xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
     3.7 -       xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
     3.8 +       xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
     3.9         dtor_set_induct_thms = dtor_Jset_induct_thms,
    3.10         xtor_co_rec_transfer_thms = dtor_corec_transfer_thms};
    3.11    in
     4.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:36:48 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:37:38 2014 +0200
     4.3 @@ -1828,7 +1828,7 @@
     4.4         ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
     4.5         xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
     4.6         xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
     4.7 -       xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
     4.8 +       xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
     4.9         dtor_set_induct_thms = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms};
    4.10    in
    4.11      timer; (fp_res, lthy')
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:36:48 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:37:38 2014 +0200
     5.3 @@ -45,7 +45,7 @@
     5.4     xtor_set_thmss = [xtor_sets],
     5.5     xtor_rel_thms = [xtor_rel],
     5.6     xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
     5.7 -   xtor_co_rec_o_map_thms = [ctor_rec_o_map],
     5.8 +   xtor_co_rec_o_maps = [ctor_rec_o_map],
     5.9     rel_xtor_co_induct_thm = xtor_rel_induct,
    5.10     dtor_set_induct_thms = [],
    5.11     xtor_co_rec_transfer_thms = []};
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Oct 06 13:36:48 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Oct 06 13:37:38 2014 +0200
     6.3 @@ -82,7 +82,7 @@
     6.4    IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
     6.5  
     6.6  fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
     6.7 -      fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, fp_nesting_bnfs,
     6.8 +      fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_maps = ctor_rec_o_maps, ...}, fp_nesting_bnfs,
     6.9        live_nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
    6.10      let
    6.11        val data = Data.get (Context.Proof lthy0);