1.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 21:13:30 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 21:33:12 2012 +0200
     1.3 @@ -104,39 +104,9 @@
     1.4  "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
     1.5  by simp
     1.6  
     1.7 -lemma UN_compreh_bex_eq_empty:
     1.8 -"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
     1.9 -by blast
    1.10 -
    1.11 -lemma UN_compreh_bex_eq_singleton:
    1.12 -"\<Union>{y. \<exists>x\<in>A. y = {f x}} = {y. \<exists>x\<in>A. y = f x}"
    1.13 -by blast
    1.14 -
    1.15 -lemma mem_UN_comprehI:
    1.16 -"z \<in> {y. \<exists>x\<in>A. y = f x} \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {f x}}"
    1.17 -"z \<in> {y. \<exists>x\<in>A. y = f x} \<union> B \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {f x}} \<union> B"
    1.18 -"z \<in> \<Union>{y. \<exists>x\<in>A. y = F x} \<union> \<Union>{y. \<exists>x\<in>A. y = G x} \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = F x \<union> G x}"
    1.19 -"z \<in> \<Union>{y. \<exists>x\<in>A. y = F x} \<union> (\<Union>{y. \<exists>x\<in>A. y = G x} \<union> B) \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = F x \<union> G x} \<union> B"
    1.20 -by blast+
    1.21 -
    1.22 -lemma mem_UN_comprehI':
    1.23 -"\<exists>y. (\<exists>x\<in>A. y = F x) \<and> z \<in> y \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {y. \<exists>y'\<in>F x. y = y'}}"
    1.24 -by blast
    1.25 -
    1.26  lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
    1.27  by blast
    1.28  
    1.29 -lemma eq_UN_compreh_Un: "(xa = \<Union>{y. \<exists>x\<in>A. y = c_set1 x \<union> c_set2 x}) =
    1.30 -  (xa = (\<Union>{y. \<exists>x\<in>A. y = c_set1 x} \<union> \<Union>{y. \<exists>x\<in>A. y = c_set2 x}))"
    1.31 -by blast
    1.32 -
    1.33 -lemma mem_compreh_eq_iff:
    1.34 -"z \<in> {y. \<exists>x\<in>A. y = f x} = (\<exists> x. x \<in> A & z \<in> {f x})"
    1.35 -by blast
    1.36 -
    1.37 -lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)"
    1.38 -by simp
    1.39 -
    1.40  lemma prod_set_simps:
    1.41  "fsts (x, y) = {x}"
    1.42  "snds (x, y) = {y}"
    1.43 @@ -149,11 +119,6 @@
    1.44  "sum_setr (Inr x) = {x}"
    1.45  unfolding sum_setl_def sum_setr_def by simp+
    1.46  
    1.47 -lemma induct_set_step:
    1.48 -"\<lbrakk>b \<in> A; c \<in> F b\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> c \<in> F x"
    1.49 -"\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and>c \<in> C"
    1.50 -by blast+
    1.51 -
    1.52  ML_file "Tools/bnf_fp_util.ML"
    1.53  ML_file "Tools/bnf_fp_sugar_tactics.ML"
    1.54  ML_file "Tools/bnf_fp_sugar.ML"

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Mon Sep 17 21:13:30 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Mon Sep 17 21:33:12 2012 +0200
     2.3 @@ -533,8 +533,6 @@
     2.4      val live = length raw_sets;
     2.5      val nwits = length raw_wits;
     2.6  
     2.7 -    val _ = tracing (Binding.name_of b)
     2.8 -
     2.9      val map_rhs = prep_term no_defs_lthy raw_map;
    2.10      val set_rhss = map (prep_term no_defs_lthy) raw_sets;
    2.11      val (bd_rhsT, bd_rhs) = (case prep_term no_defs_lthy raw_bd_Abs of

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:33:12 2012 +0200
     3.3 @@ -95,11 +95,10 @@
     3.4    (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
     3.5  
     3.6  val induct_prem_prem_thms =
     3.7 -  @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton
     3.8 -      UN_insert Un_assoc Un_empty_left Un_empty_right Un_iff Union_Un_distrib collect_def[abs_def]
     3.9 -      eq_UN_compreh_Un fst_conv image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right
    3.10 -      fst_map_pair map_pair_simp mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps
    3.11 -      sum_set_simps};
    3.12 +  @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_assoc Un_empty_left Un_empty_right Un_iff
    3.13 +      Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv snd_prod_fun
    3.14 +      sum.cases sup_bot_right fst_map_pair map_pair_simp mem_Collect_eq mem_UN_compreh_eq
    3.15 +      prod_set_simps sum_map.simps sum_set_simps};
    3.16  
    3.17  fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
    3.18    EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,