[7cfccc]: thys / Collections / ListSetImpl.thy  Maximize  Restore  History

Download this file

315 lines (262 with data), 12.7 kB

  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
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
(* Title: Isabelle Collections Library
Author: Peter Lammich <peter dot lammich at uni-muenster.de>
Maintainer: Peter Lammich <peter dot lammich at uni-muenster.de>
*)
header "Set Implementation by List"
theory ListSetImpl
imports SetSpec SetGA "common/Misc"
begin
text_raw {*\label{thy:ListSetImpl}*}
text {*
In this theory, sets are implemented by lists. Abbreviations: ls,l
*}
types
'a ls = "'a list"
subsection "Definitions"
definition ls_\<alpha> :: "'a ls \<Rightarrow> 'a set" where "ls_\<alpha> == set"
definition ls_invar :: "'a ls \<Rightarrow> bool" where "ls_invar == distinct"
definition ls_empty :: "'a ls" where "ls_empty == []"
definition ls_memb :: "'a \<Rightarrow> 'a ls \<Rightarrow> bool" where "ls_memb == (\<lambda> x xs. List.member xs x)"
definition ls_ins :: "'a \<Rightarrow> 'a ls \<Rightarrow> 'a ls" where "ls_ins == List.insert"
definition ls_ins_dj :: "'a \<Rightarrow> 'a ls \<Rightarrow> 'a ls" where "ls_ins_dj == Cons"
(* Tail recursive version *)
fun ls_delete_aux where
"ls_delete_aux x res [] = res" |
"ls_delete_aux x res (a#l) = (if x=a then revg res l else ls_delete_aux x (a#res) l)"
definition ls_delete :: "'a \<Rightarrow> 'a ls \<Rightarrow> 'a ls" where "ls_delete x l == ls_delete_aux x [] l"
fun ls_iteratei :: "('a ls,'a,'\<sigma>) iteratori" where
"ls_iteratei c f [] \<sigma> = \<sigma>" |
"ls_iteratei c f (x#l) \<sigma> = (if c \<sigma> then ls_iteratei c f l (f x \<sigma>) else \<sigma>)"
definition ls_iterate :: "('a ls,'a,'\<sigma>) iterator"
where "ls_iterate == iti_iterate ls_iteratei"
definition ls_isEmpty :: "'a ls \<Rightarrow> bool" where "ls_isEmpty s == s=[]"
definition ls_union :: "'a ls \<Rightarrow> 'a ls \<Rightarrow> 'a ls"
where "ls_union == it_union ls_iterate ls_ins"
definition ls_inter :: "'a ls \<Rightarrow> 'a ls \<Rightarrow> 'a ls"
where "ls_inter == it_inter ls_iterate ls_memb ls_empty ls_ins_dj"
definition ls_union_dj :: "'a ls \<Rightarrow> 'a ls \<Rightarrow> 'a ls"
where "ls_union_dj s1 s2 == revg s1 s2" -- "Union of disjoint sets"
definition ls_image_filter
where "ls_image_filter == it_image_filter ls_iterate ls_empty ls_ins"
definition ls_inj_image_filter
where "ls_inj_image_filter == it_inj_image_filter ls_iterate ls_empty ls_ins_dj"
definition "ls_image == iflt_image ls_image_filter"
definition "ls_inj_image == iflt_inj_image ls_inj_image_filter"
definition ls_ball :: "'a ls \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
where "ls_ball l P == list_all P l"
definition ls_sel :: "'a ls \<Rightarrow> ('a \<Rightarrow> 'r option) \<Rightarrow> 'r option"
where "ls_sel == iti_sel ls_iteratei"
definition ls_to_list :: "'a ls \<Rightarrow> 'a list" where "ls_to_list == id"
definition list_to_ls :: "'a list \<Rightarrow> 'a ls" where "list_to_ls == remdups"
definition "ls_size == it_size ls_iterate"
subsection "Correctness"
lemmas ls_defs =
ls_\<alpha>_def
ls_invar_def
ls_empty_def
ls_memb_def
ls_ins_def
ls_ins_dj_def
ls_delete_def
ls_iterate_def
ls_isEmpty_def
ls_union_def
ls_inter_def
ls_union_dj_def
ls_image_filter_def
ls_inj_image_filter_def
ls_image_def
ls_inj_image_def
ls_ball_def
ls_sel_def
ls_to_list_def
list_to_ls_def
ls_size_def
lemma ls_empty_impl: "set_empty ls_\<alpha> ls_invar ls_empty"
apply (unfold_locales)
apply (auto simp add: ls_defs)
done
lemma ls_memb_impl: "set_memb ls_\<alpha> ls_invar ls_memb"
apply (unfold_locales)
apply (auto simp add: ls_defs member_def)
done
lemma ls_ins_impl: "set_ins ls_\<alpha> ls_invar ls_ins"
apply (unfold_locales)
apply (auto simp add: ls_defs member_def)
done
lemma ls_ins_dj_impl: "set_ins_dj ls_\<alpha> ls_invar ls_ins_dj"
apply (unfold_locales)
apply (auto simp add: ls_defs)
done
lemma ls_delete_aux_impl:
"distinct (res@l)
\<Longrightarrow> distinct (ls_delete_aux x res l)
\<and> (set (ls_delete_aux x res l) = set res \<union> (set l - {x}))"
by (induct l arbitrary: res) (auto)
lemma ls_delete_impl: "set_delete ls_\<alpha> ls_invar ls_delete"
by (unfold_locales)
(simp_all add: ls_defs ls_delete_aux_impl)
lemma ls_\<alpha>_finite[simp, intro!]: "finite (ls_\<alpha> l)"
by (auto simp add: ls_defs)
lemma ls_is_finite_set: "finite_set ls_\<alpha> ls_invar"
apply (unfold_locales)
apply (auto simp add: ls_defs)
done
lemma ls_iteratei_impl: "set_iteratei ls_\<alpha> ls_invar ls_iteratei"
apply (unfold_locales)
apply (simp add: ls_defs)
proof -
case (goal1 S I \<sigma> c f)
{
fix it
assume
"it\<supseteq>ls_\<alpha> S"
"I it \<sigma>"
"\<forall>\<sigma> x it'. c \<sigma> \<and> x\<in>it' \<and> it' \<subseteq> it \<and> I it' \<sigma> \<longrightarrow> I (it' - {x}) (f x \<sigma>)"
moreover note `ls_invar S`
ultimately have "I (it-ls_\<alpha> S) (ls_iteratei c f S \<sigma>)
\<or> (\<exists>it'\<subseteq>it. it'\<noteq>{} \<and> \<not>c (ls_iteratei c f S \<sigma>) \<and> I it' (ls_iteratei c f S \<sigma>))"
proof (induct S arbitrary: it \<sigma>)
case Nil thus ?case
by (auto simp add: ls_defs)
next
case (Cons x S)
show ?case proof (cases "c \<sigma>")
case False with Cons.prems show ?thesis
by auto
next
case True
from Cons.prems(3)[rule_format, of \<sigma> x it] True Cons.prems(1-2)
have I': "I (it - {x}) (f x \<sigma>)" by (auto simp add: ls_defs)
from Cons.prems(1) Cons.prems(4) have PP: "ls_\<alpha> S \<subseteq> it - {x}" "ls_invar S"
by (auto simp add: ls_defs)
from Cons.prems(3) have
IPRES': "\<forall>\<sigma> xa it'.
c \<sigma>
\<and> xa \<in> it'
\<and> it' \<subseteq> it - {x}
\<and> I it' \<sigma>
\<longrightarrow> I (it' - {xa}) (f xa \<sigma>)"
by auto
from Cons.hyps[OF PP(1) I' IPRES' PP(2)]
have "I (it - {x} - ls_\<alpha> S) (ls_iteratei c f S (f x \<sigma>))
\<or> (\<exists>it'. it' \<subseteq> it - {x} \<and> it' \<noteq> {} \<and> \<not> c (ls_iteratei c f S (f x \<sigma>)) \<and> I it' (ls_iteratei c f S (f x \<sigma>)))"
(is "?C1 \<or> ?C2") .
moreover {
assume ?C1 hence ?thesis
by (auto simp add: ls_defs True set_diff_diff_left)
} moreover {
assume ?C2
then obtain it' where INT:
"it'\<subseteq>it-{x}"
"it'\<noteq>{}"
"\<not>c (ls_iteratei c f S (f x \<sigma>))"
"I it' (ls_iteratei c f S (f x \<sigma>))"
by blast
hence ?thesis
apply (rule_tac disjI2)
apply (rule_tac x=it' in exI)
apply (auto simp add: True)
done
} ultimately show ?thesis by blast
qed
qed
} note R=this
from R[OF subset_refl] goal1 show ?case by auto
qed
lemmas ls_iterate_impl = set_iteratei.iti_iterate_correct[OF ls_iteratei_impl, folded ls_iterate_def]
lemma ls_isEmpty_impl: "set_isEmpty ls_\<alpha> ls_invar ls_isEmpty"
apply (unfold_locales)
apply (auto simp add: ls_defs)
done
lemmas ls_union_impl = it_union_correct[OF ls_iterate_impl ls_ins_impl, folded ls_union_def]
lemmas ls_inter_impl = it_inter_correct[OF ls_iterate_impl ls_memb_impl ls_empty_impl ls_ins_dj_impl, folded ls_inter_def]
lemma ls_union_dj_impl: "set_union_dj ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_union_dj"
apply (unfold_locales)
apply (auto simp add: ls_defs)
done
lemmas ls_image_filter_impl = it_image_filter_correct[OF ls_iterate_impl ls_empty_impl ls_ins_impl, folded ls_image_filter_def]
lemmas ls_inj_image_filter_impl = it_inj_image_filter_correct[OF ls_iterate_impl ls_empty_impl ls_ins_dj_impl, folded ls_inj_image_filter_def]
lemmas ls_image_impl = iflt_image_correct[OF ls_image_filter_impl, folded ls_image_def]
lemmas ls_inj_image_impl = iflt_inj_image_correct[OF ls_inj_image_filter_impl, folded ls_inj_image_def]
lemma ls_ball_impl: "set_ball ls_\<alpha> ls_invar ls_ball"
apply (unfold_locales)
apply (auto simp add: ls_defs list_all_iff)
done
lemmas ls_sel_impl = iti_sel_correct[OF ls_iteratei_impl, folded ls_sel_def]
lemma ls_to_list_impl: "set_to_list ls_\<alpha> ls_invar ls_to_list"
apply (unfold_locales)
apply (auto simp add: ls_defs)
done
lemma list_to_ls_impl: "list_to_set ls_\<alpha> ls_invar list_to_ls"
apply (unfold_locales)
apply (auto simp add: ls_defs)
done
lemmas ls_size_impl = it_size_correct[OF ls_iterate_impl, folded ls_size_def]
interpretation ls: set_empty ls_\<alpha> ls_invar ls_empty using ls_empty_impl .
interpretation ls: set_memb ls_\<alpha> ls_invar ls_memb using ls_memb_impl .
interpretation ls: set_ins ls_\<alpha> ls_invar ls_ins using ls_ins_impl .
interpretation ls: set_ins_dj ls_\<alpha> ls_invar ls_ins_dj using ls_ins_dj_impl .
interpretation ls: set_delete ls_\<alpha> ls_invar ls_delete using ls_delete_impl .
interpretation ls: finite_set ls_\<alpha> ls_invar using ls_is_finite_set .
interpretation ls: set_iteratei ls_\<alpha> ls_invar ls_iteratei using ls_iteratei_impl .
interpretation ls: set_iterate ls_\<alpha> ls_invar ls_iterate using ls_iterate_impl .
interpretation ls: set_isEmpty ls_\<alpha> ls_invar ls_isEmpty using ls_isEmpty_impl .
interpretation ls: set_union ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_union using ls_union_impl .
interpretation ls: set_inter ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_inter using ls_inter_impl .
interpretation ls: set_union_dj ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_union_dj using ls_union_dj_impl .
interpretation ls: set_image_filter ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_image_filter using ls_image_filter_impl .
interpretation ls: set_inj_image_filter ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_inj_image_filter using ls_inj_image_filter_impl .
interpretation ls: set_image ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_image using ls_image_impl .
interpretation ls: set_inj_image ls_\<alpha> ls_invar ls_\<alpha> ls_invar ls_inj_image using ls_inj_image_impl .
interpretation ls: set_ball ls_\<alpha> ls_invar ls_ball using ls_ball_impl .
interpretation ls: set_sel ls_\<alpha> ls_invar ls_sel using ls_sel_impl .
interpretation ls: set_to_list ls_\<alpha> ls_invar ls_to_list using ls_to_list_impl .
interpretation ls: list_to_set ls_\<alpha> ls_invar list_to_ls using list_to_ls_impl .
interpretation ls: set_size ls_\<alpha> ls_invar ls_size using ls_size_impl .
declare ls.finite[simp del, rule del]
lemmas ls_correct =
ls.empty_correct
ls.memb_correct
ls.ins_correct
ls.ins_dj_correct
ls.delete_correct
ls.isEmpty_correct
ls.union_correct
ls.inter_correct
ls.union_dj_correct
ls.image_filter_correct
ls.inj_image_filter_correct
ls.image_correct
ls.inj_image_correct
ls.ball_correct
ls.to_list_correct
ls.to_set_correct
ls.size_correct
subsection "Code Generation"
export_code
ls_empty
ls_memb
ls_ins
ls_ins_dj
ls_delete_aux
ls_delete
ls_iteratei
ls_iterate
ls_isEmpty
ls_union
ls_inter
ls_union_dj
ls_image_filter
ls_inj_image_filter
ls_image
ls_inj_image
ls_ball
ls_sel
ls_to_list
list_to_ls
ls_size
in SML
module_name ListSet
file -
end

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:

JavaScript is required for this form.





No, thanks