author | wenzelm |
Tue, 03 Jan 2023 17:21:24 +0100 | |
changeset 76887 | d8cdddf7b9a5 |
parent 76055 | 8d56461f85ec |
child 79099 | 05a753360b25 |
permissions | -rw-r--r-- |
21249 | 1 |
(* Title: HOL/Lattices.thy |
2 |
Author: Tobias Nipkow |
|
3 |
*) |
|
4 |
||
60758 | 5 |
section \<open>Abstract lattices\<close> |
21249 | 6 |
|
7 |
theory Lattices |
|
54555 | 8 |
imports Groups |
21249 | 9 |
begin |
10 |
||
60758 | 11 |
subsection \<open>Abstract semilattice\<close> |
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
12 |
|
60758 | 13 |
text \<open> |
51487 | 14 |
These locales provide a basic structure for interpretation into |
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
15 |
bigger structures; extensions require careful thinking, otherwise |
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
16 |
undesired effects may occur due to interpretation. |
60758 | 17 |
\<close> |
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
18 |
|
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
19 |
locale semilattice = abel_semigroup + |
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
20 |
assumes idem [simp]: "a \<^bold>* a = a" |
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
21 |
begin |
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
22 |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
23 |
lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b" |
63322 | 24 |
by (simp add: assoc [symmetric]) |
50615 | 25 |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
26 |
lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b" |
63322 | 27 |
by (simp add: assoc) |
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
28 |
|
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
29 |
end |
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
30 |
|
51487 | 31 |
locale semilattice_neutr = semilattice + comm_monoid |
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
32 |
|
51487 | 33 |
locale semilattice_order = semilattice + |
63322 | 34 |
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50) |
35 |
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50) |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
36 |
assumes order_iff: "a \<^bold>\<le> b \<longleftrightarrow> a = a \<^bold>* b" |
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
37 |
and strict_order_iff: "a \<^bold>< b \<longleftrightarrow> a = a \<^bold>* b \<and> a \<noteq> b" |
51487 | 38 |
begin |
39 |
||
63322 | 40 |
lemma orderI: "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b" |
51487 | 41 |
by (simp add: order_iff) |
42 |
||
43 |
lemma orderE: |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
44 |
assumes "a \<^bold>\<le> b" |
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
45 |
obtains "a = a \<^bold>* b" |
51487 | 46 |
using assms by (unfold order_iff) |
47 |
||
52152 | 48 |
sublocale ordering less_eq less |
51487 | 49 |
proof |
63322 | 50 |
show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b" for a b |
59545
12a6088ed195
explicit equivalence for strict order on lattices
haftmann
parents:
58889
diff
changeset
|
51 |
by (simp add: order_iff strict_order_iff) |
51487 | 52 |
next |
63588 | 53 |
show "a \<^bold>\<le> a" for a |
51487 | 54 |
by (simp add: order_iff) |
55 |
next |
|
56 |
fix a b |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
57 |
assume "a \<^bold>\<le> b" "b \<^bold>\<le> a" |
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
58 |
then have "a = a \<^bold>* b" "a \<^bold>* b = b" |
51487 | 59 |
by (simp_all add: order_iff commute) |
60 |
then show "a = b" by simp |
|
61 |
next |
|
62 |
fix a b c |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
63 |
assume "a \<^bold>\<le> b" "b \<^bold>\<le> c" |
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
64 |
then have "a = a \<^bold>* b" "b = b \<^bold>* c" |
51487 | 65 |
by (simp_all add: order_iff commute) |
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
66 |
then have "a = a \<^bold>* (b \<^bold>* c)" |
51487 | 67 |
by simp |
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
68 |
then have "a = (a \<^bold>* b) \<^bold>* c" |
51487 | 69 |
by (simp add: assoc) |
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
70 |
with \<open>a = a \<^bold>* b\<close> [symmetric] have "a = a \<^bold>* c" by simp |
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
71 |
then show "a \<^bold>\<le> c" by (rule orderI) |
51487 | 72 |
qed |
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
73 |
|
63322 | 74 |
lemma cobounded1 [simp]: "a \<^bold>* b \<^bold>\<le> a" |
75 |
by (simp add: order_iff commute) |
|
51487 | 76 |
|
63322 | 77 |
lemma cobounded2 [simp]: "a \<^bold>* b \<^bold>\<le> b" |
51487 | 78 |
by (simp add: order_iff) |
79 |
||
80 |
lemma boundedI: |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
81 |
assumes "a \<^bold>\<le> b" and "a \<^bold>\<le> c" |
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
82 |
shows "a \<^bold>\<le> b \<^bold>* c" |
51487 | 83 |
proof (rule orderI) |
63588 | 84 |
from assms obtain "a \<^bold>* b = a" and "a \<^bold>* c = a" |
85 |
by (auto elim!: orderE) |
|
86 |
then show "a = a \<^bold>* (b \<^bold>* c)" |
|
87 |
by (simp add: assoc [symmetric]) |
|
51487 | 88 |
qed |
89 |
||
90 |
lemma boundedE: |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
91 |
assumes "a \<^bold>\<le> b \<^bold>* c" |
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
92 |
obtains "a \<^bold>\<le> b" and "a \<^bold>\<le> c" |
51487 | 93 |
using assms by (blast intro: trans cobounded1 cobounded2) |
94 |
||
63322 | 95 |
lemma bounded_iff [simp]: "a \<^bold>\<le> b \<^bold>* c \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<^bold>\<le> c" |
51487 | 96 |
by (blast intro: boundedI elim: boundedE) |
97 |
||
98 |
lemma strict_boundedE: |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
99 |
assumes "a \<^bold>< b \<^bold>* c" |
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
100 |
obtains "a \<^bold>< b" and "a \<^bold>< c" |
54859 | 101 |
using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+ |
51487 | 102 |
|
63322 | 103 |
lemma coboundedI1: "a \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c" |
51487 | 104 |
by (rule trans) auto |
105 |
||
63322 | 106 |
lemma coboundedI2: "b \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c" |
51487 | 107 |
by (rule trans) auto |
108 |
||
63322 | 109 |
lemma strict_coboundedI1: "a \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c" |
54858 | 110 |
using irrefl |
63588 | 111 |
by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order |
112 |
elim: strict_boundedE) |
|
54858 | 113 |
|
63322 | 114 |
lemma strict_coboundedI2: "b \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c" |
54858 | 115 |
using strict_coboundedI1 [of b c a] by (simp add: commute) |
116 |
||
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
117 |
lemma mono: "a \<^bold>\<le> c \<Longrightarrow> b \<^bold>\<le> d \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c \<^bold>* d" |
51487 | 118 |
by (blast intro: boundedI coboundedI1 coboundedI2) |
119 |
||
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
120 |
lemma absorb1: "a \<^bold>\<le> b \<Longrightarrow> a \<^bold>* b = a" |
63588 | 121 |
by (rule antisym) (auto simp: refl) |
51487 | 122 |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
123 |
lemma absorb2: "b \<^bold>\<le> a \<Longrightarrow> a \<^bold>* b = b" |
63588 | 124 |
by (rule antisym) (auto simp: refl) |
54858 | 125 |
|
73869 | 126 |
lemma absorb3: "a \<^bold>< b \<Longrightarrow> a \<^bold>* b = a" |
127 |
by (rule absorb1) (rule strict_implies_order) |
|
128 |
||
129 |
lemma absorb4: "b \<^bold>< a \<Longrightarrow> a \<^bold>* b = b" |
|
130 |
by (rule absorb2) (rule strict_implies_order) |
|
131 |
||
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
132 |
lemma absorb_iff1: "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>* b = a" |
54858 | 133 |
using order_iff by auto |
134 |
||
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
135 |
lemma absorb_iff2: "b \<^bold>\<le> a \<longleftrightarrow> a \<^bold>* b = b" |
54858 | 136 |
using order_iff by (auto simp add: commute) |
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
137 |
|
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
138 |
end |
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
139 |
|
51487 | 140 |
locale semilattice_neutr_order = semilattice_neutr + semilattice_order |
52152 | 141 |
begin |
51487 | 142 |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
143 |
sublocale ordering_top less_eq less "\<^bold>1" |
61169 | 144 |
by standard (simp add: order_iff) |
51487 | 145 |
|
71851 | 146 |
lemma eq_neutr_iff [simp]: \<open>a \<^bold>* b = \<^bold>1 \<longleftrightarrow> a = \<^bold>1 \<and> b = \<^bold>1\<close> |
147 |
by (simp add: eq_iff) |
|
148 |
||
149 |
lemma neutr_eq_iff [simp]: \<open>\<^bold>1 = a \<^bold>* b \<longleftrightarrow> a = \<^bold>1 \<and> b = \<^bold>1\<close> |
|
150 |
by (simp add: eq_iff) |
|
151 |
||
52152 | 152 |
end |
153 |
||
71938 | 154 |
text \<open>Interpretations for boolean operators\<close> |
63661
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
155 |
|
71938 | 156 |
interpretation conj: semilattice_neutr \<open>(\<and>)\<close> True |
63661
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
157 |
by standard auto |
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
158 |
|
71938 | 159 |
interpretation disj: semilattice_neutr \<open>(\<or>)\<close> False |
63661
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
160 |
by standard auto |
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
161 |
|
71938 | 162 |
declare conj_assoc [ac_simps del] disj_assoc [ac_simps del] \<comment> \<open>already simp by default\<close> |
163 |
||
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
164 |
|
60758 | 165 |
subsection \<open>Syntactic infimum and supremum operations\<close> |
41082 | 166 |
|
44845 | 167 |
class inf = |
168 |
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
|
25206 | 169 |
|
63322 | 170 |
class sup = |
44845 | 171 |
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
172 |
||
46691 | 173 |
|
60758 | 174 |
subsection \<open>Concrete lattices\<close> |
46691 | 175 |
|
71013 | 176 |
class semilattice_inf = order + inf + |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
177 |
assumes inf_le1 [simp]: "x \<sqinter> y \<le> x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
178 |
and inf_le2 [simp]: "x \<sqinter> y \<le> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
179 |
and inf_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z" |
21249 | 180 |
|
44845 | 181 |
class semilattice_sup = order + sup + |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
182 |
assumes sup_ge1 [simp]: "x \<le> x \<squnion> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
183 |
and sup_ge2 [simp]: "y \<le> x \<squnion> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
184 |
and sup_least: "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x" |
26014 | 185 |
begin |
186 |
||
63588 | 187 |
text \<open>Dual lattice.\<close> |
63322 | 188 |
lemma dual_semilattice: "class.semilattice_inf sup greater_eq greater" |
189 |
by (rule class.semilattice_inf.intro, rule dual_order) |
|
190 |
(unfold_locales, simp_all add: sup_least) |
|
26014 | 191 |
|
192 |
end |
|
21249 | 193 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
194 |
class lattice = semilattice_inf + semilattice_sup |
21249 | 195 |
|
25382 | 196 |
|
60758 | 197 |
subsubsection \<open>Intro and elim rules\<close> |
21733 | 198 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
199 |
context semilattice_inf |
21733 | 200 |
begin |
21249 | 201 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
202 |
lemma le_infI1: "a \<le> x \<Longrightarrow> a \<sqinter> b \<le> x" |
32064 | 203 |
by (rule order_trans) auto |
21249 | 204 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
205 |
lemma le_infI2: "b \<le> x \<Longrightarrow> a \<sqinter> b \<le> x" |
32064 | 206 |
by (rule order_trans) auto |
21733 | 207 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
208 |
lemma le_infI: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> a \<sqinter> b" |
54857 | 209 |
by (fact inf_greatest) (* FIXME: duplicate lemma *) |
21249 | 210 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
211 |
lemma le_infE: "x \<le> a \<sqinter> b \<Longrightarrow> (x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> P) \<Longrightarrow> P" |
36008 | 212 |
by (blast intro: order_trans inf_le1 inf_le2) |
21249 | 213 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
214 |
lemma le_inf_iff: "x \<le> y \<sqinter> z \<longleftrightarrow> x \<le> y \<and> x \<le> z" |
32064 | 215 |
by (blast intro: le_infI elim: le_infE) |
21733 | 216 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
217 |
lemma le_iff_inf: "x \<le> y \<longleftrightarrow> x \<sqinter> y = x" |
73411 | 218 |
by (auto intro: le_infI1 order.antisym dest: order.eq_iff [THEN iffD1] simp add: le_inf_iff) |
21249 | 219 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
220 |
lemma inf_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<le> c \<sqinter> d" |
36008 | 221 |
by (fast intro: inf_greatest le_infI1 le_infI2) |
222 |
||
25206 | 223 |
end |
21733 | 224 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
225 |
context semilattice_sup |
21733 | 226 |
begin |
21249 | 227 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
228 |
lemma le_supI1: "x \<le> a \<Longrightarrow> x \<le> a \<squnion> b" |
63322 | 229 |
by (rule order_trans) auto |
230 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
231 |
lemma le_supI2: "x \<le> b \<Longrightarrow> x \<le> a \<squnion> b" |
25062 | 232 |
by (rule order_trans) auto |
21249 | 233 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
234 |
lemma le_supI: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> a \<squnion> b \<le> x" |
54857 | 235 |
by (fact sup_least) (* FIXME: duplicate lemma *) |
21249 | 236 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
237 |
lemma le_supE: "a \<squnion> b \<le> x \<Longrightarrow> (a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> P) \<Longrightarrow> P" |
36008 | 238 |
by (blast intro: order_trans sup_ge1 sup_ge2) |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
239 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
240 |
lemma le_sup_iff: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z" |
32064 | 241 |
by (blast intro: le_supI elim: le_supE) |
21733 | 242 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
243 |
lemma le_iff_sup: "x \<le> y \<longleftrightarrow> x \<squnion> y = y" |
73411 | 244 |
by (auto intro: le_supI2 order.antisym dest: order.eq_iff [THEN iffD1] simp add: le_sup_iff) |
21734 | 245 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
246 |
lemma sup_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<le> c \<squnion> d" |
36008 | 247 |
by (fast intro: sup_least le_supI1 le_supI2) |
248 |
||
25206 | 249 |
end |
23878 | 250 |
|
21733 | 251 |
|
60758 | 252 |
subsubsection \<open>Equational laws\<close> |
21249 | 253 |
|
52152 | 254 |
context semilattice_inf |
255 |
begin |
|
256 |
||
61605 | 257 |
sublocale inf: semilattice inf |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
258 |
proof |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
259 |
fix a b c |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
260 |
show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" |
73411 | 261 |
by (rule order.antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff) |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
262 |
show "a \<sqinter> b = b \<sqinter> a" |
73411 | 263 |
by (rule order.antisym) (auto simp add: le_inf_iff) |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
264 |
show "a \<sqinter> a = a" |
73411 | 265 |
by (rule order.antisym) (auto simp add: le_inf_iff) |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
266 |
qed |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
267 |
|
61605 | 268 |
sublocale inf: semilattice_order inf less_eq less |
61169 | 269 |
by standard (auto simp add: le_iff_inf less_le) |
51487 | 270 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
271 |
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
|
272 |
by (fact inf.assoc) |
21733 | 273 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
274 |
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
|
275 |
by (fact inf.commute) |
21733 | 276 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
277 |
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
|
278 |
by (fact inf.left_commute) |
21733 | 279 |
|
44921 | 280 |
lemma inf_idem: "x \<sqinter> x = x" |
281 |
by (fact inf.idem) (* already simp *) |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
282 |
|
50615 | 283 |
lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
284 |
by (fact inf.left_idem) (* already simp *) |
|
285 |
||
286 |
lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y" |
|
287 |
by (fact inf.right_idem) (* already simp *) |
|
21733 | 288 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
289 |
lemma inf_absorb1: "x \<le> y \<Longrightarrow> x \<sqinter> y = x" |
73411 | 290 |
by (rule order.antisym) auto |
21733 | 291 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
292 |
lemma inf_absorb2: "y \<le> x \<Longrightarrow> x \<sqinter> y = y" |
73411 | 293 |
by (rule order.antisym) auto |
63322 | 294 |
|
32064 | 295 |
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem |
21733 | 296 |
|
297 |
end |
|
298 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
299 |
context semilattice_sup |
21733 | 300 |
begin |
21249 | 301 |
|
61605 | 302 |
sublocale sup: semilattice sup |
52152 | 303 |
proof |
304 |
fix a b c |
|
305 |
show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" |
|
73411 | 306 |
by (rule order.antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff) |
52152 | 307 |
show "a \<squnion> b = b \<squnion> a" |
73411 | 308 |
by (rule order.antisym) (auto simp add: le_sup_iff) |
52152 | 309 |
show "a \<squnion> a = a" |
73411 | 310 |
by (rule order.antisym) (auto simp add: le_sup_iff) |
52152 | 311 |
qed |
312 |
||
61605 | 313 |
sublocale sup: semilattice_order sup greater_eq greater |
61169 | 314 |
by standard (auto simp add: le_iff_sup sup.commute less_le) |
52152 | 315 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
316 |
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
|
317 |
by (fact sup.assoc) |
21733 | 318 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
319 |
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
|
320 |
by (fact sup.commute) |
21733 | 321 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
322 |
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
|
323 |
by (fact sup.left_commute) |
21733 | 324 |
|
44921 | 325 |
lemma sup_idem: "x \<squnion> x = x" |
326 |
by (fact sup.idem) (* already simp *) |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
327 |
|
44918 | 328 |
lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
329 |
by (fact sup.left_idem) |
21733 | 330 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
331 |
lemma sup_absorb1: "y \<le> x \<Longrightarrow> x \<squnion> y = x" |
73411 | 332 |
by (rule order.antisym) auto |
21733 | 333 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
334 |
lemma sup_absorb2: "x \<le> y \<Longrightarrow> x \<squnion> y = y" |
73411 | 335 |
by (rule order.antisym) auto |
21249 | 336 |
|
32064 | 337 |
lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem |
21733 | 338 |
|
339 |
end |
|
21249 | 340 |
|
21733 | 341 |
context lattice |
342 |
begin |
|
343 |
||
67399 | 344 |
lemma dual_lattice: "class.lattice sup (\<ge>) (>) inf" |
63588 | 345 |
by (rule class.lattice.intro, |
346 |
rule dual_semilattice, |
|
347 |
rule class.semilattice_sup.intro, |
|
348 |
rule dual_order) |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
349 |
(unfold_locales, auto) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
350 |
|
44918 | 351 |
lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x" |
73411 | 352 |
by (blast intro: order.antisym inf_le1 inf_greatest sup_ge1) |
21733 | 353 |
|
44918 | 354 |
lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x" |
73411 | 355 |
by (blast intro: order.antisym sup_ge1 sup_least inf_le1) |
21733 | 356 |
|
32064 | 357 |
lemmas inf_sup_aci = inf_aci sup_aci |
21734 | 358 |
|
22454 | 359 |
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 |
360 |
||
63588 | 361 |
text \<open>Towards distributivity.\<close> |
21249 | 362 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
363 |
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<le> (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
32064 | 364 |
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
21734 | 365 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
366 |
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<le> x \<sqinter> (y \<squnion> z)" |
32064 | 367 |
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
21734 | 368 |
|
63322 | 369 |
text \<open>If you have one of them, you have them all.\<close> |
21249 | 370 |
|
21733 | 371 |
lemma distrib_imp1: |
63322 | 372 |
assumes distrib: "\<And>x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
373 |
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
|
21249 | 374 |
proof- |
63322 | 375 |
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" |
376 |
by simp |
|
44918 | 377 |
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" |
63322 | 378 |
by (simp add: distrib inf_commute sup_assoc del: sup_inf_absorb) |
21249 | 379 |
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" |
63322 | 380 |
by (simp add: inf_commute) |
381 |
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:distrib) |
|
21249 | 382 |
finally show ?thesis . |
383 |
qed |
|
384 |
||
21733 | 385 |
lemma distrib_imp2: |
63322 | 386 |
assumes distrib: "\<And>x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
387 |
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
|
21249 | 388 |
proof- |
63322 | 389 |
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" |
390 |
by simp |
|
44918 | 391 |
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" |
63322 | 392 |
by (simp add: distrib sup_commute inf_assoc del: inf_sup_absorb) |
21249 | 393 |
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" |
63322 | 394 |
by (simp add: sup_commute) |
395 |
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by (simp add:distrib) |
|
21249 | 396 |
finally show ?thesis . |
397 |
qed |
|
398 |
||
21733 | 399 |
end |
21249 | 400 |
|
63322 | 401 |
|
60758 | 402 |
subsubsection \<open>Strict order\<close> |
32568 | 403 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
404 |
context semilattice_inf |
32568 | 405 |
begin |
406 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
407 |
lemma less_infI1: "a < x \<Longrightarrow> a \<sqinter> b < 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
|
408 |
by (auto simp add: less_le inf_absorb1 intro: le_infI1) |
32568 | 409 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
410 |
lemma less_infI2: "b < x \<Longrightarrow> a \<sqinter> b < 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
|
411 |
by (auto simp add: less_le inf_absorb2 intro: le_infI2) |
32568 | 412 |
|
413 |
end |
|
414 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
415 |
context semilattice_sup |
32568 | 416 |
begin |
417 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
418 |
lemma less_supI1: "x < a \<Longrightarrow> x < a \<squnion> b" |
44921 | 419 |
using dual_semilattice |
420 |
by (rule semilattice_inf.less_infI1) |
|
32568 | 421 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
422 |
lemma less_supI2: "x < b \<Longrightarrow> x < a \<squnion> b" |
44921 | 423 |
using dual_semilattice |
424 |
by (rule semilattice_inf.less_infI2) |
|
32568 | 425 |
|
426 |
end |
|
427 |
||
21249 | 428 |
|
60758 | 429 |
subsection \<open>Distributive lattices\<close> |
21249 | 430 |
|
22454 | 431 |
class distrib_lattice = lattice + |
21249 | 432 |
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
433 |
||
21733 | 434 |
context distrib_lattice |
435 |
begin |
|
436 |
||
63322 | 437 |
lemma sup_inf_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
44921 | 438 |
by (simp add: sup_commute sup_inf_distrib1) |
21249 | 439 |
|
63322 | 440 |
lemma inf_sup_distrib1: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
44921 | 441 |
by (rule distrib_imp2 [OF sup_inf_distrib1]) |
21249 | 442 |
|
63322 | 443 |
lemma inf_sup_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" |
44921 | 444 |
by (simp add: inf_commute inf_sup_distrib1) |
21249 | 445 |
|
67399 | 446 |
lemma dual_distrib_lattice: "class.distrib_lattice sup (\<ge>) (>) inf" |
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset
|
447 |
by (rule class.distrib_lattice.intro, rule dual_lattice) |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
448 |
(unfold_locales, fact inf_sup_distrib1) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
449 |
|
63322 | 450 |
lemmas sup_inf_distrib = sup_inf_distrib1 sup_inf_distrib2 |
36008 | 451 |
|
63322 | 452 |
lemmas inf_sup_distrib = inf_sup_distrib1 inf_sup_distrib2 |
36008 | 453 |
|
63322 | 454 |
lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 |
21249 | 455 |
|
21733 | 456 |
end |
457 |
||
21249 | 458 |
|
74123
7c5842b06114
clarified abstract and concrete boolean algebras
haftmann
parents:
73869
diff
changeset
|
459 |
subsection \<open>Bounded lattices\<close> |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
460 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
461 |
class bounded_semilattice_inf_top = semilattice_inf + order_top |
52152 | 462 |
begin |
51487 | 463 |
|
61605 | 464 |
sublocale inf_top: semilattice_neutr inf top |
465 |
+ inf_top: semilattice_neutr_order inf top less_eq less |
|
51487 | 466 |
proof |
63322 | 467 |
show "x \<sqinter> \<top> = x" for x |
51487 | 468 |
by (rule inf_absorb1) simp |
469 |
qed |
|
470 |
||
71851 | 471 |
lemma inf_top_left: "\<top> \<sqinter> x = x" |
472 |
by (fact inf_top.left_neutral) |
|
473 |
||
474 |
lemma inf_top_right: "x \<sqinter> \<top> = x" |
|
475 |
by (fact inf_top.right_neutral) |
|
476 |
||
477 |
lemma inf_eq_top_iff: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>" |
|
478 |
by (fact inf_top.eq_neutr_iff) |
|
479 |
||
480 |
lemma top_eq_inf_iff: "\<top> = x \<sqinter> y \<longleftrightarrow> x = \<top> \<and> y = \<top>" |
|
481 |
by (fact inf_top.neutr_eq_iff) |
|
482 |
||
52152 | 483 |
end |
51487 | 484 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
485 |
class bounded_semilattice_sup_bot = semilattice_sup + order_bot |
52152 | 486 |
begin |
487 |
||
61605 | 488 |
sublocale sup_bot: semilattice_neutr sup bot |
489 |
+ sup_bot: semilattice_neutr_order sup bot greater_eq greater |
|
51487 | 490 |
proof |
63322 | 491 |
show "x \<squnion> \<bottom> = x" for x |
51487 | 492 |
by (rule sup_absorb1) simp |
493 |
qed |
|
494 |
||
71851 | 495 |
lemma sup_bot_left: "\<bottom> \<squnion> x = x" |
496 |
by (fact sup_bot.left_neutral) |
|
497 |
||
498 |
lemma sup_bot_right: "x \<squnion> \<bottom> = x" |
|
499 |
by (fact sup_bot.right_neutral) |
|
500 |
||
501 |
lemma sup_eq_bot_iff: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
|
502 |
by (fact sup_bot.eq_neutr_iff) |
|
503 |
||
504 |
lemma bot_eq_sup_iff: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
|
505 |
by (fact sup_bot.neutr_eq_iff) |
|
506 |
||
52152 | 507 |
end |
508 |
||
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
509 |
class bounded_lattice_bot = lattice + order_bot |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
510 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
511 |
|
51487 | 512 |
subclass bounded_semilattice_sup_bot .. |
513 |
||
63322 | 514 |
lemma inf_bot_left [simp]: "\<bottom> \<sqinter> x = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
515 |
by (rule inf_absorb1) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
516 |
|
63322 | 517 |
lemma inf_bot_right [simp]: "x \<sqinter> \<bottom> = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
518 |
by (rule inf_absorb2) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
519 |
|
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
520 |
end |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
521 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
522 |
class bounded_lattice_top = lattice + order_top |
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
523 |
begin |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
524 |
|
51487 | 525 |
subclass bounded_semilattice_inf_top .. |
526 |
||
63322 | 527 |
lemma sup_top_left [simp]: "\<top> \<squnion> x = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
528 |
by (rule sup_absorb1) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
529 |
|
63322 | 530 |
lemma sup_top_right [simp]: "x \<squnion> \<top> = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
531 |
by (rule sup_absorb2) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
532 |
|
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
533 |
end |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
534 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
535 |
class bounded_lattice = lattice + order_bot + order_top |
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
536 |
begin |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
537 |
|
51487 | 538 |
subclass bounded_lattice_bot .. |
539 |
subclass bounded_lattice_top .. |
|
540 |
||
63322 | 541 |
lemma dual_bounded_lattice: "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>" |
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
542 |
by unfold_locales (auto simp add: less_le_not_le) |
32568 | 543 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
544 |
end |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
545 |
|
63322 | 546 |
|
61799 | 547 |
subsection \<open>\<open>min/max\<close> as special case of lattice\<close> |
51540
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset
|
548 |
|
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
549 |
context linorder |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
550 |
begin |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
551 |
|
61605 | 552 |
sublocale min: semilattice_order min less_eq less |
553 |
+ max: semilattice_order max greater_eq greater |
|
61169 | 554 |
by standard (auto simp add: min_def max_def) |
51540
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset
|
555 |
|
73869 | 556 |
declare min.absorb1 [simp] min.absorb2 [simp] |
557 |
min.absorb3 [simp] min.absorb4 [simp] |
|
558 |
max.absorb1 [simp] max.absorb2 [simp] |
|
559 |
max.absorb3 [simp] max.absorb4 [simp] |
|
560 |
||
63322 | 561 |
lemma min_le_iff_disj: "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" |
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
562 |
unfolding min_def using linear by (auto intro: order_trans) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
563 |
|
63322 | 564 |
lemma le_max_iff_disj: "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y" |
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
565 |
unfolding max_def using linear by (auto intro: order_trans) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
566 |
|
63322 | 567 |
lemma min_less_iff_disj: "min x y < z \<longleftrightarrow> x < z \<or> y < z" |
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
568 |
unfolding min_def le_less using less_linear by (auto intro: less_trans) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
569 |
|
63322 | 570 |
lemma less_max_iff_disj: "z < max x y \<longleftrightarrow> z < x \<or> z < y" |
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
571 |
unfolding max_def le_less using less_linear by (auto intro: less_trans) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
572 |
|
63322 | 573 |
lemma min_less_iff_conj [simp]: "z < min x y \<longleftrightarrow> z < x \<and> z < y" |
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
574 |
unfolding min_def le_less using less_linear by (auto intro: less_trans) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
575 |
|
63322 | 576 |
lemma max_less_iff_conj [simp]: "max x y < z \<longleftrightarrow> x < z \<and> y < z" |
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
577 |
unfolding max_def le_less using less_linear by (auto intro: less_trans) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
578 |
|
63322 | 579 |
lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)" |
54862 | 580 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
581 |
||
63322 | 582 |
lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)" |
54862 | 583 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
584 |
||
63322 | 585 |
lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)" |
54862 | 586 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
587 |
||
63322 | 588 |
lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)" |
54862 | 589 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
590 |
||
591 |
lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2 |
|
592 |
||
63322 | 593 |
lemma split_min [no_atp]: "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)" |
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
594 |
by (simp add: min_def) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
595 |
|
63322 | 596 |
lemma split_max [no_atp]: "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)" |
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
597 |
by (simp add: max_def) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
598 |
|
71138 | 599 |
lemma split_min_lin [no_atp]: |
600 |
\<open>P (min a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P a) \<and> (b < a \<longrightarrow> P b)\<close> |
|
73869 | 601 |
by (cases a b rule: linorder_cases) auto |
71138 | 602 |
|
603 |
lemma split_max_lin [no_atp]: |
|
604 |
\<open>P (max a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P b) \<and> (b < a \<longrightarrow> P a)\<close> |
|
73869 | 605 |
by (cases a b rule: linorder_cases) auto |
71138 | 606 |
|
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
607 |
end |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
608 |
|
61076 | 609 |
lemma inf_min: "inf = (min :: 'a::{semilattice_inf,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
51540
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset
|
610 |
by (auto intro: antisym simp add: min_def fun_eq_iff) |
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset
|
611 |
|
61076 | 612 |
lemma sup_max: "sup = (max :: 'a::{semilattice_sup,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
51540
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset
|
613 |
by (auto intro: antisym simp add: max_def fun_eq_iff) |
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset
|
614 |
|
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset
|
615 |
|
60758 | 616 |
subsection \<open>Uniqueness of inf and sup\<close> |
22454 | 617 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
618 |
lemma (in semilattice_inf) inf_unique: |
63322 | 619 |
fixes f (infixl "\<triangle>" 70) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
620 |
assumes le1: "\<And>x y. x \<triangle> y \<le> x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
621 |
and le2: "\<And>x y. x \<triangle> y \<le> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
622 |
and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" |
22737 | 623 |
shows "x \<sqinter> y = x \<triangle> y" |
73411 | 624 |
proof (rule order.antisym) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
625 |
show "x \<triangle> y \<le> x \<sqinter> y" |
63322 | 626 |
by (rule le_infI) (rule le1, rule le2) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
627 |
have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" |
63322 | 628 |
by (blast intro: greatest) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
629 |
show "x \<sqinter> y \<le> x \<triangle> y" |
63322 | 630 |
by (rule leI) simp_all |
22454 | 631 |
qed |
632 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
633 |
lemma (in semilattice_sup) sup_unique: |
63322 | 634 |
fixes f (infixl "\<nabla>" 70) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
635 |
assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
636 |
and ge2: "\<And>x y. y \<le> x \<nabla> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
637 |
and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x" |
22737 | 638 |
shows "x \<squnion> y = x \<nabla> y" |
73411 | 639 |
proof (rule order.antisym) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
640 |
show "x \<squnion> y \<le> x \<nabla> y" |
63322 | 641 |
by (rule le_supI) (rule ge1, rule ge2) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
642 |
have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" |
63322 | 643 |
by (blast intro: least) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
644 |
show "x \<nabla> y \<le> x \<squnion> y" |
63322 | 645 |
by (rule leI) simp_all |
22454 | 646 |
qed |
36008 | 647 |
|
22454 | 648 |
|
69593 | 649 |
subsection \<open>Lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close> |
23878 | 650 |
|
51387 | 651 |
instantiation "fun" :: (type, semilattice_sup) semilattice_sup |
25510 | 652 |
begin |
653 |
||
63322 | 654 |
definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
41080 | 655 |
|
63322 | 656 |
lemma sup_apply [simp, code]: "(f \<squnion> g) x = f x \<squnion> g x" |
41080 | 657 |
by (simp add: sup_fun_def) |
25510 | 658 |
|
63588 | 659 |
instance |
660 |
by standard (simp_all add: le_fun_def) |
|
23878 | 661 |
|
25510 | 662 |
end |
23878 | 663 |
|
51387 | 664 |
instantiation "fun" :: (type, semilattice_inf) semilattice_inf |
665 |
begin |
|
666 |
||
63322 | 667 |
definition "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" |
51387 | 668 |
|
63322 | 669 |
lemma inf_apply [simp, code]: "(f \<sqinter> g) x = f x \<sqinter> g x" |
51387 | 670 |
by (simp add: inf_fun_def) |
671 |
||
63322 | 672 |
instance by standard (simp_all add: le_fun_def) |
51387 | 673 |
|
674 |
end |
|
675 |
||
676 |
instance "fun" :: (type, lattice) lattice .. |
|
677 |
||
63322 | 678 |
instance "fun" :: (type, distrib_lattice) distrib_lattice |
679 |
by standard (rule ext, simp add: sup_inf_distrib1) |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
680 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
681 |
instance "fun" :: (type, bounded_lattice) bounded_lattice .. |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
682 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
683 |
instantiation "fun" :: (type, uminus) uminus |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
684 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
685 |
|
63322 | 686 |
definition fun_Compl_def: "- A = (\<lambda>x. - A x)" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
687 |
|
63322 | 688 |
lemma uminus_apply [simp, code]: "(- A) x = - (A x)" |
41080 | 689 |
by (simp add: fun_Compl_def) |
690 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
691 |
instance .. |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
692 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
693 |
end |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
694 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
695 |
instantiation "fun" :: (type, minus) minus |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
696 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
697 |
|
63322 | 698 |
definition fun_diff_def: "A - B = (\<lambda>x. A x - B x)" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
699 |
|
63322 | 700 |
lemma minus_apply [simp, code]: "(A - B) x = A x - B x" |
41080 | 701 |
by (simp add: fun_diff_def) |
702 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
703 |
instance .. |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
704 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
705 |
end |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
706 |
|
21249 | 707 |
end |