indexedListsScript.sml
1Theory indexedLists[bare]
2Ancestors
3 list rich_list
4Libs
5 HolKernel Parse boolLib BasicProvers TotalDefn simpLib numLib
6 IndDefLib
7
8(* bossLib approximation *)
9fun simp thl g ctxt =
10 ASM_SIMP_TAC (srw_ss_of ctxt ++ numSimps.ARITH_ss) thl g ctxt
11fun dsimp thl g ctxt =
12 ASM_SIMP_TAC (srw_ss_of ctxt ++ numSimps.ARITH_ss ++ boolSimps.DNF_ss)
13 thl g ctxt
14fun csimp thl g ctxt =
15 ASM_SIMP_TAC (srw_ss_of ctxt ++ numSimps.ARITH_ss ++ boolSimps.CONJ_ss)
16 thl g ctxt
17fun kall_tac th = K ALL_TAC th
18val metis_tac = metisLib.METIS_TAC
19val qid_spec_tac = Q.ID_SPEC_TAC
20fun rw thl = SRW_TAC[] thl
21fun fs thl g ctxt =
22 full_simp_tac (srw_ss_of ctxt ++ numSimps.ARITH_ss) thl g ctxt;
23val rename1 = Q.RENAME1_TAC
24val qspec_then = Q.SPEC_THEN
25
26Definition MAPi_def[simp,nocompute]:
27 (MAPi f [] = []) /\
28 (MAPi f (h::t) = f 0 h :: MAPi (f o SUC) t)
29End
30
31Definition MAPi_ACC_def:
32 (MAPi_ACC f i a [] = REVERSE a) /\
33 (MAPi_ACC f i a (h::t) = MAPi_ACC f (i + 1) (f i h :: a) t)
34End
35
36Theorem MAPi_ACC_MAPi:
37 MAPi_ACC f n a l = REVERSE a ++ MAPi (f o (+) n) l
38Proof
39 MAP_EVERY Q.ID_SPEC_TAC [`f`, `n`, `a`] >> Induct_on `l` >>
40 simp[MAPi_ACC_def] >> REWRITE_TAC [GSYM APPEND_ASSOC, APPEND] >>
41 REPEAT GEN_TAC >> REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) >>
42 simp[FUN_EQ_THM]
43QED
44
45Theorem MAPi_compute[compute]:
46 MAPi f l = MAPi_ACC f 0 [] l
47Proof
48 simp[MAPi_ACC_MAPi] >> REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) >>
49 simp[FUN_EQ_THM]
50QED
51
52val LT_SUC = arithmeticTheory.LT_SUC
53
54Theorem MEM_MAPi:
55 !x f l. MEM x (MAPi f l) <=>
56 ?n. n < LENGTH l /\ x = f n (EL n l)
57Proof
58 Induct_on `l` >> simp[] >> pop_assum kall_tac >>
59 dsimp[EQ_IMP_THM, LT_SUC] >> metis_tac[]
60QED
61
62Theorem MAPi_CONG[defncong]:
63 !l1 l2 f1 f2.
64 l1 = l2 /\ (!x n. MEM x l2 ==> f1 n x = f2 n x) ==>
65 MAPi f1 l1 = MAPi f2 l2
66Proof
67 Induct_on `l1` >> dsimp[LT_SUC]
68QED
69
70Theorem MAPi_CONG':
71 l1 = l2 ==> (!x n. (x = EL n l2) ==> n < LENGTH l2 ==> f1 n x = f2 n x) ==>
72 MAPi f1 l1 = MAPi f2 l2
73Proof
74 map_every qid_spec_tac [`f1`, `f2`, `l2`] >> Induct_on `l1` >>
75 dsimp[LT_SUC]
76QED
77
78Theorem LENGTH_MAPi[simp]:
79 !f l. LENGTH (MAPi f l) = LENGTH l
80Proof
81 Induct_on `l` >> simp[]
82QED
83
84Theorem MAP_MAPi[simp]:
85 !f g l. MAP f (MAPi g l) = MAPi ((o) f o g) l
86Proof
87 Induct_on `l` >> simp[]
88QED
89
90Theorem EL_MAPi[simp]:
91 !f n l. n < LENGTH l ==> EL n (MAPi f l) = f n (EL n l)
92Proof
93 Induct_on `l` >> simp[] >> dsimp[LT_SUC]
94QED
95
96Theorem MAPi_APPEND:
97 !l1 l2 f. MAPi f (l1 ++ l2) = MAPi f l1 ++ MAPi (f o (+) (LENGTH l1)) l2
98Proof
99 Induct >> simp[] >> rpt gen_tac >> rpt (AP_TERM_TAC ORELSE AP_THM_TAC) >>
100 simp[FUN_EQ_THM]
101QED
102
103Theorem MAPi_GENLIST:
104 !l f. MAPi f l = GENLIST (S f (combin$C EL l)) (LENGTH l)
105Proof
106 Induct >> simp[GENLIST_CONS] >> rpt gen_tac >>
107 rpt (AP_TERM_TAC ORELSE AP_THM_TAC) >> simp[FUN_EQ_THM]
108QED
109
110Theorem MAPi_EQ_MAP[simp]:
111 !l. MAPi (\i x. f x) l = MAP f l
112Proof
113 Induct >> simp[combinTheory.o_DEF]
114QED
115
116Definition FOLDRi_def[simp]:
117 (FOLDRi f a [] = a) /\
118 (FOLDRi f a (h::t) = f 0 h (FOLDRi (f o SUC) a t))
119End
120
121Theorem FOLDR_MAPi:
122 !f g a l. FOLDR f a (MAPi g l) = FOLDRi ($o f o g) a l
123Proof
124 Induct_on `l` >> simp[MAPi_def]
125QED
126
127Theorem FOLDRi_APPEND:
128 !f.
129 FOLDRi f a (l1 ++ l2) = FOLDRi f (FOLDRi (f o $+ (LENGTH l1)) a l2) l1
130Proof
131 Induct_on `l1` >> simp[]
132 >- (gen_tac >> `f o $+ 0 = f` suffices_by simp[] >> simp[FUN_EQ_THM]) >>
133 rpt gen_tac >>
134 `f o SUC o $+ (LENGTH l1) = f o $+ (SUC (LENGTH l1))` suffices_by simp[] >>
135 simp[FUN_EQ_THM, arithmeticTheory.ADD_CLAUSES]
136QED
137
138Theorem FOLDRi_CONG:
139 l1 = l2 ==>
140 (!n e a. n < LENGTH l2 ==> MEM e l2 ==> f1 n e a = f2 n e a) ==>
141 a1 = a2 ==>
142 FOLDRi f1 a1 l1 = FOLDRi f2 a2 l2
143Proof
144 disch_then SUBST_ALL_TAC >> strip_tac >> disch_then SUBST_ALL_TAC >>
145 pop_assum mp_tac >>
146 map_every qid_spec_tac [`f1`, `f2`] >>
147 Induct_on `l2` >> simp[] >> dsimp[LT_SUC] >> rpt strip_tac >>
148 AP_TERM_TAC >> first_x_assum match_mp_tac >> simp[]
149QED
150
151Theorem FOLDRi_CONG':
152 l1 = l2 /\ (!n a. n < LENGTH l2 ==> f1 n (EL n l2) a = f2 n (EL n l2) a) /\
153 a1 = a2 ==>
154 FOLDRi f1 a1 l1 = FOLDRi f2 a2 l2
155Proof
156 strip_tac >> rw[] >> pop_assum mp_tac >>
157 map_every qid_spec_tac [`f1`, `f2`] >> Induct_on `l1` >>
158 dsimp[LT_SUC] >> rpt strip_tac >> AP_TERM_TAC >>
159 first_x_assum match_mp_tac >> simp[]
160QED
161
162Definition findi_def:
163 findi x [] = 0 /\
164 findi x (h::t) = if x = h then 0 else 1 + findi x t
165End
166
167Theorem findi_nil = findi_def |> CONJUNCT1;
168(* val findi_nil = |- !x. findi x [] = 0: thm *)
169
170Theorem findi_cons = findi_def |> CONJUNCT2;
171(* val findi_cons = |- !x h t. findi x (h::t) = if x = h then 0 else 1 + findi x t: thm *)
172
173(* Theorem: ~MEM x ls ==> findi x ls = LENGTH ls *)
174(* Proof:
175 By induction on ls.
176 Base: ~MEM x [] ==> findi x [] = LENGTH []
177 findi x []
178 = 0 by findi_nil
179 = LENGTH [] by LENGTH
180 Step: ~MEM x ls ==> findi x ls = LENGTH ls ==>
181 !h. ~MEM x (h::ls) ==> findi x (h::ls) = LENGTH (h::ls)
182 Note ~MEM x (h::ls)
183 ==> x <> h /\ ~MEM x ls by MEM
184 Thus findi x (h::ls)
185 = 1 + findi x ls by findi_cons
186 = 1 + LENGTH ls by induction hypothesis
187 = SUC (LENGTH ls) by ADD1
188 = LENGTH (h::ls) by LENGTH
189*)
190Theorem findi_none:
191 !ls x. ~MEM x ls ==> findi x ls = LENGTH ls
192Proof
193 rpt strip_tac >>
194 Induct_on `ls` >-
195 simp[findi_nil] >>
196 simp[findi_cons]
197QED
198
199Theorem MEM_findi:
200 MEM x l ==> findi x l < LENGTH l
201Proof
202 Induct_on `l` >> simp[findi_def] >>
203 rw[arithmeticTheory.ADD1, arithmeticTheory.ZERO_LESS_ADD]
204QED
205
206Theorem findi_EL:
207 !l n. n < LENGTH l /\ ALL_DISTINCT l ==> findi (EL n l) l = n
208Proof
209 Induct >> simp[] >> map_every Q.X_GEN_TAC [`h`, `n`] >> strip_tac >>
210 Cases_on `n` >> simp[findi_def] >> rw[arithmeticTheory.ADD1] >>
211 fs[] >> metis_tac[MEM_EL]
212QED
213
214Theorem EL_findi:
215 !l x. MEM x l ==> EL (findi x l) l = x
216Proof
217 Induct_on`l` >> rw[findi_def] >> simp[DECIDE ``1 + x = SUC x``]
218QED
219
220(* Theorem: ALL_DISTINCT ls /\ MEM x ls /\ n < LENGTH ls ==> (x = EL n ls <=> findi x ls = n) *)
221(* Proof:
222 If part: x = EL n ls ==> findi x ls = n
223 Given ALL_DISTINCT ls /\ n < LENGTH ls
224 This is true by findi_EL
225 Only-if part: findi x ls = n ==> x = EL n ls
226 Given MEM x ls
227 This is true by EL_findi
228*)
229Theorem findi_EL_iff:
230 !ls x n. ALL_DISTINCT ls /\ MEM x ls /\ n < LENGTH ls ==> (x = EL n ls <=> findi x ls = n)
231Proof
232 metis_tac[findi_EL, EL_findi]
233QED
234
235(* Theorem: findi x (l1 ++ l2) = if MEM x l1 then findi x l1 else LENGTH l1 + findi x l2 *)
236(* Proof:
237 By induction on l1.
238 Base: findi x ([] ++ l2) = if MEM x [] then findi x [] else LENGTH [] + findi x l2
239 Note MEM x [] = F by MEM
240 so findi x ([] ++ l2)
241 = findi x l2 by APPEND
242 = 0 + findi x l2 by ADD
243 = LENGTH [] + findi x l2 by LENGTH
244 Step: findi x (l1 ++ l2) = if MEM x l1 then findi x l1 else LENGTH l1 + findi x l2 ==>
245 !h. findi x (h::l1 ++ l2) = if MEM x (h::l1) then findi x (h::l1)
246 else LENGTH (h::l1) + findi x l2
247
248 Note findi x (h::l1 ++ l2)
249 = if x = h then 0 else 1 + findi x (l1 ++ l2) by findi_cons
250
251 Case: MEM x (h::l1).
252 To show: findi x (h::l1 ++ l2) = findi x (h::l1).
253 Note MEM x (h::l1)
254 <=> x = h \/ MEM x l1 by MEM
255 If x = h,
256 findi x (h::l1 ++ l2)
257 = 0 = findi x (h::l1) by findi_cons
258 If x <> h, then MEM x l1.
259 findi x (h::l1 ++ l2)
260 = 1 + findi x (l1 ++ l2) by x <> h
261 = 1 + findi x l1 by induction hypothesis
262 = findi x (h::l1) by findi_cons
263
264 Case: ~MEM x (h::l1).
265 To show: findi x (h::l1 ++ l2) = LENGTH (h::l1) + findi x l2.
266 Note ~MEM x (h::l1)
267 <=> x <> h /\ ~MEM x l1 by MEM
268 findi x (h::l1 ++ l2)
269 = 1 + findi x (l1 ++ l2) by x <> h
270 = 1 + (LENGTH l1 + findi x l2) by induction hypothesis
271 = (1 + LENGTH l1) + findi x l2 by arithmetic
272 = LENGTH (h::l1) + findi x l2 by LENGTH
273*)
274Theorem findi_APPEND:
275 !l1 l2 x. findi x (l1 ++ l2) = if MEM x l1 then findi x l1 else LENGTH l1 + findi x l2
276Proof
277 rpt strip_tac >>
278 Induct_on `l1` >-
279 simp[] >>
280 (rw[findi_cons] >> fs[])
281QED
282
283Definition delN_def:
284 delN i [] = [] /\
285 delN i (h::t) = if i = 0 then t
286 else h::delN (i - 1) t
287End
288
289Theorem delN_shortens:
290 !l i. i < LENGTH l ==> LENGTH (delN i l) = LENGTH l - 1
291Proof
292 Induct >> dsimp[delN_def, LT_SUC]
293QED
294
295Theorem EL_delN_BEFORE:
296 !l i j. i < j /\ j < LENGTH l ==> EL i (delN j l) = EL i l
297Proof
298 Induct >> simp[delN_def] >> map_every Q.X_GEN_TAC [`h`, `i`, `j`] >>
299 Cases_on `i` >> simp[]
300QED
301
302Theorem EL_delN_AFTER:
303 !l i j. j <= i /\ i + 1 < LENGTH l ==> (EL i (delN j l) = EL (i + 1) l)
304Proof
305 Induct >> simp[delN_def] >> rw[]
306 >- simp[GSYM arithmeticTheory.ADD1] >>
307 `?i0. i = SUC i0` by (Cases_on `i` >> fs[]) >> rw[] >>
308 fs[arithmeticTheory.ADD_CLAUSES] >> simp[]
309QED
310
311Definition fupdLast_def[simp]:
312 (fupdLast f [] = []) /\
313 (fupdLast f [h] = [f h]) /\
314 (fupdLast f (h::t) = h::fupdLast f t)
315End
316
317Theorem fupdLast_EQ_NIL[simp]:
318 (fupdLast f x = [] <=> x = []) /\
319 ([] = fupdLast f x <=> x = [])
320Proof
321 Cases_on `x` >> simp[] >> Cases_on `t` >> simp[]
322QED
323
324Theorem fupdLast_FRONT_LAST:
325 fupdLast f l = if l = [] then []
326 else FRONT l ++ [f (LAST l)]
327Proof
328 Induct_on `l` >> simp[] >> Cases_on `l` >> simp[]
329QED
330
331(* ----------------------------------------------------------------------
332 LIST_RELi
333 ---------------------------------------------------------------------- *)
334
335val (LIST_RELi_rules, LIST_RELi_ind, LIST_RELi_cases) = Hol_reln`
336 LIST_RELi R [] [] /\
337 !h1 h2 l1 l2.
338 R (LENGTH l1) h1 h2 /\ LIST_RELi R l1 l2 ==>
339 LIST_RELi R (l1 ++ [h1]) (l2 ++ [h2])
340`;
341
342Theorem LIST_RELi_LENGTH:
343 !l1 l2. LIST_RELi R l1 l2 ==> LENGTH l1 = LENGTH l2
344Proof
345 Induct_on `LIST_RELi` >> simp[]
346QED
347
348Theorem LIST_RELi_EL_EQN:
349 LIST_RELi R l1 l2 <=>
350 LENGTH l1 = LENGTH l2 /\ !i. i < LENGTH l1 ==> R i (EL i l1) (EL i l2)
351Proof
352 eq_tac >> map_every qid_spec_tac [`l2`, `l1`]
353 >- (Induct_on `LIST_RELi` >> csimp[] >> rpt strip_tac >>
354 rename1 `i < LENGTH l2 + 1` >>
355 `i < LENGTH l2 \/ i = LENGTH l2` by simp[] >- simp[EL_APPEND1] >>
356 simp[EL_APPEND2]) >>
357 ho_match_mp_tac SNOC_INDUCT >>
358 simp[SNOC_APPEND, LENGTH_NIL_SYM, LIST_RELi_rules] >> rpt strip_tac >>
359 Q.ISPEC_THEN `l2` FULL_STRUCT_CASES_TAC SNOC_CASES >> fs[SNOC_APPEND] >>
360 irule (CONJUNCT2 (SPEC_ALL LIST_RELi_rules)) >> conj_tac
361 >- (rename1 `R (LENGTH l1) x y` >>
362 first_x_assum (qspec_then `LENGTH l1` mp_tac) >> simp[EL_APPEND2]) >>
363 reverse (first_x_assum irule >> conj_tac) >- simp[] >> Q.X_GEN_TAC `j` >>
364 strip_tac >> first_x_assum (qspec_then `j` mp_tac) >> simp[EL_APPEND1]
365QED
366
367Theorem LIST_RELi_thm:
368 (LIST_RELi R [] x <=> (x = [])) /\
369 (LIST_RELi R (h::t) l <=>
370 ?h' t'. l = h'::t' /\ R 0 h h' /\ LIST_RELi (R o SUC) t t')
371Proof
372 simp[LIST_RELi_EL_EQN, LENGTH_NIL_SYM] >> eq_tac >> strip_tac
373 >- (rename1 `l = _ :: _` >> Cases_on `l` >> fs[] >>
374 fs[LT_SUC, DISJ_IMP_THM, FORALL_AND_THM, PULL_EXISTS]) >>
375 var_eq_tac >> dsimp[LT_SUC]
376QED
377
378Theorem LIST_RELi_APPEND_I:
379 LIST_RELi R l1 l2 /\ LIST_RELi (R o ((+) (LENGTH l1))) m1 m2 ==>
380 LIST_RELi R (l1 ++ m1) (l2 ++ m2)
381Proof
382 simp[LIST_RELi_EL_EQN] >> rpt strip_tac >>
383 rename1 `i < LENGTH l2 + LENGTH m2` >> Cases_on `i < LENGTH l2`
384 >- simp[EL_APPEND1]
385 >- (simp[EL_APPEND2] >> first_x_assum (qspec_then `i - LENGTH l2` mp_tac) >>
386 simp[])
387QED
388
389(* ----------------------------------------------------------------------
390 MAP2i
391 ---------------------------------------------------------------------- *)
392
393Definition MAP2i_def[nocompute,simp]:
394 (MAP2i f [] _ = []) /\
395 (MAP2i f _ [] = []) /\
396 (MAP2i f (h1::t1) (h2::t2) = f 0 h1 h2::MAP2i (f o SUC) t1 t2)
397End
398
399(* Define doesn't generate this case, though the second pattern looks as if
400 it should *)
401Theorem MAP2i_NIL2[simp]:
402 MAP2i f l1 [] = []
403Proof
404 Cases_on ‘l1’ >> simp[]
405QED
406
407val MAP2i_ind = theorem"MAP2i_ind";
408
409Theorem LENGTH_MAP2i[simp]:
410 !f l1 l2. LENGTH (MAP2i f l1 l2) = MIN (LENGTH l1) (LENGTH l2)
411Proof
412 ho_match_mp_tac MAP2i_ind >> rw[arithmeticTheory.MIN_DEF]
413QED
414
415Theorem EL_MAP2i:
416 !f l1 l2 n.
417 n < LENGTH l1 /\ n < LENGTH l2 ==>
418 (EL n (MAP2i f l1 l2) = f n (EL n l1) (EL n l2))
419Proof
420 HO_MATCH_MP_TAC MAP2i_ind >> rw[] >> Cases_on‘n’ >> fs[]
421QED
422
423Definition MAP2ia_def[simp]:
424 (MAP2ia f i [] _ = []) /\
425 (MAP2ia f i _ [] = []) /\
426 (MAP2ia f i (h1::t1) (h2::t2) = f i h1 h2 :: MAP2ia f (i + 1) t1 t2)
427End
428
429Theorem MAP2ia_NIL2[simp]:
430 MAP2ia f i l1 [] = []
431Proof
432 Cases_on ‘l1’ >> simp[]
433QED
434
435Theorem MAP2i_compute:
436 MAP2i f l1 l2 = MAP2ia (f:num -> 'a -> 'b -> 'c) 0 l1 l2
437Proof
438 ‘!l1 l2 n f: num -> 'a -> 'b -> 'c.
439 MAP2ia f n l1 l2 = MAP2i (f o (+) n) l1 l2’
440 suffices_by
441 (simp[] >> strip_tac >> rpt (AP_TERM_TAC ORELSE AP_THM_TAC) >>
442 simp[FUN_EQ_THM]) >>
443 Induct >> simp[] >> Cases_on ‘l2’ >> simp[] >>
444 rpt gen_tac >> rpt (AP_TERM_TAC ORELSE AP_THM_TAC) >>
445 simp[FUN_EQ_THM]
446QED
447val _ = computeLib.add_persistent_funs ["MAP2i_compute"]
448val _ = remove_ovl_mapping "MAP2ia" {Name = "MAP2ia", Thy = "indexedLists"}