--- a/src/HOL/Complete_Lattices.thy Tue Nov 05 05:48:08 2013 +0100
+++ b/src/HOL/Complete_Lattices.thy Tue Nov 05 09:44:57 2013 +0100
@@ -15,10 +15,54 @@
class Inf =
fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
+begin
+
+definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ INF_def: "INFI A f = \<Sqinter>(f ` A)"
+
+end
class Sup =
fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
+begin
+definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ SUP_def: "SUPR A f = \<Squnion>(f ` A)"
+
+end
+
+text {*
+ Note: must use names @{const INFI} and @{const SUPR} here instead of
+ @{text INF} and @{text SUP} to allow the following syntax coexist
+ with the plain constant names.
+*}
+
+syntax
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _:_./ _)" [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _:_./ _)" [0, 0, 10] 10)
+
+syntax (xsymbols)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
+translations
+ "INF x y. B" == "INF x. INF y. B"
+ "INF x. B" == "CONST INFI CONST UNIV (%x. B)"
+ "INF x. B" == "INF x:CONST UNIV. B"
+ "INF x:A. B" == "CONST INFI A (%x. B)"
+ "SUP x y. B" == "SUP x. SUP y. B"
+ "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)"
+ "SUP x. B" == "SUP x:CONST UNIV. B"
+ "SUP x:A. B" == "CONST SUPR A (%x. B)"
+
+print_translation {*
+ [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
+ Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
+*} -- {* to avoid eta-contraction of body *}
subsection {* Abstract complete lattices *}
@@ -49,59 +93,17 @@
(unfold_locales, (fact Inf_empty Sup_empty
Sup_upper Sup_least Inf_lower Inf_greatest)+)
-definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
- INF_def: "INFI A f = \<Sqinter>(f ` A)"
-
-definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
- SUP_def: "SUPR A f = \<Squnion>(f ` A)"
-
-text {*
- Note: must use names @{const INFI} and @{const SUPR} here instead of
- @{text INF} and @{text SUP} to allow the following syntax coexist
- with the plain constant names.
-*}
-
end
-syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _:_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _:_./ _)" [0, 0, 10] 10)
-
-syntax (xsymbols)
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
-translations
- "INF x y. B" == "INF x. INF y. B"
- "INF x. B" == "CONST INFI CONST UNIV (%x. B)"
- "INF x. B" == "INF x:CONST UNIV. B"
- "INF x:A. B" == "CONST INFI A (%x. B)"
- "SUP x y. B" == "SUP x. SUP y. B"
- "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)"
- "SUP x. B" == "SUP x:CONST UNIV. B"
- "SUP x:A. B" == "CONST SUPR A (%x. B)"
-
-print_translation {*
- [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
- Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
-*} -- {* to avoid eta-contraction of body *}
-
context complete_lattice
begin
lemma INF_foundation_dual:
- "complete_lattice.SUPR Inf = INFI"
- by (simp add: fun_eq_iff INF_def
- complete_lattice.SUP_def [OF dual_complete_lattice])
+ "Sup.SUPR Inf = INFI"
+ by (simp add: fun_eq_iff INF_def Sup.SUP_def)
lemma SUP_foundation_dual:
- "complete_lattice.INFI Sup = SUPR"
- by (simp add: fun_eq_iff SUP_def
- complete_lattice.INF_def [OF dual_complete_lattice])
+ "Inf.INFI Sup = SUPR" by (simp add: fun_eq_iff SUP_def Inf.INF_def)
lemma Sup_eqI:
"(\<And>y. y \<in> A \<Longrightarrow> y \<le> x) \<Longrightarrow> (\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> \<Squnion>A = x"
--- a/src/HOL/Conditionally_Complete_Lattices.thy Tue Nov 05 05:48:08 2013 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Nov 05 09:44:57 2013 +0100
@@ -283,22 +283,22 @@
lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
-lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
+lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
by (auto intro!: cSup_eq_non_empty intro: dense_le)
-lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
+lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
by (auto intro!: cSup_eq intro: dense_le_bounded)
-lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
+lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
by (auto intro!: cSup_eq intro: dense_le_bounded)
-lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, unbounded_dense_linorder} <..} = x"
+lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, no_top, dense_linorder} <..} = x"
by (auto intro!: cInf_eq intro: dense_ge)
-lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
+lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, no_top, dense_linorder}} = y"
by (auto intro!: cInf_eq intro: dense_ge_bounded)
-lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
+lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, no_top, dense_linorder}} = y"
by (auto intro!: cInf_eq intro: dense_ge_bounded)
end
--- a/src/HOL/GCD.thy Tue Nov 05 05:48:08 2013 +0100
+++ b/src/HOL/GCD.thy Tue Nov 05 09:44:57 2013 +0100
@@ -1555,8 +1555,8 @@
interpretation gcd_lcm_complete_lattice_nat:
complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
where
- "complete_lattice.INFI Gcd A f = Gcd (f ` A :: nat set)"
- and "complete_lattice.SUPR Lcm A f = Lcm (f ` A)"
+ "Inf.INFI Gcd A f = Gcd (f ` A :: nat set)"
+ and "Sup.SUPR Lcm A f = Lcm (f ` A)"
proof -
show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
proof
@@ -1574,8 +1574,8 @@
qed
then interpret gcd_lcm_complete_lattice_nat:
complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
- from gcd_lcm_complete_lattice_nat.INF_def show "complete_lattice.INFI Gcd A f = Gcd (f ` A)" .
- from gcd_lcm_complete_lattice_nat.SUP_def show "complete_lattice.SUPR Lcm A f = Lcm (f ` A)" .
+ from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFI Gcd A f = Gcd (f ` A)" .
+ from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" .
qed
lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
--- a/src/HOL/Library/Continuity.thy Tue Nov 05 05:48:08 2013 +0100
+++ b/src/HOL/Library/Continuity.thy Tue Nov 05 09:44:57 2013 +0100
@@ -19,7 +19,8 @@
"continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
lemma SUP_nat_conv:
- "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
+ fixes M :: "nat \<Rightarrow> 'a::complete_lattice"
+ shows "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
apply(rule order_antisym)
apply(rule SUP_least)
apply(case_tac n)
--- a/src/HOL/Library/Liminf_Limsup.thy Tue Nov 05 05:48:08 2013 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy Tue Nov 05 09:44:57 2013 +0100
@@ -21,11 +21,13 @@
by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
lemma SUPR_pair:
- "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
+ fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
+ shows "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
by (rule antisym) (auto intro!: SUP_least SUP_upper2)
lemma INFI_pair:
- "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
+ fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
+ shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
by (rule antisym) (auto intro!: INF_greatest INF_lower2)
subsubsection {* @{text Liminf} and @{text Limsup} *}
@@ -41,12 +43,14 @@
abbreviation "limsup \<equiv> Limsup sequentially"
lemma Liminf_eqI:
- "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>
+ fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
+ shows "(\<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:
- "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>
+ fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
+ shows "(\<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)
--- a/src/HOL/Lifting_Set.thy Tue Nov 05 05:48:08 2013 +0100
+++ b/src/HOL/Lifting_Set.thy Tue Nov 05 09:44:57 2013 +0100
@@ -153,7 +153,7 @@
unfolding fun_rel_def set_rel_def by fast
lemma SUPR_parametric [transfer_rule]:
- "(set_rel R ===> (R ===> op =) ===> op =) SUPR SUPR"
+ "(set_rel R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
proof(rule fun_relI)+
fix A B f and g :: "'b \<Rightarrow> 'c"
assume AB: "set_rel R A B"
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Nov 05 05:48:08 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Nov 05 09:44:57 2013 +0100
@@ -1193,12 +1193,12 @@
qed
lemma Liminf_at:
- fixes f :: "'a::metric_space \<Rightarrow> _"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
using Liminf_within[of x UNIV f] by simp
lemma Limsup_at:
- fixes f :: "'a::metric_space \<Rightarrow> _"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
using Limsup_within[of x UNIV f] by simp
--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Nov 05 05:48:08 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Nov 05 09:44:57 2013 +0100
@@ -1138,7 +1138,7 @@
show "\<And>i x. 0 \<le> ?f i x"
using nonneg by (auto split: split_indicator)
qed
- also have "\<dots> = (SUP i::nat. F (a + real i) - F a)"
+ also have "\<dots> = (SUP i::nat. ereal (F (a + real i) - F a))"
by (subst positive_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto
also have "\<dots> = T - F a"
proof (rule SUP_Lim_ereal)