-
Notifications
You must be signed in to change notification settings - Fork 0
/
Flatten_Iter_Spec.thy
356 lines (336 loc) · 11.9 KB
/
Flatten_Iter_Spec.thy
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
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
theory Flatten_Iter_Spec
imports
Basic_Assn
"Separation_Logic_Imperative_HOL.Imp_List_Spec"
"HOL-Real_Asymp.Inst_Existentials"
begin
text "This locale takes an iterator that refines a list of elements that themselves
can be iterated and defines an iterator over the flattened list of lower level elements"
locale flatten_iter =
inner_list: imp_list_iterate is_inner_list inner_is_it inner_it_init inner_it_has_next inner_it_next +
outer_list: imp_list_iterate is_outer_list outer_is_it outer_it_init outer_it_has_next outer_it_next
for is_outer_list :: "'l list \<Rightarrow> 'm \<Rightarrow> assn"
and outer_is_it :: "'l list \<Rightarrow> 'm \<Rightarrow> 'l list \<Rightarrow> 'oit \<Rightarrow> assn"
and outer_it_init :: "'m \<Rightarrow> ('oit) Heap"
and outer_it_has_next :: "'oit \<Rightarrow> bool Heap"
and outer_it_next :: "'oit \<Rightarrow> ('l\<times>'oit) Heap"
and is_inner_list :: "'a list \<Rightarrow> 'l \<Rightarrow> assn"
and inner_is_it :: "'a list \<Rightarrow> 'l \<Rightarrow> 'a list \<Rightarrow> 'iit \<Rightarrow> assn"
and inner_it_init :: "'l \<Rightarrow> ('iit) Heap"
and inner_it_has_next :: "'iit \<Rightarrow> bool Heap"
and inner_it_next :: "'iit \<Rightarrow> ('a\<times>'iit) Heap"
begin
fun is_flatten_list :: "'a list list \<Rightarrow> 'a list \<Rightarrow> 'm \<Rightarrow> assn" where
"is_flatten_list ls' ls lsi = (\<exists>\<^sub>A lsi'.
is_outer_list lsi' lsi * list_assn is_inner_list ls' lsi' * \<up>(ls = concat ls')
)"
lemma flatten_prec:
"precise (is_flatten_list ls)"
apply (intro preciseI)
apply (auto)
done
(*type_synonym flatten_it = "'iit \<times> 'oit"*)
fun is_flatten_it :: "'a list list \<Rightarrow> 'a list \<Rightarrow> 'm \<Rightarrow> 'a list \<Rightarrow> ('oit \<times> 'iit option) \<Rightarrow> assn"
where
"is_flatten_it lsi'' ls lsi [] (oit, None) =
(\<exists>\<^sub>A lsi'.
list_assn is_inner_list lsi'' lsi' *
\<up>(ls = (concat lsi'')) *
outer_is_it lsi' lsi [] oit
)" |
"is_flatten_it lsi'' ls lsi ls2 (oit, Some iit) =
(\<exists>\<^sub>A lsi' ls2' ls1' lsi1 lsi2 lsim ls2m lsm ls1m.
list_assn is_inner_list ls1' lsi1 *
list_assn is_inner_list ls2' lsi2 *
\<up>(ls2m \<noteq> [] \<and> ls2 = ls2m@(concat ls2') \<and> ls = (concat (ls1'@lsm#ls2')) \<and> lsi'' = (ls1'@lsm#ls2')) *
outer_is_it lsi' lsi lsi2 oit *
\<up>(lsm = ls1m@ls2m \<and> lsi'=(lsi1@lsim#lsi2)) *
inner_is_it lsm lsim ls2m iit
)
" |
"is_flatten_it _ _ _ _ _ = false"
partial_function (heap) flatten_it_adjust:: "'oit \<Rightarrow> 'iit \<Rightarrow> ('oit \<times> 'iit option) Heap" where
"flatten_it_adjust oit iit = do {
ihasnext \<leftarrow> inner_it_has_next iit;
if ihasnext then
return (oit, Some iit)
else do {
ohasnext \<leftarrow> outer_it_has_next oit;
if \<not>ohasnext then
return (oit, None)
else do {
(next, oit) \<leftarrow> outer_it_next oit;
nextit \<leftarrow> inner_it_init next;
flatten_it_adjust oit nextit
}
}
}
"
declare flatten_it_adjust.simps[code]
lemma flatten_it_adjust_rule:
" <list_assn is_inner_list ls1' ls1 * list_assn is_inner_list ls2' ls2 *
outer_is_it (ls1@lsim#ls2) lsi ls2 oit * inner_is_it (lsm1@lsm2) lsim lsm2 iit>
flatten_it_adjust oit iit
<is_flatten_it (ls1'@(lsm1@lsm2)#ls2') (concat (ls1'@(lsm1@lsm2)#ls2')) lsi (concat (lsm2#ls2'))>\<^sub>t"
proof (induction ls2 arbitrary: ls1' ls1 ls2' lsim lsm1 lsm2 oit iit)
case Nil
then show ?case
apply(subst flatten_it_adjust.simps)
apply (sep_auto eintros del: exI heap add: inner_list.it_has_next_rule)
apply(inst_existentials "(ls1 @ lsim # [])" ls2' ls1' ls1 "[]::'l list" lsim lsm2 "lsm1@lsm2")
subgoal by auto
subgoal by (sep_auto)
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
subgoal
apply (vcg (ss))
apply (sep_auto eintros del: exI)
apply(inst_existentials "(ls1 @ [lsim])" "ls1'@[lsm1]")
subgoal
apply(auto simp add: list_assn_app_one)
using inner_list.quit_iteration
by (smt (z3) assn_aci(9) assn_times_comm ent_true_drop(1) fr_refl)
done
done
next
case (Cons a ls2)
show ?case
apply(subst flatten_it_adjust.simps)
apply (sep_auto eintros del: exI heap add: inner_list.it_has_next_rule)
apply(inst_existentials "(ls1 @ lsim # a # ls2)" ls2' ls1' ls1 "a #ls2" lsim lsm2 "lsm1@lsm2")
subgoal by auto
subgoal by (sep_auto)
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
subgoal by simp
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (case_tac ls2')
apply simp_all
apply (sep_auto eintros del: exI heap add: inner_list.it_init_rule)
subgoal for x oit aa list xa
supply R = "Cons.IH"[of "ls1'@[lsm1]" "ls1@[lsim]" list a oit "[]::'a list" aa xa, simplified]
thm R
find_theorems "_ \<Longrightarrow>\<^sub>A _" "<_>_<_>"
supply Q = Hoare_Triple.cons_pre_rule[of
"inner_is_it aa a aa xa * outer_is_it (ls1 @ lsim # a # ls2) lsi ls2 oit *
inner_is_it lsm1 lsim [] iit *
list_assn is_inner_list ls1' ls1 *
list_assn is_inner_list list ls2 *
true"
"list_assn is_inner_list ls1' ls1 * is_inner_list lsm1 lsim * list_assn is_inner_list list ls2 *
outer_is_it (ls1 @ lsim # a # ls2) lsi ls2 oit *
inner_is_it aa a aa
xa * true"
]
thm Q
apply(rule Q)
prefer 2
subgoal by (sep_auto heap add: R intro: inner_list.quit_iteration)
subgoal using inner_list.quit_iteration
by (smt (z3) assn_aci(10) assn_times_comm ent_refl_true ent_star_mono_true)
done
done
qed
definition flatten_it_init :: "'m \<Rightarrow> _ Heap"
where "flatten_it_init l = do {
oit \<leftarrow> outer_it_init l;
ohasnext \<leftarrow> outer_it_has_next oit;
if ohasnext then do {
(next, oit) \<leftarrow> outer_it_next oit;
nextit \<leftarrow> inner_it_init next;
flatten_it_adjust oit nextit
} else return (oit, None)
}"
lemma flatten_it_init_rule[sep_heap_rules]:
"<is_flatten_list l' l p> flatten_it_init p <is_flatten_it l' l p l>\<^sub>t"
unfolding flatten_it_init_def
apply simp
apply(rule norm_pre_ex_rule)+
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
subgoal for ls' x xa
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply (vcg (ss))
apply(case_tac ls'; case_tac l')
apply simp+
apply(rule impI)
thm inner_list.it_init_rule
apply (vcg heap add: inner_list.it_init_rule)
subgoal for _ nxt oit a list aa lista xaa
supply R = flatten_it_adjust_rule[of "[]" "[]" lista list a p oit "[]" aa xaa, simplified]
thm R
apply (sep_auto heap add: R)
done
done
apply (sep_auto)
done
definition flatten_it_next where
"flatten_it_next \<equiv> \<lambda>(oit,iit). do {
(x, iit) \<leftarrow> inner_it_next (the iit);
(oit, iit) \<leftarrow> flatten_it_adjust oit iit;
return (x, (oit,iit))
}"
lemma flatten_it_next_rule:
" l' \<noteq> [] \<Longrightarrow>
<is_flatten_it lsi'' l p l' it>
flatten_it_next it
<\<lambda>(a,it'). is_flatten_it lsi'' l p (tl l') it' * \<up>(a=hd l')>\<^sub>t"
apply(subst flatten_it_next_def)
thm inner_list.it_next_rule
apply (vcg (ss))
apply (vcg (ss))
apply(case_tac iit; case_tac l')
apply simp_all
apply(rule norm_pre_ex_rule)+
subgoal for oit iit a aa list lsi' ls2' ls1' lsi1 lsi2 lsim ls2m lsm ls1m
apply(vcg (ss))
apply(vcg (ss))
apply(vcg (ss))
apply(vcg (ss))
apply(vcg (ss))
apply(vcg (ss))
apply(vcg (ss))
apply(vcg (ss))
apply(vcg (ss))
apply(case_tac ls2m)
apply simp_all
subgoal for _ _ iita lista
supply R = flatten_it_adjust_rule[of ls1' lsi1 ls2' lsi2 lsim p oit "ls1m@[aa]" "lista" iita, simplified]
thm R
apply (sep_auto heap add: R)
done
done
done
definition flatten_it_has_next where
"flatten_it_has_next \<equiv> \<lambda>(oit, iit). do {
return (iit \<noteq> None)
}"
lemma flatten_it_has_next_rule[sep_heap_rules]:
"<is_flatten_it lsi'' l p l' it>
flatten_it_has_next it
<\<lambda>r. is_flatten_it lsi'' l p l' it * \<up>(r\<longleftrightarrow>l'\<noteq>[])>\<^sub>t"
apply(subst flatten_it_has_next_def)
apply(sep_auto)
apply(case_tac iit, case_tac l')
apply simp_all
apply sep_auto
done
declare mult.left_assoc[simp add]
lemma flatten_quit_iteration:
"is_flatten_it lsi'' l p l' it \<Longrightarrow>\<^sub>A is_flatten_list lsi'' l p * true"
apply(cases it)
subgoal for oit iit
apply(cases iit; cases l')
proof (goal_cases)
case 1
then show ?case
apply (sep_auto eintros del: exI)
subgoal for lsi'
apply(inst_existentials lsi')
subgoal by (metis (no_types, lifting) assn_aci(10) assn_times_comm fr_refl outer_list.quit_iteration)
done
done
next
case (2 lsim ll')
then show ?case
by (sep_auto eintros del: exI)
next
case (3 iit)
then show ?case
by (sep_auto eintros del: exI)
next
case (4 iit lsim ll')
then show ?case
apply (sep_auto eintros del: exI)
subgoal for ls2' ls1' lsi1 lsi2 lsima ls2m ls1m
apply(inst_existentials "(lsi1 @ lsima # lsi2)")
apply(rule entails_preI)
apply(sep_auto dest!: mod_starD list_assn_len)
subgoal
apply(simp add:
mult.commute[where ?b="outer_is_it (lsi1 @ lsima # lsi2) p lsi2 oit"]
mult.commute[where ?b="is_outer_list (lsi1 @ lsima # lsi2) p"]
mult.left_assoc )?
apply(rule rem_true)
supply R = ent_star_mono_true[of
"outer_is_it (lsi1 @ lsima # lsi2) p lsi2 oit"
"is_outer_list (lsi1 @ lsima # lsi2) p"
"list_assn is_inner_list ls1' lsi1 *
list_assn is_inner_list ls2' lsi2 *
inner_is_it (ls1m @ ls2m) lsima ls2m iit"
" list_assn is_inner_list ls1' lsi1 *
is_inner_list (ls1m @ ls2m) lsima *
list_assn is_inner_list ls2' lsi2"
,simplified]
thm R
apply(rule R)
subgoal by (rule outer_list.quit_iteration)
apply(simp add:
mult.commute[where ?b="inner_is_it (ls1m @ ls2m) lsima ls2m iit"]
mult.commute[where ?b="is_inner_list (ls1m @ ls2m) lsima"]
mult.left_assoc)
apply(rule rem_true)
supply R = ent_star_mono_true[of
"inner_is_it (ls1m @ ls2m) lsima ls2m iit"
"is_inner_list (ls1m @ ls2m) lsima"
"list_assn is_inner_list ls1' lsi1 *
list_assn is_inner_list ls2' lsi2"
" list_assn is_inner_list ls1' lsi1 *
list_assn is_inner_list ls2' lsi2"
,simplified]
thm R
apply(rule R)
subgoal by (rule inner_list.quit_iteration)
subgoal by sep_auto
done
done
done
qed
done
declare mult.left_assoc[simp del]
interpretation flatten_it: imp_list_iterate "is_flatten_list lsi''" "is_flatten_it lsi''" flatten_it_init flatten_it_has_next flatten_it_next
apply(unfold_locales)
subgoal
by (rule flatten_prec)
subgoal for l p
by (rule flatten_it_init_rule[of lsi'' l p])
subgoal for l' l p it
by (rule flatten_it_next_rule[of l' lsi'' l p it]) simp
subgoal for l p l' it
by (rule flatten_it_has_next_rule[of lsi'' l p l' it])
subgoal for l p l' it
by (rule flatten_quit_iteration[of lsi'' l p l' it])
done
end
end