haftmann@31596
|
1 |
(* Author: Florian Haftmann, TU Muenchen *)
|
haftmann@26348
|
2 |
|
haftmann@26348
|
3 |
header {* Finite types as explicit enumerations *}
|
haftmann@26348
|
4 |
|
haftmann@26348
|
5 |
theory Enum
|
bulwahn@40898
|
6 |
imports Map String
|
haftmann@26348
|
7 |
begin
|
haftmann@26348
|
8 |
|
haftmann@26348
|
9 |
subsection {* Class @{text enum} *}
|
haftmann@26348
|
10 |
|
haftmann@29734
|
11 |
class enum =
|
haftmann@26348
|
12 |
fixes enum :: "'a list"
|
bulwahn@41326
|
13 |
fixes enum_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
|
bulwahn@41326
|
14 |
fixes enum_ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
|
haftmann@33635
|
15 |
assumes UNIV_enum: "UNIV = set enum"
|
haftmann@26444
|
16 |
and enum_distinct: "distinct enum"
|
bulwahn@41326
|
17 |
assumes enum_all : "enum_all P = (\<forall> x. P x)"
|
bulwahn@41326
|
18 |
assumes enum_ex : "enum_ex P = (\<exists> x. P x)"
|
haftmann@26348
|
19 |
begin
|
haftmann@26348
|
20 |
|
haftmann@29734
|
21 |
subclass finite proof
|
haftmann@29734
|
22 |
qed (simp add: UNIV_enum)
|
haftmann@26444
|
23 |
|
bulwahn@41326
|
24 |
lemma enum_UNIV: "set enum = UNIV" unfolding UNIV_enum ..
|
haftmann@26444
|
25 |
|
bulwahn@40931
|
26 |
lemma in_enum: "x \<in> set enum"
|
bulwahn@41326
|
27 |
unfolding enum_UNIV by auto
|
haftmann@26348
|
28 |
|
haftmann@26348
|
29 |
lemma enum_eq_I:
|
haftmann@26348
|
30 |
assumes "\<And>x. x \<in> set xs"
|
haftmann@26348
|
31 |
shows "set enum = set xs"
|
haftmann@26348
|
32 |
proof -
|
haftmann@26348
|
33 |
from assms UNIV_eq_I have "UNIV = set xs" by auto
|
bulwahn@41326
|
34 |
with enum_UNIV show ?thesis by simp
|
haftmann@26348
|
35 |
qed
|
haftmann@26348
|
36 |
|
haftmann@26348
|
37 |
end
|
haftmann@26348
|
38 |
|
haftmann@26348
|
39 |
|
haftmann@26348
|
40 |
subsection {* Equality and order on functions *}
|
haftmann@26348
|
41 |
|
haftmann@39086
|
42 |
instantiation "fun" :: (enum, equal) equal
|
haftmann@26513
|
43 |
begin
|
haftmann@26348
|
44 |
|
haftmann@26513
|
45 |
definition
|
haftmann@39086
|
46 |
"HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
|
haftmann@26513
|
47 |
|
haftmann@31464
|
48 |
instance proof
|
bulwahn@41326
|
49 |
qed (simp_all add: equal_fun_def enum_UNIV fun_eq_iff)
|
haftmann@26513
|
50 |
|
haftmann@26513
|
51 |
end
|
haftmann@26348
|
52 |
|
bulwahn@41142
|
53 |
lemma [code]:
|
bulwahn@41326
|
54 |
"HOL.equal f g \<longleftrightarrow> enum_all (%x. f x = g x)"
|
bulwahn@41326
|
55 |
by (auto simp add: equal enum_all fun_eq_iff)
|
bulwahn@41142
|
56 |
|
haftmann@39086
|
57 |
lemma [code nbe]:
|
haftmann@39086
|
58 |
"HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
|
haftmann@39086
|
59 |
by (fact equal_refl)
|
haftmann@39086
|
60 |
|
haftmann@28562
|
61 |
lemma order_fun [code]:
|
haftmann@26348
|
62 |
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
|
bulwahn@41326
|
63 |
shows "f \<le> g \<longleftrightarrow> enum_all (\<lambda>x. f x \<le> g x)"
|
bulwahn@41326
|
64 |
and "f < g \<longleftrightarrow> f \<le> g \<and> enum_ex (\<lambda>x. f x \<noteq> g x)"
|
bulwahn@41326
|
65 |
by (simp_all add: enum_all enum_ex fun_eq_iff le_fun_def order_less_le)
|
haftmann@26968
|
66 |
|
haftmann@26968
|
67 |
|
haftmann@26968
|
68 |
subsection {* Quantifiers *}
|
haftmann@26968
|
69 |
|
bulwahn@41326
|
70 |
lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> enum_all P"
|
bulwahn@41326
|
71 |
by (simp add: enum_all)
|
haftmann@26968
|
72 |
|
bulwahn@41326
|
73 |
lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> enum_ex P"
|
bulwahn@41326
|
74 |
by (simp add: enum_ex)
|
haftmann@26348
|
75 |
|
bulwahn@40900
|
76 |
lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
|
bulwahn@41326
|
77 |
unfolding list_ex1_iff enum_UNIV by auto
|
bulwahn@40900
|
78 |
|
haftmann@26348
|
79 |
|
haftmann@26348
|
80 |
subsection {* Default instances *}
|
haftmann@26348
|
81 |
|
haftmann@26444
|
82 |
primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
|
haftmann@26444
|
83 |
"n_lists 0 xs = [[]]"
|
haftmann@26444
|
84 |
| "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
|
haftmann@26444
|
85 |
|
haftmann@26444
|
86 |
lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
|
haftmann@26444
|
87 |
by (induct n) simp_all
|
haftmann@26444
|
88 |
|
haftmann@26444
|
89 |
lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
|
hoelzl@33639
|
90 |
by (induct n) (auto simp add: length_concat o_def listsum_triv)
|
haftmann@26444
|
91 |
|
haftmann@26444
|
92 |
lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
|
haftmann@26444
|
93 |
by (induct n arbitrary: ys) auto
|
haftmann@26444
|
94 |
|
haftmann@26444
|
95 |
lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
|
nipkow@39535
|
96 |
proof (rule set_eqI)
|
haftmann@26444
|
97 |
fix ys :: "'a list"
|
haftmann@26444
|
98 |
show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
|
haftmann@26444
|
99 |
proof -
|
haftmann@26444
|
100 |
have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
|
haftmann@26444
|
101 |
by (induct n arbitrary: ys) auto
|
haftmann@26444
|
102 |
moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
|
haftmann@26444
|
103 |
by (induct n arbitrary: ys) auto
|
haftmann@26444
|
104 |
moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
|
haftmann@26444
|
105 |
by (induct ys) auto
|
haftmann@26444
|
106 |
ultimately show ?thesis by auto
|
haftmann@26444
|
107 |
qed
|
haftmann@26444
|
108 |
qed
|
haftmann@26444
|
109 |
|
haftmann@26444
|
110 |
lemma distinct_n_lists:
|
haftmann@26444
|
111 |
assumes "distinct xs"
|
haftmann@26444
|
112 |
shows "distinct (n_lists n xs)"
|
haftmann@26444
|
113 |
proof (rule card_distinct)
|
haftmann@26444
|
114 |
from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
|
haftmann@26444
|
115 |
have "card (set (n_lists n xs)) = card (set xs) ^ n"
|
haftmann@26444
|
116 |
proof (induct n)
|
haftmann@26444
|
117 |
case 0 then show ?case by simp
|
haftmann@26444
|
118 |
next
|
haftmann@26444
|
119 |
case (Suc n)
|
haftmann@26444
|
120 |
moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
|
haftmann@26444
|
121 |
= (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
|
haftmann@26444
|
122 |
by (rule card_UN_disjoint) auto
|
haftmann@26444
|
123 |
moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
|
haftmann@26444
|
124 |
by (rule card_image) (simp add: inj_on_def)
|
haftmann@26444
|
125 |
ultimately show ?case by auto
|
haftmann@26444
|
126 |
qed
|
haftmann@26444
|
127 |
also have "\<dots> = length xs ^ n" by (simp add: card_length)
|
haftmann@26444
|
128 |
finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
|
haftmann@26444
|
129 |
by (simp add: length_n_lists)
|
haftmann@26444
|
130 |
qed
|
haftmann@26444
|
131 |
|
haftmann@26444
|
132 |
lemma map_of_zip_enum_is_Some:
|
haftmann@26444
|
133 |
assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
|
haftmann@26444
|
134 |
shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
|
haftmann@26444
|
135 |
proof -
|
haftmann@26444
|
136 |
from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow>
|
haftmann@26444
|
137 |
(\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)"
|
haftmann@26444
|
138 |
by (auto intro!: map_of_zip_is_Some)
|
bulwahn@41326
|
139 |
then show ?thesis using enum_UNIV by auto
|
haftmann@26444
|
140 |
qed
|
haftmann@26444
|
141 |
|
haftmann@26444
|
142 |
lemma map_of_zip_enum_inject:
|
haftmann@26444
|
143 |
fixes xs ys :: "'b\<Colon>enum list"
|
haftmann@26444
|
144 |
assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)"
|
haftmann@26444
|
145 |
"length ys = length (enum \<Colon> 'a\<Colon>enum list)"
|
haftmann@26444
|
146 |
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)"
|
haftmann@26444
|
147 |
shows "xs = ys"
|
haftmann@26444
|
148 |
proof -
|
haftmann@26444
|
149 |
have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)"
|
haftmann@26444
|
150 |
proof
|
haftmann@26444
|
151 |
fix x :: 'a
|
haftmann@26444
|
152 |
from length map_of_zip_enum_is_Some obtain y1 y2
|
haftmann@26444
|
153 |
where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
|
haftmann@26444
|
154 |
and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
|
haftmann@26444
|
155 |
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)"
|
haftmann@26444
|
156 |
by (auto dest: fun_cong)
|
haftmann@26444
|
157 |
ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
|
haftmann@26444
|
158 |
by simp
|
haftmann@26444
|
159 |
qed
|
haftmann@26444
|
160 |
with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
|
haftmann@26444
|
161 |
qed
|
haftmann@26444
|
162 |
|
bulwahn@41326
|
163 |
definition
|
bulwahn@41326
|
164 |
all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
|
bulwahn@41326
|
165 |
where
|
bulwahn@41326
|
166 |
"all_n_lists P n = (\<forall>xs \<in> set (n_lists n enum). P xs)"
|
bulwahn@41326
|
167 |
|
bulwahn@41326
|
168 |
lemma [code]:
|
bulwahn@41326
|
169 |
"all_n_lists P n = (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))"
|
bulwahn@41326
|
170 |
unfolding all_n_lists_def enum_all
|
bulwahn@41326
|
171 |
by (cases n) (auto simp add: enum_UNIV)
|
bulwahn@41326
|
172 |
|
bulwahn@41326
|
173 |
definition
|
bulwahn@41326
|
174 |
ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
|
bulwahn@41326
|
175 |
where
|
bulwahn@41326
|
176 |
"ex_n_lists P n = (\<exists>xs \<in> set (n_lists n enum). P xs)"
|
bulwahn@41326
|
177 |
|
bulwahn@41326
|
178 |
lemma [code]:
|
bulwahn@41326
|
179 |
"ex_n_lists P n = (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))"
|
bulwahn@41326
|
180 |
unfolding ex_n_lists_def enum_ex
|
bulwahn@41326
|
181 |
by (cases n) (auto simp add: enum_UNIV)
|
bulwahn@41326
|
182 |
|
bulwahn@41326
|
183 |
|
haftmann@26444
|
184 |
instantiation "fun" :: (enum, enum) enum
|
haftmann@26444
|
185 |
begin
|
haftmann@26444
|
186 |
|
haftmann@26444
|
187 |
definition
|
haftmann@37765
|
188 |
"enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
|
haftmann@26444
|
189 |
|
bulwahn@41326
|
190 |
definition
|
bulwahn@41326
|
191 |
"enum_all P = all_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
|
bulwahn@41326
|
192 |
|
bulwahn@41326
|
193 |
definition
|
bulwahn@41326
|
194 |
"enum_ex P = ex_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
|
bulwahn@41326
|
195 |
|
bulwahn@41326
|
196 |
|
haftmann@26444
|
197 |
instance proof
|
haftmann@26444
|
198 |
show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
|
haftmann@26444
|
199 |
proof (rule UNIV_eq_I)
|
haftmann@26444
|
200 |
fix f :: "'a \<Rightarrow> 'b"
|
haftmann@26444
|
201 |
have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
|
bulwahn@40931
|
202 |
by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
|
haftmann@26444
|
203 |
then show "f \<in> set enum"
|
bulwahn@40931
|
204 |
by (auto simp add: enum_fun_def set_n_lists intro: in_enum)
|
haftmann@26444
|
205 |
qed
|
haftmann@26444
|
206 |
next
|
haftmann@26444
|
207 |
from map_of_zip_enum_inject
|
haftmann@26444
|
208 |
show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
|
haftmann@26444
|
209 |
by (auto intro!: inj_onI simp add: enum_fun_def
|
haftmann@26444
|
210 |
distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
|
bulwahn@41326
|
211 |
next
|
bulwahn@41326
|
212 |
fix P
|
bulwahn@41326
|
213 |
show "enum_all (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<forall>x. P x)"
|
bulwahn@41326
|
214 |
proof
|
bulwahn@41326
|
215 |
assume "enum_all P"
|
bulwahn@41326
|
216 |
show "\<forall>x. P x"
|
bulwahn@41326
|
217 |
proof
|
bulwahn@41326
|
218 |
fix f :: "'a \<Rightarrow> 'b"
|
bulwahn@41326
|
219 |
have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
|
bulwahn@41326
|
220 |
by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
|
bulwahn@41326
|
221 |
from `enum_all P` have "P (the \<circ> map_of (zip enum (map f enum)))"
|
bulwahn@41326
|
222 |
unfolding enum_all_fun_def all_n_lists_def
|
bulwahn@41326
|
223 |
apply (simp add: set_n_lists)
|
bulwahn@41326
|
224 |
apply (erule_tac x="map f enum" in allE)
|
bulwahn@41326
|
225 |
apply (auto intro!: in_enum)
|
bulwahn@41326
|
226 |
done
|
bulwahn@41326
|
227 |
from this f show "P f" by auto
|
bulwahn@41326
|
228 |
qed
|
bulwahn@41326
|
229 |
next
|
bulwahn@41326
|
230 |
assume "\<forall>x. P x"
|
bulwahn@41326
|
231 |
from this show "enum_all P"
|
bulwahn@41326
|
232 |
unfolding enum_all_fun_def all_n_lists_def by auto
|
bulwahn@41326
|
233 |
qed
|
bulwahn@41326
|
234 |
next
|
bulwahn@41326
|
235 |
fix P
|
bulwahn@41326
|
236 |
show "enum_ex (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<exists>x. P x)"
|
bulwahn@41326
|
237 |
proof
|
bulwahn@41326
|
238 |
assume "enum_ex P"
|
bulwahn@41326
|
239 |
from this show "\<exists>x. P x"
|
bulwahn@41326
|
240 |
unfolding enum_ex_fun_def ex_n_lists_def by auto
|
bulwahn@41326
|
241 |
next
|
bulwahn@41326
|
242 |
assume "\<exists>x. P x"
|
bulwahn@41326
|
243 |
from this obtain f where "P f" ..
|
bulwahn@41326
|
244 |
have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
|
bulwahn@41326
|
245 |
by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
|
bulwahn@41326
|
246 |
from `P f` this have "P (the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum)))"
|
bulwahn@41326
|
247 |
by auto
|
bulwahn@41326
|
248 |
from this show "enum_ex P"
|
bulwahn@41326
|
249 |
unfolding enum_ex_fun_def ex_n_lists_def
|
bulwahn@41326
|
250 |
apply (auto simp add: set_n_lists)
|
bulwahn@41326
|
251 |
apply (rule_tac x="map f enum" in exI)
|
bulwahn@41326
|
252 |
apply (auto intro!: in_enum)
|
bulwahn@41326
|
253 |
done
|
bulwahn@41326
|
254 |
qed
|
haftmann@26444
|
255 |
qed
|
haftmann@26444
|
256 |
|
haftmann@26444
|
257 |
end
|
haftmann@26444
|
258 |
|
haftmann@39086
|
259 |
lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
|
haftmann@28245
|
260 |
in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
|
haftmann@28245
|
261 |
by (simp add: enum_fun_def Let_def)
|
haftmann@26444
|
262 |
|
bulwahn@41326
|
263 |
lemma enum_all_fun_code [code]:
|
bulwahn@41326
|
264 |
"enum_all P = (let enum_a = (enum :: 'a::{enum, equal} list)
|
bulwahn@41326
|
265 |
in all_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
|
bulwahn@41326
|
266 |
by (simp add: enum_all_fun_def Let_def)
|
bulwahn@41326
|
267 |
|
bulwahn@41326
|
268 |
lemma enum_ex_fun_code [code]:
|
bulwahn@41326
|
269 |
"enum_ex P = (let enum_a = (enum :: 'a::{enum, equal} list)
|
bulwahn@41326
|
270 |
in ex_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
|
bulwahn@41326
|
271 |
by (simp add: enum_ex_fun_def Let_def)
|
bulwahn@41326
|
272 |
|
haftmann@26348
|
273 |
instantiation unit :: enum
|
haftmann@26348
|
274 |
begin
|
haftmann@26348
|
275 |
|
haftmann@26348
|
276 |
definition
|
haftmann@26348
|
277 |
"enum = [()]"
|
haftmann@26348
|
278 |
|
bulwahn@41326
|
279 |
definition
|
bulwahn@41326
|
280 |
"enum_all P = P ()"
|
bulwahn@41326
|
281 |
|
bulwahn@41326
|
282 |
definition
|
bulwahn@41326
|
283 |
"enum_ex P = P ()"
|
bulwahn@41326
|
284 |
|
haftmann@31464
|
285 |
instance proof
|
bulwahn@41326
|
286 |
qed (auto simp add: enum_unit_def UNIV_unit enum_all_unit_def enum_ex_unit_def intro: unit.exhaust)
|
haftmann@26348
|
287 |
|
haftmann@26348
|
288 |
end
|
haftmann@26348
|
289 |
|
haftmann@26348
|
290 |
instantiation bool :: enum
|
haftmann@26348
|
291 |
begin
|
haftmann@26348
|
292 |
|
haftmann@26348
|
293 |
definition
|
haftmann@26348
|
294 |
"enum = [False, True]"
|
haftmann@26348
|
295 |
|
bulwahn@41326
|
296 |
definition
|
bulwahn@41326
|
297 |
"enum_all P = (P False \<and> P True)"
|
bulwahn@41326
|
298 |
|
bulwahn@41326
|
299 |
definition
|
bulwahn@41326
|
300 |
"enum_ex P = (P False \<or> P True)"
|
bulwahn@41326
|
301 |
|
haftmann@31464
|
302 |
instance proof
|
bulwahn@41326
|
303 |
fix P
|
bulwahn@41326
|
304 |
show "enum_all (P :: bool \<Rightarrow> bool) = (\<forall>x. P x)"
|
bulwahn@41326
|
305 |
unfolding enum_all_bool_def by (auto, case_tac x) auto
|
bulwahn@41326
|
306 |
next
|
bulwahn@41326
|
307 |
fix P
|
bulwahn@41326
|
308 |
show "enum_ex (P :: bool \<Rightarrow> bool) = (\<exists>x. P x)"
|
bulwahn@41326
|
309 |
unfolding enum_ex_bool_def by (auto, case_tac x) auto
|
bulwahn@41326
|
310 |
qed (auto simp add: enum_bool_def UNIV_bool)
|
haftmann@26348
|
311 |
|
haftmann@26348
|
312 |
end
|
haftmann@26348
|
313 |
|
haftmann@26348
|
314 |
primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
|
haftmann@26348
|
315 |
"product [] _ = []"
|
haftmann@26348
|
316 |
| "product (x#xs) ys = map (Pair x) ys @ product xs ys"
|
haftmann@26348
|
317 |
|
haftmann@26348
|
318 |
lemma product_list_set:
|
haftmann@26348
|
319 |
"set (product xs ys) = set xs \<times> set ys"
|
haftmann@26348
|
320 |
by (induct xs) auto
|
haftmann@26348
|
321 |
|
haftmann@26444
|
322 |
lemma distinct_product:
|
haftmann@26444
|
323 |
assumes "distinct xs" and "distinct ys"
|
haftmann@26444
|
324 |
shows "distinct (product xs ys)"
|
haftmann@26444
|
325 |
using assms by (induct xs)
|
haftmann@26444
|
326 |
(auto intro: inj_onI simp add: product_list_set distinct_map)
|
haftmann@26444
|
327 |
|
haftmann@37678
|
328 |
instantiation prod :: (enum, enum) enum
|
haftmann@26348
|
329 |
begin
|
haftmann@26348
|
330 |
|
haftmann@26348
|
331 |
definition
|
haftmann@26348
|
332 |
"enum = product enum enum"
|
haftmann@26348
|
333 |
|
bulwahn@41326
|
334 |
definition
|
bulwahn@41326
|
335 |
"enum_all P = enum_all (%x. enum_all (%y. P (x, y)))"
|
bulwahn@41326
|
336 |
|
bulwahn@41326
|
337 |
definition
|
bulwahn@41326
|
338 |
"enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))"
|
bulwahn@41326
|
339 |
|
bulwahn@41326
|
340 |
|
haftmann@26348
|
341 |
instance by default
|
bulwahn@41326
|
342 |
(simp_all add: enum_prod_def product_list_set distinct_product
|
bulwahn@41326
|
343 |
enum_UNIV enum_distinct enum_all_prod_def enum_all enum_ex_prod_def enum_ex)
|
haftmann@26348
|
344 |
|
haftmann@26348
|
345 |
end
|
haftmann@26348
|
346 |
|
haftmann@37678
|
347 |
instantiation sum :: (enum, enum) enum
|
haftmann@26348
|
348 |
begin
|
haftmann@26348
|
349 |
|
haftmann@26348
|
350 |
definition
|
haftmann@26348
|
351 |
"enum = map Inl enum @ map Inr enum"
|
haftmann@26348
|
352 |
|
bulwahn@41326
|
353 |
definition
|
bulwahn@41326
|
354 |
"enum_all P = (enum_all (%x. P (Inl x)) \<and> enum_all (%x. P (Inr x)))"
|
bulwahn@41326
|
355 |
|
bulwahn@41326
|
356 |
definition
|
bulwahn@41326
|
357 |
"enum_ex P = (enum_ex (%x. P (Inl x)) \<or> enum_ex (%x. P (Inr x)))"
|
bulwahn@41326
|
358 |
|
bulwahn@41326
|
359 |
instance proof
|
bulwahn@41326
|
360 |
fix P
|
bulwahn@41326
|
361 |
show "enum_all (P :: ('a + 'b) \<Rightarrow> bool) = (\<forall>x. P x)"
|
bulwahn@41326
|
362 |
unfolding enum_all_sum_def enum_all
|
bulwahn@41326
|
363 |
by (auto, case_tac x) auto
|
bulwahn@41326
|
364 |
next
|
bulwahn@41326
|
365 |
fix P
|
bulwahn@41326
|
366 |
show "enum_ex (P :: ('a + 'b) \<Rightarrow> bool) = (\<exists>x. P x)"
|
bulwahn@41326
|
367 |
unfolding enum_ex_sum_def enum_ex
|
bulwahn@41326
|
368 |
by (auto, case_tac x) auto
|
bulwahn@41326
|
369 |
qed (auto simp add: enum_UNIV enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
|
haftmann@26348
|
370 |
|
haftmann@26348
|
371 |
end
|
haftmann@26348
|
372 |
|
haftmann@26348
|
373 |
primrec sublists :: "'a list \<Rightarrow> 'a list list" where
|
haftmann@26348
|
374 |
"sublists [] = [[]]"
|
haftmann@26348
|
375 |
| "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
|
haftmann@26348
|
376 |
|
haftmann@26444
|
377 |
lemma length_sublists:
|
haftmann@26444
|
378 |
"length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
|
haftmann@26444
|
379 |
by (induct xs) (simp_all add: Let_def)
|
haftmann@26444
|
380 |
|
haftmann@26348
|
381 |
lemma sublists_powset:
|
haftmann@26444
|
382 |
"set ` set (sublists xs) = Pow (set xs)"
|
haftmann@26348
|
383 |
proof -
|
haftmann@26348
|
384 |
have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
|
haftmann@26348
|
385 |
by (auto simp add: image_def)
|
haftmann@26444
|
386 |
have "set (map set (sublists xs)) = Pow (set xs)"
|
haftmann@26348
|
387 |
by (induct xs)
|
hoelzl@33639
|
388 |
(simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
|
haftmann@26444
|
389 |
then show ?thesis by simp
|
haftmann@26444
|
390 |
qed
|
haftmann@26444
|
391 |
|
haftmann@26444
|
392 |
lemma distinct_set_sublists:
|
haftmann@26444
|
393 |
assumes "distinct xs"
|
haftmann@26444
|
394 |
shows "distinct (map set (sublists xs))"
|
haftmann@26444
|
395 |
proof (rule card_distinct)
|
haftmann@26444
|
396 |
have "finite (set xs)" by rule
|
haftmann@26444
|
397 |
then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
|
haftmann@26444
|
398 |
with assms distinct_card [of xs]
|
haftmann@26444
|
399 |
have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
|
haftmann@26444
|
400 |
then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
|
haftmann@26444
|
401 |
by (simp add: sublists_powset length_sublists)
|
haftmann@26348
|
402 |
qed
|
haftmann@26348
|
403 |
|
haftmann@26348
|
404 |
instantiation nibble :: enum
|
haftmann@26348
|
405 |
begin
|
haftmann@26348
|
406 |
|
haftmann@26348
|
407 |
definition
|
haftmann@26348
|
408 |
"enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
|
haftmann@26348
|
409 |
Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
|
haftmann@26348
|
410 |
|
bulwahn@41326
|
411 |
definition
|
bulwahn@41326
|
412 |
"enum_all P = (P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7
|
bulwahn@41326
|
413 |
\<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF)"
|
bulwahn@41326
|
414 |
|
bulwahn@41326
|
415 |
definition
|
bulwahn@41326
|
416 |
"enum_ex P = (P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7
|
bulwahn@41326
|
417 |
\<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF)"
|
bulwahn@41326
|
418 |
|
haftmann@31464
|
419 |
instance proof
|
bulwahn@41326
|
420 |
fix P
|
bulwahn@41326
|
421 |
show "enum_all (P :: nibble \<Rightarrow> bool) = (\<forall>x. P x)"
|
bulwahn@41326
|
422 |
unfolding enum_all_nibble_def
|
bulwahn@41326
|
423 |
by (auto, case_tac x) auto
|
bulwahn@41326
|
424 |
next
|
bulwahn@41326
|
425 |
fix P
|
bulwahn@41326
|
426 |
show "enum_ex (P :: nibble \<Rightarrow> bool) = (\<exists>x. P x)"
|
bulwahn@41326
|
427 |
unfolding enum_ex_nibble_def
|
bulwahn@41326
|
428 |
by (auto, case_tac x) auto
|
haftmann@31464
|
429 |
qed (simp_all add: enum_nibble_def UNIV_nibble)
|
haftmann@26348
|
430 |
|
haftmann@26348
|
431 |
end
|
haftmann@26348
|
432 |
|
haftmann@26348
|
433 |
instantiation char :: enum
|
haftmann@26348
|
434 |
begin
|
haftmann@26348
|
435 |
|
haftmann@26348
|
436 |
definition
|
haftmann@37765
|
437 |
"enum = map (split Char) (product enum enum)"
|
haftmann@26444
|
438 |
|
haftmann@31491
|
439 |
lemma enum_chars [code]:
|
haftmann@31491
|
440 |
"enum = chars"
|
haftmann@31491
|
441 |
unfolding enum_char_def chars_def enum_nibble_def by simp
|
haftmann@26348
|
442 |
|
bulwahn@41326
|
443 |
definition
|
bulwahn@41326
|
444 |
"enum_all P = list_all P chars"
|
bulwahn@41326
|
445 |
|
bulwahn@41326
|
446 |
definition
|
bulwahn@41326
|
447 |
"enum_ex P = list_ex P chars"
|
bulwahn@41326
|
448 |
|
bulwahn@41326
|
449 |
lemma set_enum_char: "set (enum :: char list) = UNIV"
|
bulwahn@41326
|
450 |
by (auto intro: char.exhaust simp add: enum_char_def product_list_set enum_UNIV full_SetCompr_eq [symmetric])
|
bulwahn@41326
|
451 |
|
haftmann@31464
|
452 |
instance proof
|
bulwahn@41326
|
453 |
fix P
|
bulwahn@41326
|
454 |
show "enum_all (P :: char \<Rightarrow> bool) = (\<forall>x. P x)"
|
bulwahn@41326
|
455 |
unfolding enum_all_char_def enum_chars[symmetric]
|
bulwahn@41326
|
456 |
by (auto simp add: list_all_iff set_enum_char)
|
bulwahn@41326
|
457 |
next
|
bulwahn@41326
|
458 |
fix P
|
bulwahn@41326
|
459 |
show "enum_ex (P :: char \<Rightarrow> bool) = (\<exists>x. P x)"
|
bulwahn@41326
|
460 |
unfolding enum_ex_char_def enum_chars[symmetric]
|
bulwahn@41326
|
461 |
by (auto simp add: list_ex_iff set_enum_char)
|
bulwahn@41326
|
462 |
next
|
bulwahn@41326
|
463 |
show "distinct (enum :: char list)"
|
bulwahn@41326
|
464 |
by (auto intro: inj_onI simp add: enum_char_def product_list_set distinct_map distinct_product enum_distinct)
|
bulwahn@41326
|
465 |
qed (auto simp add: set_enum_char)
|
haftmann@26348
|
466 |
|
haftmann@26348
|
467 |
end
|
haftmann@26348
|
468 |
|
huffman@29024
|
469 |
instantiation option :: (enum) enum
|
huffman@29024
|
470 |
begin
|
huffman@29024
|
471 |
|
huffman@29024
|
472 |
definition
|
huffman@29024
|
473 |
"enum = None # map Some enum"
|
huffman@29024
|
474 |
|
bulwahn@41326
|
475 |
definition
|
bulwahn@41326
|
476 |
"enum_all P = (P None \<and> enum_all (%x. P (Some x)))"
|
bulwahn@41326
|
477 |
|
bulwahn@41326
|
478 |
definition
|
bulwahn@41326
|
479 |
"enum_ex P = (P None \<or> enum_ex (%x. P (Some x)))"
|
bulwahn@41326
|
480 |
|
haftmann@31464
|
481 |
instance proof
|
bulwahn@41326
|
482 |
fix P
|
bulwahn@41326
|
483 |
show "enum_all (P :: 'a option \<Rightarrow> bool) = (\<forall>x. P x)"
|
bulwahn@41326
|
484 |
unfolding enum_all_option_def enum_all
|
bulwahn@41326
|
485 |
by (auto, case_tac x) auto
|
bulwahn@41326
|
486 |
next
|
bulwahn@41326
|
487 |
fix P
|
bulwahn@41326
|
488 |
show "enum_ex (P :: 'a option \<Rightarrow> bool) = (\<exists>x. P x)"
|
bulwahn@41326
|
489 |
unfolding enum_ex_option_def enum_ex
|
bulwahn@41326
|
490 |
by (auto, case_tac x) auto
|
bulwahn@41326
|
491 |
qed (auto simp add: enum_UNIV enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
|
huffman@29024
|
492 |
|
huffman@29024
|
493 |
end
|
huffman@29024
|
494 |
|
bulwahn@40895
|
495 |
subsection {* Small finite types *}
|
bulwahn@40895
|
496 |
|
bulwahn@40895
|
497 |
text {* We define small finite types for the use in Quickcheck *}
|
bulwahn@40895
|
498 |
|
bulwahn@40895
|
499 |
datatype finite_1 = a\<^isub>1
|
bulwahn@40895
|
500 |
|
bulwahn@41144
|
501 |
notation (output) a\<^isub>1 ("a\<^isub>1")
|
bulwahn@41144
|
502 |
|
bulwahn@40895
|
503 |
instantiation finite_1 :: enum
|
bulwahn@40895
|
504 |
begin
|
bulwahn@40895
|
505 |
|
bulwahn@40895
|
506 |
definition
|
bulwahn@40895
|
507 |
"enum = [a\<^isub>1]"
|
bulwahn@40895
|
508 |
|
bulwahn@41326
|
509 |
definition
|
bulwahn@41326
|
510 |
"enum_all P = P a\<^isub>1"
|
bulwahn@41326
|
511 |
|
bulwahn@41326
|
512 |
definition
|
bulwahn@41326
|
513 |
"enum_ex P = P a\<^isub>1"
|
bulwahn@41326
|
514 |
|
bulwahn@40895
|
515 |
instance proof
|
bulwahn@41326
|
516 |
fix P
|
bulwahn@41326
|
517 |
show "enum_all (P :: finite_1 \<Rightarrow> bool) = (\<forall>x. P x)"
|
bulwahn@41326
|
518 |
unfolding enum_all_finite_1_def
|
bulwahn@41326
|
519 |
by (auto, case_tac x) auto
|
bulwahn@41326
|
520 |
next
|
bulwahn@41326
|
521 |
fix P
|
bulwahn@41326
|
522 |
show "enum_ex (P :: finite_1 \<Rightarrow> bool) = (\<exists>x. P x)"
|
bulwahn@41326
|
523 |
unfolding enum_ex_finite_1_def
|
bulwahn@41326
|
524 |
by (auto, case_tac x) auto
|
bulwahn@40895
|
525 |
qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust)
|
bulwahn@40895
|
526 |
|
huffman@29024
|
527 |
end
|
bulwahn@40895
|
528 |
|
bulwahn@40899
|
529 |
instantiation finite_1 :: linorder
|
bulwahn@40899
|
530 |
begin
|
bulwahn@40899
|
531 |
|
bulwahn@40899
|
532 |
definition less_eq_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
|
bulwahn@40899
|
533 |
where
|
bulwahn@40899
|
534 |
"less_eq_finite_1 x y = True"
|
bulwahn@40899
|
535 |
|
bulwahn@40899
|
536 |
definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
|
bulwahn@40899
|
537 |
where
|
bulwahn@40899
|
538 |
"less_finite_1 x y = False"
|
bulwahn@40899
|
539 |
|
bulwahn@40899
|
540 |
instance
|
bulwahn@40899
|
541 |
apply (intro_classes)
|
bulwahn@40899
|
542 |
apply (auto simp add: less_finite_1_def less_eq_finite_1_def)
|
bulwahn@40899
|
543 |
apply (metis finite_1.exhaust)
|
bulwahn@40899
|
544 |
done
|
bulwahn@40899
|
545 |
|
bulwahn@40899
|
546 |
end
|
bulwahn@40899
|
547 |
|
bulwahn@41333
|
548 |
hide_const (open) a\<^isub>1
|
bulwahn@40905
|
549 |
|
bulwahn@40895
|
550 |
datatype finite_2 = a\<^isub>1 | a\<^isub>2
|
bulwahn@40895
|
551 |
|
bulwahn@41144
|
552 |
notation (output) a\<^isub>1 ("a\<^isub>1")
|
bulwahn@41144
|
553 |
notation (output) a\<^isub>2 ("a\<^isub>2")
|
bulwahn@41144
|
554 |
|
bulwahn@40895
|
555 |
instantiation finite_2 :: enum
|
bulwahn@40895
|
556 |
begin
|
bulwahn@40895
|
557 |
|
bulwahn@40895
|
558 |
definition
|
bulwahn@40895
|
559 |
"enum = [a\<^isub>1, a\<^isub>2]"
|
bulwahn@40895
|
560 |
|
bulwahn@41326
|
561 |
definition
|
bulwahn@41326
|
562 |
"enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2)"
|
bulwahn@41326
|
563 |
|
bulwahn@41326
|
564 |
definition
|
bulwahn@41326
|
565 |
"enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2)"
|
bulwahn@41326
|
566 |
|
bulwahn@40895
|
567 |
instance proof
|
bulwahn@41326
|
568 |
fix P
|
bulwahn@41326
|
569 |
show "enum_all (P :: finite_2 \<Rightarrow> bool) = (\<forall>x. P x)"
|
bulwahn@41326
|
570 |
unfolding enum_all_finite_2_def
|
bulwahn@41326
|
571 |
by (auto, case_tac x) auto
|
bulwahn@41326
|
572 |
next
|
bulwahn@41326
|
573 |
fix P
|
bulwahn@41326
|
574 |
show "enum_ex (P :: finite_2 \<Rightarrow> bool) = (\<exists>x. P x)"
|
bulwahn@41326
|
575 |
unfolding enum_ex_finite_2_def
|
bulwahn@41326
|
576 |
by (auto, case_tac x) auto
|
bulwahn@40895
|
577 |
qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust)
|
bulwahn@40895
|
578 |
|
bulwahn@40895
|
579 |
end
|
bulwahn@40895
|
580 |
|
bulwahn@40899
|
581 |
instantiation finite_2 :: linorder
|
bulwahn@40899
|
582 |
begin
|
bulwahn@40899
|
583 |
|
bulwahn@40899
|
584 |
definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
|
bulwahn@40899
|
585 |
where
|
bulwahn@40899
|
586 |
"less_finite_2 x y = ((x = a\<^isub>1) & (y = a\<^isub>2))"
|
bulwahn@40899
|
587 |
|
bulwahn@40899
|
588 |
definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
|
bulwahn@40899
|
589 |
where
|
bulwahn@40899
|
590 |
"less_eq_finite_2 x y = ((x = y) \<or> (x < y))"
|
bulwahn@40899
|
591 |
|
bulwahn@40899
|
592 |
|
bulwahn@40899
|
593 |
instance
|
bulwahn@40899
|
594 |
apply (intro_classes)
|
bulwahn@40899
|
595 |
apply (auto simp add: less_finite_2_def less_eq_finite_2_def)
|
bulwahn@40899
|
596 |
apply (metis finite_2.distinct finite_2.nchotomy)+
|
bulwahn@40899
|
597 |
done
|
bulwahn@40899
|
598 |
|
bulwahn@40899
|
599 |
end
|
bulwahn@40899
|
600 |
|
bulwahn@41333
|
601 |
hide_const (open) a\<^isub>1 a\<^isub>2
|
bulwahn@40905
|
602 |
|
bulwahn@40899
|
603 |
|
bulwahn@40895
|
604 |
datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
|
bulwahn@40895
|
605 |
|
bulwahn@41144
|
606 |
notation (output) a\<^isub>1 ("a\<^isub>1")
|
bulwahn@41144
|
607 |
notation (output) a\<^isub>2 ("a\<^isub>2")
|
bulwahn@41144
|
608 |
notation (output) a\<^isub>3 ("a\<^isub>3")
|
bulwahn@41144
|
609 |
|
bulwahn@40895
|
610 |
instantiation finite_3 :: enum
|
bulwahn@40895
|
611 |
begin
|
bulwahn@40895
|
612 |
|
bulwahn@40895
|
613 |
definition
|
bulwahn@40895
|
614 |
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]"
|
bulwahn@40895
|
615 |
|
bulwahn@41326
|
616 |
definition
|
bulwahn@41326
|
617 |
"enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3)"
|
bulwahn@41326
|
618 |
|
bulwahn@41326
|
619 |
definition
|
bulwahn@41326
|
620 |
"enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3)"
|
bulwahn@41326
|
621 |
|
bulwahn@40895
|
622 |
instance proof
|
bulwahn@41326
|
623 |
fix P
|
bulwahn@41326
|
624 |
show "enum_all (P :: finite_3 \<Rightarrow> bool) = (\<forall>x. P x)"
|
bulwahn@41326
|
625 |
unfolding enum_all_finite_3_def
|
bulwahn@41326
|
626 |
by (auto, case_tac x) auto
|
bulwahn@41326
|
627 |
next
|
bulwahn@41326
|
628 |
fix P
|
bulwahn@41326
|
629 |
show "enum_ex (P :: finite_3 \<Rightarrow> bool) = (\<exists>x. P x)"
|
bulwahn@41326
|
630 |
unfolding enum_ex_finite_3_def
|
bulwahn@41326
|
631 |
by (auto, case_tac x) auto
|
bulwahn@40895
|
632 |
qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust)
|
bulwahn@40895
|
633 |
|
bulwahn@40895
|
634 |
end
|
bulwahn@40895
|
635 |
|
bulwahn@40899
|
636 |
instantiation finite_3 :: linorder
|
bulwahn@40899
|
637 |
begin
|
bulwahn@40899
|
638 |
|
bulwahn@40899
|
639 |
definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
|
bulwahn@40899
|
640 |
where
|
bulwahn@40899
|
641 |
"less_finite_3 x y = (case x of a\<^isub>1 => (y \<noteq> a\<^isub>1)
|
bulwahn@40899
|
642 |
| a\<^isub>2 => (y = a\<^isub>3)| a\<^isub>3 => False)"
|
bulwahn@40899
|
643 |
|
bulwahn@40899
|
644 |
definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
|
bulwahn@40899
|
645 |
where
|
bulwahn@40899
|
646 |
"less_eq_finite_3 x y = ((x = y) \<or> (x < y))"
|
bulwahn@40899
|
647 |
|
bulwahn@40899
|
648 |
|
bulwahn@40899
|
649 |
instance proof (intro_classes)
|
bulwahn@40899
|
650 |
qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm)
|
bulwahn@40899
|
651 |
|
bulwahn@40899
|
652 |
end
|
bulwahn@40899
|
653 |
|
bulwahn@41333
|
654 |
hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3
|
bulwahn@40905
|
655 |
|
bulwahn@40899
|
656 |
|
bulwahn@40895
|
657 |
datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
|
bulwahn@40895
|
658 |
|
bulwahn@41144
|
659 |
notation (output) a\<^isub>1 ("a\<^isub>1")
|
bulwahn@41144
|
660 |
notation (output) a\<^isub>2 ("a\<^isub>2")
|
bulwahn@41144
|
661 |
notation (output) a\<^isub>3 ("a\<^isub>3")
|
bulwahn@41144
|
662 |
notation (output) a\<^isub>4 ("a\<^isub>4")
|
bulwahn@41144
|
663 |
|
bulwahn@40895
|
664 |
instantiation finite_4 :: enum
|
bulwahn@40895
|
665 |
begin
|
bulwahn@40895
|
666 |
|
bulwahn@40895
|
667 |
definition
|
bulwahn@40895
|
668 |
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]"
|
bulwahn@40895
|
669 |
|
bulwahn@41326
|
670 |
definition
|
bulwahn@41326
|
671 |
"enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4)"
|
bulwahn@41326
|
672 |
|
bulwahn@41326
|
673 |
definition
|
bulwahn@41326
|
674 |
"enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4)"
|
bulwahn@41326
|
675 |
|
bulwahn@40895
|
676 |
instance proof
|
bulwahn@41326
|
677 |
fix P
|
bulwahn@41326
|
678 |
show "enum_all (P :: finite_4 \<Rightarrow> bool) = (\<forall>x. P x)"
|
bulwahn@41326
|
679 |
unfolding enum_all_finite_4_def
|
bulwahn@41326
|
680 |
by (auto, case_tac x) auto
|
bulwahn@41326
|
681 |
next
|
bulwahn@41326
|
682 |
fix P
|
bulwahn@41326
|
683 |
show "enum_ex (P :: finite_4 \<Rightarrow> bool) = (\<exists>x. P x)"
|
bulwahn@41326
|
684 |
unfolding enum_ex_finite_4_def
|
bulwahn@41326
|
685 |
by (auto, case_tac x) auto
|
bulwahn@40895
|
686 |
qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust)
|
bulwahn@40895
|
687 |
|
bulwahn@40895
|
688 |
end
|
bulwahn@40895
|
689 |
|
bulwahn@41333
|
690 |
hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
|
bulwahn@40899
|
691 |
|
bulwahn@40899
|
692 |
|
bulwahn@40895
|
693 |
datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
|
bulwahn@40895
|
694 |
|
bulwahn@41144
|
695 |
notation (output) a\<^isub>1 ("a\<^isub>1")
|
bulwahn@41144
|
696 |
notation (output) a\<^isub>2 ("a\<^isub>2")
|
bulwahn@41144
|
697 |
notation (output) a\<^isub>3 ("a\<^isub>3")
|
bulwahn@41144
|
698 |
notation (output) a\<^isub>4 ("a\<^isub>4")
|
bulwahn@41144
|
699 |
notation (output) a\<^isub>5 ("a\<^isub>5")
|
bulwahn@41144
|
700 |
|
bulwahn@40895
|
701 |
instantiation finite_5 :: enum
|
bulwahn@40895
|
702 |
begin
|
bulwahn@40895
|
703 |
|
bulwahn@40895
|
704 |
definition
|
bulwahn@40895
|
705 |
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]"
|
bulwahn@40895
|
706 |
|
bulwahn@41326
|
707 |
definition
|
bulwahn@41326
|
708 |
"enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4 \<and> P a\<^isub>5)"
|
bulwahn@41326
|
709 |
|
bulwahn@41326
|
710 |
definition
|
bulwahn@41326
|
711 |
"enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4 \<or> P a\<^isub>5)"
|
bulwahn@41326
|
712 |
|
bulwahn@40895
|
713 |
instance proof
|
bulwahn@41326
|
714 |
fix P
|
bulwahn@41326
|
715 |
show "enum_all (P :: finite_5 \<Rightarrow> bool) = (\<forall>x. P x)"
|
bulwahn@41326
|
716 |
unfolding enum_all_finite_5_def
|
bulwahn@41326
|
717 |
by (auto, case_tac x) auto
|
bulwahn@41326
|
718 |
next
|
bulwahn@41326
|
719 |
fix P
|
bulwahn@41326
|
720 |
show "enum_ex (P :: finite_5 \<Rightarrow> bool) = (\<exists>x. P x)"
|
bulwahn@41326
|
721 |
unfolding enum_ex_finite_5_def
|
bulwahn@41326
|
722 |
by (auto, case_tac x) auto
|
bulwahn@40895
|
723 |
qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)
|
bulwahn@40895
|
724 |
|
bulwahn@40895
|
725 |
end
|
bulwahn@40895
|
726 |
|
bulwahn@41363
|
727 |
subsection {* An executable THE operator on finite types *}
|
bulwahn@41363
|
728 |
|
bulwahn@41363
|
729 |
definition
|
bulwahn@41363
|
730 |
[code del]: "enum_the P = The P"
|
bulwahn@41363
|
731 |
|
bulwahn@41363
|
732 |
lemma [code]:
|
bulwahn@41363
|
733 |
"The P = (case filter P enum of [x] => x | _ => enum_the P)"
|
bulwahn@41363
|
734 |
proof -
|
bulwahn@41363
|
735 |
{
|
bulwahn@41363
|
736 |
fix a
|
bulwahn@41363
|
737 |
assume filter_enum: "filter P enum = [a]"
|
bulwahn@41363
|
738 |
have "The P = a"
|
bulwahn@41363
|
739 |
proof (rule the_equality)
|
bulwahn@41363
|
740 |
fix x
|
bulwahn@41363
|
741 |
assume "P x"
|
bulwahn@41363
|
742 |
show "x = a"
|
bulwahn@41363
|
743 |
proof (rule ccontr)
|
bulwahn@41363
|
744 |
assume "x \<noteq> a"
|
bulwahn@41363
|
745 |
from filter_enum obtain us vs
|
bulwahn@41363
|
746 |
where enum_eq: "enum = us @ [a] @ vs"
|
bulwahn@41363
|
747 |
and "\<forall> x \<in> set us. \<not> P x"
|
bulwahn@41363
|
748 |
and "\<forall> x \<in> set vs. \<not> P x"
|
bulwahn@41363
|
749 |
and "P a"
|
bulwahn@41363
|
750 |
by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric])
|
bulwahn@41363
|
751 |
with `P x` in_enum[of x, unfolded enum_eq] `x \<noteq> a` show "False" by auto
|
bulwahn@41363
|
752 |
qed
|
bulwahn@41363
|
753 |
next
|
bulwahn@41363
|
754 |
from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff)
|
bulwahn@41363
|
755 |
qed
|
bulwahn@41363
|
756 |
}
|
bulwahn@41363
|
757 |
from this show ?thesis
|
bulwahn@41363
|
758 |
unfolding enum_the_def by (auto split: list.split)
|
bulwahn@41363
|
759 |
qed
|
bulwahn@41363
|
760 |
|
bulwahn@45969
|
761 |
subsection {* An executable card operator on finite types *}
|
bulwahn@45969
|
762 |
|
bulwahn@45969
|
763 |
lemma
|
bulwahn@45969
|
764 |
[code]: "card R = length (filter R enum)"
|
bulwahn@45969
|
765 |
by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV Collect_def)
|
bulwahn@45969
|
766 |
|
bulwahn@45969
|
767 |
subsection {* An executable (reflexive) transitive closure on finite relations *}
|
bulwahn@45969
|
768 |
|
bulwahn@45971
|
769 |
text {* Definitions could be moved to Transitive Closure theory if they are of more general use. *}
|
bulwahn@45969
|
770 |
|
bulwahn@45969
|
771 |
definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a => bool)"
|
bulwahn@45969
|
772 |
where
|
bulwahn@45969
|
773 |
[code del]: "ntrancl R n = (UN i : {i. 0 < i & i <= (Suc n)}. R ^^ i)"
|
bulwahn@45969
|
774 |
|
bulwahn@45969
|
775 |
lemma [code]:
|
bulwahn@45969
|
776 |
"ntrancl (R :: 'a * 'a => bool) 0 = R"
|
bulwahn@45969
|
777 |
proof
|
bulwahn@45969
|
778 |
show "R <= ntrancl R 0"
|
bulwahn@45969
|
779 |
unfolding ntrancl_def by fastforce
|
bulwahn@45969
|
780 |
next
|
bulwahn@45969
|
781 |
{
|
bulwahn@45969
|
782 |
fix i have "(0 < i & i <= Suc 0) = (i = 1)" by auto
|
bulwahn@45969
|
783 |
}
|
bulwahn@45969
|
784 |
from this show "ntrancl R 0 <= R"
|
bulwahn@45969
|
785 |
unfolding ntrancl_def by auto
|
bulwahn@45969
|
786 |
qed
|
bulwahn@45969
|
787 |
|
bulwahn@45969
|
788 |
lemma [code]:
|
bulwahn@45969
|
789 |
"ntrancl (R :: 'a * 'a => bool) (Suc n) = (ntrancl R n) O (Id Un R)"
|
bulwahn@45969
|
790 |
proof
|
bulwahn@45969
|
791 |
{
|
bulwahn@45969
|
792 |
fix a b
|
bulwahn@45969
|
793 |
assume "(a, b) : ntrancl R (Suc n)"
|
bulwahn@45969
|
794 |
from this obtain i where "0 < i" "i <= Suc (Suc n)" "(a, b) : R ^^ i"
|
bulwahn@45969
|
795 |
unfolding ntrancl_def by auto
|
bulwahn@45969
|
796 |
have "(a, b) : ntrancl R n O (Id Un R)"
|
bulwahn@45969
|
797 |
proof (cases "i = 1")
|
bulwahn@45969
|
798 |
case True
|
bulwahn@45969
|
799 |
from this `(a, b) : R ^^ i` show ?thesis
|
bulwahn@45969
|
800 |
unfolding ntrancl_def by auto
|
bulwahn@45969
|
801 |
next
|
bulwahn@45969
|
802 |
case False
|
bulwahn@45969
|
803 |
from this `0 < i` obtain j where j: "i = Suc j" "0 < j"
|
bulwahn@45969
|
804 |
by (cases i) auto
|
bulwahn@45969
|
805 |
from this `(a, b) : R ^^ i` obtain c where c1: "(a, c) : R ^^ j" and c2:"(c, b) : R"
|
bulwahn@45969
|
806 |
by auto
|
bulwahn@45969
|
807 |
from c1 j `i <= Suc (Suc n)` have "(a, c): ntrancl R n"
|
bulwahn@45969
|
808 |
unfolding ntrancl_def by fastforce
|
bulwahn@45969
|
809 |
from this c2 show ?thesis by fastforce
|
bulwahn@45969
|
810 |
qed
|
bulwahn@45969
|
811 |
}
|
bulwahn@45969
|
812 |
from this show "ntrancl R (Suc n) <= ntrancl R n O (Id Un R)" by auto
|
bulwahn@45969
|
813 |
next
|
bulwahn@45969
|
814 |
show "ntrancl R n O (Id Un R) <= ntrancl R (Suc n)"
|
bulwahn@45969
|
815 |
unfolding ntrancl_def by fastforce
|
bulwahn@45969
|
816 |
qed
|
bulwahn@45969
|
817 |
|
bulwahn@45969
|
818 |
lemma [code]: "trancl (R :: ('a :: finite) * 'a => bool) = ntrancl R (card R - 1)"
|
bulwahn@45969
|
819 |
by (cases "card R") (auto simp add: trancl_finite_eq_rel_pow rel_pow_empty ntrancl_def)
|
bulwahn@45969
|
820 |
|
bulwahn@45969
|
821 |
(* a copy of Nitpick.rtrancl_unfold, should be moved to Transitive_Closure *)
|
bulwahn@45969
|
822 |
lemma [code]: "r^* = (r^+)^="
|
bulwahn@45969
|
823 |
by simp
|
bulwahn@45969
|
824 |
|
bulwahn@45969
|
825 |
subsection {* Closing up *}
|
bulwahn@45969
|
826 |
|
bulwahn@41363
|
827 |
code_abort enum_the
|
bulwahn@41363
|
828 |
|
bulwahn@41333
|
829 |
hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
|
bulwahn@40905
|
830 |
|
bulwahn@40905
|
831 |
|
bulwahn@41333
|
832 |
hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
|
bulwahn@45969
|
833 |
hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product ntrancl
|
bulwahn@40895
|
834 |
|
bulwahn@40895
|
835 |
end
|