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