1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
|
theory Why3_Set
imports
Why3_Setup
Why3_Map
"HOL-Library.FSet"
begin
section \<open> Potentially infinite sets \<close>
definition complement :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
"complement S v = Not (S v)"
definition mapi :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool)" where
"mapi f s x = Set.member x (image f (Collect s))"
definition filteri :: " ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
"filteri f s x = conj (s x) (f x)"
definition product :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> bool)" where
"product s1 s2 p = conj (s1 (fst p)) (s2 (snd p))"
why3_open "set/Set.xml"
constants
empty = bot
add = insert
remove = Set.remove
union = sup
inter = inf
diff = minus
complement = complement
pick = Eps
all = top
map = mapi
filter = filteri
product = product
why3_vc diffqtdef by (simp add: mem_def)
why3_vc interqtdef by (simp add: mem_def)
why3_vc is_empty_empty by (simp add: constqtdef mem_def set.Set.is_empty_def)
why3_vc unionqtdef by (simp add: mem_def)
why3_vc add_remove
using assms
by (simp add: fun_upd_idem_iff mem_def)
why3_vc remove_add by auto
why3_vc pick_def
using assms
by (auto simp add: mem_def is_empty_def intro: someI_ex)
why3_vc subset_diff
by (simp add: mem_def diffqtdef subset_def)
why3_vc subset_refl
by (simp add: subset_def)
why3_vc subset_trans
using assms
by (simp add: subset_def)
why3_vc subset_remove
by (simp add: mem_def remove_def subset_def)
why3_vc complementqtdef
by (simp add: mem_def complement_def)
why3_vc extensionality
using assms
by (auto simp add: infix_eqeq_def mem_def)
why3_vc mapqtdef by (simp add: mem_def mapi_def image_iff)
why3_vc mem_map
using assms
by (meson facts.mapqtdef mem_def)
why3_vc mem_singleton
by (metis assms constqtdef fun_upd_other mem_def)
why3_vc empty_is_empty
using assms
by (metis Collect_empty_eq Collect_empty_eq_bot is_empty_empty mem_def set.Set.is_empty_def)
why3_vc subset_inter_1
by (simp add: set.Set.subset_def mem_def)
why3_vc subset_inter_2
by (simp add: set.Set.subset_def mem_def)
why3_vc subset_union_1
by (simp add: set.Set.subset_def mem_def)
why3_vc subset_union_2
by (simp add: set.Set.subset_def mem_def)
why3_vc disjoint_diff_s2
by (simp add: disjoint_def mem_def)
why3_vc disjoint_inter_empty
by (simp add: disjoint_def mem_def set.Set.is_empty_def)
why3_vc disjoint_diff_eq
by (smt diffqtdef disjoint_diff_s2 disjoint_inter_empty empty_is_empty
inf.absorb_iff2 inf.cobounded2 inf.idem inf_absorb1 interqtdef le_fun_def)
why3_vc filter_def
by (metis filteri_def mem_def)
why3_vc subset_filter
by (simp add: filter_def subset_def)
why3_vc product_def
by (simp add: product_def mem_def)
why3_end
section \<open> Finite sets \<close>
definition fremove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
"fremove x A = A - {|x|}"
definition fchoose :: "'a fset \<Rightarrow> 'a" where
"fchoose S = (\<some>x. x |\<in>| S)"
definition is_empty :: "'a fset \<Rightarrow> bool" where
"is_empty S = (S = fempty)"
definition filter :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a fset" where
"filter S p = ffilter p S"
why3_open "set/Fset.xml"
constants
mem = fmember
empty = bot
add = finsert
remove = fremove
union = sup
inter = inf
diff = minus
choose = fchoose
all = top
pick = fchoose
filter = filter
map = fimage
types
fset = fset
why3_vc add_def by auto
why3_vc add_remove
using assms
by (auto simp add: fremove_def)
why3_vc remove_add by (simp add: fremove_def)
why3_vc map_def by auto
why3_vc mem_map by (simp add: assms)
why3_vc inter_def by simp
why3_vc union_def by simp
why3_vc remove_def by (auto simp add: fremove_def)
why3_vc diff_def by auto
why3_vc pick_def
using assms
by (auto simp add: fchoose_def is_empty_def intro: someI_ex)
why3_vc subset_diff by (simp add: Fset.subset_def)
why3_vc subset_refl by (simp add: Fset.subset_def)
why3_vc subset_trans
using assms
by (simp add: Fset.subset_def)
why3_vc subset_remove by (auto simp add: Fset.subset_def fremove_def)
why3_vc subset_eq
using assms fcard_seteq
by (metis Fset.subset_def eq_imp_le fsubsetI of_nat_eq_iff)
why3_vc extensionality
using assms
by (simp add: Fset.infix_eqeq_def fset_eqI)
why3_vc cardinal1
proof (cases s rule: fset_strong_cases)
case 1
with assms
show ?thesis by (simp add: fcard_fempty)
next
case (2 s' x)
show ?thesis
proof (cases s' rule: fset_strong_cases)
case 1
with `s = finsert x s'` assms
show ?thesis by (simp add: fchoose_def)
next
case (2 s'' y)
with `s = finsert x s'` assms
show ?thesis by (auto simp add: fcard_finsert_if fchoose_def
split: if_split_asm)
qed
qed
why3_vc cardinal_add by (auto simp add: fcard_finsert_if finsert_absorb)
why3_vc cardinal_empty by (simp add: is_empty_def)
why3_vc cardinal_nonneg by simp
lemma cardinal_remove_in:
"x |\<in>| s \<longrightarrow> int (fcard (fremove x s)) = int (fcard s) - 1"
by (smt cardinal_add(2) fminus_finsert_absorb fremove_def set_finsert)
lemma cardinal_remove_out:
"x |\<notin>| s \<longrightarrow> int (fcard (fremove x s)) = int (fcard s)"
by (simp add: fremove_def)
why3_vc cardinal_remove by (auto simp add: cardinal_remove_out cardinal_remove_in)
why3_vc cardinal_subset
using assms
by (simp add: Fset.subset_def fcard_mono fsubsetI)
why3_vc filter_def by (simp add: Why3_Set.filter_def)
why3_vc cardinal_map
apply (simp add: fcard_def card_def)
by (metis card_def card_image_le finite_fset)
why3_vc cardinal_diff
by (metis fcard_funion_fsubset fcard_mono fminus_finter2 inf.idem inf_commute inf_sup_ord(1) of_nat_diff)
(* by (smt fcard_funion_fsubset fcard_mono finter_lower1 fminus_finter2 inf.idem inf_commute int_ops(6) of_nat_mono)*)
why3_vc mem_singleton
using assms by auto
why3_vc subset_filter
by (simp add: Fset.subset_def Why3_Set.filter_def)
why3_vc cardinal_union
by (smt fcard_funion_finter of_nat_add)
why3_vc empty_is_empty
by (meson Fset.is_empty_def assms bot.extremum_uniqueI fsubsetI)
why3_vc is_empty_empty
by (simp add: cardinal_empty)
why3_vc subset_inter_1
by (simp add: Fset.subset_def)
why3_vc subset_inter_2
by (simp add: Fset.subset_def)
why3_vc subset_union_1
by (simp add: Fset.subset_def)
why3_vc subset_union_2
by (simp add: Fset.subset_def)
why3_vc cardinal_filter
using cardinal_subset subset_filter by blast
why3_vc disjoint_diff_eq
by (smt Fset.disjoint_def Fset.facts.diff_def fsubsetI fsubset_antisym)
why3_vc disjoint_diff_s2
by (simp add: Fset.facts.disjoint_diff_eq)
why3_vc disjoint_inter_empty
by (metis Fset.facts.disjoint_diff_eq Fset.facts.empty_is_empty Fset.facts.is_empty_empty fminus_disjoint fminus_triv)
why3_vc cardinal_inter_disjoint
by (meson Fset.facts.disjoint_inter_empty assms cardinal_empty)
why3_end
end
|
