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
```