author | haftmann |
Thu, 18 Nov 2010 17:01:16 +0100 | |
changeset 40606 | af1a0b0c6202 |
parent 40604 | c0770657c8de |
permissions | -rw-r--r-- |
31807 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
||
39929 | 4 |
header {* A set type which is executable on its finite part *} |
31807 | 5 |
|
31849 | 6 |
theory Fset |
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
7 |
imports More_Set More_List |
31807 | 8 |
begin |
9 |
||
10 |
subsection {* Lifting *} |
|
11 |
||
37468 | 12 |
typedef (open) 'a fset = "UNIV :: 'a set set" |
13 |
morphisms member Fset by rule+ |
|
31807 | 14 |
|
37468 | 15 |
lemma member_Fset [simp]: |
31807 | 16 |
"member (Fset A) = A" |
37468 | 17 |
by (rule Fset_inverse) rule |
34048 | 18 |
|
31807 | 19 |
lemma Fset_member [simp]: |
20 |
"Fset (member A) = A" |
|
37699 | 21 |
by (fact member_inverse) |
37468 | 22 |
|
23 |
lemma Fset_inject [simp]: |
|
24 |
"Fset A = Fset B \<longleftrightarrow> A = B" |
|
25 |
by (simp add: Fset_inject) |
|
26 |
||
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
27 |
lemma fset_eq_iff: |
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
28 |
"A = B \<longleftrightarrow> member A = member B" |
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
29 |
by (simp add: member_inject) |
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
30 |
|
37473 | 31 |
lemma fset_eqI: |
32 |
"member A = member B \<Longrightarrow> A = B" |
|
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
33 |
by (simp add: fset_eq_iff) |
37473 | 34 |
|
37468 | 35 |
declare mem_def [simp] |
31807 | 36 |
|
37 |
definition Set :: "'a list \<Rightarrow> 'a fset" where |
|
38 |
"Set xs = Fset (set xs)" |
|
39 |
||
40 |
lemma member_Set [simp]: |
|
41 |
"member (Set xs) = set xs" |
|
42 |
by (simp add: Set_def) |
|
43 |
||
32880 | 44 |
definition Coset :: "'a list \<Rightarrow> 'a fset" where |
45 |
"Coset xs = Fset (- set xs)" |
|
46 |
||
47 |
lemma member_Coset [simp]: |
|
48 |
"member (Coset xs) = - set xs" |
|
49 |
by (simp add: Coset_def) |
|
50 |
||
51 |
code_datatype Set Coset |
|
52 |
||
53 |
lemma member_code [code]: |
|
37023 | 54 |
"member (Set xs) = List.member xs" |
55 |
"member (Coset xs) = Not \<circ> List.member xs" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39200
diff
changeset
|
56 |
by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def) |
32880 | 57 |
|
58 |
lemma member_image_UNIV [simp]: |
|
59 |
"member ` UNIV = UNIV" |
|
60 |
proof - |
|
61 |
have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a fset. A = member B" |
|
62 |
proof |
|
63 |
fix A :: "'a set" |
|
64 |
show "A = member (Fset A)" by simp |
|
65 |
qed |
|
66 |
then show ?thesis by (simp add: image_def) |
|
67 |
qed |
|
31807 | 68 |
|
37468 | 69 |
definition (in term_syntax) |
70 |
setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term) |
|
71 |
\<Rightarrow> 'a fset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
|
72 |
[code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\<cdot>} xs" |
|
73 |
||
37751 | 74 |
notation fcomp (infixl "\<circ>>" 60) |
75 |
notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
37468 | 76 |
|
77 |
instantiation fset :: (random) random |
|
78 |
begin |
|
79 |
||
80 |
definition |
|
37751 | 81 |
"Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))" |
37468 | 82 |
|
83 |
instance .. |
|
84 |
||
85 |
end |
|
86 |
||
37751 | 87 |
no_notation fcomp (infixl "\<circ>>" 60) |
88 |
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
37468 | 89 |
|
31807 | 90 |
|
34048 | 91 |
subsection {* Lattice instantiation *} |
92 |
||
93 |
instantiation fset :: (type) boolean_algebra |
|
94 |
begin |
|
95 |
||
96 |
definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
97 |
[simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B" |
|
98 |
||
99 |
definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
100 |
[simp]: "A < B \<longleftrightarrow> member A \<subset> member B" |
|
101 |
||
102 |
definition inf_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
103 |
[simp]: "inf A B = Fset (member A \<inter> member B)" |
|
104 |
||
105 |
definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
106 |
[simp]: "sup A B = Fset (member A \<union> member B)" |
|
107 |
||
108 |
definition bot_fset :: "'a fset" where |
|
109 |
[simp]: "bot = Fset {}" |
|
110 |
||
111 |
definition top_fset :: "'a fset" where |
|
112 |
[simp]: "top = Fset UNIV" |
|
113 |
||
114 |
definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" where |
|
115 |
[simp]: "- A = Fset (- (member A))" |
|
116 |
||
117 |
definition minus_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
118 |
[simp]: "A - B = Fset (member A - member B)" |
|
119 |
||
120 |
instance proof |
|
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
121 |
qed (auto intro: fset_eqI) |
34048 | 122 |
|
123 |
end |
|
124 |
||
125 |
instantiation fset :: (type) complete_lattice |
|
126 |
begin |
|
127 |
||
128 |
definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" where |
|
37765 | 129 |
[simp]: "Inf_fset As = Fset (Inf (image member As))" |
34048 | 130 |
|
131 |
definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" where |
|
37765 | 132 |
[simp]: "Sup_fset As = Fset (Sup (image member As))" |
34048 | 133 |
|
134 |
instance proof |
|
135 |
qed (auto simp add: le_fun_def le_bool_def) |
|
136 |
||
137 |
end |
|
138 |
||
37023 | 139 |
|
31807 | 140 |
subsection {* Basic operations *} |
141 |
||
142 |
definition is_empty :: "'a fset \<Rightarrow> bool" where |
|
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
143 |
[simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)" |
31807 | 144 |
|
145 |
lemma is_empty_Set [code]: |
|
37595
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37473
diff
changeset
|
146 |
"is_empty (Set xs) \<longleftrightarrow> List.null xs" |
31846 | 147 |
by (simp add: is_empty_set) |
31807 | 148 |
|
34048 | 149 |
lemma empty_Set [code]: |
150 |
"bot = Set []" |
|
37468 | 151 |
by (simp add: Set_def) |
31807 | 152 |
|
34048 | 153 |
lemma UNIV_Set [code]: |
154 |
"top = Coset []" |
|
37468 | 155 |
by (simp add: Coset_def) |
31807 | 156 |
|
157 |
definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
31846 | 158 |
[simp]: "insert x A = Fset (Set.insert x (member A))" |
31807 | 159 |
|
160 |
lemma insert_Set [code]: |
|
34976
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
161 |
"insert x (Set xs) = Set (List.insert x xs)" |
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
162 |
"insert x (Coset xs) = Coset (removeAll x xs)" |
37023 | 163 |
by (simp_all add: Set_def Coset_def) |
31807 | 164 |
|
165 |
definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
166 |
[simp]: "remove x A = Fset (More_Set.remove x (member A))" |
31807 | 167 |
|
168 |
lemma remove_Set [code]: |
|
34976
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
169 |
"remove x (Set xs) = Set (removeAll x xs)" |
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
170 |
"remove x (Coset xs) = Coset (List.insert x xs)" |
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
171 |
by (simp_all add: Set_def Coset_def remove_set_compl) |
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
172 |
(simp add: More_Set.remove_def) |
31807 | 173 |
|
174 |
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where |
|
31846 | 175 |
[simp]: "map f A = Fset (image f (member A))" |
31807 | 176 |
|
177 |
lemma map_Set [code]: |
|
178 |
"map f (Set xs) = Set (remdups (List.map f xs))" |
|
31846 | 179 |
by (simp add: Set_def) |
31807 | 180 |
|
40604 | 181 |
type_mapper map |
182 |
by (simp_all add: image_image) |
|
183 |
||
31847 | 184 |
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
185 |
[simp]: "filter P A = Fset (More_Set.project P (member A))" |
31807 | 186 |
|
31847 | 187 |
lemma filter_Set [code]: |
188 |
"filter P (Set xs) = Set (List.filter P xs)" |
|
31846 | 189 |
by (simp add: Set_def project_set) |
31807 | 190 |
|
191 |
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
31846 | 192 |
[simp]: "forall P A \<longleftrightarrow> Ball (member A) P" |
31807 | 193 |
|
194 |
lemma forall_Set [code]: |
|
195 |
"forall P (Set xs) \<longleftrightarrow> list_all P xs" |
|
37595
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37473
diff
changeset
|
196 |
by (simp add: Set_def list_all_iff) |
31807 | 197 |
|
198 |
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
31846 | 199 |
[simp]: "exists P A \<longleftrightarrow> Bex (member A) P" |
31807 | 200 |
|
201 |
lemma exists_Set [code]: |
|
202 |
"exists P (Set xs) \<longleftrightarrow> list_ex P xs" |
|
37595
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37473
diff
changeset
|
203 |
by (simp add: Set_def list_ex_iff) |
31846 | 204 |
|
31849 | 205 |
definition card :: "'a fset \<Rightarrow> nat" where |
206 |
[simp]: "card A = Finite_Set.card (member A)" |
|
207 |
||
208 |
lemma card_Set [code]: |
|
209 |
"card (Set xs) = length (remdups xs)" |
|
210 |
proof - |
|
211 |
have "Finite_Set.card (set (remdups xs)) = length (remdups xs)" |
|
212 |
by (rule distinct_card) simp |
|
37023 | 213 |
then show ?thesis by (simp add: Set_def) |
31849 | 214 |
qed |
215 |
||
37023 | 216 |
lemma compl_Set [simp, code]: |
217 |
"- Set xs = Coset xs" |
|
218 |
by (simp add: Set_def Coset_def) |
|
219 |
||
220 |
lemma compl_Coset [simp, code]: |
|
221 |
"- Coset xs = Set xs" |
|
222 |
by (simp add: Set_def Coset_def) |
|
223 |
||
31846 | 224 |
|
225 |
subsection {* Derived operations *} |
|
226 |
||
227 |
lemma subfset_eq_forall [code]: |
|
34048 | 228 |
"A \<le> B \<longleftrightarrow> forall (member B) A" |
31846 | 229 |
by (simp add: subset_eq) |
230 |
||
231 |
lemma subfset_subfset_eq [code]: |
|
34048 | 232 |
"A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)" |
233 |
by (fact less_le_not_le) |
|
31846 | 234 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset
|
235 |
instantiation fset :: (type) equal |
37468 | 236 |
begin |
237 |
||
39190
a2775776be3f
adding code attribute to definition of equality of finite sets for executability of equality of finite sets
bulwahn
parents:
38857
diff
changeset
|
238 |
definition [code]: |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset
|
239 |
"HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)" |
37468 | 240 |
|
241 |
instance proof |
|
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
242 |
qed (simp add: equal_fset_def set_eq [symmetric] fset_eq_iff) |
37468 | 243 |
|
244 |
end |
|
31846 | 245 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset
|
246 |
lemma [code nbe]: |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset
|
247 |
"HOL.equal (A :: 'a fset) A \<longleftrightarrow> True" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset
|
248 |
by (fact equal_refl) |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset
|
249 |
|
31807 | 250 |
|
251 |
subsection {* Functorial operations *} |
|
252 |
||
32880 | 253 |
lemma inter_project [code]: |
34048 | 254 |
"inf A (Set xs) = Set (List.filter (member A) xs)" |
37023 | 255 |
"inf A (Coset xs) = foldr remove xs A" |
31807 | 256 |
proof - |
34048 | 257 |
show "inf A (Set xs) = Set (List.filter (member A) xs)" |
32880 | 258 |
by (simp add: inter project_def Set_def) |
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
259 |
have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member)" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39200
diff
changeset
|
260 |
by (simp add: fun_eq_iff) |
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
261 |
have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs = |
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
262 |
fold More_Set.remove xs \<circ> member" |
39921 | 263 |
by (rule fold_commute) (simp add: fun_eq_iff) |
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
264 |
then have "fold More_Set.remove xs (member A) = |
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
265 |
member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39200
diff
changeset
|
266 |
by (simp add: fun_eq_iff) |
37023 | 267 |
then have "inf A (Coset xs) = fold remove xs A" |
268 |
by (simp add: Diff_eq [symmetric] minus_set *) |
|
269 |
moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y" |
|
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
270 |
by (auto simp add: More_Set.remove_def * intro: ext) |
37023 | 271 |
ultimately show "inf A (Coset xs) = foldr remove xs A" |
272 |
by (simp add: foldr_fold) |
|
31807 | 273 |
qed |
274 |
||
275 |
lemma subtract_remove [code]: |
|
37023 | 276 |
"A - Set xs = foldr remove xs A" |
34048 | 277 |
"A - Coset xs = Set (List.filter (member A) xs)" |
37023 | 278 |
by (simp_all only: diff_eq compl_Set compl_Coset inter_project) |
32880 | 279 |
|
280 |
lemma union_insert [code]: |
|
37023 | 281 |
"sup (Set xs) A = foldr insert xs A" |
34048 | 282 |
"sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)" |
32880 | 283 |
proof - |
37023 | 284 |
have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39200
diff
changeset
|
285 |
by (simp add: fun_eq_iff) |
37023 | 286 |
have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs = |
287 |
fold Set.insert xs \<circ> member" |
|
39921 | 288 |
by (rule fold_commute) (simp add: fun_eq_iff) |
37023 | 289 |
then have "fold Set.insert xs (member A) = |
290 |
member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39200
diff
changeset
|
291 |
by (simp add: fun_eq_iff) |
37023 | 292 |
then have "sup (Set xs) A = fold insert xs A" |
293 |
by (simp add: union_set *) |
|
294 |
moreover have "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y" |
|
295 |
by (auto simp add: * intro: ext) |
|
296 |
ultimately show "sup (Set xs) A = foldr insert xs A" |
|
297 |
by (simp add: foldr_fold) |
|
34048 | 298 |
show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)" |
32880 | 299 |
by (auto simp add: Coset_def) |
31807 | 300 |
qed |
301 |
||
34048 | 302 |
context complete_lattice |
303 |
begin |
|
31807 | 304 |
|
34048 | 305 |
definition Infimum :: "'a fset \<Rightarrow> 'a" where |
306 |
[simp]: "Infimum A = Inf (member A)" |
|
31807 | 307 |
|
34048 | 308 |
lemma Infimum_inf [code]: |
37023 | 309 |
"Infimum (Set As) = foldr inf As top" |
34048 | 310 |
"Infimum (Coset []) = bot" |
37023 | 311 |
by (simp_all add: Inf_set_foldr Inf_UNIV) |
31807 | 312 |
|
34048 | 313 |
definition Supremum :: "'a fset \<Rightarrow> 'a" where |
314 |
[simp]: "Supremum A = Sup (member A)" |
|
315 |
||
316 |
lemma Supremum_sup [code]: |
|
37023 | 317 |
"Supremum (Set As) = foldr sup As bot" |
34048 | 318 |
"Supremum (Coset []) = top" |
37023 | 319 |
by (simp_all add: Sup_set_foldr Sup_UNIV) |
34048 | 320 |
|
321 |
end |
|
31807 | 322 |
|
323 |
||
31846 | 324 |
subsection {* Simplified simprules *} |
325 |
||
326 |
lemma is_empty_simp [simp]: |
|
327 |
"is_empty A \<longleftrightarrow> member A = {}" |
|
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
328 |
by (simp add: More_Set.is_empty_def) |
31846 | 329 |
declare is_empty_def [simp del] |
330 |
||
331 |
lemma remove_simp [simp]: |
|
332 |
"remove x A = Fset (member A - {x})" |
|
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
333 |
by (simp add: More_Set.remove_def) |
31846 | 334 |
declare remove_def [simp del] |
335 |
||
31847 | 336 |
lemma filter_simp [simp]: |
337 |
"filter P A = Fset {x \<in> member A. P x}" |
|
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
338 |
by (simp add: More_Set.project_def) |
31847 | 339 |
declare filter_def [simp del] |
31846 | 340 |
|
341 |
declare mem_def [simp del] |
|
342 |
||
31849 | 343 |
|
37468 | 344 |
hide_const (open) setify is_empty insert remove map filter forall exists card |
34048 | 345 |
Inter Union |
31849 | 346 |
|
31807 | 347 |
end |