1.1 --- a/NEWS	Sat Jul 23 23:33:59 2011 +0200
     1.2 +++ b/NEWS	Sun Jul 24 21:27:25 2011 +0200
     1.3 @@ -79,6 +79,10 @@
     1.4    SUPR_apply ~> SUP_apply
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Theorem collections ball_simps and bex_simps do not contain theorems referring
     1.8 +to UNION any longer;  these have been moved to collection UN_ball_bex_simps.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * Archimedian_Field.thy:
    1.12      floor now is defined as parameter of a separate type class floor_ceiling.
    1.13   

     2.1 --- a/src/HOL/Complete_Lattice.thy	Sat Jul 23 23:33:59 2011 +0200
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 24 21:27:25 2011 +0200
     2.3 @@ -476,6 +476,14 @@
     2.4    from dual.Sup_eq_top_iff show ?thesis .
     2.5  qed
     2.6  
     2.7 +lemma INF_eq_bot_iff:
     2.8 +  "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
     2.9 +  unfolding INF_def Inf_eq_bot_iff by auto
    2.10 +
    2.11 +lemma SUP_eq_top_iff:
    2.12 +  "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
    2.13 +  unfolding SUP_def Sup_eq_top_iff by auto
    2.14 +
    2.15  end
    2.16  
    2.17  
    2.18 @@ -929,7 +937,7 @@
    2.19  lemma UN_Un[simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
    2.20    by (fact SUP_union)
    2.21  
    2.22 -lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)" -- "FIXME generalize"
    2.23 +lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)"
    2.24    by blast
    2.25  
    2.26  lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
    2.27 @@ -1067,44 +1075,13 @@
    2.28    "\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
    2.29    by auto
    2.30  
    2.31 -lemma ball_simps [simp,no_atp]:
    2.32 -  "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"
    2.33 -  "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"
    2.34 -  "\<And>A P Q. (\<forall>x\<in>A. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q x))"
    2.35 -  "\<And>A P Q. (\<forall>x\<in>A. P x \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<longrightarrow> Q)"
    2.36 -  "\<And>P. (\<forall>x\<in>{}. P x) \<longleftrightarrow> True"
    2.37 -  "\<And>P. (\<forall>x\<in>UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
    2.38 -  "\<And>a B P. (\<forall>x\<in>insert a B. P x) \<longleftrightarrow> (P a \<and> (\<forall>x\<in>B. P x))"
    2.39 +lemma UN_ball_bex_simps [simp, no_atp]:
    2.40    "\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
    2.41 -  "\<And>A B P. (\<forall>x\<in> UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
    2.42 -  "\<And>P Q. (\<forall>x\<in>Collect Q. P x) \<longleftrightarrow> (\<forall>x. Q x \<longrightarrow> P x)"
    2.43 -  "\<And>A P f. (\<forall>x\<in>f`A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P (f x))"
    2.44 -  "\<And>A P. (\<not> (\<forall>x\<in>A. P x)) \<longleftrightarrow> (\<exists>x\<in>A. \<not> P x)"
    2.45 -  by auto
    2.46 -
    2.47 -lemma bex_simps [simp,no_atp]:
    2.48 -  "\<And>A P Q. (\<exists>x\<in>A. P x \<and> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<and> Q)"
    2.49 -  "\<And>A P Q. (\<exists>x\<in>A. P \<and> Q x) \<longleftrightarrow> (P \<and> (\<exists>x\<in>A. Q x))"
    2.50 -  "\<And>P. (\<exists>x\<in>{}. P x) \<longleftrightarrow> False"
    2.51 -  "\<And>P. (\<exists>x\<in>UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
    2.52 -  "\<And>a B P. (\<exists>x\<in>insert a B. P x) \<longleftrightarrow> (P a | (\<exists>x\<in>B. P x))"
    2.53 +  "\<And>A B P. (\<forall>x\<in>UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
    2.54    "\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
    2.55    "\<And>A B P. (\<exists>x\<in>UNION A B. P x) \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x\<in>B a. P x)"
    2.56 -  "\<And>P Q. (\<exists>x\<in>Collect Q. P x) \<longleftrightarrow> (\<exists>x. Q x \<and> P x)"
    2.57 -  "\<And>A P f. (\<exists>x\<in>f`A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"
    2.58 -  "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
    2.59    by auto
    2.60  
    2.61 -lemma (in complete_linorder) INF_eq_bot_iff:
    2.62 -  fixes f :: "'b \<Rightarrow> 'a"
    2.63 -  shows "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
    2.64 -  unfolding INF_def Inf_eq_bot_iff by auto
    2.65 -
    2.66 -lemma (in complete_linorder) SUP_eq_top_iff:
    2.67 -  fixes f :: "'b \<Rightarrow> 'a"
    2.68 -  shows "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
    2.69 -  unfolding SUP_def Sup_eq_top_iff by auto
    2.70 -
    2.71  
    2.72  text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
    2.73  

     3.1 --- a/src/HOL/Set.thy	Sat Jul 23 23:33:59 2011 +0200
     3.2 +++ b/src/HOL/Set.thy	Sun Jul 24 21:27:25 2011 +0200
     3.3 @@ -1540,6 +1540,30 @@
     3.4  lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
     3.5    by iprover
     3.6  
     3.7 +lemma ball_simps [simp, no_atp]:
     3.8 +  "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"
     3.9 +  "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"
    3.10 +  "\<And>A P Q. (\<forall>x\<in>A. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q x))"
    3.11 +  "\<And>A P Q. (\<forall>x\<in>A. P x \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<longrightarrow> Q)"
    3.12 +  "\<And>P. (\<forall>x\<in>{}. P x) \<longleftrightarrow> True"
    3.13 +  "\<And>P. (\<forall>x\<in>UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
    3.14 +  "\<And>a B P. (\<forall>x\<in>insert a B. P x) \<longleftrightarrow> (P a \<and> (\<forall>x\<in>B. P x))"
    3.15 +  "\<And>P Q. (\<forall>x\<in>Collect Q. P x) \<longleftrightarrow> (\<forall>x. Q x \<longrightarrow> P x)"
    3.16 +  "\<And>A P f. (\<forall>x\<in>f`A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P (f x))"
    3.17 +  "\<And>A P. (\<not> (\<forall>x\<in>A. P x)) \<longleftrightarrow> (\<exists>x\<in>A. \<not> P x)"
    3.18 +  by auto
    3.19 +
    3.20 +lemma bex_simps [simp, no_atp]:
    3.21 +  "\<And>A P Q. (\<exists>x\<in>A. P x \<and> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<and> Q)"
    3.22 +  "\<And>A P Q. (\<exists>x\<in>A. P \<and> Q x) \<longleftrightarrow> (P \<and> (\<exists>x\<in>A. Q x))"
    3.23 +  "\<And>P. (\<exists>x\<in>{}. P x) \<longleftrightarrow> False"
    3.24 +  "\<And>P. (\<exists>x\<in>UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
    3.25 +  "\<And>a B P. (\<exists>x\<in>insert a B. P x) \<longleftrightarrow> (P a | (\<exists>x\<in>B. P x))"
    3.26 +  "\<And>P Q. (\<exists>x\<in>Collect Q. P x) \<longleftrightarrow> (\<exists>x. Q x \<and> P x)"
    3.27 +  "\<And>A P f. (\<exists>x\<in>f`A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"
    3.28 +  "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
    3.29 +  by auto
    3.30 +
    3.31  
    3.32  subsubsection {* Monotonicity of various operations *}
    3.33