author | haftmann |
Fri, 12 Feb 2010 14:28:01 +0100 | |
changeset 35121 | 36c0a6dd8c6f |
parent 35028 | 108662d50512 |
child 35301 | 90e42f9ba4d1 |
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 |
|
35121 | 8 |
imports Orderings Groups |
21249 | 9 |
begin |
10 |
||
28562 | 11 |
subsection {* Lattices *} |
21249 | 12 |
|
25206 | 13 |
notation |
25382 | 14 |
less_eq (infix "\<sqsubseteq>" 50) and |
32568 | 15 |
less (infix "\<sqsubset>" 50) and |
16 |
top ("\<top>") and |
|
17 |
bot ("\<bottom>") |
|
25206 | 18 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
19 |
class semilattice_inf = order + |
21249 | 20 |
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
22737 | 21 |
assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" |
22 |
and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" |
|
21733 | 23 |
and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" |
21249 | 24 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
25 |
class semilattice_sup = order + |
21249 | 26 |
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
22737 | 27 |
assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" |
28 |
and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" |
|
21733 | 29 |
and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x" |
26014 | 30 |
begin |
31 |
||
32 |
text {* Dual lattice *} |
|
33 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
34 |
lemma dual_semilattice: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
35 |
"semilattice_inf (op \<ge>) (op >) sup" |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
36 |
by (rule semilattice_inf.intro, rule dual_order) |
27682 | 37 |
(unfold_locales, simp_all add: sup_least) |
26014 | 38 |
|
39 |
end |
|
21249 | 40 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
41 |
class lattice = semilattice_inf + semilattice_sup |
21249 | 42 |
|
25382 | 43 |
|
28562 | 44 |
subsubsection {* Intro and elim rules*} |
21733 | 45 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
46 |
context semilattice_inf |
21733 | 47 |
begin |
21249 | 48 |
|
32064 | 49 |
lemma le_infI1: |
50 |
"a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
|
51 |
by (rule order_trans) auto |
|
21249 | 52 |
|
32064 | 53 |
lemma le_infI2: |
54 |
"b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
|
55 |
by (rule order_trans) auto |
|
21733 | 56 |
|
32064 | 57 |
lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b" |
58 |
by (blast intro: inf_greatest) |
|
21249 | 59 |
|
32064 | 60 |
lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" |
61 |
by (blast intro: order_trans le_infI1 le_infI2) |
|
21249 | 62 |
|
21734 | 63 |
lemma le_inf_iff [simp]: |
32064 | 64 |
"x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z" |
65 |
by (blast intro: le_infI elim: le_infE) |
|
21733 | 66 |
|
32064 | 67 |
lemma le_iff_inf: |
68 |
"x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x" |
|
69 |
by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) |
|
21249 | 70 |
|
25206 | 71 |
lemma mono_inf: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
72 |
fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf" |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
73 |
shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" |
25206 | 74 |
by (auto simp add: mono_def intro: Lattices.inf_greatest) |
21733 | 75 |
|
25206 | 76 |
end |
21733 | 77 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
78 |
context semilattice_sup |
21733 | 79 |
begin |
21249 | 80 |
|
32064 | 81 |
lemma le_supI1: |
82 |
"x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
|
25062 | 83 |
by (rule order_trans) auto |
21249 | 84 |
|
32064 | 85 |
lemma le_supI2: |
86 |
"x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
|
25062 | 87 |
by (rule order_trans) auto |
21733 | 88 |
|
32064 | 89 |
lemma le_supI: |
90 |
"a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x" |
|
26014 | 91 |
by (blast intro: sup_least) |
21249 | 92 |
|
32064 | 93 |
lemma le_supE: |
94 |
"a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" |
|
95 |
by (blast intro: le_supI1 le_supI2 order_trans) |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
96 |
|
32064 | 97 |
lemma le_sup_iff [simp]: |
98 |
"x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
|
99 |
by (blast intro: le_supI elim: le_supE) |
|
21733 | 100 |
|
32064 | 101 |
lemma le_iff_sup: |
102 |
"x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y" |
|
103 |
by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) |
|
21734 | 104 |
|
25206 | 105 |
lemma mono_sup: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
106 |
fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup" |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
107 |
shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" |
25206 | 108 |
by (auto simp add: mono_def intro: Lattices.sup_least) |
21733 | 109 |
|
25206 | 110 |
end |
23878 | 111 |
|
21733 | 112 |
|
32064 | 113 |
subsubsection {* Equational laws *} |
21249 | 114 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
115 |
sublocale semilattice_inf < inf!: semilattice inf |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
116 |
proof |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
117 |
fix a b c |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
118 |
show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
119 |
by (rule antisym) (auto intro: le_infI1 le_infI2) |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
120 |
show "a \<sqinter> b = b \<sqinter> a" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
121 |
by (rule antisym) auto |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
122 |
show "a \<sqinter> a = a" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
123 |
by (rule antisym) auto |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
124 |
qed |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
125 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
126 |
context semilattice_inf |
21733 | 127 |
begin |
128 |
||
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
129 |
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
130 |
by (fact inf.assoc) |
21733 | 131 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
132 |
lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
133 |
by (fact inf.commute) |
21733 | 134 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
135 |
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
136 |
by (fact inf.left_commute) |
21733 | 137 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
138 |
lemma inf_idem: "x \<sqinter> x = x" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
139 |
by (fact inf.idem) |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
140 |
|
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
141 |
lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
142 |
by (fact inf.left_idem) |
21733 | 143 |
|
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset
|
144 |
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
32064 | 145 |
by (rule antisym) auto |
21733 | 146 |
|
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset
|
147 |
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" |
32064 | 148 |
by (rule antisym) auto |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
149 |
|
32064 | 150 |
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem |
21733 | 151 |
|
152 |
end |
|
153 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
154 |
sublocale semilattice_sup < sup!: semilattice sup |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
155 |
proof |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
156 |
fix a b c |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
157 |
show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
158 |
by (rule antisym) (auto intro: le_supI1 le_supI2) |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
159 |
show "a \<squnion> b = b \<squnion> a" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
160 |
by (rule antisym) auto |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
161 |
show "a \<squnion> a = a" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
162 |
by (rule antisym) auto |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
163 |
qed |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
164 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
165 |
context semilattice_sup |
21733 | 166 |
begin |
21249 | 167 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
168 |
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
169 |
by (fact sup.assoc) |
21733 | 170 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
171 |
lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
172 |
by (fact sup.commute) |
21733 | 173 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
174 |
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
175 |
by (fact sup.left_commute) |
21733 | 176 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
177 |
lemma sup_idem: "x \<squnion> x = x" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
178 |
by (fact sup.idem) |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
179 |
|
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
180 |
lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
181 |
by (fact sup.left_idem) |
21733 | 182 |
|
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset
|
183 |
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" |
32064 | 184 |
by (rule antisym) auto |
21733 | 185 |
|
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset
|
186 |
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" |
32064 | 187 |
by (rule antisym) auto |
21249 | 188 |
|
32064 | 189 |
lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem |
21733 | 190 |
|
191 |
end |
|
21249 | 192 |
|
21733 | 193 |
context lattice |
194 |
begin |
|
195 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
196 |
lemma dual_lattice: |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
197 |
"lattice (op \<ge>) (op >) sup inf" |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
198 |
by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order) |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
199 |
(unfold_locales, auto) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
200 |
|
21733 | 201 |
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
|
202 |
by (blast intro: antisym inf_le1 inf_greatest sup_ge1) |
21733 | 203 |
|
204 |
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
|
205 |
by (blast intro: antisym sup_ge1 sup_least inf_le1) |
21733 | 206 |
|
32064 | 207 |
lemmas inf_sup_aci = inf_aci sup_aci |
21734 | 208 |
|
22454 | 209 |
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 |
210 |
||
21734 | 211 |
text{* Towards distributivity *} |
21249 | 212 |
|
21734 | 213 |
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
32064 | 214 |
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
21734 | 215 |
|
216 |
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)" |
|
32064 | 217 |
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
21734 | 218 |
|
219 |
text{* If you have one of them, you have them all. *} |
|
21249 | 220 |
|
21733 | 221 |
lemma distrib_imp1: |
21249 | 222 |
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
223 |
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
|
224 |
proof- |
|
225 |
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb) |
|
34209 | 226 |
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc) |
21249 | 227 |
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" |
228 |
by(simp add:inf_sup_absorb inf_commute) |
|
229 |
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D) |
|
230 |
finally show ?thesis . |
|
231 |
qed |
|
232 |
||
21733 | 233 |
lemma distrib_imp2: |
21249 | 234 |
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
235 |
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
|
236 |
proof- |
|
237 |
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb) |
|
34209 | 238 |
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc) |
21249 | 239 |
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" |
240 |
by(simp add:sup_inf_absorb sup_commute) |
|
241 |
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D) |
|
242 |
finally show ?thesis . |
|
243 |
qed |
|
244 |
||
21733 | 245 |
end |
21249 | 246 |
|
32568 | 247 |
subsubsection {* Strict order *} |
248 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
249 |
context semilattice_inf |
32568 | 250 |
begin |
251 |
||
252 |
lemma less_infI1: |
|
253 |
"a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x" |
|
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset
|
254 |
by (auto simp add: less_le inf_absorb1 intro: le_infI1) |
32568 | 255 |
|
256 |
lemma less_infI2: |
|
257 |
"b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x" |
|
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset
|
258 |
by (auto simp add: less_le inf_absorb2 intro: le_infI2) |
32568 | 259 |
|
260 |
end |
|
261 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
262 |
context semilattice_sup |
32568 | 263 |
begin |
264 |
||
265 |
lemma less_supI1: |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
266 |
"x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b" |
32568 | 267 |
proof - |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
268 |
interpret dual: semilattice_inf "op \<ge>" "op >" sup |
32568 | 269 |
by (fact dual_semilattice) |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
270 |
assume "x \<sqsubset> a" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
271 |
then show "x \<sqsubset> a \<squnion> b" |
32568 | 272 |
by (fact dual.less_infI1) |
273 |
qed |
|
274 |
||
275 |
lemma less_supI2: |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
276 |
"x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b" |
32568 | 277 |
proof - |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
278 |
interpret dual: semilattice_inf "op \<ge>" "op >" sup |
32568 | 279 |
by (fact dual_semilattice) |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
280 |
assume "x \<sqsubset> b" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
281 |
then show "x \<sqsubset> a \<squnion> b" |
32568 | 282 |
by (fact dual.less_infI2) |
283 |
qed |
|
284 |
||
285 |
end |
|
286 |
||
21249 | 287 |
|
24164 | 288 |
subsection {* Distributive lattices *} |
21249 | 289 |
|
22454 | 290 |
class distrib_lattice = lattice + |
21249 | 291 |
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
292 |
||
21733 | 293 |
context distrib_lattice |
294 |
begin |
|
295 |
||
296 |
lemma sup_inf_distrib2: |
|
21249 | 297 |
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
32064 | 298 |
by(simp add: inf_sup_aci sup_inf_distrib1) |
21249 | 299 |
|
21733 | 300 |
lemma inf_sup_distrib1: |
21249 | 301 |
"x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
302 |
by(rule distrib_imp2[OF sup_inf_distrib1]) |
|
303 |
||
21733 | 304 |
lemma inf_sup_distrib2: |
21249 | 305 |
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" |
32064 | 306 |
by(simp add: inf_sup_aci inf_sup_distrib1) |
21249 | 307 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
308 |
lemma dual_distrib_lattice: |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
309 |
"distrib_lattice (op \<ge>) (op >) sup inf" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
310 |
by (rule distrib_lattice.intro, rule dual_lattice) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
311 |
(unfold_locales, fact inf_sup_distrib1) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
312 |
|
21733 | 313 |
lemmas distrib = |
21249 | 314 |
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 |
315 |
||
21733 | 316 |
end |
317 |
||
21249 | 318 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
319 |
subsection {* Bounded lattices and boolean algebras *} |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
320 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
321 |
class bounded_lattice = lattice + top + bot |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
322 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
323 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
324 |
lemma dual_bounded_lattice: |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
325 |
"bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
326 |
by (rule bounded_lattice.intro, rule dual_lattice) |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
327 |
(unfold_locales, auto simp add: less_le_not_le) |
31991
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 inf_bot_left [simp]: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
330 |
"\<bottom> \<sqinter> x = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
331 |
by (rule inf_absorb1) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
332 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
333 |
lemma inf_bot_right [simp]: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
334 |
"x \<sqinter> \<bottom> = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
335 |
by (rule inf_absorb2) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
336 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
337 |
lemma sup_top_left [simp]: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
338 |
"\<top> \<squnion> x = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
339 |
by (rule sup_absorb1) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
340 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
341 |
lemma sup_top_right [simp]: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
342 |
"x \<squnion> \<top> = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
343 |
by (rule sup_absorb2) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
344 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
345 |
lemma inf_top_left [simp]: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
346 |
"\<top> \<sqinter> x = x" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
347 |
by (rule inf_absorb2) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
348 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
349 |
lemma inf_top_right [simp]: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
350 |
"x \<sqinter> \<top> = x" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
351 |
by (rule inf_absorb1) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
352 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
353 |
lemma sup_bot_left [simp]: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
354 |
"\<bottom> \<squnion> x = x" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
355 |
by (rule sup_absorb2) simp |
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 sup_bot_right [simp]: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
358 |
"x \<squnion> \<bottom> = x" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
359 |
by (rule sup_absorb1) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
360 |
|
32568 | 361 |
lemma inf_eq_top_eq1: |
362 |
assumes "A \<sqinter> B = \<top>" |
|
363 |
shows "A = \<top>" |
|
364 |
proof (cases "B = \<top>") |
|
365 |
case True with assms show ?thesis by simp |
|
366 |
next |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
367 |
case False with top_greatest have "B \<sqsubset> \<top>" by (auto intro: neq_le_trans) |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
368 |
then have "A \<sqinter> B \<sqsubset> \<top>" by (rule less_infI2) |
32568 | 369 |
with assms show ?thesis by simp |
370 |
qed |
|
371 |
||
372 |
lemma inf_eq_top_eq2: |
|
373 |
assumes "A \<sqinter> B = \<top>" |
|
374 |
shows "B = \<top>" |
|
375 |
by (rule inf_eq_top_eq1, unfold inf_commute [of B]) (fact assms) |
|
376 |
||
377 |
lemma sup_eq_bot_eq1: |
|
378 |
assumes "A \<squnion> B = \<bottom>" |
|
379 |
shows "A = \<bottom>" |
|
380 |
proof - |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
381 |
interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom> |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
382 |
by (rule dual_bounded_lattice) |
32568 | 383 |
from dual.inf_eq_top_eq1 assms show ?thesis . |
384 |
qed |
|
385 |
||
386 |
lemma sup_eq_bot_eq2: |
|
387 |
assumes "A \<squnion> B = \<bottom>" |
|
388 |
shows "B = \<bottom>" |
|
389 |
proof - |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
390 |
interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom> |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
391 |
by (rule dual_bounded_lattice) |
32568 | 392 |
from dual.inf_eq_top_eq2 assms show ?thesis . |
393 |
qed |
|
394 |
||
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
395 |
end |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
396 |
|
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
397 |
class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus + |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
398 |
assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
399 |
and sup_compl_top: "x \<squnion> - x = \<top>" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
400 |
assumes diff_eq: "x - y = x \<sqinter> - y" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
401 |
begin |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
402 |
|
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
403 |
lemma dual_boolean_algebra: |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
404 |
"boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
405 |
by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice) |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
406 |
(unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq) |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
407 |
|
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
408 |
lemma compl_inf_bot: |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
409 |
"- x \<sqinter> x = \<bottom>" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
410 |
by (simp add: inf_commute inf_compl_bot) |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
411 |
|
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
412 |
lemma compl_sup_top: |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
413 |
"- x \<squnion> x = \<top>" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
414 |
by (simp add: sup_commute sup_compl_top) |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
415 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
416 |
lemma compl_unique: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
417 |
assumes "x \<sqinter> y = \<bottom>" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
418 |
and "x \<squnion> y = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
419 |
shows "- x = y" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
420 |
proof - |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
421 |
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
|
422 |
using inf_compl_bot assms(1) by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
423 |
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
|
424 |
by (simp add: inf_commute) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
425 |
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
|
426 |
by (simp add: inf_sup_distrib1) |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
427 |
then have "- x \<sqinter> \<top> = y \<sqinter> \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
428 |
using sup_compl_top assms(2) by simp |
34209 | 429 |
then show "- x = y" by simp |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
430 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
431 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
432 |
lemma double_compl [simp]: |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
433 |
"- (- x) = x" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
434 |
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
|
435 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
436 |
lemma compl_eq_compl_iff [simp]: |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
437 |
"- x = - y \<longleftrightarrow> x = y" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
438 |
proof |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
439 |
assume "- x = - y" |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
440 |
then have "- x \<sqinter> y = \<bottom>" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
441 |
and "- x \<squnion> y = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
442 |
by (simp_all add: compl_inf_bot compl_sup_top) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
443 |
then have "- (- x) = y" by (rule compl_unique) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
444 |
then show "x = y" by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
445 |
next |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
446 |
assume "x = y" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
447 |
then show "- x = - y" by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
448 |
qed |
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 |
lemma compl_bot_eq [simp]: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
451 |
"- \<bottom> = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
452 |
proof - |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
453 |
from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" . |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
454 |
then show ?thesis by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
455 |
qed |
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 |
lemma compl_top_eq [simp]: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
458 |
"- \<top> = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
459 |
proof - |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
460 |
from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" . |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
461 |
then show ?thesis by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
462 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
463 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
464 |
lemma compl_inf [simp]: |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
465 |
"- (x \<sqinter> y) = - x \<squnion> - y" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
466 |
proof (rule compl_unique) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
467 |
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
|
468 |
by (rule inf_sup_distrib1) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
469 |
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
|
470 |
by (simp only: inf_commute inf_assoc inf_left_commute) |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
471 |
finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
472 |
by (simp add: inf_compl_bot) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
473 |
next |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
474 |
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
|
475 |
by (rule sup_inf_distrib2) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
476 |
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
|
477 |
by (simp only: sup_commute sup_assoc sup_left_commute) |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
478 |
finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
479 |
by (simp add: sup_compl_top) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
480 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
481 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
482 |
lemma compl_sup [simp]: |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
483 |
"- (x \<squnion> y) = - x \<sqinter> - y" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
484 |
proof - |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
485 |
interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom> |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
486 |
by (rule dual_boolean_algebra) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
487 |
then show ?thesis by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
488 |
qed |
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 |
end |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
491 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
492 |
|
22454 | 493 |
subsection {* Uniqueness of inf and sup *} |
494 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
495 |
lemma (in semilattice_inf) inf_unique: |
22454 | 496 |
fixes f (infixl "\<triangle>" 70) |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
497 |
assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
498 |
and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" |
22737 | 499 |
shows "x \<sqinter> y = x \<triangle> y" |
22454 | 500 |
proof (rule antisym) |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
501 |
show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2) |
22454 | 502 |
next |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
503 |
have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest) |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
504 |
show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all |
22454 | 505 |
qed |
506 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
507 |
lemma (in semilattice_sup) sup_unique: |
22454 | 508 |
fixes f (infixl "\<nabla>" 70) |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
509 |
assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
510 |
and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x" |
22737 | 511 |
shows "x \<squnion> y = x \<nabla> y" |
22454 | 512 |
proof (rule antisym) |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
513 |
show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2) |
22454 | 514 |
next |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
515 |
have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least) |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
516 |
show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all |
22454 | 517 |
qed |
518 |
||
519 |
||
22916 | 520 |
subsection {* @{const min}/@{const max} on linear orders as |
521 |
special case of @{const inf}/@{const sup} *} |
|
522 |
||
32512 | 523 |
sublocale linorder < min_max!: distrib_lattice less_eq less min max |
28823 | 524 |
proof |
22916 | 525 |
fix x y z |
32512 | 526 |
show "max x (min y z) = min (max x y) (max x z)" |
527 |
by (auto simp add: min_def max_def) |
|
22916 | 528 |
qed (auto simp add: min_def max_def not_le less_imp_le) |
21249 | 529 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
530 |
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset
|
531 |
by (rule ext)+ (auto intro: antisym) |
21733 | 532 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
533 |
lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset
|
534 |
by (rule ext)+ (auto intro: antisym) |
21733 | 535 |
|
21249 | 536 |
lemmas le_maxI1 = min_max.sup_ge1 |
537 |
lemmas le_maxI2 = min_max.sup_ge2 |
|
21381 | 538 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
539 |
lemmas min_ac = min_max.inf_assoc min_max.inf_commute |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
540 |
min_max.inf.left_commute |
21249 | 541 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
542 |
lemmas max_ac = min_max.sup_assoc min_max.sup_commute |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
543 |
min_max.sup.left_commute |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
544 |
|
21249 | 545 |
|
22454 | 546 |
|
547 |
subsection {* Bool as lattice *} |
|
548 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
549 |
instantiation bool :: boolean_algebra |
25510 | 550 |
begin |
551 |
||
552 |
definition |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
553 |
bool_Compl_def: "uminus = Not" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
554 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
555 |
definition |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
556 |
bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
557 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
558 |
definition |
25510 | 559 |
inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" |
560 |
||
561 |
definition |
|
562 |
sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" |
|
563 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
564 |
instance proof |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
565 |
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
|
566 |
bot_bool_eq top_bool_eq bool_Compl_def bool_diff_def, auto) |
22454 | 567 |
|
25510 | 568 |
end |
569 |
||
32781 | 570 |
lemma sup_boolI1: |
571 |
"P \<Longrightarrow> P \<squnion> Q" |
|
572 |
by (simp add: sup_bool_eq) |
|
573 |
||
574 |
lemma sup_boolI2: |
|
575 |
"Q \<Longrightarrow> P \<squnion> Q" |
|
576 |
by (simp add: sup_bool_eq) |
|
577 |
||
578 |
lemma sup_boolE: |
|
579 |
"P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" |
|
580 |
by (auto simp add: sup_bool_eq) |
|
581 |
||
23878 | 582 |
|
583 |
subsection {* Fun as lattice *} |
|
584 |
||
25510 | 585 |
instantiation "fun" :: (type, lattice) lattice |
586 |
begin |
|
587 |
||
588 |
definition |
|
28562 | 589 |
inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" |
25510 | 590 |
|
591 |
definition |
|
28562 | 592 |
sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
25510 | 593 |
|
32780 | 594 |
instance proof |
595 |
qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq) |
|
23878 | 596 |
|
25510 | 597 |
end |
23878 | 598 |
|
599 |
instance "fun" :: (type, distrib_lattice) distrib_lattice |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
600 |
proof |
32780 | 601 |
qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1) |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
602 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
603 |
instance "fun" :: (type, bounded_lattice) bounded_lattice .. |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
604 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
605 |
instantiation "fun" :: (type, uminus) uminus |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
606 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
607 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
608 |
definition |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
609 |
fun_Compl_def: "- A = (\<lambda>x. - A x)" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
610 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
611 |
instance .. |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
612 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
613 |
end |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
614 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
615 |
instantiation "fun" :: (type, minus) minus |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
616 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
617 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
618 |
definition |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
619 |
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
|
620 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
621 |
instance .. |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
622 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
623 |
end |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
624 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
625 |
instance "fun" :: (type, boolean_algebra) boolean_algebra |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
626 |
proof |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
627 |
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
|
628 |
inf_compl_bot sup_compl_top diff_eq) |
23878 | 629 |
|
26794 | 630 |
|
25062 | 631 |
no_notation |
25382 | 632 |
less_eq (infix "\<sqsubseteq>" 50) and |
633 |
less (infix "\<sqsubset>" 50) and |
|
634 |
inf (infixl "\<sqinter>" 70) and |
|
32568 | 635 |
sup (infixl "\<squnion>" 65) and |
636 |
top ("\<top>") and |
|
637 |
bot ("\<bottom>") |
|
25062 | 638 |
|
21249 | 639 |
end |