# HG changeset patch
# User haftmann
# Date 1311281233 -7200
# Node ID e6928fc2332a5b7bd27e629b7ac9220f5d0b9473
# Parent  3406cd754dd28a783d3a3c867312ae417e4a3ef5
moved some lemmas

diff -r 3406cd754dd2 -r e6928fc2332a src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Thu Jul 21 21:56:24 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Thu Jul 21 22:47:13 2011 +0200
@@ -356,6 +356,24 @@
  "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   by (auto simp add: SUP_def Sup_bot_conv)
 
+lemma less_INF_D:
+  assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
+proof -
+  note `y < (\<Sqinter>i\<in>A. f i)`
+  also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using `i \<in> A`
+    by (rule INF_leI)
+  finally show "y < f i" .
+qed
+
+lemma SUP_lessD:
+  assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
+proof -
+  have "f i \<le> (\<Squnion>i\<in>A. f i)" using `i \<in> A`
+    by (rule le_SUP_I)
+  also note `(\<Squnion>i\<in>A. f i) < y`
+  finally show "f i < y" .
+qed
+
 lemma INF_UNIV_range:
   "(\<Sqinter>x. f x) = \<Sqinter>range f"
   by (fact INF_def)
@@ -377,6 +395,10 @@
 class complete_boolean_algebra = boolean_algebra + complete_lattice
 begin
 
+lemma dual_complete_boolean_algebra:
+  "class.complete_boolean_algebra Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
+  by (rule class.complete_boolean_algebra.intro, rule dual_complete_lattice, rule dual_boolean_algebra)
+
 lemma uminus_Inf:
   "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
 proof (rule antisym)
@@ -404,6 +426,10 @@
 class complete_linorder = linorder + complete_lattice
 begin
 
+lemma dual_complete_linorder:
+  "class.complete_linorder Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
+  by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
+
 lemma Inf_less_iff:
   "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   unfolding not_le [symmetric] le_Inf_iff by auto
@@ -420,6 +446,36 @@
   "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   unfolding SUP_def less_Sup_iff by auto
 
+lemma Sup_eq_top_iff:
+  "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
+proof
+  assume *: "\<Squnion>A = \<top>"
+  show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
+  proof (intro allI impI)
+    fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
+      unfolding less_Sup_iff by auto
+  qed
+next
+  assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i"
+  show "\<Squnion>A = \<top>"
+  proof (rule ccontr)
+    assume "\<Squnion>A \<noteq> \<top>"
+    with top_greatest [of "\<Squnion>A"]
+    have "\<Squnion>A < \<top>" unfolding le_less by auto
+    then have "\<Squnion>A < \<Squnion>A"
+      using * unfolding less_Sup_iff by auto
+    then show False by auto
+  qed
+qed
+
+lemma Inf_eq_bot_iff:
+  "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
+proof -
+  interpret dual: complete_linorder Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
+    by (fact dual_complete_linorder)
+  from dual.Sup_eq_top_iff show ?thesis .
+qed
+
 end
 
 
@@ -1039,6 +1095,17 @@
   "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
   by auto
 
+lemma (in complete_linorder) INF_eq_bot_iff:
+  fixes f :: "'b \<Rightarrow> 'a"
+  shows "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
+  unfolding INF_def Inf_eq_bot_iff by auto
+
+lemma (in complete_linorder) SUP_eq_top_iff:
+  fixes f :: "'b \<Rightarrow> 'a"
+  shows "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
+  unfolding SUP_def Sup_eq_top_iff by auto
+
+
 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
 
 lemma UN_extend_simps:
@@ -1075,6 +1142,7 @@
 lemmas (in complete_lattice) le_SUPI = le_SUP_I
 lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
 lemmas (in complete_lattice) le_INFI = le_INF_I
+lemmas (in complete_lattice) less_INFD = less_INF_D
 
 lemma (in complete_lattice) INF_subset:
   "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
diff -r 3406cd754dd2 -r e6928fc2332a src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jul 21 21:56:24 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 21 22:47:13 2011 +0200
@@ -1338,33 +1338,6 @@
     by (cases e) auto
 qed
 
-lemma (in complete_linorder) Sup_eq_top_iff: -- "FIXME move"
-  "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)"
-proof
-  assume *: "Sup A = top"
-  show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
-  proof (intro allI impI)
-    fix x assume "x < Sup A" then show "\<exists>i\<in>A. x < i"
-      unfolding less_Sup_iff by auto
-  qed
-next
-  assume *: "\<forall>x<top. \<exists>i\<in>A. x < i"
-  show "Sup A = top"
-  proof (rule ccontr)
-    assume "Sup A \<noteq> top"
-    with top_greatest [of "Sup A"]
-    have "Sup A < top" unfolding le_less by auto
-    then have "Sup A < Sup A"
-      using * unfolding less_Sup_iff by auto
-    then show False by auto
-  qed
-qed
-
-lemma (in complete_linorder) SUP_eq_top_iff: -- "FIXME move"
-  fixes f :: "'b \<Rightarrow> 'a"
-  shows "(SUP i:A. f i) = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < f i)"
-  unfolding SUPR_def Sup_eq_top_iff by auto
-
 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
 proof -
   { fix x ::ereal assume "x \<noteq> \<infinity>"
@@ -2374,14 +2347,6 @@
 
 abbreviation "limsup \<equiv> Limsup sequentially"
 
-lemma (in complete_lattice) less_INFD:
-  assumes "y < INFI A f"" i \<in> A" shows "y < f i"
-proof -
-  note `y < INFI A f`
-  also have "INFI A f \<le> f i" using `i \<in> A` by (rule INF_leI)
-  finally show "y < f i" .
-qed
-
 lemma liminf_SUPR_INFI:
   fixes f :: "nat \<Rightarrow> ereal"
   shows "liminf f = (SUP n. INF m:{n..}. f m)"