author  haftmann 
Thu, 05 Mar 2009 08:23:09 +0100  
changeset 30302  5ffa9d4dbea7 
parent 29580  117b88da143c 
child 30729  461ee3e49ad3 
permissions  rwrr 
21249  1 
(* Title: HOL/Lattices.thy 
2 
Author: Tobias Nipkow 

3 
*) 

4 

22454  5 
header {* Abstract lattices *} 
21249  6 

7 
theory Lattices 

30302  8 
imports Orderings 
21249  9 
begin 
10 

28562  11 
subsection {* Lattices *} 
21249  12 

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

25206  16 

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

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

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

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

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

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

30 
text {* Dual lattice *} 

31 

32 
lemma dual_lattice: 

33 
"lower_semilattice (op \<ge>) (op >) sup" 

27682  34 
by (rule lower_semilattice.intro, rule dual_order) 
35 
(unfold_locales, simp_all add: sup_least) 

26014  36 

37 
end 

21249  38 

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

39 
class lattice = lower_semilattice + upper_semilattice 
21249  40 

25382  41 

28562  42 
subsubsection {* Intro and elim rules*} 
21733  43 

44 
context lower_semilattice 

45 
begin 

21249  46 

25062  47 
lemma le_infI1[intro]: 
48 
assumes "a \<sqsubseteq> x" 

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

50 
proof (rule order_trans) 

25482  51 
from assms show "a \<sqsubseteq> x" . 
52 
show "a \<sqinter> b \<sqsubseteq> a" 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_infI1 
21249  55 

25062  56 
lemma le_infI2[intro]: 
57 
assumes "b \<sqsubseteq> x" 

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

59 
proof (rule order_trans) 

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

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

63 
lemmas (in ) [rule del] = le_infI2 
21733  64 

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

67 
lemmas (in ) [rule del] = le_infI 
21249  68 

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

69 
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

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

71 
lemmas (in ) [rule del] = le_infE 
21249  72 

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

74 
"x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)" 
21733  75 
by blast 
76 

21734  77 
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

78 
by (blast intro: antisym dest: eq_iff [THEN iffD1]) 
21249  79 

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

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

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

21733  84 

25206  85 
end 
21733  86 

87 
context upper_semilattice 

88 
begin 

21249  89 

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

92 
lemmas (in ) [rule del] = le_supI1 
21249  93 

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

96 
lemmas (in ) [rule del] = le_supI2 
21733  97 

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

100 
lemmas (in ) [rule del] = le_supI 
21249  101 

21734  102 
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

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

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

105 

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

107 
"x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)" 
21733  108 
by blast 
109 

21734  110 
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

111 
by (blast intro: antisym dest: eq_iff [THEN iffD1]) 
21734  112 

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

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

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

21733  117 

25206  118 
end 
23878  119 

21733  120 

121 
subsubsection{* Equational laws *} 

21249  122 

21733  123 
context lower_semilattice 
124 
begin 

125 

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

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_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

130 
by (blast intro: antisym) 
21733  131 

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

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_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

136 
by (blast intro: antisym) 
21733  137 

138 
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

139 
by (blast intro: antisym) 
21733  140 

141 
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

142 
by (blast intro: antisym) 
21733  143 

144 
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

145 
by (blast intro: antisym) 
21733  146 

147 
lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem 

148 

149 
end 

150 

151 

152 
context upper_semilattice 

153 
begin 

21249  154 

21733  155 
lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)" 
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_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

159 
by (blast intro: antisym) 
21733  160 

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

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

162 
by (blast intro: antisym) 
21733  163 

164 
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

165 
by (blast intro: antisym) 
21733  166 

167 
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

168 
by (blast intro: antisym) 
21733  169 

170 
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

171 
by (blast intro: antisym) 
21249  172 

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

174 
by (blast intro: antisym) 
21733  175 

176 
lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem 

177 

178 
end 

21249  179 

21733  180 
context lattice 
181 
begin 

182 

183 
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

184 
by (blast intro: antisym inf_le1 inf_greatest sup_ge1) 
21733  185 

186 
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

187 
by (blast intro: antisym sup_ge1 sup_least inf_le1) 
21733  188 

21734  189 
lemmas ACI = inf_ACI sup_ACI 
190 

22454  191 
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 
192 

21734  193 
text{* Towards distributivity *} 
21249  194 

21734  195 
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

196 
by blast 
21734  197 

198 
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

199 
by blast 
21734  200 

201 

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

21249  203 

21733  204 
lemma distrib_imp1: 
21249  205 
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 
206 
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 

207 
proof 

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

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

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

211 
by(simp add:inf_sup_absorb inf_commute) 

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

213 
finally show ?thesis . 

214 
qed 

215 

21733  216 
lemma distrib_imp2: 
21249  217 
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
218 
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 

219 
proof 

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

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

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

223 
by(simp add:sup_inf_absorb sup_commute) 

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

225 
finally show ?thesis . 

226 
qed 

227 

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

230 
by blast 

231 

21733  232 
end 
21249  233 

234 

24164  235 
subsection {* Distributive lattices *} 
21249  236 

22454  237 
class distrib_lattice = lattice + 
21249  238 
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
239 

21733  240 
context distrib_lattice 
241 
begin 

242 

243 
lemma sup_inf_distrib2: 

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

246 

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

250 

21733  251 
lemma inf_sup_distrib2: 
21249  252 
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" 
253 
by(simp add:ACI inf_sup_distrib1) 

254 

21733  255 
lemmas distrib = 
21249  256 
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 
257 

21733  258 
end 
259 

21249  260 

22454  261 
subsection {* Uniqueness of inf and sup *} 
262 

22737  263 
lemma (in lower_semilattice) inf_unique: 
22454  264 
fixes f (infixl "\<triangle>" 70) 
25062  265 
assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y" 
266 
and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" 

22737  267 
shows "x \<sqinter> y = x \<triangle> y" 
22454  268 
proof (rule antisym) 
25062  269 
show "x \<triangle> y \<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2) 
22454  270 
next 
25062  271 
have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest) 
272 
show "x \<sqinter> y \<le> x \<triangle> y" by (rule leI) simp_all 

22454  273 
qed 
274 

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

22737  279 
shows "x \<squnion> y = x \<nabla> y" 
22454  280 
proof (rule antisym) 
25062  281 
show "x \<squnion> y \<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2) 
22454  282 
next 
25062  283 
have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least) 
284 
show "x \<nabla> y \<le> x \<squnion> y" by (rule leI) simp_all 

22454  285 
qed 
286 

287 

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

290 

291 
lemma (in linorder) distrib_lattice_min_max: 

25062  292 
"distrib_lattice (op \<le>) (op <) min max" 
28823  293 
proof 
25062  294 
have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" 
22916  295 
by (auto simp add: less_le antisym) 
296 
fix x y z 

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

298 
unfolding min_def max_def 

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

299 
by auto 
22916  300 
qed (auto simp add: min_def max_def not_le less_imp_le) 
21249  301 

29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29223
diff
changeset

302 
interpretation min_max!: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max 
23948  303 
by (rule distrib_lattice_min_max) 
21249  304 

22454  305 
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

306 
by (rule ext)+ (auto intro: antisym) 
21733  307 

22454  308 
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

309 
by (rule ext)+ (auto intro: antisym) 
21733  310 

21249  311 
lemmas le_maxI1 = min_max.sup_ge1 
312 
lemmas le_maxI2 = min_max.sup_ge2 

21381  313 

21249  314 
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

315 
mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute] 
21249  316 

317 
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

318 
mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute] 
21249  319 

22454  320 
text {* 
321 
Now we have inherited antisymmetry as an introrule on all 

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

323 
undesirable. 

324 
*} 

325 

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

326 
lemmas [rule del] = min_max.le_infI min_max.le_supI 
22454  327 
min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2 
328 
min_max.le_infI1 min_max.le_infI2 

329 

330 

331 
subsection {* Bool as lattice *} 

332 

25510  333 
instantiation bool :: distrib_lattice 
334 
begin 

335 

336 
definition 

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

338 

339 
definition 

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

341 

342 
instance 

22454  343 
by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def) 
344 

25510  345 
end 
346 

23878  347 

348 
subsection {* Fun as lattice *} 

349 

25510  350 
instantiation "fun" :: (type, lattice) lattice 
351 
begin 

352 

353 
definition 

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

356 
definition 

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

359 
instance 

23878  360 
apply intro_classes 
361 
unfolding inf_fun_eq sup_fun_eq 

362 
apply (auto intro: le_funI) 

363 
apply (rule le_funI) 

364 
apply (auto dest: le_funD) 

365 
apply (rule le_funI) 

366 
apply (auto dest: le_funD) 

367 
done 

368 

25510  369 
end 
23878  370 

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

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

373 

26794  374 

23878  375 
text {* redundant bindings *} 
22454  376 

377 
lemmas inf_aci = inf_ACI 

378 
lemmas sup_aci = sup_ACI 

379 

25062  380 
no_notation 
25382  381 
less_eq (infix "\<sqsubseteq>" 50) and 
382 
less (infix "\<sqsubset>" 50) and 

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

30302  384 
sup (infixl "\<squnion>" 65) 
25062  385 

21249  386 
end 