# HG changeset patch
# User hoelzl
# Date 1383641097 -3600
# Node ID 5c7a3b6b05a9cf4e4f14748f6be80bf2d52e4876
# Parent  4843082be7efe7a64b5b5df77112e7a736d44ce1
generalize SUP and INF to the syntactic type classes Sup and Inf

diff -r 4843082be7ef -r 5c7a3b6b05a9 src/HOL/Complete_Lattices.thy
--- 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"
diff -r 4843082be7ef -r 5c7a3b6b05a9 src/HOL/Conditionally_Complete_Lattices.thy
--- 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
diff -r 4843082be7ef -r 5c7a3b6b05a9 src/HOL/GCD.thy
--- 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)"
diff -r 4843082be7ef -r 5c7a3b6b05a9 src/HOL/Library/Continuity.thy
--- 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)
diff -r 4843082be7ef -r 5c7a3b6b05a9 src/HOL/Library/Liminf_Limsup.thy
--- 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)
 
diff -r 4843082be7ef -r 5c7a3b6b05a9 src/HOL/Lifting_Set.thy
--- 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"
diff -r 4843082be7ef -r 5c7a3b6b05a9 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- 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
 
diff -r 4843082be7ef -r 5c7a3b6b05a9 src/HOL/Probability/Lebesgue_Measure.thy
--- 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)