author | haftmann |
Mon, 02 Aug 2021 10:01:06 +0000 | |
changeset 74101 | d804e93ae9ff |
parent 73869 | 7181130f5872 |
child 74123 | 7c5842b06114 |
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 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
223 |
lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf" |
25206 | 224 |
by (auto simp add: mono_def intro: Lattices.inf_greatest) |
21733 | 225 |
|
25206 | 226 |
end |
21733 | 227 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
228 |
context semilattice_sup |
21733 | 229 |
begin |
21249 | 230 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
231 |
lemma le_supI1: "x \<le> a \<Longrightarrow> x \<le> a \<squnion> b" |
63322 | 232 |
by (rule order_trans) auto |
233 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
234 |
lemma le_supI2: "x \<le> b \<Longrightarrow> x \<le> a \<squnion> b" |
25062 | 235 |
by (rule order_trans) auto |
21249 | 236 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
237 |
lemma le_supI: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> a \<squnion> b \<le> x" |
54857 | 238 |
by (fact sup_least) (* FIXME: duplicate lemma *) |
21249 | 239 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
240 |
lemma le_supE: "a \<squnion> b \<le> x \<Longrightarrow> (a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> P) \<Longrightarrow> P" |
36008 | 241 |
by (blast intro: order_trans sup_ge1 sup_ge2) |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
242 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
243 |
lemma le_sup_iff: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z" |
32064 | 244 |
by (blast intro: le_supI elim: le_supE) |
21733 | 245 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
246 |
lemma le_iff_sup: "x \<le> y \<longleftrightarrow> x \<squnion> y = y" |
73411 | 247 |
by (auto intro: le_supI2 order.antisym dest: order.eq_iff [THEN iffD1] simp add: le_sup_iff) |
21734 | 248 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
249 |
lemma sup_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<le> c \<squnion> d" |
36008 | 250 |
by (fast intro: sup_least le_supI1 le_supI2) |
251 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
252 |
lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup" |
25206 | 253 |
by (auto simp add: mono_def intro: Lattices.sup_least) |
21733 | 254 |
|
25206 | 255 |
end |
23878 | 256 |
|
21733 | 257 |
|
60758 | 258 |
subsubsection \<open>Equational laws\<close> |
21249 | 259 |
|
52152 | 260 |
context semilattice_inf |
261 |
begin |
|
262 |
||
61605 | 263 |
sublocale inf: semilattice inf |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
264 |
proof |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
265 |
fix a b c |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
266 |
show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" |
73411 | 267 |
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
|
268 |
show "a \<sqinter> b = b \<sqinter> a" |
73411 | 269 |
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
|
270 |
show "a \<sqinter> a = a" |
73411 | 271 |
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
|
272 |
qed |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
273 |
|
61605 | 274 |
sublocale inf: semilattice_order inf less_eq less |
61169 | 275 |
by standard (auto simp add: le_iff_inf less_le) |
51487 | 276 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
277 |
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
|
278 |
by (fact inf.assoc) |
21733 | 279 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
280 |
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
|
281 |
by (fact inf.commute) |
21733 | 282 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
283 |
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
|
284 |
by (fact inf.left_commute) |
21733 | 285 |
|
44921 | 286 |
lemma inf_idem: "x \<sqinter> x = x" |
287 |
by (fact inf.idem) (* already simp *) |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
288 |
|
50615 | 289 |
lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
290 |
by (fact inf.left_idem) (* already simp *) |
|
291 |
||
292 |
lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y" |
|
293 |
by (fact inf.right_idem) (* already simp *) |
|
21733 | 294 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
295 |
lemma inf_absorb1: "x \<le> y \<Longrightarrow> x \<sqinter> y = x" |
73411 | 296 |
by (rule order.antisym) auto |
21733 | 297 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
298 |
lemma inf_absorb2: "y \<le> x \<Longrightarrow> x \<sqinter> y = y" |
73411 | 299 |
by (rule order.antisym) auto |
63322 | 300 |
|
32064 | 301 |
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem |
21733 | 302 |
|
303 |
end |
|
304 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
305 |
context semilattice_sup |
21733 | 306 |
begin |
21249 | 307 |
|
61605 | 308 |
sublocale sup: semilattice sup |
52152 | 309 |
proof |
310 |
fix a b c |
|
311 |
show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" |
|
73411 | 312 |
by (rule order.antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff) |
52152 | 313 |
show "a \<squnion> b = b \<squnion> a" |
73411 | 314 |
by (rule order.antisym) (auto simp add: le_sup_iff) |
52152 | 315 |
show "a \<squnion> a = a" |
73411 | 316 |
by (rule order.antisym) (auto simp add: le_sup_iff) |
52152 | 317 |
qed |
318 |
||
61605 | 319 |
sublocale sup: semilattice_order sup greater_eq greater |
61169 | 320 |
by standard (auto simp add: le_iff_sup sup.commute less_le) |
52152 | 321 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
322 |
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
|
323 |
by (fact sup.assoc) |
21733 | 324 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
325 |
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
|
326 |
by (fact sup.commute) |
21733 | 327 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
328 |
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
|
329 |
by (fact sup.left_commute) |
21733 | 330 |
|
44921 | 331 |
lemma sup_idem: "x \<squnion> x = x" |
332 |
by (fact sup.idem) (* already simp *) |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
333 |
|
44918 | 334 |
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
|
335 |
by (fact sup.left_idem) |
21733 | 336 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
337 |
lemma sup_absorb1: "y \<le> x \<Longrightarrow> x \<squnion> y = x" |
73411 | 338 |
by (rule order.antisym) auto |
21733 | 339 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
340 |
lemma sup_absorb2: "x \<le> y \<Longrightarrow> x \<squnion> y = y" |
73411 | 341 |
by (rule order.antisym) auto |
21249 | 342 |
|
32064 | 343 |
lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem |
21733 | 344 |
|
345 |
end |
|
21249 | 346 |
|
21733 | 347 |
context lattice |
348 |
begin |
|
349 |
||
67399 | 350 |
lemma dual_lattice: "class.lattice sup (\<ge>) (>) inf" |
63588 | 351 |
by (rule class.lattice.intro, |
352 |
rule dual_semilattice, |
|
353 |
rule class.semilattice_sup.intro, |
|
354 |
rule dual_order) |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
355 |
(unfold_locales, auto) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
356 |
|
44918 | 357 |
lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x" |
73411 | 358 |
by (blast intro: order.antisym inf_le1 inf_greatest sup_ge1) |
21733 | 359 |
|
44918 | 360 |
lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x" |
73411 | 361 |
by (blast intro: order.antisym sup_ge1 sup_least inf_le1) |
21733 | 362 |
|
32064 | 363 |
lemmas inf_sup_aci = inf_aci sup_aci |
21734 | 364 |
|
22454 | 365 |
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 |
366 |
||
63588 | 367 |
text \<open>Towards distributivity.\<close> |
21249 | 368 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
369 |
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<le> (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
32064 | 370 |
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
21734 | 371 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
372 |
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<le> x \<sqinter> (y \<squnion> z)" |
32064 | 373 |
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
21734 | 374 |
|
63322 | 375 |
text \<open>If you have one of them, you have them all.\<close> |
21249 | 376 |
|
21733 | 377 |
lemma distrib_imp1: |
63322 | 378 |
assumes distrib: "\<And>x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
379 |
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
|
21249 | 380 |
proof- |
63322 | 381 |
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" |
382 |
by simp |
|
44918 | 383 |
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" |
63322 | 384 |
by (simp add: distrib inf_commute sup_assoc del: sup_inf_absorb) |
21249 | 385 |
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" |
63322 | 386 |
by (simp add: inf_commute) |
387 |
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:distrib) |
|
21249 | 388 |
finally show ?thesis . |
389 |
qed |
|
390 |
||
21733 | 391 |
lemma distrib_imp2: |
63322 | 392 |
assumes distrib: "\<And>x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
393 |
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
|
21249 | 394 |
proof- |
63322 | 395 |
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" |
396 |
by simp |
|
44918 | 397 |
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" |
63322 | 398 |
by (simp add: distrib sup_commute inf_assoc del: inf_sup_absorb) |
21249 | 399 |
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" |
63322 | 400 |
by (simp add: sup_commute) |
401 |
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by (simp add:distrib) |
|
21249 | 402 |
finally show ?thesis . |
403 |
qed |
|
404 |
||
21733 | 405 |
end |
21249 | 406 |
|
63322 | 407 |
|
60758 | 408 |
subsubsection \<open>Strict order\<close> |
32568 | 409 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
410 |
context semilattice_inf |
32568 | 411 |
begin |
412 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
413 |
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
|
414 |
by (auto simp add: less_le inf_absorb1 intro: le_infI1) |
32568 | 415 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
416 |
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
|
417 |
by (auto simp add: less_le inf_absorb2 intro: le_infI2) |
32568 | 418 |
|
419 |
end |
|
420 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
421 |
context semilattice_sup |
32568 | 422 |
begin |
423 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
424 |
lemma less_supI1: "x < a \<Longrightarrow> x < a \<squnion> b" |
44921 | 425 |
using dual_semilattice |
426 |
by (rule semilattice_inf.less_infI1) |
|
32568 | 427 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
428 |
lemma less_supI2: "x < b \<Longrightarrow> x < a \<squnion> b" |
44921 | 429 |
using dual_semilattice |
430 |
by (rule semilattice_inf.less_infI2) |
|
32568 | 431 |
|
432 |
end |
|
433 |
||
21249 | 434 |
|
60758 | 435 |
subsection \<open>Distributive lattices\<close> |
21249 | 436 |
|
22454 | 437 |
class distrib_lattice = lattice + |
21249 | 438 |
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
439 |
||
21733 | 440 |
context distrib_lattice |
441 |
begin |
|
442 |
||
63322 | 443 |
lemma sup_inf_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
44921 | 444 |
by (simp add: sup_commute sup_inf_distrib1) |
21249 | 445 |
|
63322 | 446 |
lemma inf_sup_distrib1: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
44921 | 447 |
by (rule distrib_imp2 [OF sup_inf_distrib1]) |
21249 | 448 |
|
63322 | 449 |
lemma inf_sup_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" |
44921 | 450 |
by (simp add: inf_commute inf_sup_distrib1) |
21249 | 451 |
|
67399 | 452 |
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
|
453 |
by (rule class.distrib_lattice.intro, rule dual_lattice) |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
454 |
(unfold_locales, fact inf_sup_distrib1) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
455 |
|
63322 | 456 |
lemmas sup_inf_distrib = sup_inf_distrib1 sup_inf_distrib2 |
36008 | 457 |
|
63322 | 458 |
lemmas inf_sup_distrib = inf_sup_distrib1 inf_sup_distrib2 |
36008 | 459 |
|
63322 | 460 |
lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 |
21249 | 461 |
|
21733 | 462 |
end |
463 |
||
21249 | 464 |
|
60758 | 465 |
subsection \<open>Bounded lattices and boolean algebras\<close> |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
466 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
467 |
class bounded_semilattice_inf_top = semilattice_inf + order_top |
52152 | 468 |
begin |
51487 | 469 |
|
61605 | 470 |
sublocale inf_top: semilattice_neutr inf top |
471 |
+ inf_top: semilattice_neutr_order inf top less_eq less |
|
51487 | 472 |
proof |
63322 | 473 |
show "x \<sqinter> \<top> = x" for x |
51487 | 474 |
by (rule inf_absorb1) simp |
475 |
qed |
|
476 |
||
71851 | 477 |
lemma inf_top_left: "\<top> \<sqinter> x = x" |
478 |
by (fact inf_top.left_neutral) |
|
479 |
||
480 |
lemma inf_top_right: "x \<sqinter> \<top> = x" |
|
481 |
by (fact inf_top.right_neutral) |
|
482 |
||
483 |
lemma inf_eq_top_iff: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>" |
|
484 |
by (fact inf_top.eq_neutr_iff) |
|
485 |
||
486 |
lemma top_eq_inf_iff: "\<top> = x \<sqinter> y \<longleftrightarrow> x = \<top> \<and> y = \<top>" |
|
487 |
by (fact inf_top.neutr_eq_iff) |
|
488 |
||
52152 | 489 |
end |
51487 | 490 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
491 |
class bounded_semilattice_sup_bot = semilattice_sup + order_bot |
52152 | 492 |
begin |
493 |
||
61605 | 494 |
sublocale sup_bot: semilattice_neutr sup bot |
495 |
+ sup_bot: semilattice_neutr_order sup bot greater_eq greater |
|
51487 | 496 |
proof |
63322 | 497 |
show "x \<squnion> \<bottom> = x" for x |
51487 | 498 |
by (rule sup_absorb1) simp |
499 |
qed |
|
500 |
||
71851 | 501 |
lemma sup_bot_left: "\<bottom> \<squnion> x = x" |
502 |
by (fact sup_bot.left_neutral) |
|
503 |
||
504 |
lemma sup_bot_right: "x \<squnion> \<bottom> = x" |
|
505 |
by (fact sup_bot.right_neutral) |
|
506 |
||
507 |
lemma sup_eq_bot_iff: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
|
508 |
by (fact sup_bot.eq_neutr_iff) |
|
509 |
||
510 |
lemma bot_eq_sup_iff: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
|
511 |
by (fact sup_bot.neutr_eq_iff) |
|
512 |
||
52152 | 513 |
end |
514 |
||
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
515 |
class bounded_lattice_bot = lattice + order_bot |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
516 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
517 |
|
51487 | 518 |
subclass bounded_semilattice_sup_bot .. |
519 |
||
63322 | 520 |
lemma inf_bot_left [simp]: "\<bottom> \<sqinter> x = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
521 |
by (rule inf_absorb1) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
522 |
|
63322 | 523 |
lemma inf_bot_right [simp]: "x \<sqinter> \<bottom> = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
524 |
by (rule inf_absorb2) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
525 |
|
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
526 |
end |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
527 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
528 |
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
|
529 |
begin |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
530 |
|
51487 | 531 |
subclass bounded_semilattice_inf_top .. |
532 |
||
63322 | 533 |
lemma sup_top_left [simp]: "\<top> \<squnion> x = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
534 |
by (rule sup_absorb1) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
535 |
|
63322 | 536 |
lemma sup_top_right [simp]: "x \<squnion> \<top> = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
537 |
by (rule sup_absorb2) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
538 |
|
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
539 |
end |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
540 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
541 |
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
|
542 |
begin |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
543 |
|
51487 | 544 |
subclass bounded_lattice_bot .. |
545 |
subclass bounded_lattice_top .. |
|
546 |
||
63322 | 547 |
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
|
548 |
by unfold_locales (auto simp add: less_le_not_le) |
32568 | 549 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
550 |
end |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
551 |
|
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
552 |
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
|
553 |
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
|
554 |
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
|
555 |
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
|
556 |
begin |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
557 |
|
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
558 |
lemma dual_boolean_algebra: |
44845 | 559 |
"class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>" |
63588 | 560 |
by (rule class.boolean_algebra.intro, |
561 |
rule dual_bounded_lattice, |
|
562 |
rule dual_distrib_lattice) |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
563 |
(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
|
564 |
|
63322 | 565 |
lemma compl_inf_bot [simp]: "- x \<sqinter> x = \<bottom>" |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
566 |
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
|
567 |
|
63322 | 568 |
lemma compl_sup_top [simp]: "- x \<squnion> x = \<top>" |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
569 |
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
|
570 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
571 |
lemma compl_unique: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
572 |
assumes "x \<sqinter> y = \<bottom>" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
573 |
and "x \<squnion> y = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
574 |
shows "- x = y" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
575 |
proof - |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
576 |
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
|
577 |
using inf_compl_bot assms(1) by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
578 |
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
|
579 |
by (simp add: inf_commute) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
580 |
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
|
581 |
by (simp add: inf_sup_distrib1) |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
582 |
then have "- x \<sqinter> \<top> = y \<sqinter> \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
583 |
using sup_compl_top assms(2) by simp |
34209 | 584 |
then show "- x = y" by simp |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
585 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
586 |
|
63322 | 587 |
lemma double_compl [simp]: "- (- x) = x" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
588 |
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
|
589 |
|
63322 | 590 |
lemma compl_eq_compl_iff [simp]: "- x = - y \<longleftrightarrow> x = y" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
591 |
proof |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
592 |
assume "- x = - y" |
36008 | 593 |
then have "- (- x) = - (- y)" by (rule arg_cong) |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
594 |
then show "x = y" by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
595 |
next |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
596 |
assume "x = y" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
597 |
then show "- x = - y" by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
598 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
599 |
|
63322 | 600 |
lemma compl_bot_eq [simp]: "- \<bottom> = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
601 |
proof - |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
602 |
from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" . |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
603 |
then show ?thesis by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
604 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
605 |
|
63322 | 606 |
lemma compl_top_eq [simp]: "- \<top> = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
607 |
proof - |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
608 |
from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" . |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
609 |
then show ?thesis by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
610 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
611 |
|
63322 | 612 |
lemma compl_inf [simp]: "- (x \<sqinter> y) = - x \<squnion> - y" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
613 |
proof (rule compl_unique) |
36008 | 614 |
have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))" |
615 |
by (simp only: inf_sup_distrib inf_aci) |
|
616 |
then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>" |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
617 |
by (simp add: inf_compl_bot) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
618 |
next |
36008 | 619 |
have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))" |
620 |
by (simp only: sup_inf_distrib sup_aci) |
|
621 |
then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>" |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
622 |
by (simp add: sup_compl_top) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
623 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
624 |
|
63322 | 625 |
lemma compl_sup [simp]: "- (x \<squnion> y) = - x \<sqinter> - y" |
44921 | 626 |
using dual_boolean_algebra |
627 |
by (rule boolean_algebra.compl_inf) |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
628 |
|
36008 | 629 |
lemma compl_mono: |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
630 |
assumes "x \<le> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
631 |
shows "- y \<le> - x" |
36008 | 632 |
proof - |
63322 | 633 |
from assms have "x \<squnion> y = y" by (simp only: le_iff_sup) |
36008 | 634 |
then have "- (x \<squnion> y) = - y" by simp |
635 |
then have "- x \<sqinter> - y = - y" by simp |
|
636 |
then have "- y \<sqinter> - x = - y" by (simp only: inf_commute) |
|
63322 | 637 |
then show ?thesis by (simp only: le_iff_inf) |
36008 | 638 |
qed |
639 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
640 |
lemma compl_le_compl_iff [simp]: "- x \<le> - y \<longleftrightarrow> y \<le> x" |
43873 | 641 |
by (auto dest: compl_mono) |
642 |
||
643 |
lemma compl_le_swap1: |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
644 |
assumes "y \<le> - x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
645 |
shows "x \<le> -y" |
43873 | 646 |
proof - |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
647 |
from assms have "- (- x) \<le> - y" by (simp only: compl_le_compl_iff) |
43873 | 648 |
then show ?thesis by simp |
649 |
qed |
|
650 |
||
651 |
lemma compl_le_swap2: |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
652 |
assumes "- y \<le> x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
653 |
shows "- x \<le> y" |
43873 | 654 |
proof - |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
655 |
from assms have "- x \<le> - (- y)" by (simp only: compl_le_compl_iff) |
43873 | 656 |
then show ?thesis by simp |
657 |
qed |
|
658 |
||
73869 | 659 |
lemma compl_less_compl_iff [simp]: "- x < - y \<longleftrightarrow> y < x" |
44919 | 660 |
by (auto simp add: less_le) |
43873 | 661 |
|
662 |
lemma compl_less_swap1: |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
663 |
assumes "y < - x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
664 |
shows "x < - y" |
43873 | 665 |
proof - |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
666 |
from assms have "- (- x) < - y" by (simp only: compl_less_compl_iff) |
43873 | 667 |
then show ?thesis by simp |
668 |
qed |
|
669 |
||
670 |
lemma compl_less_swap2: |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
671 |
assumes "- y < x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
672 |
shows "- x < y" |
43873 | 673 |
proof - |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
674 |
from assms have "- x < - (- y)" |
63588 | 675 |
by (simp only: compl_less_compl_iff) |
43873 | 676 |
then show ?thesis by simp |
677 |
qed |
|
36008 | 678 |
|
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
679 |
lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top" |
73869 | 680 |
by (simp add: ac_simps sup_compl_top) |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
681 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
682 |
lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top" |
73869 | 683 |
by (simp add: ac_simps sup_compl_top) |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
684 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
685 |
lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot" |
73869 | 686 |
by (simp add: ac_simps inf_compl_bot) |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
687 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
688 |
lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot" |
73869 | 689 |
by (simp add: ac_simps inf_compl_bot) |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
690 |
|
63588 | 691 |
declare inf_compl_bot [simp] |
692 |
and sup_compl_top [simp] |
|
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
693 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
694 |
lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top" |
63322 | 695 |
by (simp add: sup_assoc[symmetric]) |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
696 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
697 |
lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top" |
63322 | 698 |
using sup_compl_top_left1[of "- x" y] by simp |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
699 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
700 |
lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot" |
63322 | 701 |
by (simp add: inf_assoc[symmetric]) |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
702 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
703 |
lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot" |
63322 | 704 |
using inf_compl_bot_left1[of "- x" y] by simp |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
705 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
706 |
lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot" |
63322 | 707 |
by (subst inf_left_commute) simp |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
708 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
709 |
end |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
710 |
|
70490 | 711 |
locale boolean_algebra_cancel |
712 |
begin |
|
713 |
||
714 |
lemma sup1: "(A::'a::semilattice_sup) \<equiv> sup k a \<Longrightarrow> sup A b \<equiv> sup k (sup a b)" |
|
715 |
by (simp only: ac_simps) |
|
716 |
||
717 |
lemma sup2: "(B::'a::semilattice_sup) \<equiv> sup k b \<Longrightarrow> sup a B \<equiv> sup k (sup a b)" |
|
718 |
by (simp only: ac_simps) |
|
719 |
||
720 |
lemma sup0: "(a::'a::bounded_semilattice_sup_bot) \<equiv> sup a bot" |
|
721 |
by simp |
|
722 |
||
723 |
lemma inf1: "(A::'a::semilattice_inf) \<equiv> inf k a \<Longrightarrow> inf A b \<equiv> inf k (inf a b)" |
|
724 |
by (simp only: ac_simps) |
|
725 |
||
726 |
lemma inf2: "(B::'a::semilattice_inf) \<equiv> inf k b \<Longrightarrow> inf a B \<equiv> inf k (inf a b)" |
|
727 |
by (simp only: ac_simps) |
|
728 |
||
729 |
lemma inf0: "(a::'a::bounded_semilattice_inf_top) \<equiv> inf a top" |
|
730 |
by simp |
|
731 |
||
732 |
end |
|
733 |
||
69605 | 734 |
ML_file \<open>Tools/boolean_algebra_cancel.ML\<close> |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
735 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
736 |
simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") = |
61799 | 737 |
\<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close> |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
738 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
739 |
simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") = |
61799 | 740 |
\<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close> |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
741 |
|
63322 | 742 |
|
61799 | 743 |
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
|
744 |
|
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
745 |
context linorder |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
746 |
begin |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
747 |
|
61605 | 748 |
sublocale min: semilattice_order min less_eq less |
749 |
+ max: semilattice_order max greater_eq greater |
|
61169 | 750 |
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
|
751 |
|
73869 | 752 |
declare min.absorb1 [simp] min.absorb2 [simp] |
753 |
min.absorb3 [simp] min.absorb4 [simp] |
|
754 |
max.absorb1 [simp] max.absorb2 [simp] |
|
755 |
max.absorb3 [simp] max.absorb4 [simp] |
|
756 |
||
63322 | 757 |
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
|
758 |
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
|
759 |
|
63322 | 760 |
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
|
761 |
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
|
762 |
|
63322 | 763 |
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
|
764 |
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
|
765 |
|
63322 | 766 |
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
|
767 |
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
|
768 |
|
63322 | 769 |
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
|
770 |
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
|
771 |
|
63322 | 772 |
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
|
773 |
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
|
774 |
|
63322 | 775 |
lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)" |
54862 | 776 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
777 |
||
63322 | 778 |
lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)" |
54862 | 779 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
780 |
||
63322 | 781 |
lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)" |
54862 | 782 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
783 |
||
63322 | 784 |
lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)" |
54862 | 785 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
786 |
||
787 |
lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2 |
|
788 |
||
63322 | 789 |
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
|
790 |
by (simp add: min_def) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
791 |
|
63322 | 792 |
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
|
793 |
by (simp add: max_def) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
794 |
|
71138 | 795 |
lemma split_min_lin [no_atp]: |
796 |
\<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 | 797 |
by (cases a b rule: linorder_cases) auto |
71138 | 798 |
|
799 |
lemma split_max_lin [no_atp]: |
|
800 |
\<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 | 801 |
by (cases a b rule: linorder_cases) auto |
71138 | 802 |
|
63322 | 803 |
lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder" |
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
804 |
by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
805 |
|
63322 | 806 |
lemma max_of_mono: "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" for f :: "'a \<Rightarrow> 'b::linorder" |
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
807 |
by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
808 |
|
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
809 |
end |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
810 |
|
67727
ce3e87a51488
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
immler
parents:
67399
diff
changeset
|
811 |
lemma max_of_antimono: "antimono f \<Longrightarrow> max (f x) (f y) = f (min x y)" |
ce3e87a51488
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
immler
parents:
67399
diff
changeset
|
812 |
and min_of_antimono: "antimono f \<Longrightarrow> min (f x) (f y) = f (max x y)" |
ce3e87a51488
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
immler
parents:
67399
diff
changeset
|
813 |
for f::"'a::linorder \<Rightarrow> 'b::linorder" |
ce3e87a51488
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
immler
parents:
67399
diff
changeset
|
814 |
by (auto simp: antimono_def Orderings.max_def min_def intro!: antisym) |
ce3e87a51488
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
immler
parents:
67399
diff
changeset
|
815 |
|
61076 | 816 |
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
|
817 |
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
|
818 |
|
61076 | 819 |
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
|
820 |
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
|
821 |
|
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset
|
822 |
|
60758 | 823 |
subsection \<open>Uniqueness of inf and sup\<close> |
22454 | 824 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
825 |
lemma (in semilattice_inf) inf_unique: |
63322 | 826 |
fixes f (infixl "\<triangle>" 70) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
827 |
assumes le1: "\<And>x y. x \<triangle> y \<le> x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
828 |
and le2: "\<And>x y. x \<triangle> y \<le> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
829 |
and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" |
22737 | 830 |
shows "x \<sqinter> y = x \<triangle> y" |
73411 | 831 |
proof (rule order.antisym) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
832 |
show "x \<triangle> y \<le> x \<sqinter> y" |
63322 | 833 |
by (rule le_infI) (rule le1, rule le2) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
834 |
have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" |
63322 | 835 |
by (blast intro: greatest) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
836 |
show "x \<sqinter> y \<le> x \<triangle> y" |
63322 | 837 |
by (rule leI) simp_all |
22454 | 838 |
qed |
839 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
840 |
lemma (in semilattice_sup) sup_unique: |
63322 | 841 |
fixes f (infixl "\<nabla>" 70) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
842 |
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
|
843 |
and ge2: "\<And>x y. y \<le> x \<nabla> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
844 |
and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x" |
22737 | 845 |
shows "x \<squnion> y = x \<nabla> y" |
73411 | 846 |
proof (rule order.antisym) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
847 |
show "x \<squnion> y \<le> x \<nabla> y" |
63322 | 848 |
by (rule le_supI) (rule ge1, rule ge2) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
849 |
have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" |
63322 | 850 |
by (blast intro: least) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
851 |
show "x \<nabla> y \<le> x \<squnion> y" |
63322 | 852 |
by (rule leI) simp_all |
22454 | 853 |
qed |
36008 | 854 |
|
22454 | 855 |
|
69593 | 856 |
subsection \<open>Lattice on \<^typ>\<open>bool\<close>\<close> |
22454 | 857 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
858 |
instantiation bool :: boolean_algebra |
25510 | 859 |
begin |
860 |
||
63322 | 861 |
definition bool_Compl_def [simp]: "uminus = Not" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
862 |
|
63322 | 863 |
definition bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
864 |
|
63322 | 865 |
definition [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" |
25510 | 866 |
|
63322 | 867 |
definition [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" |
25510 | 868 |
|
63322 | 869 |
instance by standard auto |
22454 | 870 |
|
25510 | 871 |
end |
872 |
||
63322 | 873 |
lemma sup_boolI1: "P \<Longrightarrow> P \<squnion> Q" |
41080 | 874 |
by simp |
32781 | 875 |
|
63322 | 876 |
lemma sup_boolI2: "Q \<Longrightarrow> P \<squnion> Q" |
41080 | 877 |
by simp |
32781 | 878 |
|
63322 | 879 |
lemma sup_boolE: "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" |
41080 | 880 |
by auto |
32781 | 881 |
|
23878 | 882 |
|
69593 | 883 |
subsection \<open>Lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close> |
23878 | 884 |
|
51387 | 885 |
instantiation "fun" :: (type, semilattice_sup) semilattice_sup |
25510 | 886 |
begin |
887 |
||
63322 | 888 |
definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
41080 | 889 |
|
63322 | 890 |
lemma sup_apply [simp, code]: "(f \<squnion> g) x = f x \<squnion> g x" |
41080 | 891 |
by (simp add: sup_fun_def) |
25510 | 892 |
|
63588 | 893 |
instance |
894 |
by standard (simp_all add: le_fun_def) |
|
23878 | 895 |
|
25510 | 896 |
end |
23878 | 897 |
|
51387 | 898 |
instantiation "fun" :: (type, semilattice_inf) semilattice_inf |
899 |
begin |
|
900 |
||
63322 | 901 |
definition "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" |
51387 | 902 |
|
63322 | 903 |
lemma inf_apply [simp, code]: "(f \<sqinter> g) x = f x \<sqinter> g x" |
51387 | 904 |
by (simp add: inf_fun_def) |
905 |
||
63322 | 906 |
instance by standard (simp_all add: le_fun_def) |
51387 | 907 |
|
908 |
end |
|
909 |
||
910 |
instance "fun" :: (type, lattice) lattice .. |
|
911 |
||
63322 | 912 |
instance "fun" :: (type, distrib_lattice) distrib_lattice |
913 |
by standard (rule ext, simp add: sup_inf_distrib1) |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
914 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
915 |
instance "fun" :: (type, bounded_lattice) bounded_lattice .. |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
916 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
917 |
instantiation "fun" :: (type, uminus) uminus |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
918 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
919 |
|
63322 | 920 |
definition fun_Compl_def: "- A = (\<lambda>x. - A x)" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
921 |
|
63322 | 922 |
lemma uminus_apply [simp, code]: "(- A) x = - (A x)" |
41080 | 923 |
by (simp add: fun_Compl_def) |
924 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
925 |
instance .. |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
926 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
927 |
end |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
928 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
929 |
instantiation "fun" :: (type, minus) minus |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
930 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
931 |
|
63322 | 932 |
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
|
933 |
|
63322 | 934 |
lemma minus_apply [simp, code]: "(A - B) x = A x - B x" |
41080 | 935 |
by (simp add: fun_diff_def) |
936 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
937 |
instance .. |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
938 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
939 |
end |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
940 |
|
63322 | 941 |
instance "fun" :: (type, boolean_algebra) boolean_algebra |
942 |
by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+ |
|
26794 | 943 |
|
46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
944 |
|
60758 | 945 |
subsection \<open>Lattice on unary and binary predicates\<close> |
46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
946 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
947 |
lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
948 |
by (simp add: inf_fun_def) |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
949 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
950 |
lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
951 |
by (simp add: inf_fun_def) |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
952 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
953 |
lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
954 |
by (simp add: inf_fun_def) |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
955 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
956 |
lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
957 |
by (simp add: inf_fun_def) |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
958 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
959 |
lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x" |
54857 | 960 |
by (rule inf1E) |
46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
961 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
962 |
lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y" |
54857 | 963 |
by (rule inf2E) |
46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
964 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
965 |
lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x" |
54857 | 966 |
by (rule inf1E) |
46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
967 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
968 |
lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y" |
54857 | 969 |
by (rule inf2E) |
46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
970 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
971 |
lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
972 |
by (simp add: sup_fun_def) |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
973 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
974 |
lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
975 |
by (simp add: sup_fun_def) |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
976 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
977 |
lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
978 |
by (simp add: sup_fun_def) |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
979 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
980 |
lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
981 |
by (simp add: sup_fun_def) |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
982 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
983 |
lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
984 |
by (simp add: sup_fun_def) iprover |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
985 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
986 |
lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
987 |
by (simp add: sup_fun_def) iprover |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
988 |
|
63322 | 989 |
text \<open> \<^medskip> Classical introduction rule: no commitment to \<open>A\<close> vs \<open>B\<close>.\<close> |
46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
990 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
991 |
lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
992 |
by (auto simp add: sup_fun_def) |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
993 |
|
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
994 |
lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y" |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
995 |
by (auto simp add: sup_fun_def) |
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset
|
996 |
|
21249 | 997 |
end |