clarified interaction with dead variables in the composition of BNFs

--- a/src/HOL/Basic_BNFs.thy	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy	Mon Feb 24 10:16:10 2014 +0100
@@ -25,11 +25,9 @@
 
 bnf DEADID: 'a
   map: "id :: 'a \<Rightarrow> 'a"
-  bd: "natLeq +c |UNIV :: 'a set|"
+  bd: natLeq
   rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
-by (auto simp add: Grp_def
-  card_order_csum natLeq_card_order card_of_card_order_on
-  cinfinite_csum natLeq_cinfinite)
+by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
 
 definition setl :: "'a + 'b \<Rightarrow> 'a set" where
 "setl x = (case x of Inl z => {z} | _ => {})"

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Feb 24 10:16:10 2014 +0100
@@ -301,10 +301,7 @@
     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
     val sets = drop n bnf_sets;
 
-    (*(|UNIV :: A1 set| +c ... +c |UNIV :: An set|) *c bnf.bd*)
-    val bnf_bd = mk_bd_of_bnf Ds As bnf;
-    val bd = mk_cprod
-      (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
+    val bd = mk_bd_of_bnf Ds As bnf;
 
     fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
     fun map_comp0_tac ctxt =
@@ -313,11 +310,9 @@
     fun map_cong0_tac ctxt =
       mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
     val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_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_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
-        (drop n (set_bd_of_bnf bnf));
+    fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
+    fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
+    val set_bd_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_bd_of_bnf bnf));
 
     val in_alt_thm =
       let
@@ -611,8 +606,9 @@
     (*bd may depend only on dead type variables*)
     val bd_repT = fst (dest_relT (fastype_of bnf_bd));
     val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b);
-    val params = fold Term.add_tfreesT Ds [];
+    val params = Term.add_tfreesT bd_repT [];
     val deads = map TFree params;
+    val all_deads = map TFree (fold Term.add_tfreesT Ds []);
 
     val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
       typedef (bdT_bind, params, NoSyn)
@@ -649,11 +645,11 @@
       mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
 
     val (bnf', lthy') =
-      bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)
+      bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME all_deads)
         Binding.empty Binding.empty []
         ((((((b, T), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   in
-    ((bnf', deads), lthy')
+    ((bnf', all_deads), lthy')
   end;
 
 fun key_of_types Ts = Type ("", Ts);

--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Feb 24 10:16:10 2014 +0100
@@ -19,11 +19,8 @@
   val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic
   val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> 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_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic
-  val mk_kill_set_bd_tac: thm -> thm -> tactic
 
   val empty_natural_tac: tactic
   val lift_in_alt_tac: tactic
@@ -42,10 +39,8 @@
 open BNF_Util
 open BNF_Tactics
 
-val Cnotzero_UNIV = @{thm Cnotzero_UNIV};
 val arg_cong_Union = @{thm arg_cong[of _ _ Union]};
 val comp_eq_dest_lhs = @{thm comp_eq_dest_lhs};
-val csum_Cnotzero1 = @{thm csum_Cnotzero1};
 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
 val trans_o_apply = @{thm trans[OF o_apply]};
 
@@ -180,28 +175,6 @@
   (rtac map_cong0 THEN' EVERY' (replicate n (rtac refl)) THEN'
     EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1;
 
-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'
-    rtac @{thm card_of_card_order_on}) 1)) THEN'
-  rtac @{thm card_of_card_order_on} THEN'
-  rtac bd_card_order) 1;
-
-fun mk_kill_bd_cinfinite_tac bd_Cinfinite =
-  (rtac @{thm cinfinite_cprod2} THEN'
-  TRY o rtac csum_Cnotzero1 THEN'
-  rtac Cnotzero_UNIV THEN'
-  rtac bd_Cinfinite) 1;
-
-fun mk_kill_set_bd_tac bd_Card_order set_bd =
-  (rtac ctrans THEN'
-  rtac set_bd THEN'
-  rtac @{thm ordLeq_cprod2} THEN'
-  TRY o rtac csum_Cnotzero1 THEN'
-  rtac Cnotzero_UNIV THEN'
-  rtac bd_Card_order) 1
-
 val kill_in_alt_tac =
   ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN
   REPEAT_DETERM (CHANGED (etac conjE 1)) THEN