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"