author  haftmann 
Sun, 17 Jul 2011 22:24:08 +0200  
changeset 43873  8a2f339641c1 
parent 43753  fe5e846c0839 
child 44085  a65e26f1427b 
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 
41082  51 
bot ("\<bottom>") and 
52 
top ("\<top>") 

53 

25206  54 

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

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

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

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

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

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

68 
text {* Dual lattice *} 

69 

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

70 
lemma dual_semilattice: 
43753  71 
"class.semilattice_inf greater_eq greater sup" 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

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

75 
end 

21249  76 

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

77 
class lattice = semilattice_inf + semilattice_sup 
21249  78 

25382  79 

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

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

82 
context semilattice_inf 
21733  83 
begin 
21249  84 

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

87 
by (rule order_trans) auto 

21249  88 

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

91 
by (rule order_trans) auto 

21733  92 

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

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

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

21733  102 

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

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

21249  106 

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

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

111 
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

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

25206  115 
end 
21733  116 

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

117 
context semilattice_sup 
21733  118 
begin 
21249  119 

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

25062  122 
by (rule order_trans) auto 
21249  123 

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

25062  126 
by (rule order_trans) auto 
21733  127 

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

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

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

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

135 

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

138 
by (blast intro: le_supI elim: le_supE) 

21733  139 

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

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

21734  143 

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

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

148 
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

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

25206  152 
end 
23878  153 

21733  154 

32064  155 
subsubsection {* Equational laws *} 
21249  156 

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

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

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

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

160 
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

161 
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

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

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

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

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

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

167 

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

168 
context semilattice_inf 
21733  169 
begin 
170 

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

171 
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

172 
by (fact inf.assoc) 
21733  173 

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

174 
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

175 
by (fact inf.commute) 
21733  176 

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

177 
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

178 
by (fact inf.left_commute) 
21733  179 

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

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

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

182 

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

183 
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

184 
by (fact inf.left_idem) 
21733  185 

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

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

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

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

191 

32064  192 
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem 
21733  193 

194 
end 

195 

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

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

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

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

199 
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

200 
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

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

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

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

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

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

206 

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

207 
context semilattice_sup 
21733  208 
begin 
21249  209 

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

210 
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

211 
by (fact sup.assoc) 
21733  212 

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

213 
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

214 
by (fact sup.commute) 
21733  215 

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

216 
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

217 
by (fact sup.left_commute) 
21733  218 

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

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

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

221 

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

222 
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

223 
by (fact sup.left_idem) 
21733  224 

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

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

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

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

32064  231 
lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem 
21733  232 

233 
end 

21249  234 

21733  235 
context lattice 
236 
begin 

237 

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

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

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

240 
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

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

242 

21733  243 
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

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

246 
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

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

32064  249 
lemmas inf_sup_aci = inf_aci sup_aci 
21734  250 

22454  251 
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 
252 

21734  253 
text{* Towards distributivity *} 
21249  254 

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

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

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

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

21249  262 

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

266 
proof 

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

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

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

272 
finally show ?thesis . 

273 
qed 

274 

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

278 
proof 

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

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

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

284 
finally show ?thesis . 

285 
qed 

286 

21733  287 
end 
21249  288 

32568  289 
subsubsection {* Strict order *} 
290 

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

291 
context semilattice_inf 
32568  292 
begin 
293 

294 
lemma less_infI1: 

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

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

298 
lemma less_infI2: 

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

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

302 
end 

303 

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

304 
context semilattice_sup 
32568  305 
begin 
306 

307 
lemma less_supI1: 

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

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

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

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

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

316 

317 
lemma less_supI2: 

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

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

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

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

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

326 

327 
end 

328 

21249  329 

24164  330 
subsection {* Distributive lattices *} 
21249  331 

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

21733  335 
context distrib_lattice 
336 
begin 

337 

338 
lemma sup_inf_distrib2: 

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

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

345 

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

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

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

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

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

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

354 

36008  355 
lemmas sup_inf_distrib = 
356 
sup_inf_distrib1 sup_inf_distrib2 

357 

358 
lemmas inf_sup_distrib = 

359 
inf_sup_distrib1 inf_sup_distrib2 

360 

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

21733  364 
end 
365 

21249  366 

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

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

368 

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

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

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

371 

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

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

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

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

375 

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

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

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

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

379 

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

380 
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

381 
"\<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

382 
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

383 

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

384 
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

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

386 
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

387 

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

388 
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

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

390 
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

391 

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

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

393 

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

394 
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

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

396 

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

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

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

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

400 

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

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

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

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

404 

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

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

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

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

408 

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

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

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

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

412 

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

415 
by (simp add: eq_iff) 

32568  416 

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

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

418 

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

419 
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

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

421 

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

422 
lemma dual_bounded_lattice: 
43753  423 
"class.bounded_lattice greater_eq greater sup 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

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

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

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

427 

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

428 
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

429 
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

430 
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

431 
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

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

433 

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

434 
lemma dual_boolean_algebra: 
43753  435 
"class.boolean_algebra (\<lambda>x y. x \<squnion>  y) uminus greater_eq greater sup inf \<top> \<bottom>" 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

436 
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

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

438 

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

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

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

441 
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

442 

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

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

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

445 
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

446 

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

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

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

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

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

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

452 
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

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

454 
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

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

456 
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

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

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

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

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

462 

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

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

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

465 
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

466 

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

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

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

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

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

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

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

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

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

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

477 

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

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

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

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

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

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

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

484 

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

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

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

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

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

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

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

491 

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

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

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

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

497 
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

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

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

502 
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

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

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

505 

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

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

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

508 
proof  
43753  509 
interpret boolean_algebra "\<lambda>x y. x \<squnion>  y" uminus greater_eq greater sup inf \<top> \<bottom> 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

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

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

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

513 

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

516 
proof  

517 
assume "x \<sqsubseteq> y" 

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

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

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

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

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

523 
qed 

524 

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

43753  526 
" x \<sqsubseteq>  y \<longleftrightarrow> y \<sqsubseteq> x" 
43873  527 
by (auto dest: compl_mono) 
528 

529 
lemma compl_le_swap1: 

530 
assumes "y \<sqsubseteq>  x" shows "x \<sqsubseteq> y" 

531 
proof  

532 
from assms have " ( x) \<sqsubseteq>  y" by (simp only: compl_le_compl_iff) 

533 
then show ?thesis by simp 

534 
qed 

535 

536 
lemma compl_le_swap2: 

537 
assumes " y \<sqsubseteq> x" shows " x \<sqsubseteq> y" 

538 
proof  

539 
from assms have " x \<sqsubseteq>  ( y)" by (simp only: compl_le_compl_iff) 

540 
then show ?thesis by simp 

541 
qed 

542 

543 
lemma compl_less_compl_iff: (* TODO: declare [simp] ? *) 

544 
" x \<sqsubset>  y \<longleftrightarrow> y \<sqsubset> x" 

545 
by (auto simp add: less_le compl_le_compl_iff) 

546 

547 
lemma compl_less_swap1: 

548 
assumes "y \<sqsubset>  x" shows "x \<sqsubset>  y" 

549 
proof  

550 
from assms have " ( x) \<sqsubset>  y" by (simp only: compl_less_compl_iff) 

551 
then show ?thesis by simp 

552 
qed 

553 

554 
lemma compl_less_swap2: 

555 
assumes " y \<sqsubset> x" shows " x \<sqsubset> y" 

556 
proof  

557 
from assms have " x \<sqsubset>  ( y)" by (simp only: compl_less_compl_iff) 

558 
then show ?thesis by simp 

559 
qed 

36008  560 

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

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

562 

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

563 

22454  564 
subsection {* Uniqueness of inf and sup *} 
565 

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

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

568 
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

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

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

574 
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

575 
show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all 
22454  576 
qed 
577 

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

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

580 
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

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

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

586 
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

587 
show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all 
22454  588 
qed 
36008  589 

22454  590 

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

593 

32512  594 
sublocale linorder < min_max!: distrib_lattice less_eq less min max 
28823  595 
proof 
22916  596 
fix x y z 
32512  597 
show "max x (min y z) = min (max x y) (max x z)" 
598 
by (auto simp add: min_def max_def) 

22916  599 
qed (auto simp add: min_def max_def not_le less_imp_le) 
21249  600 

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

601 
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

602 
by (rule ext)+ (auto intro: antisym) 
21733  603 

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

604 
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

605 
by (rule ext)+ (auto intro: antisym) 
21733  606 

21249  607 
lemmas le_maxI1 = min_max.sup_ge1 
608 
lemmas le_maxI2 = min_max.sup_ge2 

21381  609 

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

610 
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

611 
min_max.inf.left_commute 
21249  612 

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

613 
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

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

615 

21249  616 

22454  617 
subsection {* Bool as lattice *} 
618 

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

619 
instantiation bool :: boolean_algebra 
25510  620 
begin 
621 

622 
definition 

41080  623 
bool_Compl_def [simp]: "uminus = Not" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

624 

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

625 
definition 
41080  626 
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

627 

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

628 
definition 
41080  629 
[simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" 
25510  630 

631 
definition 

41080  632 
[simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" 
25510  633 

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

634 
instance proof 
41080  635 
qed auto 
22454  636 

25510  637 
end 
638 

32781  639 
lemma sup_boolI1: 
640 
"P \<Longrightarrow> P \<squnion> Q" 

41080  641 
by simp 
32781  642 

643 
lemma sup_boolI2: 

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

41080  645 
by simp 
32781  646 

647 
lemma sup_boolE: 

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

41080  649 
by auto 
32781  650 

23878  651 

652 
subsection {* Fun as lattice *} 

653 

25510  654 
instantiation "fun" :: (type, lattice) lattice 
655 
begin 

656 

657 
definition 

41080  658 
"f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" 
659 

660 
lemma inf_apply: 

661 
"(f \<sqinter> g) x = f x \<sqinter> g x" 

662 
by (simp add: inf_fun_def) 

25510  663 

664 
definition 

41080  665 
"f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" 
666 

667 
lemma sup_apply: 

668 
"(f \<squnion> g) x = f x \<squnion> g x" 

669 
by (simp add: sup_fun_def) 

25510  670 

32780  671 
instance proof 
41080  672 
qed (simp_all add: le_fun_def inf_apply sup_apply) 
23878  673 

25510  674 
end 
23878  675 

41080  676 
instance "fun" :: (type, distrib_lattice) distrib_lattice proof 
677 
qed (rule ext, simp add: sup_inf_distrib1 inf_apply sup_apply) 

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

678 

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

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

680 

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

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

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

683 

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

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

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

686 

41080  687 
lemma uminus_apply: 
688 
"( A) x =  (A x)" 

689 
by (simp add: fun_Compl_def) 

690 

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

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

692 

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

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

694 

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

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

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

697 

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

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

699 
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

700 

41080  701 
lemma minus_apply: 
702 
"(A  B) x = A x  B x" 

703 
by (simp add: fun_diff_def) 

704 

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

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

706 

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

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

708 

41080  709 
instance "fun" :: (type, boolean_algebra) boolean_algebra proof 
710 
qed (rule ext, simp_all add: inf_apply sup_apply bot_apply top_apply uminus_apply minus_apply inf_compl_bot sup_compl_top diff_eq)+ 

26794  711 

25062  712 
no_notation 
25382  713 
less_eq (infix "\<sqsubseteq>" 50) and 
714 
less (infix "\<sqsubset>" 50) and 

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

32568  716 
sup (infixl "\<squnion>" 65) and 
717 
top ("\<top>") and 

718 
bot ("\<bottom>") 

25062  719 

21249  720 
end 