4 header {* Relating (finite) sets and lists *} |
4 header {* Relating (finite) sets and lists *} |
5 |
5 |
6 theory More_Set |
6 theory More_Set |
7 imports List |
7 imports List |
8 begin |
8 begin |
9 |
|
10 lemma comp_fun_idem_remove: |
|
11 "comp_fun_idem Set.remove" |
|
12 proof - |
|
13 have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
|
14 show ?thesis by (simp only: comp_fun_idem_remove rem) |
|
15 qed |
|
16 |
|
17 lemma minus_fold_remove: |
|
18 assumes "finite A" |
|
19 shows "B - A = Finite_Set.fold Set.remove B A" |
|
20 proof - |
|
21 have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
|
22 show ?thesis by (simp only: rem assms minus_fold_remove) |
|
23 qed |
|
24 |
|
25 lemma bounded_Collect_code: (* FIXME delete candidate *) |
|
26 "{x \<in> A. P x} = Set.project P A" |
|
27 by (simp add: project_def) |
|
28 |
|
29 |
9 |
30 subsection {* Basic set operations *} |
10 subsection {* Basic set operations *} |
31 |
11 |
32 lemma is_empty_set [code]: |
12 lemma is_empty_set [code]: |
33 "Set.is_empty (set xs) \<longleftrightarrow> List.null xs" |
13 "Set.is_empty (set xs) \<longleftrightarrow> List.null xs" |
35 |
15 |
36 lemma empty_set [code]: |
16 lemma empty_set [code]: |
37 "{} = set []" |
17 "{} = set []" |
38 by simp |
18 by simp |
39 |
19 |
40 lemma insert_set_compl: |
|
41 "insert x (- set xs) = - set (removeAll x xs)" |
|
42 by auto |
|
43 |
|
44 lemma remove_set_compl: |
|
45 "Set.remove x (- set xs) = - set (List.insert x xs)" |
|
46 by (auto simp add: remove_def List.insert_def) |
|
47 |
|
48 lemma image_set: |
|
49 "image f (set xs) = set (map f xs)" |
|
50 by simp |
|
51 |
|
52 lemma project_set: |
|
53 "Set.project P (set xs) = set (filter P xs)" |
|
54 by (auto simp add: project_def) |
|
55 |
|
56 |
20 |
57 subsection {* Functorial set operations *} |
21 subsection {* Functorial set operations *} |
58 |
22 |
59 lemma union_set: |
23 lemma union_set_fold: |
60 "set xs \<union> A = fold Set.insert xs A" |
24 "set xs \<union> A = fold Set.insert xs A" |
61 proof - |
25 proof - |
62 interpret comp_fun_idem Set.insert |
26 interpret comp_fun_idem Set.insert |
63 by (fact comp_fun_idem_insert) |
27 by (fact comp_fun_idem_insert) |
64 show ?thesis by (simp add: union_fold_insert fold_set_fold) |
28 show ?thesis by (simp add: union_fold_insert fold_set_fold) |
67 lemma union_set_foldr: |
31 lemma union_set_foldr: |
68 "set xs \<union> A = foldr Set.insert xs A" |
32 "set xs \<union> A = foldr Set.insert xs A" |
69 proof - |
33 proof - |
70 have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y" |
34 have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y" |
71 by auto |
35 by auto |
72 then show ?thesis by (simp add: union_set foldr_fold) |
36 then show ?thesis by (simp add: union_set_fold foldr_fold) |
73 qed |
37 qed |
74 |
38 |
75 lemma minus_set: |
39 lemma minus_set_fold: |
76 "A - set xs = fold Set.remove xs A" |
40 "A - set xs = fold Set.remove xs A" |
77 proof - |
41 proof - |
78 interpret comp_fun_idem Set.remove |
42 interpret comp_fun_idem Set.remove |
79 by (fact comp_fun_idem_remove) |
43 by (fact comp_fun_idem_remove) |
80 show ?thesis |
44 show ?thesis |
84 lemma minus_set_foldr: |
48 lemma minus_set_foldr: |
85 "A - set xs = foldr Set.remove xs A" |
49 "A - set xs = foldr Set.remove xs A" |
86 proof - |
50 proof - |
87 have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y" |
51 have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y" |
88 by (auto simp add: remove_def) |
52 by (auto simp add: remove_def) |
89 then show ?thesis by (simp add: minus_set foldr_fold) |
53 then show ?thesis by (simp add: minus_set_fold foldr_fold) |
90 qed |
54 qed |
91 |
|
92 |
|
93 subsection {* Derived set operations *} |
|
94 |
|
95 lemma member [code]: |
|
96 "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)" |
|
97 by simp |
|
98 |
|
99 lemma subset [code]: |
|
100 "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A" |
|
101 by (fact less_le_not_le) |
|
102 |
|
103 lemma set_eq [code]: |
|
104 "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
|
105 by (fact eq_iff) |
|
106 |
|
107 lemma inter [code]: |
|
108 "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B" |
|
109 by (auto simp add: project_def) |
|
110 |
|
111 |
|
112 subsection {* Code generator setup *} |
|
113 |
|
114 definition coset :: "'a list \<Rightarrow> 'a set" where |
|
115 [simp]: "coset xs = - set xs" |
|
116 |
|
117 code_datatype set coset |
|
118 |
55 |
119 |
56 |
120 subsection {* Basic operations *} |
57 subsection {* Basic operations *} |
121 |
58 |
122 lemma [code]: |
59 lemma [code]: |
123 "x \<in> set xs \<longleftrightarrow> List.member xs x" |
60 "x \<in> set xs \<longleftrightarrow> List.member xs x" |
124 "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x" |
61 "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x" |
125 by (simp_all add: member_def) |
62 by (simp_all add: member_def) |
126 |
63 |
127 lemma UNIV_coset [code]: |
64 lemma UNIV_coset [code]: |
128 "UNIV = coset []" |
65 "UNIV = List.coset []" |
129 by simp |
66 by simp |
130 |
67 |
131 lemma insert_code [code]: |
68 lemma insert_code [code]: |
132 "insert x (set xs) = set (List.insert x xs)" |
69 "insert x (set xs) = set (List.insert x xs)" |
133 "insert x (coset xs) = coset (removeAll x xs)" |
70 "insert x (List.coset xs) = List.coset (removeAll x xs)" |
134 by simp_all |
71 by simp_all |
135 |
72 |
136 lemma remove_code [code]: |
73 lemma remove_code [code]: |
137 "Set.remove x (set xs) = set (removeAll x xs)" |
74 "Set.remove x (set xs) = set (removeAll x xs)" |
138 "Set.remove x (coset xs) = coset (List.insert x xs)" |
75 "Set.remove x (List.coset xs) = List.coset (List.insert x xs)" |
139 by (simp_all add: remove_def Compl_insert) |
76 by (simp_all add: remove_def Compl_insert) |
140 |
77 |
141 lemma Ball_set [code]: |
78 lemma Ball_set [code]: |
142 "Ball (set xs) P \<longleftrightarrow> list_all P xs" |
79 "Ball (set xs) P \<longleftrightarrow> list_all P xs" |
143 by (simp add: list_all_iff) |
80 by (simp add: list_all_iff) |
157 |
94 |
158 subsection {* Functorial operations *} |
95 subsection {* Functorial operations *} |
159 |
96 |
160 lemma inter_code [code]: |
97 lemma inter_code [code]: |
161 "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
98 "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
162 "A \<inter> coset xs = foldr Set.remove xs A" |
99 "A \<inter> List.coset xs = foldr Set.remove xs A" |
163 by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) |
100 by (simp add: inter_project project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) |
164 |
101 |
165 lemma subtract_code [code]: |
102 lemma subtract_code [code]: |
166 "A - set xs = foldr Set.remove xs A" |
103 "A - set xs = foldr Set.remove xs A" |
167 "A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
104 "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
168 by (auto simp add: minus_set_foldr) |
105 by (auto simp add: minus_set_foldr) |
169 |
106 |
170 lemma union_code [code]: |
107 lemma union_code [code]: |
171 "set xs \<union> A = foldr insert xs A" |
108 "set xs \<union> A = foldr insert xs A" |
172 "coset xs \<union> A = coset (List.filter (\<lambda>x. x \<notin> A) xs)" |
109 "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)" |
173 by (auto simp add: union_set_foldr) |
110 by (auto simp add: union_set_foldr) |
174 |
111 |
175 definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where |
112 definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where |
176 [simp, code_abbrev]: "Inf = Complete_Lattices.Inf" |
113 [simp, code_abbrev]: "Inf = Complete_Lattices.Inf" |
177 |
114 |
182 |
119 |
183 hide_const (open) Sup |
120 hide_const (open) Sup |
184 |
121 |
185 lemma Inf_code [code]: |
122 lemma Inf_code [code]: |
186 "More_Set.Inf (set xs) = foldr inf xs top" |
123 "More_Set.Inf (set xs) = foldr inf xs top" |
187 "More_Set.Inf (coset []) = bot" |
124 "More_Set.Inf (List.coset []) = bot" |
188 by (simp_all add: Inf_set_foldr) |
125 by (simp_all add: Inf_set_foldr) |
189 |
126 |
190 lemma Sup_sup [code]: |
127 lemma Sup_sup [code]: |
191 "More_Set.Sup (set xs) = foldr sup xs bot" |
128 "More_Set.Sup (set xs) = foldr sup xs bot" |
192 "More_Set.Sup (coset []) = top" |
129 "More_Set.Sup (List.coset []) = top" |
193 by (simp_all add: Sup_set_foldr) |
130 by (simp_all add: Sup_set_foldr) |
194 |
131 |
195 (* FIXME: better implement conversion by bisection *) |
132 (* FIXME: better implement conversion by bisection *) |
196 |
133 |
197 lemma pred_of_set_fold_sup: |
134 lemma pred_of_set_fold_sup: |
224 |
161 |
225 lemma Id_on_set [code]: |
162 lemma Id_on_set [code]: |
226 "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]" |
163 "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]" |
227 by (auto simp add: Id_on_def) |
164 by (auto simp add: Id_on_def) |
228 |
165 |
229 lemma trancl_set_ntrancl [code]: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" |
166 lemma trancl_set_ntrancl [code]: |
|
167 "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" |
230 by (simp add: finite_trancl_ntranl) |
168 by (simp add: finite_trancl_ntranl) |
231 |
169 |
232 lemma set_rel_comp [code]: |
170 lemma set_rel_comp [code]: |
233 "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])" |
171 "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])" |
234 by (auto simp add: Bex_def) |
172 by (auto simp add: Bex_def) |