generalize SUP and INF to the syntactic type classes Sup and Inf
authorhoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 542575c7a3b6b05a9
parent 54256 4843082be7ef
child 54258 adfc759263ab
generalize SUP and INF to the syntactic type classes Sup and Inf
src/HOL/Complete_Lattices.thy
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/GCD.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Lifting_Set.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Probability/Lebesgue_Measure.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Tue Nov 05 05:48:08 2013 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Nov 05 09:44:57 2013 +0100
     1.3 @@ -15,10 +15,54 @@
     1.4  
     1.5  class Inf =
     1.6    fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
     1.7 +begin
     1.8 +
     1.9 +definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.10 +  INF_def: "INFI A f = \<Sqinter>(f ` A)"
    1.11 +
    1.12 +end
    1.13  
    1.14  class Sup =
    1.15    fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    1.16 +begin
    1.17  
    1.18 +definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.19 +  SUP_def: "SUPR A f = \<Squnion>(f ` A)"
    1.20 +
    1.21 +end
    1.22 +
    1.23 +text {*
    1.24 +  Note: must use names @{const INFI} and @{const SUPR} here instead of
    1.25 +  @{text INF} and @{text SUP} to allow the following syntax coexist
    1.26 +  with the plain constant names.
    1.27 +*}
    1.28 +
    1.29 +syntax
    1.30 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
    1.31 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    1.32 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
    1.33 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
    1.34 +
    1.35 +syntax (xsymbols)
    1.36 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    1.37 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    1.38 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    1.39 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    1.40 +
    1.41 +translations
    1.42 +  "INF x y. B"   == "INF x. INF y. B"
    1.43 +  "INF x. B"     == "CONST INFI CONST UNIV (%x. B)"
    1.44 +  "INF x. B"     == "INF x:CONST UNIV. B"
    1.45 +  "INF x:A. B"   == "CONST INFI A (%x. B)"
    1.46 +  "SUP x y. B"   == "SUP x. SUP y. B"
    1.47 +  "SUP x. B"     == "CONST SUPR CONST UNIV (%x. B)"
    1.48 +  "SUP x. B"     == "SUP x:CONST UNIV. B"
    1.49 +  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
    1.50 +
    1.51 +print_translation {*
    1.52 +  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
    1.53 +    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
    1.54 +*} -- {* to avoid eta-contraction of body *}
    1.55  
    1.56  subsection {* Abstract complete lattices *}
    1.57  
    1.58 @@ -49,59 +93,17 @@
    1.59      (unfold_locales, (fact Inf_empty Sup_empty
    1.60          Sup_upper Sup_least Inf_lower Inf_greatest)+)
    1.61  
    1.62 -definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.63 -  INF_def: "INFI A f = \<Sqinter>(f ` A)"
    1.64 -
    1.65 -definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.66 -  SUP_def: "SUPR A f = \<Squnion>(f ` A)"
    1.67 -
    1.68 -text {*
    1.69 -  Note: must use names @{const INFI} and @{const SUPR} here instead of
    1.70 -  @{text INF} and @{text SUP} to allow the following syntax coexist
    1.71 -  with the plain constant names.
    1.72 -*}
    1.73 -
    1.74  end
    1.75  
    1.76 -syntax
    1.77 -  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
    1.78 -  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    1.79 -  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
    1.80 -  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
    1.81 -
    1.82 -syntax (xsymbols)
    1.83 -  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    1.84 -  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    1.85 -  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    1.86 -  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    1.87 -
    1.88 -translations
    1.89 -  "INF x y. B"   == "INF x. INF y. B"
    1.90 -  "INF x. B"     == "CONST INFI CONST UNIV (%x. B)"
    1.91 -  "INF x. B"     == "INF x:CONST UNIV. B"
    1.92 -  "INF x:A. B"   == "CONST INFI A (%x. B)"
    1.93 -  "SUP x y. B"   == "SUP x. SUP y. B"
    1.94 -  "SUP x. B"     == "CONST SUPR CONST UNIV (%x. B)"
    1.95 -  "SUP x. B"     == "SUP x:CONST UNIV. B"
    1.96 -  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
    1.97 -
    1.98 -print_translation {*
    1.99 -  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
   1.100 -    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
   1.101 -*} -- {* to avoid eta-contraction of body *}
   1.102 -
   1.103  context complete_lattice
   1.104  begin
   1.105  
   1.106  lemma INF_foundation_dual:
   1.107 -  "complete_lattice.SUPR Inf = INFI"
   1.108 -  by (simp add: fun_eq_iff INF_def
   1.109 -    complete_lattice.SUP_def [OF dual_complete_lattice])
   1.110 +  "Sup.SUPR Inf = INFI"
   1.111 +  by (simp add: fun_eq_iff INF_def Sup.SUP_def)
   1.112  
   1.113  lemma SUP_foundation_dual:
   1.114 -  "complete_lattice.INFI Sup = SUPR"
   1.115 -  by (simp add: fun_eq_iff SUP_def
   1.116 -    complete_lattice.INF_def [OF dual_complete_lattice])
   1.117 +  "Inf.INFI Sup = SUPR" by (simp add: fun_eq_iff SUP_def Inf.INF_def)
   1.118  
   1.119  lemma Sup_eqI:
   1.120    "(\<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"
     2.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 05:48:08 2013 +0100
     2.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:44:57 2013 +0100
     2.3 @@ -283,22 +283,22 @@
     2.4  lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
     2.5    using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
     2.6  
     2.7 -lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
     2.8 +lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
     2.9    by (auto intro!: cSup_eq_non_empty intro: dense_le)
    2.10  
    2.11 -lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
    2.12 +lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
    2.13    by (auto intro!: cSup_eq intro: dense_le_bounded)
    2.14  
    2.15 -lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
    2.16 +lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
    2.17    by (auto intro!: cSup_eq intro: dense_le_bounded)
    2.18  
    2.19 -lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, unbounded_dense_linorder} <..} = x"
    2.20 +lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, no_top, dense_linorder} <..} = x"
    2.21    by (auto intro!: cInf_eq intro: dense_ge)
    2.22  
    2.23 -lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
    2.24 +lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, no_top, dense_linorder}} = y"
    2.25    by (auto intro!: cInf_eq intro: dense_ge_bounded)
    2.26  
    2.27 -lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
    2.28 +lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, no_top, dense_linorder}} = y"
    2.29    by (auto intro!: cInf_eq intro: dense_ge_bounded)
    2.30  
    2.31  end
     3.1 --- a/src/HOL/GCD.thy	Tue Nov 05 05:48:08 2013 +0100
     3.2 +++ b/src/HOL/GCD.thy	Tue Nov 05 09:44:57 2013 +0100
     3.3 @@ -1555,8 +1555,8 @@
     3.4  interpretation gcd_lcm_complete_lattice_nat:
     3.5    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
     3.6  where
     3.7 -  "complete_lattice.INFI Gcd A f = Gcd (f ` A :: nat set)"
     3.8 -  and "complete_lattice.SUPR Lcm A f = Lcm (f ` A)"
     3.9 +  "Inf.INFI Gcd A f = Gcd (f ` A :: nat set)"
    3.10 +  and "Sup.SUPR Lcm A f = Lcm (f ` A)"
    3.11  proof -
    3.12    show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
    3.13    proof
    3.14 @@ -1574,8 +1574,8 @@
    3.15    qed
    3.16    then interpret gcd_lcm_complete_lattice_nat:
    3.17      complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
    3.18 -  from gcd_lcm_complete_lattice_nat.INF_def show "complete_lattice.INFI Gcd A f = Gcd (f ` A)" .
    3.19 -  from gcd_lcm_complete_lattice_nat.SUP_def show "complete_lattice.SUPR Lcm A f = Lcm (f ` A)" .
    3.20 +  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFI Gcd A f = Gcd (f ` A)" .
    3.21 +  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" .
    3.22  qed
    3.23  
    3.24  lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
     4.1 --- a/src/HOL/Library/Continuity.thy	Tue Nov 05 05:48:08 2013 +0100
     4.2 +++ b/src/HOL/Library/Continuity.thy	Tue Nov 05 09:44:57 2013 +0100
     4.3 @@ -19,7 +19,8 @@
     4.4    "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
     4.5  
     4.6  lemma SUP_nat_conv:
     4.7 -  "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
     4.8 +  fixes M :: "nat \<Rightarrow> 'a::complete_lattice"
     4.9 +  shows "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
    4.10  apply(rule order_antisym)
    4.11   apply(rule SUP_least)
    4.12   apply(case_tac n)
     5.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Tue Nov 05 05:48:08 2013 +0100
     5.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Nov 05 09:44:57 2013 +0100
     5.3 @@ -21,11 +21,13 @@
     5.4    by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
     5.5  
     5.6  lemma SUPR_pair:
     5.7 -  "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
     5.8 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
     5.9 +  shows "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
    5.10    by (rule antisym) (auto intro!: SUP_least SUP_upper2)
    5.11  
    5.12  lemma INFI_pair:
    5.13 -  "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
    5.14 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
    5.15 +  shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
    5.16    by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    5.17  
    5.18  subsubsection {* @{text Liminf} and @{text Limsup} *}
    5.19 @@ -41,12 +43,14 @@
    5.20  abbreviation "limsup \<equiv> Limsup sequentially"
    5.21  
    5.22  lemma Liminf_eqI:
    5.23 -  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
    5.24 +  fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
    5.25 +  shows "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
    5.26      (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
    5.27    unfolding Liminf_def by (auto intro!: SUP_eqI)
    5.28  
    5.29  lemma Limsup_eqI:
    5.30 -  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
    5.31 +  fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
    5.32 +  shows "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
    5.33      (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    5.34    unfolding Limsup_def by (auto intro!: INF_eqI)
    5.35  
     6.1 --- a/src/HOL/Lifting_Set.thy	Tue Nov 05 05:48:08 2013 +0100
     6.2 +++ b/src/HOL/Lifting_Set.thy	Tue Nov 05 09:44:57 2013 +0100
     6.3 @@ -153,7 +153,7 @@
     6.4    unfolding fun_rel_def set_rel_def by fast
     6.5  
     6.6  lemma SUPR_parametric [transfer_rule]:
     6.7 -  "(set_rel R ===> (R ===> op =) ===> op =) SUPR SUPR"
     6.8 +  "(set_rel R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
     6.9  proof(rule fun_relI)+
    6.10    fix A B f and g :: "'b \<Rightarrow> 'c"
    6.11    assume AB: "set_rel R A B"
     7.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 05 05:48:08 2013 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 05 09:44:57 2013 +0100
     7.3 @@ -1193,12 +1193,12 @@
     7.4  qed
     7.5  
     7.6  lemma Liminf_at:
     7.7 -  fixes f :: "'a::metric_space \<Rightarrow> _"
     7.8 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
     7.9    shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
    7.10    using Liminf_within[of x UNIV f] by simp
    7.11  
    7.12  lemma Limsup_at:
    7.13 -  fixes f :: "'a::metric_space \<Rightarrow> _"
    7.14 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
    7.15    shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
    7.16    using Limsup_within[of x UNIV f] by simp
    7.17  
     8.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Nov 05 05:48:08 2013 +0100
     8.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Nov 05 09:44:57 2013 +0100
     8.3 @@ -1138,7 +1138,7 @@
     8.4      show "\<And>i x. 0 \<le> ?f i x"
     8.5        using nonneg by (auto split: split_indicator)
     8.6    qed
     8.7 -  also have "\<dots> = (SUP i::nat. F (a + real i) - F a)"
     8.8 +  also have "\<dots> = (SUP i::nat. ereal (F (a + real i) - F a))"
     8.9      by (subst positive_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto
    8.10    also have "\<dots> = T - F a"
    8.11    proof (rule SUP_Lim_ereal)