rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
authordesharna
Mon Oct 06 13:39:12 2014 +0200 (2014-10-06)
changeset 58581e2e2d775869c
parent 58580 8ee2d984caa8
child 58582 a408c72a849c
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
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:38:40 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:39:12 2014 +0200
     1.3 @@ -1936,7 +1936,7 @@
     1.4               dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
     1.5               ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
     1.6               xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
     1.7 -             xtor_co_rec_transfer_thms, ...},
     1.8 +             xtor_co_rec_transfers, ...},
     1.9             lthy)) =
    1.10        fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
    1.11          (map dest_TFree killed_As) fp_eqs no_defs_lthy
    1.12 @@ -2162,7 +2162,7 @@
    1.13          Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
    1.14            (fn {context = ctxt, prems = _} =>
    1.15               mk_rec_transfer_tac ctxt nn ns (map (certify ctxt) Ss) (map (certify ctxt) Rs) rec_defs
    1.16 -               xtor_co_rec_transfer_thms pre_rel_defs live_nesting_rel_eqs)
    1.17 +               xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs)
    1.18          |> Conjunction.elim_balanced nn
    1.19          |> Proof_Context.export names_lthy lthy
    1.20          |> map Thm.close_derivation
    1.21 @@ -2244,7 +2244,7 @@
    1.22          Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
    1.23            (fn {context = ctxt, prems = _} =>
    1.24               mk_corec_transfer_tac ctxt (map (certify ctxt) Ss) (map (certify ctxt) Rs)
    1.25 -               type_definitions corec_defs xtor_co_rec_transfer_thms pre_rel_defs
    1.26 +               type_definitions corec_defs xtor_co_rec_transfers pre_rel_defs
    1.27                 live_nesting_rel_eqs (flat pgss) pss qssss gssss)
    1.28          |> Conjunction.elim_balanced (length goals)
    1.29          |> Proof_Context.export names_lthy lthy
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:38:40 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:39:12 2014 +0200
     2.3 @@ -478,7 +478,7 @@
     2.4          xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
     2.5          xtor_rel_co_induct = xtor_rel_co_induct,
     2.6          dtor_set_inducts = [],
     2.7 -        xtor_co_rec_transfer_thms = []}
     2.8 +        xtor_co_rec_transfers = []}
     2.9         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
    2.10    in
    2.11      (fp_res, lthy)
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 13:38:40 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 13:39:12 2014 +0200
     3.3 @@ -28,7 +28,7 @@
     3.4       xtor_co_rec_o_maps: thm list,
     3.5       xtor_rel_co_induct: thm,
     3.6       dtor_set_inducts: thm list,
     3.7 -     xtor_co_rec_transfer_thms: thm list}
     3.8 +     xtor_co_rec_transfers: thm list}
     3.9  
    3.10    val morph_fp_result: morphism -> fp_result -> fp_result
    3.11  
    3.12 @@ -220,12 +220,12 @@
    3.13     xtor_co_rec_o_maps: thm list,
    3.14     xtor_rel_co_induct: thm,
    3.15     dtor_set_inducts: thm list,
    3.16 -   xtor_co_rec_transfer_thms: thm list};
    3.17 +   xtor_co_rec_transfers: thm list};
    3.18  
    3.19  fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
    3.20      dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
    3.21      xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct,
    3.22 -    dtor_set_inducts, xtor_co_rec_transfer_thms} =
    3.23 +    dtor_set_inducts, xtor_co_rec_transfers} =
    3.24    {Ts = map (Morphism.typ phi) Ts,
    3.25     bnfs = map (morph_bnf phi) bnfs,
    3.26     ctors = map (Morphism.term phi) ctors,
    3.27 @@ -243,7 +243,7 @@
    3.28     xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
    3.29     xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct,
    3.30     dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts,
    3.31 -   xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_rec_transfer_thms};
    3.32 +   xtor_co_rec_transfers = map (Morphism.thm phi) xtor_co_rec_transfers};
    3.33  
    3.34  fun time ctxt timer msg = (if Config.get ctxt bnf_timing
    3.35    then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
     4.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 13:38:40 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 13:39:12 2014 +0200
     4.3 @@ -2543,7 +2543,7 @@
     4.4         xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
     4.5         xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_rel_co_induct = Jrel_coinduct_thm,
     4.6         dtor_set_inducts = dtor_Jset_induct_thms,
     4.7 -       xtor_co_rec_transfer_thms = dtor_corec_transfer_thms};
     4.8 +       xtor_co_rec_transfers = dtor_corec_transfer_thms};
     4.9    in
    4.10      timer; (fp_res, lthy')
    4.11    end;
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:38:40 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:39:12 2014 +0200
     5.3 @@ -1829,7 +1829,7 @@
     5.4         xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
     5.5         xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
     5.6         xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, xtor_rel_co_induct = Irel_induct_thm,
     5.7 -       dtor_set_inducts = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms};
     5.8 +       dtor_set_inducts = [], xtor_co_rec_transfers = ctor_rec_transfer_thms};
     5.9    in
    5.10      timer; (fp_res, lthy')
    5.11    end;
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:38:40 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:39:12 2014 +0200
     6.3 @@ -48,7 +48,7 @@
     6.4     xtor_co_rec_o_maps = [ctor_rec_o_map],
     6.5     xtor_rel_co_induct = xtor_rel_induct,
     6.6     dtor_set_inducts = [],
     6.7 -   xtor_co_rec_transfer_thms = []};
     6.8 +   xtor_co_rec_transfers = []};
     6.9  
    6.10  fun fp_sugar_of_sum ctxt =
    6.11    let