# HG changeset patch
# User hoelzl
# Date 1383641100 -3600
# Node ID 89991ef58448e225d4949e8aba9040f1d4e92801
# Parent  6a967667fd45de6363df8ecb4b4717b3f9fb8b4c
restrict Limsup and Liminf to complete lattices

diff -r 6a967667fd45 -r 89991ef58448 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:44:59 2013 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:00 2013 +0100
@@ -90,6 +90,12 @@
 
 end
 
+lemma (in order_top) bdd_above_top[simp, intro!]: "bdd_above A"
+  by (rule bdd_aboveI[of _ top]) simp
+
+lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A"
+  by (rule bdd_belowI[of _ bot]) simp
+
 context lattice
 begin
 
@@ -270,6 +276,12 @@
 lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPR A f"
   by (auto intro: cSUP_upper assms order_trans)
 
+lemma cSUP_const: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c"
+  by (intro antisym cSUP_least) (auto intro: cSUP_upper)
+
+lemma cINF_const: "A \<noteq> {} \<Longrightarrow> (INF x:A. c) = c"
+  by (intro antisym cINF_greatest) (auto intro: cINF_lower)
+
 lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFI A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
   by (metis cINF_greatest cINF_lower assms order_trans)
 
diff -r 6a967667fd45 -r 89991ef58448 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Tue Nov 05 09:44:59 2013 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Nov 05 09:45:00 2013 +0100
@@ -32,10 +32,10 @@
 
 subsubsection {* @{text Liminf} and @{text Limsup} *}
 
-definition
+definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
   "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
 
-definition
+definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
   "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
 
 abbreviation "liminf \<equiv> Liminf sequentially"
@@ -43,32 +43,26 @@
 abbreviation "limsup \<equiv> Limsup sequentially"
 
 lemma Liminf_eqI:
-  fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
-  shows "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
+  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
   unfolding Liminf_def by (auto intro!: SUP_eqI)
 
 lemma Limsup_eqI:
-  fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
-  shows "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
+  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
   unfolding Limsup_def by (auto intro!: INF_eqI)
 
-lemma liminf_SUPR_INFI:
-  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
-  shows "liminf f = (SUP n. INF m:{n..}. f m)"
+lemma liminf_SUPR_INFI: "liminf f = (SUP n. INF m:{n..}. f m)"
   unfolding Liminf_def eventually_sequentially
   by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
 
-lemma limsup_INFI_SUPR:
-  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
-  shows "limsup f = (INF n. SUP m:{n..}. f m)"
+lemma limsup_INFI_SUPR: "limsup f = (INF n. SUP m:{n..}. f m)"
   unfolding Limsup_def eventually_sequentially
   by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
 
 lemma Limsup_const: 
   assumes ntriv: "\<not> trivial_limit F"
-  shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
+  shows "Limsup F (\<lambda>x. c) = c"
 proof -
   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
   have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
@@ -81,7 +75,7 @@
 
 lemma Liminf_const:
   assumes ntriv: "\<not> trivial_limit F"
-  shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
+  shows "Liminf F (\<lambda>x. c) = c"
 proof -
   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
   have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
@@ -93,7 +87,6 @@
 qed
 
 lemma Liminf_mono:
-  fixes f g :: "'a => 'b :: complete_lattice"
   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
   shows "Liminf F f \<le> Liminf F g"
   unfolding Liminf_def
@@ -105,13 +98,11 @@
 qed
 
 lemma Liminf_eq:
-  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
   assumes "eventually (\<lambda>x. f x = g x) F"
   shows "Liminf F f = Liminf F g"
   by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
 
 lemma Limsup_mono:
-  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
   shows "Limsup F f \<le> Limsup F g"
   unfolding Limsup_def
@@ -123,18 +114,16 @@
 qed
 
 lemma Limsup_eq:
-  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
   assumes "eventually (\<lambda>x. f x = g x) net"
   shows "Limsup net f = Limsup net g"
   by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
 
 lemma Liminf_le_Limsup:
-  fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   assumes ntriv: "\<not> trivial_limit F"
   shows "Liminf F f \<le> Limsup F f"
   unfolding Limsup_def Liminf_def
-  apply (rule complete_lattice_class.SUP_least)
-  apply (rule complete_lattice_class.INF_greatest)
+  apply (rule SUP_least)
+  apply (rule INF_greatest)
 proof safe
   fix P Q assume "eventually P F" "eventually Q F"
   then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
@@ -150,14 +139,12 @@
 qed
 
 lemma Liminf_bounded:
-  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
   assumes ntriv: "\<not> trivial_limit F"
   assumes le: "eventually (\<lambda>n. C \<le> X n) F"
   shows "C \<le> Liminf F X"
   using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
 
 lemma Limsup_bounded:
-  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
   assumes ntriv: "\<not> trivial_limit F"
   assumes le: "eventually (\<lambda>n. X n \<le> C) F"
   shows "Limsup F X \<le> C"