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