207 (* LIFTING DEFS *) |
207 (* LIFTING DEFS *) |
208 |
208 |
209 |
209 |
210 section {* Constants on the Quotient Type *} |
210 section {* Constants on the Quotient Type *} |
211 |
211 |
212 quotient_def |
212 quotient_definition |
213 "fempty :: 'a fset" |
213 "fempty :: 'a fset" |
214 as "[]::'a list" |
214 as "[]::'a list" |
215 |
215 |
216 quotient_def |
216 quotient_definition |
217 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
217 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
218 as "op #" |
218 as "op #" |
219 |
219 |
220 quotient_def |
220 quotient_definition |
221 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50) |
221 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50) |
222 as "\<lambda>x X. x \<in> set X" |
222 as "\<lambda>x X. x \<in> set X" |
223 |
223 |
224 abbreviation |
224 abbreviation |
225 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50) |
225 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50) |
226 where |
226 where |
227 "a \<notin>f S \<equiv> \<not>(a \<in>f S)" |
227 "a \<notin>f S \<equiv> \<not>(a \<in>f S)" |
228 |
228 |
229 quotient_def |
229 quotient_definition |
230 "fcard :: 'a fset \<Rightarrow> nat" |
230 "fcard :: 'a fset \<Rightarrow> nat" |
231 as "card_raw" |
231 as "card_raw" |
232 |
232 |
233 quotient_def |
233 quotient_definition |
234 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
234 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
235 as "delete_raw" |
235 as "delete_raw" |
236 |
236 |
237 quotient_def |
237 quotient_definition |
238 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50) |
238 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50) |
239 as "op @" |
239 as "op @" |
240 |
240 |
241 quotient_def |
241 quotient_definition |
242 "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) |
242 "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) |
243 as "inter_raw" |
243 as "inter_raw" |
244 |
244 |
245 quotient_def |
245 quotient_definition |
246 "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
246 "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
247 as "fold_raw" |
247 as "fold_raw" |
248 |
248 |
249 quotient_def |
249 quotient_definition |
250 "fset_to_set :: 'a fset \<Rightarrow> 'a set" |
250 "fset_to_set :: 'a fset \<Rightarrow> 'a set" |
251 as "set" |
251 as "set" |
252 |
252 |
253 |
253 |
254 section {* Lifted Theorems *} |
254 section {* Lifted Theorems *} |
302 (* We also have map and some properties of it in FSet *) |
302 (* We also have map and some properties of it in FSet *) |
303 (* and the following which still lifts ok *) |
303 (* and the following which still lifts ok *) |
304 lemma "funion (funion x xa) xb = funion x (funion xa xb)" |
304 lemma "funion (funion x xa) xb = funion x (funion xa xb)" |
305 by (lifting append_assoc) |
305 by (lifting append_assoc) |
306 |
306 |
307 quotient_def |
307 quotient_definition |
308 "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
308 "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
309 as |
309 as |
310 "list_case" |
310 "list_case" |
311 |
311 |
312 (* NOT SURE IF TRUE *) |
312 (* NOT SURE IF TRUE *) |