author  haftmann 
Tue, 04 May 2010 08:55:43 +0200  
changeset 36635  080b755377c0 
parent 36352  f71978e47cd5 
child 36673  6d25e8dab1e3 
permissions  rwrr 
21249  1 
(* Title: HOL/Lattices.thy 
2 
Author: Tobias Nipkow 

3 
*) 

4 

22454  5 
header {* Abstract lattices *} 
21249  6 

7 
theory Lattices 

35121  8 
imports Orderings Groups 
21249  9 
begin 
10 

35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

11 
subsection {* Abstract semilattice *} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

12 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

13 
text {* 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

14 
This locales provide a basic structure for interpretation into 
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. 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

17 
*} 
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 + 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

20 
assumes idem [simp]: "f a a = a" 
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 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

23 
lemma left_idem [simp]: 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

24 
"f a (f a b) = f a b" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

25 
by (simp add: assoc [symmetric]) 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

26 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

27 
end 
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 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

30 
subsection {* Idempotent semigroup *} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

31 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

32 
class ab_semigroup_idem_mult = ab_semigroup_mult + 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

33 
assumes mult_idem: "x * x = x" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

34 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

35 
sublocale ab_semigroup_idem_mult < times!: semilattice times proof 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

36 
qed (fact mult_idem) 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

37 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

38 
context ab_semigroup_idem_mult 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

39 
begin 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

40 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

41 
lemmas mult_left_idem = times.left_idem 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

42 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

43 
end 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

44 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

45 

35724  46 
subsection {* Concrete lattices *} 
21249  47 

25206  48 
notation 
25382  49 
less_eq (infix "\<sqsubseteq>" 50) and 
32568  50 
less (infix "\<sqsubset>" 50) and 
51 
top ("\<top>") and 

52 
bot ("\<bottom>") 

25206  53 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

54 
class semilattice_inf = order + 
21249  55 
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) 
22737  56 
assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" 
57 
and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" 

21733  58 
and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" 
21249  59 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

60 
class semilattice_sup = order + 
21249  61 
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) 
22737  62 
assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" 
63 
and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" 

21733  64 
and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x" 
26014  65 
begin 
66 

67 
text {* Dual lattice *} 

68 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

69 
lemma dual_semilattice: 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

70 
"class.semilattice_inf (op \<ge>) (op >) sup" 
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

71 
by (rule class.semilattice_inf.intro, rule dual_order) 
27682  72 
(unfold_locales, simp_all add: sup_least) 
26014  73 

74 
end 

21249  75 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

76 
class lattice = semilattice_inf + semilattice_sup 
21249  77 

25382  78 

28562  79 
subsubsection {* Intro and elim rules*} 
21733  80 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

81 
context semilattice_inf 
21733  82 
begin 
21249  83 

32064  84 
lemma le_infI1: 
85 
"a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" 

86 
by (rule order_trans) auto 

21249  87 

32064  88 
lemma le_infI2: 
89 
"b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" 

90 
by (rule order_trans) auto 

21733  91 

32064  92 
lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b" 
36008  93 
by (rule inf_greatest) (* FIXME: duplicate lemma *) 
21249  94 

32064  95 
lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" 
36008  96 
by (blast intro: order_trans inf_le1 inf_le2) 
21249  97 

21734  98 
lemma le_inf_iff [simp]: 
32064  99 
"x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z" 
100 
by (blast intro: le_infI elim: le_infE) 

21733  101 

32064  102 
lemma le_iff_inf: 
103 
"x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x" 

104 
by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) 

21249  105 

36008  106 
lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d" 
107 
by (fast intro: inf_greatest le_infI1 le_infI2) 

108 

25206  109 
lemma mono_inf: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

110 
fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf" 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

111 
shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" 
25206  112 
by (auto simp add: mono_def intro: Lattices.inf_greatest) 
21733  113 

25206  114 
end 
21733  115 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

116 
context semilattice_sup 
21733  117 
begin 
21249  118 

32064  119 
lemma le_supI1: 
120 
"x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" 

25062  121 
by (rule order_trans) auto 
21249  122 

32064  123 
lemma le_supI2: 
124 
"x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" 

25062  125 
by (rule order_trans) auto 
21733  126 

32064  127 
lemma le_supI: 
128 
"a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x" 

36008  129 
by (rule sup_least) (* FIXME: duplicate lemma *) 
21249  130 

32064  131 
lemma le_supE: 
132 
"a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" 

36008  133 
by (blast intro: order_trans sup_ge1 sup_ge2) 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

134 

32064  135 
lemma le_sup_iff [simp]: 
136 
"x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" 

137 
by (blast intro: le_supI elim: le_supE) 

21733  138 

32064  139 
lemma le_iff_sup: 
140 
"x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y" 

141 
by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) 

21734  142 

36008  143 
lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d" 
144 
by (fast intro: sup_least le_supI1 le_supI2) 

145 

25206  146 
lemma mono_sup: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

147 
fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup" 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

148 
shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" 
25206  149 
by (auto simp add: mono_def intro: Lattices.sup_least) 
21733  150 

25206  151 
end 
23878  152 

21733  153 

32064  154 
subsubsection {* Equational laws *} 
21249  155 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

156 
sublocale semilattice_inf < inf!: semilattice inf 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

157 
proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

158 
fix a b c 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

159 
show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

160 
by (rule antisym) (auto intro: le_infI1 le_infI2) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

161 
show "a \<sqinter> b = b \<sqinter> a" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

162 
by (rule antisym) auto 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

163 
show "a \<sqinter> a = a" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

164 
by (rule antisym) auto 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

165 
qed 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

166 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

167 
context semilattice_inf 
21733  168 
begin 
169 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

170 
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

171 
by (fact inf.assoc) 
21733  172 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

173 
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

174 
by (fact inf.commute) 
21733  175 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

176 
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

177 
by (fact inf.left_commute) 
21733  178 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

179 
lemma inf_idem: "x \<sqinter> x = x" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

180 
by (fact inf.idem) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

181 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

182 
lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

183 
by (fact inf.left_idem) 
21733  184 

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

185 
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" 
32064  186 
by (rule antisym) auto 
21733  187 

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

188 
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" 
32064  189 
by (rule antisym) auto 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

190 

32064  191 
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem 
21733  192 

193 
end 

194 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

195 
sublocale semilattice_sup < sup!: semilattice sup 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

196 
proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

197 
fix a b c 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

198 
show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

199 
by (rule antisym) (auto intro: le_supI1 le_supI2) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

200 
show "a \<squnion> b = b \<squnion> a" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

201 
by (rule antisym) auto 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

202 
show "a \<squnion> a = a" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

203 
by (rule antisym) auto 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

204 
qed 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

205 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

206 
context semilattice_sup 
21733  207 
begin 
21249  208 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

209 
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

210 
by (fact sup.assoc) 
21733  211 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

212 
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

213 
by (fact sup.commute) 
21733  214 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

215 
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

216 
by (fact sup.left_commute) 
21733  217 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

218 
lemma sup_idem: "x \<squnion> x = x" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

219 
by (fact sup.idem) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

220 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

221 
lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

222 
by (fact sup.left_idem) 
21733  223 

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

224 
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" 
32064  225 
by (rule antisym) auto 
21733  226 

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

227 
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" 
32064  228 
by (rule antisym) auto 
21249  229 

32064  230 
lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem 
21733  231 

232 
end 

21249  233 

21733  234 
context lattice 
235 
begin 

236 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

237 
lemma dual_lattice: 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

238 
"class.lattice (op \<ge>) (op >) sup inf" 
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

239 
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

240 
(unfold_locales, auto) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

241 

21733  242 
lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

243 
by (blast intro: antisym inf_le1 inf_greatest sup_ge1) 
21733  244 

245 
lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x" 

25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

246 
by (blast intro: antisym sup_ge1 sup_least inf_le1) 
21733  247 

32064  248 
lemmas inf_sup_aci = inf_aci sup_aci 
21734  249 

22454  250 
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 
251 

21734  252 
text{* Towards distributivity *} 
21249  253 

21734  254 
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
32064  255 
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) 
21734  256 

257 
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)" 

32064  258 
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) 
21734  259 

260 
text{* If you have one of them, you have them all. *} 

21249  261 

21733  262 
lemma distrib_imp1: 
21249  263 
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 
264 
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 

265 
proof 

266 
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb) 

34209  267 
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc) 
21249  268 
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" 
269 
by(simp add:inf_sup_absorb inf_commute) 

270 
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D) 

271 
finally show ?thesis . 

272 
qed 

273 

21733  274 
lemma distrib_imp2: 
21249  275 
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
276 
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 

277 
proof 

278 
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb) 

34209  279 
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc) 
21249  280 
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" 
281 
by(simp add:sup_inf_absorb sup_commute) 

282 
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D) 

283 
finally show ?thesis . 

284 
qed 

285 

21733  286 
end 
21249  287 

32568  288 
subsubsection {* Strict order *} 
289 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

290 
context semilattice_inf 
32568  291 
begin 
292 

293 
lemma less_infI1: 

294 
"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

295 
by (auto simp add: less_le inf_absorb1 intro: le_infI1) 
32568  296 

297 
lemma less_infI2: 

298 
"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

299 
by (auto simp add: less_le inf_absorb2 intro: le_infI2) 
32568  300 

301 
end 

302 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

303 
context semilattice_sup 
32568  304 
begin 
305 

306 
lemma less_supI1: 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

307 
"x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b" 
32568  308 
proof  
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

309 
interpret dual: semilattice_inf "op \<ge>" "op >" sup 
32568  310 
by (fact dual_semilattice) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

311 
assume "x \<sqsubset> a" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

312 
then show "x \<sqsubset> a \<squnion> b" 
32568  313 
by (fact dual.less_infI1) 
314 
qed 

315 

316 
lemma less_supI2: 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

317 
"x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b" 
32568  318 
proof  
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

319 
interpret dual: semilattice_inf "op \<ge>" "op >" sup 
32568  320 
by (fact dual_semilattice) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

321 
assume "x \<sqsubset> b" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

322 
then show "x \<sqsubset> a \<squnion> b" 
32568  323 
by (fact dual.less_infI2) 
324 
qed 

325 

326 
end 

327 

21249  328 

24164  329 
subsection {* Distributive lattices *} 
21249  330 

22454  331 
class distrib_lattice = lattice + 
21249  332 
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
333 

21733  334 
context distrib_lattice 
335 
begin 

336 

337 
lemma sup_inf_distrib2: 

21249  338 
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" 
32064  339 
by(simp add: inf_sup_aci sup_inf_distrib1) 
21249  340 

21733  341 
lemma inf_sup_distrib1: 
21249  342 
"x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 
343 
by(rule distrib_imp2[OF sup_inf_distrib1]) 

344 

21733  345 
lemma inf_sup_distrib2: 
21249  346 
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" 
32064  347 
by(simp add: inf_sup_aci inf_sup_distrib1) 
21249  348 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

349 
lemma dual_distrib_lattice: 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

350 
"class.distrib_lattice (op \<ge>) (op >) sup inf" 
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

351 
by (rule class.distrib_lattice.intro, rule dual_lattice) 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

352 
(unfold_locales, fact inf_sup_distrib1) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

353 

36008  354 
lemmas sup_inf_distrib = 
355 
sup_inf_distrib1 sup_inf_distrib2 

356 

357 
lemmas inf_sup_distrib = 

358 
inf_sup_distrib1 inf_sup_distrib2 

359 

21733  360 
lemmas distrib = 
21249  361 
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 
362 

21733  363 
end 
364 

21249  365 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

366 
subsection {* Bounded lattices and boolean algebras *} 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

367 

36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

368 
class bounded_lattice_bot = lattice + bot 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

369 
begin 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

370 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

371 
lemma inf_bot_left [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

372 
"\<bottom> \<sqinter> x = \<bottom>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

373 
by (rule inf_absorb1) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

374 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

375 
lemma inf_bot_right [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

376 
"x \<sqinter> \<bottom> = \<bottom>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

377 
by (rule inf_absorb2) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

378 

36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

379 
lemma sup_bot_left [simp]: 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

380 
"\<bottom> \<squnion> x = x" 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

381 
by (rule sup_absorb2) simp 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

382 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

383 
lemma sup_bot_right [simp]: 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

384 
"x \<squnion> \<bottom> = x" 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

385 
by (rule sup_absorb1) simp 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

386 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

387 
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

388 
"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

389 
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

390 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

391 
end 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

392 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

393 
class bounded_lattice_top = lattice + top 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

394 
begin 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

395 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

396 
lemma sup_top_left [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

397 
"\<top> \<squnion> x = \<top>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

398 
by (rule sup_absorb1) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

399 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

400 
lemma sup_top_right [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

401 
"x \<squnion> \<top> = \<top>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

402 
by (rule sup_absorb2) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

403 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

404 
lemma inf_top_left [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

405 
"\<top> \<sqinter> x = x" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

406 
by (rule inf_absorb2) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

407 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

408 
lemma inf_top_right [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

409 
"x \<sqinter> \<top> = x" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

410 
by (rule inf_absorb1) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

411 

36008  412 
lemma inf_eq_top_iff [simp]: 
413 
"x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>" 

414 
by (simp add: eq_iff) 

32568  415 

36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

416 
end 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

417 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

418 
class bounded_lattice = bounded_lattice_bot + bounded_lattice_top 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

419 
begin 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

420 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

421 
lemma dual_bounded_lattice: 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

422 
"class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>" 
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

423 
by unfold_locales (auto simp add: less_le_not_le) 
32568  424 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

425 
end 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

426 

aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

427 
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

428 
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

429 
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

430 
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

431 
begin 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

432 

aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

433 
lemma dual_boolean_algebra: 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

434 
"class.boolean_algebra (\<lambda>x y. x \<squnion>  y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>" 
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

435 
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

436 
(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

437 

aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

438 
lemma compl_inf_bot: 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

439 
" x \<sqinter> x = \<bottom>" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

440 
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

441 

aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

442 
lemma compl_sup_top: 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

443 
" x \<squnion> x = \<top>" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

444 
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

445 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

446 
lemma compl_unique: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

447 
assumes "x \<sqinter> y = \<bottom>" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

448 
and "x \<squnion> y = \<top>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

449 
shows " x = y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

450 
proof  
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

451 
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

452 
using inf_compl_bot assms(1) by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

453 
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

454 
by (simp add: inf_commute) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

455 
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

456 
by (simp add: inf_sup_distrib1) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

457 
then have " x \<sqinter> \<top> = y \<sqinter> \<top>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

458 
using sup_compl_top assms(2) by simp 
34209  459 
then show " x = y" by simp 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

460 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

461 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

462 
lemma double_compl [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

463 
" ( x) = x" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

464 
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

465 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

466 
lemma compl_eq_compl_iff [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

467 
" x =  y \<longleftrightarrow> x = y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

468 
proof 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

469 
assume " x =  y" 
36008  470 
then have " ( x) =  ( y)" by (rule arg_cong) 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

471 
then show "x = y" by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

472 
next 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

473 
assume "x = y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

474 
then show " x =  y" by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

475 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

476 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

477 
lemma compl_bot_eq [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

478 
" \<bottom> = \<top>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

479 
proof  
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

480 
from sup_compl_top have "\<bottom> \<squnion>  \<bottom> = \<top>" . 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

481 
then show ?thesis by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

482 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

483 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

484 
lemma compl_top_eq [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

485 
" \<top> = \<bottom>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

486 
proof  
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

487 
from inf_compl_bot have "\<top> \<sqinter>  \<top> = \<bottom>" . 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

488 
then show ?thesis by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

489 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

490 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

491 
lemma compl_inf [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

492 
" (x \<sqinter> y) =  x \<squnion>  y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

493 
proof (rule compl_unique) 
36008  494 
have "(x \<sqinter> y) \<sqinter> ( x \<squnion>  y) = (y \<sqinter> (x \<sqinter>  x)) \<squnion> (x \<sqinter> (y \<sqinter>  y))" 
495 
by (simp only: inf_sup_distrib inf_aci) 

496 
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

497 
by (simp add: inf_compl_bot) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

498 
next 
36008  499 
have "(x \<sqinter> y) \<squnion> ( x \<squnion>  y) = ( y \<squnion> (x \<squnion>  x)) \<sqinter> ( x \<squnion> (y \<squnion>  y))" 
500 
by (simp only: sup_inf_distrib sup_aci) 

501 
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

502 
by (simp add: sup_compl_top) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

503 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

504 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

505 
lemma compl_sup [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

506 
" (x \<squnion> y) =  x \<sqinter>  y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

507 
proof  
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

508 
interpret boolean_algebra "\<lambda>x y. x \<squnion>  y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom> 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

509 
by (rule dual_boolean_algebra) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

510 
then show ?thesis by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

511 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

512 

36008  513 
lemma compl_mono: 
514 
"x \<sqsubseteq> y \<Longrightarrow>  y \<sqsubseteq>  x" 

515 
proof  

516 
assume "x \<sqsubseteq> y" 

517 
then have "x \<squnion> y = y" by (simp only: le_iff_sup) 

518 
then have " (x \<squnion> y) =  y" by simp 

519 
then have " x \<sqinter>  y =  y" by simp 

520 
then have " y \<sqinter>  x =  y" by (simp only: inf_commute) 

521 
then show " y \<sqsubseteq>  x" by (simp only: le_iff_inf) 

522 
qed 

523 

524 
lemma compl_le_compl_iff: (* TODO: declare [simp] ? *) 

525 
" x \<le>  y \<longleftrightarrow> y \<le> x" 

526 
by (auto dest: compl_mono) 

527 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

528 
end 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

529 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

530 

22454  531 
subsection {* Uniqueness of inf and sup *} 
532 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

533 
lemma (in semilattice_inf) inf_unique: 
22454  534 
fixes f (infixl "\<triangle>" 70) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

535 
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

536 
and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" 
22737  537 
shows "x \<sqinter> y = x \<triangle> y" 
22454  538 
proof (rule antisym) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

539 
show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2) 
22454  540 
next 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

541 
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

542 
show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all 
22454  543 
qed 
544 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

545 
lemma (in semilattice_sup) sup_unique: 
22454  546 
fixes f (infixl "\<nabla>" 70) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

547 
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

548 
and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x" 
22737  549 
shows "x \<squnion> y = x \<nabla> y" 
22454  550 
proof (rule antisym) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

551 
show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2) 
22454  552 
next 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

553 
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

554 
show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all 
22454  555 
qed 
36008  556 

22454  557 

22916  558 
subsection {* @{const min}/@{const max} on linear orders as 
559 
special case of @{const inf}/@{const sup} *} 

560 

32512  561 
sublocale linorder < min_max!: distrib_lattice less_eq less min max 
28823  562 
proof 
22916  563 
fix x y z 
32512  564 
show "max x (min y z) = min (max x y) (max x z)" 
565 
by (auto simp add: min_def max_def) 

22916  566 
qed (auto simp add: min_def max_def not_le less_imp_le) 
21249  567 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

568 
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

569 
by (rule ext)+ (auto intro: antisym) 
21733  570 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

571 
lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

572 
by (rule ext)+ (auto intro: antisym) 
21733  573 

21249  574 
lemmas le_maxI1 = min_max.sup_ge1 
575 
lemmas le_maxI2 = min_max.sup_ge2 

21381  576 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

577 
lemmas min_ac = min_max.inf_assoc min_max.inf_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

578 
min_max.inf.left_commute 
21249  579 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

580 
lemmas max_ac = min_max.sup_assoc min_max.sup_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

581 
min_max.sup.left_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

582 

21249  583 

22454  584 

585 
subsection {* Bool as lattice *} 

586 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

587 
instantiation bool :: boolean_algebra 
25510  588 
begin 
589 

590 
definition 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

591 
bool_Compl_def: "uminus = Not" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

592 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

593 
definition 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

594 
bool_diff_def: "A  B \<longleftrightarrow> A \<and> \<not> B" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

595 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

596 
definition 
25510  597 
inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" 
598 

599 
definition 

600 
sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" 

601 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

602 
instance proof 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

603 
qed (simp_all add: inf_bool_eq sup_bool_eq le_bool_def 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

604 
bot_bool_eq top_bool_eq bool_Compl_def bool_diff_def, auto) 
22454  605 

25510  606 
end 
607 

32781  608 
lemma sup_boolI1: 
609 
"P \<Longrightarrow> P \<squnion> Q" 

610 
by (simp add: sup_bool_eq) 

611 

612 
lemma sup_boolI2: 

613 
"Q \<Longrightarrow> P \<squnion> Q" 

614 
by (simp add: sup_bool_eq) 

615 

616 
lemma sup_boolE: 

617 
"P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" 

618 
by (auto simp add: sup_bool_eq) 

619 

23878  620 

621 
subsection {* Fun as lattice *} 

622 

25510  623 
instantiation "fun" :: (type, lattice) lattice 
624 
begin 

625 

626 
definition 

28562  627 
inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" 
25510  628 

629 
definition 

28562  630 
sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" 
25510  631 

32780  632 
instance proof 
633 
qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq) 

23878  634 

25510  635 
end 
23878  636 

637 
instance "fun" :: (type, distrib_lattice) distrib_lattice 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

638 
proof 
32780  639 
qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1) 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

640 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

641 
instance "fun" :: (type, bounded_lattice) bounded_lattice .. 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

642 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

643 
instantiation "fun" :: (type, uminus) uminus 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

644 
begin 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

645 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

646 
definition 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

647 
fun_Compl_def: " A = (\<lambda>x.  A x)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

648 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

649 
instance .. 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

650 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

651 
end 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

652 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

653 
instantiation "fun" :: (type, minus) minus 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

654 
begin 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

655 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

656 
definition 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

657 
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

658 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

659 
instance .. 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

660 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

661 
end 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

662 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

663 
instance "fun" :: (type, boolean_algebra) boolean_algebra 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

664 
proof 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

665 
qed (simp_all add: inf_fun_eq sup_fun_eq bot_fun_eq top_fun_eq fun_Compl_def fun_diff_def 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

666 
inf_compl_bot sup_compl_top diff_eq) 
23878  667 

26794  668 

25062  669 
no_notation 
25382  670 
less_eq (infix "\<sqsubseteq>" 50) and 
671 
less (infix "\<sqsubset>" 50) and 

672 
inf (infixl "\<sqinter>" 70) and 

32568  673 
sup (infixl "\<squnion>" 65) and 
674 
top ("\<top>") and 

675 
bot ("\<bottom>") 

25062  676 

21249  677 
end 