1.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 16:57:22 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 21:13:30 2012 +0200
     1.3 @@ -104,11 +104,25 @@
     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:
     1.8 -"\<Union>{y. \<exists>x \<in> A. y = {}} = {}"
     1.9 -"\<Union>{y. \<exists>x \<in> A. y = {f x}} = {y. \<exists>x \<in> A. y = f x}"
    1.10 +lemma UN_compreh_bex_eq_empty:
    1.11 +"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
    1.12 +by blast
    1.13 +
    1.14 +lemma UN_compreh_bex_eq_singleton:
    1.15 +"\<Union>{y. \<exists>x\<in>A. y = {f x}} = {y. \<exists>x\<in>A. y = f x}"
    1.16 +by blast
    1.17 +
    1.18 +lemma mem_UN_comprehI:
    1.19 +"z \<in> {y. \<exists>x\<in>A. y = f x} \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {f x}}"
    1.20 +"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.21 +"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.22 +"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.23  by blast+
    1.24  
    1.25 +lemma mem_UN_comprehI':
    1.26 +"\<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.27 +by blast
    1.28 +
    1.29  lemma induct_set_step: "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and> c \<in> C"
    1.30  apply (rule exI)
    1.31  apply (rule conjI)