author | haftmann |
Thu, 03 Sep 2009 15:39:02 +0200 | |
changeset 32512 | d14762642cdd |
parent 32436 | 10cd49e0c067 |
child 32568 | 89518a3074e1 |
permissions | -rw-r--r-- |
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 |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32204
diff
changeset
|
128 |
lemma inf_absorb1[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
32064 | 129 |
by (rule antisym) auto |
21733 | 130 |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32204
diff
changeset
|
131 |
lemma inf_absorb2[simp]: "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 |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32204
diff
changeset
|
156 |
lemma sup_absorb1[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" |
32064 | 157 |
by (rule antisym) auto |
21733 | 158 |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32204
diff
changeset
|
159 |
lemma sup_absorb2[simp]: "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) |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32204
diff
changeset
|
202 |
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc del:sup_absorb1) |
21249 | 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) |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32204
diff
changeset
|
214 |
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc del:inf_absorb1) |
21249 | 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 |
||
32512 | 416 |
sublocale linorder < min_max!: distrib_lattice less_eq less min max |
28823 | 417 |
proof |
22916 | 418 |
fix x y z |
32512 | 419 |
show "max x (min y z) = min (max x y) (max x z)" |
420 |
by (auto simp add: min_def max_def) |
|
22916 | 421 |
qed (auto simp add: min_def max_def not_le less_imp_le) |
21249 | 422 |
|
22454 | 423 |
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
|
424 |
by (rule ext)+ (auto intro: antisym) |
21733 | 425 |
|
22454 | 426 |
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
|
427 |
by (rule ext)+ (auto intro: antisym) |
21733 | 428 |
|
21249 | 429 |
lemmas le_maxI1 = min_max.sup_ge1 |
430 |
lemmas le_maxI2 = min_max.sup_ge2 |
|
21381 | 431 |
|
21249 | 432 |
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
|
433 |
mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute] |
21249 | 434 |
|
435 |
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
|
436 |
mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute] |
21249 | 437 |
|
22454 | 438 |
|
439 |
subsection {* Bool as lattice *} |
|
440 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
441 |
instantiation bool :: boolean_algebra |
25510 | 442 |
begin |
443 |
||
444 |
definition |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
445 |
bool_Compl_def: "uminus = Not" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
446 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
447 |
definition |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
448 |
bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
449 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
450 |
definition |
25510 | 451 |
inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" |
452 |
||
453 |
definition |
|
454 |
sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" |
|
455 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
456 |
instance proof |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
457 |
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
|
458 |
bot_bool_eq top_bool_eq bool_Compl_def bool_diff_def, auto) |
22454 | 459 |
|
25510 | 460 |
end |
461 |
||
23878 | 462 |
|
463 |
subsection {* Fun as lattice *} |
|
464 |
||
25510 | 465 |
instantiation "fun" :: (type, lattice) lattice |
466 |
begin |
|
467 |
||
468 |
definition |
|
28562 | 469 |
inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" |
25510 | 470 |
|
471 |
definition |
|
28562 | 472 |
sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
25510 | 473 |
|
474 |
instance |
|
23878 | 475 |
apply intro_classes |
476 |
unfolding inf_fun_eq sup_fun_eq |
|
477 |
apply (auto intro: le_funI) |
|
478 |
apply (rule le_funI) |
|
479 |
apply (auto dest: le_funD) |
|
480 |
apply (rule le_funI) |
|
481 |
apply (auto dest: le_funD) |
|
482 |
done |
|
483 |
||
25510 | 484 |
end |
23878 | 485 |
|
486 |
instance "fun" :: (type, distrib_lattice) distrib_lattice |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
487 |
proof |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
488 |
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
|
489 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
490 |
instantiation "fun" :: (type, uminus) uminus |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
491 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
492 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
493 |
definition |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
494 |
fun_Compl_def: "- A = (\<lambda>x. - A x)" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
495 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
496 |
instance .. |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
497 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
498 |
end |
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 |
instantiation "fun" :: (type, minus) minus |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
501 |
begin |
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 |
definition |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
504 |
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
|
505 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
506 |
instance .. |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
507 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
508 |
end |
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 |
instance "fun" :: (type, boolean_algebra) boolean_algebra |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
511 |
proof |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
512 |
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
|
513 |
inf_compl_bot sup_compl_top diff_eq) |
23878 | 514 |
|
26794 | 515 |
|
25062 | 516 |
no_notation |
25382 | 517 |
less_eq (infix "\<sqsubseteq>" 50) and |
518 |
less (infix "\<sqsubset>" 50) and |
|
519 |
inf (infixl "\<sqinter>" 70) and |
|
30302 | 520 |
sup (infixl "\<squnion>" 65) |
25062 | 521 |
|
21249 | 522 |
end |