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