alist_treeScript.sml

1(*
2  Definitions and theorems that support automation (the Lib file) for
3  fast insertion and lookup into association lists (alists).
4*)
5Theory alist_tree
6Ancestors
7  rich_list alist[qualified]
8Libs
9  boolSimps
10
11(* key property: a partial function f can be represented by an assoc list
12   al which is known to be sorted according to R *)
13Definition sorted_alist_repr_def:
14  sorted_alist_repr R al f <=>
15    SORTED R (MAP FST al) /\ irreflexive R /\ transitive R /\ (f = ALOOKUP al)
16End
17
18(* inserts on sorted alists *)
19
20Definition count_append_def:
21  count_append (n : num) xs ys = APPEND xs ys
22End
23
24Definition is_insert_def:
25  is_insert frame_l frame_r R k x al al' <=>
26     irreflexive R /\ transitive R ==>
27        SORTED R (MAP FST al) ==>
28         (ALOOKUP al' = ALOOKUP ((k, x) :: al)) /\
29         (frame_l ==> al <> [] /\ (FST (HD al') = FST (HD al))) /\
30         (frame_r ==> al <> [] /\ (FST (LAST al') = FST (LAST al))) /\
31         SORTED R (MAP FST al')
32End
33
34Theorem HD_APPEND:
35  HD (xs ++ ys) = (if xs = [] then HD ys else HD xs)
36Proof  Induct_on `xs` \\ fs []
37QED
38
39Theorem LAST_APPEND:
40  LAST (xs ++ ys) = (if ys = [] then LAST xs else LAST ys)
41Proof  Cases_on `ys` \\ fs []
42QED
43
44Theorem HD_MAP:
45  xs <> [] ==> (HD (MAP f xs) = f (HD xs))
46Proof  Cases_on `xs` \\ fs []
47QED
48
49Theorem HD_MEM:
50  xs <> []  ==> MEM (HD xs) xs
51Proof Cases_on `xs` \\ fs []
52QED
53
54Theorem is_insert_l:
55  !n. is_insert fl T R k x l l' ==>
56    is_insert fl T R k x (count_append n l r) (count_append ARB l' r)
57Proof
58  fs [is_insert_def, count_append_def, sortingTheory.SORTED_APPEND_GEN,
59    alistTheory.ALOOKUP_APPEND, FUN_EQ_THM, HD_APPEND, LAST_APPEND,
60    listTheory.LAST_MAP]
61  \\ (Cases_on `l'` \\ fs [] >- metis_tac [optionTheory.option_CLAUSES])
62  \\ (Cases_on `l = []` \\ fs [])
63  \\ fs [listTheory.LAST_MAP]
64  \\ (rpt strip_tac \\ fs [] \\ CASE_TAC)
65QED
66
67Theorem insert_fl_R:
68  is_insert fl fr R k x al al' ==> fl ==> SORTED R (MAP FST al)
69    ==> irreflexive R /\ transitive R
70    ==> (k = FST (HD al)) \/ R (HD (MAP FST al)) k
71Proof
72  fs [is_insert_def, FUN_EQ_THM]
73  \\ rpt strip_tac
74  \\ fs []
75  \\ FIRST_X_ASSUM (MP_TAC o Q.SPEC `k`)
76  \\ fs []
77  \\ strip_tac
78  \\ FIRST_X_ASSUM (MP_TAC o MATCH_MP alistTheory.ALOOKUP_MEM)
79  \\ (Cases_on `al'` \\ fs [sortingTheory.SORTED_EQ])
80  \\ fs [listTheory.MEM_MAP, pairTheory.EXISTS_PROD, HD_MAP]
81  \\ metis_tac [pairTheory.FST]
82QED
83
84Theorem insert_fl_R_append:
85  is_insert T fr R k x r r'
86    ==> SORTED R (MAP FST (l ++ r))
87    ==> irreflexive R /\ transitive R
88    ==> ~ MEM k (MAP FST l)
89Proof
90  strip_tac
91  \\ FIRST_ASSUM (MP_TAC o MATCH_MP insert_fl_R)
92  \\ fs [METIS_PROVE [] ``b \/ c <=> ~b ==> c``]
93  \\ rpt strip_tac
94  \\ fs [sortingTheory.SORTED_APPEND, is_insert_def]
95  \\ FIRST_X_ASSUM (MP_TAC o Q.SPEC `k`)
96  \\ fs []
97  \\ (Cases_on `HD r` \\ Cases_on `r` \\ fs [])
98  \\ metis_tac [relationTheory.transitive_def, relationTheory.irreflexive_def]
99QED
100
101Theorem is_insert_r:
102  !n. is_insert T fr R k x r r' ==>
103    is_insert T fr R k x (count_append n l r) (count_append ARB l r')
104Proof
105  rpt strip_tac
106  \\ MP_TAC insert_fl_R_append
107  \\ fs [is_insert_def, count_append_def, sortingTheory.SORTED_APPEND_GEN,
108    alistTheory.ALOOKUP_APPEND, FUN_EQ_THM, HD_APPEND, LAST_APPEND, HD_MAP]
109  \\ ((Cases_on `r'` \\ fs []) >- metis_tac [optionTheory.option_CLAUSES])
110  \\ (rpt strip_tac \\ rpt (CHANGED_TAC (rfs [HD_MAP] \\ fs [])))
111  \\ rpt (CASE_TAC \\ fs [])
112  \\ FIRST_ASSUM (MP_TAC o MATCH_MP alistTheory.ALOOKUP_MEM)
113  \\ metis_tac [listTheory.MEM_MAP, pairTheory.FST]
114QED
115
116Theorem is_insert_to_empty:
117  !R k x. is_insert F F R k x [] [(k, x)]
118Proof   fs [is_insert_def]
119QED
120
121Theorem is_insert_overwrite:
122  !R k x v. (FST v = k) ==> is_insert T T R k x [v] [(k, x)]
123Proof
124  Cases_on `v` \\ fs [is_insert_def, FUN_EQ_THM]
125QED
126
127Theorem sorted_fst_insert_centre:
128  !k. SORTED R (MAP FST l ++ MAP FST r) ==>
129    (~ (l = []) ==> R (FST (LAST l)) k) ==>
130    (~ (r = []) ==> R k (FST (HD r))) ==>
131    SORTED R (MAP FST l ++ (k :: MAP FST r))
132Proof
133  Cases_on `r` \\ Cases_on `l` \\
134  fs [sortingTheory.SORTED_APPEND_GEN, sortingTheory.SORTED_DEF,
135      listTheory.LAST_MAP, HD_MAP]
136QED
137
138Theorem is_insert_centre_rule:
139  (fl ==> ~ (l = [])) ==> (~ (l = []) ==> R (FST (LAST l)) k) ==>
140    (fr ==> ~ (r = [])) ==> (~ (r = []) ==> R k (FST (HD r))) ==>
141    is_insert fl fr R k x (count_append n l r)
142        (count_append ARB l (count_append ARB [(k, x)] r))
143Proof
144  fs [is_insert_def, count_append_def, HD_APPEND, LAST_APPEND,
145      listTheory.LAST_CONS_cond]
146  \\ rpt disch_tac
147  \\ FIRST_X_ASSUM (MP_TAC o MATCH_MP (Q.SPEC `k` sorted_fst_insert_centre))
148  \\ fs [sortingTheory.SORTED_APPEND]
149  \\ fs [FUN_EQ_THM, alistTheory.ALOOKUP_APPEND]
150  \\ rpt (strip_tac \\ fs [])
151  \\ rpt (CASE_TAC \\ fs [])
152  \\ FIRST_ASSUM (MP_TAC o MATCH_MP alistTheory.ALOOKUP_MEM)
153  \\ fs [listTheory.MEM_MAP, pairTheory.EXISTS_PROD]
154  \\ metis_tac [relationTheory.irreflexive_def]
155QED
156
157Theorem is_insert_centre =
158  is_insert_centre_rule |> Q.GENL [`fl`, `fr`, `R`, `n`, `k`, `x`]
159    |> SPECL [T, T] |> CONV_RULE (SIMP_CONV bool_ss []);
160
161Theorem is_insert_far_left:
162  !R k x xs. ~ (xs = []) ==> R k (FST (HD xs)) ==>
163    is_insert F T R k x xs (count_append ARB [(k, x)] xs)
164Proof
165  Cases_on `xs` \\
166  fs [is_insert_def, count_append_def, sortingTheory.SORTED_DEF]
167QED
168
169Theorem is_insert_far_right:
170  !R k x xs. ~ (xs = []) ==> R (FST (LAST xs)) k ==>
171    is_insert T F R k x xs (count_append ARB xs [(k, x)])
172Proof
173  rpt strip_tac
174  \\ MP_TAC (Q.GENL [`fl`, `fr`, `r`, `l`, `x`] is_insert_centre_rule
175    |> Q.SPECL [`T`, `F`, `[]`, `xs`, `x`])
176  \\ fs [is_insert_def, count_append_def]
177QED
178
179(* bookkeeping and balancing count_append trees *)
180
181Theorem count_append_HD_LAST:
182  (HD (count_append i (count_append j xs ys) zs)
183    = HD (count_append 0 xs (count_append 0 ys zs))) /\
184  (HD (count_append i (x :: xs) ys) = x) /\
185  (HD (count_append i [] ys) = HD ys) /\
186  (LAST (count_append i xs (count_append j ys zs))
187      = LAST (count_append 0 (count_append 0 xs ys) zs)) /\
188  (LAST (count_append i xs (y :: ys)) = LAST (y :: ys)) /\
189  (LAST (count_append i xs []) = LAST xs) /\
190  (HD (x :: xs) = x) /\
191  (LAST (x :: y :: zs) = LAST (y :: zs)) /\
192  (LAST [x] = x) /\
193  ((count_append i (count_append j xs ys) zs = []) =
194      (count_append 0 xs (count_append 0 ys zs) = [])) /\
195  ((count_append i [] ys = []) = (ys = [])) /\
196  ((count_append i (x :: xs) ys = []) = F) /\
197  ((x :: xs = []) = F)
198Proof fs [count_append_def]
199QED
200
201Theorem balance_r:
202  count_append i (count_append j xs ys) zs
203     = count_append ARB xs (count_append ARB ys zs)
204Proof
205  fs [count_append_def]
206QED
207
208Theorem balance_l:
209  count_append i xs (count_append j ys zs)
210     = count_append ARB (count_append ARB xs ys) zs
211Proof fs [count_append_def]
212QED
213
214Theorem set_count:
215  !j. count_append i xs ys = count_append j xs ys
216Proof
217  fs [count_append_def]
218QED
219
220(* reprs of various partial function constructions *)
221Definition option_choice_f_def:
222  option_choice_f f g = (\x. OPTION_CHOICE (f x) (g x))
223End
224
225Theorem alookup_append_option_choice_f:
226  ALOOKUP (xs ++ ys) = option_choice_f (ALOOKUP xs) (ALOOKUP ys)
227Proof
228  rpt (strip_tac ORELSE CASE_TAC ORELSE
229       fs [option_choice_f_def, alistTheory.ALOOKUP_APPEND, FUN_EQ_THM])
230QED
231
232Theorem alookup_empty_option_choice_f:
233  (option_choice_f (ALOOKUP []) f = f)
234    /\ (option_choice_f f (ALOOKUP []) = f)
235Proof
236  fs [FUN_EQ_THM, option_choice_f_def]
237QED
238
239Theorem option_choice_f_assoc:
240  option_choice_f (option_choice_f f g) h
241    = option_choice_f f (option_choice_f g h)
242Proof
243  fs [option_choice_f_def, FUN_EQ_THM] \\ Cases_on `f x` \\ fs []
244QED
245
246Theorem empty_is_ALOOKUP: (\x. NONE) = ALOOKUP []
247Proof    fs [FUN_EQ_THM]
248QED
249
250Theorem repr_insert:
251  sorted_alist_repr R al f /\ is_insert fl fr R k x al al' ==>
252    sorted_alist_repr R al' (option_choice_f (ALOOKUP [(k, x)]) f)
253Proof
254  fs [sorted_alist_repr_def, is_insert_def,
255      GSYM alookup_append_option_choice_f]
256QED
257
258Theorem alookup_to_option_choice:
259  (ALOOKUP (x :: y :: zs) = option_choice_f (ALOOKUP [x]) (ALOOKUP (y :: zs)))
260    /\ (option_choice_f (ALOOKUP []) g = g)
261Proof
262  fs [GSYM alookup_append_option_choice_f]
263    \\ fs [FUN_EQ_THM, option_choice_f_def]
264QED
265
266Theorem alist_repr_choice_trans_left:
267  sorted_alist_repr R al f /\
268    sorted_alist_repr R al' (option_choice_f (ALOOKUP al) g) ==>
269    sorted_alist_repr R al' (option_choice_f f g)
270Proof
271  fs [sorted_alist_repr_def]
272QED
273
274Theorem alist_repr_refl:
275  !al. irreflexive R /\ transitive R ==> SORTED R (MAP FST al) ==>
276    sorted_alist_repr R al (ALOOKUP al)
277Proof   fs [sorted_alist_repr_def]
278QED
279
280(* lookups on sorted alists *)
281Definition is_lookup_def:
282  is_lookup fl fr R al x r = (!xs ys. (fl \/ (xs = [])) ==>
283    (fr \/ (ys = [])) ==> irreflexive R /\ transitive R ==>
284    SORTED R (MAP FST (xs ++ al ++ ys)) ==>
285    (ALOOKUP (xs ++ al ++ ys) x = r))
286End
287
288Theorem lookup_repr:
289  sorted_alist_repr R al f /\ is_lookup fl fr R al x r ==> (f x = r)
290Proof
291  fs [is_lookup_def, sorted_alist_repr_def]
292  \\ metis_tac [APPEND_NIL, MAP]
293QED
294
295Theorem is_lookup_l:
296  !n. is_lookup fl T R l x res
297    ==> is_lookup fl T R (count_append n l r) x res
298Proof
299  fs [is_lookup_def, count_append_def]
300  \\ metis_tac [APPEND_ASSOC, MAP_APPEND]
301QED
302
303Theorem is_lookup_r:
304  !n. is_lookup T fr R r x res
305    ==> is_lookup T fr R (count_append n l r) x res
306Proof
307  fs [is_lookup_def, count_append_def]
308  \\ metis_tac [APPEND_ASSOC, MAP_APPEND]
309QED
310
311Theorem is_lookup_far_left:
312  !R k k' v. R k k' ==> is_lookup F T R [(k', v)] k NONE
313Proof
314  fs [is_lookup_def, sortingTheory.SORTED_EQ, listTheory.MEM_MAP,
315      pairTheory.EXISTS_PROD,alistTheory.ALOOKUP_NONE,PULL_EXISTS]
316  \\ rpt strip_tac
317  \\ metis_tac [ relationTheory.irreflexive_def,
318     relationTheory.transitive_def]
319QED
320
321Theorem is_lookup_far_right:
322  !R k k' v. R k' k ==> is_lookup T F R [(k', v)] k NONE
323Proof
324  fs [is_lookup_def, sortingTheory.SORTED_APPEND, listTheory.MEM_MAP,
325      pairTheory.EXISTS_PROD, alistTheory.ALOOKUP_APPEND]
326  \\ rpt strip_tac
327  \\ Cases_on `ALOOKUP xs k` \\ CASE_TAC \\ fs []
328  \\ metis_tac [alistTheory.ALOOKUP_MEM, relationTheory.irreflexive_def,
329                relationTheory.transitive_def]
330QED
331
332Theorem is_lookup_hit:
333  !R k k' v. (k' = k) ==> is_lookup T T R [(k', v)] k (SOME v)
334Proof
335  fs [is_lookup_def, sortingTheory.SORTED_APPEND, listTheory.MEM_MAP,
336      pairTheory.EXISTS_PROD, alistTheory.ALOOKUP_APPEND]
337  \\ rpt strip_tac
338  \\ rpt (CASE_TAC \\ fs [])
339  \\ metis_tac [alistTheory.ALOOKUP_MEM, relationTheory.irreflexive_def,
340                relationTheory.transitive_def]
341QED
342
343Theorem DISJ_EQ_IMP: (P \/ Q) = (~ P ==> Q)
344Proof metis_tac []
345QED
346
347val sorted_fst_insert_centre2 = sorted_fst_insert_centre
348  |> Q.GENL [`l`, `r`] |> Q.SPECL [`lxs ++ lys`, `rxs ++ rys`]
349  |> SIMP_RULE list_ss []
350
351Theorem is_lookup_centre:
352  !R n l r k.
353     l <> [] ==> R (FST (LAST l)) k ==> r <> [] ==> R k (FST (HD r)) ==>
354     is_lookup T T R (count_append n l r) k NONE
355Proof
356  fs [is_lookup_def, listTheory.MEM_MAP,
357      pairTheory.EXISTS_PROD, alistTheory.ALOOKUP_APPEND, count_append_def]
358  \\ rpt strip_tac
359  \\ FIRST_X_ASSUM (MP_TAC o MATCH_MP (Q.SPEC `k` sorted_fst_insert_centre2))
360  \\ fs [LAST_APPEND, HD_APPEND]
361  \\ fs [sortingTheory.SORTED_APPEND, sortingTheory.SORTED_EQ,
362    listTheory.MEM_MAP, pairTheory.EXISTS_PROD]
363  \\ rpt strip_tac
364  \\ (Cases_on `ALOOKUP ys k` \\ rpt (CASE_TAC \\ fs [])
365    \\ metis_tac [alistTheory.ALOOKUP_MEM, relationTheory.irreflexive_def,
366                  relationTheory.transitive_def])
367QED
368
369Theorem is_lookup_empty:
370  !R k al. (al = []) ==> is_lookup F F R al k NONE
371Proof
372  fs [is_lookup_def]
373QED
374