equal
deleted
inserted
replaced
112 quotient_definition |
112 quotient_definition |
113 "fcard :: 'a fset \<Rightarrow> nat" |
113 "fcard :: 'a fset \<Rightarrow> nat" |
114 is |
114 is |
115 "fcard_raw" |
115 "fcard_raw" |
116 |
116 |
|
117 lemma fcard_raw_0: |
|
118 fixes a :: "'a list" |
|
119 shows "(fcard_raw a = 0) = (a \<approx> [])" |
|
120 apply (induct a) |
|
121 apply auto |
|
122 apply (drule memb_absorb) |
|
123 apply (auto simp add: nil_not_cons) |
|
124 done |
|
125 |
117 lemma fcard_raw_gt_0: |
126 lemma fcard_raw_gt_0: |
118 assumes a: "x \<in> set xs" |
127 assumes a: "x \<in> set xs" |
119 shows "0 < fcard_raw xs" |
128 shows "0 < fcard_raw xs" |
120 using a |
129 using a |
121 by (induct xs) (auto simp add: memb_def) |
130 by (induct xs) (auto simp add: memb_def) |
|
131 |
|
132 lemma fcard_raw_not_memb: |
|
133 fixes x :: "'a" |
|
134 fixes xs :: "'a list" |
|
135 shows "(~(memb x xs)) = (fcard_raw (x # xs) = Suc (fcard_raw xs))" |
|
136 by auto |
|
137 |
|
138 lemma fcard_raw_suc: |
|
139 fixes xs :: "'a list" |
|
140 fixes n :: "nat" |
|
141 assumes c: "fcard_raw xs = Suc n" |
|
142 shows "\<exists>a ys. ~(memb a ys) \<and> xs \<approx> (a # ys)" |
|
143 using c |
|
144 apply(induct xs) |
|
145 apply simp |
|
146 apply (auto) |
|
147 apply (metis memb_def) |
|
148 done |
122 |
149 |
123 lemma fcard_raw_delete_one: |
150 lemma fcard_raw_delete_one: |
124 "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" |
151 "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" |
125 by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def) |
152 by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def) |
126 |
153 |
145 |
172 |
146 quotient_definition |
173 quotient_definition |
147 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
174 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
148 is |
175 is |
149 "map" |
176 "map" |
|
177 |
|
178 lemma map_append: |
|
179 "(map f (a @ b)) \<approx> (map f a) @ (map f b)" |
|
180 by simp |
150 |
181 |
151 text {* raw section *} |
182 text {* raw section *} |
152 |
183 |
153 lemma map_rsp_aux: |
184 lemma map_rsp_aux: |
154 assumes a: "a \<approx> b" |
185 assumes a: "a \<approx> b" |
268 |
299 |
269 lemma inj_map_eq_iff: |
300 lemma inj_map_eq_iff: |
270 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)" |
301 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)" |
271 by (simp add: expand_set_eq[symmetric] inj_image_eq_iff) |
302 by (simp add: expand_set_eq[symmetric] inj_image_eq_iff) |
272 |
303 |
273 |
304 quotient_definition |
274 |
305 "fconcat :: ('a fset) fset \<Rightarrow> 'a fset" |
|
306 is |
|
307 "concat" |
|
308 |
|
309 lemma list_equiv_rsp[quot_respect]: |
|
310 shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>" |
|
311 by auto |
275 |
312 |
276 section {* lifted part *} |
313 section {* lifted part *} |
277 |
314 |
278 |
315 |
279 lemma fin_finsert_iff[simp]: |
316 lemma fin_finsert_iff[simp]: |
333 |
370 |
334 lemma fcard_finsert_if [simp]: |
371 lemma fcard_finsert_if [simp]: |
335 shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))" |
372 shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))" |
336 by (lifting fcard_raw_cons) |
373 by (lifting fcard_raw_cons) |
337 |
374 |
|
375 lemma fcard_0: "(fcard a = 0) = (a = {||})" |
|
376 by (lifting fcard_raw_0) |
|
377 |
338 lemma fcard_gt_0: "x \<in> fset_to_set xs \<Longrightarrow> 0 < fcard xs" |
378 lemma fcard_gt_0: "x \<in> fset_to_set xs \<Longrightarrow> 0 < fcard xs" |
339 by (lifting fcard_raw_gt_0) |
379 by (lifting fcard_raw_gt_0) |
|
380 |
|
381 lemma fcard_not_memb: "(x |\<notin>| xs) = (fcard (finsert x xs) = Suc (fcard xs))" |
|
382 by (lifting fcard_raw_not_memb) |
|
383 |
|
384 lemma fcard_suc: "fcard xs = Suc n \<Longrightarrow> \<exists>a ys. a |\<notin>| ys \<and> xs = finsert a ys" |
|
385 by (lifting fcard_raw_suc) |
340 |
386 |
341 text {* funion *} |
387 text {* funion *} |
342 |
388 |
343 lemma funion_simps[simp]: |
389 lemma funion_simps[simp]: |
344 "{||} |\<union>| ys = ys" |
390 "{||} |\<union>| ys = ys" |
416 |
462 |
417 lemma inj_fmap_eq_iff: |
463 lemma inj_fmap_eq_iff: |
418 "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)" |
464 "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)" |
419 by (lifting inj_map_eq_iff) |
465 by (lifting inj_map_eq_iff) |
420 |
466 |
|
467 lemma fmap_funion: "fmap f (a |\<union>| b) = fmap f a |\<union>| fmap f b" |
|
468 by (lifting map_append) |
|
469 |
421 ML {* |
470 ML {* |
422 fun dest_fsetT (Type ("FSet.fset", [T])) = T |
471 fun dest_fsetT (Type ("FSet.fset", [T])) = T |
423 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
472 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
424 *} |
473 *} |
425 |
474 |