1.1 --- a/NEWS	Mon Jul 25 14:10:12 2011 +0200
     1.2 +++ b/NEWS	Mon Jul 25 23:27:20 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	Mon Jul 25 14:10:12 2011 +0200
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Mon Jul 25 23:27:20 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/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jul 25 14:10:12 2011 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jul 25 23:27:20 2011 +0200
     3.3 @@ -2539,7 +2539,7 @@
     3.4    fixes s :: "'a::real_normed_vector set"
     3.5    assumes "open s"
     3.6    shows "open(convex hull s)"
     3.7 -  unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10)
     3.8 +  unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(8)
     3.9  proof(rule, rule) fix a
    3.10    assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a"
    3.11    then obtain t u where obt:"finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a" by auto

     4.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Jul 25 14:10:12 2011 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Jul 25 23:27:20 2011 +0200
     4.3 @@ -2505,7 +2505,7 @@
     4.4        by auto
     4.5      from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
     4.6      have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
     4.7 -    from "2.prems"(2)[unfolded dependent_def bex_simps(10), rule_format, of "f a"]
     4.8 +    from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
     4.9      have "f a \<notin> span (f ` b)" using tha
    4.10        using "2.hyps"(2)
    4.11        "2.prems"(3) by auto

     5.1 --- a/src/HOL/Set.thy	Mon Jul 25 14:10:12 2011 +0200
     5.2 +++ b/src/HOL/Set.thy	Mon Jul 25 23:27:20 2011 +0200
     5.3 @@ -1540,6 +1540,30 @@
     5.4  lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
     5.5    by iprover
     5.6  
     5.7 +lemma ball_simps [simp, no_atp]:
     5.8 +  "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"
     5.9 +  "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"
    5.10 +  "\<And>A P Q. (\<forall>x\<in>A. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q x))"
    5.11 +  "\<And>A P Q. (\<forall>x\<in>A. P x \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<longrightarrow> Q)"
    5.12 +  "\<And>P. (\<forall>x\<in>{}. P x) \<longleftrightarrow> True"
    5.13 +  "\<And>P. (\<forall>x\<in>UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
    5.14 +  "\<And>a B P. (\<forall>x\<in>insert a B. P x) \<longleftrightarrow> (P a \<and> (\<forall>x\<in>B. P x))"
    5.15 +  "\<And>P Q. (\<forall>x\<in>Collect Q. P x) \<longleftrightarrow> (\<forall>x. Q x \<longrightarrow> P x)"
    5.16 +  "\<And>A P f. (\<forall>x\<in>f`A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P (f x))"
    5.17 +  "\<And>A P. (\<not> (\<forall>x\<in>A. P x)) \<longleftrightarrow> (\<exists>x\<in>A. \<not> P x)"
    5.18 +  by auto
    5.19 +
    5.20 +lemma bex_simps [simp, no_atp]:
    5.21 +  "\<And>A P Q. (\<exists>x\<in>A. P x \<and> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<and> Q)"
    5.22 +  "\<And>A P Q. (\<exists>x\<in>A. P \<and> Q x) \<longleftrightarrow> (P \<and> (\<exists>x\<in>A. Q x))"
    5.23 +  "\<And>P. (\<exists>x\<in>{}. P x) \<longleftrightarrow> False"
    5.24 +  "\<And>P. (\<exists>x\<in>UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
    5.25 +  "\<And>a B P. (\<exists>x\<in>insert a B. P x) \<longleftrightarrow> (P a | (\<exists>x\<in>B. P x))"
    5.26 +  "\<And>P Q. (\<exists>x\<in>Collect Q. P x) \<longleftrightarrow> (\<exists>x. Q x \<and> P x)"
    5.27 +  "\<And>A P f. (\<exists>x\<in>f`A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"
    5.28 +  "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
    5.29 +  by auto
    5.30 +
    5.31  
    5.32  subsubsection {* Monotonicity of various operations *}
    5.33