author | haftmann |
Sat, 16 May 2009 20:16:49 +0200 | |
changeset 31186 | b458b4ac570f |
parent 30664 | 167da873c3b3 |
child 31847 | 7de0e20ca24d |
permissions | -rw-r--r-- |
23854 | 1 |
(* Title: HOL/Library/Executable_Set.thy |
2 |
Author: Stefan Berghofer, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Implementation of finite sets by lists *} |
|
6 |
||
7 |
theory Executable_Set |
|
30664
167da873c3b3
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
30304
diff
changeset
|
8 |
imports Main |
23854 | 9 |
begin |
10 |
||
11 |
subsection {* Definitional rewrites *} |
|
12 |
||
28522 | 13 |
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
14 |
"subset = op \<le>" |
|
15 |
||
16 |
declare subset_def [symmetric, code unfold] |
|
17 |
||
28939 | 18 |
lemma [code]: "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
28522 | 19 |
unfolding subset_def subset_eq .. |
23854 | 20 |
|
28522 | 21 |
definition is_empty :: "'a set \<Rightarrow> bool" where |
22 |
"is_empty A \<longleftrightarrow> A = {}" |
|
23 |
||
24 |
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
25 |
[code del]: "eq_set = op =" |
|
26 |
||
27 |
lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
|
28 |
unfolding eq_set_def by auto |
|
26816 | 29 |
|
29107 | 30 |
(* FIXME allow for Stefan's code generator: |
31 |
declare set_eq_subset[code unfold] |
|
32 |
*) |
|
33 |
||
23854 | 34 |
lemma [code]: |
35 |
"a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)" |
|
36 |
unfolding bex_triv_one_point1 .. |
|
37 |
||
28939 | 38 |
definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
23854 | 39 |
"filter_set P xs = {x\<in>xs. P x}" |
40 |
||
29107 | 41 |
declare filter_set_def[symmetric, code unfold] |
42 |
||
23854 | 43 |
|
44 |
subsection {* Operations on lists *} |
|
45 |
||
46 |
subsubsection {* Basic definitions *} |
|
47 |
||
48 |
definition |
|
49 |
flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where |
|
50 |
"flip f a b = f b a" |
|
51 |
||
52 |
definition |
|
53 |
member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where |
|
54 |
"member xs x \<longleftrightarrow> x \<in> set xs" |
|
55 |
||
56 |
definition |
|
57 |
insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
58 |
"insertl x xs = (if member xs x then xs else x#xs)" |
|
59 |
||
60 |
lemma [code target: List]: "member [] y \<longleftrightarrow> False" |
|
61 |
and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y" |
|
62 |
unfolding member_def by (induct xs) simp_all |
|
63 |
||
64 |
fun |
|
65 |
drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
66 |
"drop_first f [] = []" |
|
67 |
| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)" |
|
68 |
declare drop_first.simps [code del] |
|
69 |
declare drop_first.simps [code target: List] |
|
70 |
||
71 |
declare remove1.simps [code del] |
|
72 |
lemma [code target: List]: |
|
73 |
"remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)" |
|
74 |
proof (cases "member xs x") |
|
75 |
case False thus ?thesis unfolding member_def by (induct xs) auto |
|
76 |
next |
|
77 |
case True |
|
78 |
have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all |
|
79 |
with True show ?thesis by simp |
|
80 |
qed |
|
81 |
||
82 |
lemma member_nil [simp]: |
|
83 |
"member [] = (\<lambda>x. False)" |
|
26816 | 84 |
proof (rule ext) |
23854 | 85 |
fix x |
86 |
show "member [] x = False" unfolding member_def by simp |
|
87 |
qed |
|
88 |
||
89 |
lemma member_insertl [simp]: |
|
90 |
"x \<in> set (insertl x xs)" |
|
91 |
unfolding insertl_def member_def mem_iff by simp |
|
92 |
||
93 |
lemma insertl_member [simp]: |
|
94 |
fixes xs x |
|
95 |
assumes member: "member xs x" |
|
96 |
shows "insertl x xs = xs" |
|
97 |
using member unfolding insertl_def by simp |
|
98 |
||
99 |
lemma insertl_not_member [simp]: |
|
100 |
fixes xs x |
|
101 |
assumes member: "\<not> (member xs x)" |
|
102 |
shows "insertl x xs = x # xs" |
|
103 |
using member unfolding insertl_def by simp |
|
104 |
||
105 |
lemma foldr_remove1_empty [simp]: |
|
106 |
"foldr remove1 xs [] = []" |
|
107 |
by (induct xs) simp_all |
|
108 |
||
109 |
||
110 |
subsubsection {* Derived definitions *} |
|
111 |
||
112 |
function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
113 |
where |
|
114 |
"unionl [] ys = ys" |
|
115 |
| "unionl xs ys = foldr insertl xs ys" |
|
116 |
by pat_completeness auto |
|
117 |
termination by lexicographic_order |
|
118 |
||
26312 | 119 |
lemmas unionl_eq = unionl.simps(2) |
23854 | 120 |
|
121 |
function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
122 |
where |
|
123 |
"intersect [] ys = []" |
|
124 |
| "intersect xs [] = []" |
|
125 |
| "intersect xs ys = filter (member xs) ys" |
|
126 |
by pat_completeness auto |
|
127 |
termination by lexicographic_order |
|
128 |
||
26312 | 129 |
lemmas intersect_eq = intersect.simps(3) |
23854 | 130 |
|
131 |
function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
132 |
where |
|
133 |
"subtract [] ys = ys" |
|
134 |
| "subtract xs [] = []" |
|
135 |
| "subtract xs ys = foldr remove1 xs ys" |
|
136 |
by pat_completeness auto |
|
137 |
termination by lexicographic_order |
|
138 |
||
26312 | 139 |
lemmas subtract_eq = subtract.simps(3) |
23854 | 140 |
|
141 |
function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" |
|
142 |
where |
|
143 |
"map_distinct f [] = []" |
|
144 |
| "map_distinct f xs = foldr (insertl o f) xs []" |
|
145 |
by pat_completeness auto |
|
146 |
termination by lexicographic_order |
|
147 |
||
26312 | 148 |
lemmas map_distinct_eq = map_distinct.simps(2) |
23854 | 149 |
|
150 |
function unions :: "'a list list \<Rightarrow> 'a list" |
|
151 |
where |
|
152 |
"unions [] = []" |
|
153 |
| "unions xs = foldr unionl xs []" |
|
154 |
by pat_completeness auto |
|
155 |
termination by lexicographic_order |
|
156 |
||
26312 | 157 |
lemmas unions_eq = unions.simps(2) |
23854 | 158 |
|
159 |
consts intersects :: "'a list list \<Rightarrow> 'a list" |
|
160 |
primrec |
|
161 |
"intersects (x#xs) = foldr intersect xs x" |
|
162 |
||
163 |
definition |
|
164 |
map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where |
|
165 |
"map_union xs f = unions (map f xs)" |
|
166 |
||
167 |
definition |
|
168 |
map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where |
|
169 |
"map_inter xs f = intersects (map f xs)" |
|
170 |
||
171 |
||
172 |
subsection {* Isomorphism proofs *} |
|
173 |
||
174 |
lemma iso_member: |
|
175 |
"member xs x \<longleftrightarrow> x \<in> set xs" |
|
176 |
unfolding member_def mem_iff .. |
|
177 |
||
178 |
lemma iso_insert: |
|
179 |
"set (insertl x xs) = insert x (set xs)" |
|
30304
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
29110
diff
changeset
|
180 |
unfolding insertl_def iso_member by (simp add: insert_absorb) |
23854 | 181 |
|
182 |
lemma iso_remove1: |
|
183 |
assumes distnct: "distinct xs" |
|
184 |
shows "set (remove1 x xs) = set xs - {x}" |
|
185 |
using distnct set_remove1_eq by auto |
|
186 |
||
187 |
lemma iso_union: |
|
188 |
"set (unionl xs ys) = set xs \<union> set ys" |
|
26312 | 189 |
unfolding unionl_eq |
23854 | 190 |
by (induct xs arbitrary: ys) (simp_all add: iso_insert) |
191 |
||
192 |
lemma iso_intersect: |
|
193 |
"set (intersect xs ys) = set xs \<inter> set ys" |
|
26312 | 194 |
unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto |
23854 | 195 |
|
196 |
definition |
|
197 |
subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
198 |
"subtract' = flip subtract" |
|
199 |
||
200 |
lemma iso_subtract: |
|
201 |
fixes ys |
|
202 |
assumes distnct: "distinct ys" |
|
203 |
shows "set (subtract' ys xs) = set ys - set xs" |
|
204 |
and "distinct (subtract' ys xs)" |
|
26312 | 205 |
unfolding subtract'_def flip_def subtract_eq |
23854 | 206 |
using distnct by (induct xs arbitrary: ys) auto |
207 |
||
208 |
lemma iso_map_distinct: |
|
209 |
"set (map_distinct f xs) = image f (set xs)" |
|
26312 | 210 |
unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert) |
23854 | 211 |
|
212 |
lemma iso_unions: |
|
213 |
"set (unions xss) = \<Union> set (map set xss)" |
|
26312 | 214 |
unfolding unions_eq |
23854 | 215 |
proof (induct xss) |
216 |
case Nil show ?case by simp |
|
217 |
next |
|
218 |
case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert) |
|
219 |
qed |
|
220 |
||
221 |
lemma iso_intersects: |
|
222 |
"set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))" |
|
223 |
by (induct xss) (simp_all add: Int_def iso_member, auto) |
|
224 |
||
225 |
lemma iso_UNION: |
|
226 |
"set (map_union xs f) = UNION (set xs) (set o f)" |
|
227 |
unfolding map_union_def iso_unions by simp |
|
228 |
||
229 |
lemma iso_INTER: |
|
230 |
"set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)" |
|
231 |
unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto) |
|
232 |
||
233 |
definition |
|
234 |
Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where |
|
235 |
"Blall = flip list_all" |
|
236 |
definition |
|
237 |
Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where |
|
238 |
"Blex = flip list_ex" |
|
239 |
||
240 |
lemma iso_Ball: |
|
241 |
"Blall xs f = Ball (set xs) f" |
|
242 |
unfolding Blall_def flip_def by (induct xs) simp_all |
|
243 |
||
244 |
lemma iso_Bex: |
|
245 |
"Blex xs f = Bex (set xs) f" |
|
246 |
unfolding Blex_def flip_def by (induct xs) simp_all |
|
247 |
||
248 |
lemma iso_filter: |
|
249 |
"set (filter P xs) = filter_set P (set xs)" |
|
250 |
unfolding filter_set_def by (induct xs) auto |
|
251 |
||
252 |
subsection {* code generator setup *} |
|
253 |
||
254 |
ML {* |
|
255 |
nonfix inter; |
|
256 |
nonfix union; |
|
257 |
nonfix subset; |
|
258 |
*} |
|
259 |
||
260 |
subsubsection {* const serializations *} |
|
261 |
||
262 |
consts_code |
|
30304
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
29110
diff
changeset
|
263 |
"Set.empty" ("{*[]*}") |
23854 | 264 |
insert ("{*insertl*}") |
28522 | 265 |
is_empty ("{*null*}") |
23854 | 266 |
"op \<union>" ("{*unionl*}") |
267 |
"op \<inter>" ("{*intersect*}") |
|
268 |
"op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}") |
|
269 |
image ("{*map_distinct*}") |
|
270 |
Union ("{*unions*}") |
|
271 |
Inter ("{*intersects*}") |
|
272 |
UNION ("{*map_union*}") |
|
273 |
INTER ("{*map_inter*}") |
|
274 |
Ball ("{*Blall*}") |
|
275 |
Bex ("{*Blex*}") |
|
276 |
filter_set ("{*filter*}") |
|
29110 | 277 |
fold ("{* foldl o flip *}") |
23854 | 278 |
|
279 |
end |