author  haftmann 
Fri, 30 Nov 2007 20:13:03 +0100  
changeset 25510  38c15efe603b 
parent 25482  4ed49eccb1eb 
child 26014  00c2c3525bef 
permissions  rwrr 
21249  1 
(* Title: HOL/Lattices.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
*) 

5 

22454  6 
header {* Abstract lattices *} 
21249  7 

8 
theory Lattices 

9 
imports Orderings 

10 
begin 

11 

12 
subsection{* Lattices *} 

13 

25206  14 
notation 
25382  15 
less_eq (infix "\<sqsubseteq>" 50) and 
16 
less (infix "\<sqsubset>" 50) 

25206  17 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

18 
class lower_semilattice = order + 
21249  19 
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) 
22737  20 
assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" 
21 
and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" 

21733  22 
and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" 
21249  23 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

24 
class upper_semilattice = order + 
21249  25 
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) 
22737  26 
assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" 
27 
and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" 

21733  28 
and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x" 
21249  29 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

30 
class lattice = lower_semilattice + upper_semilattice 
21249  31 

25382  32 

21733  33 
subsubsection{* Intro and elim rules*} 
34 

35 
context lower_semilattice 

36 
begin 

21249  37 

25062  38 
lemma le_infI1[intro]: 
39 
assumes "a \<sqsubseteq> x" 

40 
shows "a \<sqinter> b \<sqsubseteq> x" 

41 
proof (rule order_trans) 

25482  42 
from assms show "a \<sqsubseteq> x" . 
43 
show "a \<sqinter> b \<sqsubseteq> a" by simp 

25062  44 
qed 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

45 
lemmas (in ) [rule del] = le_infI1 
21249  46 

25062  47 
lemma le_infI2[intro]: 
48 
assumes "b \<sqsubseteq> x" 

49 
shows "a \<sqinter> b \<sqsubseteq> x" 

50 
proof (rule order_trans) 

25482  51 
from assms show "b \<sqsubseteq> x" . 
52 
show "a \<sqinter> b \<sqsubseteq> b" by simp 

25062  53 
qed 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

54 
lemmas (in ) [rule del] = le_infI2 
21733  55 

21734  56 
lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b" 
21733  57 
by(blast intro: inf_greatest) 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

58 
lemmas (in ) [rule del] = le_infI 
21249  59 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

60 
lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

61 
by (blast intro: order_trans) 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

62 
lemmas (in ) [rule del] = le_infE 
21249  63 

21734  64 
lemma le_inf_iff [simp]: 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

65 
"x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)" 
21733  66 
by blast 
67 

21734  68 
lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

69 
by (blast intro: antisym dest: eq_iff [THEN iffD1]) 
21249  70 

25206  71 
lemma mono_inf: 
72 
fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice" 

73 
shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" 

74 
by (auto simp add: mono_def intro: Lattices.inf_greatest) 

21733  75 

25206  76 
end 
21733  77 

78 
context upper_semilattice 

79 
begin 

21249  80 

21734  81 
lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" 
25062  82 
by (rule order_trans) auto 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

83 
lemmas (in ) [rule del] = le_supI1 
21249  84 

21734  85 
lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" 
25062  86 
by (rule order_trans) auto 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

87 
lemmas (in ) [rule del] = le_supI2 
21733  88 

21734  89 
lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x" 
21733  90 
by(blast intro: sup_least) 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

91 
lemmas (in ) [rule del] = le_supI 
21249  92 

21734  93 
lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

94 
by (blast intro: order_trans) 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

95 
lemmas (in ) [rule del] = le_supE 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

96 

21734  97 
lemma ge_sup_conv[simp]: 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

98 
"x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)" 
21733  99 
by blast 
100 

21734  101 
lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

102 
by (blast intro: antisym dest: eq_iff [THEN iffD1]) 
21734  103 

25206  104 
lemma mono_sup: 
105 
fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice" 

106 
shows "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" 

107 
by (auto simp add: mono_def intro: Lattices.sup_least) 

21733  108 

25206  109 
end 
23878  110 

21733  111 

112 
subsubsection{* Equational laws *} 

21249  113 

21733  114 
context lower_semilattice 
115 
begin 

116 

117 
lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" 

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

118 
by (blast intro: antisym) 
21733  119 

120 
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" 

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

121 
by (blast intro: antisym) 
21733  122 

123 
lemma inf_idem[simp]: "x \<sqinter> x = x" 

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

124 
by (blast intro: antisym) 
21733  125 

126 
lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" 

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

127 
by (blast intro: antisym) 
21733  128 

129 
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" 

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

130 
by (blast intro: antisym) 
21733  131 

132 
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" 

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

133 
by (blast intro: antisym) 
21733  134 

135 
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" 

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

136 
by (blast intro: antisym) 
21733  137 

138 
lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem 

139 

140 
end 

141 

142 

143 
context upper_semilattice 

144 
begin 

21249  145 

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

147 
by (blast intro: antisym) 
21733  148 

149 
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" 

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

150 
by (blast intro: antisym) 
21733  151 

152 
lemma sup_idem[simp]: "x \<squnion> x = x" 

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

153 
by (blast intro: antisym) 
21733  154 

155 
lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" 

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

156 
by (blast intro: antisym) 
21733  157 

158 
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" 

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

159 
by (blast intro: antisym) 
21733  160 

161 
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" 

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

162 
by (blast intro: antisym) 
21249  163 

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

165 
by (blast intro: antisym) 
21733  166 

167 
lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem 

168 

169 
end 

21249  170 

21733  171 
context lattice 
172 
begin 

173 

174 
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

175 
by (blast intro: antisym inf_le1 inf_greatest sup_ge1) 
21733  176 

177 
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

178 
by (blast intro: antisym sup_ge1 sup_least inf_le1) 
21733  179 

21734  180 
lemmas ACI = inf_ACI sup_ACI 
181 

22454  182 
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 
183 

21734  184 
text{* Towards distributivity *} 
21249  185 

21734  186 
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

187 
by blast 
21734  188 

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

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

190 
by blast 
21734  191 

192 

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

21249  194 

21733  195 
lemma distrib_imp1: 
21249  196 
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 
197 
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 

198 
proof 

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

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

201 
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" 

202 
by(simp add:inf_sup_absorb inf_commute) 

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

204 
finally show ?thesis . 

205 
qed 

206 

21733  207 
lemma distrib_imp2: 
21249  208 
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
209 
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 

210 
proof 

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

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

213 
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" 

214 
by(simp add:sup_inf_absorb sup_commute) 

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

216 
finally show ?thesis . 

217 
qed 

218 

21734  219 
(* seems unused *) 
220 
lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z" 

221 
by blast 

222 

21733  223 
end 
21249  224 

225 

24164  226 
subsection {* Distributive lattices *} 
21249  227 

22454  228 
class distrib_lattice = lattice + 
21249  229 
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
230 

21733  231 
context distrib_lattice 
232 
begin 

233 

234 
lemma sup_inf_distrib2: 

21249  235 
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" 
236 
by(simp add:ACI sup_inf_distrib1) 

237 

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

241 

21733  242 
lemma inf_sup_distrib2: 
21249  243 
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" 
244 
by(simp add:ACI inf_sup_distrib1) 

245 

21733  246 
lemmas distrib = 
21249  247 
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 
248 

21733  249 
end 
250 

21249  251 

22454  252 
subsection {* Uniqueness of inf and sup *} 
253 

22737  254 
lemma (in lower_semilattice) inf_unique: 
22454  255 
fixes f (infixl "\<triangle>" 70) 
25062  256 
assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y" 
257 
and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" 

22737  258 
shows "x \<sqinter> y = x \<triangle> y" 
22454  259 
proof (rule antisym) 
25062  260 
show "x \<triangle> y \<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2) 
22454  261 
next 
25062  262 
have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest) 
263 
show "x \<sqinter> y \<le> x \<triangle> y" by (rule leI) simp_all 

22454  264 
qed 
265 

22737  266 
lemma (in upper_semilattice) sup_unique: 
22454  267 
fixes f (infixl "\<nabla>" 70) 
25062  268 
assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y" 
269 
and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x" 

22737  270 
shows "x \<squnion> y = x \<nabla> y" 
22454  271 
proof (rule antisym) 
25062  272 
show "x \<squnion> y \<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2) 
22454  273 
next 
25062  274 
have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least) 
275 
show "x \<nabla> y \<le> x \<squnion> y" by (rule leI) simp_all 

22454  276 
qed 
277 

278 

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

281 

282 
lemma (in linorder) distrib_lattice_min_max: 

25062  283 
"distrib_lattice (op \<le>) (op <) min max" 
22916  284 
proof unfold_locales 
25062  285 
have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" 
22916  286 
by (auto simp add: less_le antisym) 
287 
fix x y z 

288 
show "max x (min y z) = min (max x y) (max x z)" 

289 
unfolding min_def max_def 

24640
85a6c200ecd3
Simplified proofs due to transitivity reasoner setup.
ballarin
parents:
24514
diff
changeset

290 
by auto 
22916  291 
qed (auto simp add: min_def max_def not_le less_imp_le) 
21249  292 

293 
interpretation min_max: 

22454  294 
distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max] 
23948  295 
by (rule distrib_lattice_min_max) 
21249  296 

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

298 
by (rule ext)+ (auto intro: antisym) 
21733  299 

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

301 
by (rule ext)+ (auto intro: antisym) 
21733  302 

21249  303 
lemmas le_maxI1 = min_max.sup_ge1 
304 
lemmas le_maxI2 = min_max.sup_ge2 

21381  305 

21249  306 
lemmas max_ac = min_max.sup_assoc min_max.sup_commute 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

307 
mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute] 
21249  308 

309 
lemmas min_ac = min_max.inf_assoc min_max.inf_commute 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

310 
mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute] 
21249  311 

22454  312 
text {* 
313 
Now we have inherited antisymmetry as an introrule on all 

314 
linear orders. This is a problem because it applies to bool, which is 

315 
undesirable. 

316 
*} 

317 

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

318 
lemmas [rule del] = min_max.le_infI min_max.le_supI 
22454  319 
min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2 
320 
min_max.le_infI1 min_max.le_infI2 

321 

322 

23878  323 
subsection {* Complete lattices *} 
324 

325 
class complete_lattice = lattice + 

326 
fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900) 

24345  327 
and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900) 
23878  328 
assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x" 
24345  329 
and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A" 
330 
assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A" 

331 
and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z" 

23878  332 
begin 
333 

25062  334 
lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

335 
by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) 
23878  336 

25062  337 
lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

338 
by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) 
23878  339 

340 
lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}" 

24345  341 
unfolding Sup_Inf by auto 
23878  342 

343 
lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}" 

344 
unfolding Inf_Sup by auto 

345 

346 
lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A" 

347 
apply (rule antisym) 

348 
apply (rule le_infI) 

349 
apply (rule Inf_lower) 

350 
apply simp 

351 
apply (rule Inf_greatest) 

352 
apply (rule Inf_lower) 

353 
apply simp 

354 
apply (rule Inf_greatest) 

355 
apply (erule insertE) 

356 
apply (rule le_infI1) 

357 
apply simp 

358 
apply (rule le_infI2) 

359 
apply (erule Inf_lower) 

360 
done 

361 

24345  362 
lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A" 
23878  363 
apply (rule antisym) 
364 
apply (rule Sup_least) 

365 
apply (erule insertE) 

366 
apply (rule le_supI1) 

367 
apply simp 

368 
apply (rule le_supI2) 

369 
apply (erule Sup_upper) 

370 
apply (rule le_supI) 

371 
apply (rule Sup_upper) 

372 
apply simp 

373 
apply (rule Sup_least) 

374 
apply (rule Sup_upper) 

375 
apply simp 

376 
done 

377 

378 
lemma Inf_singleton [simp]: 

379 
"\<Sqinter>{a} = a" 

380 
by (auto intro: antisym Inf_lower Inf_greatest) 

381 

24345  382 
lemma Sup_singleton [simp]: 
23878  383 
"\<Squnion>{a} = a" 
384 
by (auto intro: antisym Sup_upper Sup_least) 

385 

386 
lemma Inf_insert_simp: 

387 
"\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)" 

388 
by (cases "A = {}") (simp_all, simp add: Inf_insert) 

389 

390 
lemma Sup_insert_simp: 

391 
"\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)" 

392 
by (cases "A = {}") (simp_all, simp add: Sup_insert) 

393 

394 
lemma Inf_binary: 

395 
"\<Sqinter>{a, b} = a \<sqinter> b" 

396 
by (simp add: Inf_insert_simp) 

397 

398 
lemma Sup_binary: 

399 
"\<Squnion>{a, b} = a \<squnion> b" 

400 
by (simp add: Sup_insert_simp) 

401 

402 
definition 

25382  403 
top :: 'a where 
25206  404 
"top = \<Sqinter>{}" 
23878  405 

406 
definition 

25382  407 
bot :: 'a where 
25206  408 
"bot = \<Squnion>{}" 
23878  409 

25062  410 
lemma top_greatest [simp]: "x \<le> top" 
23878  411 
by (unfold top_def, rule Inf_greatest, simp) 
412 

25062  413 
lemma bot_least [simp]: "bot \<le> x" 
23878  414 
by (unfold bot_def, rule Sup_least, simp) 
415 

416 
definition 

24749  417 
SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" 
23878  418 
where 
25206  419 
"SUPR A f == \<Squnion> (f ` A)" 
23878  420 

421 
definition 

24749  422 
INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" 
23878  423 
where 
25206  424 
"INFI A f == \<Sqinter> (f ` A)" 
23878  425 

24749  426 
end 
427 

23878  428 
syntax 
429 
"_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10) 

430 
"_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10) 

431 
"_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10) 

432 
"_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10) 

433 

434 
translations 

435 
"SUP x y. B" == "SUP x. SUP y. B" 

436 
"SUP x. B" == "CONST SUPR UNIV (%x. B)" 

437 
"SUP x. B" == "SUP x:UNIV. B" 

438 
"SUP x:A. B" == "CONST SUPR A (%x. B)" 

439 
"INF x y. B" == "INF x. INF y. B" 

440 
"INF x. B" == "CONST INFI UNIV (%x. B)" 

441 
"INF x. B" == "INF x:UNIV. B" 

442 
"INF x:A. B" == "CONST INFI A (%x. B)" 

443 

444 
(* To avoid etacontraction of body: *) 

445 
print_translation {* 

446 
let 

447 
fun btr' syn (A :: Abs abs :: ts) = 

448 
let val (x,t) = atomic_abs_tr' abs 

449 
in list_comb (Syntax.const syn $ x $ A $ t, ts) end 

450 
val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const 

451 
in 

452 
[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")] 

453 
end 

454 
*} 

455 

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

456 
context complete_lattice 
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

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

458 

23878  459 
lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)" 
460 
by (auto simp add: SUPR_def intro: Sup_upper) 

461 

462 
lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u" 

463 
by (auto simp add: SUPR_def intro: Sup_least) 

464 

465 
lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i" 

466 
by (auto simp add: INFI_def intro: Inf_lower) 

467 

468 
lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)" 

469 
by (auto simp add: INFI_def intro: Inf_greatest) 

470 

471 
lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M" 

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

472 
by (auto intro: antisym SUP_leI le_SUPI) 
23878  473 

474 
lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M" 

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

475 
by (auto intro: antisym INF_leI le_INFI) 
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

476 

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

477 
end 
23878  478 

479 

22454  480 
subsection {* Bool as lattice *} 
481 

25510  482 
instantiation bool :: distrib_lattice 
483 
begin 

484 

485 
definition 

486 
inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" 

487 

488 
definition 

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

490 

491 
instance 

22454  492 
by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def) 
493 

25510  494 
end 
495 

496 
instantiation bool :: complete_lattice 

497 
begin 

498 

499 
definition 

500 
Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)" 

501 

502 
definition 

503 
Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)" 

504 

505 
instance 

24345  506 
by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def) 
23878  507 

25510  508 
end 
509 

23878  510 
lemma Inf_empty_bool [simp]: 
25206  511 
"\<Sqinter>{}" 
23878  512 
unfolding Inf_bool_def by auto 
513 

514 
lemma not_Sup_empty_bool [simp]: 

515 
"\<not> Sup {}" 

24345  516 
unfolding Sup_bool_def by auto 
23878  517 

518 
lemma top_bool_eq: "top = True" 

519 
by (iprover intro!: order_antisym le_boolI top_greatest) 

520 

521 
lemma bot_bool_eq: "bot = False" 

522 
by (iprover intro!: order_antisym le_boolI bot_least) 

523 

524 

525 
subsection {* Set as lattice *} 

526 

25510  527 
instantiation set :: (type) distrib_lattice 
528 
begin 

529 

530 
definition 

531 
inf_set_eq [code func del]: "A \<sqinter> B = A \<inter> B" 

532 

533 
definition 

534 
sup_set_eq [code func del]: "A \<squnion> B = A \<union> B" 

535 

536 
instance 

23878  537 
by intro_classes (auto simp add: inf_set_eq sup_set_eq) 
538 

25510  539 
end 
23878  540 

24514
540eaf87e42d
mono_Int/Un: proper proof, avoid illegal schematic type vars;
wenzelm
parents:
24345
diff
changeset

541 
lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B" 
540eaf87e42d
mono_Int/Un: proper proof, avoid illegal schematic type vars;
wenzelm
parents:
24345
diff
changeset

542 
apply (fold inf_set_eq sup_set_eq) 
540eaf87e42d
mono_Int/Un: proper proof, avoid illegal schematic type vars;
wenzelm
parents:
24345
diff
changeset

543 
apply (erule mono_inf) 
540eaf87e42d
mono_Int/Un: proper proof, avoid illegal schematic type vars;
wenzelm
parents:
24345
diff
changeset

544 
done 
23878  545 

24514
540eaf87e42d
mono_Int/Un: proper proof, avoid illegal schematic type vars;
wenzelm
parents:
24345
diff
changeset

546 
lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)" 
540eaf87e42d
mono_Int/Un: proper proof, avoid illegal schematic type vars;
wenzelm
parents:
24345
diff
changeset

547 
apply (fold inf_set_eq sup_set_eq) 
540eaf87e42d
mono_Int/Un: proper proof, avoid illegal schematic type vars;
wenzelm
parents:
24345
diff
changeset

548 
apply (erule mono_sup) 
540eaf87e42d
mono_Int/Un: proper proof, avoid illegal schematic type vars;
wenzelm
parents:
24345
diff
changeset

549 
done 
23878  550 

25510  551 
instantiation set :: (type) complete_lattice 
552 
begin 

553 

554 
definition 

555 
Inf_set_def [code func del]: "\<Sqinter>S \<equiv> \<Inter>S" 

556 

557 
definition 

558 
Sup_set_def [code func del]: "\<Squnion>S \<equiv> \<Union>S" 

559 

560 
instance 

24345  561 
by intro_classes (auto simp add: Inf_set_def Sup_set_def) 
23878  562 

25510  563 
end 
23878  564 

565 
lemma top_set_eq: "top = UNIV" 

566 
by (iprover intro!: subset_antisym subset_UNIV top_greatest) 

567 

568 
lemma bot_set_eq: "bot = {}" 

569 
by (iprover intro!: subset_antisym empty_subsetI bot_least) 

570 

571 

572 
subsection {* Fun as lattice *} 

573 

25510  574 
instantiation "fun" :: (type, lattice) lattice 
575 
begin 

576 

577 
definition 

578 
inf_fun_eq [code func del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" 

579 

580 
definition 

581 
sup_fun_eq [code func del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" 

582 

583 
instance 

23878  584 
apply intro_classes 
585 
unfolding inf_fun_eq sup_fun_eq 

586 
apply (auto intro: le_funI) 

587 
apply (rule le_funI) 

588 
apply (auto dest: le_funD) 

589 
apply (rule le_funI) 

590 
apply (auto dest: le_funD) 

591 
done 

592 

25510  593 
end 
23878  594 

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

596 
by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1) 

597 

25510  598 
instantiation "fun" :: (type, complete_lattice) complete_lattice 
599 
begin 

600 

601 
definition 

602 
Inf_fun_def [code func del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})" 

603 

604 
definition 

605 
Sup_fun_def [code func del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})" 

606 

607 
instance 

24345  608 
by intro_classes 
609 
(auto simp add: Inf_fun_def Sup_fun_def le_fun_def 

610 
intro: Inf_lower Sup_upper Inf_greatest Sup_least) 

23878  611 

25510  612 
end 
23878  613 

614 
lemma Inf_empty_fun: 

25206  615 
"\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})" 
23878  616 
by rule (auto simp add: Inf_fun_def) 
617 

618 
lemma Sup_empty_fun: 

25206  619 
"\<Squnion>{} = (\<lambda>_. \<Squnion>{})" 
24345  620 
by rule (auto simp add: Sup_fun_def) 
23878  621 

622 
lemma top_fun_eq: "top = (\<lambda>x. top)" 

623 
by (iprover intro!: order_antisym le_funI top_greatest) 

624 

625 
lemma bot_fun_eq: "bot = (\<lambda>x. bot)" 

626 
by (iprover intro!: order_antisym le_funI bot_least) 

627 

628 

629 
text {* redundant bindings *} 

22454  630 

631 
lemmas inf_aci = inf_ACI 

632 
lemmas sup_aci = sup_ACI 

633 

25062  634 
no_notation 
25382  635 
less_eq (infix "\<sqsubseteq>" 50) and 
636 
less (infix "\<sqsubset>" 50) and 

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

638 
sup (infixl "\<squnion>" 65) and 

639 
Inf ("\<Sqinter>_" [900] 900) and 

640 
Sup ("\<Squnion>_" [900] 900) 

25062  641 

21249  642 
end 