author  haftmann 
Mon, 08 Jun 2009 08:38:50 +0200  
changeset 31482  7288382fd549 
parent 31464  b2aca38301c4 
child 31596  c96d7e5df659 
permissions  rwrr 
31482  1 
(* Author: Florian Haftmann, TU Muenchen 
26348  2 
*) 
3 

4 
header {* Finite types as explicit enumerations *} 

5 

6 
theory Enum 

30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
29961
diff
changeset

7 
imports Map Main 
26348  8 
begin 
9 

10 
subsection {* Class @{text enum} *} 

11 

29797  12 
class enum = 
26348  13 
fixes enum :: "'a list" 
28562  14 
assumes UNIV_enum [code]: "UNIV = set enum" 
26444  15 
and enum_distinct: "distinct enum" 
26348  16 
begin 
17 

29797  18 
subclass finite proof 
19 
qed (simp add: UNIV_enum) 

26444  20 

21 
lemma enum_all: "set enum = UNIV" unfolding UNIV_enum .. 

22 

26348  23 
lemma in_enum [intro]: "x \<in> set enum" 
24 
unfolding enum_all by auto 

25 

26 
lemma enum_eq_I: 

27 
assumes "\<And>x. x \<in> set xs" 

28 
shows "set enum = set xs" 

29 
proof  

30 
from assms UNIV_eq_I have "UNIV = set xs" by auto 

31 
with enum_all show ?thesis by simp 

32 
qed 

33 

34 
end 

35 

36 

37 
subsection {* Equality and order on functions *} 

38 

26513  39 
instantiation "fun" :: (enum, eq) eq 
40 
begin 

26348  41 

26513  42 
definition 
26732  43 
"eq_class.eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)" 
26513  44 

31464  45 
instance proof 
46 
qed (simp_all add: eq_fun_def enum_all expand_fun_eq) 

26513  47 

48 
end 

26348  49 

28562  50 
lemma order_fun [code]: 
26348  51 
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order" 
26968  52 
shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum" 
53 
and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum" 

28684  54 
by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def order_less_le) 
26968  55 

56 

57 
subsection {* Quantifiers *} 

58 

28562  59 
lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum" 
26968  60 
by (simp add: list_all_iff enum_all) 
61 

28562  62 
lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum" 
26968  63 
by (simp add: list_all_iff enum_all) 
26348  64 

65 

66 
subsection {* Default instances *} 

67 

26444  68 
primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where 
69 
"n_lists 0 xs = [[]]" 

70 
 "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))" 

71 

72 
lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])" 

73 
by (induct n) simp_all 

74 

75 
lemma length_n_lists: "length (n_lists n xs) = length xs ^ n" 

76 
by (induct n) (auto simp add: length_concat map_compose [symmetric] o_def listsum_triv) 

77 

78 
lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n" 

79 
by (induct n arbitrary: ys) auto 

80 

81 
lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}" 

82 
proof (rule set_ext) 

83 
fix ys :: "'a list" 

84 
show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}" 

85 
proof  

86 
have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n" 

87 
by (induct n arbitrary: ys) auto 

88 
moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs" 

89 
by (induct n arbitrary: ys) auto 

90 
moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)" 

91 
by (induct ys) auto 

92 
ultimately show ?thesis by auto 

93 
qed 

94 
qed 

95 

96 
lemma distinct_n_lists: 

97 
assumes "distinct xs" 

98 
shows "distinct (n_lists n xs)" 

99 
proof (rule card_distinct) 

100 
from assms have card_length: "card (set xs) = length xs" by (rule distinct_card) 

101 
have "card (set (n_lists n xs)) = card (set xs) ^ n" 

102 
proof (induct n) 

103 
case 0 then show ?case by simp 

104 
next 

105 
case (Suc n) 

106 
moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs) 

107 
= (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))" 

108 
by (rule card_UN_disjoint) auto 

109 
moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)" 

110 
by (rule card_image) (simp add: inj_on_def) 

111 
ultimately show ?case by auto 

112 
qed 

113 
also have "\<dots> = length xs ^ n" by (simp add: card_length) 

114 
finally show "card (set (n_lists n xs)) = length (n_lists n xs)" 

115 
by (simp add: length_n_lists) 

116 
qed 

117 

31193  118 
lemma map_of_zip_map: (*FIXME move to Map.thy*) 
119 
"map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)" 

26444  120 
by (induct xs) (simp_all add: expand_fun_eq) 
121 

122 
lemma map_of_zip_enum_is_Some: 

123 
assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)" 

124 
shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y" 

125 
proof  

126 
from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow> 

127 
(\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)" 

128 
by (auto intro!: map_of_zip_is_Some) 

129 
then show ?thesis using enum_all by auto 

130 
qed 

131 

132 
lemma map_of_zip_enum_inject: 

133 
fixes xs ys :: "'b\<Colon>enum list" 

134 
assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)" 

135 
"length ys = length (enum \<Colon> 'a\<Colon>enum list)" 

136 
and map_of: "the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys)" 

137 
shows "xs = ys" 

138 
proof  

139 
have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)" 

140 
proof 

141 
fix x :: 'a 

142 
from length map_of_zip_enum_is_Some obtain y1 y2 

143 
where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1" 

144 
and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast 

145 
moreover from map_of have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)" 

146 
by (auto dest: fun_cong) 

147 
ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x" 

148 
by simp 

149 
qed 

150 
with length enum_distinct show "xs = ys" by (rule map_of_zip_inject) 

151 
qed 

152 

153 
instantiation "fun" :: (enum, enum) enum 

154 
begin 

155 

156 
definition 

28562  157 
[code del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)" 
26444  158 

159 
instance proof 

160 
show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)" 

161 
proof (rule UNIV_eq_I) 

162 
fix f :: "'a \<Rightarrow> 'b" 

163 
have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))" 

164 
by (auto simp add: map_of_zip_map expand_fun_eq) 

165 
then show "f \<in> set enum" 

166 
by (auto simp add: enum_fun_def set_n_lists) 

167 
qed 

168 
next 

169 
from map_of_zip_enum_inject 

170 
show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)" 

171 
by (auto intro!: inj_onI simp add: enum_fun_def 

172 
distinct_map distinct_n_lists enum_distinct set_n_lists enum_all) 

173 
qed 

174 

175 
end 

176 

28562  177 
lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list) 
28245
9767dd8e1e54
celver code lemma avoid type ambiguity problem with Haskell
haftmann
parents:
27487
diff
changeset

178 
in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))" 
9767dd8e1e54
celver code lemma avoid type ambiguity problem with Haskell
haftmann
parents:
27487
diff
changeset

179 
by (simp add: enum_fun_def Let_def) 
26444  180 

26348  181 
instantiation unit :: enum 
182 
begin 

183 

184 
definition 

185 
"enum = [()]" 

186 

31464  187 
instance proof 
188 
qed (simp_all add: enum_unit_def UNIV_unit) 

26348  189 

190 
end 

191 

192 
instantiation bool :: enum 

193 
begin 

194 

195 
definition 

196 
"enum = [False, True]" 

197 

31464  198 
instance proof 
199 
qed (simp_all add: enum_bool_def UNIV_bool) 

26348  200 

201 
end 

202 

203 
primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where 

204 
"product [] _ = []" 

205 
 "product (x#xs) ys = map (Pair x) ys @ product xs ys" 

206 

207 
lemma product_list_set: 

208 
"set (product xs ys) = set xs \<times> set ys" 

209 
by (induct xs) auto 

210 

26444  211 
lemma distinct_product: 
212 
assumes "distinct xs" and "distinct ys" 

213 
shows "distinct (product xs ys)" 

214 
using assms by (induct xs) 

215 
(auto intro: inj_onI simp add: product_list_set distinct_map) 

216 

26348  217 
instantiation * :: (enum, enum) enum 
218 
begin 

219 

220 
definition 

221 
"enum = product enum enum" 

222 

223 
instance by default 

26444  224 
(simp_all add: enum_prod_def product_list_set distinct_product enum_all enum_distinct) 
26348  225 

226 
end 

227 

228 
instantiation "+" :: (enum, enum) enum 

229 
begin 

230 

231 
definition 

232 
"enum = map Inl enum @ map Inr enum" 

233 

234 
instance by default 

26444  235 
(auto simp add: enum_all enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct) 
26348  236 

237 
end 

238 

239 
primrec sublists :: "'a list \<Rightarrow> 'a list list" where 

240 
"sublists [] = [[]]" 

241 
 "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" 

242 

26444  243 
lemma length_sublists: 
244 
"length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs" 

245 
by (induct xs) (simp_all add: Let_def) 

246 

26348  247 
lemma sublists_powset: 
26444  248 
"set ` set (sublists xs) = Pow (set xs)" 
26348  249 
proof  
250 
have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A" 

251 
by (auto simp add: image_def) 

26444  252 
have "set (map set (sublists xs)) = Pow (set xs)" 
26348  253 
by (induct xs) 
26444  254 
(simp_all add: aux Let_def Pow_insert Un_commute) 
255 
then show ?thesis by simp 

256 
qed 

257 

258 
lemma distinct_set_sublists: 

259 
assumes "distinct xs" 

260 
shows "distinct (map set (sublists xs))" 

261 
proof (rule card_distinct) 

262 
have "finite (set xs)" by rule 

263 
then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow) 

264 
with assms distinct_card [of xs] 

265 
have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp 

266 
then show "card (set (map set (sublists xs))) = length (map set (sublists xs))" 

267 
by (simp add: sublists_powset length_sublists) 

26348  268 
qed 
269 

270 
instantiation nibble :: enum 

271 
begin 

272 

273 
definition 

274 
"enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7, 

275 
Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]" 

276 

31464  277 
instance proof 
278 
qed (simp_all add: enum_nibble_def UNIV_nibble) 

26348  279 

280 
end 

281 

282 
instantiation char :: enum 

283 
begin 

284 

285 
definition 

28562  286 
[code del]: "enum = map (split Char) (product enum enum)" 
26444  287 

31482  288 
lemma enum_chars [code]: 
289 
"enum = chars" 

290 
unfolding enum_char_def chars_def enum_nibble_def by simp 

26348  291 

31464  292 
instance proof 
293 
qed (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric] 

294 
distinct_map distinct_product enum_distinct) 

26348  295 

296 
end 

297 

29024  298 
instantiation option :: (enum) enum 
299 
begin 

300 

301 
definition 

302 
"enum = None # map Some enum" 

303 

31464  304 
instance proof 
305 
qed (auto simp add: enum_all enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct) 

29024  306 

307 
end 

308 

309 
end 