author  bulwahn 
Mon, 22 Nov 2010 11:34:58 +0100  
changeset 40652  7bdfc1d6b143 
parent 40651  9752ba7348b5 
child 40657  58a6ba7ccfc5 
permissions  rwrr 
31596  1 
(* Author: Florian Haftmann, TU Muenchen *) 
26348  2 

3 
header {* Finite types as explicit enumerations *} 

4 

5 
theory Enum 

40650
d40b347d5b0b
adding Enum to HOLMain image and removing it from HOLLibrary
bulwahn
parents:
40649
diff
changeset

6 
imports Map String 
26348  7 
begin 
8 

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

10 

29797  11 
class enum = 
26348  12 
fixes enum :: "'a list" 
33635  13 
assumes UNIV_enum: "UNIV = set enum" 
26444  14 
and enum_distinct: "distinct enum" 
26348  15 
begin 
16 

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

26444  19 

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

21 

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

24 

25 
lemma enum_eq_I: 

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

27 
shows "set enum = set xs" 

28 
proof  

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

30 
with enum_all show ?thesis by simp 

31 
qed 

32 

33 
end 

34 

35 

36 
subsection {* Equality and order on functions *} 

37 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

38 
instantiation "fun" :: (enum, equal) equal 
26513  39 
begin 
26348  40 

26513  41 
definition 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

42 
"HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)" 
26513  43 

31464  44 
instance proof 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

45 
qed (simp_all add: equal_fun_def enum_all fun_eq_iff) 
26513  46 

47 
end 

26348  48 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

49 
lemma [code nbe]: 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

50 
"HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

51 
by (fact equal_refl) 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

52 

40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

53 
lemma [code]: 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

54 
"HOL.equal f g \<longleftrightarrow> list_all (%x. f x = g x) enum" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

55 
by (auto simp add: list_all_iff enum_all equal fun_eq_iff) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

56 

28562  57 
lemma order_fun [code]: 
26348  58 
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order" 
26968  59 
shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum" 
37601  60 
and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

61 
by (simp_all add: list_all_iff list_ex_iff enum_all fun_eq_iff le_fun_def order_less_le) 
26968  62 

63 

64 
subsection {* Quantifiers *} 

65 

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

37601  69 
lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum" 
70 
by (simp add: list_ex_iff enum_all) 

26348  71 

40652  72 
lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum" 
73 
unfolding list_ex1_iff enum_all by auto 

74 

26348  75 

76 
subsection {* Default instances *} 

77 

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

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

81 

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

83 
by (induct n) simp_all 

84 

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

33639
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33635
diff
changeset

86 
by (induct n) (auto simp add: length_concat o_def listsum_triv) 
26444  87 

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

89 
by (induct n arbitrary: ys) auto 

90 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

92 
proof (rule set_eqI) 
26444  93 
fix ys :: "'a list" 
94 
show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}" 

95 
proof  

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

97 
by (induct n arbitrary: ys) auto 

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

99 
by (induct n arbitrary: ys) auto 

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

101 
by (induct ys) auto 

102 
ultimately show ?thesis by auto 

103 
qed 

104 
qed 

105 

106 
lemma distinct_n_lists: 

107 
assumes "distinct xs" 

108 
shows "distinct (n_lists n xs)" 

109 
proof (rule card_distinct) 

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

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

112 
proof (induct n) 

113 
case 0 then show ?case by simp 

114 
next 

115 
case (Suc n) 

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

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

118 
by (rule card_UN_disjoint) auto 

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

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

121 
ultimately show ?case by auto 

122 
qed 

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

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

125 
by (simp add: length_n_lists) 

126 
qed 

127 

128 
lemma map_of_zip_enum_is_Some: 

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

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

131 
proof  

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

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

134 
by (auto intro!: map_of_zip_is_Some) 

135 
then show ?thesis using enum_all by auto 

136 
qed 

137 

138 
lemma map_of_zip_enum_inject: 

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

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

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

142 
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)" 

143 
shows "xs = ys" 

144 
proof  

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

146 
proof 

147 
fix x :: 'a 

148 
from length map_of_zip_enum_is_Some obtain y1 y2 

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

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

151 
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)" 

152 
by (auto dest: fun_cong) 

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

154 
by simp 

155 
qed 

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

157 
qed 

158 

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

160 
begin 

161 

162 
definition 

37765  163 
"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  164 

165 
instance proof 

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

167 
proof (rule UNIV_eq_I) 

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

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

170 
by (auto simp add: map_of_zip_map fun_eq_iff) 
26444  171 
then show "f \<in> set enum" 
172 
by (auto simp add: enum_fun_def set_n_lists) 

173 
qed 

174 
next 

175 
from map_of_zip_enum_inject 

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

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

178 
distinct_map distinct_n_lists enum_distinct set_n_lists enum_all) 

179 
qed 

180 

181 
end 

182 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

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

184 
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

185 
by (simp add: enum_fun_def Let_def) 
26444  186 

26348  187 
instantiation unit :: enum 
188 
begin 

189 

190 
definition 

191 
"enum = [()]" 

192 

31464  193 
instance proof 
194 
qed (simp_all add: enum_unit_def UNIV_unit) 

26348  195 

196 
end 

197 

198 
instantiation bool :: enum 

199 
begin 

200 

201 
definition 

202 
"enum = [False, True]" 

203 

31464  204 
instance proof 
205 
qed (simp_all add: enum_bool_def UNIV_bool) 

26348  206 

207 
end 

208 

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

210 
"product [] _ = []" 

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

212 

213 
lemma product_list_set: 

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

215 
by (induct xs) auto 

216 

26444  217 
lemma distinct_product: 
218 
assumes "distinct xs" and "distinct ys" 

219 
shows "distinct (product xs ys)" 

220 
using assms by (induct xs) 

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

222 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37601
diff
changeset

223 
instantiation prod :: (enum, enum) enum 
26348  224 
begin 
225 

226 
definition 

227 
"enum = product enum enum" 

228 

229 
instance by default 

26444  230 
(simp_all add: enum_prod_def product_list_set distinct_product enum_all enum_distinct) 
26348  231 

232 
end 

233 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37601
diff
changeset

234 
instantiation sum :: (enum, enum) enum 
26348  235 
begin 
236 

237 
definition 

238 
"enum = map Inl enum @ map Inr enum" 

239 

240 
instance by default 

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

243 
end 

244 

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

246 
"sublists [] = [[]]" 

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

248 

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

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

252 

26348  253 
lemma sublists_powset: 
26444  254 
"set ` set (sublists xs) = Pow (set xs)" 
26348  255 
proof  
256 
have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A" 

257 
by (auto simp add: image_def) 

26444  258 
have "set (map set (sublists xs)) = Pow (set xs)" 
26348  259 
by (induct xs) 
33639
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33635
diff
changeset

260 
(simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map) 
26444  261 
then show ?thesis by simp 
262 
qed 

263 

264 
lemma distinct_set_sublists: 

265 
assumes "distinct xs" 

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

267 
proof (rule card_distinct) 

268 
have "finite (set xs)" by rule 

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

270 
with assms distinct_card [of xs] 

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

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

273 
by (simp add: sublists_powset length_sublists) 

26348  274 
qed 
275 

276 
instantiation nibble :: enum 

277 
begin 

278 

279 
definition 

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

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

282 

31464  283 
instance proof 
284 
qed (simp_all add: enum_nibble_def UNIV_nibble) 

26348  285 

286 
end 

287 

288 
instantiation char :: enum 

289 
begin 

290 

291 
definition 

37765  292 
"enum = map (split Char) (product enum enum)" 
26444  293 

31482  294 
lemma enum_chars [code]: 
295 
"enum = chars" 

296 
unfolding enum_char_def chars_def enum_nibble_def by simp 

26348  297 

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

300 
distinct_map distinct_product enum_distinct) 

26348  301 

302 
end 

303 

29024  304 
instantiation option :: (enum) enum 
305 
begin 

306 

307 
definition 

308 
"enum = None # map Some enum" 

309 

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

29024  312 

313 
end 

314 

40647  315 
subsection {* Small finite types *} 
316 

317 
text {* We define small finite types for the use in Quickcheck *} 

318 

319 
datatype finite_1 = a\<^isub>1 

320 

321 
instantiation finite_1 :: enum 

322 
begin 

323 

324 
definition 

325 
"enum = [a\<^isub>1]" 

326 

327 
instance proof 

328 
qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust) 

329 

29024  330 
end 
40647  331 

40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

332 
instantiation finite_1 :: linorder 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

333 
begin 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

334 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

335 
definition less_eq_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

336 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

337 
"less_eq_finite_1 x y = True" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

338 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

339 
definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

340 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

341 
"less_finite_1 x y = False" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

342 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

343 
instance 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

344 
apply (intro_classes) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

345 
apply (auto simp add: less_finite_1_def less_eq_finite_1_def) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

346 
apply (metis finite_1.exhaust) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

347 
done 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

348 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

349 
end 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

350 

40647  351 
datatype finite_2 = a\<^isub>1  a\<^isub>2 
352 

353 
instantiation finite_2 :: enum 

354 
begin 

355 

356 
definition 

357 
"enum = [a\<^isub>1, a\<^isub>2]" 

358 

359 
instance proof 

360 
qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust) 

361 

362 
end 

363 

40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

364 
instantiation finite_2 :: linorder 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

365 
begin 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

366 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

367 
definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

368 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

369 
"less_finite_2 x y = ((x = a\<^isub>1) & (y = a\<^isub>2))" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

370 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

371 
definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

372 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

373 
"less_eq_finite_2 x y = ((x = y) \<or> (x < y))" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

374 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

375 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

376 
instance 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

377 
apply (intro_classes) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

378 
apply (auto simp add: less_finite_2_def less_eq_finite_2_def) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

379 
apply (metis finite_2.distinct finite_2.nchotomy)+ 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

380 
done 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

381 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

382 
end 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

383 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

384 

40647  385 
datatype finite_3 = a\<^isub>1  a\<^isub>2  a\<^isub>3 
386 

387 
instantiation finite_3 :: enum 

388 
begin 

389 

390 
definition 

391 
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]" 

392 

393 
instance proof 

394 
qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust) 

395 

396 
end 

397 

40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

398 
instantiation finite_3 :: linorder 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

399 
begin 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

400 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

401 
definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

402 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

403 
"less_finite_3 x y = (case x of a\<^isub>1 => (y \<noteq> a\<^isub>1) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

404 
 a\<^isub>2 => (y = a\<^isub>3) a\<^isub>3 => False)" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

405 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

406 
definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

407 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

408 
"less_eq_finite_3 x y = ((x = y) \<or> (x < y))" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

409 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

410 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

411 
instance proof (intro_classes) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

412 
qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

413 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

414 
end 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

415 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

416 

40647  417 
datatype finite_4 = a\<^isub>1  a\<^isub>2  a\<^isub>3  a\<^isub>4 
418 

419 
instantiation finite_4 :: enum 

420 
begin 

421 

422 
definition 

423 
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]" 

424 

425 
instance proof 

426 
qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust) 

427 

428 
end 

429 

40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

430 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

431 

40647  432 
datatype finite_5 = a\<^isub>1  a\<^isub>2  a\<^isub>3  a\<^isub>4  a\<^isub>5 
433 

434 
instantiation finite_5 :: enum 

435 
begin 

436 

437 
definition 

438 
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]" 

439 

440 
instance proof 

441 
qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust) 

442 

443 
end 

444 

445 
hide_type finite_1 finite_2 finite_3 finite_4 finite_5 

40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

446 
hide_const (open) n_lists product 
40647  447 

448 
end 