src/HOL/Lattices.thy
changeset 44845 5e51075cbd97
parent 44085 a65e26f1427b
child 44918 6a80fbc4e72c
     1.1 --- a/src/HOL/Lattices.thy	Thu Sep 08 08:41:28 2011 -0700
     1.2 +++ b/src/HOL/Lattices.thy	Fri Sep 09 00:22:18 2011 +0200
     1.3 @@ -51,15 +51,18 @@
     1.4    bot ("\<bottom>") and
     1.5    top ("\<top>")
     1.6  
     1.7 +class inf =
     1.8 +  fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
     1.9  
    1.10 -class semilattice_inf = order +
    1.11 -  fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    1.12 +class sup = 
    1.13 +  fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    1.14 +
    1.15 +class semilattice_inf =  order + inf +
    1.16    assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
    1.17    and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    1.18    and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    1.19  
    1.20 -class semilattice_sup = order +
    1.21 -  fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    1.22 +class semilattice_sup = order + sup +
    1.23    assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
    1.24    and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    1.25    and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    1.26 @@ -68,7 +71,7 @@
    1.27  text {* Dual lattice *}
    1.28  
    1.29  lemma dual_semilattice:
    1.30 -  "class.semilattice_inf greater_eq greater sup"
    1.31 +  "class.semilattice_inf sup greater_eq greater"
    1.32  by (rule class.semilattice_inf.intro, rule dual_order)
    1.33    (unfold_locales, simp_all add: sup_least)
    1.34  
    1.35 @@ -236,7 +239,7 @@
    1.36  begin
    1.37  
    1.38  lemma dual_lattice:
    1.39 -  "class.lattice (op \<ge>) (op >) sup inf"
    1.40 +  "class.lattice sup (op \<ge>) (op >) inf"
    1.41    by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
    1.42      (unfold_locales, auto)
    1.43  
    1.44 @@ -307,7 +310,7 @@
    1.45  lemma less_supI1:
    1.46    "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
    1.47  proof -
    1.48 -  interpret dual: semilattice_inf "op \<ge>" "op >" sup
    1.49 +  interpret dual: semilattice_inf sup "op \<ge>" "op >"
    1.50      by (fact dual_semilattice)
    1.51    assume "x \<sqsubset> a"
    1.52    then show "x \<sqsubset> a \<squnion> b"
    1.53 @@ -317,7 +320,7 @@
    1.54  lemma less_supI2:
    1.55    "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
    1.56  proof -
    1.57 -  interpret dual: semilattice_inf "op \<ge>" "op >" sup
    1.58 +  interpret dual: semilattice_inf sup "op \<ge>" "op >"
    1.59      by (fact dual_semilattice)
    1.60    assume "x \<sqsubset> b"
    1.61    then show "x \<sqsubset> a \<squnion> b"
    1.62 @@ -348,7 +351,7 @@
    1.63  by(simp add: inf_sup_aci inf_sup_distrib1)
    1.64  
    1.65  lemma dual_distrib_lattice:
    1.66 -  "class.distrib_lattice (op \<ge>) (op >) sup inf"
    1.67 +  "class.distrib_lattice sup (op \<ge>) (op >) inf"
    1.68    by (rule class.distrib_lattice.intro, rule dual_lattice)
    1.69      (unfold_locales, fact inf_sup_distrib1)
    1.70  
    1.71 @@ -420,7 +423,7 @@
    1.72  begin
    1.73  
    1.74  lemma dual_bounded_lattice:
    1.75 -  "class.bounded_lattice greater_eq greater sup inf \<top> \<bottom>"
    1.76 +  "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
    1.77    by unfold_locales (auto simp add: less_le_not_le)
    1.78  
    1.79  end
    1.80 @@ -432,7 +435,7 @@
    1.81  begin
    1.82  
    1.83  lemma dual_boolean_algebra:
    1.84 -  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus greater_eq greater sup inf \<top> \<bottom>"
    1.85 +  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>"
    1.86    by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    1.87      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
    1.88  
    1.89 @@ -506,7 +509,7 @@
    1.90  lemma compl_sup [simp]:
    1.91    "- (x \<squnion> y) = - x \<sqinter> - y"
    1.92  proof -
    1.93 -  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus greater_eq greater sup inf \<top> \<bottom>
    1.94 +  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus sup greater_eq greater inf \<top> \<bottom>
    1.95      by (rule dual_boolean_algebra)
    1.96    then show ?thesis by simp
    1.97  qed
    1.98 @@ -591,7 +594,7 @@
    1.99  subsection {* @{const min}/@{const max} on linear orders as
   1.100    special case of @{const inf}/@{const sup} *}
   1.101  
   1.102 -sublocale linorder < min_max!: distrib_lattice less_eq less min max
   1.103 +sublocale linorder < min_max!: distrib_lattice min less_eq less max
   1.104  proof
   1.105    fix x y z
   1.106    show "max x (min y z) = min (max x y) (max x z)"