author  wenzelm 
Wed, 17 Jun 2015 11:03:05 +0200  
changeset 60500  903bb1495239 
parent 56796  9f84219715a7 
child 60679  ade12ef2773c 
permissions  rwrr 
56796  1 
(* Title: HOL/Library/Finite_Lattice.thy 
2 
Author: Alessandro Coglio 

3 
*) 

50634  4 

5 
theory Finite_Lattice 

51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
50634
diff
changeset

6 
imports Product_Order 
50634  7 
begin 
8 

60500  9 
text \<open>A nonempty finite lattice is a complete lattice. 
50634  10 
Since types are never empty in Isabelle/HOL, 
11 
a type of classes @{class finite} and @{class lattice} 

12 
should also have class @{class complete_lattice}. 

13 
A type class is defined 

14 
that extends classes @{class finite} and @{class lattice} 

15 
with the operators @{const bot}, @{const top}, @{const Inf}, and @{const Sup}, 

16 
along with assumptions that define these operators 

17 
in terms of the ones of classes @{class finite} and @{class lattice}. 

60500  18 
The resulting class is a subclass of @{class complete_lattice}.\<close> 
50634  19 

20 
class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup + 

56796  21 
assumes bot_def: "bot = Inf_fin UNIV" 
22 
assumes top_def: "top = Sup_fin UNIV" 

23 
assumes Inf_def: "Inf A = Finite_Set.fold inf top A" 

24 
assumes Sup_def: "Sup A = Finite_Set.fold sup bot A" 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

25 

60500  26 
text \<open>The definitional assumptions 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

27 
on the operators @{const bot} and @{const top} 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

28 
of class @{class finite_lattice_complete} 
60500  29 
ensure that they yield bottom and top.\<close> 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

30 

56796  31 
lemma finite_lattice_complete_bot_least: "(bot::'a::finite_lattice_complete) \<le> x" 
32 
by (auto simp: bot_def intro: Inf_fin.coboundedI) 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

33 

412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

34 
instance finite_lattice_complete \<subseteq> order_bot 
56796  35 
by default (auto simp: finite_lattice_complete_bot_least) 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

36 

56796  37 
lemma finite_lattice_complete_top_greatest: "(top::'a::finite_lattice_complete) \<ge> x" 
38 
by (auto simp: top_def Sup_fin.coboundedI) 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

39 

412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

40 
instance finite_lattice_complete \<subseteq> order_top 
56796  41 
by default (auto simp: finite_lattice_complete_top_greatest) 
50634  42 

43 
instance finite_lattice_complete \<subseteq> bounded_lattice .. 

44 

60500  45 
text \<open>The definitional assumptions 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

46 
on the operators @{const Inf} and @{const Sup} 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

47 
of class @{class finite_lattice_complete} 
60500  48 
ensure that they yield infimum and supremum.\<close> 
50634  49 

56796  50 
lemma finite_lattice_complete_Inf_empty: "Inf {} = (top :: 'a::finite_lattice_complete)" 
51489  51 
by (simp add: Inf_def) 
52 

56796  53 
lemma finite_lattice_complete_Sup_empty: "Sup {} = (bot :: 'a::finite_lattice_complete)" 
51489  54 
by (simp add: Sup_def) 
55 

56 
lemma finite_lattice_complete_Inf_insert: 

57 
fixes A :: "'a::finite_lattice_complete set" 

58 
shows "Inf (insert x A) = inf x (Inf A)" 

59 
proof  

56796  60 
interpret comp_fun_idem "inf :: 'a \<Rightarrow> _" 
61 
by (fact comp_fun_idem_inf) 

51489  62 
show ?thesis by (simp add: Inf_def) 
63 
qed 

64 

65 
lemma finite_lattice_complete_Sup_insert: 

66 
fixes A :: "'a::finite_lattice_complete set" 

67 
shows "Sup (insert x A) = sup x (Sup A)" 

68 
proof  

56796  69 
interpret comp_fun_idem "sup :: 'a \<Rightarrow> _" 
70 
by (fact comp_fun_idem_sup) 

51489  71 
show ?thesis by (simp add: Sup_def) 
72 
qed 

73 

50634  74 
lemma finite_lattice_complete_Inf_lower: 
75 
"(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x" 

56796  76 
using finite [of A] 
77 
by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2) 

50634  78 

79 
lemma finite_lattice_complete_Inf_greatest: 

80 
"\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A" 

56796  81 
using finite [of A] 
82 
by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert) 

50634  83 

84 
lemma finite_lattice_complete_Sup_upper: 

85 
"(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x" 

56796  86 
using finite [of A] 
87 
by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2) 

50634  88 

89 
lemma finite_lattice_complete_Sup_least: 

90 
"\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A" 

56796  91 
using finite [of A] 
92 
by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert) 

50634  93 

94 
instance finite_lattice_complete \<subseteq> complete_lattice 

95 
proof 

96 
qed (auto simp: 

56796  97 
finite_lattice_complete_Inf_lower 
98 
finite_lattice_complete_Inf_greatest 

99 
finite_lattice_complete_Sup_upper 

100 
finite_lattice_complete_Sup_least 

101 
finite_lattice_complete_Inf_empty 

102 
finite_lattice_complete_Sup_empty) 

50634  103 

60500  104 
text \<open>The product of two finite lattices is already a finite lattice.\<close> 
50634  105 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

106 
lemma finite_bot_prod: 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

107 
"(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) = 
56796  108 
Inf_fin UNIV" 
109 
by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV) 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

110 

412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

111 
lemma finite_top_prod: 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

112 
"(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) = 
56796  113 
Sup_fin UNIV" 
114 
by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV) 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

115 

50634  116 
lemma finite_Inf_prod: 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

117 
"Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) = 
56796  118 
Finite_Set.fold inf top A" 
119 
by (metis Inf_fold_inf finite_code) 

50634  120 

121 
lemma finite_Sup_prod: 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

122 
"Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) = 
56796  123 
Finite_Set.fold sup bot A" 
124 
by (metis Sup_fold_sup finite_code) 

50634  125 

56796  126 
instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete 
127 
by default (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod) 

50634  128 

60500  129 
text \<open>Functions with a finite domain and with a finite lattice as codomain 
130 
already form a finite lattice.\<close> 

50634  131 

56796  132 
lemma finite_bot_fun: "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV" 
133 
by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code) 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

134 

56796  135 
lemma finite_top_fun: "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV" 
136 
by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code) 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

137 

50634  138 
lemma finite_Inf_fun: 
139 
"Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) = 

56796  140 
Finite_Set.fold inf top A" 
141 
by (metis Inf_fold_inf finite_code) 

50634  142 

143 
lemma finite_Sup_fun: 

144 
"Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) = 

56796  145 
Finite_Set.fold sup bot A" 
146 
by (metis Sup_fold_sup finite_code) 

50634  147 

148 
instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete 

56796  149 
by default (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun) 
50634  150 

151 

60500  152 
subsection \<open>Finite Distributive Lattices\<close> 
50634  153 

60500  154 
text \<open>A finite distributive lattice is a complete lattice 
50634  155 
whose @{const inf} and @{const sup} operators 
60500  156 
distribute over @{const Sup} and @{const Inf}.\<close> 
50634  157 

158 
class finite_distrib_lattice_complete = 

159 
distrib_lattice + finite_lattice_complete 

160 

161 
lemma finite_distrib_lattice_complete_sup_Inf: 

162 
"sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)" 

56796  163 
using finite 
164 
by (induct A rule: finite_induct) (simp_all add: sup_inf_distrib1) 

50634  165 

166 
lemma finite_distrib_lattice_complete_inf_Sup: 

167 
"inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)" 

56796  168 
apply (rule finite_induct) 
169 
apply (metis finite_code) 

170 
apply (metis SUP_empty Sup_empty inf_bot_right) 

171 
apply (metis SUP_insert Sup_insert inf_sup_distrib1) 

172 
done 

50634  173 

174 
instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice 

175 
proof 

176 
qed (auto simp: 

56796  177 
finite_distrib_lattice_complete_sup_Inf 
178 
finite_distrib_lattice_complete_inf_Sup) 

50634  179 

60500  180 
text \<open>The product of two finite distributive lattices 
181 
is already a finite distributive lattice.\<close> 

50634  182 

183 
instance prod :: 

184 
(finite_distrib_lattice_complete, finite_distrib_lattice_complete) 

185 
finite_distrib_lattice_complete 

56796  186 
.. 
50634  187 

60500  188 
text \<open>Functions with a finite domain 
50634  189 
and with a finite distributive lattice as codomain 
60500  190 
already form a finite distributive lattice.\<close> 
50634  191 

192 
instance "fun" :: 

193 
(finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete 

56796  194 
.. 
50634  195 

196 

60500  197 
subsection \<open>Linear Orders\<close> 
50634  198 

60500  199 
text \<open>A linear order is a distributive lattice. 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

200 
A type class is defined 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

201 
that extends class @{class linorder} 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

202 
with the operators @{const inf} and @{const sup}, 
50634  203 
along with assumptions that define these operators 
204 
in terms of the ones of class @{class linorder}. 

60500  205 
The resulting class is a subclass of @{class distrib_lattice}.\<close> 
50634  206 

207 
class linorder_lattice = linorder + inf + sup + 

56796  208 
assumes inf_def: "inf x y = (if x \<le> y then x else y)" 
209 
assumes sup_def: "sup x y = (if x \<ge> y then x else y)" 

50634  210 

60500  211 
text \<open>The definitional assumptions 
50634  212 
on the operators @{const inf} and @{const sup} 
213 
of class @{class linorder_lattice} 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

214 
ensure that they yield infimum and supremum 
60500  215 
and that they distribute over each other.\<close> 
50634  216 

217 
lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x" 

56796  218 
unfolding inf_def by (metis (full_types) linorder_linear) 
50634  219 

220 
lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y" 

56796  221 
unfolding inf_def by (metis (full_types) linorder_linear) 
50634  222 

223 
lemma linorder_lattice_inf_greatest: 

224 
"(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z" 

56796  225 
unfolding inf_def by (metis (full_types)) 
50634  226 

227 
lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x" 

56796  228 
unfolding sup_def by (metis (full_types) linorder_linear) 
50634  229 

230 
lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y" 

56796  231 
unfolding sup_def by (metis (full_types) linorder_linear) 
50634  232 

233 
lemma linorder_lattice_sup_least: 

234 
"(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z" 

56796  235 
by (auto simp: sup_def) 
50634  236 

237 
lemma linorder_lattice_sup_inf_distrib1: 

238 
"sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)" 

56796  239 
by (auto simp: inf_def sup_def) 
240 

50634  241 
instance linorder_lattice \<subseteq> distrib_lattice 
56796  242 
proof 
50634  243 
qed (auto simp: 
56796  244 
linorder_lattice_inf_le1 
245 
linorder_lattice_inf_le2 

246 
linorder_lattice_inf_greatest 

247 
linorder_lattice_sup_ge1 

248 
linorder_lattice_sup_ge2 

249 
linorder_lattice_sup_least 

250 
linorder_lattice_sup_inf_distrib1) 

50634  251 

252 

60500  253 
subsection \<open>Finite Linear Orders\<close> 
50634  254 

60500  255 
text \<open>A (nonempty) finite linear order is a complete linear order.\<close> 
50634  256 

257 
class finite_linorder_complete = linorder_lattice + finite_lattice_complete 

258 

259 
instance finite_linorder_complete \<subseteq> complete_linorder .. 

260 

60500  261 
text \<open>A (nonempty) finite linear order is a complete lattice 
50634  262 
whose @{const inf} and @{const sup} operators 
60500  263 
distribute over @{const Sup} and @{const Inf}.\<close> 
50634  264 

265 
instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete .. 

266 

267 
end 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51489
diff
changeset

268 