--- a/src/HOL/Codatatype/BNF_FP.thy Mon Sep 17 21:13:30 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy Mon Sep 17 21:33:12 2012 +0200
@@ -104,39 +104,9 @@
"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
by simp
-lemma UN_compreh_bex_eq_empty:
-"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
-by blast
-
-lemma UN_compreh_bex_eq_singleton:
-"\<Union>{y. \<exists>x\<in>A. y = {f x}} = {y. \<exists>x\<in>A. y = f x}"
-by blast
-
-lemma mem_UN_comprehI:
-"z \<in> {y. \<exists>x\<in>A. y = f x} \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {f x}}"
-"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"
-"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}"
-"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"
-by blast+
-
-lemma mem_UN_comprehI':
-"\<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'}}"
-by blast
-
lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
by blast
-lemma eq_UN_compreh_Un: "(xa = \<Union>{y. \<exists>x\<in>A. y = c_set1 x \<union> c_set2 x}) =
- (xa = (\<Union>{y. \<exists>x\<in>A. y = c_set1 x} \<union> \<Union>{y. \<exists>x\<in>A. y = c_set2 x}))"
-by blast
-
-lemma mem_compreh_eq_iff:
-"z \<in> {y. \<exists>x\<in>A. y = f x} = (\<exists> x. x \<in> A & z \<in> {f x})"
-by blast
-
-lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)"
-by simp
-
lemma prod_set_simps:
"fsts (x, y) = {x}"
"snds (x, y) = {y}"
@@ -149,11 +119,6 @@
"sum_setr (Inr x) = {x}"
unfolding sum_setl_def sum_setr_def by simp+
-lemma induct_set_step:
-"\<lbrakk>b \<in> A; c \<in> F b\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> c \<in> F x"
-"\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and>c \<in> C"
-by blast+
-
ML_file "Tools/bnf_fp_util.ML"
ML_file "Tools/bnf_fp_sugar_tactics.ML"
ML_file "Tools/bnf_fp_sugar.ML"
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Mon Sep 17 21:13:30 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Mon Sep 17 21:33:12 2012 +0200
@@ -533,8 +533,6 @@
val live = length raw_sets;
val nwits = length raw_wits;
- val _ = tracing (Binding.name_of b)
-
val map_rhs = prep_term no_defs_lthy raw_map;
val set_rhss = map (prep_term no_defs_lthy) raw_sets;
val (bd_rhsT, bd_rhs) = (case prep_term no_defs_lthy raw_bd_Abs of
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Mon Sep 17 21:13:30 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Mon Sep 17 21:33:12 2012 +0200
@@ -95,11 +95,10 @@
(rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
val induct_prem_prem_thms =
- @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton
- UN_insert Un_assoc Un_empty_left Un_empty_right Un_iff Union_Un_distrib collect_def[abs_def]
- eq_UN_compreh_Un fst_conv image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right
- fst_map_pair map_pair_simp mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps
- sum_set_simps};
+ @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_assoc Un_empty_left Un_empty_right Un_iff
+ Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv snd_prod_fun
+ sum.cases sup_bot_right fst_map_pair map_pair_simp mem_Collect_eq mem_UN_compreh_eq
+ prod_set_simps sum_map.simps sum_set_simps};
fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,