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