src/HOL/Lattices.thy
changeset 51487 f4bfdee99304
parent 51387 dbc4a77488b2
child 51489 f738e6dbd844
     1.1 --- a/src/HOL/Lattices.thy	Sat Mar 23 07:30:53 2013 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Sat Mar 23 17:11:06 2013 +0100
     1.3 @@ -11,39 +11,134 @@
     1.4  subsection {* Abstract semilattice *}
     1.5  
     1.6  text {*
     1.7 -  This locales provide a basic structure for interpretation into
     1.8 +  These locales provide a basic structure for interpretation into
     1.9    bigger structures;  extensions require careful thinking, otherwise
    1.10    undesired effects may occur due to interpretation.
    1.11  *}
    1.12  
    1.13 +no_notation times (infixl "*" 70)
    1.14 +no_notation Groups.one ("1")
    1.15 +
    1.16  locale semilattice = abel_semigroup +
    1.17 -  assumes idem [simp]: "f a a = a"
    1.18 +  assumes idem [simp]: "a * a = a"
    1.19  begin
    1.20  
    1.21 -lemma left_idem [simp]: "f a (f a b) = f a b"
    1.22 +lemma left_idem [simp]: "a * (a * b) = a * b"
    1.23  by (simp add: assoc [symmetric])
    1.24  
    1.25 -lemma right_idem [simp]: "f (f a b) b = f a b"
    1.26 +lemma right_idem [simp]: "(a * b) * b = a * b"
    1.27  by (simp add: assoc)
    1.28  
    1.29  end
    1.30  
    1.31 +locale semilattice_neutr = semilattice + comm_monoid
    1.32  
    1.33 -subsection {* Idempotent semigroup *}
    1.34 +locale semilattice_order = semilattice +
    1.35 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
    1.36 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
    1.37 +  assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
    1.38 +    and semilattice_strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    1.39 +begin
    1.40 +
    1.41 +lemma orderI:
    1.42 +  "a = a * b \<Longrightarrow> a \<preceq> b"
    1.43 +  by (simp add: order_iff)
    1.44 +
    1.45 +lemma orderE:
    1.46 +  assumes "a \<preceq> b"
    1.47 +  obtains "a = a * b"
    1.48 +  using assms by (unfold order_iff)
    1.49 +
    1.50 +end
    1.51  
    1.52 -class ab_semigroup_idem_mult = ab_semigroup_mult +
    1.53 -  assumes mult_idem: "x * x = x"
    1.54 +sublocale semilattice_order < ordering less_eq less
    1.55 +proof
    1.56 +  fix a b
    1.57 +  show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    1.58 +    by (fact semilattice_strict_iff_order)
    1.59 +next
    1.60 +  fix a
    1.61 +  show "a \<preceq> a"
    1.62 +    by (simp add: order_iff)
    1.63 +next
    1.64 +  fix a b
    1.65 +  assume "a \<preceq> b" "b \<preceq> a"
    1.66 +  then have "a = a * b" "a * b = b"
    1.67 +    by (simp_all add: order_iff commute)
    1.68 +  then show "a = b" by simp
    1.69 +next
    1.70 +  fix a b c
    1.71 +  assume "a \<preceq> b" "b \<preceq> c"
    1.72 +  then have "a = a * b" "b = b * c"
    1.73 +    by (simp_all add: order_iff commute)
    1.74 +  then have "a = a * (b * c)"
    1.75 +    by simp
    1.76 +  then have "a = (a * b) * c"
    1.77 +    by (simp add: assoc)
    1.78 +  with `a = a * b` [symmetric] have "a = a * c" by simp
    1.79 +  then show "a \<preceq> c" by (rule orderI)
    1.80 +qed
    1.81  
    1.82 -sublocale ab_semigroup_idem_mult < times!: semilattice times proof
    1.83 -qed (fact mult_idem)
    1.84 -
    1.85 -context ab_semigroup_idem_mult
    1.86 +context semilattice_order
    1.87  begin
    1.88  
    1.89 -lemmas mult_left_idem = times.left_idem
    1.90 +lemma cobounded1 [simp]:
    1.91 +  "a * b \<preceq> a"
    1.92 +  by (simp add: order_iff commute)  
    1.93 +
    1.94 +lemma cobounded2 [simp]:
    1.95 +  "a * b \<preceq> b"
    1.96 +  by (simp add: order_iff)
    1.97 +
    1.98 +lemma boundedI:
    1.99 +  assumes "a \<preceq> b" and "a \<preceq> c"
   1.100 +  shows "a \<preceq> b * c"
   1.101 +proof (rule orderI)
   1.102 +  from assms obtain "a * b = a" and "a * c = a" by (auto elim!: orderE)
   1.103 +  then show "a = a * (b * c)" by (simp add: assoc [symmetric])
   1.104 +qed
   1.105 +
   1.106 +lemma boundedE:
   1.107 +  assumes "a \<preceq> b * c"
   1.108 +  obtains "a \<preceq> b" and "a \<preceq> c"
   1.109 +  using assms by (blast intro: trans cobounded1 cobounded2)
   1.110 +
   1.111 +lemma bounded_iff:
   1.112 +  "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c"
   1.113 +  by (blast intro: boundedI elim: boundedE)
   1.114 +
   1.115 +lemma strict_boundedE:
   1.116 +  assumes "a \<prec> b * c"
   1.117 +  obtains "a \<prec> b" and "a \<prec> c"
   1.118 +  using assms by (auto simp add: commute strict_iff_order bounded_iff elim: orderE intro!: that)+
   1.119 +
   1.120 +lemma coboundedI1:
   1.121 +  "a \<preceq> c \<Longrightarrow> a * b \<preceq> c"
   1.122 +  by (rule trans) auto
   1.123 +
   1.124 +lemma coboundedI2:
   1.125 +  "b \<preceq> c \<Longrightarrow> a * b \<preceq> c"
   1.126 +  by (rule trans) auto
   1.127 +
   1.128 +lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d"
   1.129 +  by (blast intro: boundedI coboundedI1 coboundedI2)
   1.130 +
   1.131 +lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a"
   1.132 +  by (rule antisym) (auto simp add: refl bounded_iff)
   1.133 +
   1.134 +lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b"
   1.135 +  by (rule antisym) (auto simp add: refl bounded_iff)
   1.136  
   1.137  end
   1.138  
   1.139 +locale semilattice_neutr_order = semilattice_neutr + semilattice_order
   1.140 +
   1.141 +sublocale semilattice_neutr_order < ordering_top less_eq less 1
   1.142 +  by default (simp add: order_iff)
   1.143 +
   1.144 +notation times (infixl "*" 70)
   1.145 +notation Groups.one ("1")
   1.146 +
   1.147  
   1.148  subsection {* Syntactic infimum and supremum operations *}
   1.149  
   1.150 @@ -171,6 +266,23 @@
   1.151      by (rule antisym) auto
   1.152  qed
   1.153  
   1.154 +sublocale semilattice_sup < sup!: semilattice sup
   1.155 +proof
   1.156 +  fix a b c
   1.157 +  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
   1.158 +    by (rule antisym) (auto intro: le_supI1 le_supI2)
   1.159 +  show "a \<squnion> b = b \<squnion> a"
   1.160 +    by (rule antisym) auto
   1.161 +  show "a \<squnion> a = a"
   1.162 +    by (rule antisym) auto
   1.163 +qed
   1.164 +
   1.165 +sublocale semilattice_inf < inf!: semilattice_order inf less_eq less
   1.166 +  by default (auto simp add: le_iff_inf less_le)
   1.167 +
   1.168 +sublocale semilattice_sup < sup!: semilattice_order sup greater_eq greater
   1.169 +  by default (auto simp add: le_iff_sup sup.commute less_le)
   1.170 +
   1.171  context semilattice_inf
   1.172  begin
   1.173  
   1.174 @@ -202,17 +314,6 @@
   1.175  
   1.176  end
   1.177  
   1.178 -sublocale semilattice_sup < sup!: semilattice sup
   1.179 -proof
   1.180 -  fix a b c
   1.181 -  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
   1.182 -    by (rule antisym) (auto intro: le_supI1 le_supI2)
   1.183 -  show "a \<squnion> b = b \<squnion> a"
   1.184 -    by (rule antisym) auto
   1.185 -  show "a \<squnion> a = a"
   1.186 -    by (rule antisym) auto
   1.187 -qed
   1.188 -
   1.189  context semilattice_sup
   1.190  begin
   1.191  
   1.192 @@ -367,9 +468,33 @@
   1.193  
   1.194  subsection {* Bounded lattices and boolean algebras *}
   1.195  
   1.196 +class bounded_semilattice_inf_top = semilattice_inf + top
   1.197 +
   1.198 +sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
   1.199 +proof
   1.200 +  fix x
   1.201 +  show "x \<sqinter> \<top> = x"
   1.202 +    by (rule inf_absorb1) simp
   1.203 +qed
   1.204 +
   1.205 +sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr_order inf top less_eq less ..
   1.206 +
   1.207 +class bounded_semilattice_sup_bot = semilattice_sup + bot
   1.208 +
   1.209 +sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
   1.210 +proof
   1.211 +  fix x
   1.212 +  show "x \<squnion> \<bottom> = x"
   1.213 +    by (rule sup_absorb1) simp
   1.214 +qed
   1.215 +
   1.216 +sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr_order sup bot greater_eq greater ..
   1.217 +
   1.218  class bounded_lattice_bot = lattice + bot
   1.219  begin
   1.220  
   1.221 +subclass bounded_semilattice_sup_bot ..
   1.222 +
   1.223  lemma inf_bot_left [simp]:
   1.224    "\<bottom> \<sqinter> x = \<bottom>"
   1.225    by (rule inf_absorb1) simp
   1.226 @@ -378,13 +503,13 @@
   1.227    "x \<sqinter> \<bottom> = \<bottom>"
   1.228    by (rule inf_absorb2) simp
   1.229  
   1.230 -lemma sup_bot_left [simp]:
   1.231 +lemma sup_bot_left:
   1.232    "\<bottom> \<squnion> x = x"
   1.233 -  by (rule sup_absorb2) simp
   1.234 +  by (fact sup_bot.left_neutral)
   1.235  
   1.236 -lemma sup_bot_right [simp]:
   1.237 +lemma sup_bot_right:
   1.238    "x \<squnion> \<bottom> = x"
   1.239 -  by (rule sup_absorb1) simp
   1.240 +  by (fact sup_bot.right_neutral)
   1.241  
   1.242  lemma sup_eq_bot_iff [simp]:
   1.243    "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   1.244 @@ -395,6 +520,8 @@
   1.245  class bounded_lattice_top = lattice + top
   1.246  begin
   1.247  
   1.248 +subclass bounded_semilattice_inf_top ..
   1.249 +
   1.250  lemma sup_top_left [simp]:
   1.251    "\<top> \<squnion> x = \<top>"
   1.252    by (rule sup_absorb1) simp
   1.253 @@ -403,13 +530,13 @@
   1.254    "x \<squnion> \<top> = \<top>"
   1.255    by (rule sup_absorb2) simp
   1.256  
   1.257 -lemma inf_top_left [simp]:
   1.258 +lemma inf_top_left:
   1.259    "\<top> \<sqinter> x = x"
   1.260 -  by (rule inf_absorb2) simp
   1.261 +  by (fact inf_top.left_neutral)
   1.262  
   1.263 -lemma inf_top_right [simp]:
   1.264 +lemma inf_top_right:
   1.265    "x \<sqinter> \<top> = x"
   1.266 -  by (rule inf_absorb1) simp
   1.267 +  by (fact inf_top.right_neutral)
   1.268  
   1.269  lemma inf_eq_top_iff [simp]:
   1.270    "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   1.271 @@ -417,9 +544,12 @@
   1.272  
   1.273  end
   1.274  
   1.275 -class bounded_lattice = bounded_lattice_bot + bounded_lattice_top
   1.276 +class bounded_lattice = lattice + bot + top
   1.277  begin
   1.278  
   1.279 +subclass bounded_lattice_bot ..
   1.280 +subclass bounded_lattice_top ..
   1.281 +
   1.282  lemma dual_bounded_lattice:
   1.283    "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
   1.284    by unfold_locales (auto simp add: less_le_not_le)