1.1 --- a/src/HOL/Complete_Lattice.thy	Thu Jul 21 21:56:24 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Thu Jul 21 22:47:13 2011 +0200
     1.3 @@ -356,6 +356,24 @@
     1.4   "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
     1.5    by (auto simp add: SUP_def Sup_bot_conv)
     1.6  
     1.7 +lemma less_INF_D:
     1.8 +  assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
     1.9 +proof -
    1.10 +  note `y < (\<Sqinter>i\<in>A. f i)`
    1.11 +  also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using `i \<in> A`
    1.12 +    by (rule INF_leI)
    1.13 +  finally show "y < f i" .
    1.14 +qed
    1.15 +
    1.16 +lemma SUP_lessD:
    1.17 +  assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
    1.18 +proof -
    1.19 +  have "f i \<le> (\<Squnion>i\<in>A. f i)" using `i \<in> A`
    1.20 +    by (rule le_SUP_I)
    1.21 +  also note `(\<Squnion>i\<in>A. f i) < y`
    1.22 +  finally show "f i < y" .
    1.23 +qed
    1.24 +
    1.25  lemma INF_UNIV_range:
    1.26    "(\<Sqinter>x. f x) = \<Sqinter>range f"
    1.27    by (fact INF_def)
    1.28 @@ -377,6 +395,10 @@
    1.29  class complete_boolean_algebra = boolean_algebra + complete_lattice
    1.30  begin
    1.31  
    1.32 +lemma dual_complete_boolean_algebra:
    1.33 +  "class.complete_boolean_algebra Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
    1.34 +  by (rule class.complete_boolean_algebra.intro, rule dual_complete_lattice, rule dual_boolean_algebra)
    1.35 +
    1.36  lemma uminus_Inf:
    1.37    "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
    1.38  proof (rule antisym)
    1.39 @@ -404,6 +426,10 @@
    1.40  class complete_linorder = linorder + complete_lattice
    1.41  begin
    1.42  
    1.43 +lemma dual_complete_linorder:
    1.44 +  "class.complete_linorder Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
    1.45 +  by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
    1.46 +
    1.47  lemma Inf_less_iff:
    1.48    "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
    1.49    unfolding not_le [symmetric] le_Inf_iff by auto
    1.50 @@ -420,6 +446,36 @@
    1.51    "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
    1.52    unfolding SUP_def less_Sup_iff by auto
    1.53  
    1.54 +lemma Sup_eq_top_iff:
    1.55 +  "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
    1.56 +proof
    1.57 +  assume *: "\<Squnion>A = \<top>"
    1.58 +  show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
    1.59 +  proof (intro allI impI)
    1.60 +    fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
    1.61 +      unfolding less_Sup_iff by auto
    1.62 +  qed
    1.63 +next
    1.64 +  assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i"
    1.65 +  show "\<Squnion>A = \<top>"
    1.66 +  proof (rule ccontr)
    1.67 +    assume "\<Squnion>A \<noteq> \<top>"
    1.68 +    with top_greatest [of "\<Squnion>A"]
    1.69 +    have "\<Squnion>A < \<top>" unfolding le_less by auto
    1.70 +    then have "\<Squnion>A < \<Squnion>A"
    1.71 +      using * unfolding less_Sup_iff by auto
    1.72 +    then show False by auto
    1.73 +  qed
    1.74 +qed
    1.75 +
    1.76 +lemma Inf_eq_bot_iff:
    1.77 +  "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
    1.78 +proof -
    1.79 +  interpret dual: complete_linorder Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
    1.80 +    by (fact dual_complete_linorder)
    1.81 +  from dual.Sup_eq_top_iff show ?thesis .
    1.82 +qed
    1.83 +
    1.84  end
    1.85  
    1.86  
    1.87 @@ -1039,6 +1095,17 @@
    1.88    "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
    1.89    by auto
    1.90  
    1.91 +lemma (in complete_linorder) INF_eq_bot_iff:
    1.92 +  fixes f :: "'b \<Rightarrow> 'a"
    1.93 +  shows "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
    1.94 +  unfolding INF_def Inf_eq_bot_iff by auto
    1.95 +
    1.96 +lemma (in complete_linorder) SUP_eq_top_iff:
    1.97 +  fixes f :: "'b \<Rightarrow> 'a"
    1.98 +  shows "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
    1.99 +  unfolding SUP_def Sup_eq_top_iff by auto
   1.100 +
   1.101 +
   1.102  text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
   1.103  
   1.104  lemma UN_extend_simps:
   1.105 @@ -1075,6 +1142,7 @@
   1.106  lemmas (in complete_lattice) le_SUPI = le_SUP_I
   1.107  lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
   1.108  lemmas (in complete_lattice) le_INFI = le_INF_I
   1.109 +lemmas (in complete_lattice) less_INFD = less_INF_D
   1.110  
   1.111  lemma (in complete_lattice) INF_subset:
   1.112    "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"

     2.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Jul 21 21:56:24 2011 +0200
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 21 22:47:13 2011 +0200
     2.3 @@ -1338,33 +1338,6 @@
     2.4      by (cases e) auto
     2.5  qed
     2.6  
     2.7 -lemma (in complete_linorder) Sup_eq_top_iff: -- "FIXME move"
     2.8 -  "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)"
     2.9 -proof
    2.10 -  assume *: "Sup A = top"
    2.11 -  show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
    2.12 -  proof (intro allI impI)
    2.13 -    fix x assume "x < Sup A" then show "\<exists>i\<in>A. x < i"
    2.14 -      unfolding less_Sup_iff by auto
    2.15 -  qed
    2.16 -next
    2.17 -  assume *: "\<forall>x<top. \<exists>i\<in>A. x < i"
    2.18 -  show "Sup A = top"
    2.19 -  proof (rule ccontr)
    2.20 -    assume "Sup A \<noteq> top"
    2.21 -    with top_greatest [of "Sup A"]
    2.22 -    have "Sup A < top" unfolding le_less by auto
    2.23 -    then have "Sup A < Sup A"
    2.24 -      using * unfolding less_Sup_iff by auto
    2.25 -    then show False by auto
    2.26 -  qed
    2.27 -qed
    2.28 -
    2.29 -lemma (in complete_linorder) SUP_eq_top_iff: -- "FIXME move"
    2.30 -  fixes f :: "'b \<Rightarrow> 'a"
    2.31 -  shows "(SUP i:A. f i) = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < f i)"
    2.32 -  unfolding SUPR_def Sup_eq_top_iff by auto
    2.33 -
    2.34  lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
    2.35  proof -
    2.36    { fix x ::ereal assume "x \<noteq> \<infinity>"
    2.37 @@ -2374,14 +2347,6 @@
    2.38  
    2.39  abbreviation "limsup \<equiv> Limsup sequentially"
    2.40  
    2.41 -lemma (in complete_lattice) less_INFD:
    2.42 -  assumes "y < INFI A f"" i \<in> A" shows "y < f i"
    2.43 -proof -
    2.44 -  note `y < INFI A f`
    2.45 -  also have "INFI A f \<le> f i" using `i \<in> A` by (rule INF_leI)
    2.46 -  finally show "y < f i" .
    2.47 -qed
    2.48 -
    2.49  lemma liminf_SUPR_INFI:
    2.50    fixes f :: "nat \<Rightarrow> ereal"
    2.51    shows "liminf f = (SUP n. INF m:{n..}. f m)"