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