author  haftmann 
Tue, 14 Jul 2009 15:54:19 +0200  
changeset 32064  53ca12ff305d 
parent 32063  2aab4f2af536 
child 32204  b330aa4d59cb 
permissions  rwrr 
21249  1 
(* Title: HOL/Lattices.thy 
2 
Author: Tobias Nipkow 

3 
*) 

4 

22454  5 
header {* Abstract lattices *} 
21249  6 

7 
theory Lattices 

30302  8 
imports Orderings 
21249  9 
begin 
10 

28562  11 
subsection {* Lattices *} 
21249  12 

25206  13 
notation 
25382  14 
less_eq (infix "\<sqsubseteq>" 50) and 
15 
less (infix "\<sqsubset>" 50) 

25206  16 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

17 
class lower_semilattice = order + 
21249  18 
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) 
22737  19 
assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" 
20 
and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" 

21733  21 
and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" 
21249  22 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

23 
class upper_semilattice = order + 
21249  24 
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) 
22737  25 
assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" 
26 
and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" 

21733  27 
and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x" 
26014  28 
begin 
29 

30 
text {* Dual lattice *} 

31 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

32 
lemma dual_semilattice: 
26014  33 
"lower_semilattice (op \<ge>) (op >) sup" 
27682  34 
by (rule lower_semilattice.intro, rule dual_order) 
35 
(unfold_locales, simp_all add: sup_least) 

26014  36 

37 
end 

21249  38 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

39 
class lattice = lower_semilattice + upper_semilattice 
21249  40 

25382  41 

28562  42 
subsubsection {* Intro and elim rules*} 
21733  43 

44 
context lower_semilattice 

45 
begin 

21249  46 

32064  47 
lemma le_infI1: 
48 
"a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" 

49 
by (rule order_trans) auto 

21249  50 

32064  51 
lemma le_infI2: 
52 
"b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" 

53 
by (rule order_trans) auto 

21733  54 

32064  55 
lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b" 
56 
by (blast intro: inf_greatest) 

21249  57 

32064  58 
lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" 
59 
by (blast intro: order_trans le_infI1 le_infI2) 

21249  60 

21734  61 
lemma le_inf_iff [simp]: 
32064  62 
"x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z" 
63 
by (blast intro: le_infI elim: le_infE) 

21733  64 

32064  65 
lemma le_iff_inf: 
66 
"x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x" 

67 
by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) 

21249  68 

25206  69 
lemma mono_inf: 
70 
fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice" 

71 
shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" 

72 
by (auto simp add: mono_def intro: Lattices.inf_greatest) 

21733  73 

25206  74 
end 
21733  75 

76 
context upper_semilattice 

77 
begin 

21249  78 

32064  79 
lemma le_supI1: 
80 
"x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" 

25062  81 
by (rule order_trans) auto 
21249  82 

32064  83 
lemma le_supI2: 
84 
"x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" 

25062  85 
by (rule order_trans) auto 
21733  86 

32064  87 
lemma le_supI: 
88 
"a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x" 

26014  89 
by (blast intro: sup_least) 
21249  90 

32064  91 
lemma le_supE: 
92 
"a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" 

93 
by (blast intro: le_supI1 le_supI2 order_trans) 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

94 

32064  95 
lemma le_sup_iff [simp]: 
96 
"x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" 

97 
by (blast intro: le_supI elim: le_supE) 

21733  98 

32064  99 
lemma le_iff_sup: 
100 
"x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y" 

101 
by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) 

21734  102 

25206  103 
lemma mono_sup: 
104 
fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice" 

105 
shows "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" 

106 
by (auto simp add: mono_def intro: Lattices.sup_least) 

21733  107 

25206  108 
end 
23878  109 

21733  110 

32064  111 
subsubsection {* Equational laws *} 
21249  112 

21733  113 
context lower_semilattice 
114 
begin 

115 

116 
lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" 

32064  117 
by (rule antisym) auto 
21733  118 

119 
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" 

32064  120 
by (rule antisym) (auto intro: le_infI1 le_infI2) 
21733  121 

122 
lemma inf_idem[simp]: "x \<sqinter> x = x" 

32064  123 
by (rule antisym) auto 
21733  124 

125 
lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" 

32064  126 
by (rule antisym) (auto intro: le_infI2) 
21733  127 

128 
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" 

32064  129 
by (rule antisym) auto 
21733  130 

131 
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" 

32064  132 
by (rule antisym) auto 
21733  133 

134 
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" 

32064  135 
by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+ 
136 

137 
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem 

21733  138 

139 
end 

140 

141 
context upper_semilattice 

142 
begin 

21249  143 

21733  144 
lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)" 
32064  145 
by (rule antisym) auto 
21733  146 

147 
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" 

32064  148 
by (rule antisym) (auto intro: le_supI1 le_supI2) 
21733  149 

150 
lemma sup_idem[simp]: "x \<squnion> x = x" 

32064  151 
by (rule antisym) auto 
21733  152 

153 
lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" 

32064  154 
by (rule antisym) (auto intro: le_supI2) 
21733  155 

156 
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" 

32064  157 
by (rule antisym) auto 
21733  158 

159 
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" 

32064  160 
by (rule antisym) auto 
21249  161 

21733  162 
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)" 
32064  163 
by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+ 
21733  164 

32064  165 
lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem 
21733  166 

167 
end 

21249  168 

21733  169 
context lattice 
170 
begin 

171 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

172 
lemma dual_lattice: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

173 
"lattice (op \<ge>) (op >) sup inf" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

174 
by (rule lattice.intro, rule dual_semilattice, rule upper_semilattice.intro, rule dual_order) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

175 
(unfold_locales, auto) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

176 

21733  177 
lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

178 
by (blast intro: antisym inf_le1 inf_greatest sup_ge1) 
21733  179 

180 
lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x" 

25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

181 
by (blast intro: antisym sup_ge1 sup_least inf_le1) 
21733  182 

32064  183 
lemmas inf_sup_aci = inf_aci sup_aci 
21734  184 

22454  185 
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 
186 

21734  187 
text{* Towards distributivity *} 
21249  188 

21734  189 
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
32064  190 
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) 
21734  191 

192 
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)" 

32064  193 
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) 
21734  194 

195 
text{* If you have one of them, you have them all. *} 

21249  196 

21733  197 
lemma distrib_imp1: 
21249  198 
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 
199 
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 

200 
proof 

201 
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb) 

202 
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc) 

203 
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" 

204 
by(simp add:inf_sup_absorb inf_commute) 

205 
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D) 

206 
finally show ?thesis . 

207 
qed 

208 

21733  209 
lemma distrib_imp2: 
21249  210 
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
211 
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 

212 
proof 

213 
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb) 

214 
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc) 

215 
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" 

216 
by(simp add:sup_inf_absorb sup_commute) 

217 
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D) 

218 
finally show ?thesis . 

219 
qed 

220 

21733  221 
end 
21249  222 

223 

24164  224 
subsection {* Distributive lattices *} 
21249  225 

22454  226 
class distrib_lattice = lattice + 
21249  227 
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
228 

21733  229 
context distrib_lattice 
230 
begin 

231 

232 
lemma sup_inf_distrib2: 

21249  233 
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" 
32064  234 
by(simp add: inf_sup_aci sup_inf_distrib1) 
21249  235 

21733  236 
lemma inf_sup_distrib1: 
21249  237 
"x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 
238 
by(rule distrib_imp2[OF sup_inf_distrib1]) 

239 

21733  240 
lemma inf_sup_distrib2: 
21249  241 
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" 
32064  242 
by(simp add: inf_sup_aci inf_sup_distrib1) 
21249  243 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

244 
lemma dual_distrib_lattice: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

245 
"distrib_lattice (op \<ge>) (op >) sup inf" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

246 
by (rule distrib_lattice.intro, rule dual_lattice) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

247 
(unfold_locales, fact inf_sup_distrib1) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

248 

21733  249 
lemmas distrib = 
21249  250 
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 
251 

21733  252 
end 
253 

21249  254 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

255 
subsection {* Boolean algebras *} 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

256 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

257 
class boolean_algebra = distrib_lattice + top + bot + minus + uminus + 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

258 
assumes inf_compl_bot: "x \<sqinter>  x = bot" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

259 
and sup_compl_top: "x \<squnion>  x = top" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

260 
assumes diff_eq: "x  y = x \<sqinter>  y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

261 
begin 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

262 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

263 
lemma dual_boolean_algebra: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

264 
"boolean_algebra (\<lambda>x y. x \<squnion>  y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) top bot" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

265 
by (rule boolean_algebra.intro, rule dual_distrib_lattice) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

266 
(unfold_locales, 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

267 
auto simp add: inf_compl_bot sup_compl_top diff_eq less_le_not_le) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

268 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

269 
lemma compl_inf_bot: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

270 
" x \<sqinter> x = bot" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

271 
by (simp add: inf_commute inf_compl_bot) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

272 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

273 
lemma compl_sup_top: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

274 
" x \<squnion> x = top" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

275 
by (simp add: sup_commute sup_compl_top) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

276 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

277 
lemma inf_bot_left [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

278 
"bot \<sqinter> x = bot" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

279 
by (rule inf_absorb1) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

280 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

281 
lemma inf_bot_right [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

282 
"x \<sqinter> bot = bot" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

283 
by (rule inf_absorb2) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

284 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

285 
lemma sup_top_left [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

286 
"top \<squnion> x = top" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

287 
by (rule sup_absorb1) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

288 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

289 
lemma sup_top_right [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

290 
"x \<squnion> top = top" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

291 
by (rule sup_absorb2) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

292 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

293 
lemma inf_top_left [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

294 
"top \<sqinter> x = x" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

295 
by (rule inf_absorb2) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

296 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

297 
lemma inf_top_right [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

298 
"x \<sqinter> top = x" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

299 
by (rule inf_absorb1) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

300 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

301 
lemma sup_bot_left [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

302 
"bot \<squnion> x = x" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

303 
by (rule sup_absorb2) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

304 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

305 
lemma sup_bot_right [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

306 
"x \<squnion> bot = x" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

307 
by (rule sup_absorb1) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

308 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

309 
lemma compl_unique: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

310 
assumes "x \<sqinter> y = bot" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

311 
and "x \<squnion> y = top" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

312 
shows " x = y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

313 
proof  
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

314 
have "(x \<sqinter>  x) \<squnion> ( x \<sqinter> y) = (x \<sqinter> y) \<squnion> ( x \<sqinter> y)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

315 
using inf_compl_bot assms(1) by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

316 
then have "( x \<sqinter> x) \<squnion> ( x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter>  x)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

317 
by (simp add: inf_commute) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

318 
then have " x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion>  x)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

319 
by (simp add: inf_sup_distrib1) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

320 
then have " x \<sqinter> top = y \<sqinter> top" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

321 
using sup_compl_top assms(2) by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

322 
then show " x = y" by (simp add: inf_top_right) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

323 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

324 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

325 
lemma double_compl [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

326 
" ( x) = x" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

327 
using compl_inf_bot compl_sup_top by (rule compl_unique) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

328 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

329 
lemma compl_eq_compl_iff [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

330 
" x =  y \<longleftrightarrow> x = y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

331 
proof 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

332 
assume " x =  y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

333 
then have " x \<sqinter> y = bot" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

334 
and " x \<squnion> y = top" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

335 
by (simp_all add: compl_inf_bot compl_sup_top) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

336 
then have " ( x) = y" by (rule compl_unique) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

337 
then show "x = y" by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

338 
next 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

339 
assume "x = y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

340 
then show " x =  y" by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

341 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

342 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

343 
lemma compl_bot_eq [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

344 
" bot = top" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

345 
proof  
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

346 
from sup_compl_top have "bot \<squnion>  bot = top" . 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

347 
then show ?thesis by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

348 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

349 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

350 
lemma compl_top_eq [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

351 
" top = bot" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

352 
proof  
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

353 
from inf_compl_bot have "top \<sqinter>  top = bot" . 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

354 
then show ?thesis by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

355 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

356 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

357 
lemma compl_inf [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

358 
" (x \<sqinter> y) =  x \<squnion>  y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

359 
proof (rule compl_unique) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

360 
have "(x \<sqinter> y) \<sqinter> ( x \<squnion>  y) = ((x \<sqinter> y) \<sqinter>  x) \<squnion> ((x \<sqinter> y) \<sqinter>  y)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

361 
by (rule inf_sup_distrib1) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

362 
also have "... = (y \<sqinter> (x \<sqinter>  x)) \<squnion> (x \<sqinter> (y \<sqinter>  y))" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

363 
by (simp only: inf_commute inf_assoc inf_left_commute) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

364 
finally show "(x \<sqinter> y) \<sqinter> ( x \<squnion>  y) = bot" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

365 
by (simp add: inf_compl_bot) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

366 
next 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

367 
have "(x \<sqinter> y) \<squnion> ( x \<squnion>  y) = (x \<squnion> ( x \<squnion>  y)) \<sqinter> (y \<squnion> ( x \<squnion>  y))" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

368 
by (rule sup_inf_distrib2) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

369 
also have "... = ( y \<squnion> (x \<squnion>  x)) \<sqinter> ( x \<squnion> (y \<squnion>  y))" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

370 
by (simp only: sup_commute sup_assoc sup_left_commute) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

371 
finally show "(x \<sqinter> y) \<squnion> ( x \<squnion>  y) = top" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

372 
by (simp add: sup_compl_top) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

373 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

374 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

375 
lemma compl_sup [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

376 
" (x \<squnion> y) =  x \<sqinter>  y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

377 
proof  
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

378 
interpret boolean_algebra "\<lambda>x y. x \<squnion>  y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

379 
by (rule dual_boolean_algebra) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

380 
then show ?thesis by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

381 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

382 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

383 
end 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

384 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

385 

22454  386 
subsection {* Uniqueness of inf and sup *} 
387 

22737  388 
lemma (in lower_semilattice) inf_unique: 
22454  389 
fixes f (infixl "\<triangle>" 70) 
25062  390 
assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y" 
391 
and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" 

22737  392 
shows "x \<sqinter> y = x \<triangle> y" 
22454  393 
proof (rule antisym) 
25062  394 
show "x \<triangle> y \<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2) 
22454  395 
next 
25062  396 
have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest) 
397 
show "x \<sqinter> y \<le> x \<triangle> y" by (rule leI) simp_all 

22454  398 
qed 
399 

22737  400 
lemma (in upper_semilattice) sup_unique: 
22454  401 
fixes f (infixl "\<nabla>" 70) 
25062  402 
assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y" 
403 
and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x" 

22737  404 
shows "x \<squnion> y = x \<nabla> y" 
22454  405 
proof (rule antisym) 
25062  406 
show "x \<squnion> y \<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2) 
22454  407 
next 
25062  408 
have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least) 
409 
show "x \<nabla> y \<le> x \<squnion> y" by (rule leI) simp_all 

22454  410 
qed 
411 

412 

22916  413 
subsection {* @{const min}/@{const max} on linear orders as 
414 
special case of @{const inf}/@{const sup} *} 

415 

416 
lemma (in linorder) distrib_lattice_min_max: 

25062  417 
"distrib_lattice (op \<le>) (op <) min max" 
28823  418 
proof 
25062  419 
have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" 
22916  420 
by (auto simp add: less_le antisym) 
421 
fix x y z 

422 
show "max x (min y z) = min (max x y) (max x z)" 

423 
unfolding min_def max_def 

24640
85a6c200ecd3
Simplified proofs due to transitivity reasoner setup.
ballarin
parents:
24514
diff
changeset

424 
by auto 
22916  425 
qed (auto simp add: min_def max_def not_le less_imp_le) 
21249  426 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30302
diff
changeset

427 
interpretation min_max: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max 
23948  428 
by (rule distrib_lattice_min_max) 
21249  429 

22454  430 
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

431 
by (rule ext)+ (auto intro: antisym) 
21733  432 

22454  433 
lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{upper_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

434 
by (rule ext)+ (auto intro: antisym) 
21733  435 

21249  436 
lemmas le_maxI1 = min_max.sup_ge1 
437 
lemmas le_maxI2 = min_max.sup_ge2 

21381  438 

21249  439 
lemmas max_ac = min_max.sup_assoc min_max.sup_commute 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

440 
mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute] 
21249  441 

442 
lemmas min_ac = min_max.inf_assoc min_max.inf_commute 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

443 
mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute] 
21249  444 

22454  445 

446 
subsection {* Bool as lattice *} 

447 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

448 
instantiation bool :: boolean_algebra 
25510  449 
begin 
450 

451 
definition 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

452 
bool_Compl_def: "uminus = Not" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

453 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

454 
definition 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

455 
bool_diff_def: "A  B \<longleftrightarrow> A \<and> \<not> B" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

456 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

457 
definition 
25510  458 
inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" 
459 

460 
definition 

461 
sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" 

462 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

463 
instance proof 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

464 
qed (simp_all add: inf_bool_eq sup_bool_eq le_bool_def 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

465 
bot_bool_eq top_bool_eq bool_Compl_def bool_diff_def, auto) 
22454  466 

25510  467 
end 
468 

23878  469 

470 
subsection {* Fun as lattice *} 

471 

25510  472 
instantiation "fun" :: (type, lattice) lattice 
473 
begin 

474 

475 
definition 

28562  476 
inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" 
25510  477 

478 
definition 

28562  479 
sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" 
25510  480 

481 
instance 

23878  482 
apply intro_classes 
483 
unfolding inf_fun_eq sup_fun_eq 

484 
apply (auto intro: le_funI) 

485 
apply (rule le_funI) 

486 
apply (auto dest: le_funD) 

487 
apply (rule le_funI) 

488 
apply (auto dest: le_funD) 

489 
done 

490 

25510  491 
end 
23878  492 

493 
instance "fun" :: (type, distrib_lattice) distrib_lattice 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

494 
proof 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

495 
qed (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

496 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

497 
instantiation "fun" :: (type, uminus) uminus 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

498 
begin 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

499 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

500 
definition 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

501 
fun_Compl_def: " A = (\<lambda>x.  A x)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

502 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

503 
instance .. 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

504 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

505 
end 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

506 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

507 
instantiation "fun" :: (type, minus) minus 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

508 
begin 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

509 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

510 
definition 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

511 
fun_diff_def: "A  B = (\<lambda>x. A x  B x)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

512 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

513 
instance .. 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

514 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

515 
end 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

516 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

517 
instance "fun" :: (type, boolean_algebra) boolean_algebra 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

518 
proof 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

519 
qed (simp_all add: inf_fun_eq sup_fun_eq bot_fun_eq top_fun_eq fun_Compl_def fun_diff_def 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

520 
inf_compl_bot sup_compl_top diff_eq) 
23878  521 

26794  522 

23878  523 
text {* redundant bindings *} 
22454  524 

525 

25062  526 
no_notation 
25382  527 
less_eq (infix "\<sqsubseteq>" 50) and 
528 
less (infix "\<sqsubset>" 50) and 

529 
inf (infixl "\<sqinter>" 70) and 

30302  530 
sup (infixl "\<squnion>" 65) 
25062  531 

21249  532 
end 