equal
deleted
inserted
replaced
47 |
47 |
48 lemma [code, code del]: |
48 lemma [code, code del]: |
49 "UNIV = UNIV" .. |
49 "UNIV = UNIV" .. |
50 |
50 |
51 lemma [code, code del]: |
51 lemma [code, code del]: |
52 "Set.project = Set.project" .. |
52 "Set.filter = Set.filter" .. |
53 |
53 |
54 lemma [code, code del]: |
54 lemma [code, code del]: |
55 "image = image" .. |
55 "image = image" .. |
56 |
56 |
57 lemma [code, code del]: |
57 lemma [code, code del]: |
600 |
600 |
601 lemma minus_Coset [code]: |
601 lemma minus_Coset [code]: |
602 "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t" |
602 "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t" |
603 by (simp add: inter_Set[simplified Int_commute]) |
603 by (simp add: inter_Set[simplified Int_commute]) |
604 |
604 |
605 lemma project_Set [code]: |
605 lemma filter_Set [code]: |
606 "Set.project P (Set t) = (rbt_filter P t)" |
606 "Set.filter P (Set t) = (rbt_filter P t)" |
607 by (auto simp add: project_filter finite_filter_rbt_filter) |
607 by (auto simp add: project_filter finite_filter_rbt_filter) |
608 |
608 |
609 lemma image_Set [code]: |
609 lemma image_Set [code]: |
610 "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}" |
610 "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}" |
611 proof - |
611 proof - |