listScript.sml
1(* ===================================================================== *)
2(* FILE : listScript.sml *)
3(* DESCRIPTION : The logical definition of the list type operator. The *)
4(* type is defined and the following "axiomatization" is *)
5(* proven from the definition of the type: *)
6(* *)
7(* |- !x f. ?fn. (fn [] = x) /\ *)
8(* (!h t. fn (h::t) = f (fn t) h t) *)
9(* *)
10(* Translated from hol88. *)
11(* *)
12(* AUTHOR : (c) Tom Melham, University of Cambridge *)
13(* DATE : 86.11.24 *)
14(* REVISED : 87.03.14 *)
15(* TRANSLATOR : Konrad Slind, University of Calgary *)
16(* DATE : September 15, 1991 *)
17(* ===================================================================== *)
18Theory list[bare]
19Ancestors
20 arithmetic pair pred_set relation combin basicSize[qualified]
21Libs
22 HolKernel Parse boolLib BasicProvers Num_conv mesonLib simpLib
23 boolSimps pred_setLib TotalDefn metisLib quotientLib
24 Datatype[qualified] OpenTheoryMap[qualified]
25
26val ERR = mk_HOL_ERR "listScript"
27
28val arith_ss = bool_ss ++ numSimps.ARITH_ss ++ numSimps.REDUCE_ss
29fun simp l = ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss++numSimps.ARITH_ss) l
30val rw = SRW_TAC []
31val metis_tac = METIS_TAC
32fun fs l = FULL_SIMP_TAC (srw_ss()) l
33val std_ss = arith_ss ++ boolSimps.LET_ss;
34
35fun DECIDE_TAC (g as (asl,_)) =
36 ((MAP_EVERY UNDISCH_TAC (filter numSimps.is_arith asl) THEN
37 CONV_TAC Arith.ARITH_CONV)
38 ORELSE tautLib.TAUT_TAC) g;
39val decide_tac = DECIDE_TAC;
40val qexists_tac = Q.EXISTS_TAC;
41val qid_spec_tac = Q.ID_SPEC_TAC;
42val qx_gen_tac = Q.X_GEN_TAC;
43
44val qxch = Q.X_CHOOSE_THEN;
45fun qxchl [] ttac = ttac
46 | qxchl (q::qs) ttac = qxch q (qxchl qs ttac);
47
48val _ = Rewrite.add_implicit_rewrites pairLib.pair_rws;
49
50val NOT_SUC = numTheory.NOT_SUC
51and INV_SUC = numTheory.INV_SUC
52fun INDUCT_TAC g = INDUCT_THEN numTheory.INDUCTION ASSUME_TAC g;
53
54val LESS_0 = prim_recTheory.LESS_0;
55val NOT_LESS_0 = prim_recTheory.NOT_LESS_0;
56val PRE = prim_recTheory.PRE;
57val LESS_MONO = prim_recTheory.LESS_MONO;
58val INV_SUC_EQ = prim_recTheory.INV_SUC_EQ;
59val num_Axiom = prim_recTheory.num_Axiom;
60val PAIR_EQ = pairTheory.PAIR_EQ;
61
62(*---------------------------------------------------------------------------*)
63(* Declare the datatype of lists *)
64(*---------------------------------------------------------------------------*)
65
66val _ = Datatype.Hol_datatype ‘list = NIL | CONS of 'a => list’;
67
68local open OpenTheoryMap val cname = OpenTheory_const_name in
69val ns = ["Data","List"]
70val _ = OpenTheory_tyop_name{tyop={Thy="list",Tyop="list"},name=(ns,"list")}
71val _ = cname{const={Thy="list",Name="APPEND"},name=(ns,"@")}
72val _ = cname{const={Thy="list",Name="CONS"},name=(ns,"::")}
73val _ = cname{const={Thy="list",Name="HD"},name=(ns,"head")}
74val _ = cname{const={Thy="list",Name="EVERY"},name=(ns,"all")}
75val _ = cname{const={Thy="list",Name="EXISTS"},name=(ns,"any")}
76val _ = cname{const={Thy="list",Name="FILTER"},name=(ns,"filter")}
77val _ = cname{const={Thy="list",Name="FLAT"},name=(ns,"concat")}
78val _ = cname{const={Thy="list",Name="LENGTH"},name=(ns,"length")}
79val _ = cname{const={Thy="list",Name="MAP"},name=(ns,"map")}
80val _ = cname{const={Thy="list",Name="NIL"},name=(ns,"[]")}
81val _ = cname{const={Thy="list",Name="REVERSE"},name=(ns,"reverse")}
82val _ = cname{const={Thy="list",Name="TAKE"},name=(ns,"take")}
83val _ = cname{const={Thy="list",Name="TL"},name=(ns,"tail")}
84end
85
86(*---------------------------------------------------------------------------*)
87(* Fiddle with concrete syntax *)
88(*---------------------------------------------------------------------------*)
89
90val _ = add_rule {term_name = "CONS", fixity = Infixr 490,
91 pp_elements = [TOK "::", BreakSpace(0,2)],
92 paren_style = OnlyIfNecessary,
93 block_style = (AroundSameName, (PP.INCONSISTENT, 0))};
94
95val _ = add_listform {separator = [TOK ";", BreakSpace(1,0)],
96 leftdelim = [TOK "["], rightdelim = [TOK "]"],
97 cons = "CONS", nilstr = "NIL",
98 block_info = (PP.INCONSISTENT, 1)};
99
100(*---------------------------------------------------------------------------*)
101(* Prove the axiomatization of lists *)
102(*---------------------------------------------------------------------------*)
103
104val list_Axiom = TypeBase.axiom_of “:'a list”;
105
106Theorem list_Axiom_old:
107 !x f. ?!fn1:'a list -> 'b.
108 (fn1 [] = x) /\ (!h t. fn1 (h::t) = f (fn1 t) h t)
109Proof
110 REPEAT GEN_TAC THEN CONV_TAC EXISTS_UNIQUE_CONV THEN CONJ_TAC THENL [
111 ASSUME_TAC list_Axiom THEN
112 POP_ASSUM (ACCEPT_TAC o BETA_RULE o Q.SPECL [‘x’, ‘\x y z. f z x y’]),
113 REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN
114 HO_MATCH_MP_TAC (TypeBase.induction_of “:'a list”) THEN
115 simpLib.ASM_SIMP_TAC boolSimps.bool_ss []
116 ]
117QED
118
119(*---------------------------------------------------------------------------
120 Now some definitions.
121 ---------------------------------------------------------------------------*)
122
123Definition NULL_DEF:
124 (NULL [] = T) /\
125 (NULL (h::t) = F)
126End
127
128Definition HD[simp]:
129 HD (h::t) = h
130End
131
132Definition TL_DEF[simp]:
133 TL [] = [] /\
134 TL (h::t) = t
135End
136Theorem TL = CONJUNCT2 TL_DEF
137
138Definition SUM:
139 SUM [] = 0 /\
140 SUM (h::t) = h + SUM t
141End
142
143Definition APPEND_def:
144 APPEND [] l = l /\
145 APPEND (h::l1) l2 = h::APPEND l1 l2
146End
147
148val _ = set_fixity "++" (Infixl 480);
149Overload "++" = Term‘APPEND’
150val _ = Unicode.unicode_version {u = UnicodeChars.doubleplus, tmnm = "++"}
151val _ = TeX_notation { hol = UnicodeChars.doubleplus,
152 TeX = ("\\HOLTokenDoublePlus", 1) }
153val _ = TeX_notation { hol = "++", TeX = ("\\HOLTokenDoublePlus", 1) };
154
155(* preserving old choice of quantification order *)
156Theorem APPEND[simp]:
157 (!l:'a list. APPEND [] l = l) /\
158 (!l1 l2 h:'a. APPEND (h::l1) l2 = h::(APPEND l1 l2))
159Proof
160 REWRITE_TAC[APPEND_def]
161QED
162
163Definition FLAT[simp]:
164 FLAT [] = [] /\
165 FLAT (h::t) = APPEND h (FLAT t)
166End
167
168Definition LENGTH[simp]:
169 LENGTH [] = 0 /\
170 LENGTH (h::t) = SUC (LENGTH t)
171End
172
173Definition MAP[simp]:
174 MAP (f:'a -> 'b) [] = [] /\
175 MAP f (h::t) = f h::MAP f t
176End
177
178Definition LIST_TO_SET_DEF[simp]:
179 (LIST_TO_SET [] x <=> F) /\
180 (LIST_TO_SET (h::t) x <=> (x = h) \/ LIST_TO_SET t x)
181End
182
183Overload set = “LIST_TO_SET”
184Overload MEM = “\h:'a l:'a list. h IN LIST_TO_SET l”
185Overload "" = “\h:'a l:'a list. ~(h IN LIST_TO_SET l)”
186 (* last over load here causes the term ~(h IN LIST_TO_SET l) to not print
187 using overloads. In particular, this prevents the existing overload for
188 NOTIN from firing in this type instance, and allows ~MEM a l to print
189 because the pretty-printer will traverse into the negated term (printing
190 the ~), and then the MEM overload will "fire".
191 *)
192
193Theorem LIST_TO_SET[simp]:
194 LIST_TO_SET [] = {} /\
195 LIST_TO_SET (h::t) = h INSERT LIST_TO_SET t
196Proof
197 SRW_TAC [] [FUN_EQ_THM, IN_DEF]
198QED
199
200Definition FILTER[simp]:
201 FILTER P [] = [] /\
202 FILTER P (h::t) = if P h then (h::FILTER P t) else FILTER P t
203End
204
205Definition FOLDR:
206 FOLDR (f:'a->'b->'b) e [] = e /\
207 FOLDR f e (x::l) = f x (FOLDR f e l)
208End
209
210Definition FOLDL:
211 FOLDL (f:'b->'a->'b) e [] = e /\
212 FOLDL f e (x::l) = FOLDL f (f e x) l
213End
214
215Definition EVERY_DEF[simp]:
216 (EVERY P [] <=> T) /\
217 (EVERY P (h::t) <=> P h /\ EVERY P t)
218End
219
220Definition EXISTS_DEF[simp]:
221 (EXISTS P [] <=> F) /\
222 (EXISTS P (h::t) <=> P h \/ EXISTS P t)
223End
224
225Definition EL_def:
226 EL 0 l = (HD l:'a) /\
227 EL (SUC n) l = EL n (TL l)
228End
229
230(* preserving particular variable quantification order *)
231Theorem EL:
232 (!(l:'a list). EL 0 l = HD l:'a) /\
233 (!(l:'a list) n. EL (SUC n) l = EL n (TL l))
234Proof
235 REWRITE_TAC[EL_def]
236QED
237
238(* ---------------------------------------------------------------------*)
239(* Definition of a function *)
240(* *)
241(* MAP2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list *)
242(* *)
243(* for mapping a curried binary function down a pair of lists: *)
244(* *)
245(* |- (!f. MAP2 f[][] = []) /\ *)
246(* (!f h1 t1 h2 t2. *)
247(* MAP2 f(h1::t1)(h2::t2) = CONS(f h1 h2)(MAP2 f t1 t2)) *)
248(* *)
249(* [TFM 92.04.21] *)
250(* ---------------------------------------------------------------------*)
251
252Definition MAP2_DEF[simp]:
253 (MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2) /\
254 (MAP2 f x y = [])
255End
256
257Theorem MAP2:
258 (!f. MAP2 f [] [] = []) /\
259 (!f h1 t1 h2 t2. MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2)
260Proof
261METIS_TAC[MAP2_DEF]
262QED
263
264Theorem MAP2_NIL[simp]:
265 MAP2 f x [] = []
266Proof
267 Cases_on ‘x’ >> simp[]
268QED
269
270Theorem LENGTH_MAP2[simp]:
271 !xs ys. LENGTH (MAP2 f xs ys) = MIN (LENGTH xs) (LENGTH ys)
272Proof
273 Induct \\ rw [] \\ Cases_on ‘ys’ \\ fs [arithmeticTheory.MIN_DEF, MAP2_DEF]
274 \\ SRW_TAC[][]
275QED
276
277Theorem EL_MAP2:
278 !ts tt n.
279 n < MIN (LENGTH ts) (LENGTH tt) ==>
280 (EL n (MAP2 f ts tt) = f (EL n ts) (EL n tt))
281Proof
282 Induct \\ rw [] \\ Cases_on ‘tt’ \\ Cases_on ‘n’ \\ fs [EL]
283QED
284
285Theorem MAP2_APPEND:
286 !xs ys xs1 ys1 f.
287 (LENGTH xs = LENGTH xs1) ==>
288 (MAP2 f (xs ++ ys) (xs1 ++ ys1) = MAP2 f xs xs1 ++ MAP2 f ys ys1)
289Proof Induct >> Cases_on ‘xs1’ >> fs [MAP2]
290QED
291
292(* ----------------------------------------------------------------------
293 mapPartial : ('a -> 'b option) -> 'a list -> 'b list
294 ---------------------------------------------------------------------- *)
295
296Definition mapPartial_def[simp]:
297 mapPartial f [] = [] /\
298 mapPartial f (x :: xs) = case f x of NONE => mapPartial f xs
299 | SOME y => y :: mapPartial f xs
300End
301
302Theorem mapPartial_EQ_NIL[simp]:
303 mapPartial f xs = [] <=> !x. MEM x xs ==> f x = NONE
304Proof
305 Q.ID_SPEC_TAC ‘xs’ >> Induct >> simp[optionTheory.option_case_eq] >>
306 metis_tac[]
307QED
308
309Theorem LENGTH_mapPartial:
310 LENGTH (mapPartial f xs) <= LENGTH xs
311Proof
312 Q.ID_SPEC_TAC ‘xs’ >> Induct >>
313 simp[] >> strip_tac >>
314 DEEP_INTRO_TAC (GEN_ALL $ iffRL $ TypeBase.case_pred_disj_of “:'a option”) >>
315 simp[] >> metis_tac[TypeBase.nchotomy_of “:'a option”]
316QED
317
318(* Some searches *)
319
320Definition INDEX_FIND_def:
321 (INDEX_FIND i P [] = NONE) /\
322 (INDEX_FIND i P (h :: t) =
323 if P h then SOME (i, h) else INDEX_FIND (SUC i) P t)
324End
325
326Definition FIND_def: FIND P = OPTION_MAP SND o INDEX_FIND 0 P
327End
328Definition INDEX_OF_def: INDEX_OF x = OPTION_MAP FST o INDEX_FIND 0 ($= x)
329End
330
331Theorem INDEX_FIND_add:
332 !ls n.
333 INDEX_FIND n P ls = OPTION_MAP (\(i, x). (i + n, x)) (INDEX_FIND 0 P ls)
334Proof
335 Induct >- ( rw[Once INDEX_FIND_def] \\ rw[Once INDEX_FIND_def] )
336 \\ simp_tac(srw_ss())[Once INDEX_FIND_def, SimpRHS]
337 \\ simp_tac(srw_ss())[Once INDEX_FIND_def]
338 \\ rpt gen_tac
339 \\ IF_CASES_TAC \\ simp_tac(srw_ss())[]
340 \\ first_assum(Q.SPEC_THEN`SUC n`(fn th => simp_tac(srw_ss())[th]))
341 \\ first_x_assum(Q.SPEC_THEN`1`(fn th => simp_tac(srw_ss())[th]))
342 \\ Cases_on`INDEX_FIND 0 P ls` \\ simp[]
343 \\ simp[UNCURRY]
344QED
345
346Theorem FIND_thm:
347 (FIND P [] = NONE) /\
348 (FIND P (h::t) = if P h then SOME h else FIND P t)
349Proof
350 rw[FIND_def, INDEX_FIND_def] >> simp[Once INDEX_FIND_add, SimpLHS] >>
351 simp[optionTheory.OPTION_MAP_COMPOSE, o_UNCURRY_R, combinTheory.o_ABS_R] >>
352 rpt (AP_TERM_TAC ORELSE AP_THM_TAC) >>
353 simp[FUN_EQ_THM, FORALL_PROD]
354QED
355
356
357Theorem INDEX_OF_eq_NONE:
358 !x l. INDEX_OF x l = NONE <=> ~MEM x l
359Proof
360 gen_tac \\ Induct
361 \\ rw[INDEX_OF_def, INDEX_FIND_def]
362 \\ rw[Once INDEX_FIND_add]
363 \\ fs[INDEX_OF_def]
364QED
365
366Theorem INDEX_OF_eq_SOME:
367 !x l i. INDEX_OF x l = SOME i <=>
368 (i < LENGTH l) /\ (EL i l = x) /\ (!j. (j < i) ==> EL j l <> x)
369Proof
370 gen_tac \\ Induct
371 \\ simp[INDEX_OF_def, INDEX_FIND_def]
372 \\ rpt gen_tac
373 \\ simp[Once INDEX_FIND_add]
374 \\ fs[INDEX_OF_def]
375 \\ rw[PULL_EXISTS, UNCURRY]
376 >- (
377 Cases_on`i` \\ rw[EL]
378 \\ rpt disj2_tac
379 \\ Q.EXISTS_TAC`0` \\ rw[EL] )
380 \\ Cases_on`i` \\ rw[arithmeticTheory.ADD1, EL]
381 \\ rw[Once arithmeticTheory.FORALL_NUM, SimpRHS]
382 \\ rw[arithmeticTheory.ADD1, EL]
383QED
384
385(* ---------------------------------------------------------------------*)
386(* Proofs of some theorems about lists. *)
387(* ---------------------------------------------------------------------*)
388
389Theorem NULL:
390 NULL ([] :'a list) /\ (!h t. ~NULL(CONS (h:'a) t))
391Proof
392 REWRITE_TAC [NULL_DEF]
393QED
394
395(*---------------------------------------------------------------------------*)
396(* List induction *)
397(* |- P [] /\ (!t. P t ==> !h. P(h::t)) ==> (!x.P x) *)
398(*---------------------------------------------------------------------------*)
399
400Theorem list_INDUCT0 = TypeBase.induction_of “:'a list”;
401
402Theorem list_INDUCT:
403 !P. P [] /\ (!t. P t ==> !h. P (h::t)) ==> !l. P l
404Proof
405 REWRITE_TAC [list_INDUCT0]
406QED(* must use REWRITE_TAC, ACCEPT_TAC refuses
407 to respect bound variable names *)
408
409Theorem list_induction[allow_rebind] = list_INDUCT
410val LIST_INDUCT_TAC = INDUCT_THEN list_INDUCT ASSUME_TAC;
411
412(*---------------------------------------------------------------------------*)
413(* Cases theorem: |- !l. (l = []) \/ (?t h. l = h::t) *)
414(*---------------------------------------------------------------------------*)
415
416val list_cases = TypeBase.nchotomy_of “:'a list”;
417
418
419Theorem list_CASES:
420 !l. (l = []) \/ (?h t. l = h::t)
421Proof
422 mesonLib.MESON_TAC [list_cases]
423QED
424
425Theorem list_nchotomy[allow_rebind] = list_CASES
426
427(*---------------------------------------------------------------------------*)
428(* Definition of list_case more suitable to call-by-value computations *)
429(*---------------------------------------------------------------------------*)
430
431val list_case_def = TypeBase.case_def_of “:'a list”;
432
433Theorem list_case_compute:
434 !(l:'a list). list_CASE l (b:'b) f =
435 if NULL l then b else f (HD l) (TL l)
436Proof
437 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [list_case_def, HD, TL, NULL_DEF]
438QED
439
440(*---------------------------------------------------------------------------*)
441(* CONS_11: |- !h t h' t'. (h::t = h' :: t') = (h = h') /\ (t = t') *)
442(*---------------------------------------------------------------------------*)
443
444Theorem CONS_11 = TypeBase.one_one_of “:'a list”
445
446Theorem NOT_NIL_CONS = TypeBase.distinct_of “:'a list”;
447
448Theorem NOT_CONS_NIL =
449 CONV_RULE(ONCE_DEPTH_CONV SYM_CONV) NOT_NIL_CONS;
450
451Theorem LIST_NOT_EQ:
452 !l1 l2. ~(l1 = l2) ==> !h1:'a. !h2. ~(h1::l1 = h2::l2)
453Proof
454 REPEAT GEN_TAC THEN
455 STRIP_TAC THEN
456 ASM_REWRITE_TAC [CONS_11]
457QED
458
459Theorem NOT_EQ_LIST:
460 !h1:'a. !h2. ~(h1 = h2) ==> !l1 l2. ~(h1::l1 = h2::l2)
461Proof
462 REPEAT GEN_TAC THEN
463 STRIP_TAC THEN
464 ASM_REWRITE_TAC [CONS_11]
465QED
466
467Theorem EQ_LIST:
468 !h1:'a.!h2.(h1=h2) ==> !l1 l2. (l1 = l2) ==> (h1::l1 = h2::l2)
469Proof
470 REPEAT STRIP_TAC THEN
471 ASM_REWRITE_TAC [CONS_11]
472QED
473
474(* Theorem: ls <> [] <=> (ls = HD ls::TL ls) *)
475(* Proof:
476 If part: ls <> [] ==> (ls = HD ls::TL ls)
477 ls <> []
478 ==> ?h t. ls = h::t by list_CASES
479 ==> ls = (HD ls)::(TL ls) by HD, TL
480 Only-if part: (ls = HD ls::TL ls) ==> ls <> []
481 This is true by NOT_NIL_CONS
482*)
483Theorem LIST_NOT_NIL:
484 !ls. ls <> [] <=> (ls = HD ls::TL ls)
485Proof
486 metis_tac[list_CASES, HD, TL, NOT_NIL_CONS]
487QED
488
489Theorem CONS:
490 !l : 'a list. ~NULL l ==> HD l :: TL l = l
491Proof
492 STRIP_TAC THEN
493 STRIP_ASSUME_TAC (SPEC “l:'a list” list_CASES) THEN
494 POP_ASSUM SUBST1_TAC THEN
495 ASM_REWRITE_TAC [HD, TL, NULL]
496QED
497
498Theorem APPEND_NIL[simp]:
499 !(l:'a list). APPEND l [] = l
500Proof LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [APPEND]
501QED
502
503
504Theorem APPEND_ASSOC:
505 !(l1:'a list) l2 l3.
506 APPEND l1 (APPEND l2 l3) = APPEND (APPEND l1 l2) l3
507Proof LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [APPEND]
508QED
509
510Theorem LENGTH_APPEND[simp]:
511 !(l1:'a list) (l2:'a list).
512 LENGTH (APPEND l1 l2) = LENGTH l1 + LENGTH l2
513Proof
514 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [LENGTH, APPEND, ADD_CLAUSES]
515QED
516
517Theorem MAP_APPEND[simp]:
518 !(f:'a->'b) l1 l2.
519 MAP f (APPEND l1 l2) = APPEND (MAP f l1) (MAP f l2)
520Proof
521 STRIP_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [MAP, APPEND]
522QED
523
524Theorem MAP_ID[simp]:
525 (MAP (\x. x) l = l) /\ (MAP I l = l)
526Proof
527 Induct_on ‘l’ THEN SRW_TAC [] [MAP]
528QED
529
530Theorem MAP_ID_I[quotient_simp]:
531 MAP I = I
532Proof
533 simp[FUN_EQ_THM]
534QED
535
536Theorem LENGTH_MAP[simp]:
537 !l (f:'a->'b). LENGTH (MAP f l) = LENGTH l
538Proof
539 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [MAP, LENGTH]
540QED
541
542Theorem MAP_EQ_NIL[simp]:
543 !(l:'a list) (f:'a->'b).
544 (MAP f l = [] <=> l = []) /\
545 ([] = MAP f l <=> l = [])
546Proof
547 LIST_INDUCT_TAC THEN REWRITE_TAC [MAP, NOT_CONS_NIL, NOT_NIL_CONS]
548QED
549
550Theorem MAP_EQ_CONS:
551 MAP (f:'a -> 'b) l = h::t <=> ?x0 t0. l = x0::t0 /\ h = f x0 /\ t = MAP f t0
552Proof
553 Q.ISPEC_THEN ‘l’ STRUCT_CASES_TAC list_CASES THEN SIMP_TAC (srw_ss()) [] THEN
554 METIS_TAC[]
555QED
556
557Theorem MAP_EQ_SING[simp]:
558 (MAP (f:'a -> 'b) l = [x]) <=> ?x0. (l = [x0]) /\ (x = f x0)
559Proof SIMP_TAC (srw_ss()) [MAP_EQ_CONS]
560QED
561
562Theorem MAP_EQ_f:
563 !f1 f2 l. MAP f1 l = MAP f2 l <=> !e. MEM e l ==> f1 e = f2 e
564Proof
565 Induct_on ‘l’ THEN
566 ASM_SIMP_TAC (srw_ss()) [DISJ_IMP_THM, MAP, CONS_11, FORALL_AND_THM]
567QED
568
569Theorem MAP_o:
570 !f:'b->'c. !g:'a->'b. MAP (f o g) = (MAP f) o (MAP g)
571Proof
572 REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV
573 THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [MAP, o_THM]
574QED
575
576Theorem MAP_MAP_o:
577 !(f:'b->'c) (g:'a->'b) l. MAP f (MAP g l) = MAP (f o g) l
578Proof
579 REPEAT GEN_TAC THEN REWRITE_TAC [MAP_o, o_DEF]
580 THEN BETA_TAC THEN REFL_TAC
581QED
582
583(* Theorem alias *)
584Theorem MAP_COMPOSE = MAP_MAP_o;
585(* val MAP_COMPOSE = |- !f g l. MAP f (MAP g l) = MAP (f o g) l: thm *)
586
587Theorem EL_MAP:
588 !n l. n < (LENGTH l) ==> !f:'a->'b. EL n (MAP f l) = f (EL n l)
589Proof
590 INDUCT_TAC THEN LIST_INDUCT_TAC
591 THEN ASM_REWRITE_TAC[LENGTH, EL, MAP, LESS_MONO_EQ, NOT_LESS_0, HD, TL]
592QED
593
594Theorem EL_APPEND_EQN:
595 !l1 l2 n.
596 EL n (l1 ++ l2) =
597 if n < LENGTH l1 then EL n l1 else EL (n - LENGTH l1) l2
598Proof
599 LIST_INDUCT_TAC >> simp_tac (srw_ss()) [] >> Cases_on ‘n’ >>
600 asm_simp_tac (srw_ss()) [EL]
601QED
602
603Theorem MAP_TL:
604 !l f. MAP f (TL l) = TL (MAP f l)
605Proof
606 Induct THEN REWRITE_TAC [TL_DEF, MAP]
607QED
608
609Theorem MEM_TL:
610 !l x. MEM x (TL l) ==> MEM x l
611Proof
612 Induct \\ simp [TL]
613QED
614
615Theorem EVERY_EL:
616 !(l:'a list) P. EVERY P l = !n. n < LENGTH l ==> P (EL n l)
617Proof
618 LIST_INDUCT_TAC THEN
619 ASM_REWRITE_TAC [EVERY_DEF, LENGTH, NOT_LESS_0] THEN
620 REPEAT STRIP_TAC THEN EQ_TAC THENL
621 [STRIP_TAC THEN INDUCT_TAC THENL
622 [ASM_REWRITE_TAC [EL, HD],
623 ASM_REWRITE_TAC [LESS_MONO_EQ, EL, TL]],
624 REPEAT STRIP_TAC THENL
625 [POP_ASSUM (MP_TAC o (SPEC (“0”))) THEN
626 REWRITE_TAC [LESS_0, EL, HD],
627 POP_ASSUM ((ANTE_RES_THEN ASSUME_TAC) o (MATCH_MP LESS_MONO)) THEN
628 POP_ASSUM MP_TAC THEN REWRITE_TAC [EL, TL]]]
629QED
630
631Theorem EVERY_CONJ:
632 !P Q l. EVERY (\(x:'a). (P x) /\ (Q x)) l = (EVERY P l /\ EVERY Q l)
633Proof
634 NTAC 2 GEN_TAC THEN LIST_INDUCT_TAC THEN
635 ASM_REWRITE_TAC [EVERY_DEF] THEN
636 CONV_TAC (DEPTH_CONV BETA_CONV) THEN
637 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN
638 FIRST_ASSUM ACCEPT_TAC
639QED
640
641Theorem EVERY_MEM:
642 !P l:'a list. EVERY P l = !e. MEM e l ==> P e
643Proof
644 GEN_TAC THEN LIST_INDUCT_TAC THEN
645 ASM_REWRITE_TAC [EVERY_DEF, LIST_TO_SET, IN_INSERT, NOT_IN_EMPTY] THEN
646 mesonLib.MESON_TAC []
647QED
648
649Theorem EVERY_MAP:
650 !P f l:'a list. EVERY P (MAP f l) = EVERY (\x. P (f x)) l
651Proof
652 NTAC 2 GEN_TAC THEN LIST_INDUCT_TAC THEN
653 ASM_REWRITE_TAC [EVERY_DEF, MAP] THEN BETA_TAC THEN REWRITE_TAC []
654QED
655
656Theorem EVERY_SIMP:
657 !c l:'a list. EVERY (\x. c) l <=> l = [] \/ c
658Proof
659 GEN_TAC THEN LIST_INDUCT_TAC THEN
660 ASM_REWRITE_TAC [EVERY_DEF, NOT_CONS_NIL] THEN
661 EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC []
662QED
663
664Theorem MONO_EVERY[mono]:
665 (!x. P x ==> Q x) ==> (EVERY P l ==> EVERY Q l)
666Proof
667 Q.ID_SPEC_TAC ‘l’ THEN LIST_INDUCT_TAC THEN
668 ASM_SIMP_TAC (srw_ss()) []
669QED
670
671Theorem EXISTS_MEM:
672 !P l:'a list. EXISTS P l = ?e. MEM e l /\ P e
673Proof
674 Induct_on ‘l’ THEN SRW_TAC [] [] THEN MESON_TAC[]
675QED
676
677Theorem EXISTS_MAP:
678 !P f l:'a list. EXISTS P (MAP f l) = EXISTS (\x. P (f x)) l
679Proof
680 NTAC 2 GEN_TAC THEN LIST_INDUCT_TAC THEN
681 ASM_REWRITE_TAC [EXISTS_DEF, MAP] THEN BETA_TAC THEN REWRITE_TAC []
682QED
683
684Theorem LIST_EXISTS_SIMP[simp]:
685 !c l:'a list. EXISTS (\x. c) l <=> l <> [] /\ c
686Proof
687 GEN_TAC THEN LIST_INDUCT_TAC THEN
688 ASM_REWRITE_TAC [EXISTS_DEF, NOT_CONS_NIL] THEN
689 EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC []
690QED
691
692Theorem LIST_EXISTS_MONO[mono]:
693 (!x. P x ==> Q x) ==> (EXISTS P l ==> EXISTS Q l)
694Proof
695 Q.ID_SPEC_TAC ‘l’ THEN LIST_INDUCT_TAC THEN
696 ASM_SIMP_TAC (srw_ss()) [DISJ_IMP_THM]
697QED
698
699Theorem EVERY_NOT_EXISTS:
700 !P l. EVERY P l = ~EXISTS (\x. ~P x) l
701Proof
702 GEN_TAC THEN LIST_INDUCT_TAC THEN
703 ASM_REWRITE_TAC [EVERY_DEF, EXISTS_DEF] THEN BETA_TAC THEN
704 REWRITE_TAC [DE_MORGAN_THM]
705QED
706
707Theorem EXISTS_NOT_EVERY:
708 !P l. EXISTS P l = ~EVERY (\x. ~P x) l
709Proof
710 REWRITE_TAC [EVERY_NOT_EXISTS] THEN BETA_TAC THEN REWRITE_TAC [] THEN
711 CONV_TAC (DEPTH_CONV ETA_CONV) THEN REWRITE_TAC []
712QED
713
714Theorem MEM_APPEND[simp]:
715 !e l1 l2. MEM e (APPEND l1 l2) <=> MEM e l1 \/ MEM e l2
716Proof
717 Induct_on ‘l1’ THEN SRW_TAC [] [DISJ_ASSOC]
718QED
719
720Theorem MEM_FILTER:
721 !P L x. MEM x (FILTER P L) <=> P x /\ MEM x L
722Proof Induct_on ‘L’ THEN SRW_TAC [] [] THEN PROVE_TAC[]
723QED
724
725Theorem MEM_FLAT:
726 !x L. MEM x (FLAT L) = (?l. MEM l L /\ MEM x l)
727Proof
728 Induct_on ‘L’ THEN SRW_TAC [] [FLAT] THEN PROVE_TAC[]
729QED
730
731Theorem FLAT_APPEND[simp]:
732 !l1 l2. FLAT (APPEND l1 l2) = APPEND (FLAT l1) (FLAT l2)
733Proof
734 LIST_INDUCT_TAC
735 THEN REWRITE_TAC [APPEND, FLAT]
736 THEN ASM_REWRITE_TAC [APPEND_ASSOC]
737QED
738
739Theorem FLAT_compute:
740 (FLAT [] = []) /\
741 (FLAT ([]::t) = FLAT t) /\
742 (FLAT ((h::t1)::t2) = h::FLAT (t1::t2))
743Proof
744 SIMP_TAC (srw_ss()) []
745QED
746
747Theorem EVERY_FLAT:
748 EVERY P (FLAT ls) <=> EVERY (EVERY P) ls
749Proof rw[EVERY_MEM,MEM_FLAT,PULL_EXISTS] >> metis_tac[]
750QED
751
752Theorem EVERY_APPEND:
753 !P (l1:'a list) l2.
754 EVERY P (APPEND l1 l2) <=> EVERY P l1 /\ EVERY P l2
755Proof
756 GEN_TAC THEN LIST_INDUCT_TAC THEN
757 ASM_REWRITE_TAC [APPEND, EVERY_DEF, CONJ_ASSOC]
758QED
759
760Theorem EXISTS_APPEND:
761 !P (l1:'a list) l2.
762 EXISTS P (APPEND l1 l2) <=> EXISTS P l1 \/ EXISTS P l2
763Proof
764 GEN_TAC THEN LIST_INDUCT_TAC THEN
765 ASM_REWRITE_TAC [APPEND, EXISTS_DEF, DISJ_ASSOC]
766QED
767
768Theorem NOT_EVERY:
769 !P l. ~EVERY P l = EXISTS ($~ o P) l
770Proof
771 GEN_TAC THEN LIST_INDUCT_TAC THEN
772 ASM_REWRITE_TAC [EVERY_DEF, EXISTS_DEF, DE_MORGAN_THM,
773 o_THM]
774QED
775
776Theorem NOT_EXISTS:
777 !P l. ~EXISTS P l = EVERY ($~ o P) l
778Proof
779 GEN_TAC THEN LIST_INDUCT_TAC THEN
780 ASM_REWRITE_TAC [EVERY_DEF, EXISTS_DEF, DE_MORGAN_THM,
781 o_THM]
782QED
783
784Theorem MEM_MAP:
785 !(l:'a list) (f:'a -> 'b) x.
786 MEM x (MAP f l) = ?y. (x = f y) /\ MEM y l
787Proof
788 LIST_INDUCT_TAC THEN SRW_TAC [] [MAP] THEN PROVE_TAC[]
789QED
790
791Theorem MEM_MAP_f:
792 !f l a. MEM a l ==> MEM (f a) (MAP f l)
793Proof
794 PROVE_TAC[MEM_MAP]
795QED
796
797Theorem LENGTH_NIL[simp]:
798 !l:'a list. (LENGTH l = 0) = (l = [])
799Proof
800 LIST_INDUCT_TAC THEN
801 REWRITE_TAC [LENGTH, NOT_SUC, NOT_CONS_NIL]
802QED
803
804(* Note: There is LENGTH_NIL, but no LENGTH_NON_NIL *)
805
806(* Theorem: 0 < LENGTH l <=> l <> [] *)
807(* Proof:
808 Since (LENGTH l = 0) <=> (l = []) by LENGTH_NIL
809 l <> [] <=> LENGTH l <> 0,
810 or 0 < LENGTH l by NOT_ZERO_LT_ZERO
811*)
812Theorem LENGTH_NON_NIL:
813 !l. 0 < LENGTH l <=> l <> []
814Proof
815 metis_tac[LENGTH_NIL, NOT_ZERO_LT_ZERO]
816QED
817
818(* val LENGTH_EQ_0 = save_thm("LENGTH_EQ_0", LENGTH_EQ_NUM |> CONJUNCT1); *)
819Theorem LENGTH_EQ_0 = LENGTH_NIL;
820(* > val LENGTH_EQ_0 = |- !l. (LENGTH l = 0) <=> (l = []): thm *)
821
822Theorem LENGTH1 :
823 (1 = LENGTH l) <=> ?e. l = [e]
824Proof
825 Cases_on `l` >> srw_tac [][LENGTH_NIL]
826QED
827
828(* Theorem: (LENGTH l = 1) <=> ?x. l = [x] *)
829(* Proof:
830 If part: (LENGTH l = 1) ==> ?x. l = [x]
831 Since LENGTH l <> 0, l <> [] by LENGTH_NIL
832 or ?h t. l = h::t by list_CASES
833 and LENGTH t = 0 by LENGTH
834 so t = [] by LENGTH_NIL
835 Hence l = [x]
836 Only-if part: (l = [x]) ==> (LENGTH l = 1)
837 True by LENGTH.
838*)
839Theorem LENGTH_EQ_1:
840 !l. (LENGTH l = 1) <=> ?x. l = [x]
841Proof
842 rw [GSYM LENGTH1]
843(*rw[EQ_IMP_THM] >| [
844 `LENGTH l <> 0` by decide_tac >>
845 `?h t. l = h::t` by metis_tac[LENGTH_NIL, list_CASES] >>
846 `SUC (LENGTH t) = 1` by metis_tac[LENGTH] >>
847 `LENGTH t = 0` by decide_tac >>
848 metis_tac[LENGTH_NIL],
849 rw[]
850 ]*)
851QED
852
853Theorem LENGTH2 :
854 (2 = LENGTH l) <=> ?a b. l = [a;b]
855Proof
856 Cases_on `l` >> srw_tac [][LENGTH1]
857QED
858
859Theorem LENGTH_NIL_SYM[simp]:
860 (0 = LENGTH l) = (l = [])
861Proof
862 PROVE_TAC[LENGTH_NIL]
863QED
864
865Theorem SING_HD[simp]:
866 (([HD xs] = xs) <=> (LENGTH xs = 1)) /\
867 ((xs = [HD xs]) <=> (LENGTH xs = 1))
868Proof
869 Cases_on ‘xs’ >> full_simp_tac(srw_ss())[LENGTH_NIL] >> metis_tac []
870QED
871
872Theorem NULL_EQ:
873 !l. NULL l = (l = [])
874Proof
875 Cases_on ‘l’ THEN REWRITE_TAC[NULL, NOT_CONS_NIL]
876QED
877
878Theorem NULL_LENGTH:
879 !l. NULL l = (LENGTH l = 0)
880Proof
881 REWRITE_TAC[NULL_EQ, LENGTH_NIL]
882QED
883
884Theorem NULL_MAP[simp]:
885 NULL (MAP f ls) = NULL ls
886Proof
887 rw[NULL_EQ]
888QED
889
890Theorem LENGTH_CONS:
891 !l n. (LENGTH l = SUC n) =
892 ?h:'a. ?l'. (LENGTH l' = n) /\ (l = CONS h l')
893Proof
894 LIST_INDUCT_TAC THENL [
895 REWRITE_TAC [LENGTH, NOT_EQ_SYM(SPEC_ALL NOT_SUC), NOT_NIL_CONS],
896 REWRITE_TAC [LENGTH, INV_SUC_EQ, CONS_11] THEN
897 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN
898 simpLib.ASM_SIMP_TAC boolSimps.bool_ss []
899 ]
900QED
901
902Theorem LENGTH_EQ_CONS:
903 !P:'a list->bool.
904 !n:num.
905 (!l. (LENGTH l = SUC n) ==> P l) =
906 (!l. (LENGTH l = n) ==> (\l. !x:'a. P (CONS x l)) l)
907Proof
908 CONV_TAC (ONCE_DEPTH_CONV BETA_CONV) THEN
909 REPEAT GEN_TAC THEN EQ_TAC THENL
910 [REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
911 ASM_REWRITE_TAC [LENGTH],
912 DISCH_TAC THEN
913 INDUCT_THEN list_INDUCT STRIP_ASSUME_TAC THENL
914 [REWRITE_TAC [LENGTH, NOT_NIL_CONS, NOT_EQ_SYM(SPEC_ALL NOT_SUC)],
915 ASM_REWRITE_TAC [LENGTH, INV_SUC_EQ, CONS_11] THEN
916 REPEAT STRIP_TAC THEN RES_THEN MATCH_ACCEPT_TAC]]
917QED
918
919Theorem LENGTH_EQ_SUM:
920 !l:'a list n1 n2.
921 LENGTH l = n1+n2 <=>
922 ?l1 l2. LENGTH l1 = n1 /\ LENGTH l2 = n2 /\ l = l1++l2
923Proof
924 Induct_on ‘n1’ THEN1 (
925 SIMP_TAC arith_ss [LENGTH_NIL, APPEND]
926 ) THEN
927 ASM_SIMP_TAC arith_ss [arithmeticTheory.ADD_CLAUSES, LENGTH_CONS,
928 GSYM RIGHT_EXISTS_AND_THM, GSYM LEFT_EXISTS_AND_THM, APPEND] THEN
929 PROVE_TAC[]
930QED
931
932Theorem LENGTH_EQ_NUM:
933 (!l:'a list. LENGTH l = 0 <=> l = []) /\
934 (!l:'a list n.
935 LENGTH l = SUC n <=> ?h l'. LENGTH l' = n /\ l = h::l') /\
936 (!l:'a list n1 n2.
937 LENGTH l = n1+n2 <=>
938 ?l1 l2. LENGTH l1 = n1 /\ LENGTH l2 = n2 /\ l = l1++l2)
939Proof
940 SIMP_TAC arith_ss [LENGTH_NIL, LENGTH_CONS, LENGTH_EQ_SUM]
941QED
942
943Theorem LENGTH_EQ_NUM_compute =
944 CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV LENGTH_EQ_NUM;
945
946
947Theorem LENGTH_EQ_NIL:
948 !P: 'a list->bool.
949 (!l. (LENGTH l = 0) ==> P l) = P []
950Proof
951 REPEAT GEN_TAC THEN EQ_TAC THENL
952 [REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
953 REWRITE_TAC [LENGTH],
954 DISCH_TAC THEN
955 INDUCT_THEN list_INDUCT STRIP_ASSUME_TAC THENL
956 [ASM_REWRITE_TAC [], ASM_REWRITE_TAC [LENGTH, NOT_SUC]]]
957QED
958
959Theorem CONS_ACYCLIC:
960!l x. ~(l = x::l) /\ ~(x::l = l)
961Proof
962 LIST_INDUCT_TAC
963 THEN ASM_REWRITE_TAC[CONS_11, NOT_NIL_CONS, NOT_CONS_NIL, LENGTH_NIL]
964QED
965
966Theorem APPEND_eq_NIL[simp]:
967 (!l1 l2:'a list. ([] = APPEND l1 l2) <=> (l1=[]) /\ (l2=[])) /\
968 (!l1 l2:'a list. (APPEND l1 l2 = []) <=> (l1=[]) /\ (l2=[]))
969Proof
970 CONJ_TAC THEN
971 INDUCT_THEN list_INDUCT STRIP_ASSUME_TAC
972 THEN REWRITE_TAC [CONS_11, NOT_NIL_CONS, NOT_CONS_NIL, APPEND]
973 THEN GEN_TAC THEN MATCH_ACCEPT_TAC EQ_SYM_EQ
974QED
975
976Theorem NULL_APPEND[simp]:
977 NULL (l1 ++ l2) <=> NULL l1 /\ NULL l2
978Proof simp[NULL_LENGTH]
979QED
980
981Theorem MAP_EQ_APPEND:
982 MAP (f:'a -> 'b) l = l1 ++ l2 <=>
983 ?l10 l20. l = l10 ++ l20 /\ l1 = MAP f l10 /\ l2 = MAP f l20
984Proof
985 REVERSE EQ_TAC THEN1 SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [MAP_APPEND] THEN
986 MAP_EVERY Q.ID_SPEC_TAC [‘l1’, ‘l2’, ‘l’] THEN LIST_INDUCT_TAC THEN
987 SIMP_TAC (srw_ss()) [] THEN MAP_EVERY Q.X_GEN_TAC [‘h’, ‘l2’, ‘l1’] THEN
988 Cases_on ‘l1’ THEN SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [MAP_EQ_CONS] THEN
989 METIS_TAC[]
990QED
991
992Theorem APPEND_EQ_SING:
993 (l1 ++ l2 = [e:'a]) <=>
994 (l1 = [e]) /\ (l2 = []) \/ (l1 = []) /\ (l2 = [e])
995Proof
996 Cases_on ‘l1’ THEN SRW_TAC [] [CONJ_ASSOC]
997QED
998
999Theorem APPEND_11:
1000 (!l1 l2 l3:'a list. (APPEND l1 l2 = APPEND l1 l3) = (l2 = l3)) /\
1001 (!l1 l2 l3:'a list. (APPEND l2 l1 = APPEND l3 l1) = (l2 = l3))
1002Proof
1003 CONJ_TAC THEN LIST_INDUCT_TAC THEN
1004 ASM_REWRITE_TAC [APPEND, CONS_11, APPEND_NIL] THEN
1005 Q.SUBGOAL_THEN
1006 ‘!h l1 l2:'a list. APPEND l1 (h::l2) = APPEND (APPEND l1 [h]) l2’
1007 (ONCE_REWRITE_TAC o C cons [])
1008 THENL [
1009 GEN_TAC THEN POP_ASSUM (K ALL_TAC) THEN LIST_INDUCT_TAC THEN
1010 REWRITE_TAC [APPEND, CONS_11] THEN POP_ASSUM ACCEPT_TAC,
1011 ASM_REWRITE_TAC [] THEN GEN_TAC THEN POP_ASSUM (K ALL_TAC) THEN
1012 LIST_INDUCT_TAC THEN REWRITE_TAC [APPEND, CONS_11] THENL [
1013 LIST_INDUCT_TAC THEN
1014 REWRITE_TAC [APPEND, CONS_11, NOT_NIL_CONS, DE_MORGAN_THM,
1015 APPEND_eq_NIL, NOT_CONS_NIL],
1016 GEN_TAC THEN LIST_INDUCT_TAC THEN
1017 ASM_REWRITE_TAC [APPEND, CONS_11, APPEND_eq_NIL, NOT_CONS_NIL,
1018 NOT_NIL_CONS]
1019 ]
1020 ]
1021QED
1022
1023Theorem APPEND_LENGTH_EQ:
1024 !l1 l1'. (LENGTH l1 = LENGTH l1') ==>
1025 !l2 l2'. (LENGTH l2 = LENGTH l2') ==>
1026 ((l1 ++ l2 = l1' ++ l2') <=> (l1 = l1') /\ (l2 = l2'))
1027Proof
1028 Induct THEN1
1029 (GEN_TAC THEN STRIP_TAC THEN ‘l1' = []’ by METIS_TAC [LENGTH_NIL] THEN
1030 SRW_TAC [] []) THEN
1031 MAP_EVERY Q.X_GEN_TAC [‘h’,‘l1'’] THEN SRW_TAC [] [] THEN
1032 ‘?h' t'. l1' = h'::t'’ by METIS_TAC [LENGTH_CONS] THEN
1033 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []
1034QED
1035
1036Theorem APPEND_11_LENGTH =
1037 SIMP_RULE bool_ss [DISJ_IMP_THM, FORALL_AND_THM] (prove (
1038 (“!l1 l2 l1' l2'.
1039 ((LENGTH l1 = LENGTH l1') \/ (LENGTH l2 = LENGTH l2')) ==>
1040 (((l1 ++ l2) = (l1' ++ l2')) = ((l1 = l1') /\ (l2 = l2')))”),
1041 REPEAT GEN_TAC
1042 THEN Tactical.REVERSE
1043 (Cases_on ‘(LENGTH l1 = LENGTH l1') /\ (LENGTH l2 = LENGTH l2')’) THEN1
1044(
1045 DISCH_TAC
1046 THEN ‘~((l1 = l1') /\ (l2 = l2'))’ by PROVE_TAC[]
1047 THEN ASM_REWRITE_TAC[]
1048 THEN ‘~(LENGTH (l1 ++ l2) = LENGTH (l1' ++ l2'))’
1049 suffices_by PROVE_TAC[]
1050 THEN FULL_SIMP_TAC arith_ss [LENGTH_APPEND]
1051 ) THEN PROVE_TAC[APPEND_LENGTH_EQ]));
1052
1053
1054Theorem APPEND_EQ_SELF:
1055 (!l1 l2:'a list. ((l1 ++ l2 = l1) = (l2 = []))) /\
1056 (!l1 l2:'a list. ((l1 ++ l2 = l2) = (l1 = []))) /\
1057 (!l1 l2:'a list. ((l1 = l1 ++ l2) = (l2 = []))) /\
1058 (!l1 l2:'a list. ((l2 = l1 ++ l2) = (l1 = [])))
1059Proof
1060PROVE_TAC[APPEND_11, APPEND_NIL, APPEND]
1061QED
1062
1063Theorem mapPartial_EQ_CONS:
1064 !f xs y ys.
1065 mapPartial f xs = y::ys <=>
1066 ?p x s. xs = p ++ [x] ++ s /\ (!x0. MEM x0 p ==> f x0 = NONE) /\
1067 f x = SOME y /\ mapPartial f s = ys
1068Proof
1069 gen_tac >> Induct >> simp[APPEND_eq_NIL] >> rpt gen_tac >>
1070 Q.RENAME_TAC [‘option_CASE (f x)’] >> Cases_on ‘f x’ >> simp[]
1071 >- (rw[EQ_IMP_THM]
1072 >- (REWRITE_TAC [GSYM $ cj 2 APPEND] >>
1073 rpt $ irule_at Any EQ_REFL >> simp[DISJ_IMP_THM]) >>
1074 Q.RENAME_TAC [‘x::xs = p ++ [e] ++ s’] >> Cases_on ‘p’ >> fs[] >>
1075 rw[] >> metis_tac[]) >>
1076 iff_tac
1077 >- (rw[] >> Q.EXISTS_TAC ‘[]’ >> simp[])
1078 >- (strip_tac >> Q.RENAME_TAC [‘x::xs = p ++ [e] ++ s’] >>
1079 Cases_on ‘p’ >> fs[])
1080QED
1081
1082(* tfl_termsolve: useful for proving termination in fold and rose-tree settings *)
1083Theorem MEM_SPLIT[tfl_termsolve]:
1084 !x l. (MEM x l) = ?l1 l2. (l = l1 ++ x::l2)
1085Proof
1086 Induct_on ‘l’ THEN SRW_TAC [] [] THEN EQ_TAC THENL [
1087 SRW_TAC [][] THEN1 (MAP_EVERY Q.EXISTS_TAC [‘[]’,‘l’] THEN SRW_TAC [][]) THEN
1088 MAP_EVERY Q.EXISTS_TAC [‘a::l1’, ‘l2’] THEN SRW_TAC [] [],
1089 DISCH_THEN (Q.X_CHOOSE_THEN ‘l1’ (Q.X_CHOOSE_THEN ‘l2’ ASSUME_TAC)) THEN
1090 Cases_on ‘l1’ THEN FULL_SIMP_TAC(srw_ss()) [] THEN PROVE_TAC[]
1091 ]
1092QED
1093
1094Theorem LIST_EQ_REWRITE:
1095 !l1 l2. (l1 = l2) =
1096 ((LENGTH l1 = LENGTH l2) /\
1097 ((!x. (x < LENGTH l1) ==> (EL x l1 = EL x l2))))
1098Proof
1099
1100 LIST_INDUCT_TAC THEN Cases_on ‘l2’ THEN (
1101 ASM_SIMP_TAC arith_ss [LENGTH, NOT_CONS_NIL, CONS_11, EL]
1102 ) THEN
1103 GEN_TAC THEN EQ_TAC THEN SIMP_TAC arith_ss [] THENL [
1104 REPEAT STRIP_TAC THEN Cases_on ‘x’ THEN (
1105 ASM_SIMP_TAC arith_ss [EL, HD, TL]
1106 ),
1107 REPEAT STRIP_TAC THENL [
1108 POP_ASSUM (MP_TAC o SPEC “0:num”) THEN
1109 ASM_SIMP_TAC arith_ss [EL, HD, TL],
1110 Q.PAT_X_ASSUM ‘!x. x < Y ==> P x’ (MP_TAC o SPEC “SUC x”) THEN
1111 ASM_SIMP_TAC arith_ss [EL, HD, TL]
1112 ]
1113 ]
1114QED
1115
1116Theorem LIST_EQ =
1117 GENL[“l1:'a list”, “l2:'a list”]
1118 (snd(EQ_IMP_RULE (SPEC_ALL LIST_EQ_REWRITE)));
1119
1120Theorem FOLDL_EQ_FOLDR:
1121 !f l e. (ASSOC f /\ COMM f) ==>
1122 ((FOLDL f e l) = (FOLDR f e l))
1123Proof
1124GEN_TAC THEN
1125FULL_SIMP_TAC bool_ss [RIGHT_FORALL_IMP_THM, COMM_DEF,
1126 ASSOC_DEF] THEN
1127STRIP_TAC THEN LIST_INDUCT_TAC THENL [
1128 SIMP_TAC bool_ss [FOLDR, FOLDL],
1129
1130 ASM_SIMP_TAC bool_ss [FOLDR, FOLDL] THEN
1131 POP_ASSUM (K ALL_TAC) THEN
1132 Q.SPEC_TAC (‘l’, ‘l’) THEN
1133 LIST_INDUCT_TAC THEN ASM_SIMP_TAC bool_ss [FOLDR]
1134]
1135QED
1136
1137Theorem FOLDR_CONS:
1138 !f ls a. FOLDR (\x y. f x :: y) a ls = (MAP f ls)++a
1139Proof
1140GEN_TAC THEN Induct THEN SRW_TAC[] [FOLDR, MAP]
1141QED
1142
1143Theorem LENGTH_TL[simp]:
1144 !l. LENGTH (TL l) = LENGTH l - 1
1145Proof
1146 Cases_on ‘l’ THEN SIMP_TAC arith_ss [LENGTH, TL_DEF]
1147QED
1148
1149Theorem LENGTH_TL_LE:
1150 !ls. LENGTH (TL ls) <= LENGTH ls
1151Proof
1152 Cases \\ rw[]
1153QED
1154
1155Theorem FILTER_EQ_NIL:
1156 !P l. (FILTER P l = []) = (EVERY (\x. ~(P x)) l)
1157Proof
1158 GEN_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC THEN (
1159 ASM_SIMP_TAC bool_ss [FILTER, EVERY_DEF, COND_RATOR, COND_RAND,
1160 NOT_CONS_NIL]
1161 )
1162QED
1163
1164Theorem FILTER_NEQ_NIL:
1165 !P l. ~(FILTER P l = []) = ?x. MEM x l /\ P x
1166Proof
1167 SIMP_TAC bool_ss [FILTER_EQ_NIL, EVERY_NOT_EXISTS, EXISTS_MEM]
1168QED
1169
1170Theorem FILTER_EQ_ID:
1171 !P l. (FILTER P l = l) = (EVERY P l)
1172Proof
1173 Induct_on ‘l’ THEN SRW_TAC [] [] THEN
1174 DISCH_THEN (ASSUME_TAC o Q.AP_TERM ‘MEM a’) THEN
1175 FULL_SIMP_TAC (srw_ss()) [MEM_FILTER]
1176QED
1177
1178Theorem FILTER_NEQ_ID:
1179 !P l. ~(FILTER P l = l) = ?x. MEM x l /\ ~(P x)
1180Proof
1181 SIMP_TAC bool_ss [FILTER_EQ_ID, EVERY_NOT_EXISTS, EXISTS_MEM]
1182QED
1183
1184Theorem FILTER_EQ_CONS:
1185 !P l h lr.
1186 FILTER P l = h::lr <=>
1187 ?l1 l2. l = l1++[h]++l2 /\ FILTER P l1 = [] /\ FILTER P l2 = lr /\ P h
1188Proof
1189 GEN_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC THEN
1190 ASM_SIMP_TAC bool_ss [FILTER, NOT_CONS_NIL, APPEND_eq_NIL] THEN
1191 REPEAT STRIP_TAC THEN Cases_on ‘P h’ THEN ASM_REWRITE_TAC[] THEN
1192 EQ_TAC THEN REPEAT STRIP_TAC THENL [
1193 Q.EXISTS_TAC ‘[]’ THEN Q.EXISTS_TAC ‘l’ THEN
1194 FULL_SIMP_TAC bool_ss [CONS_11, APPEND, FILTER],
1195
1196 Cases_on ‘l1’ THEN
1197 FULL_SIMP_TAC bool_ss
1198 [APPEND, CONS_11, FILTER, COND_RAND, COND_RATOR, NOT_CONS_NIL],
1199
1200 Q.EXISTS_TAC ‘h::l1’ THEN Q.EXISTS_TAC ‘l2’ THEN
1201 ASM_SIMP_TAC bool_ss [CONS_11, APPEND, FILTER],
1202
1203 Cases_on ‘l1’ THENL [
1204 FULL_SIMP_TAC bool_ss [APPEND, CONS_11],
1205 Q.EXISTS_TAC ‘l'’ THEN Q.EXISTS_TAC ‘l2’ THEN
1206 FULL_SIMP_TAC bool_ss [CONS_11, APPEND, FILTER, COND_RATOR,
1207 COND_RAND, NOT_CONS_NIL]
1208 ]
1209 ]
1210QED
1211
1212Theorem FILTER_F[simp]:
1213 !xs. FILTER (\x. F) xs = []
1214Proof Induct >> simp[]
1215QED
1216
1217Theorem FILTER_T[simp]:
1218 !xs. FILTER (\x. T) xs = xs
1219Proof Induct >> simp[]
1220QED
1221
1222Theorem FILTER_APPEND_DISTRIB:
1223 !P L M. FILTER P (APPEND L M) = APPEND (FILTER P L) (FILTER P M)
1224Proof
1225 GEN_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC
1226 THEN RW_TAC bool_ss [FILTER, APPEND]
1227QED
1228
1229Theorem MEM[simp]:
1230 (!x:'a. MEM x [] <=> F) /\ (!x:'a h t. MEM x (h::t) <=> x = h \/ MEM x t)
1231Proof SRW_TAC [] []
1232QED
1233
1234Theorem FILTER_EQ_APPEND:
1235 !P l l1 l2.
1236 (FILTER P l = l1 ++ l2) =
1237 (?l3 l4. (l = l3++l4) /\ (FILTER P l3 = l1) /\ (FILTER P l4 = l2))
1238Proof
1239GEN_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC THEN1 (
1240 ASM_SIMP_TAC bool_ss [FILTER, APPEND_eq_NIL] THEN PROVE_TAC[]
1241) THEN
1242REPEAT STRIP_TAC THEN Cases_on ‘P h’ THEN
1243ASM_SIMP_TAC bool_ss [FILTER] THENL [
1244 Cases_on ‘l1’ THENL [
1245 Cases_on ‘l2’ THENL [
1246 SIMP_TAC bool_ss [APPEND, NOT_CONS_NIL, FILTER_EQ_NIL, EVERY_MEM] THEN
1247 PROVE_TAC[MEM_APPEND, MEM],
1248
1249 ASM_SIMP_TAC bool_ss [APPEND, CONS_11] THEN
1250 EQ_TAC THEN STRIP_TAC THENL [
1251 Q.EXISTS_TAC ‘[]’ THEN Q.EXISTS_TAC ‘h::l’ THEN
1252 FULL_SIMP_TAC bool_ss [APPEND, FILTER],
1253
1254 Tactical.REVERSE (Cases_on ‘l3’) THEN1 (
1255 FULL_SIMP_TAC bool_ss [CONS_11, FILTER, APPEND,
1256 COND_RAND, COND_RATOR, NOT_CONS_NIL]
1257 ) THEN
1258 Cases_on ‘l4’ THEN (
1259 FULL_SIMP_TAC bool_ss [FILTER, NOT_CONS_NIL, APPEND,
1260 COND_RATOR, COND_RAND, CONS_11] THEN
1261 PROVE_TAC[]
1262 )
1263 ]
1264 ],
1265
1266 ASM_SIMP_TAC bool_ss [APPEND, CONS_11] THEN
1267 EQ_TAC THEN STRIP_TAC THENL [
1268 Q.EXISTS_TAC ‘h::l3’ THEN Q.EXISTS_TAC ‘l4’ THEN
1269 FULL_SIMP_TAC bool_ss [APPEND, FILTER],
1270
1271 Cases_on ‘l3’ THEN (
1272 FULL_SIMP_TAC bool_ss [APPEND, FILTER, NOT_CONS_NIL, FILTER, CONS_11,
1273 COND_RAND, COND_RATOR] THEN
1274 PROVE_TAC[]
1275 )
1276 ]
1277 ],
1278
1279 EQ_TAC THEN STRIP_TAC THENL [
1280 Q.EXISTS_TAC ‘h::l3’ THEN Q.EXISTS_TAC ‘l4’ THEN
1281 ASM_SIMP_TAC bool_ss [APPEND, FILTER],
1282
1283 Cases_on ‘l3’ THENL [
1284 Cases_on ‘l4’ THEN
1285 FULL_SIMP_TAC bool_ss [APPEND, NOT_CONS_NIL, CONS_11] THEN
1286 Q.EXISTS_TAC ‘[]’ THEN Q.EXISTS_TAC ‘l’ THEN
1287 FULL_SIMP_TAC bool_ss [FILTER, APPEND] THEN
1288 PROVE_TAC[],
1289
1290 Q.EXISTS_TAC ‘l'’ THEN Q.EXISTS_TAC ‘l4’ THEN
1291 FULL_SIMP_TAC bool_ss [FILTER, APPEND, CONS_11] THEN
1292 PROVE_TAC[]
1293 ]
1294 ]
1295]
1296QED
1297
1298Theorem EVERY_FILTER:
1299 !P1 P2 l. EVERY P1 (FILTER P2 l) =
1300 EVERY (\x. P2 x ==> P1 x) l
1301Proof
1302
1303GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN (
1304 ASM_SIMP_TAC bool_ss [FILTER, EVERY_DEF, COND_RATOR, COND_RAND]
1305)
1306QED
1307
1308Theorem EVERY_FILTER_IMP:
1309 !P1 P2 l. EVERY P1 l ==> EVERY P1 (FILTER P2 l)
1310Proof
1311GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN (
1312 ASM_SIMP_TAC bool_ss [FILTER, EVERY_DEF, COND_RATOR, COND_RAND]
1313)
1314QED
1315
1316Theorem FILTER_COND_REWRITE:
1317 (FILTER P [] = []) /\
1318 (!h. (P h) ==> ((FILTER P (h::l) = h::FILTER P l))) /\
1319 (!h. ~(P h) ==> (FILTER P (h::l) = FILTER P l))
1320Proof
1321SIMP_TAC bool_ss [FILTER]
1322QED
1323
1324Theorem NOT_NULL_MEM:
1325 !l. ~(NULL l) = (?e. MEM e l)
1326Proof
1327 Cases_on ‘l’ THEN SIMP_TAC bool_ss [EXISTS_OR_THM, MEM, NOT_CONS_NIL, NULL]
1328QED
1329
1330(* Computing EL when n is in numeral representation *)
1331Theorem EL_compute[allow_rebind]:
1332 !n. EL n l = if n=0 then HD l else EL (PRE n) (TL l)
1333Proof INDUCT_TAC THEN ASM_REWRITE_TAC [NOT_SUC, EL, PRE]
1334QED
1335
1336(* a version of the above that is safe to use in the simplifier *)
1337(* only bother with BIT1/2 cases because the zero case is already provided
1338 by the definition. *)
1339Theorem EL_simp:
1340 (EL (NUMERAL (BIT1 n)) l = EL (PRE (NUMERAL (BIT1 n))) (TL l)) /\
1341 (EL (NUMERAL (BIT2 n)) l = EL (NUMERAL (BIT1 n)) (TL l))
1342Proof
1343 REWRITE_TAC [arithmeticTheory.NUMERAL_DEF,
1344 arithmeticTheory.BIT1, arithmeticTheory.BIT2,
1345 arithmeticTheory.ADD_CLAUSES,
1346 prim_recTheory.PRE, EL]
1347QED
1348
1349Theorem EL_restricted[simp]:
1350 (EL 0 = HD) /\
1351 (EL (SUC n) (l::ls) = EL n ls)
1352Proof
1353 REWRITE_TAC [FUN_EQ_THM, EL, TL, HD]
1354QED
1355
1356Theorem EL_simp_restricted[simp]:
1357 (EL (NUMERAL (BIT1 n)) (l::ls) = EL (PRE (NUMERAL (BIT1 n))) ls) /\
1358 (EL (NUMERAL (BIT2 n)) (l::ls) = EL (NUMERAL (BIT1 n)) ls)
1359Proof
1360 REWRITE_TAC [EL_simp, TL]
1361QED
1362
1363Theorem SUM_eq_0:
1364 !ls. (SUM ls = 0) = !x. MEM x ls ==> (x = 0)
1365Proof
1366 LIST_INDUCT_TAC THEN SRW_TAC[] [SUM, MEM] THEN METIS_TAC[]
1367QED
1368
1369Theorem NULL_FILTER:
1370 !P ls. NULL (FILTER P ls) = !x. MEM x ls ==> ~P x
1371Proof
1372 GEN_TAC THEN LIST_INDUCT_TAC THEN
1373 SRW_TAC[] [NULL, FILTER, MEM] THEN METIS_TAC[]
1374QED
1375
1376
1377Theorem WF_LIST_PRED:
1378WF \L1 L2. ?h:'a. L2 = h::L1
1379Proof
1380REWRITE_TAC[relationTheory.WF_DEF] THEN BETA_TAC THEN GEN_TAC
1381 THEN CONV_TAC CONTRAPOS_CONV
1382 THEN Ho_Rewrite.REWRITE_TAC
1383 [NOT_FORALL_THM, NOT_EXISTS_THM, NOT_IMP, DE_MORGAN_THM]
1384 THEN REWRITE_TAC [GSYM IMP_DISJ_THM] THEN STRIP_TAC
1385 THEN LIST_INDUCT_TAC THENL [ALL_TAC, GEN_TAC]
1386 THEN STRIP_TAC THEN RES_TAC
1387 THEN RULE_ASSUM_TAC(REWRITE_RULE[NOT_NIL_CONS, CONS_11])
1388 THENL [FIRST_ASSUM ACCEPT_TAC,
1389 PAT_X_ASSUM (Term‘x /\ y’) (SUBST_ALL_TAC o CONJUNCT2) THEN RES_TAC]
1390QED
1391
1392(* ----------------------------------------------------------------------
1393 LIST_REL : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
1394
1395 Lifts a relation point-wise to two lists
1396 ---------------------------------------------------------------------- *)
1397
1398Inductive LIST_REL:
1399[~nil_rule:]
1400 LIST_REL R [] []
1401[~cons_I:]
1402 !h1 h2 t1 t2. R h1 h2 /\ LIST_REL R t1 t2 ==> LIST_REL R (h1::t1) (h2::t2)
1403End
1404
1405Theorem LIST_REL_EL_EQN:
1406 !R l1 l2. LIST_REL R l1 l2 <=>
1407 (LENGTH l1 = LENGTH l2) /\
1408 !n. n < LENGTH l1 ==> R (EL n l1) (EL n l2)
1409Proof
1410 GEN_TAC THEN SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN
1411 CONJ_TAC THENL [
1412 Induct_on ‘LIST_REL’ THEN SRW_TAC [] [] THEN
1413 Cases_on ‘n’ THEN FULL_SIMP_TAC (srw_ss()) [],
1414 Induct_on ‘l1’ THEN Cases_on ‘l2’ THEN SRW_TAC [] [LIST_REL_rules] THEN
1415 POP_ASSUM (fn th => Q.SPEC_THEN ‘0’ MP_TAC th THEN
1416 Q.SPEC_THEN ‘SUC m’ (MP_TAC o Q.GEN ‘m’) th) THEN
1417 SRW_TAC [] [LIST_REL_rules]
1418 ]
1419QED
1420
1421Theorem LIST_REL_def[simp,compute]:
1422 (LIST_REL R [] [] <=> T) /\
1423 (LIST_REL R (a::as) [] <=> F) /\
1424 (LIST_REL R [] (b::bs) <=> F) /\
1425 (LIST_REL R (a::as) (b::bs) <=> R a b /\ LIST_REL R as bs)
1426Proof REPEAT CONJ_TAC THEN SRW_TAC [] [Once LIST_REL_cases, SimpLHS]
1427QED
1428
1429Theorem LIST_REL_mono:
1430 (!x y. R1 x y ==> R2 x y) ==> LIST_REL R1 l1 l2 ==> LIST_REL R2 l1 l2
1431Proof
1432 SRW_TAC [] [LIST_REL_EL_EQN]
1433QED
1434val _ = IndDefLib.export_mono "LIST_REL_mono"
1435
1436Theorem LIST_REL_NIL[simp]:
1437 (LIST_REL R [] y <=> (y = [])) /\ (LIST_REL R x [] <=> (x = []))
1438Proof
1439 Cases_on ‘x’ THEN Cases_on ‘y’ THEN SRW_TAC [] []
1440QED
1441
1442Theorem LIST_REL_CONS1:
1443 LIST_REL R (h::t) xs <=> ?h' t'. (xs = h'::t') /\ R h h' /\ LIST_REL R t t'
1444Proof
1445 Cases_on ‘xs’ THEN SRW_TAC [] []
1446QED
1447
1448Theorem LIST_REL_CONS2:
1449 LIST_REL R xs (h::t) <=> ?h' t'. (xs = h'::t') /\ R h' h /\ LIST_REL R t' t
1450Proof
1451 Cases_on ‘xs’ THEN SRW_TAC [] []
1452QED
1453
1454Theorem LIST_REL_CONJ:
1455 LIST_REL (\a b. P a b /\ Q a b) l1 l2 <=>
1456 LIST_REL (\a b. P a b) l1 l2 /\ LIST_REL (\a b. Q a b) l1 l2
1457Proof
1458 SRW_TAC [] [LIST_REL_EL_EQN] THEN METIS_TAC []
1459QED
1460
1461Theorem LIST_REL_MAP1:
1462 LIST_REL R (MAP f l1) l2 <=> LIST_REL (R o f) l1 l2
1463Proof
1464 SRW_TAC [] [LIST_REL_EL_EQN, EL_MAP, LENGTH_MAP]
1465QED
1466
1467Theorem LIST_REL_MAP2:
1468 LIST_REL R l1 (MAP f l2) <=>
1469 LIST_REL (\a b. R a (f b)) l1 l2
1470Proof
1471 SRW_TAC [CONJ_ss] [LIST_REL_EL_EQN, EL_MAP, LENGTH_MAP]
1472QED
1473
1474Theorem LIST_REL_LENGTH:
1475 !x y. LIST_REL R x y ==> (LENGTH x = LENGTH y)
1476Proof
1477 Induct_on ‘LIST_REL’ THEN SRW_TAC [] [LENGTH]
1478QED
1479
1480Theorem LIST_REL_SPLIT1:
1481 !xs1 zs.
1482 LIST_REL P (xs1 ++ xs2) zs <=>
1483 ?ys1 ys2. (zs = ys1 ++ ys2) /\ LIST_REL P xs1 ys1 /\ LIST_REL P xs2 ys2
1484Proof
1485 Induct >> fs[APPEND] >> Cases_on ‘zs’ >> fs[] >> rpt strip_tac >>
1486 simp[LIST_REL_CONS1, PULL_EXISTS] >> metis_tac[]
1487QED
1488
1489Theorem LIST_REL_SPLIT2:
1490 !xs1 zs.
1491 LIST_REL P zs (xs1 ++ xs2) <=>
1492 ?ys1 ys2. (zs = ys1 ++ ys2) /\ LIST_REL P ys1 xs1 /\ LIST_REL P ys2 xs2
1493Proof
1494 Induct >> fs[APPEND] >> Cases_on ‘zs’ >> fs[] >> rpt strip_tac >>
1495 simp[LIST_REL_CONS2, PULL_EXISTS] >> metis_tac[]
1496QED
1497
1498(* example of LIST_REL in action :
1499val (rules,ind,cases) = IndDefLib.Hol_reln`
1500 (!n m. n < m ==> R n m) /\
1501 (!n m. R n m ==> R1 (INL n) (INL m)) /\
1502 (!l1 l2. LIST_REL R l1 l2 ==> R1 (INR l1) (INR l2))
1503`
1504val strong = IndDefLib.derive_strong_induction (rules,ind)
1505*)
1506
1507Theorem LIST_REL_equivalence :
1508 !R. equivalence R ==> equivalence (LIST_REL R)
1509Proof
1510 SRW_TAC [] [equivalence_def, reflexive_def, symmetric_def,
1511 transitive_def, LIST_REL_EL_EQN]
1512 >- (EQ_TAC >> SRW_TAC [][])
1513 >> Q.PAT_X_ASSUM `!x y z. R x y /\ R y z ==> R x z` MATCH_MP_TAC
1514 >> Q.EXISTS_TAC `EL n y`
1515 >> CONJ_TAC >> FIRST_X_ASSUM MATCH_MP_TAC
1516 >> ASM_REWRITE_TAC []
1517QED
1518
1519(*---------------------------------------------------------------------------
1520 Congruence rules for higher-order functions. Used when making
1521 recursive definitions by so-called higher-order recursion.
1522 ---------------------------------------------------------------------------*)
1523
1524Theorem list_size_thm[simp] =
1525 REWRITE_RULE [arithmeticTheory.ADD_ASSOC]
1526 (#2 (TypeBase.size_of “:'a list”));
1527
1528val Induct = INDUCT_THEN list_INDUCT STRIP_ASSUME_TAC;
1529
1530Theorem list_size_cong[defncong]:
1531 !M N f f'.
1532 M=N /\ (!x. MEM x N ==> (f x = f' x))
1533 ==>
1534 list_size f M = list_size f' N
1535Proof
1536Induct
1537 THEN REWRITE_TAC [list_size_thm, MEM]
1538 THEN REPEAT STRIP_TAC
1539 THEN PAT_X_ASSUM (Term‘x = y’) (SUBST_ALL_TAC o SYM)
1540 THEN REWRITE_TAC [list_size_thm]
1541 THEN MK_COMB_TAC THENL
1542 [NTAC 2 (MK_COMB_TAC THEN TRY REFL_TAC)
1543 THEN FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC [MEM],
1544 FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC [] THEN GEN_TAC
1545 THEN PAT_X_ASSUM (Term‘!x. MEM x l ==> Q x’)
1546 (MP_TAC o SPEC (Term‘x:'a’))
1547 THEN REWRITE_TAC [MEM] THEN REPEAT STRIP_TAC
1548 THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]
1549QED
1550
1551Theorem list_size_append:
1552 !f xs ys. list_size f (xs ++ ys) = list_size f xs + list_size f ys
1553Proof
1554 GEN_TAC \\ Induct \\ FULL_SIMP_TAC arith_ss [APPEND, list_size_thm]
1555QED
1556
1557Theorem FOLDR_CONG[defncong]:
1558 !l l' b b' (f:'a->'b->'b) f'.
1559 l=l' /\ b=b' /\ (!x a. MEM x l' ==> (f x a = f' x a))
1560 ==>
1561 FOLDR f b l = FOLDR f' b' l'
1562Proof
1563Induct
1564 THEN REWRITE_TAC [FOLDR, MEM]
1565 THEN REPEAT STRIP_TAC
1566 THEN REPEAT (PAT_X_ASSUM (Term‘x = y’) (SUBST_ALL_TAC o SYM))
1567 THEN REWRITE_TAC [FOLDR]
1568 THEN POP_ASSUM (fn th => MP_TAC (SPEC (Term‘h’) th) THEN ASSUME_TAC th)
1569 THEN REWRITE_TAC [MEM]
1570 THEN DISCH_TAC
1571 THEN MK_COMB_TAC
1572 THENL [CONV_TAC FUN_EQ_CONV THEN ASM_REWRITE_TAC [],
1573 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC []
1574 THEN REPEAT STRIP_TAC
1575 THEN FIRST_ASSUM MATCH_MP_TAC
1576 THEN ASM_REWRITE_TAC [MEM]]
1577QED
1578
1579Theorem FOLDL_CONG[defncong]:
1580 !l l' b b' (f:'b->'a->'b) f'.
1581 l=l' /\ b=b' /\ (!x a. MEM x l' ==> (f a x = f' a x))
1582 ==>
1583 FOLDL f b l = FOLDL f' b' l'
1584Proof
1585Induct
1586 THEN REWRITE_TAC [FOLDL, MEM]
1587 THEN REPEAT STRIP_TAC
1588 THEN REPEAT (PAT_X_ASSUM (Term‘x = y’) (SUBST_ALL_TAC o SYM))
1589 THEN REWRITE_TAC [FOLDL]
1590 THEN FIRST_ASSUM MATCH_MP_TAC
1591 THEN REWRITE_TAC[]
1592 THEN CONJ_TAC
1593 THENL [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC [MEM],
1594 REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC
1595 THEN ASM_REWRITE_TAC [MEM]]
1596QED
1597
1598
1599Theorem MAP_CONG[defncong]:
1600 !l1 l2 f f'.
1601 l1=l2 /\ (!x. MEM x l2 ==> (f x = f' x)) ==>
1602 MAP f l1 = MAP f' l2
1603Proof
1604Induct THEN REWRITE_TAC [MAP, MEM]
1605 THEN REPEAT STRIP_TAC
1606 THEN REPEAT (PAT_X_ASSUM (Term‘x = y’) (SUBST_ALL_TAC o SYM))
1607 THEN REWRITE_TAC [MAP]
1608 THEN MK_COMB_TAC
1609 THENL [MK_COMB_TAC THEN TRY REFL_TAC
1610 THEN FIRST_ASSUM MATCH_MP_TAC
1611 THEN REWRITE_TAC [MEM],
1612 FIRST_ASSUM MATCH_MP_TAC
1613 THEN REWRITE_TAC [] THEN REPEAT STRIP_TAC
1614 THEN FIRST_ASSUM MATCH_MP_TAC
1615 THEN ASM_REWRITE_TAC [MEM]]
1616QED
1617
1618Theorem MAP2_CONG[defncong]:
1619 !l1 l1' l2 l2' f f'.
1620 l1=l1' /\ l2=l2' /\
1621 (!x y. MEM x l1' /\ MEM y l2' ==> (f x y = f' x y))
1622 ==>
1623 (MAP2 f l1 l2 = MAP2 f' l1' l2')
1624Proof
1625 Induct THEN SRW_TAC[] [MAP2_DEF, MEM] THEN
1626 SRW_TAC[] [MAP2_DEF] THEN
1627 Cases_on ‘l2’ THEN
1628 SRW_TAC[][MAP2_DEF]
1629QED
1630
1631Theorem EXISTS_CONG[defncong]:
1632 !l1 l2 P P'.
1633 (l1=l2) /\ (!x. MEM x l2 ==> (P x = P' x))
1634 ==>
1635 (EXISTS P l1 = EXISTS P' l2)
1636Proof
1637Induct THEN REWRITE_TAC [EXISTS_DEF, MEM]
1638 THEN REPEAT STRIP_TAC
1639 THEN REPEAT (PAT_X_ASSUM (Term‘x = y’) (SUBST_ALL_TAC o SYM))
1640 THENL [PAT_X_ASSUM (Term‘EXISTS x y’) MP_TAC THEN REWRITE_TAC [EXISTS_DEF],
1641 REWRITE_TAC [EXISTS_DEF]
1642 THEN MK_COMB_TAC
1643 THENL [MK_COMB_TAC THEN TRY REFL_TAC
1644 THEN FIRST_ASSUM MATCH_MP_TAC
1645 THEN REWRITE_TAC [MEM],
1646 FIRST_ASSUM MATCH_MP_TAC
1647 THEN REWRITE_TAC [] THEN REPEAT STRIP_TAC
1648 THEN FIRST_ASSUM MATCH_MP_TAC
1649 THEN ASM_REWRITE_TAC [MEM]]]
1650QED
1651
1652
1653Theorem EVERY_CONG[defncong]:
1654 !l1 l2 P P'.
1655 l1=l2 /\ (!x. MEM x l2 ==> (P x <=> P' x))
1656 ==>
1657 (EVERY P l1 <=> EVERY P' l2)
1658Proof
1659Induct THEN REWRITE_TAC [EVERY_DEF, MEM]
1660 THEN REPEAT STRIP_TAC
1661 THEN REPEAT (PAT_X_ASSUM (Term‘x = y’) (SUBST_ALL_TAC o SYM))
1662 THEN REWRITE_TAC [EVERY_DEF]
1663 THEN MK_COMB_TAC
1664 THENL [MK_COMB_TAC THEN TRY REFL_TAC
1665 THEN FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC [MEM],
1666 FIRST_ASSUM MATCH_MP_TAC
1667 THEN REWRITE_TAC [] THEN REPEAT STRIP_TAC
1668 THEN FIRST_ASSUM MATCH_MP_TAC
1669 THEN ASM_REWRITE_TAC [MEM]]
1670QED
1671
1672Theorem EVERY_MONOTONIC = MONO_EVERY
1673
1674(* ----------------------------------------------------------------------
1675 ZIP and UNZIP functions (taken from rich_listTheory)
1676 ---------------------------------------------------------------------- *)
1677val ZIP_def =
1678 let val lemma = prove(
1679 (“?ZIP.
1680 (!l2. ZIP ([], l2) = []) /\
1681 (!l1. ZIP (l1, []) = []) /\
1682 (!(x1:'a) l1 (x2:'b) l2.
1683 ZIP ((CONS x1 l1), (CONS x2 l2)) = CONS (x1,x2)(ZIP (l1, l2)))”),
1684 let val th = prove_rec_fn_exists list_Axiom
1685 (“(fn [] l = []) /\
1686 (fn (CONS (x:'a) l') (l:'b list) =
1687 if l = [] then [] else
1688 CONS (x, (HD l)) (fn l' (TL l)))”)
1689 in
1690 STRIP_ASSUME_TAC th
1691 THEN EXISTS_TAC
1692 (“UNCURRY (fn:('a)list -> (('b)list -> ('a # 'b)list))”)
1693 THEN ASM_REWRITE_TAC[pairTheory.UNCURRY_DEF, HD, TL, NOT_CONS_NIL]
1694 THEN STRIP_TAC
1695 THEN STRIP_ASSUME_TAC (SPEC “l1:'a list” list_CASES)
1696 THEN ASM_REWRITE_TAC[]
1697 end)
1698 in
1699 Rsyntax.new_specification
1700 {consts = [{const_name = "ZIP", fixity = NONE}],
1701 name = "ZIP_def",
1702 sat_thm = lemma
1703 }
1704 end;
1705
1706Theorem ZIP_ind:
1707 !P. (!l2. P ([], l2)) /\ (!l1. P(l1, [])) /\
1708 (!l1 l2 h1 h2. P (l1, l2) ==> P (h1::l1, h2::l2)) ==>
1709 !p. P p
1710Proof
1711 gen_tac >> strip_tac >> simp[pairTheory.FORALL_PROD] >> Induct >> simp[] >>
1712 gen_tac >> Cases >> simp[]
1713QED
1714
1715val _ = DefnBase.register_indn(ZIP_ind, [{Thy = "list", Name = "ZIP"}])
1716
1717Theorem ZIP_ind_alt :
1718 !P.
1719 (!l. P ([],l)) /\ (!h t. P (h::t,[])) /\
1720 (!x xs y ys. P (xs,ys) ==> P (x::xs,y::ys)) ==>
1721 !v v1. P (v,v1)
1722Proof
1723 ntac 2 strip_tac
1724 \\ Induct \\ ASM_REWRITE_TAC[]
1725 \\ gen_tac \\ Cases \\ ASM_SIMP_TAC bool_ss []
1726QED
1727
1728Theorem ZIP:
1729 (ZIP ([],[]) = []) /\
1730 (!(x1:'a) l1 (x2:'b) l2.
1731 ZIP ((CONS x1 l1), (CONS x2 l2)) = CONS (x1,x2)(ZIP (l1, l2)))
1732Proof
1733 REWRITE_TAC [ZIP_def]
1734QED
1735
1736Definition UNZIP:
1737 (UNZIP [] = ([], [])) /\
1738 (UNZIP (CONS (x:'a # 'b) l) =
1739 (CONS (FST x) (FST (UNZIP l)),
1740 CONS (SND x) (SND (UNZIP l))))
1741End
1742
1743Theorem UNZIP_THM:
1744 (UNZIP [] = ([]:'a list,[]:'b list)) /\
1745 (UNZIP ((x:'a,y:'b)::t) = let (L1,L2) = UNZIP t in (x::L1, y::L2))
1746Proof
1747 RW_TAC bool_ss [UNZIP]
1748 THEN Cases_on ‘UNZIP t’
1749 THEN RW_TAC bool_ss [LET_THM, pairTheory.UNCURRY_DEF,
1750 pairTheory.FST, pairTheory.SND]
1751QED
1752
1753Theorem UNZIP_MAP:
1754 !L. UNZIP L = (MAP FST L, MAP SND L)
1755Proof
1756 LIST_INDUCT_TAC THEN
1757 ASM_SIMP_TAC arith_ss [UNZIP, MAP,
1758 PAIR_EQ, pairTheory.FST, pairTheory.SND]
1759QED
1760
1761val SUC_NOT = arithmeticTheory.SUC_NOT
1762Theorem LENGTH_ZIP:
1763 !(l1:'a list) (l2:'b list).
1764 (LENGTH l1 = LENGTH l2) ==>
1765 (LENGTH(ZIP(l1,l2)) = LENGTH l1) /\
1766 (LENGTH(ZIP(l1,l2)) = LENGTH l2)
1767Proof
1768 LIST_INDUCT_TAC THEN REPEAT (FILTER_GEN_TAC (“l2:'b list”)) THEN
1769 LIST_INDUCT_TAC THEN
1770 REWRITE_TAC[ZIP, LENGTH, NOT_SUC, SUC_NOT, INV_SUC_EQ] THEN
1771 DISCH_TAC THEN RES_TAC THEN ASM_REWRITE_TAC[]
1772QED
1773
1774Theorem LENGTH_ZIP_MIN[simp]:
1775 !xs ys. LENGTH (ZIP (xs,ys)) = MIN (LENGTH xs) (LENGTH ys)
1776Proof
1777 Induct >> fs [LENGTH,ZIP_def] >> Cases_on ‘ys’ >> fs [LENGTH,ZIP_def] >>
1778 rw [arithmeticTheory.MIN_DEF]
1779QED
1780
1781Theorem LENGTH_UNZIP:
1782 !pl. (LENGTH (FST (UNZIP pl)) = LENGTH pl) /\
1783 (LENGTH (SND (UNZIP pl)) = LENGTH pl)
1784Proof
1785 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [UNZIP, LENGTH]
1786QED
1787
1788Theorem ZIP_UNZIP:
1789 !l:('a # 'b)list. ZIP(UNZIP l) = l
1790Proof
1791 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[UNZIP, ZIP]
1792QED
1793
1794Theorem UNZIP_ZIP:
1795 !l1:'a list. !l2:'b list.
1796 (LENGTH l1 = LENGTH l2) ==> (UNZIP(ZIP(l1,l2)) = (l1,l2))
1797Proof
1798 LIST_INDUCT_TAC THEN REPEAT (FILTER_GEN_TAC (“l2:'b list”))
1799 THEN LIST_INDUCT_TAC
1800 THEN ASM_REWRITE_TAC[UNZIP, ZIP, LENGTH, NOT_SUC, SUC_NOT, INV_SUC_EQ]
1801 THEN REPEAT STRIP_TAC THEN RES_THEN SUBST1_TAC THEN REWRITE_TAC[]
1802QED
1803
1804
1805Theorem ZIP_MAP:
1806 !l1 l2 f1 f2.
1807 (LENGTH l1 = LENGTH l2) ==>
1808 (ZIP (MAP f1 l1, l2) = MAP (\p. (f1 (FST p), SND p)) (ZIP (l1, l2))) /\
1809 (ZIP (l1, MAP f2 l2) = MAP (\p. (FST p, f2 (SND p))) (ZIP (l1, l2)))
1810Proof
1811 LIST_INDUCT_TAC THEN REWRITE_TAC [MAP, LENGTH] THEN REPEAT GEN_TAC THEN
1812 STRIP_TAC THENL [
1813 Q.SUBGOAL_THEN ‘l2 = []’ SUBST_ALL_TAC THEN
1814 REWRITE_TAC [ZIP, MAP] THEN mesonLib.ASM_MESON_TAC [LENGTH_NIL],
1815 Q.SUBGOAL_THEN
1816 ‘?l2h l2t. (l2 = l2h::l2t) /\ (LENGTH l2t = LENGTH l1)’
1817 STRIP_ASSUME_TAC THENL [
1818 mesonLib.ASM_MESON_TAC [LENGTH_CONS],
1819 ASM_SIMP_TAC bool_ss [ZIP, MAP, FST, SND]
1820 ]
1821 ]
1822QED
1823
1824Theorem MEM_ZIP:
1825 !(l1:'a list) (l2:'b list) p.
1826 (LENGTH l1 = LENGTH l2) ==>
1827 (MEM p (ZIP(l1, l2)) =
1828 ?n. n < LENGTH l1 /\ (p = (EL n l1, EL n l2)))
1829Proof
1830 LIST_INDUCT_TAC THEN SIMP_TAC bool_ss [LENGTH] THEN REPEAT STRIP_TAC THENL [
1831 ‘l2 = []’ by ASM_MESON_TAC [LENGTH_NIL] THEN
1832 FULL_SIMP_TAC arith_ss [ZIP, MEM, LENGTH],
1833 ‘?l2h l2t. (l2 = l2h::l2t) /\ (LENGTH l2t = LENGTH l1)’
1834 by ASM_MESON_TAC [LENGTH_CONS] THEN
1835 FULL_SIMP_TAC arith_ss [MEM, ZIP, LENGTH] THEN EQ_TAC THEN
1836 STRIP_TAC THENL [
1837 Q.EXISTS_TAC ‘0’ THEN ASM_SIMP_TAC arith_ss [EL, HD],
1838 Q.EXISTS_TAC ‘SUC n’ THEN ASM_SIMP_TAC arith_ss [EL, TL],
1839 Cases_on ‘n’ THEN FULL_SIMP_TAC arith_ss [EL, HD, TL] THEN
1840 ASM_MESON_TAC []
1841 ]
1842 ]
1843QED
1844
1845Theorem EL_ZIP:
1846 !(l1:'a list) (l2:'b list) n.
1847 (LENGTH l1 = LENGTH l2) /\ n < LENGTH l1 ==>
1848 (EL n (ZIP (l1, l2)) = (EL n l1, EL n l2))
1849Proof
1850 Induct THEN SIMP_TAC arith_ss [LENGTH] THEN REPEAT STRIP_TAC THEN
1851 ‘?l2h l2t. (l2 = l2h::l2t) /\ (LENGTH l2t = LENGTH l1)’
1852 by ASM_MESON_TAC [LENGTH_CONS] THEN
1853 FULL_SIMP_TAC arith_ss [ZIP, LENGTH] THEN
1854 Cases_on ‘n’ THEN ASM_SIMP_TAC arith_ss [ZIP, EL, HD, TL]
1855QED
1856
1857
1858Theorem MAP2_ZIP:
1859 !l1 l2. (LENGTH l1 = LENGTH l2) ==>
1860 !f:'a->'b->'c. MAP2 f l1 l2 = MAP (UNCURRY f) (ZIP (l1,l2))
1861Proof
1862 let val UNCURRY_DEF = pairTheory.UNCURRY_DEF
1863 in
1864 LIST_INDUCT_TAC THEN REPEAT (FILTER_GEN_TAC (“l2:'b list”))
1865 THEN LIST_INDUCT_TAC
1866 THEN REWRITE_TAC[MAP, MAP2, ZIP, LENGTH, NOT_SUC, SUC_NOT]
1867 THEN ASM_REWRITE_TAC[CONS_11, UNCURRY_DEF, INV_SUC_EQ]
1868 end
1869QED
1870
1871Theorem MAP2_MAP = MAP2_ZIP
1872
1873Theorem MAP_ZIP:
1874 (LENGTH l1 = LENGTH l2) ==>
1875 (MAP FST (ZIP (l1,l2)) = l1) /\
1876 (MAP SND (ZIP (l1,l2)) = l2) /\
1877 (MAP (f o FST) (ZIP (l1,l2)) = MAP f l1) /\
1878 (MAP (g o SND) (ZIP (l1,l2)) = MAP g l2)
1879Proof
1880 Q.ID_SPEC_TAC ‘l2’ THEN Induct_on ‘l1’ THEN
1881 SRW_TAC [] [] THEN TRY(Cases_on ‘l2’) THEN
1882 FULL_SIMP_TAC (srw_ss()) [ZIP, MAP]
1883QED
1884
1885Theorem MEM_EL:
1886 !(l:'a list) x. MEM x l = ?n. n < LENGTH l /\ (x = EL n l)
1887Proof
1888 Induct THEN ASM_SIMP_TAC arith_ss [MEM, LENGTH] THEN REPEAT GEN_TAC THEN
1889 EQ_TAC THEN STRIP_TAC THENL [
1890 Q.EXISTS_TAC ‘0’ THEN ASM_SIMP_TAC arith_ss [EL, HD],
1891 Q.EXISTS_TAC ‘SUC n’ THEN ASM_SIMP_TAC arith_ss [EL, TL],
1892 Cases_on ‘n’ THEN FULL_SIMP_TAC arith_ss [EL, HD, TL] THEN
1893 ASM_MESON_TAC []
1894 ]
1895QED
1896
1897Theorem EL_MEM :
1898 !n l. n < LENGTH l ==> MEM (EL n l) l
1899Proof
1900 RW_TAC std_ss [MEM_EL]
1901 >> Q.EXISTS_TAC ‘n’ >> ASM_REWRITE_TAC []
1902QED
1903
1904Theorem SUM_MAP_PLUS_ZIP:
1905 !ls1 ls2.
1906 (LENGTH ls1 = LENGTH ls2) /\ (!x y. f (x,y) = g x + h y) ==>
1907 (SUM (MAP f (ZIP (ls1,ls2))) = SUM (MAP g ls1) + SUM (MAP h ls2))
1908Proof
1909 Induct THEN Cases_on ‘ls2’ THEN
1910 SRW_TAC [numSimps.ARITH_ss] [MAP, ZIP, MAP_ZIP, SUM]
1911QED
1912
1913Theorem LIST_REL_EVERY_ZIP:
1914 !R l1 l2.
1915 LIST_REL R l1 l2 <=>
1916 LENGTH l1 = LENGTH l2 /\ EVERY (UNCURRY R) (ZIP (l1,l2))
1917Proof
1918 GEN_TAC THEN Induct THEN SRW_TAC[] [LENGTH_NIL_SYM] THEN
1919 SRW_TAC [] [EQ_IMP_THM, LIST_REL_CONS1] THEN SRW_TAC [] [EVERY_DEF, ZIP] THEN
1920 Cases_on ‘l2’ THEN FULL_SIMP_TAC(srw_ss())[EVERY_DEF, ZIP]
1921QED
1922
1923Theorem NOT_EVERY_EXISTS_FIRST :
1924 !P l. ~EVERY P l <=> ?i. i < LENGTH l /\ ~P (EL i l) /\ !j. j < i ==> P (EL j l)
1925Proof
1926 rpt STRIP_TAC
1927 >> reverse EQ_TAC
1928 >- (rw [NOT_EVERY, EXISTS_MEM] \\
1929 Q.EXISTS_TAC ‘EL i l’ >> rw [MEM_EL] \\
1930 Q.EXISTS_TAC ‘i’ >> rw [])
1931 >> rw [EVERY_EL, EXISTS_MEM, MEM_EL]
1932 >> Q.EXISTS_TAC ‘LEAST n. n < LENGTH l /\ ~P (EL n l)’
1933 >> numLib.LEAST_ELIM_TAC
1934 >> CONJ_TAC >- (Q.EXISTS_TAC ‘n’ >> rw [])
1935 >> Q.X_GEN_TAC ‘i’ >> rw []
1936 >> Q.PAT_X_ASSUM ‘!m. m < i ==> _’ (MP_TAC o (Q.SPEC ‘j’))
1937 >> ‘j < LENGTH l’ by RW_TAC arith_ss []
1938 >> RW_TAC bool_ss []
1939QED
1940
1941Theorem EXISTS_FIRST :
1942 !P l. EXISTS P l <=> ?i. i < LENGTH l /\ P (EL i l) /\ !j. j < i ==> ~P (EL j l)
1943Proof
1944 rw [EXISTS_NOT_EVERY]
1945 >> MP_TAC (Q.SPEC ‘\x. ~P x’ NOT_EVERY_EXISTS_FIRST) >> rw []
1946QED
1947
1948(* --------------------------------------------------------------------- *)
1949(* REVERSE *)
1950(* --------------------------------------------------------------------- *)
1951
1952Definition REVERSE_DEF[nocompute,simp]:
1953 (REVERSE [] = []) /\
1954 (REVERSE (h::t) = (REVERSE t) ++ [h])
1955End
1956
1957Theorem REVERSE_APPEND:
1958 !l1 l2:'a list.
1959 REVERSE (l1 ++ l2) = (REVERSE l2) ++ (REVERSE l1)
1960Proof
1961 LIST_INDUCT_TAC THEN
1962 ASM_REWRITE_TAC [APPEND, REVERSE_DEF, APPEND_NIL, APPEND_ASSOC]
1963QED
1964
1965Theorem REVERSE_REVERSE[simp]:
1966 !l:'a list. REVERSE (REVERSE l) = l
1967Proof
1968 LIST_INDUCT_TAC THEN
1969 ASM_REWRITE_TAC [REVERSE_DEF, REVERSE_APPEND, APPEND]
1970QED
1971
1972Theorem REVERSE_11[simp]:
1973 !l1 l2:'a list. (REVERSE l1 = REVERSE l2) <=> (l1 = l2)
1974Proof
1975 REPEAT GEN_TAC THEN EQ_TAC THEN1
1976 (DISCH_THEN (MP_TAC o AP_TERM “REVERSE : 'a list -> 'a list”) THEN
1977 REWRITE_TAC [REVERSE_REVERSE]) THEN
1978 STRIP_TAC THEN ASM_REWRITE_TAC []
1979QED
1980
1981Theorem MEM_REVERSE[simp]:
1982 !l x. MEM x (REVERSE l) = MEM x l
1983Proof
1984 Induct THEN SRW_TAC [] [] THEN PROVE_TAC []
1985QED
1986
1987Theorem LENGTH_REVERSE[simp]:
1988 !l. LENGTH (REVERSE l) = LENGTH l
1989Proof
1990 Induct THEN SRW_TAC [] [arithmeticTheory.ADD1]
1991QED
1992
1993Theorem REVERSE_EQ_NIL[simp]:
1994 (REVERSE l = []) <=> (l = [])
1995Proof
1996 Cases_on ‘l’ THEN SRW_TAC [] []
1997QED
1998
1999Theorem REVERSE_EQ_SING[simp]:
2000 (REVERSE l = [e:'a]) <=> (l = [e])
2001Proof
2002 Cases_on ‘l’ THEN SRW_TAC [] [APPEND_EQ_SING, CONJ_COMM]
2003QED
2004
2005Theorem FILTER_REVERSE:
2006 !l P. FILTER P (REVERSE l) = REVERSE (FILTER P l)
2007Proof
2008 Induct THEN
2009 ASM_SIMP_TAC bool_ss [FILTER, REVERSE_DEF, FILTER_APPEND_DISTRIB,
2010 COND_RAND, COND_RATOR, APPEND_NIL]
2011QED
2012
2013(* ----------------------------------------------------------------------
2014 FRONT and LAST
2015 ---------------------------------------------------------------------- *)
2016
2017Definition LAST_DEF[nocompute]:
2018 LAST (h::t) = if t = [] then h else LAST t
2019End
2020
2021Definition FRONT_DEF[nocompute]:
2022 FRONT [] = [] /\
2023 FRONT (h::t) = if t = [] then [] else h :: FRONT t
2024End
2025
2026Theorem FRONT_NIL[simp] = cj 1 FRONT_DEF
2027
2028Theorem LAST_CONS[simp]:
2029 (!x:'a. LAST [x] = x) /\
2030 (!(x:'a) y z. LAST (x::y::z) = LAST(y::z))
2031Proof
2032 REWRITE_TAC [LAST_DEF, NOT_CONS_NIL]
2033QED
2034
2035Theorem LAST_EL:
2036 !ls. (ls <> []) ==> (LAST ls = EL (PRE (LENGTH ls)) ls)
2037Proof
2038Induct THEN SRW_TAC[] [] THEN
2039Cases_on ‘ls’ THEN FULL_SIMP_TAC (srw_ss()) []
2040QED
2041
2042Theorem LAST_MAP[simp]:
2043 !l f. l <> [] ==> (LAST (MAP f l) = f (LAST l))
2044Proof
2045 rpt strip_tac >> ‘?h t. l = h::t’ by METIS_TAC[list_CASES] >>
2046 srw_tac[][MAP] >> Q.ID_SPEC_TAC ‘h’ >> Induct_on ‘t’ >>
2047 asm_simp_tac (srw_ss()) []
2048QED
2049
2050Theorem FRONT_CONS[simp]:
2051 (!x:'a. FRONT [x] = []) /\
2052 (!x:'a y z. FRONT (x::y::z) = x :: FRONT (y::z))
2053Proof
2054 REWRITE_TAC [FRONT_DEF, NOT_CONS_NIL]
2055QED
2056
2057Theorem FRONT_CONS_NOT_NIL :
2058 !h t. t <> [] ==> FRONT (h::t) = h :: FRONT t
2059Proof
2060 RW_TAC std_ss [FRONT_DEF]
2061QED
2062
2063Theorem LENGTH_FRONT_CONS[simp]:
2064 !x xs. LENGTH (FRONT (x::xs)) = LENGTH xs
2065Proof
2066Induct_on ‘xs’ THEN ASM_SIMP_TAC bool_ss [FRONT_CONS, LENGTH]
2067QED
2068
2069Theorem LENGTH_FRONT:
2070 !xs. LENGTH (FRONT xs) = LENGTH xs - 1
2071Proof
2072 Cases >> simp[LENGTH_FRONT_CONS]
2073QED
2074
2075Theorem FRONT_CONS_EQ_NIL[simp]:
2076 (!x:'a xs. (FRONT (x::xs) = []) = (xs = [])) /\
2077 (!x:'a xs. ([] = FRONT (x::xs)) = (xs = [])) /\
2078 (!x:'a xs. NULL (FRONT (x::xs)) = NULL xs)
2079Proof
2080SIMP_TAC bool_ss [GSYM FORALL_AND_THM] THEN
2081Cases_on ‘xs’ THEN SIMP_TAC bool_ss [FRONT_CONS, NOT_NIL_CONS, NULL_DEF]
2082QED
2083
2084Theorem APPEND_FRONT_LAST:
2085 !l:'a list. ~(l = []) ==> (APPEND (FRONT l) [LAST l] = l)
2086Proof
2087 LIST_INDUCT_TAC THEN REWRITE_TAC [NOT_CONS_NIL] THEN
2088 POP_ASSUM MP_TAC THEN Q.SPEC_THEN ‘l’ STRUCT_CASES_TAC list_CASES THEN
2089 REWRITE_TAC [NOT_CONS_NIL] THEN STRIP_TAC THEN
2090 ASM_REWRITE_TAC [FRONT_CONS, LAST_CONS, APPEND]
2091QED
2092
2093Theorem LAST_CONS_cond:
2094 LAST (h::t) = if t = [] then h else LAST t
2095Proof
2096 Cases_on ‘t’ THEN SRW_TAC [] []
2097QED
2098
2099Theorem LAST_APPEND_CONS[simp]:
2100 !h l1 l2. LAST (l1 ++ h::l2) = LAST (h::l2)
2101Proof
2102 Induct_on ‘l1’ THEN SRW_TAC [] [LAST_CONS_cond]
2103QED
2104
2105
2106(* ----------------------------------------------------------------------
2107 TAKE and DROP
2108 ---------------------------------------------------------------------- *)
2109
2110(* these are FIRSTN and BUTFIRSTN from rich_listTheory, but made total *)
2111
2112Definition TAKE_def[nocompute]:
2113 (TAKE n [] = []) /\
2114 (TAKE n (x::xs) = if n = 0 then [] else x :: TAKE (n - 1) xs)
2115End
2116
2117Definition DROP_def[nocompute]:
2118 (DROP n [] = []) /\
2119 (DROP n (x::xs) = if n = 0 then x::xs else DROP (n - 1) xs)
2120End
2121
2122Theorem TAKE_nil[simp] = cj 1 TAKE_def
2123
2124Theorem TAKE_cons[simp]: 0 < n ==> (TAKE n (x::xs) = x::(TAKE (n-1) xs))
2125Proof
2126 SRW_TAC[][TAKE_def]
2127QED
2128
2129Theorem DROP_nil[simp] = CONJUNCT1 DROP_def
2130
2131Theorem DROP_cons[simp]: 0 < n ==> (DROP n (x::xs) = DROP (n-1) xs)
2132Proof
2133 SRW_TAC[][DROP_def]
2134QED
2135
2136Theorem TAKE_0[simp]:
2137 TAKE 0 l = []
2138Proof
2139 Cases_on ‘l’ THEN SRW_TAC [] [TAKE_def]
2140QED
2141
2142Theorem TAKE_LENGTH_ID[simp]:
2143 !l. TAKE (LENGTH l) l = l
2144Proof
2145 Induct_on ‘l’ THEN SRW_TAC [] []
2146QED
2147
2148Theorem LENGTH_TAKE[simp]:
2149 !n l. n <= LENGTH l ==> (LENGTH (TAKE n l) = n)
2150Proof
2151 Induct_on ‘l’ THEN SRW_TAC [numSimps.ARITH_ss] [TAKE_def]
2152QED
2153
2154Theorem TAKE_LENGTH_TOO_LONG:
2155 !l n. LENGTH l <= n ==> (TAKE n l = l)
2156Proof
2157 Induct THEN SRW_TAC [numSimps.ARITH_ss] []
2158QED
2159
2160Theorem LENGTH_TAKE_EQ:
2161 LENGTH (TAKE n xs) = if n <= LENGTH xs then n else LENGTH xs
2162Proof
2163 SRW_TAC [] [] THEN fs [GSYM NOT_LESS] THEN AP_TERM_TAC
2164 THEN MATCH_MP_TAC TAKE_LENGTH_TOO_LONG THEN numLib.DECIDE_TAC
2165QED
2166
2167Theorem EL_TAKE:
2168 !n x l. x < n ==> (EL x (TAKE n l) = EL x l)
2169Proof
2170 Induct_on ‘n’ >> ASM_SIMP_TAC (srw_ss()) [TAKE_def] >>
2171 Cases_on ‘x’ >> Cases_on ‘l’ >>
2172 ASM_SIMP_TAC (srw_ss()) [TAKE_def]
2173QED
2174
2175(* |- !n l. 0 < n ==> HD (TAKE n l) = HD l *)
2176Theorem HD_TAKE = GEN_ALL (REWRITE_RULE [EL] (Q.SPECL [‘n’, ‘0’] EL_TAKE))
2177
2178Theorem MAP_TAKE:
2179 !f n l. MAP f (TAKE n l) = TAKE n (MAP f l)
2180Proof
2181 Induct_on‘l’ THEN SRW_TAC[][TAKE_def]
2182QED
2183
2184Theorem TAKE_APPEND1:
2185 !n. n <= LENGTH l1 ==> (TAKE n (APPEND l1 l2) = TAKE n l1)
2186Proof
2187 Induct_on ‘l1’ THEN SRW_TAC [numSimps.ARITH_ss] [TAKE_def]
2188QED
2189
2190Theorem TAKE_APPEND2:
2191 !n. LENGTH l1 < n ==> (TAKE n (l1 ++ l2) = l1 ++ TAKE (n - LENGTH l1) l2)
2192Proof
2193 Induct_on ‘l1’ THEN SRW_TAC [numSimps.ARITH_ss] [arithmeticTheory.ADD1]
2194QED
2195
2196Theorem DROP_0[simp]:
2197 DROP 0 l = l
2198Proof
2199 Induct_on ‘l’ THEN SRW_TAC [] [DROP_def]
2200QED
2201
2202Theorem DROP_LENGTH_NIL[simp]:
2203 !l. DROP (LENGTH l) l = []
2204Proof
2205 Induct >> simp[]
2206QED
2207
2208Theorem DROP_APPEND1:
2209 !n l1. n <= LENGTH l1 ==> !l2. DROP n (l1 ++ l2) = DROP n l1 ++ l2
2210Proof
2211 Induct_on ‘l1’ >> simp[] >> Cases_on ‘n’ >> simp[]
2212QED
2213
2214Theorem DROP_APPEND2:
2215 !l1 n. LENGTH l1 <= n ==> !l2. DROP n (l1 ++ l2) = DROP (n - LENGTH l1) l2
2216Proof
2217 Induct >> simp[] >> Cases_on ‘n’ >> simp[GSYM arithmeticTheory.ADD1]
2218QED
2219
2220Theorem DROP_APPEND:
2221 !n l1 l2. DROP n (l1 ++ l2) = DROP n l1 ++ DROP (n - LENGTH l1) l2
2222Proof
2223 Induct_on ‘l1’ >> simp[] >> Cases_on ‘n’ >> simp[]
2224QED
2225
2226Theorem TAKE_DROP[simp]:
2227 !n l. TAKE n l ++ DROP n l = l
2228Proof
2229 Induct_on ‘l’ THEN SRW_TAC [numSimps.ARITH_ss] [TAKE_def]
2230QED
2231
2232Theorem TAKE1:
2233 !l. l <> [] ==> (TAKE 1 l = [EL 0 l])
2234Proof Induct_on ‘l’ >> srw_tac[][]
2235QED
2236
2237Theorem TAKE1_DROP[simp]:
2238 !n l. n < LENGTH l ==> (TAKE 1 (DROP n l) = [EL n l])
2239Proof
2240 Induct_on ‘l’ >> rw[] >> Cases_on ‘n’ >> fs[EL_restricted]
2241QED
2242
2243Theorem TAKE_EQ_NIL[simp]:
2244 (TAKE n l = []) <=> (n = 0) \/ (l = [])
2245Proof
2246 Q.ID_SPEC_TAC ‘l’ THEN Induct_on ‘n’ THEN ASM_SIMP_TAC (srw_ss()) [] THEN
2247 Cases THEN ASM_SIMP_TAC (srw_ss()) []
2248QED
2249
2250Theorem TAKE_EQ_REWRITE :
2251 !l m n. m <= LENGTH l /\ n <= LENGTH l ==> (TAKE m l = TAKE n l <=> m = n)
2252Proof
2253 rpt STRIP_TAC
2254 >> rw [LIST_EQ_REWRITE]
2255 >> EQ_TAC >> rw []
2256QED
2257
2258Theorem TAKE_TAKE_MIN:
2259 !m n. TAKE n (TAKE m l) = TAKE (MIN n m) l
2260Proof
2261 Induct_on‘l’ >> rw[] >>
2262 Cases_on‘m’ >> Cases_on‘n’ >>
2263 SRW_TAC[numSimps.ARITH_ss][arithmeticTheory.MIN_DEF, arithmeticTheory.ADD1] >>
2264 FULL_SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) []
2265QED
2266
2267Theorem FRONT_TAKE :
2268 !l n. 0 < n /\ n <= LENGTH l ==> (FRONT (TAKE n l) = TAKE (n - 1) l)
2269Proof
2270 Induct THEN SRW_TAC [numSimps.ARITH_ss][TAKE_def, DROP_def] >>
2271 `0 < n - 1 /\ n - 1 <= LENGTH l` by numLib.DECIDE_TAC THEN
2272 SRW_TAC [][FRONT_DEF] THENL [
2273 fs [],
2274 `(n - 1) - 1 = n - 2` by numLib.DECIDE_TAC THEN
2275 SRW_TAC [][]
2276 ]
2277QED
2278
2279Theorem LENGTH_DROP[simp]:
2280 !n l. LENGTH (DROP n l) = LENGTH l - n
2281Proof
2282 Induct_on ‘l’ THEN SRW_TAC [numSimps.ARITH_ss] [DROP_def]
2283QED
2284
2285Theorem DROP_LENGTH_TOO_LONG:
2286 !l n. LENGTH l <= n ==> (DROP n l = [])
2287Proof Induct THEN SRW_TAC [numSimps.ARITH_ss] []
2288QED
2289
2290Theorem LT_SUC[local] = arithmeticTheory.LT_SUC
2291
2292Theorem MEM_DROP:
2293 !x ls n. MEM x (DROP n ls) <=>
2294 ?m. m + n < LENGTH ls /\ x = EL (m + n) ls
2295Proof
2296 Induct_on ‘ls’ >> rw[DROP_def, LT_SUC] >> asm_simp_tac(srw_ss() ++ DNF_ss)[]
2297 >- simp[MEM_EL] >>
2298 Q.RENAME_TAC [‘n <> 0’] >> Cases_on ‘n’ >> fs[] >>
2299 asm_simp_tac (srw_ss() ++ numSimps.ARITH_ss ++ CONJ_ss)
2300 [GSYM arithmeticTheory.ADD1, ADD_CLAUSES]
2301QED
2302
2303Theorem DROP_EQ_NIL[simp]:
2304 !ls n. DROP n ls = [] <=> LENGTH ls <= n
2305Proof
2306 Induct THEN SRW_TAC[] [DROP_def] THEN numLib.DECIDE_TAC
2307QED
2308
2309Theorem HD_DROP:
2310 !n l. n < LENGTH l ==> (HD (DROP n l) = EL n l)
2311Proof Induct_on ‘l’ >> asm_simp_tac (srw_ss() ++ DNF_ss) [LT_SUC]
2312QED
2313
2314Theorem EL_DROP:
2315 !m n l. m + n < LENGTH l ==> (EL m (DROP n l) = EL (m + n) l)
2316Proof
2317 Induct_on ‘l’ >> SIMP_TAC (srw_ss()) [] >> Cases_on ‘n’ >>
2318 FULL_SIMP_TAC (srw_ss()) [DROP_def, ADD_CLAUSES]
2319QED
2320
2321Theorem MAP_DROP:
2322 !l i. MAP f (DROP i l) = DROP i (MAP f l)
2323Proof Induct \\ simp[DROP_def] \\ rw[]
2324QED
2325
2326Theorem MAP_FRONT:
2327 !ls. MAP f (FRONT ls) = FRONT (MAP f ls)
2328Proof
2329 Induct >> simp[] >> Cases_on ‘ls’ >> fs[]
2330QED
2331(* More functions for operating on pairs of lists *)
2332
2333Definition FOLDL2_def[simp]:
2334 (FOLDL2 f a (b::bs) (c::cs) = FOLDL2 f (f a b c) bs cs) /\
2335 (FOLDL2 f a bs cs = a)
2336End
2337
2338Theorem FOLDL2_cong[defncong]:
2339 !l1 l1' l2 l2' a a' f f'.
2340 l1 = l1' /\ l2 = l2' /\ a = a' /\
2341 (!z b c. MEM b l1' /\ MEM c l2' ==> (f z b c = f' z b c)) ==>
2342 FOLDL2 f a l1 l2 = FOLDL2 f' a' l1' l2'
2343Proof
2344Induct THEN SIMP_TAC(srw_ss()) [FOLDL2_def] THEN
2345GEN_TAC THEN Cases THEN SRW_TAC[] [FOLDL2_def]
2346QED
2347
2348Theorem FOLDL2_FOLDL:
2349 !l1 l2. LENGTH l1 = LENGTH l2 ==>
2350 !f a. FOLDL2 f a l1 l2 = FOLDL (\a. UNCURRY (f a)) a (ZIP (l1,l2))
2351Proof
2352 Induct THEN1 SRW_TAC[] [LENGTH_NIL_SYM, ZIP, FOLDL] THEN
2353 GEN_TAC THEN Cases THEN SRW_TAC [] [ZIP, FOLDL]
2354QED
2355
2356Overload EVERY2[inferior] = “LIST_REL”
2357
2358Theorem EVERY2_cong[defncong]:
2359 !l1 l1' l2 l2' P P'.
2360 l1 = l1' /\ l2 = l2' /\
2361 (!x y. MEM x l1' /\ MEM y l2' ==> (P x y = P' x y)) ==>
2362 (EVERY2 P l1 l2 <=> EVERY2 P' l1' l2')
2363Proof
2364 Induct THEN SIMP_TAC (srw_ss()) [] THEN
2365 GEN_TAC THEN Cases THEN SRW_TAC [] [] THEN
2366 METIS_TAC[]
2367QED
2368
2369Theorem LIST_REL_cong = EVERY2_cong
2370
2371Theorem MAP_EQ_EVERY2:
2372 !f1 f2 l1 l2. (MAP f1 l1 = MAP f2 l2) <=>
2373 (LENGTH l1 = LENGTH l2) /\
2374 LIST_REL (\x y. f1 x = f2 y) l1 l2
2375Proof
2376NTAC 2 GEN_TAC THEN
2377Induct THEN SRW_TAC [] [LENGTH_NIL_SYM, MAP] THEN
2378Cases_on ‘l2’ THEN SRW_TAC [] [MAP] THEN
2379PROVE_TAC[]
2380QED
2381
2382Theorem MAP_EQ_LIST_REL = MAP_EQ_EVERY2
2383
2384Theorem EVERY2_EVERY:
2385 !l1 l2 f. EVERY2 f l1 l2 <=>
2386 LENGTH l1 = LENGTH l2 /\ EVERY (UNCURRY f) (ZIP (l1,l2))
2387Proof
2388Induct THEN1 SRW_TAC [] [LENGTH_NIL_SYM, EQ_IMP_THM, ZIP] THEN
2389GEN_TAC THEN Cases THEN SRW_TAC [] [ZIP, EQ_IMP_THM]
2390QED
2391
2392Theorem LIST_REL_EVERY = EVERY2_EVERY
2393
2394Theorem EVERY2_LENGTH:
2395 !P l1 l2. EVERY2 P l1 l2 ==> (LENGTH l1 = LENGTH l2)
2396Proof
2397PROVE_TAC[EVERY2_EVERY]
2398QED
2399
2400Theorem EVERY2_mono = LIST_REL_mono
2401
2402(* ----------------------------------------------------------------------
2403 ALL_DISTINCT
2404 ---------------------------------------------------------------------- *)
2405
2406Definition ALL_DISTINCT[nocompute,simp]:
2407 (ALL_DISTINCT [] <=> T) /\
2408 (ALL_DISTINCT (h::t) <=> ~MEM h t /\ ALL_DISTINCT t)
2409End
2410
2411Theorem lemma[local]:
2412 !l x. (FILTER ((=) x) l = []) = ~MEM x l
2413Proof
2414 LIST_INDUCT_TAC THEN
2415 ASM_SIMP_TAC (bool_ss ++ COND_elim_ss)
2416 [FILTER, MEM, NOT_CONS_NIL, EQ_IMP_THM,
2417 LEFT_AND_OVER_OR, FORALL_AND_THM, DISJ_IMP_THM]
2418QED
2419
2420Theorem ALL_DISTINCT_FILTER:
2421 !l. ALL_DISTINCT l = !x. MEM x l ==> (FILTER ((=) x) l = [x])
2422Proof
2423 LIST_INDUCT_TAC THEN
2424 ASM_SIMP_TAC (bool_ss ++ COND_elim_ss)
2425 [ALL_DISTINCT, MEM, FILTER, DISJ_IMP_THM,
2426 FORALL_AND_THM, CONS_11, EQ_IMP_THM, lemma] THEN
2427 metisLib.METIS_TAC []
2428QED
2429
2430Theorem FILTER_ALL_DISTINCT:
2431 !P l. ALL_DISTINCT l ==> ALL_DISTINCT (FILTER P l)
2432Proof
2433 Induct_on ‘l’ THEN SRW_TAC [] [MEM_FILTER]
2434QED
2435
2436Theorem ALL_DISTINCT_MAP:
2437 !f ls. ALL_DISTINCT (MAP f ls) ==> ALL_DISTINCT ls
2438Proof
2439GEN_TAC THEN Induct THEN SRW_TAC[][ALL_DISTINCT, MAP, MEM_MAP] THEN PROVE_TAC[]
2440QED
2441
2442Theorem EL_ALL_DISTINCT_EL_EQ:
2443 !l. ALL_DISTINCT l =
2444 (!n1 n2. n1 < LENGTH l /\ n2 < LENGTH l ==>
2445 ((EL n1 l = EL n2 l) = (n1 = n2)))
2446Proof
2447 Induct THEN SRW_TAC [] [] THEN EQ_TAC THENL [
2448 REPEAT STRIP_TAC THEN Cases_on ‘n1’ THEN Cases_on ‘n2’ THEN
2449 SRW_TAC [numSimps.ARITH_ss] [] THEN PROVE_TAC [MEM_EL, LESS_MONO_EQ],
2450
2451 REPEAT STRIP_TAC THENL [
2452 FULL_SIMP_TAC (srw_ss()) [MEM_EL] THEN
2453 FIRST_X_ASSUM (Q.SPECL_THEN [‘0’, ‘SUC n’] MP_TAC) THEN
2454 SRW_TAC [] [],
2455
2456 FIRST_X_ASSUM (Q.SPECL_THEN [‘SUC n1’, ‘SUC n2’] MP_TAC) THEN
2457 SRW_TAC [] []
2458 ]
2459 ]
2460QED
2461
2462Theorem ALL_DISTINCT_EL_IMP:
2463 !l n1 n2. ALL_DISTINCT l /\ n1 < LENGTH l /\ n2 < LENGTH l ==>
2464 ((EL n1 l = EL n2 l) = (n1 = n2))
2465Proof
2466 PROVE_TAC[EL_ALL_DISTINCT_EL_EQ]
2467QED
2468
2469
2470Theorem ALL_DISTINCT_APPEND:
2471 !l1 l2. ALL_DISTINCT (l1++l2) =
2472 (ALL_DISTINCT l1 /\ ALL_DISTINCT l2 /\
2473 (!e. MEM e l1 ==> ~(MEM e l2)))
2474Proof
2475 Induct THEN SRW_TAC [] [] THEN PROVE_TAC []
2476QED
2477
2478Theorem ALL_DISTINCT_APPEND' :
2479 !l1 l2. ALL_DISTINCT (l1 ++ l2) <=>
2480 ALL_DISTINCT l1 /\ ALL_DISTINCT l2 /\ DISJOINT (set l1) (set l2)
2481Proof
2482 RW_TAC std_ss [ALL_DISTINCT_APPEND, DISJOINT_ALT]
2483QED
2484
2485Theorem ALL_DISTINCT_SING:
2486 !x. ALL_DISTINCT [x]
2487Proof
2488 SRW_TAC [] []
2489QED
2490
2491Theorem ALL_DISTINCT_ZIP:
2492 !l1 l2. ALL_DISTINCT l1 /\ (LENGTH l1 = LENGTH l2) ==>
2493 ALL_DISTINCT (ZIP (l1,l2))
2494Proof
2495 Induct THEN Cases_on `l2` THEN SRW_TAC [] [ZIP] THEN
2496 FULL_SIMP_TAC (srw_ss()) [MEM_EL, MEM_ZIP]
2497QED
2498
2499Theorem ALL_DISTINCT_ZIP_SWAP:
2500 !l1 l2. ALL_DISTINCT (ZIP (l1,l2)) /\ (LENGTH l1 = LENGTH l2) ==>
2501 ALL_DISTINCT (ZIP (l2,l1))
2502Proof
2503 SRW_TAC [] [EL_ALL_DISTINCT_EL_EQ] THEN
2504 Q.PAT_X_ASSUM ‘X = Y’ (ASSUME_TAC o SYM) THEN
2505 FULL_SIMP_TAC (srw_ss()) [EL_ZIP, LENGTH_ZIP] THEN
2506 METIS_TAC []
2507QED
2508
2509Theorem ALL_DISTINCT_REVERSE[simp]:
2510 !l. ALL_DISTINCT (REVERSE l) = ALL_DISTINCT l
2511Proof
2512 SIMP_TAC bool_ss [ALL_DISTINCT_FILTER, MEM_REVERSE, FILTER_REVERSE] THEN
2513 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [
2514 RES_TAC THEN
2515 ‘(FILTER ($= x) l) = REVERSE [x]’ by METIS_TAC[REVERSE_REVERSE] THEN
2516 FULL_SIMP_TAC bool_ss [REVERSE_DEF, APPEND],
2517 ASM_SIMP_TAC bool_ss [REVERSE_DEF, APPEND]
2518 ]
2519QED
2520
2521Theorem ALL_DISTINCT_FLAT_REVERSE[simp]:
2522 !xs. ALL_DISTINCT (FLAT (REVERSE xs)) = ALL_DISTINCT (FLAT xs)
2523Proof
2524 Induct \\ FULL_SIMP_TAC(srw_ss())[ALL_DISTINCT_APPEND]
2525 \\ FULL_SIMP_TAC(srw_ss())[MEM_FLAT,PULL_EXISTS] \\ METIS_TAC []
2526QED
2527
2528Theorem ALL_DISTINCT_INDEX_OF_EL:
2529 !l n.
2530 (ALL_DISTINCT l /\ n < LENGTH l) ==>
2531 INDEX_OF (EL n l) l = SOME n
2532Proof
2533 Induct
2534 \\ rw[INDEX_OF_def]
2535 \\ rw[INDEX_FIND_def]
2536 >- (
2537 Cases_on`n` \\ fs[]
2538 \\ metis_tac[MEM_EL] )
2539 \\ rw[Once INDEX_FIND_add, PULL_EXISTS]
2540 \\ fs[INDEX_OF_def]
2541 \\ Cases_on`n` \\ fs[]
2542 \\ first_x_assum drule
2543 \\ rw[]
2544 \\ rw[UNCURRY, arithmeticTheory.ADD1]
2545QED
2546
2547(* ----------------------------------------------------------------------
2548 LRC
2549 Where NRC has the number of steps in a transitive path,
2550 LRC has a list of the elements in the path (excluding the rightmost)
2551 ---------------------------------------------------------------------- *)
2552
2553Definition LRC_def:
2554 (LRC R [] x y <=> (x = y)) /\
2555 (LRC R (h::t) x y <=>
2556 x = h /\ ?z. R x z /\ LRC R t z y)
2557End
2558
2559Theorem NRC_LRC:
2560 NRC R n x y <=> ?ls. LRC R ls x y /\ (LENGTH ls = n)
2561Proof
2562MAP_EVERY Q.ID_SPEC_TAC [‘y’,‘x’] THEN
2563Induct_on ‘n’ THEN SRW_TAC [] [] THEN1 (
2564 SRW_TAC [] [EQ_IMP_THM] THEN1 (
2565 SRW_TAC [] [LRC_def] ) THEN
2566 FULL_SIMP_TAC (srw_ss()) [LRC_def]
2567) THEN
2568SRW_TAC [] [arithmeticTheory.NRC, EQ_IMP_THM] THEN1 (
2569 Q.EXISTS_TAC ‘x::ls’ THEN
2570 SRW_TAC [] [LRC_def] THEN
2571 METIS_TAC [] ) THEN
2572Cases_on ‘ls’ THEN FULL_SIMP_TAC (srw_ss()) [LRC_def] THEN
2573SRW_TAC [] [] THEN METIS_TAC []
2574QED
2575
2576Theorem LRC_MEM:
2577 LRC R ls x y /\ MEM e ls ==> ?z t. R e z /\ LRC R t z y
2578Proof
2579Q_TAC SUFF_TAC
2580‘!ls x y. LRC R ls x y ==> !e. MEM e ls ==> ?z t. R e z /\ LRC R t z y’
2581THEN1 METIS_TAC [] THEN
2582Induct THEN SRW_TAC [] [LRC_def] THEN METIS_TAC []
2583QED
2584
2585Theorem LRC_MEM_right:
2586 LRC R (h::t) x y /\ MEM e t ==> ?z p. R z e /\ LRC R p x z
2587Proof
2588 Q_TAC SUFF_TAC
2589 ‘!ls x y. LRC R ls x y ==>
2590 !h t e. (ls = h::t) /\ MEM e t ==> ?z p. R z e /\ LRC R p x z’
2591 THEN1 METIS_TAC [] THEN
2592 Induct THEN SRW_TAC [] [LRC_def] THEN
2593 Cases_on ‘ls’ THEN FULL_SIMP_TAC (srw_ss()) [LRC_def] THEN
2594 SRW_TAC [] [] THENL [
2595 MAP_EVERY Q.EXISTS_TAC [‘h’,‘[]’] THEN SRW_TAC [] [LRC_def],
2596 RES_TAC THEN
2597 MAP_EVERY Q.EXISTS_TAC [‘z''’,‘h::p’] THEN
2598 SRW_TAC [] [LRC_def] THEN
2599 METIS_TAC []
2600 ]
2601QED
2602
2603(* ----------------------------------------------------------------------
2604 Theorems relating (finite) sets and lists. First
2605
2606 LIST_TO_SET : 'a list -> 'a set
2607
2608 which is overloaded to "set".
2609 ---------------------------------------------------------------------- *)
2610
2611Theorem LIST_TO_SET_APPEND[simp]:
2612 !l1 l2. set (l1 ++ l2) = set l1 UNION set l2
2613Proof
2614 Induct THEN SRW_TAC [] [INSERT_UNION_EQ]
2615QED
2616
2617Theorem UNION_APPEND = GSYM LIST_TO_SET_APPEND
2618
2619Theorem LIST_TO_SET_EQ_EMPTY[simp]:
2620 ((set l = {}) <=> (l = [])) /\ (({} = set l) <=> (l = []))
2621Proof
2622 Cases_on ‘l’ THEN SRW_TAC [] []
2623QED
2624
2625Theorem FINITE_LIST_TO_SET[simp]:
2626 !l. FINITE (set l)
2627Proof
2628 Induct THEN SRW_TAC [] []
2629QED
2630
2631Theorem SUM_IMAGE_LIST_TO_SET_upper_bound:
2632 !ls. SIGMA f (set ls) <= SUM (MAP f ls)
2633Proof
2634 Induct THEN
2635 SRW_TAC [] [MAP, SUM, SUM_IMAGE_THM, SUM_IMAGE_DELETE] THEN
2636 numLib.DECIDE_TAC
2637QED
2638
2639Theorem SUM_MAP_MEM_bound:
2640 !f x ls. MEM x ls ==> f x <= SUM (MAP f ls)
2641Proof
2642NTAC 2 GEN_TAC THEN Induct THEN SRW_TAC[] [] THEN
2643FULL_SIMP_TAC(srw_ss()++numSimps.ARITH_ss)[MEM, MAP, SUM]
2644QED
2645
2646Theorem INJ_MAP_EQ:
2647 !f l1 l2. INJ f (set l1 UNION set l2) UNIV /\ MAP f l1 = MAP f l2 ==>
2648 l1 = l2
2649Proof
2650 GEN_TAC THEN Induct THEN1 SRW_TAC[] [MAP] THEN
2651 GEN_TAC THEN Cases THEN SRW_TAC[] [MAP]
2652 THEN1 (IMP_RES_TAC INJ_DEF THEN
2653 FIRST_X_ASSUM (MATCH_MP_TAC o MP_CANON) THEN
2654 SRW_TAC [] []) THEN
2655 PROVE_TAC[INJ_SUBSET, SUBSET_REFL, SUBSET_DEF, IN_UNION, IN_INSERT]
2656QED
2657
2658(* this turns out to be more useful; in particular, INJ_MAP_EQ can't
2659 be used as an introduction rule without explicit instantiation of
2660 its beta type variable, which only appears in the assumption *)
2661Theorem INJ_MAP_EQ_IFF:
2662 !f l1 l2.
2663 INJ f (set l1 UNION set l2) UNIV ==>
2664 ((MAP f l1 = MAP f l2) <=> (l1 = l2))
2665Proof
2666 rw[] >> EQ_TAC >- metis_tac[INJ_MAP_EQ] >> rw[]
2667QED
2668
2669local open numLib in
2670Theorem CARD_LIST_TO_SET:
2671 CARD (set ls) <= LENGTH ls
2672Proof
2673Induct_on ‘ls’ THEN SRW_TAC [] [] THEN
2674DECIDE_TAC
2675QED
2676end
2677
2678Theorem ALL_DISTINCT_CARD_LIST_TO_SET:
2679 !ls. ALL_DISTINCT ls ==> (CARD (set ls) = LENGTH ls)
2680Proof
2681Induct THEN SRW_TAC [] []
2682QED
2683
2684val th1 = MATCH_MP arithmeticTheory.LESS_EQ_IMP_LESS_SUC CARD_LIST_TO_SET ;
2685val th2 = MATCH_MP prim_recTheory.LESS_NOT_EQ th1 ;
2686
2687Theorem CARD_LIST_TO_SET_ALL_DISTINCT:
2688 !ls. (CARD (set ls) = LENGTH ls) ==> ALL_DISTINCT ls
2689Proof
2690Induct THEN SRW_TAC [] [th2]
2691QED
2692
2693Theorem LIST_TO_SET_REVERSE[simp]:
2694 !ls: 'a list. set (REVERSE ls) = set ls
2695Proof
2696 Induct THEN SRW_TAC [] [pred_setTheory.EXTENSION]
2697QED
2698
2699Theorem LIST_TO_SET_THM = LIST_TO_SET
2700Theorem LIST_TO_SET_MAP:
2701 !f l. LIST_TO_SET (MAP f l) = IMAGE f (LIST_TO_SET l)
2702Proof
2703Induct_on ‘l’ THEN
2704ASM_SIMP_TAC bool_ss [pred_setTheory.IMAGE_EMPTY, pred_setTheory.IMAGE_INSERT,
2705 MAP, LIST_TO_SET_THM]
2706QED
2707
2708Theorem LIST_TO_SET_FILTER:
2709 LIST_TO_SET (FILTER P l) = { x | P x } INTER LIST_TO_SET l
2710Proof
2711 SRW_TAC [] [pred_setTheory.EXTENSION, MEM_FILTER]
2712QED
2713
2714
2715(* ----------------------------------------------------------------------
2716 SET_TO_LIST : 'a set -> 'a list
2717
2718 Only defined if the set is finite; order of elements in list is
2719 unspecified.
2720 ---------------------------------------------------------------------- *)
2721
2722val SET_TO_LIST_defn = Lib.with_flag (Defn.def_suffix, "") Defn.Hol_defn
2723 "SET_TO_LIST"
2724 ‘SET_TO_LIST s =
2725 if FINITE s then
2726 if s={} then []
2727 else CHOICE s :: SET_TO_LIST (REST s)
2728 else ARB’;
2729
2730(*---------------------------------------------------------------------------
2731 Termination of SET_TO_LIST.
2732 ---------------------------------------------------------------------------*)
2733
2734val (SET_TO_LIST_EQN, SET_TO_LIST_IND) =
2735 Defn.tprove (SET_TO_LIST_defn,
2736 TotalDefn.WF_REL_TAC ‘measure CARD’ THEN
2737 PROVE_TAC [CARD_PSUBSET, REST_PSUBSET]);
2738
2739(*---------------------------------------------------------------------------
2740 Desired recursion equation.
2741
2742 FINITE s |- SET_TO_LIST s = if s = {} then []
2743 else CHOICE s::SET_TO_LIST (REST s)
2744
2745 ---------------------------------------------------------------------------*)
2746
2747Theorem SET_TO_LIST_THM =
2748 DISCH_ALL (ASM_REWRITE_RULE [ASSUME “FINITE s”] SET_TO_LIST_EQN);
2749
2750Theorem SET_TO_LIST_IND = SET_TO_LIST_IND;
2751
2752
2753
2754(*---------------------------------------------------------------------------
2755 Some consequences
2756 ---------------------------------------------------------------------------*)
2757
2758Theorem SET_TO_LIST_EMPTY[simp]:
2759 SET_TO_LIST {} = []
2760Proof
2761 SRW_TAC [] [SET_TO_LIST_THM]
2762QED
2763
2764Theorem SET_TO_LIST_EMPTY_IFF:
2765 !s. FINITE s ==>
2766 (SET_TO_LIST s = [] <=> s = {})
2767Proof
2768 ho_match_mp_tac FINITE_INDUCT \\ rw[SET_TO_LIST_THM]
2769QED
2770
2771Theorem SET_TO_LIST_INV:
2772 !s. FINITE s ==> (LIST_TO_SET(SET_TO_LIST s) = s)
2773Proof
2774 Induction.recInduct SET_TO_LIST_IND
2775 THEN RW_TAC bool_ss []
2776 THEN ONCE_REWRITE_TAC [UNDISCH SET_TO_LIST_THM]
2777 THEN RW_TAC bool_ss [LIST_TO_SET_THM]
2778 THEN PROVE_TAC [REST_DEF, FINITE_DELETE, CHOICE_INSERT_REST]
2779QED
2780
2781Theorem SET_TO_LIST_CARD:
2782 !s. FINITE s ==> (LENGTH (SET_TO_LIST s) = CARD s)
2783Proof
2784 Induction.recInduct SET_TO_LIST_IND
2785 THEN REPEAT STRIP_TAC
2786 THEN SRW_TAC [] [Once (UNDISCH SET_TO_LIST_THM)]
2787 THEN ‘FINITE (REST s)’ by METIS_TAC [REST_DEF, FINITE_DELETE]
2788 THEN ‘~(CARD s = 0)’ by METIS_TAC [CARD_EQ_0]
2789 THEN SRW_TAC [numSimps.ARITH_ss] [REST_DEF, CHOICE_DEF]
2790QED
2791
2792Theorem SET_TO_LIST_IN_MEM:
2793 !s. FINITE s ==> !x. x IN s <=> MEM x (SET_TO_LIST s)
2794Proof
2795 Induction.recInduct SET_TO_LIST_IND
2796 THEN RW_TAC bool_ss []
2797 THEN ONCE_REWRITE_TAC [UNDISCH SET_TO_LIST_THM]
2798 THEN RW_TAC bool_ss [MEM, NOT_IN_EMPTY]
2799 THEN PROVE_TAC [REST_DEF, FINITE_DELETE, IN_INSERT, CHOICE_INSERT_REST]
2800QED
2801
2802(* this version of the above is a more likely rewrite: a complicated LHS
2803 turns into a simple RHS *)
2804Theorem MEM_SET_TO_LIST[simp]:
2805 !s. FINITE s ==> !x. MEM x (SET_TO_LIST s) <=> x IN s
2806Proof METIS_TAC [SET_TO_LIST_IN_MEM]
2807QED
2808
2809Theorem SET_TO_LIST_SING[simp]:
2810 SET_TO_LIST {x} = [x]
2811Proof
2812 SRW_TAC [] [SET_TO_LIST_THM]
2813QED
2814
2815Theorem LIST_TO_SET_TAKE:
2816 !i l. set (TAKE i l) SUBSET set l
2817Proof
2818 simp[SUBSET_DEF] >> Induct_on ‘l’ >> simp[] >>
2819 Cases_on ‘i’ >> simp[DISJ_IMP_THM] >> metis_tac[]
2820QED
2821
2822Theorem LIST_TO_SET_DROP:
2823 !i l. set (DROP i l) SUBSET set l
2824Proof
2825 simp[SUBSET_DEF] >> Induct_on ‘l’ >> simp[] >>
2826 Cases_on ‘i’ >> simp[DISJ_IMP_THM] >> metis_tac[]
2827QED
2828
2829val op >>~- = Q.>>~-
2830val op >~ = Q.>~
2831
2832
2833Theorem ALL_DISTINCT_SET_TO_LIST[simp]:
2834 !s. FINITE s ==> ALL_DISTINCT (SET_TO_LIST s)
2835Proof
2836 Induction.recInduct SET_TO_LIST_IND THEN
2837 REPEAT STRIP_TAC THEN
2838 IMP_RES_TAC SET_TO_LIST_THM THEN
2839 ‘FINITE (REST s)’ by PROVE_TAC[pred_setTheory.FINITE_DELETE,
2840 pred_setTheory.REST_DEF] THEN
2841 Cases_on ‘s = EMPTY’ THEN
2842 FULL_SIMP_TAC bool_ss [ALL_DISTINCT, MEM_SET_TO_LIST,
2843 pred_setTheory.CHOICE_NOT_IN_REST]
2844QED
2845
2846Theorem ITSET_eq_FOLDL_SET_TO_LIST:
2847 !s. FINITE s ==> !f a. ITSET f s a = FOLDL (combin$C f) a (SET_TO_LIST s)
2848Proof
2849HO_MATCH_MP_TAC pred_setTheory.FINITE_COMPLETE_INDUCTION THEN
2850SRW_TAC [] [pred_setTheory.ITSET_THM, SET_TO_LIST_THM, FOLDL]
2851QED
2852
2853Theorem LIST_TO_SET_SING :
2854 !vs x. ALL_DISTINCT vs /\ set vs = {x} <=> vs = [x]
2855Proof
2856 rpt GEN_TAC >> reverse EQ_TAC >- rw []
2857 (* necessary case analysis, to use ALL_DISTINCT *)
2858 >> Cases_on ‘vs’ >> rw []
2859 >- (fs [Once EXTENSION] >> METIS_TAC [])
2860 >> Q_TAC KNOW_TAC ‘a = x’
2861 >- (fs [Once EXTENSION] >> METIS_TAC [])
2862 >> DISCH_THEN (fn th => fs [th])
2863 >> Cases_on ‘set l = {}’ >- fs []
2864 >> ‘?y. y IN set l’ by METIS_TAC [MEMBER_NOT_EMPTY]
2865 >> Cases_on ‘x = y’ >- PROVE_TAC []
2866 >> fs [Once EXTENSION]
2867 >> METIS_TAC []
2868QED
2869
2870(* ----------------------------------------------------------------------
2871 FINITE set of lists
2872 ---------------------------------------------------------------------- *)
2873
2874Theorem bounded_length_FINITE:
2875 FINITE (UNIV:'a set) ==>
2876 !m (s:'a list set). (!x. x IN s ==> LENGTH x <= m) ==> FINITE s
2877Proof
2878 strip_tac
2879 \\ ho_match_mp_tac numTheory.INDUCTION
2880 \\ rw[]
2881 >- (
2882 Cases_on`s` \\ fs[]
2883 \\ `x = []` by metis_tac[] \\ rw[]
2884 \\ Cases_on`t` \\ fs[] \\ metis_tac[] )
2885 \\ `s SUBSET
2886 [] INSERT BIGUNION (IMAGE (\f. IMAGE (f o TL) s) (IMAGE CONS UNIV))`
2887 by (rw[SUBSET_DEF, PULL_EXISTS]
2888 \\ res_tac
2889 \\ Cases_on`x` \\ fs[]
2890 \\ Q.EXISTS_TAC`a::l` \\ simp[] )
2891 \\ match_mp_tac (MP_CANON SUBSET_FINITE)
2892 \\ goal_assum(first_assum o mp_then Any mp_tac)
2893 \\ rewrite_tac[FINITE_INSERT]
2894 \\ match_mp_tac FINITE_BIGUNION
2895 \\ simp[PULL_EXISTS]
2896 \\ simp[IMAGE_COMPOSE]
2897 \\ first_x_assum match_mp_tac
2898 \\ Q.X_GEN_TAC`z`
2899 \\ rw[PULL_EXISTS]
2900 \\ res_tac
2901 \\ Cases_on`x`
2902 \\ full_simp_tac(arith_ss) []
2903QED
2904
2905(* ----------------------------------------------------------------------
2906 isPREFIX
2907 ---------------------------------------------------------------------- *)
2908
2909Definition isPREFIX[simp]:
2910 (isPREFIX [] l = T) /\
2911 (isPREFIX (h::t) l = case l of [] => F
2912 | h'::t' => (h = h') /\ isPREFIX t t')
2913End
2914
2915Overload "<<=" = “isPREFIX”
2916
2917(* type annotations are there solely to make theorem have only one
2918 type variable; without them the theorem ends up with three (because the
2919 three clauses are independent). *)
2920Theorem isPREFIX_THM[simp]:
2921 (([]:'a list) <<= l <=> T) /\
2922 ((h::t:'a list) <<= [] <=> F) /\
2923 ((h1::t1:'a list) <<= h2::t2 <=> (h1 = h2) /\ isPREFIX t1 t2)
2924Proof
2925 SRW_TAC [] []
2926QED
2927
2928Theorem isPREFIX_NILR[simp]:
2929 x <<= [] <=> (x = [])
2930Proof
2931 Cases_on ‘x’ >> simp[]
2932QED
2933
2934Theorem isPREFIX_CONSR:
2935 x <<= y::ys <=> (x = []) \/ ?xs. (x = y::xs) /\ xs <<= ys
2936Proof
2937 Cases_on ‘x’ >> simp[]
2938QED
2939
2940(* ----------------------------------------------------------------------
2941 SNOC
2942 ---------------------------------------------------------------------- *)
2943
2944Definition SNOC[simp]:
2945 (SNOC x [] = [x]) /\
2946 (SNOC x (CONS x' l) = CONS x' (SNOC x l))
2947End
2948
2949Theorem SNOC_NIL = SNOC |> CONJUNCT1;
2950(* > val SNOC_NIL = |- !x. SNOC x [] = [x]: thm *)
2951Theorem SNOC_CONS = SNOC |> CONJUNCT2;
2952(* > val SNOC_CONS = |- !x x' l. SNOC x (x'::l) = x'::SNOC x l: thm *)
2953
2954Theorem LENGTH_SNOC[simp]:
2955 !(x:'a) l. LENGTH (SNOC x l) = SUC (LENGTH l)
2956Proof
2957 GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [LENGTH, SNOC]
2958QED
2959
2960Theorem LAST_SNOC[simp]:
2961 !x:'a l. LAST (SNOC x l) = x
2962Proof
2963 GEN_TAC THEN LIST_INDUCT_TAC THEN
2964 RW_TAC bool_ss [SNOC, LAST_DEF] THEN
2965 POP_ASSUM MP_TAC THEN
2966 Q.SPEC_THEN ‘l’ STRUCT_CASES_TAC list_CASES THEN
2967 RW_TAC bool_ss [SNOC]
2968QED
2969
2970Theorem FRONT_SNOC[simp]:
2971 !x:'a l. FRONT (SNOC x l) = l
2972Proof
2973 GEN_TAC THEN LIST_INDUCT_TAC THEN
2974 RW_TAC bool_ss [SNOC, FRONT_DEF] THEN
2975 POP_ASSUM MP_TAC THEN
2976 Q.SPEC_THEN ‘l’ STRUCT_CASES_TAC list_CASES THEN
2977 RW_TAC bool_ss [SNOC]
2978QED
2979
2980(* NOTE: Do NOT put [simp] here! *)
2981Theorem SNOC_APPEND:
2982 !x (l:('a) list). SNOC x l = APPEND l [x]
2983Proof
2984 GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [SNOC, APPEND]
2985QED
2986
2987(* |- !l. l <> [] ==> SNOC (LAST l) (FRONT l) = l *)
2988Theorem SNOC_LAST_FRONT =
2989 REWRITE_RULE [GSYM SNOC_APPEND] APPEND_FRONT_LAST
2990
2991Theorem LIST_TO_SET_SNOC:
2992 set (SNOC x ls) = x INSERT set ls
2993Proof
2994 Induct_on ‘ls’ THEN SRW_TAC [] [INSERT_COMM]
2995QED
2996
2997Theorem MAP_SNOC:
2998 !(f:'a->'b) x (l:'a list). MAP f(SNOC x l) = SNOC(f x)(MAP f l)
2999Proof
3000 (REWRITE_TAC [SNOC_APPEND, MAP_APPEND, MAP])
3001QED
3002
3003Theorem EL_SNOC:
3004 !n (l:'a list). n < (LENGTH l) ==> (!x. EL n (SNOC x l) = EL n l)
3005Proof
3006 INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH, NOT_LESS_0]
3007 THENL[
3008 REWRITE_TAC[SNOC, EL, HD],
3009 REWRITE_TAC[SNOC, EL, TL, LESS_MONO_EQ]
3010 THEN FIRST_ASSUM MATCH_ACCEPT_TAC]
3011QED
3012
3013Theorem EL_LENGTH_SNOC:
3014 !l:'a list. !x. EL (LENGTH l) (SNOC x l) = x
3015Proof
3016 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[EL, SNOC, HD, TL, LENGTH]
3017QED
3018
3019Theorem APPEND_SNOC[simp] :
3020 !l1 (x:'a) l2. APPEND l1 (SNOC x l2) = SNOC x (APPEND l1 l2)
3021Proof
3022 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[APPEND, SNOC]
3023QED
3024
3025Theorem EVERY_SNOC[simp] :
3026 !P (x:'a) l. EVERY P (SNOC x l) <=> EVERY P l /\ P x
3027Proof
3028 GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC
3029 THEN ASM_REWRITE_TAC[SNOC, EVERY_DEF, CONJ_ASSOC]
3030QED
3031
3032Theorem EXISTS_SNOC:
3033 !P (x:'a) l. EXISTS P (SNOC x l) <=> P x \/ (EXISTS P l)
3034Proof
3035 GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC
3036 THEN ASM_REWRITE_TAC[SNOC, EXISTS_DEF] THEN GEN_TAC
3037 THEN PURE_ONCE_REWRITE_TAC[DISJ_ASSOC]
3038 THEN CONV_TAC ((RAND_CONV o RATOR_CONV o ONCE_DEPTH_CONV)
3039 (REWR_CONV DISJ_SYM)) THEN REFL_TAC
3040QED
3041
3042Theorem MEM_SNOC[simp]:
3043 !(y:'a) x l. MEM y (SNOC x l) <=> (y = x) \/ MEM y l
3044Proof
3045 GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC
3046 THEN ASM_REWRITE_TAC[SNOC, MEM] THEN GEN_TAC
3047 THEN PURE_ONCE_REWRITE_TAC[DISJ_ASSOC]
3048 THEN CONV_TAC ((RAND_CONV o RATOR_CONV o ONCE_DEPTH_CONV)
3049 (REWR_CONV DISJ_SYM)) THEN REFL_TAC
3050QED
3051
3052Theorem SNOC_11[simp]:
3053 !x y a b. (SNOC x y = SNOC a b) <=> (x = a) /\ (y = b)
3054Proof
3055 SRW_TAC [] [EQ_IMP_THM] THENL [
3056 POP_ASSUM (MP_TAC o Q.AP_TERM ‘LAST’) THEN SRW_TAC [] [LAST_SNOC],
3057 POP_ASSUM (MP_TAC o Q.AP_TERM ‘FRONT’) THEN SRW_TAC [] [FRONT_SNOC]
3058 ]
3059QED
3060
3061Theorem REVERSE_SNOC_DEF:
3062 (REVERSE [] = []) /\
3063 (!x:'a l. REVERSE (x::l) = SNOC x (REVERSE l))
3064Proof
3065 REWRITE_TAC [REVERSE_DEF, SNOC_APPEND]
3066QED
3067
3068Theorem REVERSE_SNOC:
3069 !(x:'a) l. REVERSE (SNOC x l) = CONS x (REVERSE l)
3070Proof
3071 GEN_TAC THEN LIST_INDUCT_TAC
3072 THEN ASM_REWRITE_TAC[SNOC, REVERSE_SNOC_DEF]
3073QED
3074
3075val forall_REVERSE = TAC_PROOF(([],
3076 (“!P. (!l:('a)list. P(REVERSE l)) = (!l. P l)”)),
3077 GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN GEN_TAC
3078 THEN POP_ASSUM (ACCEPT_TAC o (REWRITE_RULE[REVERSE_REVERSE]
3079 o (SPEC (“REVERSE l:('a)list”)))));
3080
3081val f_REVERSE_lemma = TAC_PROOF (([],
3082 (“!f1 f2.
3083 ((\x. (f1:('a)list->'b) (REVERSE x)) = (\x. f2 (REVERSE x))) = (f1 = f2)”)),
3084 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL[
3085 POP_ASSUM (fn x => ACCEPT_TAC (EXT (REWRITE_RULE[REVERSE_REVERSE]
3086 (GEN (“x:('a)list”) (BETA_RULE (AP_THM x (“REVERSE (x:('a)list)”))))))),
3087 ASM_REWRITE_TAC[]]);
3088
3089Theorem SNOC_Axiom_old[local]:
3090 !(e:'b) (f:'b -> ('a -> (('a)list -> 'b))).
3091 ?! fn1.
3092 (fn1[] = e) /\
3093 (!x l. fn1(SNOC x l) = f(fn1 l)x l)
3094Proof
3095
3096 let val lemma = CONV_RULE (EXISTS_UNIQUE_CONV)
3097 (REWRITE_RULE[REVERSE_REVERSE] (BETA_RULE (SPECL
3098 [“e:'b”,“(\ft x l. f ft x (REVERSE l)):'b -> ('a -> (('a)list -> 'b))”]
3099 (PURE_ONCE_REWRITE_RULE
3100 [SYM (CONJUNCT1 REVERSE_DEF),
3101 PURE_ONCE_REWRITE_RULE[SYM (SPEC_ALL REVERSE_SNOC)]
3102 (BETA_RULE (SPEC (“\l:('a)list.fn1(CONS x l) =
3103 (f:'b -> ('a -> (('a)list -> 'b)))(fn1 l)x l”)
3104 (CONV_RULE (ONCE_DEPTH_CONV SYM_CONV) forall_REVERSE)))]
3105 list_Axiom_old))))
3106 in
3107 REPEAT GEN_TAC THEN CONV_TAC EXISTS_UNIQUE_CONV
3108 THEN STRIP_ASSUME_TAC lemma THEN CONJ_TAC THENL
3109 [
3110 EXISTS_TAC (“(fn1:('a)list->'b) o REVERSE”)
3111 THEN REWRITE_TAC[o_DEF] THEN BETA_TAC THEN ASM_REWRITE_TAC[],
3112
3113 REPEAT GEN_TAC THEN
3114 POP_ASSUM (ACCEPT_TAC o SPEC_ALL o
3115 REWRITE_RULE[REVERSE_REVERSE, f_REVERSE_lemma] o
3116 BETA_RULE o REWRITE_RULE[o_DEF] o
3117 SPECL [“(fn1' o REVERSE):('a)list->'b”,
3118 “(fn1'' o REVERSE):('a)list->'b”])
3119 ]
3120 end
3121QED
3122
3123Theorem SNOC_Axiom:
3124 !e f. ?fn:'a list -> 'b.
3125 (fn [] = e) /\
3126 (!x l. fn (SNOC x l) = f x l (fn l))
3127Proof
3128 REPEAT GEN_TAC THEN
3129 STRIP_ASSUME_TAC (CONV_RULE EXISTS_UNIQUE_CONV
3130 (BETA_RULE
3131 (Q.SPECL [‘e’, ‘\x y z. f y z x’] SNOC_Axiom_old))) THEN
3132 Q.EXISTS_TAC ‘fn1’ THEN ASM_REWRITE_TAC []
3133QED
3134
3135Theorem SNOC_INDUCT = prove_induction_thm SNOC_Axiom_old;
3136Theorem SNOC_CASES = hd (prove_cases_thm SNOC_INDUCT);
3137
3138(* cf. rich_listTheory.IS_PREFIX_SNOC *)
3139Theorem isPREFIX_SNOC[simp] :
3140 l <<= SNOC x l
3141Proof
3142 Induct_on ‘l’ >> rw [SNOC, isPREFIX]
3143QED
3144
3145local val REVERSE = REVERSE_SNOC_DEF
3146in
3147Theorem MAP_REVERSE:
3148 !f l. MAP f (REVERSE l) = REVERSE (MAP f l)
3149Proof
3150 GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [REVERSE, MAP, MAP_SNOC]
3151QED
3152end;
3153
3154(*--------------------------------------------------------------*)
3155(* List generator *)
3156(* GENLIST f n = [f 0;...; f(n-1)] *)
3157(*--------------------------------------------------------------*)
3158
3159Definition GENLIST:
3160 GENLIST (f:num->'a) 0 = [] /\
3161 GENLIST f (SUC n) = SNOC (f n) (GENLIST f n)
3162End
3163
3164Theorem LENGTH_GENLIST[simp]:
3165 !(f:num->'a) n. LENGTH(GENLIST f n) = n
3166Proof
3167 GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[GENLIST, LENGTH, LENGTH_SNOC]
3168QED
3169
3170Definition GENLIST_AUX:
3171 (GENLIST_AUX f 0 l = l) /\
3172 (GENLIST_AUX f (SUC n) l = GENLIST_AUX f n ((f n)::l))
3173End
3174val _ = export_rewrites ["GENLIST_AUX_compute"]
3175
3176(*---------------------------------------------------------------------------
3177 List padding (left and right)
3178 ---------------------------------------------------------------------------*)
3179
3180Definition PAD_LEFT:
3181 PAD_LEFT c n s = (GENLIST (K c) (n - LENGTH s)) ++ s
3182End
3183
3184Definition PAD_RIGHT:
3185 PAD_RIGHT c n s = s ++ (GENLIST (K c) (n - LENGTH s))
3186End
3187
3188(*---------------------------------------------------------------------------
3189 Theorems about genlist. From Anthony Fox's theories. Added by Thomas Tuerk.
3190 Moved from rich_listTheory.
3191 ---------------------------------------------------------------------------*)
3192
3193Theorem MAP_GENLIST:
3194 !f g n. MAP f (GENLIST g n) = GENLIST (f o g) n
3195Proof
3196 Induct_on ‘n’
3197 THEN ASM_SIMP_TAC arith_ss [GENLIST, MAP_SNOC, MAP, o_THM]
3198QED
3199
3200Theorem EL_GENLIST[simp]:
3201 !f n x. x < n ==> (EL x (GENLIST f n) = f x)
3202Proof
3203 Induct_on ‘n’ THEN1 SIMP_TAC arith_ss [] THEN
3204 REPEAT STRIP_TAC THEN REWRITE_TAC [GENLIST] THEN
3205 Cases_on ‘x < n’ THEN
3206 POP_ASSUM (fn th => ASSUME_TAC
3207 (SUBS [(GSYM o Q.SPECL [‘f’,‘n’]) LENGTH_GENLIST] th) THEN
3208 ASSUME_TAC th) THEN1 (
3209 ASM_SIMP_TAC bool_ss [EL_SNOC]
3210 ) THEN
3211 ‘x = LENGTH (GENLIST f n)’ by FULL_SIMP_TAC arith_ss [LENGTH_GENLIST] THEN
3212 ASM_SIMP_TAC bool_ss [EL_LENGTH_SNOC] THEN
3213 REWRITE_TAC [LENGTH_GENLIST]
3214QED
3215
3216Theorem HD_GENLIST =
3217 (SIMP_RULE arith_ss [EL] o Q.SPECL [‘f’,‘SUC n’,‘0’]) EL_GENLIST;
3218
3219Theorem HD_GENLIST_COR:
3220 !n f. 0 < n ==> (HD (GENLIST f n) = f 0)
3221Proof
3222 Cases THEN REWRITE_TAC [prim_recTheory.LESS_REFL, HD_GENLIST]
3223QED
3224
3225Theorem GENLIST_FUN_EQ:
3226 !n f g. (GENLIST f n = GENLIST g n) = (!x. x < n ==> (f x = g x))
3227Proof
3228 SIMP_TAC bool_ss [LIST_EQ_REWRITE, LENGTH_GENLIST, EL_GENLIST]
3229QED
3230
3231Theorem GENLIST_APPEND:
3232 !f a b. GENLIST f (a + b) = (GENLIST f b) ++ (GENLIST (\t. f (t + b)) a)
3233Proof
3234 Induct_on ‘a’ THEN
3235 ASM_SIMP_TAC arith_ss
3236 [GENLIST, APPEND_SNOC, APPEND_NIL, arithmeticTheory.ADD_CLAUSES]
3237QED
3238
3239Theorem EVERY_GENLIST:
3240 !n. EVERY P (GENLIST f n) = (!i. i < n ==> P (f i))
3241Proof
3242 Induct_on ‘n’ THEN ASM_SIMP_TAC arith_ss [GENLIST, EVERY_SNOC, EVERY_DEF]
3243 THEN metisLib.METIS_TAC [prim_recTheory.LESS_THM]
3244QED
3245
3246Theorem EXISTS_GENLIST:
3247 !n. EXISTS P (GENLIST f n) = (?i. i < n /\ P (f i))
3248Proof
3249 Induct_on ‘n’ THEN RW_TAC arith_ss [GENLIST, EXISTS_SNOC, EXISTS_DEF]
3250 THEN metisLib.METIS_TAC [prim_recTheory.LESS_THM]
3251QED
3252
3253Theorem TL_GENLIST:
3254 !f n. TL (GENLIST f (SUC n)) = GENLIST (f o SUC) n
3255Proof
3256 REPEAT STRIP_TAC THEN MATCH_MP_TAC LIST_EQ
3257 THEN SRW_TAC [] [EL_GENLIST, LENGTH_GENLIST, LENGTH_TL]
3258 THEN ONCE_REWRITE_TAC [EL |> CONJUNCT2 |> GSYM]
3259 THEN ‘SUC x < SUC n’ by numLib.DECIDE_TAC
3260 THEN IMP_RES_TAC EL_GENLIST
3261 THEN ASM_SIMP_TAC arith_ss []
3262QED
3263
3264Theorem ZIP_GENLIST:
3265 !l f n. (LENGTH l = n) ==>
3266 (ZIP (l,GENLIST f n) = GENLIST (\x. (EL x l,f x)) n)
3267Proof
3268 REPEAT STRIP_TAC THEN
3269 ‘LENGTH (ZIP (l,GENLIST f n)) = LENGTH (GENLIST (\x. (EL x l,f x)) n)’
3270 by ASM_SIMP_TAC arith_ss [LENGTH_GENLIST, LENGTH_ZIP] THEN
3271 ASM_SIMP_TAC arith_ss [LIST_EQ_REWRITE, LENGTH_GENLIST, LENGTH_ZIP,
3272 EL_ZIP, EL_GENLIST]
3273QED
3274
3275Theorem GENLIST_CONS:
3276 GENLIST f (SUC n) = f 0 :: (GENLIST (f o SUC) n)
3277Proof
3278 Induct_on ‘n’ THEN SRW_TAC [] [GENLIST, SNOC]
3279QED
3280
3281Theorem GENLIST_ID:
3282 !x. GENLIST (\i. EL i x) (LENGTH x) = x
3283Proof
3284 Induct >> simp[GENLIST_CONS, GENLIST, combinTheory.o_ABS_L]
3285QED
3286
3287Theorem NULL_GENLIST[simp]:
3288 !n f. NULL (GENLIST f n) = (n = 0)
3289Proof
3290 Cases THEN
3291 REWRITE_TAC [numTheory.NOT_SUC, NULL_DEF, CONJUNCT1 GENLIST, GENLIST_CONS]
3292QED
3293
3294Theorem GENLIST_AUX_lem[local]:
3295 !n l1 l2. GENLIST_AUX f n l1 ++ l2 = GENLIST_AUX f n (l1 ++ l2)
3296Proof
3297 Induct_on ‘n’ THEN SRW_TAC [] [GENLIST_AUX]
3298QED
3299
3300Theorem GENLIST_GENLIST_AUX:
3301 !n. GENLIST f n = GENLIST_AUX f n []
3302Proof
3303 Induct_on ‘n’
3304 THEN RW_TAC bool_ss
3305 [SNOC_APPEND, APPEND, GENLIST_AUX, GENLIST_AUX_lem, GENLIST]
3306QED
3307
3308Theorem GENLIST_NUMERALS[simp]:
3309 (GENLIST f 0 = []) /\
3310 (GENLIST f (NUMERAL n) = GENLIST_AUX f (NUMERAL n) [])
3311Proof
3312 REWRITE_TAC [GENLIST_GENLIST_AUX, GENLIST_AUX]
3313QED
3314
3315(* Theorem: GENLIST f 0 = [] *)
3316(* Proof: by GENLIST *)
3317Theorem GENLIST_0:
3318 !f. GENLIST f 0 = []
3319Proof
3320 rw[]
3321QED
3322
3323(* Theorem: GENLIST f 1 = [f 0] *)
3324(* Proof:
3325 GENLIST f 1
3326 = GENLIST f (SUC 0) by ONE
3327 = SNOC (f 0) (GENLIST f 0) by GENLIST
3328 = SNOC (f 0) [] by GENLIST
3329 = [f 0] by SNOC
3330*)
3331Theorem GENLIST_1:
3332 !f. GENLIST f 1 = [f 0]
3333Proof
3334 rw[]
3335QED
3336
3337Theorem MEM_GENLIST:
3338 MEM x (GENLIST f n) <=> ?m. m < n /\ (x = f m)
3339Proof
3340SRW_TAC [] [MEM_EL, EL_GENLIST, EQ_IMP_THM] THEN
3341PROVE_TAC [EL_GENLIST]
3342QED
3343
3344Theorem ALL_DISTINCT_SNOC:
3345 !x l. ALL_DISTINCT (SNOC x l) <=> ~MEM x l /\ ALL_DISTINCT l
3346Proof SRW_TAC [] [SNOC_APPEND, ALL_DISTINCT_APPEND] THEN PROVE_TAC[]
3347QED
3348
3349Theorem ALL_DISTINCT_GENLIST:
3350 ALL_DISTINCT (GENLIST f n) <=>
3351 (!m1 m2. m1 < n /\ m2 < n /\ (f m1 = f m2) ==> (m1 = m2))
3352Proof
3353 Induct_on `n` THEN
3354 SRW_TAC [] [GENLIST, ALL_DISTINCT_SNOC, MEM_EL] THEN
3355 SRW_TAC [] [EQ_IMP_THM] THEN1 (
3356 IMP_RES_TAC prim_recTheory.LESS_SUC_IMP THEN
3357 Cases_on `m1 = n` THEN Cases_on `m2 = n` THEN SRW_TAC [] [] THEN
3358 FULL_SIMP_TAC (srw_ss()) [] THEN1 (
3359 NTAC 2 (FIRST_X_ASSUM (Q.SPEC_THEN `m2` MP_TAC)) THEN
3360 SRW_TAC [] [] ) THEN
3361 NTAC 2 (FIRST_X_ASSUM (Q.SPEC_THEN `m1` MP_TAC)) THEN
3362 SRW_TAC [] [] )
3363 THEN1 (Q.RENAME_TAC [‘~(m < n)’, ‘f n = EL m (GENLIST f n)’] THEN
3364 STRIP_TAC THEN
3365 FIRST_X_ASSUM (Q.SPECL_THEN [`m`,`n`] MP_TAC) THEN
3366 SRW_TAC [] [prim_recTheory.LESS_SUC] THEN
3367 METIS_TAC [prim_recTheory.LESS_REFL] ) THEN
3368 METIS_TAC [prim_recTheory.LESS_SUC]
3369QED
3370
3371Theorem TAKE_GENLIST:
3372 TAKE n (GENLIST f m) = GENLIST f (MIN n m)
3373Proof
3374 SRW_TAC[numSimps.ARITH_ss][LIST_EQ_REWRITE, LENGTH_TAKE_EQ,
3375 arithmeticTheory.MIN_DEF, EL_TAKE]
3376QED
3377
3378Theorem DROP_GENLIST:
3379 DROP n (GENLIST f m) = GENLIST (f o (+) n) (m-n)
3380Proof
3381 SRW_TAC[numSimps.ARITH_ss][LIST_EQ_REWRITE,EL_DROP]
3382QED
3383
3384Theorem GENLIST_CONG[defncong]:
3385 !n1 n2 f1 f2.
3386 n1 = n2 /\ (!m. m < n2 ==> f1 m = f2 m) ==> GENLIST f1 n1 = GENLIST f2 n2
3387Proof
3388 simp[] >>
3389 Prim_rec.INDUCT_THEN (TypeBase.induction_of “:num”) strip_assume_tac >>
3390 simp[GENLIST_CONS]
3391QED
3392
3393(* Theorem alias *)
3394Theorem GENLIST_EQ =
3395 GENLIST_CONG |> GEN ``n:num`` |> GEN ``f2:num -> 'a``
3396 |> GEN ``f1:num -> 'a``;
3397(*
3398val GENLIST_EQ = |- !f1 f2 n. (!m. m < n ==> f1 m = f2 m) ==> GENLIST f1 n = GENLIST f2 n: thm
3399*)
3400
3401Theorem LIST_REL_O:
3402 !R1 R2. LIST_REL (R1 O R2) = LIST_REL R1 O LIST_REL R2
3403Proof
3404 simp[FUN_EQ_THM, O_DEF, LIST_REL_EL_EQN, EQ_IMP_THM] >> rw[]
3405 >- (full_simp_tac(srw_ss())[GSYM RIGHT_EXISTS_IMP_THM,SKOLEM_THM] >>
3406 Q.RENAME_TAC [‘LENGTH as = LENGTH cs’, ‘R2 (EL _ as) (f _)’,
3407 ‘R1 (f _) (EL _ cs)’] >>
3408 Q.EXISTS_TAC‘GENLIST f (LENGTH cs)’ >> simp[])
3409 >- simp[]
3410 >- metis_tac[]
3411QED
3412
3413(* Theorem: (GENLIST f n = []) <=> (n = 0) *)
3414(* Proof:
3415 If part: GENLIST f n = [] ==> n = 0
3416 By contradiction, suppose n <> 0.
3417 Then LENGTH (GENLIST f n) = n <> 0 by LENGTH_GENLIST
3418 This contradicts LENGTH [] = 0.
3419 Only-if part: GENLIST f 0 = [], true by GENLIST_0
3420*)
3421Theorem GENLIST_EQ_NIL:
3422 !f n. (GENLIST f n = []) <=> (n = 0)
3423Proof
3424 rw[EQ_IMP_THM] >>
3425 metis_tac[LENGTH_GENLIST, LENGTH_NIL]
3426QED
3427
3428(* Theorem: LAST (GENLIST f (SUC n)) = f n *)
3429(* Proof:
3430 LAST (GENLIST f (SUC n))
3431 = LAST (SNOC (f n) (GENLIST f n)) by GENLIST
3432 = f n by LAST_SNOC
3433*)
3434Theorem GENLIST_LAST:
3435 !f n. LAST (GENLIST f (SUC n)) = f n
3436Proof
3437 rw[GENLIST]
3438QED
3439
3440(* Note:
3441
3442- EVERY_MAP;
3443> val it = |- !P f l. EVERY P (MAP f l) <=> EVERY (\x. P (f x)) l : thm
3444- EVERY_GENLIST;
3445> val it = |- !n. EVERY P (GENLIST f n) <=> !i. i < n ==> P (f i) : thm
3446- MAP_GENLIST;
3447> val it = |- !f g n. MAP f (GENLIST g n) = GENLIST (f o g) n : thm
3448*)
3449
3450(* Note: the following can use EVERY_GENLIST. *)
3451
3452(* Theorem: !k. (k < n ==> f k = c) <=> EVERY (\x. x = c) (GENLIST f n) *)
3453(* Proof: by induction on n.
3454 Base case: !c. (!k. k < 0 ==> (f k = c)) <=> EVERY (\x. x = c) (GENLIST f 0)
3455 Since GENLIST f 0 = [], this is true as no k < 0.
3456 Step case: (!k. k < n ==> (f k = c)) <=> EVERY (\x. x = c) (GENLIST f n) ==>
3457 (!k. k < SUC n ==> (f k = c)) <=> EVERY (\x. x = c) (GENLIST f (SUC n))
3458 EVERY (\x. x = c) (GENLIST f (SUC n))
3459 <=> EVERY (\x. x = c) (SNOC (f n) (GENLIST f n)) by GENLIST
3460 <=> EVERY (\x. x = c) (GENLIST f n) /\ (f n = c) by EVERY_SNOC
3461 <=> (!k. k < n ==> (f k = c)) /\ (f n = c) by induction hypothesis
3462 <=> !k. k < SUC n ==> (f k = c)
3463*)
3464Theorem GENLIST_CONSTANT:
3465 !f n c. (!k. k < n ==> (f k = c)) <=> EVERY (\x. x = c) (GENLIST f n)
3466Proof
3467 strip_tac >>
3468 Induct_on ‘n’ >-
3469 rw[] >>
3470 rw_tac std_ss[EVERY_DEF, GENLIST, EVERY_SNOC, EQ_IMP_THM] >-
3471 metis_tac[prim_recTheory.LESS_SUC] >>
3472 Cases_on `k = n` >-
3473 rw_tac std_ss[] >>
3474 metis_tac[prim_recTheory.LESS_THM]
3475QED
3476
3477Theorem isPREFIX_NIL :
3478 !x. [] <<= x /\ (x <<= [] <=> (x = []))
3479Proof
3480 qx_gen_tac ‘x’
3481 >> Cases_on ‘x’ >- rw []
3482 >> rw [isPREFIX]
3483QED
3484
3485Theorem isPREFIX_REFL :
3486 !x. x <<= x
3487Proof
3488 Induct_on ‘x’ >> rw [isPREFIX]
3489QED
3490
3491Theorem isPREFIX_TRANS :
3492 !x y z. x <<= y /\ y <<= z ==> x <<= z
3493Proof
3494 Induct_on ‘x’ >- rw []
3495 >> rpt GEN_TAC
3496 >> Cases_on ‘y’ >- rw []
3497 >> Cases_on ‘z’ >- rw []
3498 >> rw []
3499 >> FIRST_X_ASSUM MATCH_MP_TAC
3500 >> Q.EXISTS_TAC ‘l’ >> rw []
3501QED
3502
3503Theorem isPREFIX_ANTISYM :
3504 !x y. x <<= y /\ y <<= x ==> x = y
3505Proof
3506 Induct_on ‘x’ >- rw []
3507 >> rpt GEN_TAC
3508 >> Cases_on ‘y’ >- rw []
3509 >> STRIP_TAC
3510 >> rw []
3511 >> fs []
3512QED
3513
3514Theorem isPREFIX_SNOC_EQ :
3515 !x y z. z <<= SNOC x y <=> z <<= y \/ z = SNOC x y
3516Proof
3517 NTAC 2 GEN_TAC
3518 >> Q.ID_SPEC_TAC `x`
3519 >> Q.ID_SPEC_TAC `y`
3520 >> INDUCT_THEN list_INDUCT ASSUME_TAC
3521 >- (rpt GEN_TAC \\
3522 MP_TAC (Q.SPEC `z` list_CASES) \\
3523 STRIP_TAC \\
3524 rw [SNOC, isPREFIX_NIL, isPREFIX, CONS_11, NOT_CONS_NIL])
3525 >> rpt GEN_TAC
3526 >> MP_TAC (Q.SPEC `z` list_CASES)
3527 >> STRIP_TAC
3528 >> rw [SNOC, isPREFIX_NIL, isPREFIX, CONS_11, NOT_CONS_NIL]
3529 >> PROVE_TAC []
3530QED
3531
3532Theorem isPREFIX_GENLIST_lemma[local] :
3533 !f m n. m <= n ==> GENLIST f m <<= GENLIST f n
3534Proof
3535 qx_gen_tac ‘f’
3536 >> Induct_on ‘n’ >- rw []
3537 >> rpt STRIP_TAC
3538 >> ‘m = SUC n \/ m <= n’ by METIS_TAC [LE]
3539 >- rw [isPREFIX_REFL]
3540 >> MATCH_MP_TAC isPREFIX_TRANS
3541 >> Q.EXISTS_TAC ‘GENLIST f n’ >> rw []
3542 >> rw [GENLIST, isPREFIX_SNOC]
3543QED
3544
3545Theorem isPREFIX_GENLIST :
3546 !(f :num -> 'a) m n. GENLIST f m <<= GENLIST f n <=> m <= n
3547Proof
3548 rpt GEN_TAC
3549 >> reverse EQ_TAC
3550 >- rw [isPREFIX_GENLIST_lemma]
3551 >> qid_spec_tac ‘m’
3552 >> qid_spec_tac ‘n’
3553 >> Induct_on ‘n’
3554 >- (rw [] >> fs [GENLIST_EQ_NIL])
3555 >> GEN_TAC
3556 >> simp [GENLIST, isPREFIX_SNOC_EQ]
3557 >> STRIP_TAC
3558 >- (MATCH_MP_TAC LESS_EQ_TRANS \\
3559 Q.EXISTS_TAC ‘n’ >> rw [])
3560 >> fs [LIST_EQ_REWRITE]
3561QED
3562
3563Theorem isPREFIX_MAP :
3564 !f l1 l2. l1 <<= l2 ==> MAP f l1 <<= MAP f l2
3565Proof
3566 qx_gen_tac ‘f’
3567 >> Induct_on ‘l1’ >- rw []
3568 >> rpt STRIP_TAC
3569 >> Cases_on ‘l2’ >- fs []
3570 >> fs []
3571QED
3572
3573(* ---------------------------------------------------------------------- *)
3574
3575Theorem FOLDL_SNOC:
3576 !(f:'b->'a->'b) e x l. FOLDL f e (SNOC x l) = f (FOLDL f e l) x
3577Proof
3578 let val lem = prove(
3579 (“!l (f:'b->'a->'b) e x. FOLDL f e (SNOC x l) = f (FOLDL f e l) x”),
3580 LIST_INDUCT_TAC THEN REWRITE_TAC[SNOC, FOLDL]
3581 THEN REPEAT GEN_TAC THEN ASM_REWRITE_TAC[])
3582 in
3583 MATCH_ACCEPT_TAC lem
3584 end
3585QED
3586
3587local open arithmeticTheory in
3588Theorem SUM_SNOC:
3589 !x l. SUM (SNOC x l) = (SUM l) + x
3590Proof
3591 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[SUM, SNOC, ADD, ADD_0]
3592 THEN GEN_TAC THEN ASM_REWRITE_TAC[ADD_ASSOC]
3593QED
3594
3595Theorem SUM_APPEND:
3596 !l1 l2. SUM (APPEND l1 l2) = SUM l1 + SUM l2
3597Proof
3598 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[SUM, APPEND, ADD, ADD_0, ADD_ASSOC]
3599QED
3600end
3601
3602Theorem SUM_MAP_FOLDL:
3603 !ls. SUM (MAP f ls) = FOLDL (\a e. a + f e) 0 ls
3604Proof
3605HO_MATCH_MP_TAC SNOC_INDUCT THEN
3606SRW_TAC [] [FOLDL_SNOC, MAP_SNOC, SUM_SNOC, MAP, SUM, FOLDL]
3607QED
3608
3609Theorem SUM_IMAGE_eq_SUM_MAP_SET_TO_LIST:
3610 FINITE s ==> (SIGMA f s = SUM (MAP f (SET_TO_LIST s)))
3611Proof
3612SRW_TAC [] [SUM_IMAGE_DEF] THEN
3613SRW_TAC [] [ITSET_eq_FOLDL_SET_TO_LIST, SUM_MAP_FOLDL] THEN
3614AP_THM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
3615SRW_TAC [] [FUN_EQ_THM, arithmeticTheory.ADD_COMM]
3616QED
3617
3618val SNOC_INDUCT_TAC = INDUCT_THEN SNOC_INDUCT ASSUME_TAC;
3619
3620local open arithmeticTheory prim_recTheory in
3621Theorem EL_REVERSE:
3622 !n (l:'a list). n < (LENGTH l) ==>
3623 (EL n (REVERSE l) = EL (PRE(LENGTH l - n)) l)
3624Proof
3625 INDUCT_TAC THEN SNOC_INDUCT_TAC
3626 THEN ASM_REWRITE_TAC[LENGTH, LENGTH_SNOC,
3627 EL, HD, TL, NOT_LESS_0, LESS_MONO_EQ, SUB_0] THENL[
3628 REWRITE_TAC[REVERSE_SNOC, PRE, EL_LENGTH_SNOC, HD],
3629 REWRITE_TAC[REVERSE_SNOC, SUB_MONO_EQ, TL]
3630 THEN REPEAT STRIP_TAC THEN RES_THEN SUBST1_TAC
3631 THEN MATCH_MP_TAC (GSYM EL_SNOC)
3632 THEN REWRITE_TAC(PRE_SUB1 :: (map GSYM [SUB_PLUS, ADD1]))
3633 THEN numLib.DECIDE_TAC]
3634QED
3635end
3636
3637Theorem REVERSE_GENLIST:
3638 REVERSE (GENLIST f n) = GENLIST (\m. f (PRE n - m)) n
3639Proof
3640 MATCH_MP_TAC LIST_EQ THEN
3641 SRW_TAC [] [EL_REVERSE] THEN
3642 ‘PRE (n - x) < n’ by numLib.DECIDE_TAC THEN
3643 SRW_TAC [] [EL_GENLIST] THEN
3644 AP_TERM_TAC THEN numLib.DECIDE_TAC
3645QED
3646
3647Theorem FOLDL_UNION_BIGUNION:
3648 !f ls s. FOLDL (\s x. s UNION f x) s ls = s UNION BIGUNION (IMAGE f (set ls))
3649Proof
3650GEN_TAC THEN Induct THEN SRW_TAC[] [FOLDL, UNION_ASSOC]
3651QED
3652
3653Theorem FOLDL_UNION_BIGUNION_paired:
3654 !f ls s. FOLDL (\s (x,y). s UNION f x y) s ls =
3655 s UNION BIGUNION (IMAGE (UNCURRY f) (set ls))
3656Proof
3657 GEN_TAC THEN Induct THEN1 SRW_TAC[] [FOLDL] THEN
3658 Cases THEN SRW_TAC[] [FOLDL, UNION_ASSOC, GSYM pairTheory.LAMBDA_PROD]
3659QED
3660
3661Theorem FOLDL_ZIP_SAME[simp]:
3662 !ls f e. FOLDL f e (ZIP (ls,ls)) = FOLDL (\x y. f x (y,y)) e ls
3663Proof
3664Induct THEN SRW_TAC[] [FOLDL, ZIP]
3665QED
3666
3667Theorem MAP_ZIP_SAME[simp]:
3668 !ls f. MAP f (ZIP (ls,ls)) = MAP (\x. f (x,x)) ls
3669Proof
3670Induct THEN SRW_TAC [] [MAP, ZIP]
3671QED
3672
3673(* ----------------------------------------------------------------------
3674 All lists have infinite universes
3675 ---------------------------------------------------------------------- *)
3676
3677Theorem INFINITE_LIST_UNIV[simp]:
3678 INFINITE univ(:'a list)
3679Proof
3680 REWRITE_TAC [] THEN
3681 SRW_TAC [] [INFINITE_UNIV] THEN
3682 Q.EXISTS_TAC ‘\l. x::l’ THEN SRW_TAC [] [] THEN
3683 Q.EXISTS_TAC ‘[]’ THEN SRW_TAC [] []
3684QED
3685
3686
3687(*---------------------------------------------------------------------------*)
3688(* Tail recursive versions for better memory usage when applied in ML *)
3689(*---------------------------------------------------------------------------*)
3690
3691(* EVAL performance of LEN seems to be worse than of LENGTH *)
3692
3693Definition LEN_DEF:
3694 LEN [] n = n /\
3695 LEN (h::t) n = LEN t (n+1)
3696End
3697
3698Definition REV_DEF:
3699 (REV [] acc = acc) /\
3700 (REV (h::t) acc = REV t (h::acc))
3701End
3702
3703Theorem LEN_LENGTH_LEM:
3704 !L n. LEN L n = LENGTH L + n
3705Proof
3706 Induct THEN RW_TAC arith_ss [LEN_DEF, LENGTH]
3707QED
3708
3709Theorem REV_REVERSE_LEM:
3710 !L1 L2. REV L1 L2 = (REVERSE L1) ++ L2
3711Proof
3712 Induct THEN RW_TAC arith_ss [REV_DEF, REVERSE_DEF, APPEND]
3713 THEN REWRITE_TAC [GSYM APPEND_ASSOC]
3714 THEN RW_TAC bool_ss [APPEND]
3715QED
3716
3717Theorem LENGTH_LEN:
3718 !L. LENGTH L = LEN L 0
3719Proof
3720 RW_TAC arith_ss [LEN_LENGTH_LEM]
3721QED
3722
3723Theorem REVERSE_REV:
3724 !L. REVERSE L = REV L []
3725Proof
3726 PROVE_TAC [REV_REVERSE_LEM, APPEND_NIL]
3727QED
3728
3729Definition SUM_ACC_DEF:
3730 (SUM_ACC [] acc = acc) /\
3731 (SUM_ACC (h::t) acc = SUM_ACC t (h+acc))
3732End
3733
3734Theorem SUM_ACC_SUM_LEM:
3735 !L n. SUM_ACC L n = SUM L + n
3736Proof
3737 Induct THEN RW_TAC arith_ss [SUM_ACC_DEF, SUM]
3738QED
3739
3740Theorem SUM_SUM_ACC:
3741 !L. SUM L = SUM_ACC L 0
3742Proof
3743 PROVE_TAC [SUM_ACC_SUM_LEM, arithmeticTheory.ADD_0]
3744QED
3745
3746(* ----------------------------------------------------------------------
3747 List "splitting" results
3748 ---------------------------------------------------------------------- *)
3749
3750(* These loop! Use with care *)
3751Theorem EXISTS_LIST:
3752 (?l. P l) <=> P [] \/ ?h t. P (h::t)
3753Proof
3754 METIS_TAC [list_CASES]
3755QED
3756
3757Theorem FORALL_LIST:
3758 (!l. P l) <=> P [] /\ !h t. P (h::t)
3759Proof
3760 METIS_TAC [list_CASES]
3761QED
3762
3763(* now on with the show *)
3764Theorem MEM_SPLIT_APPEND_first:
3765 MEM e l <=> ?pfx sfx. (l = pfx ++ [e] ++ sfx) /\ ~MEM e pfx
3766Proof
3767 Induct_on ‘l’ THEN SRW_TAC [] [] THEN Cases_on ‘e = a’ THEN
3768 SRW_TAC [] [] THENL[
3769 MAP_EVERY Q.EXISTS_TAC [‘[]’, ‘l’] THEN SRW_TAC [] [],
3770 SRW_TAC [] [SimpRHS, Once EXISTS_LIST]
3771 ]
3772QED
3773
3774Theorem MEM_SPLIT_APPEND_last:
3775 MEM e l <=> ?pfx sfx. (l = pfx ++ [e] ++ sfx) /\ ~MEM e sfx
3776Proof
3777 Q.ID_SPEC_TAC ‘l’ THEN SNOC_INDUCT_TAC THEN SRW_TAC [] [] THEN
3778 Cases_on ‘e = x’ THEN SRW_TAC [] [] THENL [
3779 MAP_EVERY Q.EXISTS_TAC [‘l’, ‘[]’] THEN SRW_TAC [] [SNOC_APPEND],
3780 SRW_TAC [] [EQ_IMP_THM] THENL [
3781 MAP_EVERY Q.EXISTS_TAC [‘pfx’, ‘SNOC x sfx’] THEN
3782 SRW_TAC [] [APPEND_ASSOC, APPEND_SNOC],
3783 Q.SPEC_THEN ‘sfx’ STRIP_ASSUME_TAC SNOC_CASES THEN
3784 SRW_TAC [] [] THEN FULL_SIMP_TAC (srw_ss()) [] THEN1
3785 FULL_SIMP_TAC (srw_ss()) [GSYM SNOC_APPEND] THEN
3786 FULL_SIMP_TAC (srw_ss()) [APPEND_SNOC] THEN SRW_TAC [] [] THEN
3787 METIS_TAC []
3788 ]
3789 ]
3790QED
3791
3792Theorem APPEND_EQ_APPEND:
3793 (l1 ++ l2 = m1 ++ m2) <=>
3794 (?l. (l1 = m1 ++ l) /\ (m2 = l ++ l2)) \/
3795 (?l. (m1 = l1 ++ l) /\ (l2 = l ++ m2))
3796Proof
3797 MAP_EVERY Q.ID_SPEC_TAC [‘m2’, ‘m1’, ‘l2’, ‘l1’] THEN Induct_on ‘l1’ THEN
3798 SRW_TAC [] [] THEN
3799 Cases_on ‘m1’ THEN SRW_TAC [] [] THEN METIS_TAC []
3800QED
3801
3802Theorem APPEND_EQ_CONS:
3803 (l1 ++ l2 = h::t) <=>
3804 ((l1 = []) /\ (l2 = h::t)) \/
3805 ?lt. (l1 = h::lt) /\ (t = lt ++ l2)
3806Proof
3807 MAP_EVERY Q.ID_SPEC_TAC [‘t’, ‘h’, ‘l2’, ‘l1’] THEN Induct_on ‘l1’ THEN
3808 SRW_TAC [] [] THEN METIS_TAC []
3809QED
3810
3811(* could just use APPEND_EQ_APPEND and APPEND_EQ_SING, but this gives you
3812 four possibilities
3813 |- (x ++ [e] ++ y = a ++ b) <=>
3814 (?l'. (x = a ++ l') /\ (b = l' ++ [e] ++ y)) \/
3815 (a = x ++ [e]) /\ (b = y) \/
3816 (a = x) /\ (b = e::y) \/
3817 ?l. (a = x ++ [e] ++ l) /\ (y = l ++ b)
3818 Note that the middle two are instances of the outer two with the
3819 existentially quantified l set to []
3820*)
3821Theorem APPEND_EQ_APPEND_MID:
3822 (l1 ++ [e] ++ l2 = m1 ++ m2) <=>
3823 (?l. (m1 = l1 ++ [e] ++ l) /\ (l2 = l ++ m2)) \/
3824 (?l. (l1 = m1 ++ l) /\ (m2 = l ++ [e] ++ l2))
3825Proof
3826 MAP_EVERY Q.ID_SPEC_TAC [‘m2’, ‘m1’, ‘l2’, ‘e’, ‘l1’] THEN Induct THEN
3827 Cases_on ‘m1’ THEN SRW_TAC [] [] THEN METIS_TAC []
3828QED
3829
3830(* --------------------------------------------------------------------- *)
3831
3832Definition LUPDATE_DEF[notuserdef,nocompute]:
3833 LUPDATE e n [] = [] /\
3834 LUPDATE e n (x::l) = if n = 0 then e :: l else x :: LUPDATE e (PRE n) l
3835End
3836
3837Theorem LUPDATE_def[userdef]:
3838 (!e n. LUPDATE e n [] = [] : 'a list) /\
3839 (!e x l. LUPDATE e 0 (x::l) = e::l) /\
3840 (!e n x l. LUPDATE e (SUC n) (x::l) = x :: LUPDATE e n l)
3841Proof
3842 simp[LUPDATE_DEF]
3843QED
3844
3845Overload fLUPDATE = “λk v l. LUPDATE v k l”
3846Overload fEL = “λl i. EL i l”
3847(* array subscript style brackets are U+2772 and U+2773 *)
3848val _ = combinpp.new_form {
3849 left = "❲", right = "❳",
3850 upd_term_name = (“LUPDATE v k l”, "fLUPDATE"),
3851 lookup_term_name = SOME (“EL i l”, "fEL")
3852 }
3853val _ = TeX_notation { hol = "❲", TeX = ("\\HOLTokenLeftELbracket{}", 1)}
3854val _ = TeX_notation { hol = "❳", TeX = ("\\HOLTokenRightELbracket{}", 1)}
3855
3856
3857val _ = DefnBase.register_indn $ Prim_rec.gen_indthm
3858 {lookup_ind = TypeBase.induction_of} LUPDATE_DEF
3859
3860Theorem LUPDATE_NIL[simp]:
3861 !xs n x. (LUPDATE x n xs = []) <=> (xs = [])
3862Proof
3863 Cases \\ Cases_on ‘n’ \\ FULL_SIMP_TAC (srw_ss()) [LUPDATE_def]
3864QED
3865
3866Theorem LUPDATE_SEM:
3867 (!e:'a n l. LENGTH (LUPDATE e n l) = LENGTH l) /\
3868 (!e:'a n l p.
3869 p < LENGTH l ==>
3870 (EL p (LUPDATE e n l) = if p = n then e else EL p l))
3871Proof
3872 CONJ_TAC
3873 THEN Induct_on ‘n’
3874 THEN Cases_on ‘l’
3875 THEN ASM_SIMP_TAC arith_ss [LUPDATE_def, LENGTH]
3876 THEN Cases_on ‘p’
3877 THEN ASM_SIMP_TAC arith_ss [EL, HD, TL]
3878QED
3879
3880Theorem EL_LUPDATE:
3881 !ys (x:'a) i k.
3882 EL i (LUPDATE x k ys) =
3883 if (i = k) /\ k < LENGTH ys then x else EL i ys
3884Proof
3885 Induct_on ‘ys’ THEN Cases_on ‘k’ THEN REPEAT STRIP_TAC
3886 THEN ASM_SIMP_TAC arith_ss [LUPDATE_def, LENGTH]
3887 THEN Cases_on ‘i’
3888 THEN FULL_SIMP_TAC arith_ss [LUPDATE_def, LENGTH, EL, HD, TL]
3889QED
3890
3891Theorem LENGTH_LUPDATE[simp]:
3892 !(x:'a) n ys. LENGTH (LUPDATE x n ys) = LENGTH ys
3893Proof
3894 SIMP_TAC bool_ss [LUPDATE_SEM]
3895QED
3896
3897Theorem LUPDATE_LENGTH:
3898 !xs x (y:'a) ys. LUPDATE x (LENGTH xs) (xs ++ y::ys) = xs ++ x::ys
3899Proof
3900 Induct THEN FULL_SIMP_TAC bool_ss [LENGTH, APPEND, LUPDATE_def,
3901 NOT_SUC, PRE, INV_SUC_EQ]
3902QED
3903
3904Theorem LUPDATE_SNOC:
3905 !ys k x (y:'a).
3906 LUPDATE x k (SNOC y ys) =
3907 if k = LENGTH ys then SNOC x ys else SNOC y (LUPDATE x k ys)
3908Proof
3909 Induct THEN Cases_on ‘k’ THEN Cases_on ‘n = LENGTH ys’
3910 THEN FULL_SIMP_TAC bool_ss [SNOC, LUPDATE_def, LENGTH, NOT_SUC,
3911 PRE, INV_SUC_EQ]
3912QED
3913
3914Theorem MEM_LUPDATE_E:
3915 !l x y i. MEM x (LUPDATE y i l) ==> (x = y) \/ MEM x l
3916Proof
3917 Induct THEN SRW_TAC [] [LUPDATE_def] THEN
3918 Cases_on‘i’THEN FULL_SIMP_TAC(srw_ss())[LUPDATE_def] THEN
3919 PROVE_TAC[]
3920QED
3921
3922Theorem MEM_LUPDATE:
3923 !l x y i. MEM x (LUPDATE y i l) <=>
3924 i < LENGTH l /\ (x = y) \/
3925 ?j. j < LENGTH l /\ i <> j /\ (EL j l = x)
3926Proof
3927 Induct THEN SRW_TAC [] [LUPDATE_def] THEN
3928 Cases_on ‘i’ THEN SRW_TAC [] [LUPDATE_def] THENL [
3929 SRW_TAC [] [Once arithmeticTheory.EXISTS_NUM] THEN
3930 METIS_TAC [MEM_EL],
3931 EQ_TAC THEN SRW_TAC [] [] THENL [
3932 DISJ2_TAC THEN Q.EXISTS_TAC ‘0’ THEN SRW_TAC [] [],
3933 DISJ2_TAC THEN Q.EXISTS_TAC ‘SUC j’ THEN SRW_TAC [] [],
3934 Cases_on ‘j’ THEN FULL_SIMP_TAC (srw_ss()) [] THEN
3935 METIS_TAC[]
3936 ]
3937 ]
3938QED
3939
3940Theorem LUPDATE_compute[compute] = numLib.SUC_RULE LUPDATE_def
3941
3942Theorem LUPDATE_MAP:
3943 !x n l f. MAP f (LUPDATE x n l) = LUPDATE (f x) n (MAP f l)
3944Proof
3945 Induct_on ‘l’ THEN SRW_TAC [] [LUPDATE_def] THEN Cases_on ‘n’ THEN
3946 FULL_SIMP_TAC (srw_ss()) [LUPDATE_def]
3947QED
3948
3949Theorem LUPDATE_GENLIST:
3950 !m n e f. LUPDATE e n (GENLIST f m) = GENLIST ((n =+ e) f) m
3951Proof
3952 BasicProvers.Induct \\ simp [GENLIST_CONS] \\ Cases \\
3953 simp [LUPDATE_def, combinTheory.APPLY_UPDATE_THM, GENLIST_FUN_EQ]
3954QED
3955
3956Definition EVERYi_def:
3957 (EVERYi P [] <=> T) /\
3958 (EVERYi P (h::t) <=> P 0 h /\ EVERYi (P o SUC) t)
3959End
3960
3961Definition splitAtPki_def:
3962 (splitAtPki P k [] = k [] []) /\
3963 (splitAtPki P k (h::t) =
3964 if P 0 h then k [] (h::t)
3965 else splitAtPki (P o SUC) (\p s. k (h::p) s) t)
3966End
3967
3968Theorem splitAtPki_APPEND:
3969 !l1 l2 P k.
3970 EVERYi (\i. $~ o P i) l1 /\ (0 < LENGTH l2 ==> P (LENGTH l1) (HD l2)) ==>
3971 (splitAtPki P k (l1 ++ l2) = k l1 l2)
3972Proof
3973 Induct THEN SRW_TAC [] [EVERYi_def, splitAtPki_def] THEN1
3974 (Cases_on ‘l2’ THEN FULL_SIMP_TAC (srw_ss())[splitAtPki_def]) THEN
3975 FULL_SIMP_TAC (srw_ss()) [o_DEF]
3976QED
3977
3978Theorem splitAtPki_EQN:
3979 splitAtPki P k l =
3980 case OLEAST i. i < LENGTH l /\ P i (EL i l) of
3981 NONE => k l []
3982 | SOME i => k (TAKE i l) (DROP i l)
3983Proof
3984 MAP_EVERY Q.ID_SPEC_TAC [‘P’, ‘k’, ‘l’] THEN Induct THEN
3985 ASM_SIMP_TAC (srw_ss()) [splitAtPki_def] THEN POP_ASSUM (K ALL_TAC) THEN
3986 MAP_EVERY Q.X_GEN_TAC [‘h’, ‘k’, ‘P’] THEN Cases_on ‘P 0 h’ THEN1
3987 (ASM_SIMP_TAC (srw_ss()) [] THEN
3988 ‘(OLEAST i. i < SUC (LENGTH l) /\ P i (EL i (h::l))) = SOME 0’
3989 suffices_by SRW_TAC [] [] THEN
3990 ASM_SIMP_TAC (srw_ss()) [WhileTheory.OLEAST_EQ_SOME]) THEN
3991 SRW_TAC [] [] THEN
3992 Cases_on ‘OLEAST i. i < LENGTH l /\ P (SUC i) (EL i l)’ >> fs[]
3993 >- (‘(OLEAST i. i < SUC (LENGTH l) /\ P i (EL i (h::l))) = NONE’
3994 suffices_by (DISCH_THEN SUBST1_TAC THEN SRW_TAC[][]) THEN
3995 SRW_TAC[][] >> Q.RENAME_TAC [‘EL i (h::t)’] >> Cases_on ‘i’ >>
3996 SRW_TAC[][]) THEN
3997 Q.RENAME_TAC [‘h::TAKE i t’] >>
3998 ‘(OLEAST i. i < SUC (LENGTH t) /\ P i (EL i (h::t))) = SOME (SUC i)’
3999 suffices_by SRW_TAC [] [] THEN
4000 fs[WhileTheory.OLEAST_EQ_SOME] >> Cases >> SRW_TAC[][]
4001QED
4002
4003Theorem TAKE_splitAtPki:
4004 TAKE n l = splitAtPki (K o (=) n) K l
4005Proof
4006 SRW_TAC [] [splitAtPki_EQN] THEN
4007 DEEP_INTRO_TAC WhileTheory.OLEAST_INTRO THEN
4008 SRW_TAC[numSimps.ARITH_ss] [TAKE_LENGTH_TOO_LONG]
4009QED
4010
4011Theorem DROP_splitAtPki:
4012 DROP n l = splitAtPki (K o (=) n) (K I) l
4013Proof
4014 SRW_TAC [] [splitAtPki_EQN] THEN
4015 DEEP_INTRO_TAC WhileTheory.OLEAST_INTRO THEN
4016 SRW_TAC[numSimps.ARITH_ss] [DROP_LENGTH_TOO_LONG]
4017QED
4018
4019Theorem splitAtPki_RAND:
4020 f (splitAtPki P k l) = splitAtPki P ($o ($o f) k) l
4021Proof
4022 rw[splitAtPki_EQN] >> BasicProvers.CASE_TAC >> simp[]
4023QED
4024
4025Theorem splitAtPki_MAP:
4026 splitAtPki P k (MAP f l) =
4027 splitAtPki (combin$C ($o $o P) f) (combin$C ($o o k o MAP f) (MAP f)) l
4028Proof
4029 rw[splitAtPki_EQN,MAP_TAKE,MAP_DROP]
4030 \\ rpt(AP_THM_TAC ORELSE AP_TERM_TAC)
4031 \\ simp[FUN_EQ_THM]
4032 \\ rw[EQ_IMP_THM] \\ REV_FULL_SIMP_TAC (srw_ss())[EL_MAP]
4033QED
4034
4035Theorem splitAtPki_change_predicate:
4036 (!i. i < LENGTH l ==> (P1 i (EL i l) <=> P2 i (EL i l))) ==>
4037 (splitAtPki P1 k l = splitAtPki P2 k l)
4038Proof
4039 rw[splitAtPki_EQN] >> rpt(AP_THM_TAC ORELSE AP_TERM_TAC) >>
4040 simp[FUN_EQ_THM] >> metis_tac[]
4041QED
4042
4043(* ----------------------------------------------------------------------
4044 List monad related stuff
4045 ---------------------------------------------------------------------- *)
4046
4047(* the bind function is flatMap with arguments in a different order *)
4048Definition LIST_BIND_def:
4049 LIST_BIND l f = FLAT (MAP f l)
4050End
4051
4052Theorem LIST_BIND_THM[simp]:
4053 (LIST_BIND [] f = []) /\
4054 (LIST_BIND (h::t) f = f h ++ LIST_BIND t f)
4055Proof
4056 SIMP_TAC (srw_ss()) [LIST_BIND_def]
4057QED
4058
4059Definition LIST_IGNORE_BIND_def:
4060 LIST_IGNORE_BIND m1 m2 = LIST_BIND m1 (K m2)
4061End
4062
4063Theorem LIST_BIND_ID:
4064 (LIST_BIND l (\x.x) = FLAT l) /\
4065 (LIST_BIND l I = FLAT l)
4066Proof
4067 SIMP_TAC (srw_ss()) [LIST_BIND_def]
4068QED
4069
4070Theorem LIST_BIND_APPEND:
4071 LIST_BIND (l1 ++ l2) f = LIST_BIND l1 f ++ LIST_BIND l2 f
4072Proof
4073 Induct_on ‘l1’ THEN ASM_SIMP_TAC (srw_ss()) [APPEND_ASSOC]
4074QED
4075
4076Theorem LIST_BIND_MAP:
4077 LIST_BIND (MAP f l) g = LIST_BIND l (g o f)
4078Proof
4079 Induct_on ‘l’ THEN ASM_SIMP_TAC (srw_ss()) []
4080QED
4081
4082Theorem MAP_LIST_BIND:
4083 MAP f (LIST_BIND l g) = LIST_BIND l (MAP f o g)
4084Proof
4085 Induct_on ‘l’ THEN ASM_SIMP_TAC (srw_ss()) [MAP_APPEND]
4086QED
4087
4088(* monad associativity *)
4089Theorem LIST_BIND_LIST_BIND:
4090 LIST_BIND (LIST_BIND l g) f = LIST_BIND l (combin$C LIST_BIND f o g)
4091Proof
4092 Induct_on ‘l’ THEN ASM_SIMP_TAC (srw_ss()) [LIST_BIND_APPEND]
4093QED
4094
4095Definition LIST_GUARD_def: LIST_GUARD b = if b then [()] else []
4096End
4097
4098(* the "return" or "pure" constant for lists isn't an existing one, unlike
4099 the situation with 'a option, where SOME fits the bill. *)
4100Overload SINGL = “\x:'a. [x]”
4101Overload "" = “\x:'a. [x]”
4102
4103Theorem SINGL_LIST_APPLY_L[simp]:
4104 LIST_BIND (SINGL x) f = f x
4105Proof
4106 SIMP_TAC (srw_ss()) []
4107QED
4108
4109Theorem SINGL_LIST_APPLY_R:
4110 LIST_BIND l SINGL = l
4111Proof
4112 Induct_on ‘l’ THEN ASM_SIMP_TAC (srw_ss()) [LIST_BIND_def]
4113QED
4114
4115(* shows that lists are what Haskell would call Applicative *)
4116(* in 'a option, the apply applies a function to an argument if both are
4117 SOME, and otherwise returns NONE. In lists, there is a cross-product
4118 created - this makes sense when you think of the list monad as being
4119 the non-determinism thing: you'd want every possible combination of
4120 the possibilities in fs and xs *)
4121Definition LIST_APPLY_def:
4122 LIST_APPLY fs xs = LIST_BIND fs (combin$C MAP xs)
4123End
4124
4125(* pick up the <*> syntax *)
4126Overload APPLICATIVE_FAPPLY = “LIST_APPLY”
4127
4128(* derives the lift2 function to boot *)
4129Definition LIST_LIFT2_def:
4130 LIST_LIFT2 f xs ys = LIST_APPLY (MAP f xs) ys
4131End
4132(* e.g.,
4133 > EVAL ``LIST_LIFT2 (+) [1;3;4] [10;5]``
4134 |- ... = [11;6;13;8;14;9]
4135 i.e., the sums of all possible pairs
4136*)
4137
4138
4139(* proofs of the relevant "laws" *)
4140Theorem SINGL_APPLY_MAP:
4141 LIST_APPLY (SINGL f) l = MAP f l
4142Proof
4143 SIMP_TAC (srw_ss()) [LIST_APPLY_def, LIST_BIND_def]
4144QED
4145
4146Theorem SINGL_SINGL_APPLY[simp]:
4147 LIST_APPLY (SINGL f) (SINGL x) = SINGL (f x)
4148Proof
4149 SIMP_TAC (srw_ss()) [LIST_APPLY_def, LIST_BIND_def]
4150QED
4151
4152Theorem SINGL_APPLY_PERMUTE:
4153 LIST_APPLY fs (SINGL x) = LIST_APPLY (SINGL (\f. f x)) fs
4154Proof
4155 SIMP_TAC (srw_ss()) [LIST_APPLY_def, LIST_BIND_def] THEN
4156 Induct_on ‘fs’ THEN ASM_SIMP_TAC (srw_ss()) []
4157QED
4158
4159Theorem MAP_FLAT:
4160 MAP f (FLAT l) = FLAT (MAP (MAP f) l)
4161Proof
4162 Induct_on ‘l’ THEN ASM_SIMP_TAC (srw_ss()) [MAP_APPEND]
4163QED
4164
4165Theorem FLAT_MAP_K_NIL:
4166 !ls. FLAT (MAP (K []) ls) = []
4167Proof
4168 Induct \\ rw[]
4169QED
4170
4171Theorem LIST_APPLY_o:
4172 LIST_APPLY (LIST_APPLY (LIST_APPLY (SINGL (o)) fs) gs) xs =
4173 LIST_APPLY fs (LIST_APPLY gs xs)
4174Proof
4175 ASM_SIMP_TAC (srw_ss()) [LIST_APPLY_def] THEN
4176 Induct_on ‘fs’ THEN
4177 ASM_SIMP_TAC (srw_ss()) [LIST_BIND_APPEND, MAP_LIST_BIND,
4178 APPEND_11] THEN
4179 SIMP_TAC (srw_ss()) [o_DEF, MAP_MAP_o, LIST_BIND_MAP]
4180QED
4181
4182(* ----------------------------------------------------------------------
4183 Various lexicographic orderings on lists
4184 ---------------------------------------------------------------------- *)
4185
4186Definition SHORTLEX_def:
4187 (SHORTLEX R [] l2 <=> l2 <> []) /\
4188 (SHORTLEX R (h1::t1) l2 <=>
4189 case l2 of
4190 [] => F
4191 | h2::t2 => if LENGTH t1 < LENGTH t2 then T
4192 else if LENGTH t1 = LENGTH t2 then
4193 if R h1 h2 then T
4194 else if h1 = h2 then SHORTLEX R t1 t2
4195 else F
4196 else F)
4197End
4198
4199val def' = uncurry CONJ (Lib.pair_map SPEC_ALL (CONJ_PAIR SHORTLEX_def))
4200Theorem SHORTLEX_THM[simp] =
4201 CONJ (def' |> Q.INST [‘l2’ |-> ‘[]’]
4202 |> SIMP_RULE (srw_ss()) [])
4203 (def' |> Q.INST [‘l2’ |-> ‘h2::t2’]
4204 |> SIMP_RULE (srw_ss()) [])
4205
4206Theorem SHORTLEX_MONO[mono]:
4207 (!x y. R1 x y ==> R2 x y) ==> SHORTLEX R1 x y ==> SHORTLEX R2 x y
4208Proof
4209 STRIP_TAC THEN Q.ID_SPEC_TAC‘y’ THEN Induct_on‘x’ THEN Cases_on‘y’ THEN
4210 SRW_TAC[][SHORTLEX_THM] THEN PROVE_TAC[]
4211QED
4212
4213Theorem SHORTLEX_NIL2[simp]:
4214 ~SHORTLEX R l []
4215Proof
4216 Cases_on ‘l’ THEN SIMP_TAC (srw_ss()) [SHORTLEX_def]
4217QED
4218
4219Theorem SHORTLEX_transitive:
4220 transitive R ==> transitive (SHORTLEX R)
4221Proof
4222 SIMP_TAC(srw_ss()) [transitive_def] THEN STRIP_TAC THEN Induct THEN
4223 SIMP_TAC (srw_ss()) [SHORTLEX_def] THEN
4224 MAP_EVERY Q.X_GEN_TAC [‘h’, ‘y’, ‘z’] THEN Cases_on ‘y’ THEN
4225 SIMP_TAC (srw_ss()) [] THEN Cases_on ‘z’ THEN
4226 SIMP_TAC (srw_ss()) [] THEN
4227 METIS_TAC[arithmeticTheory.LESS_TRANS]
4228QED
4229
4230Theorem LENGTH_LT_SHORTLEX:
4231 !l1 l2. LENGTH l1 < LENGTH l2 ==> SHORTLEX R l1 l2
4232Proof
4233 Induct >> simp[SHORTLEX_def] >> rpt gen_tac >> Cases_on ‘l2’ >> simp[]
4234QED
4235
4236Theorem SHORTLEX_LENGTH_LE:
4237 !l1 l2. SHORTLEX R l1 l2 ==> LENGTH l1 <= LENGTH l2
4238Proof
4239 Induct >> simp[SHORTLEX_def] >> rpt gen_tac >> Cases_on ‘l2’ >> simp[] >>
4240 rw[] >> simp[]
4241QED
4242
4243Theorem SHORTLEX_total:
4244 total (RC R) ==> total (RC (SHORTLEX R))
4245Proof
4246 SIMP_TAC (srw_ss()) [total_def, RC_DEF] THEN STRIP_TAC THEN Induct THEN
4247 SIMP_TAC (srw_ss()) [SHORTLEX_def] THEN MAP_EVERY Q.X_GEN_TAC [‘h’, ‘y’] THEN
4248 Cases_on ‘y’ THEN SIMP_TAC (srw_ss()) [] THEN
4249 Q.RENAME_TAC [‘LENGTH l1 < LENGTH l2’, ‘SHORTLEX R l1 l2’, ‘R h1 h2’] >>
4250 MAP_EVERY Cases_on [‘LENGTH l1 < LENGTH l2’, ‘h1 = h2’, ‘l1 = l2’] >>
4251 simp[] >> metis_tac[arithmeticTheory.LESS_LESS_CASES]
4252QED
4253
4254Theorem SHORTLEX_irreflexive :
4255 !R. irreflexive R ==> irreflexive (SHORTLEX R)
4256Proof
4257 rw [irreflexive_def]
4258 >> Induct_on ‘x’ >> rw [SHORTLEX_def]
4259QED
4260
4261Theorem SHORTLEX_same_lengths :
4262 !R h1 h2 t1 t2. LENGTH t1 = LENGTH t2 ==>
4263 (SHORTLEX R (h1::t1) (h2::t2) <=>
4264 R h1 h2 \/ h1 = h2 /\ SHORTLEX R t1 t2)
4265Proof
4266 rw [SHORTLEX_THM]
4267QED
4268
4269(* NOTE: ‘antisymmetric’ (together with ‘transitive’) is sufficient for using
4270 iterateTheory.TOPOLOGICAL_SORT' to sort a list of lists w.r.t. ‘SHORTLEX R’.
4271
4272 The antecedent ‘irreflexive R’ is necessary.
4273 *)
4274Theorem SHORTLEX_antisymmetric :
4275 !R. irreflexive R /\ antisymmetric R ==> antisymmetric (SHORTLEX R)
4276Proof
4277 rw [antisymmetric_def, irreflexive_def]
4278 >> NTAC 2 (POP_ASSUM MP_TAC)
4279 >> qid_spec_tac ‘y’
4280 >> qid_spec_tac ‘x’
4281 >> Induct_on ‘x’
4282 >- rw [SHORTLEX_THM]
4283 >> rpt STRIP_TAC
4284 >> Cases_on ‘y’ >- fs [SHORTLEX_THM]
4285 >> Q.RENAME_TAC [‘h1::t1 = h2::t2’]
4286 >> ‘LENGTH (h1::t1) <= LENGTH (h2::t2)’ by PROVE_TAC [SHORTLEX_LENGTH_LE]
4287 >> ‘LENGTH (h2::t2) <= LENGTH (h1::t1)’ by PROVE_TAC [SHORTLEX_LENGTH_LE]
4288 >> ‘LENGTH (h1::t1) = LENGTH (h2::t2)’ by PROVE_TAC [LESS_EQUAL_ANTISYM]
4289 >> FULL_SIMP_TAC arith_ss [LENGTH]
4290 >> Q.PAT_X_ASSUM ‘SHORTLEX R (h1::t1) (h2::t2)’ MP_TAC
4291 >> Q.PAT_X_ASSUM ‘SHORTLEX R (h2::t2) (h1::t1)’ MP_TAC
4292 >> rw [SHORTLEX_same_lengths] (* 5 subgoals *)
4293 >> PROVE_TAC []
4294QED
4295
4296Theorem WF_SHORTLEX_same_lengths:
4297 WF R ==>
4298 !l s. (!d. d IN s ==> (LENGTH d = l)) /\ (?a. a IN s) ==>
4299 ?b. b IN s /\ !c. SHORTLEX R c b ==> c NOTIN s
4300Proof
4301 strip_tac >> ho_match_mp_tac (TypeBase.induction_of “:num”) >>
4302 simp[] >> rw[] >- (Q.EXISTS_TAC ‘[]’ >> simp[] >> metis_tac[]) >>
4303 Q.RENAME_TAC [‘LENGTH _ = SUC N’] >>
4304 ‘[] NOTIN s’ by (strip_tac >> ‘LENGTH [] = SUC N’ by metis_tac[] >> fs[]) >>
4305 Q.ABBREV_TAC ‘hds = IMAGE HD s’ >>
4306 ‘?ah. hds ah’ by
4307 (‘?ah. ah IN hds’ suffices_by simp[IN_DEF] >>
4308 simp[Abbr‘hds’] >> metis_tac[]) >>
4309 ‘?m. hds m /\ !n. R n m ==> n NOTIN hds’
4310 by (simp[IN_DEF] >> metis_tac[relationTheory.WF_DEF]) >>
4311 Q.ABBREV_TAC ‘ms = { a | a IN s /\ (HD a = m) }’ >>
4312 ‘?b. b IN ms /\ !c. SHORTLEX R c b ==> c NOTIN ms’ suffices_by
4313 (strip_tac >> Q.EXISTS_TAC ‘b’ >>
4314 ‘b IN s’ by fs[Abbr‘ms’] >> simp[] >> rpt strip_tac >>
4315 ‘c NOTIN ms’ by metis_tac[] >>
4316 ‘HD c <> m’
4317 by (pop_assum mp_tac >> simp_tac (srw_ss()) [Abbr‘ms’] >> simp[]) >>
4318 ‘(LENGTH c = SUC N) /\ (LENGTH b = SUC N)’ by simp[] >>
4319 ‘?ch ct. c = ch :: ct’ by (Cases_on ‘c’ >> fs[]) >>
4320 ‘?bh bt. b = bh :: bt’ by (Cases_on ‘b’ >> fs[]) >>
4321 fs[Abbr‘ms’]
4322 >- (‘ch IN hds’ by (simp[Abbr‘hds’] >> metis_tac[HD]) >>
4323 metis_tac[]) >>
4324 metis_tac[]) >>
4325 CONV_TAC (HO_REWR_CONV EXISTS_LIST) >> DISJ2_TAC >>
4326 Q.EXISTS_TAC ‘m’ >>
4327 ONCE_REWRITE_TAC [tautLib.TAUT ‘(p ==> q) <=> (~q ==> ~p)’] >>
4328 simp[] >> simp[Once FORALL_LIST] >>
4329 Q.ABBREV_TAC ‘mts = { t | m::t IN s }’ >>
4330 ‘!d. d IN mts ==> (LENGTH d = N)’
4331 by (simp[Abbr‘mts’] >> rw[] >> first_x_assum drule >> simp[]) >>
4332 ‘?a0. a0 IN mts’
4333 by (simp[Abbr‘mts’] >>
4334 ‘m IN hds’ by simp[IN_DEF] >> pop_assum mp_tac >>
4335 simp[Abbr‘hds’] >> fs[] >>
4336 Q.RENAME_TAC [‘R _ m’, ‘m = HD e’, ‘e IN s’] >> Cases_on ‘e’ >>
4337 fs[] >> metis_tac[]) >>
4338 ‘?t. t IN mts /\ !u. SHORTLEX R u t ==> u NOTIN mts’ by metis_tac[] >>
4339 Q.EXISTS_TAC ‘t’ >> rw[]
4340 >- fs[Abbr‘mts’, Abbr‘ms’]
4341 >- fs[Abbr‘mts’, Abbr‘ms’]
4342 >- (fs[Abbr‘mts’, Abbr‘ms’] >> rw[]) >>
4343 fs[Abbr‘mts’, Abbr‘ms’] >> rw[] >> metis_tac[IN_DEF]
4344QED
4345
4346Theorem WF_SHORTLEX[simp]:
4347 WF R ==> WF (SHORTLEX R)
4348Proof
4349 simp[relationTheory.WF_DEF] >> rpt strip_tac >>
4350 Q.ABBREV_TAC ‘minlen = (LEAST) (IMAGE LENGTH B)’ >>
4351 ‘?a. B a /\ (LENGTH a = minlen) /\ !b. B b ==> LENGTH a <= LENGTH b’
4352 by (simp[Abbr‘minlen’] >> numLib.LEAST_ELIM_TAC >>
4353 simp[IMAGE_applied] >> simp[IN_DEF] >>
4354 metis_tac[arithmeticTheory.NOT_LESS]) >>
4355 markerLib.RM_ABBREV_TAC "minlen" >> rw[] >>
4356 Q.ABBREV_TAC ‘as = { l | B l /\ (LENGTH l = LENGTH a)}’ >>
4357 ‘!d. d IN as ==> (LENGTH d = LENGTH a)’ by simp[Abbr‘as’] >>
4358 ‘a IN as’ by simp[Abbr‘as’] >>
4359 ‘?a0. a0 IN as /\ !c. SHORTLEX R c a0 ==> c NOTIN as’
4360 by metis_tac[WF_SHORTLEX_same_lengths, relationTheory.WF_DEF] >>
4361 Q.EXISTS_TAC ‘a0’ >> conj_tac
4362 >- fs[Abbr‘as’] >>
4363 Q.X_GEN_TAC ‘bb’ >> rpt strip_tac >>
4364 ‘bb NOTIN as’ by simp[] >>
4365 ‘LENGTH bb <> LENGTH a’ by (fs[Abbr‘as’] >> metis_tac[]) >>
4366 ‘LENGTH a < LENGTH bb’ by metis_tac[arithmeticTheory.LESS_OR_EQ] >>
4367 ‘LENGTH bb <= LENGTH a0’ by metis_tac[SHORTLEX_LENGTH_LE] >>
4368 ‘LENGTH a0 = LENGTH a’ by metis_tac[] >>
4369 full_simp_tac (srw_ss() ++ numSimps.ARITH_ss) []
4370QED
4371
4372Theorem SHORTLEX_SNOC :
4373 !R l h1 h2. R h1 h2 ==> SHORTLEX R (SNOC h1 l) (SNOC h2 l)
4374Proof
4375 Q.X_GEN_TAC ‘R’
4376 >> HO_MATCH_MP_TAC list_induction
4377 >> rw []
4378QED
4379
4380Definition LLEX_def:
4381 (LLEX R [] l2 <=> l2 <> []) /\
4382 (LLEX R (h1::t1) l2 <=>
4383 case l2 of
4384 [] => F
4385 | h2::t2 => if R h1 h2 then T
4386 else if h1 = h2 then LLEX R t1 t2
4387 else F)
4388End
4389
4390val def' = uncurry CONJ (Lib.pair_map SPEC_ALL (CONJ_PAIR LLEX_def))
4391Theorem LLEX_THM[simp] =
4392 CONJ (def' |> Q.INST [‘l2’ |-> ‘[]’]
4393 |> SIMP_RULE (srw_ss()) [])
4394 (def' |> Q.INST [‘l2’ |-> ‘h2::t2’]
4395 |> SIMP_RULE (srw_ss()) [])
4396
4397Theorem LLEX_MONO[mono]:
4398 (!x y. R1 x y ==> R2 x y) ==> LLEX R1 x y ==> LLEX R2 x y
4399Proof
4400 STRIP_TAC THEN
4401 Q.ID_SPEC_TAC‘y’ THEN
4402 Induct_on‘x’ THEN
4403 Cases_on‘y’ THEN
4404 SRW_TAC[][LLEX_THM] THEN
4405 PROVE_TAC[]
4406QED
4407
4408Theorem LLEX_CONG[defncong]:
4409 !R l1 l2 R' l1' l2'.
4410 (l1 = l1') /\ (l2 = l2') /\
4411 (!a b. MEM a l1' /\ MEM b l2' ==> (R a b = R' a b))
4412 ==>
4413 (LLEX R l1 l2 = LLEX R' l1' l2')
4414Proof
4415 GEN_TAC THEN Induct
4416 THENL [ALL_TAC, GEN_TAC]
4417 THEN Induct
4418 THEN SRW_TAC [] []
4419 THEN SRW_TAC [] [LLEX_THM]
4420 THEN METIS_TAC[MEM]
4421QED
4422
4423Theorem LLEX_NIL2[simp]:
4424 ~LLEX R l []
4425Proof
4426 Cases_on ‘l’ THEN SIMP_TAC (srw_ss()) [LLEX_def]
4427QED
4428
4429Theorem LLEX_transitive:
4430 transitive R ==> transitive (LLEX R)
4431Proof
4432 SIMP_TAC(srw_ss()) [transitive_def] THEN STRIP_TAC THEN Induct THEN
4433 SIMP_TAC (srw_ss()) [LLEX_def] THEN
4434 MAP_EVERY Q.X_GEN_TAC [‘h’, ‘y’, ‘z’] THEN Cases_on ‘y’ THEN
4435 SIMP_TAC (srw_ss()) [] THEN Cases_on ‘z’ THEN
4436 SIMP_TAC (srw_ss()) [] THEN METIS_TAC[]
4437QED
4438
4439Theorem LLEX_total:
4440 total (RC R) ==> total (RC (LLEX R))
4441Proof
4442 SIMP_TAC (srw_ss()) [total_def, RC_DEF] THEN STRIP_TAC THEN Induct THEN
4443 SIMP_TAC (srw_ss()) [LLEX_def] THEN MAP_EVERY Q.X_GEN_TAC [‘h’, ‘y’] THEN
4444 Cases_on ‘y’ THEN SIMP_TAC (srw_ss()) [] THEN METIS_TAC[]
4445QED
4446
4447Theorem LLEX_not_WF:
4448 (?a b. R a b) ==> ~WF (LLEX R)
4449Proof
4450 STRIP_TAC THEN SIMP_TAC (srw_ss()) [WF_DEF] THEN
4451 Q.EXISTS_TAC ‘\s. ?n. s = GENLIST (K a) n ++ [b]’ THEN CONJ_TAC
4452 THEN1 (Q.EXISTS_TAC ‘[b]’ THEN SIMP_TAC (srw_ss()) [] THEN
4453 Q.EXISTS_TAC ‘0’ THEN SIMP_TAC (srw_ss()) []) THEN
4454 REWRITE_TAC [GSYM IMP_DISJ_THM] THEN
4455 SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [SKOLEM_THM] THEN
4456 Q.EXISTS_TAC ‘SUC’ THEN Induct_on ‘n’ THEN
4457 ONCE_REWRITE_TAC [GENLIST_CONS] THEN
4458 ASM_SIMP_TAC (srw_ss()) [LLEX_def]
4459QED
4460
4461Theorem LLEX_EL_THM:
4462 !R l1 l2. LLEX R l1 l2 <=>
4463 ?n. n <= LENGTH l1 /\ n < LENGTH l2 /\
4464 (TAKE n l1 = TAKE n l2) /\
4465 (n < LENGTH l1 ==> R (EL n l1) (EL n l2))
4466Proof
4467 GEN_TAC THEN Induct THEN Cases_on‘l2’ THEN SRW_TAC[][] THEN
4468 SRW_TAC[][EQ_IMP_THM] THEN1 (
4469 Q.EXISTS_TAC‘0’ THEN SRW_TAC[][] )
4470 THEN1 (
4471 Q.EXISTS_TAC‘SUC n’ THEN SRW_TAC[][] ) THEN
4472 Cases_on‘n’ THEN FULL_SIMP_TAC(srw_ss())[] THEN
4473 METIS_TAC[]
4474QED
4475
4476(*---------------------------------------------------------------------------*)
4477(* Various lemmas from the CakeML project https://cakeml.org *)
4478(*---------------------------------------------------------------------------*)
4479
4480(* nub *)
4481
4482Definition nub_def:
4483 (nub [] = []) /\
4484 (nub (x::l) = if MEM x l then nub l else x :: nub l)
4485End
4486
4487Theorem nub_NIL[simp] = cj 1 nub_def
4488
4489Theorem nub_EQ0[simp]:
4490 nub l = [] <=> l = []
4491Proof
4492 Induct_on ‘l’ >> rw[nub_def] >> strip_tac >> fs[]
4493QED
4494
4495Theorem nub_set[simp]:
4496 !l. set (nub l) = set l
4497Proof Induct >> rw [nub_def, EXTENSION] >> metis_tac []
4498QED
4499
4500Theorem all_distinct_nub[simp]: !l. ALL_DISTINCT (nub l)
4501Proof
4502 Induct >> rw [nub_def] >> metis_tac [nub_set]
4503QED
4504
4505Theorem all_distinct_nub_id:
4506 !l. ALL_DISTINCT l ==> nub l = l
4507Proof
4508 Induct >> simp[nub_def]
4509QED
4510
4511Theorem CARD_LIST_TO_SET_EQN:
4512 CARD (LIST_TO_SET l) = LENGTH (nub l)
4513Proof
4514 metis_tac[nub_set, CARD_LIST_TO_SET_ALL_DISTINCT,
4515 ALL_DISTINCT_CARD_LIST_TO_SET, all_distinct_nub]
4516QED
4517
4518(* doesn't need to be simp, as nub_set is *)
4519Theorem MEM_nub: MEM x (nub l) = MEM x l
4520Proof simp[]
4521QED
4522
4523Theorem filter_helper[local]:
4524 !x l1 l2.
4525 ~MEM x l2 ==> (MEM x (FILTER (\x. x NOTIN set l2) l1) = MEM x l1)
4526Proof
4527 Induct_on ‘l1’
4528 >> rw []
4529 >> metis_tac []
4530QED
4531
4532Theorem nub_append:
4533 !l1 l2. nub (l1++l2) = nub (FILTER (\x. ~MEM x l2) l1) ++ nub l2
4534Proof
4535 Induct_on ‘l1’
4536 >> rw [nub_def]
4537 >> fs []
4538 >> BasicProvers.FULL_CASE_TAC
4539 >> rw []
4540 >> metis_tac [filter_helper]
4541QED
4542
4543Theorem nub_MAP_INJ:
4544 INJ f (set ls) UNIV ==>
4545 nub (MAP f ls) = MAP f (nub ls)
4546Proof
4547 Induct_on`ls`
4548 \\ rw[]
4549 \\ simp[nub_def]
4550 \\ simp[Once COND_RAND, SimpRHS]
4551 \\ `INJ f (set ls) UNIV`
4552 by (
4553 irule INJ_SUBSET
4554 \\ goal_assum(first_assum o mp_then Any mp_tac)
4555 \\ simp[SUBSET_DEF] )
4556 \\ fs[]
4557 \\ simp[MEM_MAP]
4558 \\ fs[INJ_DEF]
4559 \\ metis_tac[]
4560QED
4561
4562Theorem list_to_set_diff:
4563 !l1 l2. set l2 DIFF set l1 = set (FILTER (\x. x NOTIN set l1) l2)
4564Proof
4565 Induct_on ‘l2’ >> rw []
4566QED
4567
4568Theorem card_eqn_help[local]:
4569 !l1 l2. CARD (set l2) - CARD (set l1 INTER set l2) =
4570 CARD (set (FILTER (\x. x NOTIN set l1) l2))
4571Proof
4572 rw [Once INTER_COMM]
4573 >> SIMP_TAC bool_ss [GSYM CARD_DIFF, FINITE_LIST_TO_SET]
4574 >> metis_tac [list_to_set_diff]
4575QED
4576
4577Theorem length_nub_append:
4578 !l1 l2. LENGTH (nub (l1 ++ l2)) =
4579 LENGTH (nub l1) + LENGTH (nub (FILTER (\x. ~MEM x l1) l2))
4580Proof
4581 rw [GSYM ALL_DISTINCT_CARD_LIST_TO_SET, all_distinct_nub]
4582 >> fs [FINITE_LIST_TO_SET, CARD_UNION_EQN]
4583 >> simp[GSYM card_eqn_help]
4584 >> ‘CARD (set l1 INTER set l2) <= CARD (set l2)’ suffices_by simp[]
4585 >> metis_tac [CARD_INTER_LESS_EQ, FINITE_LIST_TO_SET, INTER_COMM]
4586QED
4587
4588Theorem ALL_DISTINCT_DROP:
4589 !ls n. ALL_DISTINCT ls ==> ALL_DISTINCT (DROP n ls)
4590Proof
4591 Induct >> SIMP_TAC (srw_ss()) [] >> rw [DROP_def]
4592QED
4593
4594Theorem ALL_DISTINCT_TAKE:
4595 !ls n. ALL_DISTINCT ls ==> ALL_DISTINCT (TAKE n ls)
4596Proof
4597 Induct >> simp[TAKE_def] >> Cases_on ‘n’ >> simp[] >>
4598 metis_tac[SUBSET_DEF, LIST_TO_SET_TAKE]
4599QED
4600
4601fun gvs ths =
4602 global_simp_tac{elimvars = true, droptrues = true, strip = true,
4603 oldestfirst = false} (srw_ss()) ths
4604
4605Theorem FINITE_BOUNDED_LISTS:
4606 !s n. FINITE s ==> FINITE { l | set l SUBSET s /\ LENGTH l <= n}
4607Proof
4608 Induct_on ‘n’ >> simp[] >> simp[SF CONJ_ss] >> rpt strip_tac >>
4609 Q.MATCH_ABBREV_TAC ‘FINITE As’ >>
4610 ‘As = IMAGE (λ(h,t). CONS h t)
4611 (s CROSS { l | set l SUBSET s /\ LENGTH l <= n}) UNION
4612 { l | set l SUBSET s /\ LENGTH l <= n}’
4613 suffices_by simp[] >>
4614 simp[Abbr‘As’, EXTENSION, pairTheory.EXISTS_PROD] >>
4615 Q.X_GEN_TAC ‘l’ >> iff_tac >~
4616 [‘LENGTH l <= SUC n’]
4617 >- (simp[arithmeticTheory.LE] >> strip_tac >> simp[] >>
4618 gvs[LENGTH_CONS]) >>
4619 strip_tac >> simp[]
4620QED
4621
4622Theorem FINITE_ALL_DISTINCT_LISTS:
4623 !s. FINITE s ==> FINITE { l | set l SUBSET s /\ ALL_DISTINCT l}
4624Proof
4625 rpt strip_tac >> irule SUBSET_FINITE_I >>
4626 Q.EXISTS_TAC ‘{l | set l SUBSET s /\ LENGTH l <= CARD s}’ >>
4627 simp[FINITE_BOUNDED_LISTS] >>
4628 simp[Once SUBSET_DEF] >> rpt strip_tac >>
4629 drule_then (assume_tac o SYM) ALL_DISTINCT_CARD_LIST_TO_SET >> simp[] >>
4630 simp[CARD_SUBSET]
4631QED
4632
4633Theorem EXISTS_LIST_EQ_MAP:
4634 !ls f. EVERY (\x. ?y. x = f y) ls ==> ?l. ls = MAP f l
4635Proof
4636 Induct
4637 >> ASM_SIMP_TAC (srw_ss()) []
4638 >> rw []
4639 >> RES_TAC
4640 >> Q.EXISTS_TAC‘y::l’
4641 >> ASM_SIMP_TAC (srw_ss()) []
4642QED
4643
4644Theorem LIST_TO_SET_FLAT:
4645 !ls. set (FLAT ls) = BIGUNION (set (MAP set ls))
4646Proof
4647 Induct >> ASM_SIMP_TAC (srw_ss()) []
4648QED
4649
4650Theorem MEM_APPEND_lemma:
4651 !a b c d x.
4652 (a ++ [x] ++ b = c ++ [x] ++ d) /\ x NOTIN set b /\ x NOTIN set a ==>
4653 (a = c) /\ (b = d)
4654Proof
4655 rw [APPEND_EQ_APPEND_MID]
4656 >> fs []
4657 >> fs [APPEND_EQ_SING]
4658QED
4659
4660Theorem EVERY2_REVERSE:
4661 !R l1 l2. EVERY2 R l1 l2 ==> EVERY2 R (REVERSE l1) (REVERSE l2)
4662Proof
4663 rw [EVERY2_EVERY, EVERY_MEM, FORALL_PROD]
4664 >> REV_FULL_SIMP_TAC (srw_ss())
4665 [MEM_ZIP, GSYM LEFT_FORALL_IMP_THM, EL_REVERSE]
4666 >> FIRST_X_ASSUM MATCH_MP_TAC
4667 >> ASM_SIMP_TAC (arith_ss) []
4668QED
4669
4670Theorem LIST_REL_REVERSE = EVERY2_REVERSE
4671
4672Theorem SUM_MAP_PLUS:
4673 !f g ls. SUM (MAP (\x. f x + g x) ls) = SUM (MAP f ls) + SUM (MAP g ls)
4674Proof
4675 NTAC 2 GEN_TAC >> Induct >> simp [SUM]
4676QED
4677
4678Theorem TAKE_LENGTH_ID_rwt: !l m. (m = LENGTH l) ==> (TAKE m l = l)
4679Proof rw [TAKE_LENGTH_ID]
4680QED
4681
4682Theorem TAKE_LENGTH_ID_rwt2[simp]:
4683 !l m. TAKE m l = l <=> LENGTH l <= m
4684Proof
4685 Induct >> simp[] >> Cases_on ‘m’ >> simp[]
4686QED
4687
4688Theorem ZIP_DROP:
4689 !a b n. n <= LENGTH a /\ (LENGTH a = LENGTH b) ==>
4690 (ZIP (DROP n a,DROP n b) = DROP n (ZIP (a,b)))
4691Proof
4692 Induct
4693 THEN SRW_TAC [] [LENGTH_NIL_SYM, arithmeticTheory.ADD1]
4694 THEN Cases_on‘b’
4695 THEN FULL_SIMP_TAC (srw_ss()) [ZIP]
4696 THEN Cases_on‘0<n’ THEN FULL_SIMP_TAC (srw_ss()) [ZIP]
4697 THEN FIRST_X_ASSUM MATCH_MP_TAC
4698 THEN FULL_SIMP_TAC arith_ss []
4699QED
4700
4701Theorem GENLIST_EL:
4702 !ls f n. (n = LENGTH ls) /\ (!i. i < n ==> (f i = EL i ls)) ==>
4703 (GENLIST f n = ls)
4704Proof
4705 rw [LIST_EQ_REWRITE]
4706QED
4707
4708Theorem EVERY2_trans:
4709 (!x y z. R x y /\ R y z ==> R x z) ==>
4710 !x y z. EVERY2 R x y /\ EVERY2 R y z ==> EVERY2 R x z
4711Proof
4712 SRW_TAC [] [EVERY2_EVERY, EVERY_MEM, FORALL_PROD]
4713 THEN REPEAT (Q.PAT_X_ASSUM ‘LENGTH X = Y’ MP_TAC)
4714 THEN REPEAT STRIP_TAC
4715 THEN FULL_SIMP_TAC (srw_ss()++DNF_ss) [MEM_ZIP]
4716 THEN METIS_TAC []
4717QED
4718
4719Theorem LIST_REL_trans_same = EVERY2_trans
4720
4721Theorem EVERY2_sym:
4722 (!x y. R1 x y ==> R2 y x) ==> !x y. EVERY2 R1 x y ==> EVERY2 R2 y x
4723Proof
4724 SRW_TAC [] [EVERY2_EVERY, EVERY_MEM, FORALL_PROD]
4725 THEN Q.PAT_X_ASSUM ‘LENGTH X = Y’ MP_TAC
4726 THEN STRIP_TAC
4727 THEN FULL_SIMP_TAC (srw_ss()++DNF_ss) [MEM_ZIP]
4728QED
4729
4730Theorem LIST_REL_sym = EVERY2_sym
4731
4732Theorem EVERY2_LUPDATE_same:
4733 !P l1 l2 v1 v2 n.
4734 P v1 v2 /\ EVERY2 P l1 l2 ==>
4735 EVERY2 P (LUPDATE v1 n l1) (LUPDATE v2 n l2)
4736Proof
4737 GEN_TAC
4738 THEN Induct
4739 THEN SRW_TAC [] [LUPDATE_def]
4740 THEN Cases_on‘n’
4741 THEN SRW_TAC [] [LUPDATE_def]
4742 THEN Cases_on‘l2’
4743 THEN FULL_SIMP_TAC (srw_ss()) [LUPDATE_def]
4744QED
4745
4746Theorem LIST_REL_LUPDATE_same = EVERY2_LUPDATE_same
4747
4748Theorem EVERY2_refl:
4749 (!x. MEM x ls ==> R x x) ==> (EVERY2 R ls ls)
4750Proof
4751 Induct_on‘ls’ >> rw []
4752QED
4753
4754Theorem LIST_REL_refl = EVERY2_refl
4755
4756Theorem EVERY2_THM[simp]:
4757 (!P ys. EVERY2 P [] ys = (ys = [])) /\
4758 (!P yys x xs. EVERY2 P (x::xs) yys =
4759 ?y ys. (yys = y::ys) /\ (P x y) /\ (EVERY2 P xs ys)) /\
4760 (!P xs. EVERY2 P xs [] = (xs = [])) /\
4761 (!P xxs y ys. EVERY2 P xxs (y::ys) =
4762 ?x xs. (xxs = x::xs) /\ (P x y) /\ (EVERY2 P xs ys))
4763Proof
4764 REPEAT CONJ_TAC
4765 THEN GEN_TAC
4766 THEN TRY (SRW_TAC [] [EVERY2_EVERY, LENGTH_NIL]
4767 THEN SRW_TAC [] [EQ_IMP_THM]
4768 THEN NO_TAC)
4769 THEN Cases
4770 THEN SRW_TAC [] [EVERY2_EVERY]
4771QED
4772
4773Theorem LIST_REL_THM = EVERY2_THM
4774
4775Theorem LIST_REL_trans:
4776 !l1 l2 l3.
4777 (!n. n < LENGTH l1 /\ R (EL n l1) (EL n l2) /\
4778 R (EL n l2) (EL n l3) ==> R (EL n l1) (EL n l3)) /\
4779 LIST_REL R l1 l2 /\ LIST_REL R l2 l3 ==> LIST_REL R l1 l3
4780Proof
4781 Induct
4782 >> simp []
4783 >> rw [LIST_REL_CONS1]
4784 >> fs [LIST_REL_CONS1]
4785 >> rw []
4786 THEN1 (FIRST_X_ASSUM (Q.SPEC_THEN ‘0’ MP_TAC) >> rw [])
4787 >> FIRST_X_ASSUM MATCH_MP_TAC
4788 >> Q.RENAME_TAC [‘LIST_REL _ l1 l2’, ‘LIST_REL _ l2 l3’]
4789 >> Q.EXISTS_TAC‘l2’
4790 >> rw []
4791 >> FIRST_X_ASSUM (Q.SPEC_THEN ‘SUC n’ MP_TAC)
4792 >> simp []
4793QED
4794
4795Theorem LIST_REL_eq[simp,quotient_simp]:
4796 LIST_REL (=) = (=)
4797Proof
4798 simp[FUN_EQ_THM] >> Induct >> rpt gen_tac >>
4799 Q.RENAME_TAC [‘LIST_REL _ _ ys’] >> Cases_on ‘ys’ >> fs []
4800QED
4801
4802Theorem LIST_REL_MEM_IMP:
4803 !xs ys P x. LIST_REL P xs ys /\ MEM x xs ==> ?y. MEM y ys /\ P x y
4804Proof simp[LIST_REL_EL_EQN] >> metis_tac[MEM_EL]
4805QED
4806
4807Theorem LIST_REL_MEM_IMP_R:
4808 !xs ys P y. LIST_REL P xs ys /\ MEM y ys ==> ?x. MEM x xs /\ P x y
4809Proof simp[LIST_REL_EL_EQN] >> metis_tac[MEM_EL]
4810QED
4811
4812Theorem LIST_REL_SNOC:
4813 (LIST_REL R (SNOC x xs) yys <=>
4814 ?y ys. (yys = SNOC y ys) /\ LIST_REL R xs ys /\ R x y) /\
4815 (LIST_REL R xxs (SNOC y ys) <=>
4816 ?x xs. (xxs = SNOC x xs) /\ LIST_REL R xs ys /\ R x y)
4817Proof
4818 simp[EQ_IMP_THM, PULL_EXISTS, SNOC_APPEND] >> rpt strip_tac >>
4819 fs[LIST_REL_SPLIT1, LIST_REL_SPLIT2] >> metis_tac[]
4820QED
4821
4822Theorem LIST_REL_APPEND_IMP:
4823 !xs ys xs1 ys1.
4824 LIST_REL P (xs ++ xs1) (ys ++ ys1) /\ (LENGTH xs = LENGTH ys) ==>
4825 LIST_REL P xs ys /\ LIST_REL P xs1 ys1
4826Proof Induct >> Cases_on ‘ys’ >> FULL_SIMP_TAC (srw_ss()) [] >> METIS_TAC []
4827QED
4828
4829Theorem LIST_REL_APPEND:
4830 EVERY2 R l1 l2 /\ EVERY2 R l3 l4 <=>
4831 EVERY2 R (l1 ++ l3) (l2 ++ l4) /\
4832 (LENGTH l1 = LENGTH l2) /\ (LENGTH l3 = LENGTH l4)
4833Proof
4834 rw[LIST_REL_EL_EQN, EL_APPEND_EQN, EQ_IMP_THM] >> rw[]
4835 >- (first_x_assum irule >> simp[])
4836 >- (first_x_assum (Q.SPEC_THEN ‘n’ mp_tac) >> simp[])
4837 >- (first_x_assum (Q.SPEC_THEN ‘LENGTH l2 + n’ mp_tac) >> simp[])
4838QED
4839
4840Theorem LIST_REL_APPEND_suff:
4841 EVERY2 R l1 l2 /\ EVERY2 R l3 l4 ==> EVERY2 R (l1 ++ l3) (l2 ++ l4)
4842Proof metis_tac[LIST_REL_APPEND]
4843QED
4844
4845Theorem LIST_REL_APPEND_EQ:
4846 (LENGTH x1 = LENGTH x2) ==>
4847 (LIST_REL R (x1 ++ y1) (x2 ++ y2) <=> LIST_REL R x1 x2 /\ LIST_REL R y1 y2)
4848Proof
4849 metis_tac[LIST_REL_APPEND_IMP, EVERY2_LENGTH, LIST_REL_APPEND_suff]
4850QED
4851
4852Theorem LIST_REL_MAP_inv_image:
4853 LIST_REL R (MAP f l1) (MAP f l2) = LIST_REL (inv_image R f) l1 l2
4854Proof
4855 rw[LIST_REL_EL_EQN, EQ_IMP_THM, EL_MAP, LENGTH_MAP] >> metis_tac[EL_MAP]
4856QED
4857
4858Theorem SWAP_REVERSE:
4859 !l1 l2. (l1 = REVERSE l2) = (l2 = REVERSE l1)
4860Proof
4861 SRW_TAC [] [EQ_IMP_THM]
4862QED
4863
4864Theorem SWAP_REVERSE_SYM:
4865 !l1 l2. (REVERSE l1 = l2) = (l1 = REVERSE l2)
4866Proof
4867 metis_tac [SWAP_REVERSE]
4868QED
4869
4870Theorem BIGUNION_IMAGE_set_SUBSET:
4871 (BIGUNION (IMAGE f (set ls)) SUBSET s) = (!x. MEM x ls ==> f x SUBSET s)
4872Proof
4873 SRW_TAC [DNF_ss] [SUBSET_DEF] THEN METIS_TAC []
4874QED
4875
4876Theorem IMAGE_EL_count_LENGTH:
4877 !f ls. IMAGE (\n. f (EL n ls)) (count (LENGTH ls)) = IMAGE f (set ls)
4878Proof
4879 rw [EXTENSION, MEM_EL] >> PROVE_TAC []
4880QED
4881
4882Theorem GENLIST_EL_MAP:
4883 !f ls. GENLIST (\n. f (EL n ls)) (LENGTH ls) = MAP f ls
4884Proof
4885 GEN_TAC >> Induct >> rw [GENLIST_CONS, o_DEF]
4886QED
4887
4888Theorem LENGTH_FILTER_LEQ_MONO:
4889 !P Q. (!x. P x ==> Q x) ==>
4890 !ls. (LENGTH (FILTER P ls) <= LENGTH (FILTER Q ls))
4891Proof
4892 REPEAT GEN_TAC
4893 >> STRIP_TAC
4894 >> Induct
4895 >> rw []
4896 >> FULL_SIMP_TAC arith_ss []
4897 >> PROVE_TAC []
4898QED
4899
4900Theorem LIST_EQ_MAP_PAIR:
4901 !l1 l2.
4902 (MAP FST l1 = MAP FST l2) /\ (MAP SND l1 = MAP SND l2) ==> (l1 = l2)
4903Proof
4904 SRW_TAC []
4905 [MAP_EQ_EVERY2, EVERY2_EVERY, EVERY_MEM, LIST_EQ_REWRITE, FORALL_PROD]
4906 THEN REV_FULL_SIMP_TAC (srw_ss()++DNF_ss) [MEM_ZIP]
4907 THEN METIS_TAC [pair_CASES, PAIR_EQ]
4908QED
4909
4910Theorem TAKE_SUM:
4911 !n m l. TAKE (n + m) l = TAKE n l ++ TAKE m (DROP n l)
4912Proof
4913 Induct_on ‘l’ >> simp[TAKE_def] >> rw[] >> simp[] >>
4914 ‘m + n - 1 = (n - 1) + m’ by simp[] >>
4915 ASM_REWRITE_TAC[]
4916QED
4917
4918Theorem ALL_DISTINCT_FILTER_EL_IMP:
4919 !P l n1 n2.
4920 ALL_DISTINCT (FILTER P l) /\ n1 < LENGTH l /\ n2 < LENGTH l /\
4921 (P (EL n1 l)) /\ (EL n1 l = EL n2 l) ==> (n1 = n2)
4922Proof
4923 GEN_TAC
4924 THEN Induct
4925 THEN1 SRW_TAC [] []
4926 THEN SRW_TAC [] []
4927 THEN FULL_SIMP_TAC (srw_ss()) [MEM_FILTER]
4928 THEN1 PROVE_TAC []
4929 THEN Cases_on ‘n1’
4930 THEN Cases_on ‘n2’
4931 THEN FULL_SIMP_TAC (srw_ss()) [MEM_EL]
4932 THEN PROVE_TAC []
4933QED
4934
4935Theorem FLAT_EQ_NIL:
4936 !ls. (FLAT ls = []) = (EVERY ($= []) ls)
4937Proof
4938 Induct >> SRW_TAC [] [EQ_IMP_THM] >> rw [APPEND]
4939QED
4940
4941Theorem FLAT_EQ_NIL' :
4942 FLAT l = [] <=> !e. MEM e l ==> e = []
4943Proof simp[FLAT_EQ_NIL, EVERY_MEM] >> metis_tac[]
4944QED
4945
4946Theorem FLAT_EQ_SING:
4947 FLAT l = [x] <=>
4948 ?p s. l = p ++ [[x]] ++ s /\ FLAT p = [] /\ FLAT s = []
4949Proof
4950 Induct_on `l` >> simp[] >> simp[APPEND_EQ_CONS] >>
4951 simp_tac (srw_ss() ++ DNF_ss) [] >> metis_tac[]
4952QED
4953
4954Theorem FLAT_EQ_APPEND:
4955 FLAT l = x ++ y <=>
4956 (?p s. l = p ++ s /\ x = FLAT p /\ y = FLAT s) \/
4957 (?p s ip is.
4958 l = p ++ [ip ++ is] ++ s /\ ip <> [] /\ is <> [] /\
4959 x = FLAT p ++ ip /\
4960 y = is ++ FLAT s)
4961Proof
4962 reverse eq_tac >- (rw[] >> rw[APPEND_ASSOC, FLAT_APPEND]) >>
4963 map_every qid_spec_tac [`y`,`x`,`l`] >> Induct_on `l` >- simp[] >>
4964 simp[] >> map_every qx_gen_tac [`h`, `x`, `y`] >>
4965 simp[APPEND_EQ_APPEND] >>
4966 disch_then (DISJ_CASES_THEN (qxch `m` strip_assume_tac))
4967 >- (Cases_on `x = []`
4968 >- (fs[] >> map_every qexists_tac [`[]`, `m::l`] >> simp[]) >>
4969 Cases_on `m = []`
4970 >- (fs[] >> disj1_tac >> map_every qexists_tac [`[x]`, `l`] >>
4971 simp[]) >>
4972 disj2_tac >>
4973 map_every qexists_tac [`[]`, `l`, `x`, `m`] >> simp[]) >>
4974 `(?p s. l = p ++ s /\ FLAT p = m /\ FLAT s = y) \/
4975 (?p s ip is.
4976 l = p ++ [ip ++ is] ++ s /\ m = FLAT p ++ ip /\ ip <> [] /\ is <> [] /\
4977 y = is ++ FLAT s)` by metis_tac[]
4978 >- (disj1_tac >> map_every qexists_tac [`h::p`, `s`] >> simp[]) >>
4979 disj2_tac >> map_every qexists_tac [`h::p`, `s`] >> simp[APPEND_ASSOC] >>
4980 map_every qexists_tac [`ip`, `is`] >> rw []
4981QED
4982
4983Theorem ALL_DISTINCT_MAP_INJ:
4984 !ls f. (!x y. MEM x ls /\ MEM y ls /\ (f x = f y) ==> (x = y)) /\
4985 ALL_DISTINCT ls ==> ALL_DISTINCT (MAP f ls)
4986Proof
4987 Induct THEN SRW_TAC [] [MEM_MAP] THEN PROVE_TAC []
4988QED
4989
4990Theorem LENGTH_o_REVERSE:
4991 (LENGTH o REVERSE = LENGTH) /\
4992 (LENGTH o REVERSE o f = LENGTH o f)
4993Proof
4994 SRW_TAC [] [FUN_EQ_THM]
4995QED
4996
4997Theorem REVERSE_o_REVERSE:
4998 (REVERSE o REVERSE o f = f)
4999Proof
5000 SRW_TAC [] [FUN_EQ_THM]
5001QED
5002
5003Theorem GENLIST_PLUS_APPEND:
5004 GENLIST ($+ a) n1 ++ GENLIST ($+ (n1 + a)) n2 = GENLIST ($+ a) (n1 + n2)
5005Proof
5006 rw [Once arithmeticTheory.ADD_SYM, SimpRHS]
5007 >> RW_TAC arith_ss [GENLIST_APPEND]
5008 >> SRW_TAC [ETA_ss] [arithmeticTheory.ADD_ASSOC]
5009QED
5010
5011Theorem LIST_TO_SET_GENLIST:
5012 !f n. LIST_TO_SET (GENLIST f n) = IMAGE f (count n)
5013Proof
5014 SRW_TAC [] [EXTENSION, MEM_GENLIST] THEN PROVE_TAC []
5015QED
5016
5017Theorem MEM_ZIP_MEM_MAP:
5018 (LENGTH (FST ps) = LENGTH (SND ps)) /\
5019 MEM p (ZIP ps) ==> MEM (FST p) (FST ps) /\ MEM (SND p) (SND ps)
5020Proof
5021 Cases_on ‘p’
5022 >> Cases_on ‘ps’
5023 >> SRW_TAC [] []
5024 >> REV_FULL_SIMP_TAC (srw_ss()) [MEM_ZIP, MEM_EL]
5025 >> PROVE_TAC []
5026QED
5027
5028Theorem DISJOINT_GENLIST_PLUS:
5029 DISJOINT x (set (GENLIST ($+ n) (a + b))) ==>
5030 DISJOINT x (set (GENLIST ($+ n) a)) /\
5031 DISJOINT x (set (GENLIST ($+ (n + a)) b))
5032Proof
5033 rw [GSYM GENLIST_PLUS_APPEND]
5034 >> metis_tac [DISJOINT_SYM, arithmeticTheory.ADD_SYM]
5035QED
5036
5037Theorem EVERY2_MAP:
5038 (EVERY2 P (MAP f l1) l2 = EVERY2 (\x y. P (f x) y) l1 l2) /\
5039 (EVERY2 Q l1 (MAP g l2) = EVERY2 (\x y. Q x (g y)) l1 l2)
5040Proof
5041 rw [EVERY2_EVERY, LENGTH_MAP]
5042 >> Cases_on `LENGTH l1 = LENGTH l2`
5043 >> fs []
5044 >> rw [ZIP_MAP, EVERY_MEM, MEM_MAP]
5045 >> SRW_TAC [DNF_ss] [pairTheory.FORALL_PROD, LENGTH_MAP, MEM_ZIP]
5046QED
5047
5048Theorem LIST_REL_MAP = EVERY2_MAP
5049
5050Theorem exists_list_GENLIST:
5051 (?ls. P ls) = (?n f. P (GENLIST f n))
5052Proof
5053 rw [EQ_IMP_THM]
5054 THEN1 (MAP_EVERY Q.EXISTS_TAC [‘LENGTH ls’,‘combin$C EL ls’]
5055 >> Q.MATCH_ABBREV_TAC ‘P ls2’
5056 >> Q_TAC SUFF_TAC ‘ls2 = ls’
5057 THEN1 rw []
5058 >> rw [LIST_EQ_REWRITE, Abbr‘ls2’])
5059 >> PROVE_TAC []
5060QED
5061
5062Theorem EVERY_MEM_MONO:
5063 !P Q l. (!x. MEM x l /\ P x ==> Q x) /\ EVERY P l ==> EVERY Q l
5064Proof
5065 NTAC 2 GEN_TAC >> Induct >> rw []
5066QED
5067
5068Theorem EVERY2_MEM_MONO:
5069 !P Q l1 l2. (!x. MEM x (ZIP (l1,l2)) /\ UNCURRY P x ==> UNCURRY Q x) /\
5070 EVERY2 P l1 l2 ==> EVERY2 Q l1 l2
5071Proof
5072 rw [EVERY2_EVERY] >> MATCH_MP_TAC EVERY_MEM_MONO >> PROVE_TAC []
5073QED
5074
5075Theorem LIST_REL_MEM_MONO = EVERY2_MEM_MONO
5076
5077Theorem mem_exists_set:
5078 !x y l. MEM (x,y) l ==> ?z. (x = FST z) /\ z IN set l
5079Proof
5080 Induct_on ‘l’
5081 >> rw []
5082 >> metis_tac [FST]
5083QED
5084
5085Theorem every_zip_snd:
5086 !l1 l2 P.
5087 (LENGTH l1 = LENGTH l2) ==>
5088 (EVERY (\x. P (SND x)) (ZIP (l1,l2)) = EVERY P l2)
5089Proof
5090 Induct_on ‘l1’
5091 >> rw []
5092 >> TRY(Cases_on ‘l2’)
5093 >> fs [ZIP]
5094QED
5095
5096Theorem every_zip_fst:
5097 !l1 l2 P. (LENGTH l1 = LENGTH l2) ==>
5098 (EVERY (\x. P (FST x)) (ZIP (l1,l2)) = EVERY P l1)
5099Proof
5100 Induct_on ‘l1’
5101 >> rw []
5102 >> TRY(Cases_on ‘l2’)
5103 >> fs [ZIP]
5104QED
5105
5106Theorem el_append3:
5107 !l1 x l2. EL (LENGTH l1) (l1++ [x] ++ l2) = x
5108Proof
5109 Induct_on ‘l1’
5110 >> rw []
5111 >> rw []
5112QED
5113
5114Theorem lupdate_append:
5115 !x n l1 l2.
5116 n < LENGTH l1 ==> (LUPDATE x n (l1++l2) = LUPDATE x n l1 ++ l2)
5117Proof
5118 Induct_on ‘l1’
5119 >> rw []
5120 >> Cases_on ‘n’
5121 >> rw [LUPDATE_def]
5122 >> fs []
5123QED
5124
5125Theorem lupdate_append2:
5126 !v l1 x l2 l3. LUPDATE v (LENGTH l1) (l1++[x]++l2) = l1++[v]++l2
5127Proof
5128 Induct_on ‘l1’ >> rw [LUPDATE_def]
5129QED
5130
5131Theorem HD_REVERSE:
5132 !x. x <> [] ==> (HD (REVERSE x) = LAST x)
5133Proof
5134 REPEAT strip_tac >>
5135 Induct_on ‘x’ THEN1 fs[] >>
5136 rw[LAST_DEF] >>
5137 Cases_on ‘REVERSE x’ THEN1 fs[] >>
5138 fs[]
5139QED
5140
5141Theorem LAST_REVERSE:
5142 !ls. ls <> [] ==> (LAST (REVERSE ls) = HD ls)
5143Proof
5144 Induct >> simp []
5145QED
5146
5147Theorem NOT_NIL_EQ_LENGTH_NOT_0:
5148 x <> [] <=> (0 < LENGTH x)
5149Proof
5150 Cases_on ‘x’ >> rw[]
5151QED
5152
5153Theorem last_drop:
5154 !l n. n < LENGTH l ==> (LAST (DROP n l) = LAST l)
5155Proof
5156 Induct >> rw [DROP_def] >>
5157 Q.SPEC_THEN‘l’FULL_STRUCT_CASES_TAC list_CASES >> fs [] >>
5158 FULL_SIMP_TAC (srw_ss()++numSimps.ARITH_ss) [] >> SRW_TAC[] [] >>
5159 FIRST_X_ASSUM (Q.SPEC_THEN ‘n - 1’ MP_TAC) >>
5160 simp[]
5161QED
5162
5163Definition dropWhile_def[simp]:
5164 (dropWhile P [] = []) /\
5165 (dropWhile P (h::t) = if P h then dropWhile P t else (h::t))
5166End
5167
5168Theorem dropWhile_splitAtPki:
5169 !P. dropWhile P = splitAtPki (combin$C (K o $~ o P)) (K I)
5170Proof
5171 GEN_TAC
5172 >> simp [FUN_EQ_THM]
5173 >> Induct
5174 >> simp [splitAtPki_def]
5175 >> rw []
5176 >> AP_THM_TAC
5177 >> Q.MATCH_ABBREV_TAC ‘f a b = f a' b'’
5178 >> ‘b = b'’ by (markerLib.UNABBREV_ALL_TAC >> simp [FUN_EQ_THM])
5179 >> ‘a = a'’ by (markerLib.UNABBREV_ALL_TAC >> simp [FUN_EQ_THM])
5180 >> REV_FULL_SIMP_TAC (srw_ss()) []
5181QED
5182
5183Theorem dropWhile_eq_nil:
5184 !P ls. (dropWhile P ls = []) <=> EVERY P ls
5185Proof
5186 GEN_TAC >> Induct >> simp [] >> rw []
5187QED
5188
5189Theorem MEM_dropWhile_IMP:
5190 !P ls x. MEM x (dropWhile P ls) ==> MEM x ls
5191Proof
5192 GEN_TAC >> Induct >> simp [] >> rw []
5193QED
5194
5195Theorem HD_dropWhile:
5196 !P ls. EXISTS ($~ o P) ls ==> ~ P (HD (dropWhile P ls))
5197Proof
5198 GEN_TAC >> Induct >> simp [] >> rw []
5199QED
5200
5201Theorem LENGTH_dropWhile_LESS_EQ:
5202 !P ls. LENGTH (dropWhile P ls) <= LENGTH ls
5203Proof
5204 GEN_TAC >> Induct >> simp [] >> rw [] >> simp []
5205QED
5206
5207Theorem dropWhile_APPEND_EVERY:
5208 !P l1 l2. EVERY P l1 ==> (dropWhile P (l1 ++ l2) = dropWhile P l2)
5209Proof
5210 GEN_TAC >> Induct >> simp [dropWhile_def]
5211QED
5212
5213Theorem dropWhile_APPEND_EXISTS:
5214 !P l1 l2. EXISTS ($~ o P) l1 ==>
5215 (dropWhile P (l1 ++ l2) = dropWhile P l1 ++ l2)
5216Proof
5217 GEN_TAC >> Induct >> simp [dropWhile_def] >> rw []
5218QED
5219
5220local
5221 val fs = FULL_SIMP_TAC (srw_ss()++numSimps.ARITH_ss)
5222 val rw = SRW_TAC [numSimps.ARITH_ss]
5223in
5224Theorem EL_LENGTH_dropWhile_REVERSE:
5225 !P ls k. LENGTH (dropWhile P (REVERSE ls)) <= k /\ k < LENGTH ls ==>
5226 P (EL k ls)
5227Proof
5228 GEN_TAC
5229 >> Induct
5230 >> simp [LENGTH]
5231 >> rw []
5232 >> Cases_on ‘k’
5233 >> fs [LENGTH_NIL, dropWhile_eq_nil, EVERY_APPEND]
5234 >> FIRST_X_ASSUM MATCH_MP_TAC
5235 >> simp []
5236 >> Cases_on ‘EVERY P (REVERSE ls)’
5237 THEN1 (fs [dropWhile_APPEND_EVERY, GSYM dropWhile_eq_nil])
5238 >> fs [NOT_EVERY, dropWhile_APPEND_EXISTS, arithmeticTheory.ADD1]
5239QED
5240end
5241
5242Theorem dropWhile_id:
5243 (dropWhile P ls = ls) <=> NULL ls \/ ~P(HD ls)
5244Proof
5245 Cases_on`ls` \\ rw[dropWhile_def, NULL]
5246 \\ disch_then(mp_tac o Q.AP_TERM`LENGTH`)
5247 \\ Q.MATCH_GOALSUB_RENAME_TAC`dropWhile P l`
5248 \\ Q.SPECL_THEN[`P`,`l`]mp_tac LENGTH_dropWhile_LESS_EQ
5249 \\ simp[]
5250QED
5251
5252Theorem IMP_EVERY_LUPDATE:
5253 !xs h i. P h /\ EVERY P xs ==> EVERY P (LUPDATE h i xs)
5254Proof
5255 Induct THEN fs [LUPDATE_def] THEN REPEAT STRIP_TAC
5256 THEN Cases_on ‘i’ THEN fs [LUPDATE_def]
5257QED
5258
5259Theorem MAP_APPEND_MAP_EQ:
5260 !xs ys.
5261 ((MAP f1 xs ++ MAP g1 ys) = (MAP f2 xs ++ MAP g2 ys)) <=>
5262 (MAP f1 xs = MAP f2 xs) /\ (MAP g1 ys = MAP g2 ys)
5263Proof
5264 Induct THEN fs [] THEN METIS_TAC []
5265QED
5266
5267Theorem LUPDATE_SOME_MAP:
5268 !xs n f h.
5269 LUPDATE (SOME (f h)) n (MAP (OPTION_MAP f) xs) =
5270 MAP (OPTION_MAP f) (LUPDATE (SOME h) n xs)
5271Proof
5272 Induct THEN1 (fs [LUPDATE_def]) THEN
5273 Cases_on ‘n’ THEN fs [LUPDATE_def]
5274QED
5275
5276Theorem ZIP_EQ_NIL:
5277 !l1 l2. (LENGTH l1 = LENGTH l2) ==>
5278 ((ZIP (l1,l2) = []) <=> ((l1 = []) /\ (l2 = [])))
5279Proof
5280 REPEAT GEN_TAC >> Cases_on‘l1’ >> rw[LENGTH_NIL_SYM,ZIP] >> Cases_on‘l2’ >>
5281 fs[ZIP]
5282QED
5283
5284Theorem LUPDATE_SAME:
5285 !n ls. n < LENGTH ls ==> (LUPDATE (EL n ls) n ls = ls)
5286Proof
5287 rw[LIST_EQ_REWRITE,EL_LUPDATE]>>rw[]
5288QED
5289
5290(* end CakeML lemmas *)
5291
5292(* u is unique in L, learnt from Robert Beers <robert@beers.org> *)
5293Definition UNIQUE_DEF[nocompute]:
5294 UNIQUE e L = ?L1 L2. (L1 ++ [e] ++ L2 = L) /\ ~MEM e L1 /\ ~MEM e L2
5295End
5296
5297local
5298 fun take ts = MAP_EVERY Q.EXISTS_TAC ts; (* from HOL mizar mode *)
5299 val Know = Q_TAC KNOW_TAC; (* from util_prob *)
5300 val Suff = Q_TAC SUFF_TAC; (* from util_prob *)
5301 fun K_TAC _ = ALL_TAC; (* from util_prob *)
5302 val KILL_TAC = POP_ASSUM_LIST K_TAC; (* from util_prob *)
5303 fun wrap a = [a]; (* from util_prob *)
5304 val Rewr = DISCH_THEN (REWRITE_TAC o wrap); (* from util_prob *)
5305in
5306(* alternative definition of UNIQUE, by Chun Tian (binghe) *)
5307Theorem UNIQUE_FILTER: !e L. UNIQUE e L = (FILTER ($= e) L = [e])
5308Proof
5309 rpt GEN_TAC
5310 >> REWRITE_TAC [UNIQUE_DEF]
5311 >> EQ_TAC >> rpt STRIP_TAC (* 2 sub-goals here *)
5312 >| [ (* goal 1 (of 2) *)
5313 Q.PAT_X_ASSUM ‘P = L’ (REWRITE_TAC o wrap o SYM) \\
5314 REWRITE_TAC [FILTER_APPEND_DISTRIB] \\
5315 Know ‘((FILTER ($= e) L1) = []) /\ ((FILTER ($= e) L2) = [])’
5316 >- ( REWRITE_TAC [GSYM NULL_EQ] \\
5317 REWRITE_TAC [NULL_FILTER] \\
5318 rpt STRIP_TAC >> FULL_SIMP_TAC arith_ss [] ) \\
5319 Rewr \\
5320 REWRITE_TAC [APPEND, APPEND_NIL, FILTER],
5321 (* goal 2 (of 2) *)
5322 Know ‘MEM e L’
5323 >- ( ‘FILTER ($= e) L <> []’ by PROVE_TAC [NOT_CONS_NIL] \\
5324 FULL_SIMP_TAC arith_ss [FILTER_NEQ_NIL] ) \\
5325 REWRITE_TAC [MEM_SPLIT] >> rpt STRIP_TAC \\
5326 take [‘l1’, ‘l2’] >> FULL_SIMP_TAC arith_ss [] \\
5327 CONJ_TAC >- ( KILL_TAC >> REWRITE_TAC [GSYM APPEND_ASSOC] \\
5328 SIMP_TAC arith_ss [APPEND, APPEND_11] ) \\
5329 POP_ASSUM K_TAC \\
5330 POP_ASSUM MP_TAC \\
5331 SIMP_TAC arith_ss [FILTER_APPEND_DISTRIB, FILTER] \\
5332 REWRITE_TAC [APPEND_EQ_SING] \\
5333 rpt STRIP_TAC \\
5334 FULL_SIMP_TAC arith_ss [NOT_CONS_NIL, FILTER_APPEND_DISTRIB, FILTER,
5335 APPEND_eq_NIL, CONS_11] ]
5336QED
5337
5338(* alternative definition of UNIQUE, learnt from Scott Owens and Anthony Fox *)
5339Theorem UNIQUE_LENGTH_FILTER: !e L. UNIQUE e L = (LENGTH (FILTER ($= e) L) = 1)
5340Proof
5341 rpt GEN_TAC
5342 >> REWRITE_TAC [UNIQUE_FILTER]
5343 >> EQ_TAC >> DISCH_TAC
5344 >- ( ASM_REWRITE_TAC [] >> REWRITE_TAC [LENGTH] >> ACCEPT_TAC (SYM ONE) )
5345 >> POP_ASSUM MP_TAC
5346 >> REWRITE_TAC [ONE, LENGTH_EQ_NUM]
5347 >> SIMP_TAC arith_ss []
5348 >> rpt STRIP_TAC
5349 >> Cases_on ‘e = h’ >- ASM_REWRITE_TAC []
5350 >> ASM_REWRITE_TAC []
5351 >> FULL_SIMP_TAC arith_ss [CONS_11]
5352 >> Suff ‘MEM e (FILTER ($= e) L)’
5353 >- ( DISCH_TAC \\
5354 REV_FULL_SIMP_TAC (arith_ss ++ pred_setSimps.PRED_SET_ss) [LIST_TO_SET] )
5355 >> REWRITE_TAC [MEM_FILTER]
5356 >> Know ‘FILTER ($= e) L <> []’ >- FULL_SIMP_TAC arith_ss [NOT_CONS_NIL]
5357 >> KILL_TAC
5358 >> REWRITE_TAC [FILTER_NEQ_NIL]
5359 >> rpt STRIP_TAC
5360 >> ASM_REWRITE_TAC []
5361QED
5362end; (* local *)
5363
5364(* OPT_MMAP : ('a -> 'b option) -> 'a list -> 'b list option *)
5365Definition OPT_MMAP_def[simp]:
5366 (OPT_MMAP f [] = SOME []) /\
5367 (OPT_MMAP f (h0::t0) =
5368 OPTION_BIND (f h0) (\h. OPTION_BIND (OPT_MMAP f t0) (\t. SOME (h::t))))
5369End
5370
5371Theorem OPT_MMAP_cong[defncong]:
5372 !f1 f2 x1 x2.
5373 x1 = x2 /\ (!a. MEM a x2 ==> f1 a = f2 a) ==>
5374 OPT_MMAP f1 x1 = OPT_MMAP f2 x2
5375Proof
5376 ntac 2 gen_tac \\ Induct \\ rw[] \\ computeLib.EVAL_TAC
5377 \\ FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) []
5378QED
5379
5380Theorem IS_SOME_OPT_MMAP:
5381 IS_SOME (OPT_MMAP f ls) <=> EVERY IS_SOME (MAP f ls)
5382Proof
5383 Induct_on`ls` \\ rw[]
5384 \\ Q.MATCH_GOALSUB_RENAME_TAC`IS_SOME (f x)`
5385 \\ Cases_on`f x` \\ rw[]
5386 \\ Cases_on`OPT_MMAP f ls` \\ fs[]
5387QED
5388
5389Theorem LAST_compute:
5390 (!x. LAST [x] = x) /\
5391 (!h1 h2 t. LAST (h1::h2::t) = LAST (h2::t))
5392Proof
5393 SRW_TAC [] [LAST_DEF]
5394QED
5395
5396Theorem TAKE_compute[local]:
5397 (!l. TAKE 0 l = []) /\
5398 (!n. TAKE (SUC n) [] = []) /\
5399 (!n h t. TAKE (SUC n) (h::t) = h :: TAKE n t)
5400Proof
5401 SRW_TAC [] []
5402QED
5403
5404Theorem DROP_compute[local]:
5405 (!l. DROP 0 l = l) /\
5406 (!n. DROP (SUC n) [] = []) /\
5407 (!n h t. DROP (SUC n) (h::t) = DROP n t)
5408Proof
5409 SRW_TAC [] []
5410QED
5411
5412Theorem TAKE_compute = numLib.SUC_RULE TAKE_compute;
5413
5414Theorem DROP_compute = numLib.SUC_RULE DROP_compute;
5415
5416Theorem DROP_TAKE:
5417 !xs n k. DROP n (TAKE k xs) = TAKE (k - n) (DROP n xs)
5418Proof
5419 Induct \\ simp_tac bool_ss [TAKE_def,DROP_def]
5420 \\ rpt strip_tac \\ rpt IF_CASES_TAC
5421 \\ asm_simp_tac bool_ss [TAKE_def,DROP_def,TAKE_0,arithmeticTheory.SUB_0]
5422 \\ AP_THM_TAC \\ AP_TERM_TAC \\ numLib.DECIDE_TAC
5423QED
5424
5425Theorem TAKE_DROP_SWAP:
5426 !xs k n. TAKE k (DROP n xs) = DROP n (TAKE (k + n) xs)
5427Proof
5428 rewrite_tac [DROP_TAKE,arithmeticTheory.ADD_SUB]
5429QED
5430
5431(* ----------------------------------------------------------------------
5432 versions of constants with option outputs rather than unspecified
5433
5434 oHD : 'a list -> 'a option
5435 oEL : num -> 'a list -> 'a option
5436
5437 ---------------------------------------------------------------------- *)
5438
5439Definition oHD_def: oHD l = case l of [] => NONE | h::_ => SOME h
5440End
5441Theorem oHD_thm[simp]:
5442 (oHD [] = NONE) /\ (oHD (h::t) = SOME h)
5443Proof
5444 rw[oHD_def]
5445QED
5446
5447Definition oEL_def:
5448 (oEL n [] = NONE) /\
5449 (oEL n (x::xs) = if n = 0 then SOME x else oEL (n - 1) xs)
5450End
5451
5452Theorem oEL_THM:
5453 !xs n. oEL n xs = if n < LENGTH xs then SOME (EL n xs) else NONE
5454Proof
5455 Induct >> fs[oEL_def] >> rw[] >> fs[]
5456 >- (Q.RENAME_TAC [‘n < SUC (LENGTH xs)’] >> Cases_on ‘n’ >> fs[]) >>
5457 rw[] >> ASSUME_TAC (numLib.DECIDE “!x. 1 + x = SUC x”) >>
5458 fs[arithmeticTheory.NOT_ZERO_LT_ZERO] >>
5459 METIS_TAC[ONE, arithmeticTheory.LESS_LESS_SUC]
5460QED
5461
5462Theorem oEL_EQ_EL:
5463 !xs n y. (oEL n xs = SOME y) <=> n < LENGTH xs /\ (y = EL n xs)
5464Proof
5465 simp[oEL_THM] >> METIS_TAC[]
5466QED
5467
5468Theorem oEL_DROP:
5469 oEL n (DROP m xs) = oEL (m + n) xs
5470Proof
5471 MAP_EVERY Q.ID_SPEC_TAC [‘n’, ‘m’, ‘xs’] >> Induct_on ‘xs’ >>
5472 simp[DROP_def, oEL_def] >> rw[oEL_def] >> fs[] >>
5473 Q.RENAME_TAC [‘m - 1 + n’] >>
5474 ‘m - 1 + n = m + n - 1’ suffices_by simp[] >>
5475 Q.UNDISCH_THEN ‘m <> 0’ MP_TAC >> numLib.ARITH_TAC
5476QED
5477
5478Theorem oEL_TAKE_E:
5479 (oEL n (TAKE m xs) = SOME x) ==> (oEL n xs = SOME x)
5480Proof
5481 MAP_EVERY Q.ID_SPEC_TAC [‘n’, ‘m’, ‘xs’] >> Induct_on ‘xs’ >>
5482 simp[TAKE_def, oEL_def] >> rw[oEL_def] >> RES_TAC
5483QED
5484
5485Theorem oEL_LUPDATE:
5486 !xs i n x. oEL n (LUPDATE x i xs) =
5487 if i <> n then oEL n xs else
5488 if i < LENGTH xs then SOME x else NONE
5489Proof
5490 Induct >> fs[oEL_def,LUPDATE_def] >>
5491 Cases_on ‘i’ >> rw[oEL_def,LUPDATE_def] >> fs[] >> rw[] >>
5492 fs[numLib.DECIDE “!x. SUC (x - 1) <> x <=> (x = 0)”,
5493 numLib.DECIDE “!x. 1 + x = SUC x”]
5494QED
5495
5496(* ----------------------------------------------------------------------
5497 adjacent : 'a list -> 'a -> 'a -> bool
5498
5499 adjacent L a b is true if b immediately follows a somewhere in list L
5500 ---------------------------------------------------------------------- *)
5501
5502Inductive adjacent:
5503 (!a b t. adjacent (a::b::t) a b) /\
5504 (!a b h t. adjacent t a b ==> adjacent (h::t) a b)
5505End
5506
5507Theorem adjacent_thm[simp]:
5508 adjacent [] a b = F /\
5509 adjacent [e] a b = F /\
5510 adjacent (a::b::t) a b = T
5511Proof
5512 rpt conj_tac >> simp[Once adjacent_cases] >> Induct_on ‘adjacent’ >>
5513 simp[]
5514QED
5515
5516Theorem adjacent_iff:
5517 adjacent (h1::h2::t) a b <=> h1 = a /\ h2 = b \/ adjacent (h2::t) a b
5518Proof
5519 simp[EQ_IMP_THM, DISJ_IMP_THM, adjacent_rules] >>
5520 map_every Q.ID_SPEC_TAC [‘a’, ‘b’, ‘h1’, ‘h2’, ‘t’] >>
5521 Induct_on ‘adjacent’ >> simp[]
5522QED
5523
5524Theorem adjacent_EL:
5525 adjacent L a b <=> ?i. i + 1 < LENGTH L /\ a = EL i L /\ b = EL (i + 1) L
5526Proof
5527 eq_tac
5528 >- (Induct_on ‘adjacent’ >> simp[PULL_EXISTS] >> rw[]
5529 >- (Q.EXISTS_TAC ‘0’ >> simp[]) >>
5530 Q.RENAME_TAC [‘i + 1 < LENGTH L’] >> Q.EXISTS_TAC ‘SUC i’ >>
5531 simp[ADD_CLAUSES]) >>
5532 simp[PULL_EXISTS] >> Q.ID_SPEC_TAC ‘L’ >> Induct_on ‘i’ >>
5533 Cases >> simp[]
5534 >- (Q.RENAME_TAC [‘1 < SUC (LENGTH L)’] >> Cases_on ‘L’ >> simp[]) >>
5535 simp[ADD_CLAUSES, adjacent_rules]
5536QED
5537
5538Theorem adjacent_MAP:
5539 !xs a b f.
5540 adjacent (MAP f xs) a b <=> ?x y. adjacent xs x y /\ a = f x /\ b = f y
5541Proof
5542 Induct_on ‘xs’ >> simp[] >> Cases_on ‘xs’ >> gvs[] >>
5543 simp[adjacent_iff, SF DNF_ss] >> metis_tac[]
5544QED
5545
5546Theorem adjacent_MEM:
5547 !xs a b. adjacent xs a b ==> MEM a xs /\ MEM b xs
5548Proof
5549 simp[MEM_EL, adjacent_EL, PULL_EXISTS] >> rpt strip_tac >>
5550 rpt (irule_at Any EQ_REFL) >> simp[]
5551QED
5552
5553Theorem adjacent_ps_append:
5554 !xs a b. adjacent xs a b <=> ?p s. xs = p ++ [a;b] ++ s
5555Proof
5556 simp[adjacent_EL, PULL_EXISTS, EQ_IMP_THM] >> rw[]
5557 >- (Q.RENAME_TAC [‘i + 1 < LENGTH xs’] >>
5558 MAP_EVERY Q.EXISTS_TAC [‘TAKE i xs’, ‘DROP (i + 2) xs’] >>
5559 simp[LIST_EQ_REWRITE, EL_APPEND_EQN, EL_TAKE, EL_DROP] >> rw[] >>
5560 Q.RENAME_TAC [‘~(j < i)’, ‘j < i + 2’] >>
5561 ‘j = i \/ j = i + 1’ by simp[] >> simp[]) >>
5562 Q.EXISTS_TAC ‘LENGTH p’ >> simp[EL_APPEND_EQN]
5563QED
5564
5565Theorem adjacent_append1:
5566 !xs ys a b. adjacent xs a b ==> adjacent (xs ++ ys) a b
5567Proof
5568 Induct_on ‘adjacent’ >> simp[] >> metis_tac[adjacent_rules]
5569QED
5570
5571Theorem adjacent_append2:
5572 !xs ys a b. adjacent ys a b ==> adjacent (xs ++ ys) a b
5573Proof
5574 simp[adjacent_ps_append, PULL_EXISTS, APPEND_ASSOC] >> rpt strip_tac >>
5575 irule_at Any EQ_REFL
5576QED
5577
5578Theorem adjacent_REVERSE[simp]:
5579 !xs a b. adjacent (REVERSE xs) a b <=> adjacent xs b a
5580Proof
5581 simp[adjacent_ps_append, EQ_IMP_THM, PULL_EXISTS] >> rw[]
5582 >- (pop_assum (mp_tac o Q.AP_TERM ‘REVERSE’) >>
5583 REWRITE_TAC[REVERSE_REVERSE] >> simp[REVERSE_APPEND] >>
5584 strip_tac >> Q.EXISTS_TAC ‘REVERSE s’ >>
5585 simp[GSYM APPEND_ASSOC, APPEND_11]) >>
5586 simp[REVERSE_APPEND, APPEND_ASSOC] >>
5587 Q.EXISTS_TAC ‘REVERSE s’ >> simp[GSYM APPEND_ASSOC, APPEND_11]
5588QED
5589
5590(* ---------------------------------------------------------------------- *)
5591
5592Theorem lazy_list_case_compute[compute] =
5593 computeLib.lazyfy_thm list_case_compute;
5594
5595val _ = computeLib.add_persistent_funs [
5596 "APPEND", "APPEND_NIL", "FLAT", "HD", "TL", "LENGTH", "MAP", "MAP2",
5597 "NULL_DEF", "MEM", "EXISTS_DEF", "DROP_compute", "EVERY_DEF", "ZIP",
5598 "FILTER", "FOLDL", "FOLDR",
5599 "TAKE_compute", "FOLDL", "REVERSE_REV", "SUM_SUM_ACC", "ALL_DISTINCT",
5600 "GENLIST_AUX", "EL_restricted", "EL_simp_restricted",
5601 "GENLIST_NUMERALS", "list_size_def", "FRONT_DEF",
5602 "LAST_compute", "isPREFIX"
5603 ]
5604
5605val _ =
5606 let
5607 val list_info = Option.valOf (TypeBase.read {Thy = "list", Tyop="list"})
5608 val lift_list =
5609 mk_var ("listSyntax.lift_list",
5610 “:'type -> ('a -> 'term) -> 'a list -> 'term”)
5611 val list_info' =
5612 list_info |> TypeBasePure.put_lift lift_list
5613 |> TypeBasePure.put_induction
5614 (TypeBasePure.ORIG list_induction)
5615 |> TypeBasePure.put_nchotomy list_nchotomy
5616 in
5617 (* this exports a tyinfo with simpls included, but that's OK given how
5618 small they are; seems easier than taking them out again only for the
5619 benefit of a tiny amount of file size in the .dat file *)
5620 TypeBase.export [list_info']
5621 end;
5622
5623val _ = export_rewrites
5624 ["APPEND_11",
5625 "MAP2", "NULL_DEF",
5626 "SUM", "APPEND_ASSOC", "CONS", "CONS_11",
5627 "LENGTH_MAP",
5628 "NOT_CONS_NIL", "NOT_NIL_CONS",
5629 "CONS_ACYCLIC", "list_case_def",
5630 "ZIP", "UNZIP", "ZIP_UNZIP", "UNZIP_ZIP",
5631 "LENGTH_ZIP", "LENGTH_UNZIP",
5632 "EVERY_APPEND", "EXISTS_APPEND", "EVERY_SIMP",
5633 "NOT_EVERY", "NOT_EXISTS",
5634 "FOLDL", "FOLDR", "LENGTH_LUPDATE",
5635 "LUPDATE_LENGTH"];
5636
5637val _ =
5638 monadsyntax.declare_monad (
5639 "list",
5640 { bind = “LIST_BIND”, ignorebind = SOME “LIST_IGNORE_BIND”,
5641 unit = “SINGL”, choice = SOME “APPEND”, fail = SOME “[]”,
5642 guard = SOME “LIST_GUARD” }
5643 )
5644
5645(* ----------------------------------------------------------------------
5646 Supporting the quotient package
5647 ---------------------------------------------------------------------- *)
5648
5649Theorem LIST_EQUIV[quotient_equiv]:
5650 !R:'a -> 'a -> bool. EQUIV R ==> EQUIV (LIST_REL R)
5651Proof
5652 simp[EQUIV_def] >> simp[GSYM ALT_equivalence] >>
5653 simp[equivalence_def, reflexive_def, symmetric_def, transitive_def] >>
5654 rpt strip_tac
5655 >- (irule EVERY2_refl >> simp[])
5656 >- (‘!l1 l2. LIST_REL R l1 l2 ==> LIST_REL R l2 l1’ suffices_by metis_tac[] >>
5657 Induct_on ‘LIST_REL’ >> simp[]) >>
5658 irule LIST_REL_trans >> first_assum $ irule_at Any >>
5659 fs[LIST_REL_EL_EQN] >> metis_tac[]
5660QED
5661
5662Theorem LIST_QUOTIENT[quotient]:
5663 !R (abs:'a -> 'b) rep.
5664 QUOTIENT R abs rep ==>
5665 QUOTIENT (LIST_REL R) (MAP abs) (MAP rep)
5666Proof
5667 rw[] >> simp[QUOTIENT_def] >> rpt conj_tac
5668 >- (drule QUOTIENT_ABS_REP >> simp[MAP_MAP_o, o_DEF])
5669 >- (dxrule QUOTIENT_REP_REFL >> simp[LIST_REL_EL_EQN, EL_MAP]) >>
5670 dxrule_then assume_tac QUOTIENT_REL >>
5671 Induct >- simp[SF CONJ_ss] >>
5672 pop_assum (fn lrth => pop_assum (fn rth =>
5673 simp[] >> simp[Once rth, Once lrth, SimpLHS])) >>
5674 Cases_on ‘s’ >> simp[] >> metis_tac[]
5675QED
5676
5677Theorem NIL_RSP[quotient_rsp]:
5678 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> LIST_REL R [] []
5679Proof
5680 simp[]
5681QED
5682
5683Theorem NIL_PRS[quotient_prs]:
5684 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> [] = (MAP abs) []
5685Proof
5686 simp[]
5687QED
5688
5689Theorem CONS_PRS[quotient_prs]:
5690 !R (abs:'a -> 'b) rep.
5691 QUOTIENT R abs rep ==>
5692 !t h. CONS h t = (MAP abs) (CONS (rep h) (MAP rep t))
5693Proof
5694 rpt strip_tac >> drule_then assume_tac QUOTIENT_ABS_REP >>
5695 simp[MAP_MAP_o, o_DEF]
5696QED
5697
5698Theorem CONS_RSP[quotient_rsp]:
5699 !R (abs:'a -> 'b) rep.
5700 QUOTIENT R abs rep ==>
5701 !t1 t2 h1 h2.
5702 R h1 h2 /\ (LIST_REL R) t1 t2 ==> (LIST_REL R) (CONS h1 t1) (CONS h2 t2)
5703Proof
5704 simp[]
5705QED
5706
5707
5708Theorem EVERY_PRS[quotient_prs]:
5709 !R (abs:'a -> 'b) rep.
5710 QUOTIENT R abs rep ==>
5711 !l P. EVERY P l = EVERY ((abs --> I) P) (MAP rep l)
5712Proof
5713 rpt strip_tac >> drule_then assume_tac QUOTIENT_ABS_REP >>
5714 simp[EVERY_MAP, FUN_MAP_THM, SF ETA_ss]
5715QED
5716
5717Theorem LIST_TO_SET_PRS[quotient_prs]:
5718 !R (abs : 'a -> 'b) rep.
5719 QUOTIENT R abs rep ==>
5720 !l. LIST_TO_SET l = IMAGE abs (LIST_TO_SET (MAP rep l))
5721Proof
5722 rpt strip_tac >> drule_then assume_tac QUOTIENT_ABS_REP >>
5723 simp[GSYM LIST_TO_SET_MAP, MAP_MAP_o, combinTheory.o_DEF]
5724QED
5725
5726Definition SET_REL_def:
5727 SET_REL R s1 s2 <=>
5728 ?ps. IMAGE FST ps = s1 /\ IMAGE SND ps = s2 /\
5729 !p. p IN ps ==> R (FST p) (SND p)
5730End
5731
5732Theorem SET_REL_EQ:
5733 SET_REL (=) = (=)
5734Proof
5735 simp[Once FUN_EQ_THM] >> simp[Once FUN_EQ_THM] >>
5736 simp[SET_REL_def, EQ_IMP_THM, FORALL_AND_THM, FORALL_PROD] >>
5737 conj_tac
5738 >- (simp[EXTENSION, EXISTS_PROD, PULL_EXISTS] >> metis_tac[]) >>
5739 Q.X_GEN_TAC ‘s’ >> Q.EXISTS_TAC ‘{(a,a) | a IN s}’ >>
5740 simp[EXTENSION, EXISTS_PROD]
5741QED
5742
5743Theorem SET_REL_THM:
5744 SET_REL R s1 s2 <=>
5745 (!x. x IN s1 ==> ?y. y IN s2 /\ R x y) /\
5746 (!y. y IN s2 ==> ?x. x IN s1 /\ R x y)
5747Proof
5748 simp[SET_REL_def, EQ_IMP_THM] >> rw[] >>
5749 FULL_SIMP_TAC (srw_ss()) [FORALL_PROD, PULL_EXISTS, EXISTS_PROD]
5750 >- metis_tac[]
5751 >- metis_tac[] >>
5752 FULL_SIMP_TAC (srw_ss()) [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] >>
5753 Q.RENAME_TAC [‘f _ IN s2 /\ R _ (f _)’, ‘g _ IN s1 /\ R (g _) _’] >>
5754 Q.EXISTS_TAC ‘{(x,f x) | x IN s1} UNION {(g y, y) | y IN s2}’ >>
5755 simp[EXTENSION, PULL_EXISTS, SF DNF_ss, EXISTS_PROD] >> metis_tac[]
5756QED
5757
5758Theorem SET_QUOTIENT:
5759 !R abs rep.
5760 QUOTIENT R (abs : 'a -> 'b) rep ==>
5761 QUOTIENT (SET_REL R) (IMAGE abs) (IMAGE rep)
5762Proof
5763 simp[QUOTIENT_def] >> rpt strip_tac >>
5764 pop_assum (assume_tac o GSYM)
5765 >- simp[IMAGE_IMAGE, combinTheory.o_DEF]
5766 >- (simp[SET_REL_THM, PULL_EXISTS] >> metis_tac[]) >>
5767 eq_tac >> simp[SET_REL_THM] >> rw[]
5768 >- metis_tac[]
5769 >- metis_tac[]
5770 >- metis_tac[]
5771 >- metis_tac[]
5772 >- (simp[EXTENSION] >> metis_tac[]) >>
5773 Q.PAT_X_ASSUM ‘IMAGE _ _ = IMAGE _ _’ MP_TAC >>
5774 simp[EXTENSION, PULL_EXISTS] >> metis_tac[]
5775QED
5776
5777Theorem LIST_TO_SET_RSP[quotient_rsp]:
5778 !R (abs:'a -> 'b) rep.
5779 QUOTIENT R abs rep ==>
5780 !l1 l2. LIST_REL R l1 l2 ==>
5781 SET_REL R (LIST_TO_SET l1) (LIST_TO_SET l2)
5782Proof
5783 simp[SET_REL_THM, LIST_REL_EL_EQN, MEM_EL, PULL_EXISTS] >>
5784 metis_tac[]
5785QED
5786
5787Theorem EVERY_RSP[quotient_rsp]:
5788 !R (abs:'a -> 'b) rep.
5789 QUOTIENT R abs rep ==>
5790 !l1 l2 P1 P2.
5791 (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
5792 (EVERY P1 l1 <=> EVERY P2 l2)
5793Proof
5794 simp[EVERY_MEM, FUN_REL] >> rpt strip_tac >>
5795 Q.PAT_X_ASSUM ‘LIST_REL _ _ _’ MP_TAC >>
5796 Induct_on ‘LIST_REL’ >> simp[DISJ_IMP_THM, FORALL_AND_THM] >>
5797 metis_tac[]
5798QED
5799
5800Theorem MAP_RSP[quotient_rsp]:
5801 !R1 (abs1:'a -> 'c) rep1.
5802 QUOTIENT R1 abs1 rep1 ==>
5803 !R2 (abs2:'b -> 'd) rep2.
5804 QUOTIENT R2 abs2 rep2 ==>
5805 !l1 l2 f1 f2.
5806 (R1 ===> R2) f1 f2 /\ (LIST_REL R1) l1 l2 ==>
5807 (LIST_REL R2) (MAP f1 l1) (MAP f2 l2)
5808Proof
5809 simp[FUN_REL] >> rpt strip_tac >>
5810 Q.PAT_X_ASSUM ‘LIST_REL _ _ _ ’ MP_TAC >>
5811 Induct_on ‘LIST_REL’ >> simp[]
5812QED
5813
5814Theorem MAP_PRS[quotient_prs]:
5815 !R1 (abs1:'a -> 'c) rep1.
5816 QUOTIENT R1 abs1 rep1 ==>
5817 !R2 (abs2:'b -> 'd) rep2.
5818 QUOTIENT R2 abs2 rep2 ==>
5819 !l f. MAP f l = (MAP abs2) (MAP ((abs1 --> rep2) f) (MAP rep1 l))
5820Proof
5821 rpt strip_tac >> rpt (dxrule_then assume_tac QUOTIENT_ABS_REP) >>
5822 simp[MAP_MAP_o, FUN_MAP, combinTheory.o_DEF, SF ETA_ss]
5823QED
5824
5825(*---------------------------------------------------------------------------*)
5826(* relation of list_size to other list operations. *)
5827(*---------------------------------------------------------------------------*)
5828
5829val ADD_AC = AC ADD_ASSOC ADD_SYM;
5830
5831Theorem list_size_reverse[simp]:
5832 list_size f (REVERSE l) = list_size f l
5833Proof
5834 Induct_on ‘l’ >> rw [list_size_append,ADD_AC]
5835QED
5836
5837Theorem list_size_map[simp]:
5838 list_size f (MAP g l) = list_size (λx. f (g x)) l
5839Proof
5840 Induct_on ‘l’ >> rw []
5841QED
5842
5843Theorem list_size_snoc[simp]:
5844 list_size f (SNOC x l) = list_size f (x::l)
5845Proof
5846 Induct_on ‘l’ >> rw [ADD_AC]
5847QED
5848
5849Theorem list_size_zip:
5850 ∀l1 l2.
5851 LENGTH l1 = LENGTH l2 ⇒
5852 list_size (pair_size f1 f2) (ZIP (l1,l2)) =
5853 list_size f1 l1 + list_size f2 l2
5854Proof
5855 Induction.recInduct ZIP_ind_alt >> rw[ADD_AC]
5856QED
5857
5858Theorem list_size_filter[simp]:
5859 list_size f (FILTER P l) <= list_size f l
5860Proof
5861 Induct_on ‘l’ >> rw [] >> numLib.DECIDE_TAC
5862QED
5863
5864Theorem filter_size_less[simp]:
5865 ∀h t. list_size f (FILTER P t) < list_size f (h::t)
5866Proof
5867 gen_tac >> Induct >> fs[] >> rw[] >> numLib.DECIDE_TAC
5868QED
5869
5870Theorem list_size_take[simp]:
5871 ∀l n. list_size f (TAKE n l) <= list_size f l
5872Proof
5873 Induct >> rw [] >> Cases_on ‘n’ >> rw[]
5874QED
5875
5876Theorem list_size_drop[simp]:
5877 ∀l n. list_size f (DROP n l) <= list_size f l
5878Proof
5879 Induct >> rw [] >> Cases_on ‘n’ >> rw[] >>
5880 pop_assum (mp_tac o Q.SPEC ‘n'’) >> numLib.DECIDE_TAC
5881QED
5882
5883val _ =
5884 List.app TotalDefn.export_termsimp
5885 ["list.list_size_append", "list.list_size_reverse",
5886 "list.list_size_map", "list.list_size_snoc", "list.list_size_zip"];