# HG changeset patch
# User blanchet
# Date 1347408304 -7200
# Node ID 6964373dd6ac7d0e67c9fad1082eb020406ec3f4
# Parent  c87930fb5b90226b7b3aa78554182491bbbcc576
tuning

diff -r c87930fb5b90 -r 6964373dd6ac src/HOL/Codatatype/Tools/bnf_comp.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Wed Sep 12 02:05:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Wed Sep 12 02:05:04 2012 +0200
@@ -284,7 +284,7 @@
 
 (* Killing live variables *)
 
-fun killN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
+fun kill_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
   let
     val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf);
     val live = live_of_bnf bnf;
@@ -323,12 +323,12 @@
       Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
       rtac refl 1;
     fun map_cong_tac {context, ...} =
-      mk_killN_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
+      mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
     val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
-    fun bd_card_order_tac _ = mk_killN_bd_card_order_tac n (bd_card_order_of_bnf bnf);
-    fun bd_cinfinite_tac _ = mk_killN_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
+    fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
+    fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
     val set_bd_tacs =
-      map (fn thm => fn _ => mk_killN_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
+      map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
         (drop n (set_bd_of_bnf bnf));
 
     val in_alt_thm =
@@ -337,11 +337,11 @@
         val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
       in
-        Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation
+        Skip_Proof.prove lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
       end;
 
     fun in_bd_tac _ =
-      mk_killN_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf)
+      mk_kill_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf)
         (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
@@ -383,7 +383,7 @@
 
 (* Adding dummy live variables *)
 
-fun liftN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
+fun lift_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
   let
     val b = Binding.prefix_name (mk_liftN n) (name_of_bnf bnf);
     val live = live_of_bnf bnf;
@@ -431,7 +431,7 @@
       if ! quick_and_dirty then
         replicate (n + live) (K all_tac)
       else
-        replicate n (K (mk_liftN_set_bd_tac (bd_Card_order_of_bnf bnf))) @
+        replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @
         (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
 
     val in_alt_thm =
@@ -440,10 +440,10 @@
         val in_alt = mk_in (drop n Asets) bnf_sets T;
         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
       in
-        Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation
+        Skip_Proof.prove lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation
       end;
 
-    fun in_bd_tac _ = mk_liftN_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
+    fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
     val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac,
@@ -555,11 +555,11 @@
 fun permute_and_kill qualify n src dest bnf =
   bnf
   |> permute_bnf qualify src dest
-  #> uncurry (killN_bnf qualify n);
+  #> uncurry (kill_bnf qualify n);
 
 fun lift_and_permute qualify n src dest bnf =
   bnf
-  |> liftN_bnf qualify n
+  |> lift_bnf qualify n
   #> uncurry (permute_bnf qualify src dest);
 
 fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy =
diff -r c87930fb5b90 -r 6964373dd6ac src/HOL/Codatatype/Tools/bnf_comp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Wed Sep 12 02:05:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Wed Sep 12 02:05:04 2012 +0200
@@ -19,17 +19,17 @@
   val mk_comp_set_natural_tac: thm -> thm -> thm -> thm list -> tactic
   val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
 
-  val mk_killN_bd_card_order_tac: int -> thm -> tactic
-  val mk_killN_bd_cinfinite_tac: thm -> tactic
-  val killN_in_alt_tac: tactic
-  val mk_killN_in_bd_tac: int -> bool -> thm -> thm -> thm -> thm -> thm -> tactic
-  val mk_killN_map_cong_tac: Proof.context -> int -> int -> thm -> tactic
-  val mk_killN_set_bd_tac: thm -> thm -> tactic
+  val mk_kill_bd_card_order_tac: int -> thm -> tactic
+  val mk_kill_bd_cinfinite_tac: thm -> tactic
+  val kill_in_alt_tac: tactic
+  val mk_kill_in_bd_tac: int -> bool -> thm -> thm -> thm -> thm -> thm -> tactic
+  val mk_kill_map_cong_tac: Proof.context -> int -> int -> thm -> tactic
+  val mk_kill_set_bd_tac: thm -> thm -> tactic
 
   val empty_natural_tac: tactic
-  val liftN_in_alt_tac: tactic
-  val mk_liftN_in_bd_tac: int -> thm -> thm -> thm -> tactic
-  val mk_liftN_set_bd_tac: thm -> tactic
+  val lift_in_alt_tac: tactic
+  val mk_lift_in_bd_tac: int -> thm -> thm -> thm -> tactic
+  val mk_lift_set_bd_tac: thm -> tactic
 
   val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic
   val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic
@@ -220,11 +220,11 @@
 
 (* Kill operation *)
 
-fun mk_killN_map_cong_tac ctxt n m map_cong =
+fun mk_kill_map_cong_tac ctxt n m map_cong =
   (rtac map_cong THEN' EVERY' (replicate n (rtac refl)) THEN'
     EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1;
 
-fun mk_killN_bd_card_order_tac n bd_card_order =
+fun mk_kill_bd_card_order_tac n bd_card_order =
   (rtac @{thm card_order_cprod} THEN'
   K (REPEAT_DETERM_N (n - 1)
     ((rtac @{thm card_order_csum} THEN'
@@ -232,13 +232,13 @@
   rtac @{thm card_of_card_order_on} THEN'
   rtac bd_card_order) 1;
 
-fun mk_killN_bd_cinfinite_tac bd_Cinfinite =
+fun mk_kill_bd_cinfinite_tac bd_Cinfinite =
   (rtac @{thm cinfinite_cprod2} THEN'
   TRY o rtac @{thm csum_Cnotzero1} THEN'
   rtac @{thm Cnotzero_UNIV} THEN'
   rtac bd_Cinfinite) 1;
 
-fun mk_killN_set_bd_tac bd_Card_order set_bd =
+fun mk_kill_set_bd_tac bd_Card_order set_bd =
   (rtac ctrans THEN'
   rtac set_bd THEN'
   rtac @{thm ordLeq_cprod2} THEN'
@@ -246,7 +246,7 @@
   rtac @{thm Cnotzero_UNIV} THEN'
   rtac bd_Card_order) 1
 
-val killN_in_alt_tac =
+val kill_in_alt_tac =
   ((rtac @{thm Collect_cong} THEN' rtac @{thm iffI}) 1 THEN
   REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
   REPEAT_DETERM (CHANGED ((etac conjI ORELSE'
@@ -257,7 +257,7 @@
   ((rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN
     REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm subset_UNIV} 1));
 
-fun mk_killN_in_bd_tac n nontrivial_killN_in in_alt in_bd bd_Card_order bd_Cinfinite bd_Cnotzero =
+fun mk_kill_in_bd_tac n nontrivial_kill_in in_alt in_bd bd_Card_order bd_Cinfinite bd_Cnotzero =
   (rtac @{thm ordIso_ordLeq_trans} THEN'
   rtac @{thm card_of_ordIso_subst} THEN'
   rtac in_alt THEN'
@@ -265,7 +265,7 @@
   rtac in_bd THEN'
   rtac @{thm ordIso_ordLeq_trans} THEN'
   rtac @{thm cexp_cong1}) 1 THEN
-  (if nontrivial_killN_in then
+  (if nontrivial_kill_in then
     rtac @{thm ordIso_transitive} 1 THEN
     REPEAT_DETERM_N (n - 1)
       ((rtac @{thm csum_cong1} THEN'
@@ -333,9 +333,9 @@
 
 val empty_natural_tac = rtac @{thm empty_natural} 1;
 
-fun mk_liftN_set_bd_tac bd_Card_order = (rtac @{thm Card_order_empty} THEN' rtac bd_Card_order) 1;
+fun mk_lift_set_bd_tac bd_Card_order = (rtac @{thm Card_order_empty} THEN' rtac bd_Card_order) 1;
 
-val liftN_in_alt_tac =
+val lift_in_alt_tac =
   ((rtac @{thm Collect_cong} THEN' rtac @{thm iffI}) 1 THEN
   REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
   REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1)) THEN
@@ -346,7 +346,7 @@
   ((rtac sym THEN' rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN
     REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm empty_subsetI} 1));
 
-fun mk_liftN_in_bd_tac n in_alt in_bd bd_Card_order =
+fun mk_lift_in_bd_tac n in_alt in_bd bd_Card_order =
   (rtac @{thm ordIso_ordLeq_trans} THEN'
   rtac @{thm card_of_ordIso_subst} THEN'
   rtac in_alt THEN'