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