author | wenzelm |
Fri, 08 Feb 2019 14:42:28 +0100 | |
changeset 69794 | a19fdf64726c |
parent 69605 | a96320074298 |
child 70490 | c42a0a0a9a8d |
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 |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
126 |
lemma absorb_iff1: "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>* b = a" |
54858 | 127 |
using order_iff by auto |
128 |
||
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
129 |
lemma absorb_iff2: "b \<^bold>\<le> a \<longleftrightarrow> a \<^bold>* b = b" |
54858 | 130 |
using order_iff by (auto simp add: commute) |
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
131 |
|
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
132 |
end |
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
133 |
|
51487 | 134 |
locale semilattice_neutr_order = semilattice_neutr + semilattice_order |
52152 | 135 |
begin |
51487 | 136 |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
61799
diff
changeset
|
137 |
sublocale ordering_top less_eq less "\<^bold>1" |
61169 | 138 |
by standard (simp add: order_iff) |
51487 | 139 |
|
52152 | 140 |
end |
141 |
||
63661
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
142 |
text \<open>Passive interpretations for boolean operators\<close> |
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
143 |
|
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
144 |
lemma semilattice_neutr_and: |
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
145 |
"semilattice_neutr HOL.conj True" |
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
146 |
by standard auto |
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
147 |
|
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
148 |
lemma semilattice_neutr_or: |
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
149 |
"semilattice_neutr HOL.disj False" |
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
150 |
by standard auto |
92e037803666
formal passive interpretation proofs for conj and disj
haftmann
parents:
63588
diff
changeset
|
151 |
|
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset
|
152 |
|
60758 | 153 |
subsection \<open>Syntactic infimum and supremum operations\<close> |
41082 | 154 |
|
44845 | 155 |
class inf = |
156 |
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
|
25206 | 157 |
|
63322 | 158 |
class sup = |
44845 | 159 |
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
160 |
||
46691 | 161 |
|
60758 | 162 |
subsection \<open>Concrete lattices\<close> |
46691 | 163 |
|
44845 | 164 |
class semilattice_inf = order + inf + |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
165 |
assumes inf_le1 [simp]: "x \<sqinter> y \<le> x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
166 |
and inf_le2 [simp]: "x \<sqinter> y \<le> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
167 |
and inf_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z" |
21249 | 168 |
|
44845 | 169 |
class semilattice_sup = order + sup + |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
170 |
assumes sup_ge1 [simp]: "x \<le> x \<squnion> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
171 |
and sup_ge2 [simp]: "y \<le> x \<squnion> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
172 |
and sup_least: "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x" |
26014 | 173 |
begin |
174 |
||
63588 | 175 |
text \<open>Dual lattice.\<close> |
63322 | 176 |
lemma dual_semilattice: "class.semilattice_inf sup greater_eq greater" |
177 |
by (rule class.semilattice_inf.intro, rule dual_order) |
|
178 |
(unfold_locales, simp_all add: sup_least) |
|
26014 | 179 |
|
180 |
end |
|
21249 | 181 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
182 |
class lattice = semilattice_inf + semilattice_sup |
21249 | 183 |
|
25382 | 184 |
|
60758 | 185 |
subsubsection \<open>Intro and elim rules\<close> |
21733 | 186 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
187 |
context semilattice_inf |
21733 | 188 |
begin |
21249 | 189 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
190 |
lemma le_infI1: "a \<le> x \<Longrightarrow> a \<sqinter> b \<le> x" |
32064 | 191 |
by (rule order_trans) auto |
21249 | 192 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
193 |
lemma le_infI2: "b \<le> x \<Longrightarrow> a \<sqinter> b \<le> x" |
32064 | 194 |
by (rule order_trans) auto |
21733 | 195 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
196 |
lemma le_infI: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> a \<sqinter> b" |
54857 | 197 |
by (fact inf_greatest) (* FIXME: duplicate lemma *) |
21249 | 198 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
199 |
lemma le_infE: "x \<le> a \<sqinter> b \<Longrightarrow> (x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> P) \<Longrightarrow> P" |
36008 | 200 |
by (blast intro: order_trans inf_le1 inf_le2) |
21249 | 201 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
202 |
lemma le_inf_iff: "x \<le> y \<sqinter> z \<longleftrightarrow> x \<le> y \<and> x \<le> z" |
32064 | 203 |
by (blast intro: le_infI elim: le_infE) |
21733 | 204 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
205 |
lemma le_iff_inf: "x \<le> y \<longleftrightarrow> x \<sqinter> y = x" |
54859 | 206 |
by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff) |
21249 | 207 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
208 |
lemma inf_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<le> c \<sqinter> d" |
36008 | 209 |
by (fast intro: inf_greatest le_infI1 le_infI2) |
210 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
211 |
lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf" |
25206 | 212 |
by (auto simp add: mono_def intro: Lattices.inf_greatest) |
21733 | 213 |
|
25206 | 214 |
end |
21733 | 215 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
216 |
context semilattice_sup |
21733 | 217 |
begin |
21249 | 218 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
219 |
lemma le_supI1: "x \<le> a \<Longrightarrow> x \<le> a \<squnion> b" |
63322 | 220 |
by (rule order_trans) auto |
221 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
222 |
lemma le_supI2: "x \<le> b \<Longrightarrow> x \<le> a \<squnion> b" |
25062 | 223 |
by (rule order_trans) auto |
21249 | 224 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
225 |
lemma le_supI: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> a \<squnion> b \<le> x" |
54857 | 226 |
by (fact sup_least) (* FIXME: duplicate lemma *) |
21249 | 227 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
228 |
lemma le_supE: "a \<squnion> b \<le> x \<Longrightarrow> (a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> P) \<Longrightarrow> P" |
36008 | 229 |
by (blast intro: order_trans sup_ge1 sup_ge2) |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
230 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
231 |
lemma le_sup_iff: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z" |
32064 | 232 |
by (blast intro: le_supI elim: le_supE) |
21733 | 233 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
234 |
lemma le_iff_sup: "x \<le> y \<longleftrightarrow> x \<squnion> y = y" |
54859 | 235 |
by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff) |
21734 | 236 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
237 |
lemma sup_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<le> c \<squnion> d" |
36008 | 238 |
by (fast intro: sup_least le_supI1 le_supI2) |
239 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
240 |
lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup" |
25206 | 241 |
by (auto simp add: mono_def intro: Lattices.sup_least) |
21733 | 242 |
|
25206 | 243 |
end |
23878 | 244 |
|
21733 | 245 |
|
60758 | 246 |
subsubsection \<open>Equational laws\<close> |
21249 | 247 |
|
52152 | 248 |
context semilattice_inf |
249 |
begin |
|
250 |
||
61605 | 251 |
sublocale inf: semilattice inf |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
252 |
proof |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
253 |
fix a b c |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
254 |
show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" |
54859 | 255 |
by (rule 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
|
256 |
show "a \<sqinter> b = b \<sqinter> a" |
54859 | 257 |
by (rule 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
|
258 |
show "a \<sqinter> a = a" |
54859 | 259 |
by (rule 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
|
260 |
qed |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
261 |
|
61605 | 262 |
sublocale inf: semilattice_order inf less_eq less |
61169 | 263 |
by standard (auto simp add: le_iff_inf less_le) |
51487 | 264 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
265 |
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
|
266 |
by (fact inf.assoc) |
21733 | 267 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
268 |
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
|
269 |
by (fact inf.commute) |
21733 | 270 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
271 |
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
|
272 |
by (fact inf.left_commute) |
21733 | 273 |
|
44921 | 274 |
lemma inf_idem: "x \<sqinter> x = x" |
275 |
by (fact inf.idem) (* already simp *) |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
276 |
|
50615 | 277 |
lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
278 |
by (fact inf.left_idem) (* already simp *) |
|
279 |
||
280 |
lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y" |
|
281 |
by (fact inf.right_idem) (* already simp *) |
|
21733 | 282 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
283 |
lemma inf_absorb1: "x \<le> y \<Longrightarrow> x \<sqinter> y = x" |
32064 | 284 |
by (rule antisym) auto |
21733 | 285 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
286 |
lemma inf_absorb2: "y \<le> x \<Longrightarrow> x \<sqinter> y = y" |
32064 | 287 |
by (rule antisym) auto |
63322 | 288 |
|
32064 | 289 |
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem |
21733 | 290 |
|
291 |
end |
|
292 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
293 |
context semilattice_sup |
21733 | 294 |
begin |
21249 | 295 |
|
61605 | 296 |
sublocale sup: semilattice sup |
52152 | 297 |
proof |
298 |
fix a b c |
|
299 |
show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" |
|
54859 | 300 |
by (rule antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff) |
52152 | 301 |
show "a \<squnion> b = b \<squnion> a" |
54859 | 302 |
by (rule antisym) (auto simp add: le_sup_iff) |
52152 | 303 |
show "a \<squnion> a = a" |
54859 | 304 |
by (rule antisym) (auto simp add: le_sup_iff) |
52152 | 305 |
qed |
306 |
||
61605 | 307 |
sublocale sup: semilattice_order sup greater_eq greater |
61169 | 308 |
by standard (auto simp add: le_iff_sup sup.commute less_le) |
52152 | 309 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
310 |
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
|
311 |
by (fact sup.assoc) |
21733 | 312 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
313 |
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
|
314 |
by (fact sup.commute) |
21733 | 315 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
316 |
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
|
317 |
by (fact sup.left_commute) |
21733 | 318 |
|
44921 | 319 |
lemma sup_idem: "x \<squnion> x = x" |
320 |
by (fact sup.idem) (* already simp *) |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset
|
321 |
|
44918 | 322 |
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
|
323 |
by (fact sup.left_idem) |
21733 | 324 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
325 |
lemma sup_absorb1: "y \<le> x \<Longrightarrow> x \<squnion> y = x" |
32064 | 326 |
by (rule antisym) auto |
21733 | 327 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
328 |
lemma sup_absorb2: "x \<le> y \<Longrightarrow> x \<squnion> y = y" |
32064 | 329 |
by (rule antisym) auto |
21249 | 330 |
|
32064 | 331 |
lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem |
21733 | 332 |
|
333 |
end |
|
21249 | 334 |
|
21733 | 335 |
context lattice |
336 |
begin |
|
337 |
||
67399 | 338 |
lemma dual_lattice: "class.lattice sup (\<ge>) (>) inf" |
63588 | 339 |
by (rule class.lattice.intro, |
340 |
rule dual_semilattice, |
|
341 |
rule class.semilattice_sup.intro, |
|
342 |
rule dual_order) |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
343 |
(unfold_locales, auto) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
344 |
|
44918 | 345 |
lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x" |
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset
|
346 |
by (blast intro: antisym inf_le1 inf_greatest sup_ge1) |
21733 | 347 |
|
44918 | 348 |
lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x" |
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset
|
349 |
by (blast intro: antisym sup_ge1 sup_least inf_le1) |
21733 | 350 |
|
32064 | 351 |
lemmas inf_sup_aci = inf_aci sup_aci |
21734 | 352 |
|
22454 | 353 |
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 |
354 |
||
63588 | 355 |
text \<open>Towards distributivity.\<close> |
21249 | 356 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
357 |
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<le> (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
32064 | 358 |
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
21734 | 359 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
360 |
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<le> x \<sqinter> (y \<squnion> z)" |
32064 | 361 |
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) |
21734 | 362 |
|
63322 | 363 |
text \<open>If you have one of them, you have them all.\<close> |
21249 | 364 |
|
21733 | 365 |
lemma distrib_imp1: |
63322 | 366 |
assumes distrib: "\<And>x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
367 |
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
|
21249 | 368 |
proof- |
63322 | 369 |
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" |
370 |
by simp |
|
44918 | 371 |
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" |
63322 | 372 |
by (simp add: distrib inf_commute sup_assoc del: sup_inf_absorb) |
21249 | 373 |
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" |
63322 | 374 |
by (simp add: inf_commute) |
375 |
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:distrib) |
|
21249 | 376 |
finally show ?thesis . |
377 |
qed |
|
378 |
||
21733 | 379 |
lemma distrib_imp2: |
63322 | 380 |
assumes distrib: "\<And>x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
381 |
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
|
21249 | 382 |
proof- |
63322 | 383 |
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" |
384 |
by simp |
|
44918 | 385 |
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" |
63322 | 386 |
by (simp add: distrib sup_commute inf_assoc del: inf_sup_absorb) |
21249 | 387 |
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" |
63322 | 388 |
by (simp add: sup_commute) |
389 |
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by (simp add:distrib) |
|
21249 | 390 |
finally show ?thesis . |
391 |
qed |
|
392 |
||
21733 | 393 |
end |
21249 | 394 |
|
63322 | 395 |
|
60758 | 396 |
subsubsection \<open>Strict order\<close> |
32568 | 397 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
398 |
context semilattice_inf |
32568 | 399 |
begin |
400 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
401 |
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
|
402 |
by (auto simp add: less_le inf_absorb1 intro: le_infI1) |
32568 | 403 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
404 |
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
|
405 |
by (auto simp add: less_le inf_absorb2 intro: le_infI2) |
32568 | 406 |
|
407 |
end |
|
408 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
409 |
context semilattice_sup |
32568 | 410 |
begin |
411 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
412 |
lemma less_supI1: "x < a \<Longrightarrow> x < a \<squnion> b" |
44921 | 413 |
using dual_semilattice |
414 |
by (rule semilattice_inf.less_infI1) |
|
32568 | 415 |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
416 |
lemma less_supI2: "x < b \<Longrightarrow> x < a \<squnion> b" |
44921 | 417 |
using dual_semilattice |
418 |
by (rule semilattice_inf.less_infI2) |
|
32568 | 419 |
|
420 |
end |
|
421 |
||
21249 | 422 |
|
60758 | 423 |
subsection \<open>Distributive lattices\<close> |
21249 | 424 |
|
22454 | 425 |
class distrib_lattice = lattice + |
21249 | 426 |
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
427 |
||
21733 | 428 |
context distrib_lattice |
429 |
begin |
|
430 |
||
63322 | 431 |
lemma sup_inf_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
44921 | 432 |
by (simp add: sup_commute sup_inf_distrib1) |
21249 | 433 |
|
63322 | 434 |
lemma inf_sup_distrib1: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
44921 | 435 |
by (rule distrib_imp2 [OF sup_inf_distrib1]) |
21249 | 436 |
|
63322 | 437 |
lemma inf_sup_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" |
44921 | 438 |
by (simp add: inf_commute inf_sup_distrib1) |
21249 | 439 |
|
67399 | 440 |
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
|
441 |
by (rule class.distrib_lattice.intro, rule dual_lattice) |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
442 |
(unfold_locales, fact inf_sup_distrib1) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
443 |
|
63322 | 444 |
lemmas sup_inf_distrib = sup_inf_distrib1 sup_inf_distrib2 |
36008 | 445 |
|
63322 | 446 |
lemmas inf_sup_distrib = inf_sup_distrib1 inf_sup_distrib2 |
36008 | 447 |
|
63322 | 448 |
lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 |
21249 | 449 |
|
21733 | 450 |
end |
451 |
||
21249 | 452 |
|
60758 | 453 |
subsection \<open>Bounded lattices and boolean algebras\<close> |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
454 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
455 |
class bounded_semilattice_inf_top = semilattice_inf + order_top |
52152 | 456 |
begin |
51487 | 457 |
|
61605 | 458 |
sublocale inf_top: semilattice_neutr inf top |
459 |
+ inf_top: semilattice_neutr_order inf top less_eq less |
|
51487 | 460 |
proof |
63322 | 461 |
show "x \<sqinter> \<top> = x" for x |
51487 | 462 |
by (rule inf_absorb1) simp |
463 |
qed |
|
464 |
||
52152 | 465 |
end |
51487 | 466 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
467 |
class bounded_semilattice_sup_bot = semilattice_sup + order_bot |
52152 | 468 |
begin |
469 |
||
61605 | 470 |
sublocale sup_bot: semilattice_neutr sup bot |
471 |
+ sup_bot: semilattice_neutr_order sup bot greater_eq greater |
|
51487 | 472 |
proof |
63322 | 473 |
show "x \<squnion> \<bottom> = x" for x |
51487 | 474 |
by (rule sup_absorb1) simp |
475 |
qed |
|
476 |
||
52152 | 477 |
end |
478 |
||
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
479 |
class bounded_lattice_bot = lattice + order_bot |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
480 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
481 |
|
51487 | 482 |
subclass bounded_semilattice_sup_bot .. |
483 |
||
63322 | 484 |
lemma inf_bot_left [simp]: "\<bottom> \<sqinter> x = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
485 |
by (rule inf_absorb1) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
486 |
|
63322 | 487 |
lemma inf_bot_right [simp]: "x \<sqinter> \<bottom> = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
488 |
by (rule inf_absorb2) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
489 |
|
63322 | 490 |
lemma sup_bot_left: "\<bottom> \<squnion> x = x" |
51487 | 491 |
by (fact sup_bot.left_neutral) |
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
492 |
|
63322 | 493 |
lemma sup_bot_right: "x \<squnion> \<bottom> = x" |
51487 | 494 |
by (fact sup_bot.right_neutral) |
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
495 |
|
63322 | 496 |
lemma sup_eq_bot_iff [simp]: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
497 |
by (simp add: eq_iff) |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
498 |
|
63322 | 499 |
lemma bot_eq_sup_iff [simp]: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
51593 | 500 |
by (simp add: eq_iff) |
501 |
||
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
502 |
end |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
503 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
504 |
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
|
505 |
begin |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
506 |
|
51487 | 507 |
subclass bounded_semilattice_inf_top .. |
508 |
||
63322 | 509 |
lemma sup_top_left [simp]: "\<top> \<squnion> x = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
510 |
by (rule sup_absorb1) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
511 |
|
63322 | 512 |
lemma sup_top_right [simp]: "x \<squnion> \<top> = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
513 |
by (rule sup_absorb2) simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
514 |
|
63322 | 515 |
lemma inf_top_left: "\<top> \<sqinter> x = x" |
51487 | 516 |
by (fact inf_top.left_neutral) |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
517 |
|
63322 | 518 |
lemma inf_top_right: "x \<sqinter> \<top> = x" |
51487 | 519 |
by (fact inf_top.right_neutral) |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
520 |
|
63322 | 521 |
lemma inf_eq_top_iff [simp]: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>" |
36008 | 522 |
by (simp add: eq_iff) |
32568 | 523 |
|
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
524 |
end |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
525 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52152
diff
changeset
|
526 |
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
|
527 |
begin |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset
|
528 |
|
51487 | 529 |
subclass bounded_lattice_bot .. |
530 |
subclass bounded_lattice_top .. |
|
531 |
||
63322 | 532 |
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
|
533 |
by unfold_locales (auto simp add: less_le_not_le) |
32568 | 534 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
535 |
end |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
536 |
|
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
537 |
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
|
538 |
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
|
539 |
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
|
540 |
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
|
541 |
begin |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
542 |
|
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
543 |
lemma dual_boolean_algebra: |
44845 | 544 |
"class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>" |
63588 | 545 |
by (rule class.boolean_algebra.intro, |
546 |
rule dual_bounded_lattice, |
|
547 |
rule dual_distrib_lattice) |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
548 |
(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
|
549 |
|
63322 | 550 |
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
|
551 |
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
|
552 |
|
63322 | 553 |
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
|
554 |
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
|
555 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
556 |
lemma compl_unique: |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
557 |
assumes "x \<sqinter> y = \<bottom>" |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
558 |
and "x \<squnion> y = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
559 |
shows "- x = y" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
560 |
proof - |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
561 |
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
|
562 |
using inf_compl_bot assms(1) by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
563 |
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
|
564 |
by (simp add: inf_commute) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
565 |
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
|
566 |
by (simp add: inf_sup_distrib1) |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
567 |
then have "- x \<sqinter> \<top> = y \<sqinter> \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
568 |
using sup_compl_top assms(2) by simp |
34209 | 569 |
then show "- x = y" by simp |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
570 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
571 |
|
63322 | 572 |
lemma double_compl [simp]: "- (- x) = x" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
573 |
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
|
574 |
|
63322 | 575 |
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
|
576 |
proof |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
577 |
assume "- x = - y" |
36008 | 578 |
then have "- (- x) = - (- y)" by (rule arg_cong) |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
579 |
then show "x = y" by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
580 |
next |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
581 |
assume "x = y" |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
582 |
then show "- x = - y" by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
583 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
584 |
|
63322 | 585 |
lemma compl_bot_eq [simp]: "- \<bottom> = \<top>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
586 |
proof - |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
587 |
from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" . |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
588 |
then show ?thesis by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
589 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
590 |
|
63322 | 591 |
lemma compl_top_eq [simp]: "- \<top> = \<bottom>" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
592 |
proof - |
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
593 |
from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" . |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
594 |
then show ?thesis by simp |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
595 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
596 |
|
63322 | 597 |
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
|
598 |
proof (rule compl_unique) |
36008 | 599 |
have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))" |
600 |
by (simp only: inf_sup_distrib inf_aci) |
|
601 |
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
|
602 |
by (simp add: inf_compl_bot) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
603 |
next |
36008 | 604 |
have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))" |
605 |
by (simp only: sup_inf_distrib sup_aci) |
|
606 |
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
|
607 |
by (simp add: sup_compl_top) |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
608 |
qed |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
609 |
|
63322 | 610 |
lemma compl_sup [simp]: "- (x \<squnion> y) = - x \<sqinter> - y" |
44921 | 611 |
using dual_boolean_algebra |
612 |
by (rule boolean_algebra.compl_inf) |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
613 |
|
36008 | 614 |
lemma compl_mono: |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
615 |
assumes "x \<le> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
616 |
shows "- y \<le> - x" |
36008 | 617 |
proof - |
63322 | 618 |
from assms have "x \<squnion> y = y" by (simp only: le_iff_sup) |
36008 | 619 |
then have "- (x \<squnion> y) = - y" by simp |
620 |
then have "- x \<sqinter> - y = - y" by simp |
|
621 |
then have "- y \<sqinter> - x = - y" by (simp only: inf_commute) |
|
63322 | 622 |
then show ?thesis by (simp only: le_iff_inf) |
36008 | 623 |
qed |
624 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
625 |
lemma compl_le_compl_iff [simp]: "- x \<le> - y \<longleftrightarrow> y \<le> x" |
43873 | 626 |
by (auto dest: compl_mono) |
627 |
||
628 |
lemma compl_le_swap1: |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
629 |
assumes "y \<le> - x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
630 |
shows "x \<le> -y" |
43873 | 631 |
proof - |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
632 |
from assms have "- (- x) \<le> - y" by (simp only: compl_le_compl_iff) |
43873 | 633 |
then show ?thesis by simp |
634 |
qed |
|
635 |
||
636 |
lemma compl_le_swap2: |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
637 |
assumes "- y \<le> x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
638 |
shows "- x \<le> y" |
43873 | 639 |
proof - |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
640 |
from assms have "- x \<le> - (- y)" by (simp only: compl_le_compl_iff) |
43873 | 641 |
then show ?thesis by simp |
642 |
qed |
|
643 |
||
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
644 |
lemma compl_less_compl_iff: "- x < - y \<longleftrightarrow> y < x" (* TODO: declare [simp] ? *) |
44919 | 645 |
by (auto simp add: less_le) |
43873 | 646 |
|
647 |
lemma compl_less_swap1: |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
648 |
assumes "y < - x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
649 |
shows "x < - y" |
43873 | 650 |
proof - |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
651 |
from assms have "- (- x) < - y" by (simp only: compl_less_compl_iff) |
43873 | 652 |
then show ?thesis by simp |
653 |
qed |
|
654 |
||
655 |
lemma compl_less_swap2: |
|
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
656 |
assumes "- y < x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
657 |
shows "- x < y" |
43873 | 658 |
proof - |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
659 |
from assms have "- x < - (- y)" |
63588 | 660 |
by (simp only: compl_less_compl_iff) |
43873 | 661 |
then show ?thesis by simp |
662 |
qed |
|
36008 | 663 |
|
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
664 |
lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top" |
63322 | 665 |
by (simp add: inf_sup_aci sup_compl_top) |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
666 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
667 |
lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top" |
63322 | 668 |
by (simp add: inf_sup_aci sup_compl_top) |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
669 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
670 |
lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot" |
63322 | 671 |
by (simp add: inf_sup_aci inf_compl_bot) |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
672 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
673 |
lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot" |
63322 | 674 |
by (simp add: inf_sup_aci inf_compl_bot) |
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
675 |
|
63588 | 676 |
declare inf_compl_bot [simp] |
677 |
and sup_compl_top [simp] |
|
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
678 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
679 |
lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top" |
63322 | 680 |
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
|
681 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
682 |
lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top" |
63322 | 683 |
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
|
684 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
685 |
lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot" |
63322 | 686 |
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
|
687 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
688 |
lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot" |
63322 | 689 |
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
|
690 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
691 |
lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot" |
63322 | 692 |
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
|
693 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
694 |
end |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
695 |
|
69605 | 696 |
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
|
697 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
698 |
simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") = |
61799 | 699 |
\<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
|
700 |
|
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61605
diff
changeset
|
701 |
simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") = |
61799 | 702 |
\<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
|
703 |
|
63322 | 704 |
|
61799 | 705 |
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
|
706 |
|
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
707 |
context linorder |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
708 |
begin |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
709 |
|
61605 | 710 |
sublocale min: semilattice_order min less_eq less |
711 |
+ max: semilattice_order max greater_eq greater |
|
61169 | 712 |
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
|
713 |
|
63322 | 714 |
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
|
715 |
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
|
716 |
|
63322 | 717 |
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
|
718 |
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
|
719 |
|
63322 | 720 |
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
|
721 |
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
|
722 |
|
63322 | 723 |
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
|
724 |
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
|
725 |
|
63322 | 726 |
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
|
727 |
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
|
728 |
|
63322 | 729 |
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
|
730 |
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
|
731 |
|
63322 | 732 |
lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)" |
54862 | 733 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
734 |
||
63322 | 735 |
lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)" |
54862 | 736 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
737 |
||
63322 | 738 |
lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)" |
54862 | 739 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
740 |
||
63322 | 741 |
lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)" |
54862 | 742 |
by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) |
743 |
||
744 |
lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2 |
|
745 |
||
63322 | 746 |
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
|
747 |
by (simp add: min_def) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
748 |
|
63322 | 749 |
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
|
750 |
by (simp add: max_def) |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
751 |
|
63322 | 752 |
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
|
753 |
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
|
754 |
|
63322 | 755 |
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
|
756 |
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
|
757 |
|
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
758 |
end |
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54859
diff
changeset
|
759 |
|
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
|
760 |
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
|
761 |
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
|
762 |
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
|
763 |
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
|
764 |
|
61076 | 765 |
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
|
766 |
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
|
767 |
|
61076 | 768 |
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
|
769 |
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
|
770 |
|
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset
|
771 |
|
60758 | 772 |
subsection \<open>Uniqueness of inf and sup\<close> |
22454 | 773 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
774 |
lemma (in semilattice_inf) inf_unique: |
63322 | 775 |
fixes f (infixl "\<triangle>" 70) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
776 |
assumes le1: "\<And>x y. x \<triangle> y \<le> x" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
777 |
and le2: "\<And>x y. x \<triangle> y \<le> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
778 |
and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" |
22737 | 779 |
shows "x \<sqinter> y = x \<triangle> y" |
22454 | 780 |
proof (rule antisym) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
781 |
show "x \<triangle> y \<le> x \<sqinter> y" |
63322 | 782 |
by (rule le_infI) (rule le1, rule le2) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
783 |
have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" |
63322 | 784 |
by (blast intro: greatest) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
785 |
show "x \<sqinter> y \<le> x \<triangle> y" |
63322 | 786 |
by (rule leI) simp_all |
22454 | 787 |
qed |
788 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
789 |
lemma (in semilattice_sup) sup_unique: |
63322 | 790 |
fixes f (infixl "\<nabla>" 70) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
791 |
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
|
792 |
and ge2: "\<And>x y. y \<le> x \<nabla> y" |
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
793 |
and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x" |
22737 | 794 |
shows "x \<squnion> y = x \<nabla> y" |
22454 | 795 |
proof (rule antisym) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
796 |
show "x \<squnion> y \<le> x \<nabla> y" |
63322 | 797 |
by (rule le_supI) (rule ge1, rule ge2) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
798 |
have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" |
63322 | 799 |
by (blast intro: least) |
63820
9f004fbf9d5c
discontinued theory-local special syntax for lattice orderings
haftmann
parents:
63661
diff
changeset
|
800 |
show "x \<nabla> y \<le> x \<squnion> y" |
63322 | 801 |
by (rule leI) simp_all |
22454 | 802 |
qed |
36008 | 803 |
|
22454 | 804 |
|
69593 | 805 |
subsection \<open>Lattice on \<^typ>\<open>bool\<close>\<close> |
22454 | 806 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
807 |
instantiation bool :: boolean_algebra |
25510 | 808 |
begin |
809 |
||
63322 | 810 |
definition bool_Compl_def [simp]: "uminus = Not" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
811 |
|
63322 | 812 |
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
|
813 |
|
63322 | 814 |
definition [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" |
25510 | 815 |
|
63322 | 816 |
definition [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" |
25510 | 817 |
|
63322 | 818 |
instance by standard auto |
22454 | 819 |
|
25510 | 820 |
end |
821 |
||
63322 | 822 |
lemma sup_boolI1: "P \<Longrightarrow> P \<squnion> Q" |
41080 | 823 |
by simp |
32781 | 824 |
|
63322 | 825 |
lemma sup_boolI2: "Q \<Longrightarrow> P \<squnion> Q" |
41080 | 826 |
by simp |
32781 | 827 |
|
63322 | 828 |
lemma sup_boolE: "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" |
41080 | 829 |
by auto |
32781 | 830 |
|
23878 | 831 |
|
69593 | 832 |
subsection \<open>Lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close> |
23878 | 833 |
|
51387 | 834 |
instantiation "fun" :: (type, semilattice_sup) semilattice_sup |
25510 | 835 |
begin |
836 |
||
63322 | 837 |
definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
41080 | 838 |
|
63322 | 839 |
lemma sup_apply [simp, code]: "(f \<squnion> g) x = f x \<squnion> g x" |
41080 | 840 |
by (simp add: sup_fun_def) |
25510 | 841 |
|
63588 | 842 |
instance |
843 |
by standard (simp_all add: le_fun_def) |
|
23878 | 844 |
|
25510 | 845 |
end |
23878 | 846 |
|
51387 | 847 |
instantiation "fun" :: (type, semilattice_inf) semilattice_inf |
848 |
begin |
|
849 |
||
63322 | 850 |
definition "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" |
51387 | 851 |
|
63322 | 852 |
lemma inf_apply [simp, code]: "(f \<sqinter> g) x = f x \<sqinter> g x" |
51387 | 853 |
by (simp add: inf_fun_def) |
854 |
||
63322 | 855 |
instance by standard (simp_all add: le_fun_def) |
51387 | 856 |
|
857 |
end |
|
858 |
||
859 |
instance "fun" :: (type, lattice) lattice .. |
|
860 |
||
63322 | 861 |
instance "fun" :: (type, distrib_lattice) distrib_lattice |
862 |
by standard (rule ext, simp add: sup_inf_distrib1) |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
863 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
864 |
instance "fun" :: (type, bounded_lattice) bounded_lattice .. |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset
|
865 |
|
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
866 |
instantiation "fun" :: (type, uminus) uminus |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
867 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
868 |
|
63322 | 869 |
definition fun_Compl_def: "- A = (\<lambda>x. - A x)" |
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
870 |
|
63322 | 871 |
lemma uminus_apply [simp, code]: "(- A) x = - (A x)" |
41080 | 872 |
by (simp add: fun_Compl_def) |
873 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
874 |
instance .. |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
875 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
876 |
end |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
877 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
878 |
instantiation "fun" :: (type, minus) minus |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
879 |
begin |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
880 |
|
63322 | 881 |
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
|
882 |
|
63322 | 883 |
lemma minus_apply [simp, code]: "(A - B) x = A x - B x" |
41080 | 884 |
by (simp add: fun_diff_def) |
885 |
||
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
886 |
instance .. |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
887 |
|
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
888 |
end |
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset
|
889 |
|
63322 | 890 |
instance "fun" :: (type, boolean_algebra) boolean_algebra |
891 |
by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+ |
|
26794 | 892 |
|
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
|
893 |
|
60758 | 894 |
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
|
895 |
|
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
|
896 |
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
|
897 |
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
|
898 |
|
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
|
899 |
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
|
900 |
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
|
901 |
|
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
|
902 |
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
|
903 |
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
|
904 |
|
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
|
905 |
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
|
906 |
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
|
907 |
|
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
|
908 |
lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x" |
54857 | 909 |
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
|
910 |
|
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
|
911 |
lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y" |
54857 | 912 |
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
|
913 |
|
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
|
914 |
lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x" |
54857 | 915 |
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
|
916 |
|
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
|
917 |
lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y" |
54857 | 918 |
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
|
919 |
|
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
|
920 |
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
|
921 |
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
|
922 |
|
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
|
923 |
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
|
924 |
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
|
925 |
|
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
|
926 |
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
|
927 |
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
|
928 |
|
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
|
929 |
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
|
930 |
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
|
931 |
|
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
|
932 |
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
|
933 |
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
|
934 |
|
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
|
935 |
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
|
936 |
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
|
937 |
|
63322 | 938 |
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
|
939 |
|
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
|
940 |
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
|
941 |
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
|
942 |
|
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
|
943 |
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
|
944 |
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
|
945 |
|
21249 | 946 |
end |