1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:44:59 2013 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:00 2013 +0100
     1.3 @@ -90,6 +90,12 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma (in order_top) bdd_above_top[simp, intro!]: "bdd_above A"
     1.8 +  by (rule bdd_aboveI[of _ top]) simp
     1.9 +
    1.10 +lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A"
    1.11 +  by (rule bdd_belowI[of _ bot]) simp
    1.12 +
    1.13  context lattice
    1.14  begin
    1.15  
    1.16 @@ -270,6 +276,12 @@
    1.17  lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPR A f"
    1.18    by (auto intro: cSUP_upper assms order_trans)
    1.19  
    1.20 +lemma cSUP_const: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c"
    1.21 +  by (intro antisym cSUP_least) (auto intro: cSUP_upper)
    1.22 +
    1.23 +lemma cINF_const: "A \<noteq> {} \<Longrightarrow> (INF x:A. c) = c"
    1.24 +  by (intro antisym cINF_greatest) (auto intro: cINF_lower)
    1.25 +
    1.26  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)"
    1.27    by (metis cINF_greatest cINF_lower assms order_trans)
    1.28  

     2.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Tue Nov 05 09:44:59 2013 +0100
     2.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Nov 05 09:45:00 2013 +0100
     2.3 @@ -32,10 +32,10 @@
     2.4  
     2.5  subsubsection {* @{text Liminf} and @{text Limsup} *}
     2.6  
     2.7 -definition
     2.8 +definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
     2.9    "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
    2.10  
    2.11 -definition
    2.12 +definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
    2.13    "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
    2.14  
    2.15  abbreviation "liminf \<equiv> Liminf sequentially"
    2.16 @@ -43,32 +43,26 @@
    2.17  abbreviation "limsup \<equiv> Limsup sequentially"
    2.18  
    2.19  lemma Liminf_eqI:
    2.20 -  fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
    2.21 -  shows "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
    2.22 +  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
    2.23      (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
    2.24    unfolding Liminf_def by (auto intro!: SUP_eqI)
    2.25  
    2.26  lemma Limsup_eqI:
    2.27 -  fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
    2.28 -  shows "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
    2.29 +  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
    2.30      (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    2.31    unfolding Limsup_def by (auto intro!: INF_eqI)
    2.32  
    2.33 -lemma liminf_SUPR_INFI:
    2.34 -  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
    2.35 -  shows "liminf f = (SUP n. INF m:{n..}. f m)"
    2.36 +lemma liminf_SUPR_INFI: "liminf f = (SUP n. INF m:{n..}. f m)"
    2.37    unfolding Liminf_def eventually_sequentially
    2.38    by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
    2.39  
    2.40 -lemma limsup_INFI_SUPR:
    2.41 -  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
    2.42 -  shows "limsup f = (INF n. SUP m:{n..}. f m)"
    2.43 +lemma limsup_INFI_SUPR: "limsup f = (INF n. SUP m:{n..}. f m)"
    2.44    unfolding Limsup_def eventually_sequentially
    2.45    by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
    2.46  
    2.47  lemma Limsup_const: 
    2.48    assumes ntriv: "\<not> trivial_limit F"
    2.49 -  shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
    2.50 +  shows "Limsup F (\<lambda>x. c) = c"
    2.51  proof -
    2.52    have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
    2.53    have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
    2.54 @@ -81,7 +75,7 @@
    2.55  
    2.56  lemma Liminf_const:
    2.57    assumes ntriv: "\<not> trivial_limit F"
    2.58 -  shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
    2.59 +  shows "Liminf F (\<lambda>x. c) = c"
    2.60  proof -
    2.61    have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
    2.62    have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
    2.63 @@ -93,7 +87,6 @@
    2.64  qed
    2.65  
    2.66  lemma Liminf_mono:
    2.67 -  fixes f g :: "'a => 'b :: complete_lattice"
    2.68    assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
    2.69    shows "Liminf F f \<le> Liminf F g"
    2.70    unfolding Liminf_def
    2.71 @@ -105,13 +98,11 @@
    2.72  qed
    2.73  
    2.74  lemma Liminf_eq:
    2.75 -  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
    2.76    assumes "eventually (\<lambda>x. f x = g x) F"
    2.77    shows "Liminf F f = Liminf F g"
    2.78    by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
    2.79  
    2.80  lemma Limsup_mono:
    2.81 -  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
    2.82    assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
    2.83    shows "Limsup F f \<le> Limsup F g"
    2.84    unfolding Limsup_def
    2.85 @@ -123,18 +114,16 @@
    2.86  qed
    2.87  
    2.88  lemma Limsup_eq:
    2.89 -  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
    2.90    assumes "eventually (\<lambda>x. f x = g x) net"
    2.91    shows "Limsup net f = Limsup net g"
    2.92    by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
    2.93  
    2.94  lemma Liminf_le_Limsup:
    2.95 -  fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
    2.96    assumes ntriv: "\<not> trivial_limit F"
    2.97    shows "Liminf F f \<le> Limsup F f"
    2.98    unfolding Limsup_def Liminf_def
    2.99 -  apply (rule complete_lattice_class.SUP_least)
   2.100 -  apply (rule complete_lattice_class.INF_greatest)
   2.101 +  apply (rule SUP_least)
   2.102 +  apply (rule INF_greatest)
   2.103  proof safe
   2.104    fix P Q assume "eventually P F" "eventually Q F"
   2.105    then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
   2.106 @@ -150,14 +139,12 @@
   2.107  qed
   2.108  
   2.109  lemma Liminf_bounded:
   2.110 -  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
   2.111    assumes ntriv: "\<not> trivial_limit F"
   2.112    assumes le: "eventually (\<lambda>n. C \<le> X n) F"
   2.113    shows "C \<le> Liminf F X"
   2.114    using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
   2.115  
   2.116  lemma Limsup_bounded:
   2.117 -  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
   2.118    assumes ntriv: "\<not> trivial_limit F"
   2.119    assumes le: "eventually (\<lambda>n. X n \<le> C) F"
   2.120    shows "Limsup F X \<le> C"