tuned names
authortraytel
Sun, 03 Apr 2016 10:25:17 +0200 (2016-04-03)
changeset 62827 609f97d79bc2
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
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Sat Apr 02 23:29:05 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Sun Apr 03 10:25:17 2016 +0200
@@ -191,10 +191,10 @@
   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 ->
+  val mk_xtor_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
     term list -> term list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list
-  val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
+  val mk_xtor_co_iter_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     thm list -> thm list -> thm list
 
   val fixpoint_bnf: (binding -> binding) ->
@@ -560,7 +560,7 @@
     |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
   end;
 
-fun mk_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy =
+fun mk_xtor_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy =
   let
     val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_iphis)) pre_rels;
     val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
@@ -579,7 +579,7 @@
     |> split_conj_thm
   end;
 
-fun mk_xtor_un_fold_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps
+fun mk_xtor_co_iter_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps
     map_cong0s =
   let
     val n = length sym_map_comps;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Sat Apr 02 23:29:05 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Sun Apr 03 10:25:17 2016 +0200
@@ -2630,10 +2630,10 @@
       |> mk_Frees "R" JphiTs
       ||>> mk_Frees "S" activephiTs;
 
-    val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m
+    val dtor_unfold_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP false m
       dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
       sym_map_comps map_cong0s;
-    val dtor_corec_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m
+    val dtor_corec_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP true m
       dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms)
       sym_map_comps map_cong0s;
 
@@ -2642,7 +2642,7 @@
       else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
 
     val dtor_unfold_transfer_thms =
-      mk_co_iter_transfer_thms Greatest_FP rels activephis activephis Jrels Jphis
+      mk_xtor_co_iter_transfer_thms Greatest_FP rels activephis activephis Jrels Jphis
         (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
         (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm
           (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
@@ -2654,7 +2654,7 @@
     val corec_activephis =
       map2 (fn Jrel => mk_rel_sum (Term.list_comb (Jrel, Jphis))) Jrels activephis;
     val dtor_corec_transfer_thms =
-      mk_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis
+      mk_xtor_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis
         (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs)
         (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs
            dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms)
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Sat Apr 02 23:29:05 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Apr 03 10:25:17 2016 +0200
@@ -1886,9 +1886,9 @@
       ||>> mk_Frees "S" activephiTs
       ||>> mk_Frees "IR" activeIphiTs;
 
-    val ctor_fold_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm
+    val ctor_fold_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP false m ctor_fold_unique_thm
       ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
-    val ctor_rec_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm
+    val ctor_rec_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP true m ctor_rec_unique_thm
       ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s;
 
     val Irels = if m = 0 then map HOLogic.eq_const Ts
@@ -1900,7 +1900,7 @@
 
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
     val ctor_fold_transfer_thms =
-      mk_co_iter_transfer_thms Least_FP rels activephis activephis Irels Iphis
+      mk_xtor_co_iter_transfer_thms Least_FP rels activephis activephis Irels Iphis
         (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
         (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm
           (map map_transfer_of_bnf bnfs) ctor_fold_thms)
@@ -1912,7 +1912,7 @@
     val rec_activephis =
       map2 (fn Irel => mk_rel_prod (Term.list_comb (Irel, Iphis))) Irels activephis;
     val ctor_rec_transfer_thms =
-      mk_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis
+      mk_xtor_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis
         (mk_recs Ts passiveAs activeAs) (mk_recs Ts' passiveBs activeBs)
         (fn {context = ctxt, prems = _} => mk_ctor_rec_transfer_tac ctxt n m rec_defs
            ctor_fold_transfer_thms (map map_transfer_of_bnf bnfs) ctor_Irel_thms)