src/HOL/BNF_FP_Base.thy
changeset 55906 abf91ebd0820
parent 55854 ee270328a781
child 55930 25a90cebbbe5
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Tue Mar 04 18:57:17 2014 +0100
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Tue Mar 04 18:57:17 2014 +0100
     1.3 @@ -83,14 +83,6 @@
     1.4  "case_sum 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 mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
     1.8 -by blast
     1.9 -
    1.10 -lemma UN_compreh_eq_eq:
    1.11 -"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
    1.12 -"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
    1.13 -by blast+
    1.14 -
    1.15  lemma Inl_Inr_False: "(Inl x = Inr y) = False"
    1.16  by simp
    1.17  
    1.18 @@ -106,6 +98,13 @@
    1.19  "setr (Inr x) = {x}"
    1.20  unfolding sum_set_defs by simp+
    1.21  
    1.22 +lemma UN_compreh_eq_eq:
    1.23 +"\<Union>{y. y = A} = A"
    1.24 +by blast+
    1.25 +
    1.26 +lemma ex_in_single: "(\<exists>x \<in> {y}. P x) = P y"
    1.27 +by blast
    1.28 +
    1.29  lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
    1.30  by blast
    1.31