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