src/HOL/Library/Executable_Set.thy
 author huffman Thu Jun 11 09:03:24 2009 -0700 (2009-06-11) changeset 31563 ded2364d14d4 parent 30664 167da873c3b3 child 31847 7de0e20ca24d permissions -rw-r--r--
cleaned up some proofs
1 (*  Title:      HOL/Library/Executable_Set.thy
2     Author:     Stefan Berghofer, TU Muenchen
3 *)
5 header {* Implementation of finite sets by lists *}
7 theory Executable_Set
8 imports Main
9 begin
11 subsection {* Definitional rewrites *}
13 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
14   "subset = op \<le>"
16 declare subset_def [symmetric, code unfold]
18 lemma [code]: "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
19   unfolding subset_def subset_eq ..
21 definition is_empty :: "'a set \<Rightarrow> bool" where
22   "is_empty A \<longleftrightarrow> A = {}"
24 definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
25   [code del]: "eq_set = op ="
27 lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
28   unfolding eq_set_def by auto
30 (* FIXME allow for Stefan's code generator:
31 declare set_eq_subset[code unfold]
32 *)
34 lemma [code]:
35   "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
36   unfolding bex_triv_one_point1 ..
38 definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
39   "filter_set P xs = {x\<in>xs. P x}"
41 declare filter_set_def[symmetric, code unfold]
44 subsection {* Operations on lists *}
46 subsubsection {* Basic definitions *}
48 definition
49   flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
50   "flip f a b = f b a"
52 definition
53   member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
54   "member xs x \<longleftrightarrow> x \<in> set xs"
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)"
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
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]
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
82 lemma member_nil [simp]:
83   "member [] = (\<lambda>x. False)"
84 proof (rule ext)
85   fix x
86   show "member [] x = False" unfolding member_def by simp
87 qed
89 lemma member_insertl [simp]:
90   "x \<in> set (insertl x xs)"
91   unfolding insertl_def member_def mem_iff by simp
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
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
105 lemma foldr_remove1_empty [simp]:
106   "foldr remove1 xs [] = []"
107   by (induct xs) simp_all
110 subsubsection {* Derived definitions *}
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
119 lemmas unionl_eq = unionl.simps(2)
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
129 lemmas intersect_eq = intersect.simps(3)
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
139 lemmas subtract_eq = subtract.simps(3)
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
148 lemmas map_distinct_eq = map_distinct.simps(2)
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
157 lemmas unions_eq = unions.simps(2)
159 consts intersects :: "'a list list \<Rightarrow> 'a list"
160 primrec
161   "intersects (x#xs) = foldr intersect xs x"
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)"
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)"
172 subsection {* Isomorphism proofs *}
174 lemma iso_member:
175   "member xs x \<longleftrightarrow> x \<in> set xs"
176   unfolding member_def mem_iff ..
178 lemma iso_insert:
179   "set (insertl x xs) = insert x (set xs)"
180   unfolding insertl_def iso_member by (simp add: insert_absorb)
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
187 lemma iso_union:
188   "set (unionl xs ys) = set xs \<union> set ys"
189   unfolding unionl_eq
190   by (induct xs arbitrary: ys) (simp_all add: iso_insert)
192 lemma iso_intersect:
193   "set (intersect xs ys) = set xs \<inter> set ys"
194   unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
196 definition
197   subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
198   "subtract' = flip subtract"
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)"
205   unfolding subtract'_def flip_def subtract_eq
206   using distnct by (induct xs arbitrary: ys) auto
208 lemma iso_map_distinct:
209   "set (map_distinct f xs) = image f (set xs)"
210   unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
212 lemma iso_unions:
213   "set (unions xss) = \<Union> set (map set xss)"
214   unfolding unions_eq
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
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)
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
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)
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"
240 lemma iso_Ball:
241   "Blall xs f = Ball (set xs) f"
242   unfolding Blall_def flip_def by (induct xs) simp_all
244 lemma iso_Bex:
245   "Blex xs f = Bex (set xs) f"
246   unfolding Blex_def flip_def by (induct xs) simp_all
248 lemma iso_filter:
249   "set (filter P xs) = filter_set P (set xs)"
250   unfolding filter_set_def by (induct xs) auto
252 subsection {* code generator setup *}
254 ML {*
255 nonfix inter;
256 nonfix union;
257 nonfix subset;
258 *}
260 subsubsection {* const serializations *}
262 consts_code
263   "Set.empty" ("{*[]*}")
264   insert ("{*insertl*}")
265   is_empty ("{*null*}")
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*}")
277   fold ("{* foldl o flip *}")
279 end