src/HOL/Codatatype/BNF_FP.thy
changeset 49430 6df729c6a1a6
parent 49429 64ac3471005a
child 49451 7a28d22c33c6
     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"