author | haftmann |
Fri, 06 Jan 2012 10:19:49 +0100 | |
changeset 46133 | d9fe85d3d2cd |
parent 46127 | af3b95160b59 |
child 46143 | c932c80d3eae |
permissions | -rw-r--r-- |
31807 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
||
4 |
header {* Relating (finite) sets and lists *} |
|
5 |
||
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
6 |
theory More_Set |
45990
b7b905b23b2a
incorporated More_Set and More_List into the Main body -- to be consolidated later
haftmann
parents:
45986
diff
changeset
|
7 |
imports More_List |
31807 | 8 |
begin |
9 |
||
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
10 |
lemma comp_fun_idem_remove: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
11 |
"comp_fun_idem Set.remove" |
31807 | 12 |
proof - |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
13 |
have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
14 |
show ?thesis by (simp only: comp_fun_idem_remove rem) |
31807 | 15 |
qed |
16 |
||
17 |
lemma minus_fold_remove: |
|
18 |
assumes "finite A" |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
19 |
shows "B - A = Finite_Set.fold Set.remove B A" |
31807 | 20 |
proof - |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
21 |
have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
31807 | 22 |
show ?thesis by (simp only: rem assms minus_fold_remove) |
23 |
qed |
|
24 |
||
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
45990
diff
changeset
|
25 |
lemma bounded_Collect_code: (* FIXME delete candidate *) |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
26 |
"{x \<in> A. P x} = Set.project P A" |
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
27 |
by (simp add: project_def) |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
28 |
|
31807 | 29 |
|
30 |
subsection {* Basic set operations *} |
|
31 |
||
46127 | 32 |
lemma is_empty_set [code]: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
33 |
"Set.is_empty (set xs) \<longleftrightarrow> List.null xs" |
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
34 |
by (simp add: Set.is_empty_def null_def) |
31807 | 35 |
|
46127 | 36 |
lemma empty_set [code]: |
31807 | 37 |
"{} = set []" |
38 |
by simp |
|
39 |
||
32880 | 40 |
lemma insert_set_compl: |
34977 | 41 |
"insert x (- set xs) = - set (removeAll x xs)" |
42 |
by auto |
|
31807 | 43 |
|
32880 | 44 |
lemma remove_set_compl: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
45 |
"Set.remove x (- set xs) = - set (List.insert x xs)" |
44326 | 46 |
by (auto simp add: remove_def List.insert_def) |
32880 | 47 |
|
31807 | 48 |
lemma image_set: |
31846 | 49 |
"image f (set xs) = set (map f xs)" |
31807 | 50 |
by simp |
51 |
||
52 |
lemma project_set: |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
53 |
"Set.project P (set xs) = set (filter P xs)" |
31807 | 54 |
by (auto simp add: project_def) |
55 |
||
56 |
||
57 |
subsection {* Functorial set operations *} |
|
58 |
||
59 |
lemma union_set: |
|
37023 | 60 |
"set xs \<union> A = fold Set.insert xs A" |
31807 | 61 |
proof - |
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
62 |
interpret comp_fun_idem Set.insert |
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
63 |
by (fact comp_fun_idem_insert) |
45990
b7b905b23b2a
incorporated More_Set and More_List into the Main body -- to be consolidated later
haftmann
parents:
45986
diff
changeset
|
64 |
show ?thesis by (simp add: union_fold_insert fold_set_fold) |
31807 | 65 |
qed |
66 |
||
37023 | 67 |
lemma union_set_foldr: |
68 |
"set xs \<union> A = foldr Set.insert xs A" |
|
69 |
proof - |
|
70 |
have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y" |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
71 |
by auto |
37023 | 72 |
then show ?thesis by (simp add: union_set foldr_fold) |
73 |
qed |
|
74 |
||
31807 | 75 |
lemma minus_set: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
76 |
"A - set xs = fold Set.remove xs A" |
31807 | 77 |
proof - |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
78 |
interpret comp_fun_idem Set.remove |
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
79 |
by (fact comp_fun_idem_remove) |
31807 | 80 |
show ?thesis |
45990
b7b905b23b2a
incorporated More_Set and More_List into the Main body -- to be consolidated later
haftmann
parents:
45986
diff
changeset
|
81 |
by (simp add: minus_fold_remove [of _ A] fold_set_fold) |
31807 | 82 |
qed |
83 |
||
37023 | 84 |
lemma minus_set_foldr: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
85 |
"A - set xs = foldr Set.remove xs A" |
37023 | 86 |
proof - |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
87 |
have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y" |
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
88 |
by (auto simp add: remove_def) |
37023 | 89 |
then show ?thesis by (simp add: minus_set foldr_fold) |
90 |
qed |
|
91 |
||
31807 | 92 |
|
93 |
subsection {* Derived set operations *} |
|
94 |
||
46127 | 95 |
lemma member [code]: |
31807 | 96 |
"a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)" |
97 |
by simp |
|
98 |
||
46127 | 99 |
lemma subset [code]: |
31807 | 100 |
"A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A" |
101 |
by (fact less_le_not_le) |
|
102 |
||
46127 | 103 |
lemma set_eq [code]: |
31807 | 104 |
"A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
105 |
by (fact eq_iff) |
|
106 |
||
46127 | 107 |
lemma inter [code]: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
108 |
"A \<inter> B = Set.project (\<lambda>x. x \<in> A) B" |
31807 | 109 |
by (auto simp add: project_def) |
110 |
||
37023 | 111 |
|
45974 | 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 |
||
119 |
||
120 |
subsection {* Basic operations *} |
|
121 |
||
122 |
lemma [code]: |
|
123 |
"x \<in> set xs \<longleftrightarrow> List.member xs x" |
|
124 |
"x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x" |
|
125 |
by (simp_all add: member_def) |
|
126 |
||
127 |
lemma UNIV_coset [code]: |
|
128 |
"UNIV = coset []" |
|
129 |
by simp |
|
130 |
||
131 |
lemma insert_code [code]: |
|
132 |
"insert x (set xs) = set (List.insert x xs)" |
|
133 |
"insert x (coset xs) = coset (removeAll x xs)" |
|
134 |
by simp_all |
|
135 |
||
136 |
lemma remove_code [code]: |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
137 |
"Set.remove x (set xs) = set (removeAll x xs)" |
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
138 |
"Set.remove x (coset xs) = coset (List.insert x xs)" |
45974 | 139 |
by (simp_all add: remove_def Compl_insert) |
140 |
||
141 |
lemma Ball_set [code]: |
|
142 |
"Ball (set xs) P \<longleftrightarrow> list_all P xs" |
|
143 |
by (simp add: list_all_iff) |
|
144 |
||
145 |
lemma Bex_set [code]: |
|
146 |
"Bex (set xs) P \<longleftrightarrow> list_ex P xs" |
|
147 |
by (simp add: list_ex_iff) |
|
148 |
||
149 |
lemma card_set [code]: |
|
150 |
"card (set xs) = length (remdups xs)" |
|
151 |
proof - |
|
152 |
have "card (set (remdups xs)) = length (remdups xs)" |
|
153 |
by (rule distinct_card) simp |
|
154 |
then show ?thesis by simp |
|
155 |
qed |
|
156 |
||
157 |
||
158 |
subsection {* Functorial operations *} |
|
159 |
||
160 |
lemma inter_code [code]: |
|
161 |
"A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
162 |
"A \<inter> coset xs = foldr Set.remove xs A" |
45974 | 163 |
by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) |
164 |
||
165 |
lemma subtract_code [code]: |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
166 |
"A - set xs = foldr Set.remove xs A" |
45974 | 167 |
"A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
168 |
by (auto simp add: minus_set_foldr) |
|
169 |
||
170 |
lemma union_code [code]: |
|
171 |
"set xs \<union> A = foldr insert xs A" |
|
172 |
"coset xs \<union> A = coset (List.filter (\<lambda>x. x \<notin> A) xs)" |
|
173 |
by (auto simp add: union_set_foldr) |
|
174 |
||
175 |
definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where |
|
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
45990
diff
changeset
|
176 |
[simp, code_abbrev]: "Inf = Complete_Lattices.Inf" |
45974 | 177 |
|
178 |
hide_const (open) Inf |
|
179 |
||
180 |
definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where |
|
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
45990
diff
changeset
|
181 |
[simp, code_abbrev]: "Sup = Complete_Lattices.Sup" |
45974 | 182 |
|
183 |
hide_const (open) Sup |
|
184 |
||
185 |
lemma Inf_code [code]: |
|
186 |
"More_Set.Inf (set xs) = foldr inf xs top" |
|
187 |
"More_Set.Inf (coset []) = bot" |
|
188 |
by (simp_all add: Inf_set_foldr) |
|
189 |
||
190 |
lemma Sup_sup [code]: |
|
191 |
"More_Set.Sup (set xs) = foldr sup xs bot" |
|
192 |
"More_Set.Sup (coset []) = top" |
|
193 |
by (simp_all add: Sup_set_foldr) |
|
194 |
||
46037 | 195 |
(* FIXME: better implement conversion by bisection *) |
196 |
||
197 |
lemma pred_of_set_fold_sup: |
|
198 |
assumes "finite A" |
|
199 |
shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs") |
|
200 |
proof (rule sym) |
|
201 |
interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred" |
|
202 |
by (fact comp_fun_idem_sup) |
|
203 |
from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI) |
|
204 |
qed |
|
205 |
||
206 |
lemma pred_of_set_set_fold_sup: |
|
207 |
"pred_of_set (set xs) = fold sup (map Predicate.single xs) bot" |
|
208 |
proof - |
|
209 |
interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred" |
|
210 |
by (fact comp_fun_idem_sup) |
|
211 |
show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric]) |
|
212 |
qed |
|
213 |
||
214 |
lemma pred_of_set_set_foldr_sup [code]: |
|
215 |
"pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot" |
|
216 |
by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff) |
|
217 |
||
45974 | 218 |
|
219 |
subsection {* Operations on relations *} |
|
220 |
||
46127 | 221 |
lemma product_code [code]: |
222 |
"Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]" |
|
223 |
by (auto simp add: Product_Type.product_def) |
|
45974 | 224 |
|
46127 | 225 |
lemma Id_on_set [code]: |
226 |
"Id_on (set xs) = set [(x, x). x \<leftarrow> xs]" |
|
227 |
by (auto simp add: Id_on_def) |
|
45974 | 228 |
|
46127 | 229 |
lemma trancl_set_ntrancl [code]: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" |
230 |
by (simp add: finite_trancl_ntranl) |
|
45974 | 231 |
|
46127 | 232 |
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])" |
|
234 |
by (auto simp add: Bex_def) |
|
45974 | 235 |
|
46127 | 236 |
lemma wf_set [code]: |
237 |
"wf (set xs) = acyclic (set xs)" |
|
238 |
by (simp add: wf_iff_acyclic_if_finite) |
|
45974 | 239 |
|
240 |
end |
|
241 |