src/HOL/Complete_Lattices.thy
changeset 54257 5c7a3b6b05a9
parent 54147 97a8ff4e4ac9
child 54259 71c701dc5bf9
     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"