1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 header {* Relating (finite) sets and lists *} |
|
5 |
|
6 theory More_Set |
|
7 imports List |
|
8 begin |
|
9 |
|
10 subsection {* Functorial operations *} |
|
11 |
|
12 lemma inter_code [code]: |
|
13 "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
|
14 "A \<inter> List.coset xs = foldr Set.remove xs A" |
|
15 by (simp add: inter_project project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) |
|
16 |
|
17 lemma subtract_code [code]: |
|
18 "A - set xs = foldr Set.remove xs A" |
|
19 "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
|
20 by (auto simp add: minus_set_foldr) |
|
21 |
|
22 lemma union_code [code]: |
|
23 "set xs \<union> A = foldr insert xs A" |
|
24 "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)" |
|
25 by (auto simp add: union_set_foldr) |
|
26 |
|
27 definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where |
|
28 [simp, code_abbrev]: "Inf = Complete_Lattices.Inf" |
|
29 |
|
30 hide_const (open) Inf |
|
31 |
|
32 definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where |
|
33 [simp, code_abbrev]: "Sup = Complete_Lattices.Sup" |
|
34 |
|
35 hide_const (open) Sup |
|
36 |
|
37 lemma Inf_code [code]: |
|
38 "More_Set.Inf (set xs) = foldr inf xs top" |
|
39 "More_Set.Inf (List.coset []) = bot" |
|
40 by (simp_all add: Inf_set_foldr) |
|
41 |
|
42 lemma Sup_sup [code]: |
|
43 "More_Set.Sup (set xs) = foldr sup xs bot" |
|
44 "More_Set.Sup (List.coset []) = top" |
|
45 by (simp_all add: Sup_set_foldr) |
|
46 |
|
47 (* FIXME: better implement conversion by bisection *) |
|
48 |
|
49 lemma pred_of_set_fold_sup: |
|
50 assumes "finite A" |
|
51 shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs") |
|
52 proof (rule sym) |
|
53 interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred" |
|
54 by (fact comp_fun_idem_sup) |
|
55 from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI) |
|
56 qed |
|
57 |
|
58 lemma pred_of_set_set_fold_sup: |
|
59 "pred_of_set (set xs) = fold sup (map Predicate.single xs) bot" |
|
60 proof - |
|
61 interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred" |
|
62 by (fact comp_fun_idem_sup) |
|
63 show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric]) |
|
64 qed |
|
65 |
|
66 lemma pred_of_set_set_foldr_sup [code]: |
|
67 "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot" |
|
68 by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff) |
|
69 |
|
70 end |
|
71 |
|