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.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)
```