nlistScript.sml

1Theory nlist[bare]
2Ancestors
3  combin pred_set relation arithmetic set_relation numpair list
4  rich_list
5Libs
6  HolKernel Parse boolLib simpLib BasicProvers numSimps TotalDefn
7  metisLib
8
9val _ = Defn.SUC_TO_NUMERAL_DEFN_CONV_hook := numLib.SUC_TO_NUMERAL_DEFN_CONV
10
11fun simp ths g ctxt =
12    simpLib.ASM_SIMP_TAC (srw_ss_of ctxt++numSimps.ARITH_ss) ths g ctxt
13fun fs ths g ctxt =
14    simpLib.FULL_SIMP_TAC (srw_ss_of ctxt++numSimps.ARITH_ss) ths g ctxt
15fun rw ths = SRW_TAC[numSimps.ARITH_ss]ths
16val metis_tac = METIS_TAC
17val qspec_then = Q.SPEC_THEN
18
19(* ----------------------------------------------------------------------
20    lists of naturals encoded as naturals
21   ---------------------------------------------------------------------- *)
22
23Overload nnil = ``0``
24Overload "0" = ``0``
25
26Definition ncons_def:
27  ncons h t = h *, t + 1
28End
29
30Theorem ncons_11[simp]:     ncons x y = ncons h t <=> x = h /\ y = t
31Proof SRW_TAC [][ncons_def]
32QED
33
34Theorem ncons_not_nnil[simp]:
35  ncons x y <> nnil
36Proof
37  SRW_TAC [ARITH_ss][ncons_def]
38QED
39
40Theorem lt_ncons1[simp]:   h < ncons h t
41Proof simp[ncons_def, GSYM LE_LT1]
42QED
43
44Theorem lt_ncons2[simp]:   t < ncons h t
45Proof simp[ncons_def, npair_def]
46QED
47
48(* nlistrec -------------------------------------------------------- *)
49Definition nlistrec_def:
50  nlistrec n f l = if l = 0 then n
51                   else f (nfst (l - 1)) (nsnd (l - 1))
52                          (nlistrec n f (nsnd (l - 1)))
53Termination
54  WF_REL_TAC `measure (SND o SND)` THEN
55  STRIP_TAC THEN ASSUME_TAC (Q.INST [`n` |-> `l - 1`] nsnd_le) THEN
56  simp[]
57End
58
59Theorem nlistrec_thm[simp]:
60  nlistrec n f nnil = n /\
61  nlistrec n f (ncons h t) = f h t (nlistrec n f t)
62Proof
63  CONJ_TAC THEN1 SRW_TAC [][Once nlistrec_def] THEN
64  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [nlistrec_def])) THEN
65  SRW_TAC [ARITH_ss][ncons_def]
66QED
67
68(* allows an induction principle *)
69Theorem nlist_ind:
70  !P. P 0 /\ (!h t. P t ==> P (ncons h t)) ==> !n. P n
71Proof
72  GEN_TAC THEN STRIP_TAC THEN
73  Q_TAC SUFF_TAC `!(n:'a) (f:num -> num -> 'a -> 'a) l. P l`
74    THEN1 METIS_TAC [] THEN
75  HO_MATCH_MP_TAC nlistrec_ind THEN REPEAT STRIP_TAC THEN
76  Cases_on `l` THEN SRW_TAC [][] THEN
77  `SUC n = ncons (nfst n) (nsnd n)` by SRW_TAC [][ncons_def, ADD1] THEN
78  SRW_TAC [][]
79QED
80
81Theorem nlist_cases:
82  !n. (n = nnil) \/ ?h t. n = ncons h t
83Proof
84  Cases_on `n` THEN SRW_TAC [][ncons_def, GSYM ADD1] THEN
85  Q.MATCH_ABBREV_TAC `?h t. n = h *, t` THEN
86  MAP_EVERY Q.EXISTS_TAC [`nfst n`, `nsnd n`] THEN SRW_TAC [][]
87QED
88
89(* nlist_of ------------------------------------------------------- *)
90Definition nlist_of_def[simp]:
91  (nlist_of [] = 0) /\
92  (nlist_of (h::t) = ncons h (nlist_of t))
93End
94
95Theorem nlist_of_EQ0[simp]:
96  (nlist_of l = 0 <=> l = []) /\
97  (0 = nlist_of l <=> l = [])
98Proof
99  Cases_on ‘l’ >> simp[]
100QED
101
102(* listOfN -------------------------------------------------------- *)
103Definition listOfN_def:
104  listOfN = nlistrec [] (\h tn t. h :: t)
105End
106
107Theorem listOfN_zero[simp]:
108  listOfN 0 = []
109Proof simp[listOfN_def]
110QED
111
112Theorem listOfN_ncons[simp]:
113  listOfN (ncons h t) = h :: listOfN t
114Proof
115  simp[listOfN_def]
116QED
117
118Theorem listOfN_EQ_NIL[simp]:
119  (listOfN l = [] <=> l = 0) /\ ([] = listOfN l <=> l = 0)
120Proof
121  qspec_then ‘l’ strip_assume_tac nlist_cases >> simp[]
122QED
123
124Theorem listOfN_EQ_CONS:
125  listOfN n = h :: t <=> ?tn. n = ncons h tn /\ listOfN tn = t
126Proof
127  rw[listOfN_def] >> Q.SPEC_THEN ‘n’ strip_assume_tac nlist_cases >> rw[]
128QED
129
130(* nlist_of and listOfN are inverse, bijection results follow *)
131Theorem nlist_listOfN[simp]:
132  !l. nlist_of (listOfN l) = l
133Proof
134  ho_match_mp_tac nlist_ind >> simp[]
135QED
136
137Theorem listOfN_nlist[simp]:
138  !l. listOfN (nlist_of l) = l
139Proof
140  Induct_on `l` >> simp[]
141QED
142
143Theorem listOfN_SURJ:
144  !l. ?n. listOfN n = l
145Proof
146  METIS_TAC[listOfN_nlist]
147QED
148
149Theorem listOfN_INJ[simp]:
150  !l1 l2. listOfN l1 = listOfN l2 <=> l1 = l2
151Proof
152  METIS_TAC[nlist_listOfN]
153QED
154
155Theorem nlist_of_INJ[simp]:
156  !n1 n2. nlist_of n1 = nlist_of n2 <=> n1 = n2
157Proof
158  METIS_TAC[listOfN_nlist]
159QED
160
161Theorem nlist_of_SURJ:
162  !l. ?n. nlist_of n = l
163Proof
164  METIS_TAC[nlist_listOfN]
165QED
166
167(* copy various functions on maps across to number land *)
168Overload nlen = “\n. LENGTH (listOfN n)”
169Overload napp = “\n1 n2. nlist_of (listOfN n1 ++ listOfN n2)”
170Overload nfoldl = “\f a n. FOLDL f a (listOfN n)”
171Overload nmap = “\f n. nlist_of (MAP f (listOfN n))”
172
173(* some functions are partial over general lists, but can be made total
174   here by using 0 as default values *)
175
176(* nhd ------------------------------------------------------------ *)
177Definition nhd_def: nhd nl = nfst (nl - 1)
178End
179
180Theorem nhd0[simp]:
181  nhd 0 = 0
182Proof
183  simp[nhd_def]
184QED
185
186Theorem nhd_thm[simp]: nhd (ncons h t) = h
187Proof SRW_TAC [][ncons_def, nhd_def]
188QED
189
190(* ntl ------------------------------------------------------------ *)
191Definition ntl_def: ntl nlist = nsnd (nlist - 1)
192End
193
194Theorem ntl_zero[simp]:
195  ntl 0 = 0
196Proof
197  simp[ntl_def]
198QED
199
200Theorem ntl_thm[simp]:  ntl (ncons h t) = t
201Proof simp[ncons_def, ntl_def]
202QED
203
204Theorem ntl_LT:
205  0 < n ==> ntl n < n
206Proof
207  rw[ntl_def] >> Induct_on `n` >- (strip_tac >> fs[]) >>
208  rw[nsnd_def]
209QED
210
211Theorem ncons_nhd_ntl:
212  !l. l <> 0 ==> ncons (nhd l) (ntl l) = l
213Proof
214  Cases_on `l` >- simp[] >> simp[ncons_def,nhd_def,ntl_def]
215QED
216
217Theorem ntl_zero_empty_OR_ncons:
218  ntl l = 0 <=> l = 0 \/ ?x. l = ncons x 0
219Proof
220  eq_tac >- METIS_TAC[ncons_nhd_ntl] >>
221  simp[DISJ_IMP_THM, PULL_EXISTS] >>
222  rw[ntl_def]
223QED
224
225(* ndrop ---------------------------------------------------------- *)
226Overload ndrop = “\n l. nlist_of (DROP n (listOfN l))”
227
228Theorem ndrop_SUC[simp]:
229  !l n. ndrop (SUC n) l = ntl (ndrop n l)
230Proof
231  ho_match_mp_tac nlist_ind >> rw[] >>
232  Cases_on ‘n’ >> simp[]
233QED
234
235Theorem ntl_ndrop:
236  !l. ntl (ndrop n l) = ndrop n (ntl l)
237Proof     Induct_on `n` >> simp[]
238QED
239
240(* nel ------------------------------------------------------------ *)
241Definition nel_def:         nel n nlist = nhd (ndrop n nlist)
242End
243
244Theorem nel_nnil[simp]:     nel x 0 = 0
245Proof simp[nel_def]
246QED
247
248Theorem nel0_ncons[simp]:   nel 0 (ncons h t) = h
249Proof simp[nel_def]
250QED
251
252Theorem nel_nhd:            nel 0 l = nhd l
253Proof simp[nel_def]
254QED
255
256Theorem nel_SUC_CONS[simp]: !n h t. nel (SUC n) (ncons h t) = nel n t
257Proof simp[nel_def] >> Induct >> simp[]
258QED
259
260(* nlast ---------------------------------------------------------- *)
261Definition nlast_def:
262  nlast = nlistrec 0 (\h tn rn. if tn = 0 then h else rn)
263End
264
265Theorem nlast_nnil[simp]:   nlast 0 = 0
266Proof simp[nlast_def]
267QED
268
269Theorem nlast_ncons[simp]:
270  nlast (ncons h tn) = if tn = 0 then h else nlast tn
271Proof
272  simp[nlast_def]
273QED
274
275Theorem nlast_nel:
276  !l. nlast l = nel (nlen l - 1) l
277Proof
278  ho_match_mp_tac nlist_ind >> simp[] >> rw[] >>
279  Q.SPEC_THEN ‘l’ strip_assume_tac nlist_cases >> rw[]
280QED
281
282(* nfront --------------------------------------------------------- *)
283Definition nfront_def:
284  nfront = nlistrec 0 (\h tn rn. if tn = 0 then 0 else ncons h rn)
285End
286
287Theorem nfront_nnil[simp]:  nfront 0 = 0
288Proof
289  simp[nfront_def]
290QED
291
292Theorem nfront_nsingl[simp]:  nfront (ncons x 0) = 0
293Proof simp[nfront_def]
294QED
295
296Theorem nfront_thm:
297  nfront 0 = 0 /\
298  nfront (ncons h t) = if t = 0 then 0 else ncons h (nfront t)
299Proof
300  simp[nfront_def]
301QED
302
303Theorem nhd_nfront:
304  !l. l <> 0 /\ ntl l <> 0 ==> nhd (nfront l) = nhd l
305Proof
306  ho_match_mp_tac nlist_ind >> simp[] >> rw[] >>
307  simp[Once nfront_def]
308QED
309
310Theorem LENGTH_nfront:
311  !t. t <> 0 ==> nlen (nfront t) = nlen t - 1
312Proof
313  ho_match_mp_tac nlist_ind >> simp[nfront_thm] >> rw[] >>
314  ‘nlen t <> 0’ suffices_by numLib.ARITH_TAC >>
315  simp[]
316QED
317
318Theorem ncons_x_0_LENGTH_1:
319  nlen l = 1 <=> ?n. l = ncons n 0
320Proof
321  qspec_then ‘l’ strip_assume_tac nlist_cases >> simp[]
322QED
323
324Theorem ndrop_nsingl:
325  m <> 0 ==> ndrop m (ncons x 0) = 0
326Proof
327  Cases_on ‘m’ >> simp[ntl_ndrop]
328QED
329
330Theorem ntl_DROP:
331  !l m. ntl (nlist_of (DROP m l)) = ndrop m (ntl (nlist_of l))
332Proof
333  Induct >> rw[] >> Cases_on ‘m’ >> simp[] >> Cases_on ‘l’ >> simp[]
334QED
335
336Theorem nel_nfront:
337  !t. m < nlen (nfront t) ==> nel m (nfront t) = nel m t
338Proof
339  simp[nel_def] >> Induct_on `m` >> simp[] >> gen_tac >>
340  Q.SPEC_THEN `t` STRUCT_CASES_TAC nlist_cases >> simp[nfront_thm] >> rw[] >>
341  simp[ntl_DROP]
342QED
343
344Theorem nsnoc_cases:
345  !t. t = 0 \/ ?f l. t = napp f (ncons l 0)
346Proof
347  ho_match_mp_tac nlist_ind >> simp[] >> rw[]
348  >- (Q.RENAME_TAC [‘ncons h 0’] >> MAP_EVERY Q.EXISTS_TAC [‘0’, ‘h’] >>
349      simp[]) >>
350  simp[GSYM nlist_of_def, Excl "nlist_of_def"] >>
351  Q.RENAME_TAC [‘h1::(listOfN f ++ [h2])’] >>
352  MAP_EVERY Q.EXISTS_TAC [‘ncons h1 f’, ‘h2’] >> simp[]
353QED
354
355Theorem nhd_napp:
356  !l1 l2. l1 <> 0 ==> nhd (napp l1 l2) = nhd l1
357Proof
358  rpt gen_tac >> Q.SPEC_THEN ‘l1’ strip_assume_tac nlist_cases >> simp[]
359QED
360
361Theorem nel_napp:
362  !l1 l2. n < nlen l1 ==> nel n (napp l1 l2) = nel n l1
363Proof
364  Induct_on `n` >> simp[]
365  >- (rpt gen_tac >> qspec_then `l1` STRUCT_CASES_TAC nlist_cases >> simp[]) >>
366  rpt gen_tac >> qspec_then `l1` STRUCT_CASES_TAC nlist_cases >> simp[]
367QED
368
369Theorem nfront_napp_sing[simp]:
370  !pfx. nfront (napp pfx (ncons e 0)) = pfx
371Proof
372  ho_match_mp_tac nlist_ind >> simp[nfront_def]
373QED
374
375Theorem nel_napp2:
376  !y n x. nlen x <= n ==> (nel n (napp x y) = nel (n - nlen x) y)
377Proof
378  Induct_on `n` >> simp[] >>
379  rpt strip_tac >> qspec_then `x` FULL_STRUCT_CASES_TAC nlist_cases >>
380  fs[]
381QED
382
383Theorem nel_ncons_nonzero:
384  0 < n ==> (nel n (ncons h t) = nel (n - 1) t)
385Proof
386  Cases_on ‘n’ >> simp[]
387QED
388
389
390Theorem napp_nsnoc_lt:
391  !l. l < napp l (ncons x 0)
392Proof
393  ho_match_mp_tac nlist_ind >> rpt strip_tac >> simp[] >>
394  fs[ncons_def]
395QED
396
397Theorem napp_sing_eq[simp]:
398  napp l1 (ncons l 0) = ncons x 0 <=> l1 = 0 /\ x = l
399Proof
400  qspec_then `l1` STRUCT_CASES_TAC nlist_cases >> simp[]
401QED
402
403Theorem nel_correct:
404  !l i. i < nlen l ==> EL i (listOfN l) = nel i l
405Proof
406  ho_match_mp_tac nlist_ind >> simp [] >> rw[] >> Cases_on ‘i’ >> simp[]
407QED
408
409
410Theorem nel_eq_nlist:
411  !l1 l2. l1 = l2 <=>
412            nlen l1 = nlen l2 /\
413            !m. m < nlen l1 ==> nel m l1 = nel m l2
414Proof
415  rw[] >>
416  ‘(?L1. l1 = nlist_of L1) /\ (?L2. l2 = nlist_of L2)’
417     by metis_tac[nlist_of_SURJ] >>
418  simp[GSYM nel_correct, LIST_EQ_REWRITE, EQ_IMP_THM]
419QED
420
421Theorem nlast_napp:
422  !l1 l2. l2 <> 0 ==> nlast (napp l1 l2) = nlast l2
423Proof
424  ho_match_mp_tac nlist_ind >> simp[]
425QED
426
427Theorem napp_ndrop_l1_empty[simp]:
428  !l1 l2. ndrop (nlen l1) (napp l1 l2) = l2
429Proof
430  simp[DROP_LENGTH_APPEND]
431QED
432
433Theorem ntl_LE :
434!n. ntl n <= n
435Proof
436rw[ntl_def,ncons_def] >> `nsnd (n - 1) <= n - 1` by fs[nsnd_le] >> fs[]
437QED
438
439Theorem ntl_nonzero_LESS :
440!n. n <> 0 ==> ntl n < n
441Proof
442rw[ntl_def,ncons_def] >> `nsnd (n - 1) <= n - 1` by fs[nsnd_le] >>
443`n - 1 < n` by fs[] >> fs[]
444QED
445
446
447Theorem MEM_listOfN_LESS :
448  !l e. MEM e (listOfN l) ==> e < l
449Proof
450  ho_match_mp_tac nlist_ind >> simp[DISJ_IMP_THM, FORALL_AND_THM] >> rw[] >>
451  res_tac >> irule LESS_TRANS >> Q.EXISTS_TAC ‘l’ >> simp[]
452QED
453
454
455
456