1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 header {* Executable finite sets *} |
|
5 |
|
6 theory Code_Set |
|
7 imports List_Set |
|
8 begin |
|
9 |
|
10 lemma foldl_apply_inv: |
|
11 assumes "\<And>x. g (h x) = x" |
|
12 shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)" |
|
13 by (rule sym, induct xs arbitrary: s) (simp_all add: assms) |
|
14 |
|
15 declare mem_def [simp] |
|
16 |
|
17 subsection {* Lifting *} |
|
18 |
|
19 datatype 'a fset = Fset "'a set" |
|
20 |
|
21 primrec member :: "'a fset \<Rightarrow> 'a set" where |
|
22 "member (Fset A) = A" |
|
23 |
|
24 lemma Fset_member [simp]: |
|
25 "Fset (member A) = A" |
|
26 by (cases A) simp |
|
27 |
|
28 definition Set :: "'a list \<Rightarrow> 'a fset" where |
|
29 "Set xs = Fset (set xs)" |
|
30 |
|
31 lemma member_Set [simp]: |
|
32 "member (Set xs) = set xs" |
|
33 by (simp add: Set_def) |
|
34 |
|
35 code_datatype Set |
|
36 |
|
37 |
|
38 subsection {* Basic operations *} |
|
39 |
|
40 definition is_empty :: "'a fset \<Rightarrow> bool" where |
|
41 [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)" |
|
42 |
|
43 lemma is_empty_Set [code]: |
|
44 "is_empty (Set xs) \<longleftrightarrow> null xs" |
|
45 by (simp add: is_empty_set) |
|
46 |
|
47 definition empty :: "'a fset" where |
|
48 [simp]: "empty = Fset {}" |
|
49 |
|
50 lemma empty_Set [code]: |
|
51 "empty = Set []" |
|
52 by (simp add: Set_def) |
|
53 |
|
54 definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
55 [simp]: "insert x A = Fset (Set.insert x (member A))" |
|
56 |
|
57 lemma insert_Set [code]: |
|
58 "insert x (Set xs) = Set (List_Set.insert x xs)" |
|
59 by (simp add: Set_def insert_set) |
|
60 |
|
61 definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
62 [simp]: "remove x A = Fset (List_Set.remove x (member A))" |
|
63 |
|
64 lemma remove_Set [code]: |
|
65 "remove x (Set xs) = Set (remove_all x xs)" |
|
66 by (simp add: Set_def remove_set) |
|
67 |
|
68 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where |
|
69 [simp]: "map f A = Fset (image f (member A))" |
|
70 |
|
71 lemma map_Set [code]: |
|
72 "map f (Set xs) = Set (remdups (List.map f xs))" |
|
73 by (simp add: Set_def) |
|
74 |
|
75 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
76 [simp]: "filter P A = Fset (List_Set.project P (member A))" |
|
77 |
|
78 lemma filter_Set [code]: |
|
79 "filter P (Set xs) = Set (List.filter P xs)" |
|
80 by (simp add: Set_def project_set) |
|
81 |
|
82 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
83 [simp]: "forall P A \<longleftrightarrow> Ball (member A) P" |
|
84 |
|
85 lemma forall_Set [code]: |
|
86 "forall P (Set xs) \<longleftrightarrow> list_all P xs" |
|
87 by (simp add: Set_def ball_set) |
|
88 |
|
89 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
90 [simp]: "exists P A \<longleftrightarrow> Bex (member A) P" |
|
91 |
|
92 lemma exists_Set [code]: |
|
93 "exists P (Set xs) \<longleftrightarrow> list_ex P xs" |
|
94 by (simp add: Set_def bex_set) |
|
95 |
|
96 |
|
97 subsection {* Derived operations *} |
|
98 |
|
99 lemma member_exists [code]: |
|
100 "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A" |
|
101 by simp |
|
102 |
|
103 definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
104 [simp]: "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B" |
|
105 |
|
106 lemma subfset_eq_forall [code]: |
|
107 "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A" |
|
108 by (simp add: subset_eq) |
|
109 |
|
110 definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
111 [simp]: "subfset A B \<longleftrightarrow> member A \<subset> member B" |
|
112 |
|
113 lemma subfset_subfset_eq [code]: |
|
114 "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A" |
|
115 by (simp add: subset) |
|
116 |
|
117 lemma eq_fset_subfset_eq [code]: |
|
118 "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A" |
|
119 by (cases A, cases B) (simp add: eq set_eq) |
|
120 |
|
121 definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
122 [simp]: "inter A B = Fset (project (member A) (member B))" |
|
123 |
|
124 lemma inter_project [code]: |
|
125 "inter A B = filter (member A) B" |
|
126 by (simp add: inter) |
|
127 |
|
128 |
|
129 subsection {* Functorial operations *} |
|
130 |
|
131 definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
132 [simp]: "union A B = Fset (member A \<union> member B)" |
|
133 |
|
134 lemma union_insert [code]: |
|
135 "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs" |
|
136 proof - |
|
137 have "foldl (\<lambda>A x. Set.insert x A) (member A) xs = |
|
138 member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)" |
|
139 by (rule foldl_apply_inv) simp |
|
140 then show ?thesis by (simp add: union_set) |
|
141 qed |
|
142 |
|
143 definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
144 [simp]: "subtract A B = Fset (member B - member A)" |
|
145 |
|
146 lemma subtract_remove [code]: |
|
147 "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs" |
|
148 proof - |
|
149 have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs = |
|
150 member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)" |
|
151 by (rule foldl_apply_inv) simp |
|
152 then show ?thesis by (simp add: minus_set) |
|
153 qed |
|
154 |
|
155 definition Inter :: "'a fset fset \<Rightarrow> 'a fset" where |
|
156 [simp]: "Inter A = Fset (Set.Inter (member ` member A))" |
|
157 |
|
158 lemma Inter_inter [code]: |
|
159 "Inter (Set (A # As)) = foldl inter A As" |
|
160 proof - |
|
161 note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del] |
|
162 have "foldl (op \<inter>) (member A) (List.map member As) = |
|
163 member (foldl (\<lambda>B A. Fset (member B \<inter> A)) A (List.map member As))" |
|
164 by (rule foldl_apply_inv) simp |
|
165 then show ?thesis |
|
166 by (simp add: Inter_set image_set inter_def_raw inter foldl_map) |
|
167 qed |
|
168 |
|
169 definition Union :: "'a fset fset \<Rightarrow> 'a fset" where |
|
170 [simp]: "Union A = Fset (Set.Union (member ` member A))" |
|
171 |
|
172 lemma Union_union [code]: |
|
173 "Union (Set As) = foldl union empty As" |
|
174 proof - |
|
175 note Union_image_eq [simp del] set_map [simp del] |
|
176 have "foldl (op \<union>) (member empty) (List.map member As) = |
|
177 member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))" |
|
178 by (rule foldl_apply_inv) simp |
|
179 then show ?thesis |
|
180 by (simp add: Union_set image_set union_def_raw foldl_map) |
|
181 qed |
|
182 |
|
183 |
|
184 subsection {* Misc operations *} |
|
185 |
|
186 lemma size_fset [code]: |
|
187 "fset_size f A = 0" |
|
188 "size A = 0" |
|
189 by (cases A, simp) (cases A, simp) |
|
190 |
|
191 lemma fset_case_code [code]: |
|
192 "fset_case f A = f (member A)" |
|
193 by (cases A) simp |
|
194 |
|
195 lemma fset_rec_code [code]: |
|
196 "fset_rec f A = f (member A)" |
|
197 by (cases A) simp |
|
198 |
|
199 |
|
200 subsection {* Simplified simprules *} |
|
201 |
|
202 lemma is_empty_simp [simp]: |
|
203 "is_empty A \<longleftrightarrow> member A = {}" |
|
204 by (simp add: List_Set.is_empty_def) |
|
205 declare is_empty_def [simp del] |
|
206 |
|
207 lemma remove_simp [simp]: |
|
208 "remove x A = Fset (member A - {x})" |
|
209 by (simp add: List_Set.remove_def) |
|
210 declare remove_def [simp del] |
|
211 |
|
212 lemma filter_simp [simp]: |
|
213 "filter P A = Fset {x \<in> member A. P x}" |
|
214 by (simp add: List_Set.project_def) |
|
215 declare filter_def [simp del] |
|
216 |
|
217 lemma inter_simp [simp]: |
|
218 "inter A B = Fset (member A \<inter> member B)" |
|
219 by (simp add: inter) |
|
220 declare inter_def [simp del] |
|
221 |
|
222 declare mem_def [simp del] |
|
223 |
|
224 end |
|