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