# 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) \ x \ A \ u \ f x \ u \ SUPR A f" by (auto intro: cSUP_upper assms order_trans) +lemma cSUP_const: "A \ {} \ (SUP x:A. c) = c" + by (intro antisym cSUP_least) (auto intro: cSUP_upper) + +lemma cINF_const: "A \ {} \ (INF x:A. c) = c" + by (intro antisym cINF_greatest) (auto intro: cINF_lower) + lemma le_cINF_iff: "A \ {} \ bdd_below (f ` A) \ u \ INFI A f \ (\x\A. u \ 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 \ ('a \ 'b) \ '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 \ ('a \ 'b) \ 'b :: complete_lattice" where "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)" abbreviation "liminf \ Liminf sequentially" @@ -43,32 +43,26 @@ abbreviation "limsup \ Limsup sequentially" lemma Liminf_eqI: - fixes f :: "_ \ _ :: complete_lattice" - shows "(\P. eventually P F \ INFI (Collect P) f \ x) \ + "(\P. eventually P F \ INFI (Collect P) f \ x) \ (\y. (\P. eventually P F \ INFI (Collect P) f \ y) \ x \ y) \ Liminf F f = x" unfolding Liminf_def by (auto intro!: SUP_eqI) lemma Limsup_eqI: - fixes f :: "_ \ _ :: complete_lattice" - shows "(\P. eventually P F \ x \ SUPR (Collect P) f) \ + "(\P. eventually P F \ x \ SUPR (Collect P) f) \ (\y. (\P. eventually P F \ y \ SUPR (Collect P) f) \ y \ x) \ Limsup F f = x" unfolding Limsup_def by (auto intro!: INF_eqI) -lemma liminf_SUPR_INFI: - fixes f :: "nat \ '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 \ '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: "\ trivial_limit F" - shows "Limsup F (\x. c) = (c::'a::complete_lattice)" + shows "Limsup F (\x. c) = c" proof - have *: "\P. Ex P \ P \ (\x. False)" by auto have "\P. eventually P F \ (SUP x : {x. P x}. c) = c" @@ -81,7 +75,7 @@ lemma Liminf_const: assumes ntriv: "\ trivial_limit F" - shows "Liminf F (\x. c) = (c::'a::complete_lattice)" + shows "Liminf F (\x. c) = c" proof - have *: "\P. Ex P \ P \ (\x. False)" by auto have "\P. eventually P F \ (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 (\x. f x \ g x) F" shows "Liminf F f \ Liminf F g" unfolding Liminf_def @@ -105,13 +98,11 @@ qed lemma Liminf_eq: - fixes f g :: "'a \ 'b :: complete_lattice" assumes "eventually (\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 \ 'b :: complete_lattice" assumes ev: "eventually (\x. f x \ g x) F" shows "Limsup F f \ Limsup F g" unfolding Limsup_def @@ -123,18 +114,16 @@ qed lemma Limsup_eq: - fixes f g :: "'a \ 'b :: complete_lattice" assumes "eventually (\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 \ 'b::complete_lattice" assumes ntriv: "\ trivial_limit F" shows "Liminf F f \ 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 (\x. P x \ Q x) F" (is "eventually ?C F") by (rule eventually_conj) @@ -150,14 +139,12 @@ qed lemma Liminf_bounded: - fixes X Y :: "'a \ 'b::complete_lattice" assumes ntriv: "\ trivial_limit F" assumes le: "eventually (\n. C \ X n) F" shows "C \ Liminf F X" using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp lemma Limsup_bounded: - fixes X Y :: "'a \ 'b::complete_lattice" assumes ntriv: "\ trivial_limit F" assumes le: "eventually (\n. X n \ C) F" shows "Limsup F X \ C"