tuned names
authortraytel
Sun Apr 03 10:25:17 2016 +0200 (2016-04-03 ago)
changeset 62827609f97d79bc2
parent 62826 eb94e570c1a4
child 62841 388719339ada
tuned names
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Sat Apr 02 23:29:05 2016 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Sun Apr 03 10:25:17 2016 +0200
     1.3 @@ -191,10 +191,10 @@
     1.4    val mk_xtor_rel_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
     1.5      term list -> term list -> term list -> term list -> term list ->
     1.6      ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
     1.7 -  val mk_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
     1.8 +  val mk_xtor_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
     1.9      term list -> term list -> term list -> term list ->
    1.10      ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list
    1.11 -  val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
    1.12 +  val mk_xtor_co_iter_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
    1.13      thm list -> thm list -> thm list
    1.14  
    1.15    val fixpoint_bnf: (binding -> binding) ->
    1.16 @@ -560,7 +560,7 @@
    1.17      |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
    1.18    end;
    1.19  
    1.20 -fun mk_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy =
    1.21 +fun mk_xtor_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy =
    1.22    let
    1.23      val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_iphis)) pre_rels;
    1.24      val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
    1.25 @@ -579,7 +579,7 @@
    1.26      |> split_conj_thm
    1.27    end;
    1.28  
    1.29 -fun mk_xtor_un_fold_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps
    1.30 +fun mk_xtor_co_iter_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps
    1.31      map_cong0s =
    1.32    let
    1.33      val n = length sym_map_comps;
     2.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Sat Apr 02 23:29:05 2016 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Sun Apr 03 10:25:17 2016 +0200
     2.3 @@ -2630,10 +2630,10 @@
     2.4        |> mk_Frees "R" JphiTs
     2.5        ||>> mk_Frees "S" activephiTs;
     2.6  
     2.7 -    val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m
     2.8 +    val dtor_unfold_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP false m
     2.9        dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
    2.10        sym_map_comps map_cong0s;
    2.11 -    val dtor_corec_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m
    2.12 +    val dtor_corec_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP true m
    2.13        dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms)
    2.14        sym_map_comps map_cong0s;
    2.15  
    2.16 @@ -2642,7 +2642,7 @@
    2.17        else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
    2.18  
    2.19      val dtor_unfold_transfer_thms =
    2.20 -      mk_co_iter_transfer_thms Greatest_FP rels activephis activephis Jrels Jphis
    2.21 +      mk_xtor_co_iter_transfer_thms Greatest_FP rels activephis activephis Jrels Jphis
    2.22          (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
    2.23          (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm
    2.24            (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
    2.25 @@ -2654,7 +2654,7 @@
    2.26      val corec_activephis =
    2.27        map2 (fn Jrel => mk_rel_sum (Term.list_comb (Jrel, Jphis))) Jrels activephis;
    2.28      val dtor_corec_transfer_thms =
    2.29 -      mk_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis
    2.30 +      mk_xtor_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis
    2.31          (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs)
    2.32          (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs
    2.33             dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms)
     3.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Sat Apr 02 23:29:05 2016 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Apr 03 10:25:17 2016 +0200
     3.3 @@ -1886,9 +1886,9 @@
     3.4        ||>> mk_Frees "S" activephiTs
     3.5        ||>> mk_Frees "IR" activeIphiTs;
     3.6  
     3.7 -    val ctor_fold_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm
     3.8 +    val ctor_fold_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP false m ctor_fold_unique_thm
     3.9        ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
    3.10 -    val ctor_rec_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm
    3.11 +    val ctor_rec_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP true m ctor_rec_unique_thm
    3.12        ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s;
    3.13  
    3.14      val Irels = if m = 0 then map HOLogic.eq_const Ts
    3.15 @@ -1900,7 +1900,7 @@
    3.16  
    3.17      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
    3.18      val ctor_fold_transfer_thms =
    3.19 -      mk_co_iter_transfer_thms Least_FP rels activephis activephis Irels Iphis
    3.20 +      mk_xtor_co_iter_transfer_thms Least_FP rels activephis activephis Irels Iphis
    3.21          (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
    3.22          (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm
    3.23            (map map_transfer_of_bnf bnfs) ctor_fold_thms)
    3.24 @@ -1912,7 +1912,7 @@
    3.25      val rec_activephis =
    3.26        map2 (fn Irel => mk_rel_prod (Term.list_comb (Irel, Iphis))) Irels activephis;
    3.27      val ctor_rec_transfer_thms =
    3.28 -      mk_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis
    3.29 +      mk_xtor_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis
    3.30          (mk_recs Ts passiveAs activeAs) (mk_recs Ts' passiveBs activeBs)
    3.31          (fn {context = ctxt, prems = _} => mk_ctor_rec_transfer_tac ctxt n m rec_defs
    3.32             ctor_fold_transfer_thms (map map_transfer_of_bnf bnfs) ctor_Irel_thms)