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(* ===================================================================== *) 18 19 20(* ---------------------------------------------------------------------- 21 Require ancestor theory structures to be present. The parents of list 22 are "arithmetic", "pair", "pred_set" and those theories behind the 23 datatype definition library 24 ---------------------------------------------------------------------- *) 25 26local 27 open arithmeticTheory pairTheory pred_setTheory Datatype 28 OpenTheoryMap 29in end; 30 31 32(*--------------------------------------------------------------------------- 33 * Open structures used in the body. 34 *---------------------------------------------------------------------------*) 35 36open HolKernel Parse boolLib Num_conv Prim_rec BasicProvers mesonLib 37 simpLib boolSimps pairTheory pred_setTheory TotalDefn metisLib 38 relationTheory combinTheory 39 40val ERR = mk_HOL_ERR "listScript" 41 42val arith_ss = bool_ss ++ numSimps.ARITH_ss ++ numSimps.REDUCE_ss 43fun simp l = ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss++numSimps.ARITH_ss) l 44 45val rw = SRW_TAC [] 46val metis_tac = METIS_TAC 47fun fs l = FULL_SIMP_TAC (srw_ss()) l 48 49 50val _ = new_theory "list"; 51 52val _ = Rewrite.add_implicit_rewrites pairTheory.pair_rws; 53val zDefine = Lib.with_flag (computeLib.auto_import_definitions, false) Define 54val dDefine = Lib.with_flag (Defn.def_suffix, "_DEF") Define 55val bDefine = Lib.with_flag (Defn.def_suffix, "") Define 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; 67 68val ADD_CLAUSES = arithmeticTheory.ADD_CLAUSES; 69val LESS_ADD_1 = arithmeticTheory.LESS_ADD_1; 70val LESS_EQ = arithmeticTheory.LESS_EQ; 71val NOT_LESS = arithmeticTheory.NOT_LESS; 72val LESS_EQ_ADD = arithmeticTheory.LESS_EQ_ADD; 73val num_CASES = arithmeticTheory.num_CASES; 74val LESS_MONO_EQ = arithmeticTheory.LESS_MONO_EQ; 75val LESS_MONO_EQ = arithmeticTheory.LESS_MONO_EQ; 76val ADD_EQ_0 = arithmeticTheory.ADD_EQ_0; 77val ONE = arithmeticTheory.ONE; 78val PAIR_EQ = pairTheory.PAIR_EQ; 79 80(*---------------------------------------------------------------------------*) 81(* Declare the datatype of lists *) 82(*---------------------------------------------------------------------------*) 83 84val _ = Datatype.Hol_datatype `list = NIL | CONS of 'a => list`; 85 86local open OpenTheoryMap in 87val ns = ["Data","List"] 88val _ = OpenTheory_tyop_name{tyop={Thy="list",Tyop="list"},name=(ns,"list")} 89val _ = OpenTheory_const_name{const={Thy="list",Name="APPEND"},name=(ns,"@")} 90val _ = OpenTheory_const_name{const={Thy="list",Name="CONS"},name=(ns,"::")} 91val _ = OpenTheory_const_name{const={Thy="list",Name="HD"},name=(ns,"head")} 92val _ = OpenTheory_const_name{const={Thy="list",Name="EVERY"},name=(ns,"all")} 93val _ = OpenTheory_const_name{const={Thy="list",Name="EXISTS"},name=(ns,"any")} 94val _ = OpenTheory_const_name{const={Thy="list",Name="FILTER"},name=(ns,"filter")} 95val _ = OpenTheory_const_name{const={Thy="list",Name="FLAT"},name=(ns,"concat")} 96val _ = OpenTheory_const_name{const={Thy="list",Name="LENGTH"},name=(ns,"length")} 97val _ = OpenTheory_const_name{const={Thy="list",Name="MAP"},name=(ns,"map")} 98val _ = OpenTheory_const_name{const={Thy="list",Name="NIL"},name=(ns,"[]")} 99val _ = OpenTheory_const_name{const={Thy="list",Name="REVERSE"},name=(ns,"reverse")} 100val _ = OpenTheory_const_name{const={Thy="list",Name="TAKE"},name=(ns,"take")} 101val _ = OpenTheory_const_name{const={Thy="list",Name="TL"},name=(ns,"tail")} 102end 103 104(*---------------------------------------------------------------------------*) 105(* Fiddle with concrete syntax *) 106(*---------------------------------------------------------------------------*) 107 108val _ = add_rule {term_name = "CONS", fixity = Infixr 490, 109 pp_elements = [TOK "::", BreakSpace(0,2)], 110 paren_style = OnlyIfNecessary, 111 block_style = (AroundSameName, (PP.INCONSISTENT, 2))}; 112 113val _ = add_listform {separator = [TOK ";", BreakSpace(1,0)], 114 leftdelim = [TOK "["], rightdelim = [TOK "]"], 115 cons = "CONS", nilstr = "NIL", 116 block_info = (PP.INCONSISTENT, 1)}; 117 118(*---------------------------------------------------------------------------*) 119(* Prove the axiomatization of lists *) 120(*---------------------------------------------------------------------------*) 121 122val list_Axiom = TypeBase.axiom_of ``:'a list``; 123 124val list_Axiom_old = store_thm( 125 "list_Axiom_old", 126 Term`!x f. ?!fn1:'a list -> 'b. 127 (fn1 [] = x) /\ (!h t. fn1 (h::t) = f (fn1 t) h t)`, 128 REPEAT GEN_TAC THEN CONV_TAC EXISTS_UNIQUE_CONV THEN CONJ_TAC THENL [ 129 ASSUME_TAC list_Axiom THEN 130 POP_ASSUM (ACCEPT_TAC o BETA_RULE o Q.SPECL [`x`, `\x y z. f z x y`]), 131 REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN 132 HO_MATCH_MP_TAC (TypeBase.induction_of ``:'a list``) THEN 133 simpLib.ASM_SIMP_TAC boolSimps.bool_ss [] 134 ]); 135 136(*--------------------------------------------------------------------------- 137 Now some definitions. 138 ---------------------------------------------------------------------------*) 139 140val NULL_DEF = new_recursive_definition 141 {name = "NULL_DEF", 142 rec_axiom = list_Axiom, 143 def = ���(NULL [] = T) /\ 144 (NULL (h::t) = F)���}; 145 146val HD = new_recursive_definition 147 {name = "HD", 148 rec_axiom = list_Axiom, 149 def = ���HD (h::t) = h���}; 150val _ = export_rewrites ["HD"] 151 152val TL = new_recursive_definition 153 {name = "TL", 154 rec_axiom = list_Axiom, 155 def = ���TL (h::t) = t���}; 156val _ = export_rewrites ["TL"] 157 158val SUM = new_recursive_definition 159 {name = "SUM", 160 rec_axiom = list_Axiom, 161 def = ���(SUM [] = 0) /\ 162 (!h t. SUM (h::t) = h + SUM t)���}; 163 164val APPEND = new_recursive_definition 165 {name = "APPEND", 166 rec_axiom = list_Axiom, 167 def = ���(!l:'a list. APPEND [] l = l) /\ 168 (!l1 l2 h. APPEND (h::l1) l2 = h::APPEND l1 l2)���}; 169val _ = export_rewrites ["APPEND"] 170 171val _ = set_fixity "++" (Infixl 480); 172val _ = overload_on ("++", Term`APPEND`); 173val _ = Unicode.unicode_version {u = UnicodeChars.doubleplus, tmnm = "++"} 174val _ = TeX_notation { hol = UnicodeChars.doubleplus, 175 TeX = ("\\HOLTokenDoublePlus", 1) } 176 177val FLAT = new_recursive_definition 178 {name = "FLAT", 179 rec_axiom = list_Axiom, 180 def = ���(FLAT [] = []) /\ 181 (!h t. FLAT (h::t) = APPEND h (FLAT t))���}; 182val _ = export_rewrites ["FLAT"] 183 184val LENGTH = new_recursive_definition 185 {name = "LENGTH", 186 rec_axiom = list_Axiom, 187 def = ���(LENGTH [] = 0) /\ 188 (!(h:'a) t. LENGTH (h::t) = SUC (LENGTH t))���}; 189val _ = export_rewrites ["LENGTH"] 190 191val MAP = new_recursive_definition 192 {name = "MAP", 193 rec_axiom = list_Axiom, 194 def = ���(!f:'a->'b. MAP f [] = []) /\ 195 (!f h t. MAP f (h::t) = f h::MAP f t)���}; 196val _ = export_rewrites ["MAP"] 197 198val LIST_TO_SET_DEF = new_recursive_definition{ 199 name = "LIST_TO_SET_DEF", 200 rec_axiom = list_Axiom, 201 def = ``(!x:'a. LIST_TO_SET [] x <=> F) /\ 202 (!h:'a t x. LIST_TO_SET (h::t) x = (x = h) \/ LIST_TO_SET t x)``} 203val _ = export_rewrites ["LIST_TO_SET_DEF"] 204 205val _ = overload_on ("set", ``LIST_TO_SET``) 206val _ = overload_on ("MEM", ``\h:'a l:'a list. h IN LIST_TO_SET l``) 207val _ = overload_on ("", ``\h:'a l:'a list. ~(h IN LIST_TO_SET l)``) 208 (* last over load here causes the term ~(h IN LIST_TO_SET l) to not print 209 using overloads. In particular, this prevents the existing overload for 210 NOTIN from firing in this type instance, and allows ~MEM a l to print 211 because the pretty-printer will traverse into the negated term (printing 212 the ~), and then the MEM overload will "fire". 213 *) 214 215val LIST_TO_SET = store_thm( 216 "LIST_TO_SET", 217 ``(LIST_TO_SET [] = {}) /\ 218 (LIST_TO_SET (h::t) = h INSERT LIST_TO_SET t)``, 219 SRW_TAC [] [FUN_EQ_THM, IN_DEF]); 220val _ = export_rewrites ["LIST_TO_SET"] 221 222val FILTER = new_recursive_definition 223 {name = "FILTER", 224 rec_axiom = list_Axiom, 225 def = ���(!P. FILTER P [] = []) /\ 226 (!(P:'a->bool) h t. 227 FILTER P (h::t) = 228 if P h then (h::FILTER P t) else FILTER P t)���}; 229val _ = export_rewrites ["FILTER"] 230 231val FOLDR = new_recursive_definition 232 {name = "FOLDR", 233 rec_axiom = list_Axiom, 234 def = ���(!f e. FOLDR (f:'a->'b->'b) e [] = e) /\ 235 (!f e x l. FOLDR f e (x::l) = f x (FOLDR f e l))���}; 236 237val FOLDL = new_recursive_definition 238 {name = "FOLDL", 239 rec_axiom = list_Axiom, 240 def = ���(!f e. FOLDL (f:'b->'a->'b) e [] = e) /\ 241 (!f e x l. FOLDL f e (x::l) = FOLDL f (f e x) l)���}; 242 243val EVERY_DEF = new_recursive_definition 244 {name = "EVERY_DEF", 245 rec_axiom = list_Axiom, 246 def = ���(!P:'a->bool. EVERY P [] = T) /\ 247 (!P h t. EVERY P (h::t) = P h /\ EVERY P t)���}; 248val _ = export_rewrites ["EVERY_DEF"] 249 250val EXISTS_DEF = new_recursive_definition 251 {name = "EXISTS_DEF", 252 rec_axiom = list_Axiom, 253 def = ���(!P:'a->bool. EXISTS P [] = F) 254 /\ (!P h t. EXISTS P (h::t) = P h \/ EXISTS P t)���}; 255val _ = export_rewrites ["EXISTS_DEF"] 256 257val EL = new_recursive_definition 258 {name = "EL", 259 rec_axiom = num_Axiom, 260 def = ���(!l. EL 0 l = (HD l:'a)) /\ 261 (!l:'a list. !n. EL (SUC n) l = EL n (TL l))���}; 262 263 264 265(* ---------------------------------------------------------------------*) 266(* Definition of a function *) 267(* *) 268(* MAP2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list *) 269(* *) 270(* for mapping a curried binary function down a pair of lists: *) 271(* *) 272(* |- (!f. MAP2 f[][] = []) /\ *) 273(* (!f h1 t1 h2 t2. *) 274(* MAP2 f(h1::t1)(h2::t2) = CONS(f h1 h2)(MAP2 f t1 t2)) *) 275(* *) 276(* [TFM 92.04.21] *) 277(* ---------------------------------------------------------------------*) 278 279val MAP2_DEF = dDefine` 280 (MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2) /\ 281 (MAP2 f x y = [])`; 282val _ = export_rewrites ["MAP2_DEF"] 283 284val MAP2 = store_thm ("MAP2", 285``(!f. MAP2 f [] [] = []) /\ 286 (!f h1 t1 h2 t2. MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2)``, 287METIS_TAC[MAP2_DEF]); 288 289val MAP2_NIL = Q.store_thm( 290 "MAP2_NIL[simp]", 291 `MAP2 f x [] = []`, 292 Cases_on `x` >> simp[]) 293 294val LENGTH_MAP2 = Q.store_thm ("LENGTH_MAP2[simp]", 295 `!xs ys. LENGTH (MAP2 f xs ys) = MIN (LENGTH xs) (LENGTH ys)`, 296 Induct \\ rw [] \\ Cases_on `ys` \\ fs [arithmeticTheory.MIN_DEF, MAP2_DEF] 297 \\ SRW_TAC[][]); 298 299val EL_MAP2 = Q.store_thm("EL_MAP2", 300 `!ts tt n. 301 n < MIN (LENGTH ts) (LENGTH tt) ==> 302 (EL n (MAP2 f ts tt) = f (EL n ts) (EL n tt))`, 303 Induct \\ rw [] \\ Cases_on `tt` \\ Cases_on `n` \\ fs [EL]); 304 305(* Some searches *) 306 307val INDEX_FIND_def = Define` 308 (INDEX_FIND i P [] = NONE) /\ 309 (INDEX_FIND i P (h :: t) = 310 if P h then SOME (i, h) else INDEX_FIND (SUC i) P t)`; 311 312val FIND_def = Define `FIND P = OPTION_MAP SND o INDEX_FIND 0 P` 313val INDEX_OF_def = Define `INDEX_OF x = OPTION_MAP FST o INDEX_FIND 0 ($= x)` 314 315(* ---------------------------------------------------------------------*) 316(* Proofs of some theorems about lists. *) 317(* ---------------------------------------------------------------------*) 318 319val NULL = store_thm ("NULL", 320 ���NULL ([] :'a list) /\ (!h t. ~NULL(CONS (h:'a) t))���, 321 REWRITE_TAC [NULL_DEF]); 322 323(*---------------------------------------------------------------------------*) 324(* List induction *) 325(* |- P [] /\ (!t. P t ==> !h. P(h::t)) ==> (!x.P x) *) 326(*---------------------------------------------------------------------------*) 327 328val list_INDUCT0 = save_thm("list_INDUCT0",TypeBase.induction_of ``:'a list``); 329 330val list_INDUCT = Q.store_thm 331("list_INDUCT", 332 `!P. P [] /\ (!t. P t ==> !h. P (h::t)) ==> !l. P l`, 333 REWRITE_TAC [list_INDUCT0]); (* must use REWRITE_TAC, ACCEPT_TAC refuses 334 to respect bound variable names *) 335 336val list_induction = save_thm("list_induction", list_INDUCT); 337val LIST_INDUCT_TAC = INDUCT_THEN list_INDUCT ASSUME_TAC; 338 339(*---------------------------------------------------------------------------*) 340(* List induction as a rewrite rule. *) 341(* |- (!l. P l) = P [] /\ !h t. P t ==> P (h::t) *) 342(*---------------------------------------------------------------------------*) 343 344val FORALL_LIST = Q.store_thm 345 ("FORALL_LIST", 346 `(!l. P l) = P [] /\ !h t. P t ==> P (h::t)`, 347 METIS_TAC [list_INDUCT]); 348 349(*---------------------------------------------------------------------------*) 350(* Cases theorem: |- !l. (l = []) \/ (?t h. l = h::t) *) 351(*---------------------------------------------------------------------------*) 352 353val list_cases = TypeBase.nchotomy_of ``:'a list``; 354 355 356val list_CASES = store_thm 357("list_CASES", 358 ���!l. (l = []) \/ (?h t. l = h::t)���, 359 mesonLib.MESON_TAC [list_cases]); 360 361val list_nchotomy = save_thm("list_nchotomy", list_CASES); 362 363(*---------------------------------------------------------------------------*) 364(* Definition of list_case more suitable to call-by-value computations *) 365(*---------------------------------------------------------------------------*) 366 367val list_case_def = TypeBase.case_def_of ``:'a list``; 368 369val list_case_compute = store_thm("list_case_compute", 370 ���!(l:'a list). list_CASE l (b:'b) f = 371 if NULL l then b else f (HD l) (TL l)���, 372 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [list_case_def, HD, TL, NULL_DEF]); 373 374(*---------------------------------------------------------------------------*) 375(* CONS_11: |- !h t h' t'. (h::t = h' :: t') = (h = h') /\ (t = t') *) 376(*---------------------------------------------------------------------------*) 377 378val CONS_11 = save_thm("CONS_11", TypeBase.one_one_of ``:'a list``) 379 380val NOT_NIL_CONS = save_thm("NOT_NIL_CONS", TypeBase.distinct_of ``:'a list``); 381 382val NOT_CONS_NIL = save_thm("NOT_CONS_NIL", 383 CONV_RULE(ONCE_DEPTH_CONV SYM_CONV) NOT_NIL_CONS); 384 385val LIST_NOT_EQ = store_thm("LIST_NOT_EQ", 386 ���!l1 l2. ~(l1 = l2) ==> !h1:'a. !h2. ~(h1::l1 = h2::l2)���, 387 REPEAT GEN_TAC THEN 388 STRIP_TAC THEN 389 ASM_REWRITE_TAC [CONS_11]); 390 391val NOT_EQ_LIST = store_thm("NOT_EQ_LIST", 392 ���!h1:'a. !h2. ~(h1 = h2) ==> !l1 l2. ~(h1::l1 = h2::l2)���, 393 REPEAT GEN_TAC THEN 394 STRIP_TAC THEN 395 ASM_REWRITE_TAC [CONS_11]); 396 397val EQ_LIST = store_thm("EQ_LIST", 398 ���!h1:'a.!h2.(h1=h2) ==> !l1 l2. (l1 = l2) ==> (h1::l1 = h2::l2)���, 399 REPEAT STRIP_TAC THEN 400 ASM_REWRITE_TAC [CONS_11]); 401 402 403val CONS = store_thm ("CONS", 404 ���!l : 'a list. ~NULL l ==> (HD l :: TL l = l)���, 405 STRIP_TAC THEN 406 STRIP_ASSUME_TAC (SPEC (���l:'a list���) list_CASES) THEN 407 POP_ASSUM SUBST1_TAC THEN 408 ASM_REWRITE_TAC [HD, TL, NULL]); 409 410val APPEND_NIL = store_thm("APPEND_NIL", 411���!(l:'a list). APPEND l [] = l���, 412 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [APPEND]); 413val _ = export_rewrites ["APPEND_NIL"] 414 415 416val APPEND_ASSOC = store_thm ("APPEND_ASSOC", 417 ���!(l1:'a list) l2 l3. 418 APPEND l1 (APPEND l2 l3) = (APPEND (APPEND l1 l2) l3)���, 419 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [APPEND]); 420 421val LENGTH_APPEND = store_thm ("LENGTH_APPEND", 422 ���!(l1:'a list) (l2:'a list). 423 LENGTH (APPEND l1 l2) = (LENGTH l1) + (LENGTH l2)���, 424 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [LENGTH, APPEND, ADD_CLAUSES]); 425val _ = export_rewrites ["LENGTH_APPEND"] 426 427val MAP_APPEND = store_thm ("MAP_APPEND", 428 ���!(f:'a->'b).!l1 l2. MAP f (APPEND l1 l2) = APPEND (MAP f l1) (MAP f l2)���, 429 STRIP_TAC THEN 430 LIST_INDUCT_TAC THEN 431 ASM_REWRITE_TAC [MAP, APPEND]); 432 433val MAP_ID = store_thm( 434 "MAP_ID", 435 ``(MAP (\x. x) l = l) /\ (MAP I l = l)``, 436 Induct_on `l` THEN SRW_TAC [] [MAP]); 437val _ = export_rewrites ["MAP_ID"] 438 439val LENGTH_MAP = store_thm ("LENGTH_MAP", 440 ���!l. !(f:'a->'b). LENGTH (MAP f l) = LENGTH l���, 441 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [MAP, LENGTH]); 442 443val MAP_EQ_NIL = store_thm( 444 "MAP_EQ_NIL[simp]", 445 ���!(l:'a list) (f:'a->'b). 446 ((MAP f l = []) = (l = [])) /\ 447 (([] = MAP f l) = (l = []))���, 448 LIST_INDUCT_TAC THEN REWRITE_TAC [MAP, NOT_CONS_NIL, NOT_NIL_CONS]); 449 450val MAP_EQ_CONS = store_thm( 451 "MAP_EQ_CONS", 452 ``(MAP (f:'a -> 'b) l = h::t) <=> 453 ?x0 t0. (l = x0::t0) /\ (h = f x0) /\ (t = MAP f t0)``, 454 Q.ISPEC_THEN `l` STRUCT_CASES_TAC list_CASES THEN SIMP_TAC (srw_ss()) [] THEN 455 METIS_TAC[]); 456 457val MAP_EQ_SING = store_thm( 458 "MAP_EQ_SING[simp]", 459 ``(MAP (f:'a -> 'b) l = [x]) <=> ?x0. (l = [x0]) /\ (x = f x0)``, 460 SIMP_TAC (srw_ss()) [MAP_EQ_CONS]) 461 462val MAP_EQ_f = store_thm ("MAP_EQ_f", 463 ``!f1 f2 l. (MAP f1 l = MAP f2 l) = (!e. MEM e l ==> (f1 e = f2 e))``, 464 Induct_on `l` THEN 465 ASM_SIMP_TAC (srw_ss()) [DISJ_IMP_THM, MAP, CONS_11, FORALL_AND_THM]) 466 467val MAP_o = store_thm("MAP_o", 468 (���!f:'b->'c. !g:'a->'b. MAP (f o g) = (MAP f) o (MAP g)���), 469 REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV 470 THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [MAP, o_THM]); 471 472val MAP_MAP_o = store_thm("MAP_MAP_o", 473 (���!(f:'b->'c) (g:'a->'b) l. MAP f (MAP g l) = MAP (f o g) l���), 474 REPEAT GEN_TAC THEN REWRITE_TAC [MAP_o, o_DEF] 475 THEN BETA_TAC THEN REFL_TAC); 476 477val EL_MAP = store_thm("EL_MAP", 478 (���!n l. n < (LENGTH l) ==> !f:'a->'b. EL n (MAP f l) = f (EL n l)���), 479 INDUCT_TAC THEN LIST_INDUCT_TAC 480 THEN ASM_REWRITE_TAC[LENGTH, EL, MAP, LESS_MONO_EQ, NOT_LESS_0, HD, TL]); 481 482val EL_APPEND_EQN = store_thm( 483 "EL_APPEND_EQN", 484 ``!l1 l2 n. 485 EL n (l1 ++ l2) = 486 if n < LENGTH l1 then EL n l1 else EL (n - LENGTH l1) l2``, 487 LIST_INDUCT_TAC >> simp_tac (srw_ss()) [] >> Cases_on `n` >> 488 asm_simp_tac (srw_ss()) [EL]) 489 490val MAP_TL = Q.store_thm("MAP_TL", 491 `!l f. ~NULL l ==> (MAP f (TL l) = TL (MAP f l))`, 492 Induct THEN REWRITE_TAC [NULL_DEF, TL, MAP]); 493 494val EVERY_EL = store_thm ("EVERY_EL", 495 ���!(l:'a list) P. EVERY P l = !n. n < LENGTH l ==> P (EL n l)���, 496 LIST_INDUCT_TAC THEN 497 ASM_REWRITE_TAC [EVERY_DEF, LENGTH, NOT_LESS_0] THEN 498 REPEAT STRIP_TAC THEN EQ_TAC THENL 499 [STRIP_TAC THEN INDUCT_TAC THENL 500 [ASM_REWRITE_TAC [EL, HD], 501 ASM_REWRITE_TAC [LESS_MONO_EQ, EL, TL]], 502 REPEAT STRIP_TAC THENL 503 [POP_ASSUM (MP_TAC o (SPEC (���0���))) THEN 504 REWRITE_TAC [LESS_0, EL, HD], 505 POP_ASSUM ((ANTE_RES_THEN ASSUME_TAC) o (MATCH_MP LESS_MONO)) THEN 506 POP_ASSUM MP_TAC THEN REWRITE_TAC [EL, TL]]]); 507 508val EVERY_CONJ = store_thm("EVERY_CONJ", 509 ���!P Q l. EVERY (\(x:'a). (P x) /\ (Q x)) l = (EVERY P l /\ EVERY Q l)���, 510 NTAC 2 GEN_TAC THEN LIST_INDUCT_TAC THEN 511 ASM_REWRITE_TAC [EVERY_DEF] THEN 512 CONV_TAC (DEPTH_CONV BETA_CONV) THEN 513 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN 514 FIRST_ASSUM ACCEPT_TAC); 515 516val EVERY_MEM = store_thm( 517 "EVERY_MEM", 518 ``!P l:'a list. EVERY P l = !e. MEM e l ==> P e``, 519 GEN_TAC THEN LIST_INDUCT_TAC THEN 520 ASM_REWRITE_TAC [EVERY_DEF, LIST_TO_SET, IN_INSERT, NOT_IN_EMPTY] THEN 521 mesonLib.MESON_TAC []); 522 523val EVERY_MAP = store_thm( 524 "EVERY_MAP", 525 ``!P f l:'a list. EVERY P (MAP f l) = EVERY (\x. P (f x)) l``, 526 NTAC 2 GEN_TAC THEN LIST_INDUCT_TAC THEN 527 ASM_REWRITE_TAC [EVERY_DEF, MAP] THEN BETA_TAC THEN REWRITE_TAC []); 528 529val EVERY_SIMP = store_thm( 530 "EVERY_SIMP", 531 ``!c l:'a list. EVERY (\x. c) l = (l = []) \/ c``, 532 GEN_TAC THEN LIST_INDUCT_TAC THEN 533 ASM_REWRITE_TAC [EVERY_DEF, NOT_CONS_NIL] THEN 534 EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC []); 535 536val MONO_EVERY = store_thm( 537 "MONO_EVERY", 538 ``(!x. P x ==> Q x) ==> (EVERY P l ==> EVERY Q l)``, 539 Q.ID_SPEC_TAC `l` THEN LIST_INDUCT_TAC THEN 540 ASM_SIMP_TAC (srw_ss()) []); 541val _ = IndDefLib.export_mono "MONO_EVERY" 542 543val EXISTS_MEM = store_thm( 544 "EXISTS_MEM", 545 ``!P l:'a list. EXISTS P l = ?e. MEM e l /\ P e``, 546 Induct_on `l` THEN SRW_TAC [] [] THEN MESON_TAC[]); 547 548val EXISTS_MAP = store_thm( 549 "EXISTS_MAP", 550 ``!P f l:'a list. EXISTS P (MAP f l) = EXISTS (\x. P (f x)) l``, 551 NTAC 2 GEN_TAC THEN LIST_INDUCT_TAC THEN 552 ASM_REWRITE_TAC [EXISTS_DEF, MAP] THEN BETA_TAC THEN REWRITE_TAC []); 553 554val EXISTS_SIMP = store_thm( 555 "EXISTS_SIMP", 556 ``!c l:'a list. EXISTS (\x. c) l = ~(l = []) /\ c``, 557 GEN_TAC THEN LIST_INDUCT_TAC THEN 558 ASM_REWRITE_TAC [EXISTS_DEF, NOT_CONS_NIL] THEN 559 EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC []); 560 561val MONO_EXISTS = store_thm( 562 "MONO_EXISTS", 563 ``(!x. P x ==> Q x) ==> (EXISTS P l ==> EXISTS Q l)``, 564 Q.ID_SPEC_TAC `l` THEN LIST_INDUCT_TAC THEN 565 ASM_SIMP_TAC (srw_ss()) [DISJ_IMP_THM]); 566val _ = IndDefLib.export_mono "MONO_EXISTS" 567 568 569val EVERY_NOT_EXISTS = store_thm( 570 "EVERY_NOT_EXISTS", 571 ``!P l. EVERY P l = ~EXISTS (\x. ~P x) l``, 572 GEN_TAC THEN LIST_INDUCT_TAC THEN 573 ASM_REWRITE_TAC [EVERY_DEF, EXISTS_DEF] THEN BETA_TAC THEN 574 REWRITE_TAC [DE_MORGAN_THM]); 575 576val EXISTS_NOT_EVERY = store_thm( 577 "EXISTS_NOT_EVERY", 578 ``!P l. EXISTS P l = ~EVERY (\x. ~P x) l``, 579 REWRITE_TAC [EVERY_NOT_EXISTS] THEN BETA_TAC THEN REWRITE_TAC [] THEN 580 CONV_TAC (DEPTH_CONV ETA_CONV) THEN REWRITE_TAC []); 581 582val MEM_APPEND = store_thm( 583 "MEM_APPEND", 584 ``!e l1 l2. MEM e (APPEND l1 l2) = MEM e l1 \/ MEM e l2``, 585 Induct_on `l1` THEN SRW_TAC [] [DISJ_ASSOC]); 586val _ = export_rewrites ["MEM_APPEND"] 587 588val MEM_FILTER = Q.store_thm 589("MEM_FILTER", 590 `!P L x. MEM x (FILTER P L) = P x /\ MEM x L`, 591 Induct_on `L` THEN SRW_TAC [] [] THEN PROVE_TAC[]); 592 593val MEM_FLAT = Q.store_thm 594("MEM_FLAT", 595 `!x L. MEM x (FLAT L) = (?l. MEM l L /\ MEM x l)`, 596 Induct_on `L` THEN SRW_TAC [] [FLAT] THEN PROVE_TAC[]); 597 598val FLAT_APPEND = Q.store_thm ("FLAT_APPEND", 599 `!l1 l2. FLAT (APPEND l1 l2) = APPEND (FLAT l1) (FLAT l2)`, 600 LIST_INDUCT_TAC 601 THEN REWRITE_TAC [APPEND, FLAT] 602 THEN ASM_REWRITE_TAC [APPEND_ASSOC]); 603val _ = export_rewrites ["FLAT_APPEND"] 604 605val FLAT_compute = Q.store_thm( 606 "FLAT_compute", 607 `(FLAT [] = []) /\ 608 (FLAT ([]::t) = FLAT t) /\ 609 (FLAT ((h::t1)::t2) = h::FLAT (t1::t2))`, 610 SIMP_TAC (srw_ss()) []); 611 612val EVERY_APPEND = store_thm( 613 "EVERY_APPEND", 614 ``!P (l1:'a list) l2. 615 EVERY P (APPEND l1 l2) = EVERY P l1 /\ EVERY P l2``, 616 GEN_TAC THEN LIST_INDUCT_TAC THEN 617 ASM_REWRITE_TAC [APPEND, EVERY_DEF, CONJ_ASSOC]); 618 619val EXISTS_APPEND = store_thm( 620 "EXISTS_APPEND", 621 ``!P (l1:'a list) l2. 622 EXISTS P (APPEND l1 l2) = EXISTS P l1 \/ EXISTS P l2``, 623 GEN_TAC THEN LIST_INDUCT_TAC THEN 624 ASM_REWRITE_TAC [APPEND, EXISTS_DEF, DISJ_ASSOC]); 625 626val NOT_EVERY = store_thm( 627 "NOT_EVERY", 628 ``!P l. ~EVERY P l = EXISTS ($~ o P) l``, 629 GEN_TAC THEN LIST_INDUCT_TAC THEN 630 ASM_REWRITE_TAC [EVERY_DEF, EXISTS_DEF, DE_MORGAN_THM, 631 o_THM]); 632 633val NOT_EXISTS = store_thm( 634 "NOT_EXISTS", 635 ``!P l. ~EXISTS P l = EVERY ($~ o P) l``, 636 GEN_TAC THEN LIST_INDUCT_TAC THEN 637 ASM_REWRITE_TAC [EVERY_DEF, EXISTS_DEF, DE_MORGAN_THM, 638 o_THM]); 639 640val MEM_MAP = store_thm( 641 "MEM_MAP", 642 ``!(l:'a list) (f:'a -> 'b) x. 643 MEM x (MAP f l) = ?y. (x = f y) /\ MEM y l``, 644 LIST_INDUCT_TAC THEN SRW_TAC [] [MAP] THEN PROVE_TAC[]); 645 646val LENGTH_NIL = store_thm("LENGTH_NIL[simp]", 647 ���!l:'a list. (LENGTH l = 0) = (l = [])���, 648 LIST_INDUCT_TAC THEN 649 REWRITE_TAC [LENGTH, NOT_SUC, NOT_CONS_NIL]); 650 651val LENGTH_NIL_SYM = store_thm ( 652 "LENGTH_NIL_SYM[simp]", 653 ``(0 = LENGTH l) = (l = [])``, 654 PROVE_TAC[LENGTH_NIL]); 655 656val NULL_EQ = store_thm("NULL_EQ", 657 ���!l. NULL l = (l = [])���, 658 Cases_on `l` THEN REWRITE_TAC[NULL, NOT_CONS_NIL]); 659 660val NULL_LENGTH = Q.store_thm("NULL_LENGTH", 661 `!l. NULL l = (LENGTH l = 0)`, 662 REWRITE_TAC[NULL_EQ, LENGTH_NIL]) 663 664val LENGTH_CONS = store_thm("LENGTH_CONS", 665 ���!l n. (LENGTH l = SUC n) = 666 ?h:'a. ?l'. (LENGTH l' = n) /\ (l = CONS h l')���, 667 LIST_INDUCT_TAC THENL [ 668 REWRITE_TAC [LENGTH, NOT_EQ_SYM(SPEC_ALL NOT_SUC), NOT_NIL_CONS], 669 REWRITE_TAC [LENGTH, INV_SUC_EQ, CONS_11] THEN 670 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN 671 simpLib.ASM_SIMP_TAC boolSimps.bool_ss [] 672 ]); 673 674val LENGTH_EQ_CONS = store_thm("LENGTH_EQ_CONS", 675 ���!P:'a list->bool. 676 !n:num. 677 (!l. (LENGTH l = SUC n) ==> P l) = 678 (!l. (LENGTH l = n) ==> (\l. !x:'a. P (CONS x l)) l)���, 679 CONV_TAC (ONCE_DEPTH_CONV BETA_CONV) THEN 680 REPEAT GEN_TAC THEN EQ_TAC THENL 681 [REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 682 ASM_REWRITE_TAC [LENGTH], 683 DISCH_TAC THEN 684 INDUCT_THEN list_INDUCT STRIP_ASSUME_TAC THENL 685 [REWRITE_TAC [LENGTH, NOT_NIL_CONS, NOT_EQ_SYM(SPEC_ALL NOT_SUC)], 686 ASM_REWRITE_TAC [LENGTH, INV_SUC_EQ, CONS_11] THEN 687 REPEAT STRIP_TAC THEN RES_THEN MATCH_ACCEPT_TAC]]); 688 689val LENGTH_EQ_SUM = store_thm ( 690 "LENGTH_EQ_SUM", 691 ``(!l:'a list n1 n2. (LENGTH l = n1+n2) = (?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1++l2)))``, 692 Induct_on `n1` THEN1 ( 693 SIMP_TAC arith_ss [LENGTH_NIL, APPEND] 694 ) THEN 695 ASM_SIMP_TAC arith_ss [arithmeticTheory.ADD_CLAUSES, LENGTH_CONS, 696 GSYM RIGHT_EXISTS_AND_THM, GSYM LEFT_EXISTS_AND_THM, APPEND] THEN 697 PROVE_TAC[]); 698 699val LENGTH_EQ_NUM = store_thm ( 700 "LENGTH_EQ_NUM", 701 ``(!l:'a list. (LENGTH l = 0) = (l = [])) /\ 702 (!l:'a list n. (LENGTH l = (SUC n)) = (?h l'. (LENGTH l' = n) /\ (l = h::l'))) /\ 703 (!l:'a list n1 n2. (LENGTH l = n1+n2) = (?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1++l2)))``, 704 SIMP_TAC arith_ss [LENGTH_NIL, LENGTH_CONS, LENGTH_EQ_SUM]); 705 706val LENGTH_EQ_NUM_compute = save_thm ("LENGTH_EQ_NUM_compute", 707 CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV LENGTH_EQ_NUM); 708 709 710val LENGTH_EQ_NIL = store_thm("LENGTH_EQ_NIL", 711 ���!P: 'a list->bool. 712 (!l. (LENGTH l = 0) ==> P l) = P []���, 713 REPEAT GEN_TAC THEN EQ_TAC THENL 714 [REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 715 REWRITE_TAC [LENGTH], 716 DISCH_TAC THEN 717 INDUCT_THEN list_INDUCT STRIP_ASSUME_TAC THENL 718 [ASM_REWRITE_TAC [], ASM_REWRITE_TAC [LENGTH, NOT_SUC]]]);; 719 720val CONS_ACYCLIC = store_thm("CONS_ACYCLIC", 721Term`!l x. ~(l = x::l) /\ ~(x::l = l)`, 722 LIST_INDUCT_TAC 723 THEN ASM_REWRITE_TAC[CONS_11, NOT_NIL_CONS, NOT_CONS_NIL, LENGTH_NIL]); 724 725val APPEND_eq_NIL = store_thm("APPEND_eq_NIL", 726Term `(!l1 l2:'a list. ([] = APPEND l1 l2) = (l1=[]) /\ (l2=[])) /\ 727 (!l1 l2:'a list. (APPEND l1 l2 = []) = (l1=[]) /\ (l2=[]))`, 728CONJ_TAC THEN 729 INDUCT_THEN list_INDUCT STRIP_ASSUME_TAC 730 THEN REWRITE_TAC [CONS_11, NOT_NIL_CONS, NOT_CONS_NIL, APPEND] 731 THEN GEN_TAC THEN MATCH_ACCEPT_TAC EQ_SYM_EQ); 732val _ = export_rewrites ["APPEND_eq_NIL"] 733 734val MAP_EQ_APPEND = store_thm( 735 "MAP_EQ_APPEND", 736 ``(MAP (f:'a -> 'b) l = l1 ++ l2) <=> 737 ?l10 l20. (l = l10 ++ l20) /\ (l1 = MAP f l10) /\ (l2 = MAP f l20)``, 738 REVERSE EQ_TAC THEN1 SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [MAP_APPEND] THEN 739 MAP_EVERY Q.ID_SPEC_TAC [`l1`, `l2`, `l`] THEN LIST_INDUCT_TAC THEN 740 SIMP_TAC (srw_ss()) [] THEN MAP_EVERY Q.X_GEN_TAC [`h`, `l2`, `l1`] THEN 741 Cases_on `l1` THEN SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [MAP_EQ_CONS] THEN 742 METIS_TAC[]); 743 744val APPEND_EQ_SING = store_thm( 745 "APPEND_EQ_SING", 746 ``(l1 ++ l2 = [e:'a]) <=> 747 (l1 = [e]) /\ (l2 = []) \/ (l1 = []) /\ (l2 = [e])``, 748 Cases_on `l1` THEN SRW_TAC [] [CONJ_ASSOC]); 749 750val APPEND_11 = store_thm( 751 "APPEND_11", 752 Term`(!l1 l2 l3:'a list. (APPEND l1 l2 = APPEND l1 l3) = (l2 = l3)) /\ 753 (!l1 l2 l3:'a list. (APPEND l2 l1 = APPEND l3 l1) = (l2 = l3))`, 754 CONJ_TAC THEN LIST_INDUCT_TAC THEN 755 ASM_REWRITE_TAC [APPEND, CONS_11, APPEND_NIL] THEN 756 Q.SUBGOAL_THEN 757 `!h l1 l2:'a list. APPEND l1 (h::l2) = APPEND (APPEND l1 [h]) l2` 758 (ONCE_REWRITE_TAC o C cons []) 759 THENL [ 760 GEN_TAC THEN POP_ASSUM (K ALL_TAC) THEN LIST_INDUCT_TAC THEN 761 REWRITE_TAC [APPEND, CONS_11] THEN POP_ASSUM ACCEPT_TAC, 762 ASM_REWRITE_TAC [] THEN GEN_TAC THEN POP_ASSUM (K ALL_TAC) THEN 763 LIST_INDUCT_TAC THEN REWRITE_TAC [APPEND, CONS_11] THENL [ 764 LIST_INDUCT_TAC THEN 765 REWRITE_TAC [APPEND, CONS_11, NOT_NIL_CONS, DE_MORGAN_THM, 766 APPEND_eq_NIL, NOT_CONS_NIL], 767 GEN_TAC THEN LIST_INDUCT_TAC THEN 768 ASM_REWRITE_TAC [APPEND, CONS_11, APPEND_eq_NIL, NOT_CONS_NIL, 769 NOT_NIL_CONS] 770 ] 771 ]); 772 773val APPEND_LENGTH_EQ = store_thm( 774 "APPEND_LENGTH_EQ", 775 ``!l1 l1'. (LENGTH l1 = LENGTH l1') ==> 776 !l2 l2'. (LENGTH l2 = LENGTH l2') ==> 777 ((l1 ++ l2 = l1' ++ l2') = (l1 = l1') /\ (l2 = l2'))``, 778 Induct THEN1 779 (GEN_TAC THEN STRIP_TAC THEN `l1' = []` by METIS_TAC [LENGTH_NIL] THEN 780 SRW_TAC [] []) THEN 781 MAP_EVERY Q.X_GEN_TAC [`h`,`l1'`] THEN SRW_TAC [] [] THEN 782 `?h' t'. l1' = h'::t'` by METIS_TAC [LENGTH_CONS] THEN 783 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []); 784 785val APPEND_11_LENGTH = save_thm ("APPEND_11_LENGTH", 786 SIMP_RULE bool_ss [DISJ_IMP_THM, FORALL_AND_THM] (prove ( 787 (���!l1 l2 l1' l2'. 788 ((LENGTH l1 = LENGTH l1') \/ (LENGTH l2 = LENGTH l2')) ==> 789 (((l1 ++ l2) = (l1' ++ l2')) = ((l1 = l1') /\ (l2 = l2')))���), 790 REPEAT GEN_TAC 791 THEN Tactical.REVERSE 792 (Cases_on `(LENGTH l1 = LENGTH l1') /\ (LENGTH l2 = LENGTH l2')`) THEN1 793( 794 DISCH_TAC 795 THEN `~((l1 = l1') /\ (l2 = l2'))` by PROVE_TAC[] 796 THEN ASM_REWRITE_TAC[] 797 THEN `~(LENGTH (l1 ++ l2) = LENGTH (l1' ++ l2'))` 798 suffices_by PROVE_TAC[] 799 THEN FULL_SIMP_TAC arith_ss [LENGTH_APPEND] 800 ) THEN PROVE_TAC[APPEND_LENGTH_EQ]))); 801 802 803val APPEND_EQ_SELF = store_thm( 804"APPEND_EQ_SELF", 805``(!l1 l2:'a list. ((l1 ++ l2 = l1) = (l2 = []))) /\ 806 (!l1 l2:'a list. ((l1 ++ l2 = l2) = (l1 = []))) /\ 807 (!l1 l2:'a list. ((l1 = l1 ++ l2) = (l2 = []))) /\ 808 (!l1 l2:'a list. ((l2 = l1 ++ l2) = (l1 = [])))``, 809PROVE_TAC[APPEND_11, APPEND_NIL, APPEND]); 810 811 812val MEM_SPLIT = Q.store_thm 813("MEM_SPLIT", 814 `!x l. (MEM x l) = ?l1 l2. (l = l1 ++ x::l2)`, 815 Induct_on `l` THEN SRW_TAC [] [] THEN EQ_TAC THENL [ 816 SRW_TAC [][] THEN1 (MAP_EVERY Q.EXISTS_TAC [`[]`,`l`] THEN SRW_TAC [][]) THEN 817 MAP_EVERY Q.EXISTS_TAC [`a::l1`, `l2`] THEN SRW_TAC [] [], 818 DISCH_THEN (Q.X_CHOOSE_THEN `l1` (Q.X_CHOOSE_THEN `l2` ASSUME_TAC)) THEN 819 Cases_on `l1` THEN FULL_SIMP_TAC(srw_ss()) [] THEN PROVE_TAC[] 820 ]) 821 822val LIST_EQ_REWRITE = Q.store_thm 823("LIST_EQ_REWRITE", 824 `!l1 l2. (l1 = l2) = 825 ((LENGTH l1 = LENGTH l2) /\ 826 ((!x. (x < LENGTH l1) ==> (EL x l1 = EL x l2))))`, 827 828 LIST_INDUCT_TAC THEN Cases_on `l2` THEN ( 829 ASM_SIMP_TAC arith_ss [LENGTH, NOT_CONS_NIL, CONS_11, EL] 830 ) THEN 831 GEN_TAC THEN EQ_TAC THEN SIMP_TAC arith_ss [] THENL [ 832 REPEAT STRIP_TAC THEN Cases_on `x` THEN ( 833 ASM_SIMP_TAC arith_ss [EL, HD, TL] 834 ), 835 REPEAT STRIP_TAC THENL [ 836 POP_ASSUM (MP_TAC o SPEC ``0:num``) THEN 837 ASM_SIMP_TAC arith_ss [EL, HD, TL], 838 Q.PAT_X_ASSUM `!x. x < Y ==> P x` (MP_TAC o SPEC ``SUC x``) THEN 839 ASM_SIMP_TAC arith_ss [EL, HD, TL] 840 ] 841 ]); 842 843val LIST_EQ = save_thm("LIST_EQ", 844 GENL[``l1:'a list``, ``l2:'a list``] 845 (snd(EQ_IMP_RULE (SPEC_ALL LIST_EQ_REWRITE)))); 846 847val FOLDL_EQ_FOLDR = Q.store_thm 848("FOLDL_EQ_FOLDR", 849 `!f l e. (ASSOC f /\ COMM f) ==> 850 ((FOLDL f e l) = (FOLDR f e l))`, 851GEN_TAC THEN 852FULL_SIMP_TAC bool_ss [RIGHT_FORALL_IMP_THM, COMM_DEF, 853 ASSOC_DEF] THEN 854STRIP_TAC THEN LIST_INDUCT_TAC THENL [ 855 SIMP_TAC bool_ss [FOLDR, FOLDL], 856 857 ASM_SIMP_TAC bool_ss [FOLDR, FOLDL] THEN 858 POP_ASSUM (K ALL_TAC) THEN 859 Q.SPEC_TAC (`l`, `l`) THEN 860 LIST_INDUCT_TAC THEN ASM_SIMP_TAC bool_ss [FOLDR] 861]); 862 863val FOLDR_CONS = store_thm( 864"FOLDR_CONS", 865``!f ls a. FOLDR (\x y. f x :: y) a ls = (MAP f ls)++a``, 866GEN_TAC THEN Induct THEN SRW_TAC[] [FOLDR, MAP]) 867 868val LENGTH_TL = Q.store_thm 869("LENGTH_TL", 870 `!l. 0 < LENGTH l ==> (LENGTH (TL l) = LENGTH l - 1)`, 871 Cases_on `l` THEN SIMP_TAC arith_ss [LENGTH, TL]); 872 873val FILTER_EQ_NIL = Q.store_thm 874("FILTER_EQ_NIL", 875 `!P l. (FILTER P l = []) = (EVERY (\x. ~(P x)) l)`, 876 GEN_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC THEN ( 877 ASM_SIMP_TAC bool_ss [FILTER, EVERY_DEF, COND_RATOR, COND_RAND, 878 NOT_CONS_NIL] 879 )); 880 881val FILTER_NEQ_NIL = Q.store_thm 882("FILTER_NEQ_NIL", 883 `!P l. ~(FILTER P l = []) = ?x. MEM x l /\ P x`, 884 SIMP_TAC bool_ss [FILTER_EQ_NIL, EVERY_NOT_EXISTS, EXISTS_MEM]); 885 886val FILTER_EQ_ID = Q.store_thm 887("FILTER_EQ_ID", 888 `!P l. (FILTER P l = l) = (EVERY P l)`, 889 Induct_on `l` THEN SRW_TAC [] [] THEN 890 DISCH_THEN (ASSUME_TAC o Q.AP_TERM `MEM a`) THEN 891 FULL_SIMP_TAC (srw_ss()) [MEM_FILTER]); 892 893val FILTER_NEQ_ID = Q.store_thm 894("FILTER_NEQ_ID", 895 `!P l. ~(FILTER P l = l) = ?x. MEM x l /\ ~(P x)`, 896 SIMP_TAC bool_ss [FILTER_EQ_ID, EVERY_NOT_EXISTS, EXISTS_MEM]); 897 898val FILTER_EQ_CONS = Q.store_thm 899("FILTER_EQ_CONS", 900 `!P l h lr. 901 (FILTER P l = h::lr) = 902 (?l1 l2. (l = l1++[h]++l2) /\ (FILTER P l1 = []) /\ (FILTER P l2 = lr) /\ (P h))`, 903 904GEN_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC THEN ( 905 ASM_SIMP_TAC bool_ss [FILTER, NOT_CONS_NIL, APPEND_eq_NIL] 906) THEN 907REPEAT STRIP_TAC THEN Cases_on `P h` THEN ASM_REWRITE_TAC[] THEN 908EQ_TAC THEN REPEAT STRIP_TAC THENL [ 909 Q.EXISTS_TAC `[]` THEN Q.EXISTS_TAC `l` THEN 910 FULL_SIMP_TAC bool_ss [CONS_11, APPEND, FILTER], 911 912 Cases_on `l1` THEN ( 913 FULL_SIMP_TAC bool_ss [APPEND, CONS_11, FILTER, COND_RAND, COND_RATOR, NOT_CONS_NIL] 914 ), 915 916 Q.EXISTS_TAC `h::l1` THEN Q.EXISTS_TAC `l2` THEN 917 ASM_SIMP_TAC bool_ss [CONS_11, APPEND, FILTER], 918 919 Cases_on `l1` THENL [ 920 FULL_SIMP_TAC bool_ss [APPEND, CONS_11], 921 Q.EXISTS_TAC `l'` THEN Q.EXISTS_TAC `l2` THEN 922 FULL_SIMP_TAC bool_ss [CONS_11, APPEND, FILTER, COND_RATOR, 923 COND_RAND, NOT_CONS_NIL] 924 ] 925]); 926 927val FILTER_APPEND_DISTRIB = Q.store_thm 928("FILTER_APPEND_DISTRIB", 929 `!P L M. FILTER P (APPEND L M) = APPEND (FILTER P L) (FILTER P M)`, 930 GEN_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC 931 THEN RW_TAC bool_ss [FILTER, APPEND]); 932 933val MEM = store_thm( 934 "MEM", 935 ``(!x:'a. MEM x [] = F) /\ (!x:'a h t. MEM x (h::t) = (x = h) \/ MEM x t)``, 936 SRW_TAC [] []); 937val _ = export_rewrites ["MEM"]; 938 939val FILTER_EQ_APPEND = Q.store_thm 940("FILTER_EQ_APPEND", 941 `!P l l1 l2. 942 (FILTER P l = l1 ++ l2) = 943 (?l3 l4. (l = l3++l4) /\ (FILTER P l3 = l1) /\ (FILTER P l4 = l2))`, 944GEN_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC THEN1 ( 945 ASM_SIMP_TAC bool_ss [FILTER, APPEND_eq_NIL] THEN PROVE_TAC[] 946) THEN 947REPEAT STRIP_TAC THEN Cases_on `P h` THEN 948ASM_SIMP_TAC bool_ss [FILTER] THENL [ 949 Cases_on `l1` THENL [ 950 Cases_on `l2` THENL [ 951 SIMP_TAC bool_ss [APPEND, NOT_CONS_NIL, FILTER_EQ_NIL, EVERY_MEM] THEN 952 PROVE_TAC[MEM_APPEND, MEM], 953 954 ASM_SIMP_TAC bool_ss [APPEND, CONS_11] THEN 955 EQ_TAC THEN STRIP_TAC THENL [ 956 Q.EXISTS_TAC `[]` THEN Q.EXISTS_TAC `h::l` THEN 957 FULL_SIMP_TAC bool_ss [APPEND, FILTER], 958 959 Tactical.REVERSE (Cases_on `l3`) THEN1 ( 960 FULL_SIMP_TAC bool_ss [CONS_11, FILTER, APPEND, 961 COND_RAND, COND_RATOR, NOT_CONS_NIL] 962 ) THEN 963 Cases_on `l4` THEN ( 964 FULL_SIMP_TAC bool_ss [FILTER, NOT_CONS_NIL, APPEND, 965 COND_RATOR, COND_RAND, CONS_11] THEN 966 PROVE_TAC[] 967 ) 968 ] 969 ], 970 971 ASM_SIMP_TAC bool_ss [APPEND, CONS_11] THEN 972 EQ_TAC THEN STRIP_TAC THENL [ 973 Q.EXISTS_TAC `h::l3` THEN Q.EXISTS_TAC `l4` THEN 974 FULL_SIMP_TAC bool_ss [APPEND, FILTER], 975 976 Cases_on `l3` THEN ( 977 FULL_SIMP_TAC bool_ss [APPEND, FILTER, NOT_CONS_NIL, FILTER, CONS_11, 978 COND_RAND, COND_RATOR] THEN 979 PROVE_TAC[] 980 ) 981 ] 982 ], 983 984 EQ_TAC THEN STRIP_TAC THENL [ 985 Q.EXISTS_TAC `h::l3` THEN Q.EXISTS_TAC `l4` THEN 986 ASM_SIMP_TAC bool_ss [APPEND, FILTER], 987 988 Cases_on `l3` THENL [ 989 Cases_on `l4` THEN 990 FULL_SIMP_TAC bool_ss [APPEND, NOT_CONS_NIL, CONS_11] THEN 991 Q.EXISTS_TAC `[]` THEN Q.EXISTS_TAC `l` THEN 992 FULL_SIMP_TAC bool_ss [FILTER, APPEND] THEN 993 PROVE_TAC[], 994 995 Q.EXISTS_TAC `l'` THEN Q.EXISTS_TAC `l4` THEN 996 FULL_SIMP_TAC bool_ss [FILTER, APPEND, CONS_11] THEN 997 PROVE_TAC[] 998 ] 999 ] 1000]); 1001 1002val EVERY_FILTER = Q.store_thm 1003("EVERY_FILTER", 1004 `!P1 P2 l. EVERY P1 (FILTER P2 l) = 1005 EVERY (\x. P2 x ==> P1 x) l`, 1006 1007GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN ( 1008 ASM_SIMP_TAC bool_ss [FILTER, EVERY_DEF, COND_RATOR, COND_RAND] 1009)); 1010 1011val EVERY_FILTER_IMP = Q.store_thm 1012("EVERY_FILTER_IMP", 1013 `!P1 P2 l. EVERY P1 l ==> EVERY P1 (FILTER P2 l)`, 1014GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN ( 1015 ASM_SIMP_TAC bool_ss [FILTER, EVERY_DEF, COND_RATOR, COND_RAND] 1016)); 1017 1018val FILTER_COND_REWRITE = Q.store_thm 1019("FILTER_COND_REWRITE", 1020 `(FILTER P [] = []) /\ 1021 (!h. (P h) ==> ((FILTER P (h::l) = h::FILTER P l))) /\ 1022 (!h. ~(P h) ==> (FILTER P (h::l) = FILTER P l))`, 1023SIMP_TAC bool_ss [FILTER]); 1024 1025val NOT_NULL_MEM = Q.store_thm 1026("NOT_NULL_MEM", 1027 `!l. ~(NULL l) = (?e. MEM e l)`, 1028 Cases_on `l` THEN SIMP_TAC bool_ss [EXISTS_OR_THM, MEM, NOT_CONS_NIL, NULL]); 1029 1030(* Computing EL when n is in numeral representation *) 1031val EL_compute = store_thm("EL_compute", 1032Term `!n. EL n l = if n=0 then HD l else EL (PRE n) (TL l)`, 1033INDUCT_TAC THEN ASM_REWRITE_TAC [NOT_SUC, EL, PRE]); 1034 1035(* a version of the above that is safe to use in the simplifier *) 1036(* only bother with BIT1/2 cases because the zero case is already provided 1037 by the definition. *) 1038val EL_simp = store_thm( 1039 "EL_simp", 1040 ``(EL (NUMERAL (BIT1 n)) l = EL (PRE (NUMERAL (BIT1 n))) (TL l)) /\ 1041 (EL (NUMERAL (BIT2 n)) l = EL (NUMERAL (BIT1 n)) (TL l))``, 1042 REWRITE_TAC [arithmeticTheory.NUMERAL_DEF, 1043 arithmeticTheory.BIT1, arithmeticTheory.BIT2, 1044 arithmeticTheory.ADD_CLAUSES, 1045 prim_recTheory.PRE, EL]); 1046 1047val EL_restricted = store_thm( 1048 "EL_restricted", 1049 ``(EL 0 = HD) /\ 1050 (EL (SUC n) (l::ls) = EL n ls)``, 1051 REWRITE_TAC [FUN_EQ_THM, EL, TL, HD]); 1052val _ = export_rewrites ["EL_restricted"] 1053 1054val EL_simp_restricted = store_thm( 1055 "EL_simp_restricted", 1056 ``(EL (NUMERAL (BIT1 n)) (l::ls) = EL (PRE (NUMERAL (BIT1 n))) ls) /\ 1057 (EL (NUMERAL (BIT2 n)) (l::ls) = EL (NUMERAL (BIT1 n)) ls)``, 1058 REWRITE_TAC [EL_simp, TL]); 1059val _ = export_rewrites ["EL_simp_restricted"] 1060 1061val SUM_eq_0 = store_thm("SUM_eq_0", 1062 ``!ls. (SUM ls = 0) = !x. MEM x ls ==> (x = 0)``, 1063 LIST_INDUCT_TAC THEN SRW_TAC[] [SUM, MEM] THEN METIS_TAC[]) 1064 1065val NULL_FILTER = store_thm("NULL_FILTER", 1066 ``!P ls. NULL (FILTER P ls) = !x. MEM x ls ==> ~P x``, 1067 GEN_TAC THEN LIST_INDUCT_TAC THEN 1068 SRW_TAC[] [NULL, FILTER, MEM] THEN METIS_TAC[]) 1069 1070 1071val WF_LIST_PRED = store_thm("WF_LIST_PRED", 1072Term`WF \L1 L2. ?h:'a. L2 = h::L1`, 1073REWRITE_TAC[relationTheory.WF_DEF] THEN BETA_TAC THEN GEN_TAC 1074 THEN CONV_TAC CONTRAPOS_CONV 1075 THEN Ho_Rewrite.REWRITE_TAC 1076 [NOT_FORALL_THM, NOT_EXISTS_THM, NOT_IMP, DE_MORGAN_THM] 1077 THEN REWRITE_TAC [GSYM IMP_DISJ_THM] THEN STRIP_TAC 1078 THEN LIST_INDUCT_TAC THENL [ALL_TAC, GEN_TAC] 1079 THEN STRIP_TAC THEN RES_TAC 1080 THEN RULE_ASSUM_TAC(REWRITE_RULE[NOT_NIL_CONS, CONS_11]) 1081 THENL [FIRST_ASSUM ACCEPT_TAC, 1082 PAT_X_ASSUM (Term`x /\ y`) (SUBST_ALL_TAC o CONJUNCT2) THEN RES_TAC]); 1083 1084(* ---------------------------------------------------------------------- 1085 LIST_REL : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool 1086 1087 Lifts a relation point-wise to two lists 1088 ---------------------------------------------------------------------- *) 1089 1090val (LIST_REL_rules, LIST_REL_ind, LIST_REL_cases) = IndDefLib.Hol_reln` 1091 (LIST_REL R [] []) /\ 1092 (!h1 h2 t1 t2. R h1 h2 /\ LIST_REL R t1 t2 ==> LIST_REL R (h1::t1) (h2::t2)) 1093`; 1094 1095val _ = overload_on ("listRel", ``LIST_REL``) 1096val _ = overload_on ("LIST_REL", ``LIST_REL``) 1097 1098val LIST_REL_EL_EQN = store_thm( 1099 "LIST_REL_EL_EQN", 1100 ``!R l1 l2. LIST_REL R l1 l2 <=> 1101 (LENGTH l1 = LENGTH l2) /\ 1102 !n. n < LENGTH l1 ==> R (EL n l1) (EL n l2)``, 1103 GEN_TAC THEN SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN 1104 CONJ_TAC THENL [ 1105 Induct_on `LIST_REL` THEN SRW_TAC [] [] THEN 1106 Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [], 1107 Induct_on `l1` THEN Cases_on `l2` THEN SRW_TAC [] [LIST_REL_rules] THEN 1108 POP_ASSUM (fn th => Q.SPEC_THEN `0` MP_TAC th THEN 1109 Q.SPEC_THEN `SUC m` (MP_TAC o Q.GEN `m`) th) THEN 1110 SRW_TAC [] [LIST_REL_rules] 1111 ]); 1112 1113val LIST_REL_def = store_thm( 1114 "LIST_REL_def", 1115 ``(LIST_REL R [][] <=> T) /\ 1116 (LIST_REL R (a::as) [] <=> F) /\ 1117 (LIST_REL R [] (b::bs) <=> F) /\ 1118 (LIST_REL R (a::as) (b::bs) <=> R a b /\ LIST_REL R as bs)``, 1119 REPEAT CONJ_TAC THEN SRW_TAC [] [Once LIST_REL_cases, SimpLHS]); 1120val _ = export_rewrites ["LIST_REL_def"] 1121 1122val LIST_REL_mono = store_thm( 1123 "LIST_REL_mono", 1124 ``(!x y. R1 x y ==> R2 x y) ==> LIST_REL R1 l1 l2 ==> LIST_REL R2 l1 l2``, 1125 SRW_TAC [] [LIST_REL_EL_EQN]); 1126val _ = IndDefLib.export_mono "LIST_REL_mono" 1127 1128val LIST_REL_NIL = store_thm( 1129 "LIST_REL_NIL", 1130 ``(LIST_REL R [] y <=> (y = [])) /\ (LIST_REL R x [] <=> (x = []))``, 1131 Cases_on `x` THEN Cases_on `y` THEN SRW_TAC [] []); 1132val _ = export_rewrites ["LIST_REL_NIL"] 1133 1134val LIST_REL_CONS1 = store_thm( 1135 "LIST_REL_CONS1", 1136 ``LIST_REL R (h::t) xs <=> ?h' t'. (xs = h'::t') /\ R h h' /\ LIST_REL R t t'``, 1137 Cases_on `xs` THEN SRW_TAC [] []); 1138 1139val LIST_REL_CONS2 = store_thm( 1140 "LIST_REL_CONS2", 1141 ``LIST_REL R xs (h::t) <=> ?h' t'. (xs = h'::t') /\ R h' h /\ LIST_REL R t' t``, 1142 Cases_on `xs` THEN SRW_TAC [] []); 1143 1144val LIST_REL_CONJ = store_thm( 1145 "LIST_REL_CONJ", 1146 ``LIST_REL (\a b. P a b /\ Q a b) l1 l2 <=> 1147 LIST_REL (\a b. P a b) l1 l2 /\ LIST_REL (\a b. Q a b) l1 l2``, 1148 SRW_TAC [] [LIST_REL_EL_EQN] THEN METIS_TAC []); 1149 1150val LIST_REL_MAP1 = store_thm( 1151 "LIST_REL_MAP1", 1152 ``LIST_REL R (MAP f l1) l2 <=> LIST_REL (R o f) l1 l2``, 1153 SRW_TAC [] [LIST_REL_EL_EQN, EL_MAP, LENGTH_MAP]); 1154 1155val LIST_REL_MAP2 = store_thm( 1156 "LIST_REL_MAP2", 1157 ``LIST_REL (\a b. R a b) l1 (MAP f l2) <=> 1158 LIST_REL (\a b. R a (f b)) l1 l2``, 1159 SRW_TAC [CONJ_ss] [LIST_REL_EL_EQN, EL_MAP, LENGTH_MAP]); 1160 1161val LIST_REL_LENGTH = store_thm( 1162 "LIST_REL_LENGTH", 1163 ``!x y. LIST_REL R x y ==> (LENGTH x = LENGTH y)``, 1164 Induct_on `LIST_REL` THEN SRW_TAC [] [LENGTH]); 1165 1166val LIST_REL_SPLIT1 = Q.store_thm("LIST_REL_SPLIT1", 1167 ���!xs1 zs. 1168 LIST_REL P (xs1 ++ xs2) zs <=> 1169 ?ys1 ys2. (zs = ys1 ++ ys2) /\ LIST_REL P xs1 ys1 /\ LIST_REL P xs2 ys2���, 1170 Induct >> fs[APPEND] >> Cases_on `zs` >> fs[] >> rpt strip_tac >> 1171 simp[LIST_REL_CONS1, PULL_EXISTS] >> metis_tac[]); 1172 1173val LIST_REL_SPLIT2 = Q.store_thm("LIST_REL_SPLIT2", 1174 ���!xs1 zs. 1175 LIST_REL P zs (xs1 ++ xs2) <=> 1176 ?ys1 ys2. (zs = ys1 ++ ys2) /\ LIST_REL P ys1 xs1 /\ LIST_REL P ys2 xs2���, 1177 Induct >> fs[APPEND] >> Cases_on `zs` >> fs[] >> rpt strip_tac >> 1178 simp[LIST_REL_CONS2, PULL_EXISTS] >> metis_tac[]); 1179 1180(* example of LIST_REL in action : 1181val (rules,ind,cases) = IndDefLib.Hol_reln` 1182 (!n m. n < m ==> R n m) /\ 1183 (!n m. R n m ==> R1 (INL n) (INL m)) /\ 1184 (!l1 l2. LIST_REL R l1 l2 ==> R1 (INR l1) (INR l2)) 1185` 1186val strong = IndDefLib.derive_strong_induction (rules,ind) 1187*) 1188 1189 1190(*--------------------------------------------------------------------------- 1191 Congruence rules for higher-order functions. Used when making 1192 recursive definitions by so-called higher-order recursion. 1193 ---------------------------------------------------------------------------*) 1194 1195val list_size_def = 1196 REWRITE_RULE [arithmeticTheory.ADD_ASSOC] 1197 (#2 (TypeBase.size_of ``:'a list``)); 1198 1199val Induct = INDUCT_THEN list_INDUCT STRIP_ASSUME_TAC; 1200 1201val list_size_cong = store_thm("list_size_cong", 1202Term 1203 `!M N f f'. 1204 (M=N) /\ (!x. MEM x N ==> (f x = f' x)) 1205 ==> 1206 (list_size f M = list_size f' N)`, 1207Induct 1208 THEN REWRITE_TAC [list_size_def, MEM] 1209 THEN REPEAT STRIP_TAC 1210 THEN PAT_X_ASSUM (Term`x = y`) (SUBST_ALL_TAC o SYM) 1211 THEN REWRITE_TAC [list_size_def] 1212 THEN MK_COMB_TAC THENL 1213 [NTAC 2 (MK_COMB_TAC THEN TRY REFL_TAC) 1214 THEN FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC [MEM], 1215 FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC [] THEN GEN_TAC 1216 THEN PAT_X_ASSUM (Term`!x. MEM x l ==> Q x`) 1217 (MP_TAC o SPEC (Term`x:'a`)) 1218 THEN REWRITE_TAC [MEM] THEN REPEAT STRIP_TAC 1219 THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]); 1220 1221val FOLDR_CONG = store_thm("FOLDR_CONG", 1222Term 1223 `!l l' b b' (f:'a->'b->'b) f'. 1224 (l=l') /\ (b=b') /\ (!x a. MEM x l' ==> (f x a = f' x a)) 1225 ==> 1226 (FOLDR f b l = FOLDR f' b' l')`, 1227Induct 1228 THEN REWRITE_TAC [FOLDR, MEM] 1229 THEN REPEAT STRIP_TAC 1230 THEN REPEAT (PAT_X_ASSUM (Term`x = y`) (SUBST_ALL_TAC o SYM)) 1231 THEN REWRITE_TAC [FOLDR] 1232 THEN POP_ASSUM (fn th => MP_TAC (SPEC (Term`h`) th) THEN ASSUME_TAC th) 1233 THEN REWRITE_TAC [MEM] 1234 THEN DISCH_TAC 1235 THEN MK_COMB_TAC 1236 THENL [CONV_TAC FUN_EQ_CONV THEN ASM_REWRITE_TAC [], 1237 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC [] 1238 THEN REPEAT STRIP_TAC 1239 THEN FIRST_ASSUM MATCH_MP_TAC 1240 THEN ASM_REWRITE_TAC [MEM]]); 1241 1242val FOLDL_CONG = store_thm("FOLDL_CONG", 1243Term 1244 `!l l' b b' (f:'b->'a->'b) f'. 1245 (l=l') /\ (b=b') /\ (!x a. MEM x l' ==> (f a x = f' a x)) 1246 ==> 1247 (FOLDL f b l = FOLDL f' b' l')`, 1248Induct 1249 THEN REWRITE_TAC [FOLDL, MEM] 1250 THEN REPEAT STRIP_TAC 1251 THEN REPEAT (PAT_X_ASSUM (Term`x = y`) (SUBST_ALL_TAC o SYM)) 1252 THEN REWRITE_TAC [FOLDL] 1253 THEN FIRST_ASSUM MATCH_MP_TAC 1254 THEN REWRITE_TAC[] 1255 THEN CONJ_TAC 1256 THENL [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC [MEM], 1257 REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC 1258 THEN ASM_REWRITE_TAC [MEM]]); 1259 1260 1261val MAP_CONG = store_thm("MAP_CONG", 1262Term 1263 `!l1 l2 f f'. 1264 (l1=l2) /\ (!x. MEM x l2 ==> (f x = f' x)) 1265 ==> 1266 (MAP f l1 = MAP f' l2)`, 1267Induct THEN REWRITE_TAC [MAP, MEM] 1268 THEN REPEAT STRIP_TAC 1269 THEN REPEAT (PAT_X_ASSUM (Term`x = y`) (SUBST_ALL_TAC o SYM)) 1270 THEN REWRITE_TAC [MAP] 1271 THEN MK_COMB_TAC 1272 THENL [MK_COMB_TAC THEN TRY REFL_TAC 1273 THEN FIRST_ASSUM MATCH_MP_TAC 1274 THEN REWRITE_TAC [MEM], 1275 FIRST_ASSUM MATCH_MP_TAC 1276 THEN REWRITE_TAC [] THEN REPEAT STRIP_TAC 1277 THEN FIRST_ASSUM MATCH_MP_TAC 1278 THEN ASM_REWRITE_TAC [MEM]]); 1279 1280val MAP2_CONG = store_thm("MAP2_CONG", 1281Term 1282 `!l1 l1' l2 l2' f f'. 1283 (l1=l1') /\ (l2=l2') /\ 1284 (!x y. MEM x l1' /\ MEM y l2' ==> (f x y = f' x y)) 1285 ==> 1286 (MAP2 f l1 l2 = MAP2 f' l1' l2')`, 1287Induct THEN SRW_TAC[] [MAP2_DEF, MEM] THEN 1288SRW_TAC[] [MAP2_DEF] THEN 1289Cases_on `l2` THEN 1290SRW_TAC[][MAP2_DEF]) 1291 1292val EXISTS_CONG = store_thm("EXISTS_CONG", 1293Term 1294 `!l1 l2 P P'. 1295 (l1=l2) /\ (!x. MEM x l2 ==> (P x = P' x)) 1296 ==> 1297 (EXISTS P l1 = EXISTS P' l2)`, 1298Induct THEN REWRITE_TAC [EXISTS_DEF, MEM] 1299 THEN REPEAT STRIP_TAC 1300 THEN REPEAT (PAT_X_ASSUM (Term`x = y`) (SUBST_ALL_TAC o SYM)) 1301 THENL [PAT_X_ASSUM (Term`EXISTS x y`) MP_TAC THEN REWRITE_TAC [EXISTS_DEF], 1302 REWRITE_TAC [EXISTS_DEF] 1303 THEN MK_COMB_TAC 1304 THENL [MK_COMB_TAC THEN TRY REFL_TAC 1305 THEN FIRST_ASSUM MATCH_MP_TAC 1306 THEN REWRITE_TAC [MEM], 1307 FIRST_ASSUM MATCH_MP_TAC 1308 THEN REWRITE_TAC [] THEN REPEAT STRIP_TAC 1309 THEN FIRST_ASSUM MATCH_MP_TAC 1310 THEN ASM_REWRITE_TAC [MEM]]]);; 1311 1312 1313val EVERY_CONG = store_thm("EVERY_CONG", 1314Term 1315 `!l1 l2 P P'. 1316 (l1=l2) /\ (!x. MEM x l2 ==> (P x = P' x)) 1317 ==> 1318 (EVERY P l1 = EVERY P' l2)`, 1319Induct THEN REWRITE_TAC [EVERY_DEF, MEM] 1320 THEN REPEAT STRIP_TAC 1321 THEN REPEAT (PAT_X_ASSUM (Term`x = y`) (SUBST_ALL_TAC o SYM)) 1322 THEN REWRITE_TAC [EVERY_DEF] 1323 THEN MK_COMB_TAC 1324 THENL [MK_COMB_TAC THEN TRY REFL_TAC 1325 THEN FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC [MEM], 1326 FIRST_ASSUM MATCH_MP_TAC 1327 THEN REWRITE_TAC [] THEN REPEAT STRIP_TAC 1328 THEN FIRST_ASSUM MATCH_MP_TAC 1329 THEN ASM_REWRITE_TAC [MEM]]); 1330 1331val EVERY_MONOTONIC = store_thm( 1332 "EVERY_MONOTONIC", 1333 ``!(P:'a -> bool) Q. 1334 (!x. P x ==> Q x) ==> !l. EVERY P l ==> EVERY Q l``, 1335 REPEAT GEN_TAC THEN STRIP_TAC THEN LIST_INDUCT_TAC THEN 1336 REWRITE_TAC [EVERY_DEF] THEN REPEAT STRIP_TAC THEN RES_TAC); 1337 1338(* ---------------------------------------------------------------------- 1339 ZIP and UNZIP functions (taken from rich_listTheory) 1340 ---------------------------------------------------------------------- *) 1341val ZIP_def = 1342 let val lemma = prove( 1343 (���?ZIP. 1344 (!l2. ZIP ([], l2) = []) /\ 1345 (!l1. ZIP (l1, []) = []) /\ 1346 (!(x1:'a) l1 (x2:'b) l2. 1347 ZIP ((CONS x1 l1), (CONS x2 l2)) = CONS (x1,x2)(ZIP (l1, l2)))���), 1348 let val th = prove_rec_fn_exists list_Axiom 1349 (���(fn [] l = []) /\ 1350 (fn (CONS (x:'a) l') (l:'b list) = 1351 if l = [] then [] else 1352 CONS (x, (HD l)) (fn l' (TL l)))���) 1353 in 1354 STRIP_ASSUME_TAC th 1355 THEN EXISTS_TAC 1356 (���UNCURRY (fn:('a)list -> (('b)list -> ('a # 'b)list))���) 1357 THEN ASM_REWRITE_TAC[pairTheory.UNCURRY_DEF, HD, TL, NOT_CONS_NIL] 1358 THEN STRIP_TAC 1359 THEN STRIP_ASSUME_TAC (SPEC ``l1:'a list`` list_CASES) 1360 THEN ASM_REWRITE_TAC[] 1361 end) 1362 in 1363 Rsyntax.new_specification 1364 {consts = [{const_name = "ZIP", fixity = NONE}], 1365 name = "ZIP_def", 1366 sat_thm = lemma 1367 } 1368 end; 1369 1370val ZIP = store_thm("ZIP", 1371 ``(ZIP ([],[]) = []) /\ 1372 (!(x1:'a) l1 (x2:'b) l2. 1373 ZIP ((CONS x1 l1), (CONS x2 l2)) = CONS (x1,x2)(ZIP (l1, l2)))``, 1374 REWRITE_TAC [ZIP_def]); 1375 1376val UNZIP = new_recursive_definition { 1377 name = "UNZIP", rec_axiom = list_Axiom, 1378 def = ``(UNZIP [] = ([], [])) /\ 1379 (!x l. UNZIP (CONS (x:'a # 'b) l) = 1380 (CONS (FST x) (FST (UNZIP l)), 1381 CONS (SND x) (SND (UNZIP l))))``} 1382 1383val UNZIP_THM = Q.store_thm 1384("UNZIP_THM", 1385 `(UNZIP [] = ([]:'a list,[]:'b list)) /\ 1386 (UNZIP ((x:'a,y:'b)::t) = let (L1,L2) = UNZIP t in (x::L1, y::L2))`, 1387 RW_TAC bool_ss [UNZIP] 1388 THEN Cases_on `UNZIP t` 1389 THEN RW_TAC bool_ss [LET_THM, pairTheory.UNCURRY_DEF, 1390 pairTheory.FST, pairTheory.SND]); 1391 1392val UNZIP_MAP = Q.store_thm 1393("UNZIP_MAP", 1394 `!L. UNZIP L = (MAP FST L, MAP SND L)`, 1395 LIST_INDUCT_TAC THEN 1396 ASM_SIMP_TAC arith_ss [UNZIP, MAP, 1397 PAIR_EQ, pairTheory.FST, pairTheory.SND]); 1398 1399val SUC_NOT = arithmeticTheory.SUC_NOT 1400val LENGTH_ZIP = store_thm("LENGTH_ZIP", 1401 ���!(l1:'a list) (l2:'b list). 1402 (LENGTH l1 = LENGTH l2) ==> 1403 (LENGTH(ZIP(l1,l2)) = LENGTH l1) /\ 1404 (LENGTH(ZIP(l1,l2)) = LENGTH l2)���, 1405 LIST_INDUCT_TAC THEN REPEAT (FILTER_GEN_TAC (���l2:'b list���)) THEN 1406 LIST_INDUCT_TAC THEN 1407 REWRITE_TAC[ZIP, LENGTH, NOT_SUC, SUC_NOT, INV_SUC_EQ] THEN 1408 DISCH_TAC THEN RES_TAC THEN ASM_REWRITE_TAC[]); 1409 1410val LENGTH_UNZIP = store_thm( 1411 "LENGTH_UNZIP", 1412 ``!pl. (LENGTH (FST (UNZIP pl)) = LENGTH pl) /\ 1413 (LENGTH (SND (UNZIP pl)) = LENGTH pl)``, 1414 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [UNZIP, LENGTH]); 1415 1416val ZIP_UNZIP = store_thm("ZIP_UNZIP", 1417 (���!l:('a # 'b)list. ZIP(UNZIP l) = l���), 1418 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[UNZIP, ZIP]); 1419 1420val UNZIP_ZIP = store_thm("UNZIP_ZIP", 1421 (���!l1:'a list. !l2:'b list. 1422 (LENGTH l1 = LENGTH l2) ==> (UNZIP(ZIP(l1,l2)) = (l1,l2))���), 1423 LIST_INDUCT_TAC THEN REPEAT (FILTER_GEN_TAC (���l2:'b list���)) 1424 THEN LIST_INDUCT_TAC 1425 THEN ASM_REWRITE_TAC[UNZIP, ZIP, LENGTH, NOT_SUC, SUC_NOT, INV_SUC_EQ] 1426 THEN REPEAT STRIP_TAC THEN RES_THEN SUBST1_TAC THEN REWRITE_TAC[]); 1427 1428 1429val ZIP_MAP = store_thm( 1430 "ZIP_MAP", 1431 ``!l1 l2 f1 f2. 1432 (LENGTH l1 = LENGTH l2) ==> 1433 (ZIP (MAP f1 l1, l2) = MAP (\p. (f1 (FST p), SND p)) (ZIP (l1, l2))) /\ 1434 (ZIP (l1, MAP f2 l2) = MAP (\p. (FST p, f2 (SND p))) (ZIP (l1, l2)))``, 1435 LIST_INDUCT_TAC THEN REWRITE_TAC [MAP, LENGTH] THEN REPEAT GEN_TAC THEN 1436 STRIP_TAC THENL [ 1437 Q.SUBGOAL_THEN `l2 = []` SUBST_ALL_TAC THEN 1438 REWRITE_TAC [ZIP, MAP] THEN mesonLib.ASM_MESON_TAC [LENGTH_NIL], 1439 Q.SUBGOAL_THEN 1440 `?l2h l2t. (l2 = l2h::l2t) /\ (LENGTH l2t = LENGTH l1)` 1441 STRIP_ASSUME_TAC THENL [ 1442 mesonLib.ASM_MESON_TAC [LENGTH_CONS], 1443 ASM_SIMP_TAC bool_ss [ZIP, MAP, FST, SND] 1444 ] 1445 ]); 1446 1447val MEM_ZIP = store_thm( 1448 "MEM_ZIP", 1449 ``!(l1:'a list) (l2:'b list) p. 1450 (LENGTH l1 = LENGTH l2) ==> 1451 (MEM p (ZIP(l1, l2)) = 1452 ?n. n < LENGTH l1 /\ (p = (EL n l1, EL n l2)))``, 1453 LIST_INDUCT_TAC THEN SIMP_TAC bool_ss [LENGTH] THEN REPEAT STRIP_TAC THENL [ 1454 `l2 = []` by ASM_MESON_TAC [LENGTH_NIL] THEN 1455 FULL_SIMP_TAC arith_ss [ZIP, MEM, LENGTH], 1456 `?l2h l2t. (l2 = l2h::l2t) /\ (LENGTH l2t = LENGTH l1)` 1457 by ASM_MESON_TAC [LENGTH_CONS] THEN 1458 FULL_SIMP_TAC arith_ss [MEM, ZIP, LENGTH] THEN EQ_TAC THEN 1459 STRIP_TAC THENL [ 1460 Q.EXISTS_TAC `0` THEN ASM_SIMP_TAC arith_ss [EL, HD], 1461 Q.EXISTS_TAC `SUC n` THEN ASM_SIMP_TAC arith_ss [EL, TL], 1462 Cases_on `n` THEN FULL_SIMP_TAC arith_ss [EL, HD, TL] THEN 1463 ASM_MESON_TAC [] 1464 ] 1465 ]); 1466 1467val EL_ZIP = store_thm( 1468 "EL_ZIP", 1469 ``!(l1:'a list) (l2:'b list) n. 1470 (LENGTH l1 = LENGTH l2) /\ n < LENGTH l1 ==> 1471 (EL n (ZIP (l1, l2)) = (EL n l1, EL n l2))``, 1472 Induct THEN SIMP_TAC arith_ss [LENGTH] THEN REPEAT STRIP_TAC THEN 1473 `?l2h l2t. (l2 = l2h::l2t) /\ (LENGTH l2t = LENGTH l1)` 1474 by ASM_MESON_TAC [LENGTH_CONS] THEN 1475 FULL_SIMP_TAC arith_ss [ZIP, LENGTH] THEN 1476 Cases_on `n` THEN ASM_SIMP_TAC arith_ss [ZIP, EL, HD, TL]); 1477 1478 1479val MAP2_ZIP = store_thm("MAP2_ZIP", 1480 (���!l1 l2. (LENGTH l1 = LENGTH l2) ==> 1481 !f:'a->'b->'c. MAP2 f l1 l2 = MAP (UNCURRY f) (ZIP (l1,l2))���), 1482 let val UNCURRY_DEF = pairTheory.UNCURRY_DEF 1483 in 1484 LIST_INDUCT_TAC THEN REPEAT (FILTER_GEN_TAC (���l2:'b list���)) 1485 THEN LIST_INDUCT_TAC 1486 THEN REWRITE_TAC[MAP, MAP2, ZIP, LENGTH, NOT_SUC, SUC_NOT] 1487 THEN ASM_REWRITE_TAC[CONS_11, UNCURRY_DEF, INV_SUC_EQ] 1488 end); 1489 1490val MAP2_MAP = save_thm("MAP2_MAP",MAP2_ZIP) 1491 1492val MAP_ZIP = Q.store_thm( 1493 "MAP_ZIP", 1494 `(LENGTH l1 = LENGTH l2) ==> 1495 (MAP FST (ZIP (l1,l2)) = l1) /\ 1496 (MAP SND (ZIP (l1,l2)) = l2) /\ 1497 (MAP (f o FST) (ZIP (l1,l2)) = MAP f l1) /\ 1498 (MAP (g o SND) (ZIP (l1,l2)) = MAP g l2)`, 1499 Q.ID_SPEC_TAC `l2` THEN Induct_on `l1` THEN 1500 SRW_TAC [] [] THEN TRY(Cases_on `l2`) THEN 1501 FULL_SIMP_TAC (srw_ss()) [ZIP, MAP]); 1502 1503val MEM_EL = store_thm( 1504 "MEM_EL", 1505 ``!(l:'a list) x. MEM x l = ?n. n < LENGTH l /\ (x = EL n l)``, 1506 Induct THEN ASM_SIMP_TAC arith_ss [MEM, LENGTH] THEN REPEAT GEN_TAC THEN 1507 EQ_TAC THEN STRIP_TAC THENL [ 1508 Q.EXISTS_TAC `0` THEN ASM_SIMP_TAC arith_ss [EL, HD], 1509 Q.EXISTS_TAC `SUC n` THEN ASM_SIMP_TAC arith_ss [EL, TL], 1510 Cases_on `n` THEN FULL_SIMP_TAC arith_ss [EL, HD, TL] THEN 1511 ASM_MESON_TAC [] 1512 ]); 1513 1514val SUM_MAP_PLUS_ZIP = store_thm( 1515 "SUM_MAP_PLUS_ZIP", 1516 ``!ls1 ls2. (LENGTH ls1 = LENGTH ls2) /\ (!x y. f (x,y) = g x + h y) ==> 1517 (SUM (MAP f (ZIP (ls1,ls2))) = SUM (MAP g ls1) + SUM (MAP h ls2))``, 1518 Induct THEN Cases_on `ls2` THEN 1519 SRW_TAC [numSimps.ARITH_ss] [MAP, ZIP, MAP_ZIP, SUM]); 1520 1521val LIST_REL_EVERY_ZIP = store_thm( 1522"LIST_REL_EVERY_ZIP", 1523``!R l1 l2. LIST_REL R l1 l2 = ((LENGTH l1 = LENGTH l2) /\ EVERY (UNCURRY R) (ZIP (l1,l2)))``, 1524GEN_TAC THEN Induct THEN SRW_TAC[] [LENGTH_NIL_SYM] THEN 1525SRW_TAC [] [EQ_IMP_THM, LIST_REL_CONS1] THEN SRW_TAC [] [EVERY_DEF, ZIP] THEN 1526Cases_on `l2` THEN FULL_SIMP_TAC(srw_ss())[EVERY_DEF, ZIP]) 1527 1528(* --------------------------------------------------------------------- *) 1529(* REVERSE *) 1530(* --------------------------------------------------------------------- *) 1531 1532val REVERSE_DEF = new_recursive_definition { 1533 name = "REVERSE_DEF", 1534 rec_axiom = list_Axiom, 1535 def = ``(REVERSE [] = []) /\ 1536 (REVERSE (h::t) = (REVERSE t) ++ [h])``}; 1537val _ = export_rewrites ["REVERSE_DEF"] 1538 1539val REVERSE_APPEND = store_thm( 1540 "REVERSE_APPEND", 1541 ``!l1 l2:'a list. 1542 REVERSE (l1 ++ l2) = (REVERSE l2) ++ (REVERSE l1)``, 1543 LIST_INDUCT_TAC THEN 1544 ASM_REWRITE_TAC [APPEND, REVERSE_DEF, APPEND_NIL, APPEND_ASSOC]); 1545 1546val REVERSE_REVERSE = store_thm( 1547 "REVERSE_REVERSE", 1548 ``!l:'a list. REVERSE (REVERSE l) = l``, 1549 LIST_INDUCT_TAC THEN 1550 ASM_REWRITE_TAC [REVERSE_DEF, REVERSE_APPEND, APPEND]); 1551val _ = export_rewrites ["REVERSE_REVERSE"] 1552 1553val REVERSE_11 = store_thm( 1554 "REVERSE_11", 1555 ``!l1 l2:'a list. (REVERSE l1 = REVERSE l2) <=> (l1 = l2)``, 1556 REPEAT GEN_TAC THEN EQ_TAC THEN1 1557 (DISCH_THEN (MP_TAC o AP_TERM ``REVERSE : 'a list -> 'a list``) THEN 1558 REWRITE_TAC [REVERSE_REVERSE]) THEN 1559 STRIP_TAC THEN ASM_REWRITE_TAC []); 1560val _ = export_rewrites ["REVERSE_11"] 1561 1562val MEM_REVERSE = store_thm( 1563 "MEM_REVERSE", 1564 ``!l x. MEM x (REVERSE l) = MEM x l``, 1565 Induct THEN SRW_TAC [] [] THEN PROVE_TAC []); 1566val _ = export_rewrites ["MEM_REVERSE"] 1567 1568val LENGTH_REVERSE = store_thm( 1569 "LENGTH_REVERSE", 1570 ``!l. LENGTH (REVERSE l) = LENGTH l``, 1571 Induct THEN SRW_TAC [] [arithmeticTheory.ADD1]); 1572val _ = export_rewrites ["LENGTH_REVERSE"] 1573 1574val REVERSE_EQ_NIL = store_thm( 1575 "REVERSE_EQ_NIL", 1576 ``(REVERSE l = []) <=> (l = [])``, 1577 Cases_on `l` THEN SRW_TAC [] []); 1578val _ = export_rewrites ["REVERSE_EQ_NIL"] 1579 1580val REVERSE_EQ_SING = store_thm( 1581 "REVERSE_EQ_SING", 1582 ``(REVERSE l = [e:'a]) <=> (l = [e])``, 1583 Cases_on `l` THEN SRW_TAC [] [APPEND_EQ_SING, CONJ_COMM]); 1584val _ = export_rewrites ["REVERSE_EQ_SING"] 1585 1586val FILTER_REVERSE = store_thm( 1587 "FILTER_REVERSE", 1588 ``!l P. FILTER P (REVERSE l) = REVERSE (FILTER P l)``, 1589 Induct THEN 1590 ASM_SIMP_TAC bool_ss [FILTER, REVERSE_DEF, FILTER_APPEND_DISTRIB, 1591 COND_RAND, COND_RATOR, APPEND_NIL]); 1592 1593 1594(* ---------------------------------------------------------------------- 1595 FRONT and LAST 1596 ---------------------------------------------------------------------- *) 1597 1598val LAST_DEF = new_recursive_definition { 1599 name = "LAST_DEF", 1600 rec_axiom = list_Axiom, 1601 def = ``LAST (h::t) = if t = [] then h else LAST t``}; 1602 1603val FRONT_DEF = new_recursive_definition { 1604 name = "FRONT_DEF", 1605 rec_axiom = list_Axiom, 1606 def = ``FRONT (h::t) = if t = [] then [] else h :: FRONT t``}; 1607 1608val LAST_CONS = store_thm( 1609 "LAST_CONS", 1610 ``(!x:'a. LAST [x] = x) /\ 1611 (!(x:'a) y z. LAST (x::y::z) = LAST(y::z))``, 1612 REWRITE_TAC [LAST_DEF, NOT_CONS_NIL]); 1613val _ = export_rewrites ["LAST_CONS"] 1614 1615val LAST_EL = store_thm( 1616"LAST_EL", 1617``!ls. (ls <> []) ==> (LAST ls = EL (PRE (LENGTH ls)) ls)``, 1618Induct THEN SRW_TAC[] [] THEN 1619Cases_on `ls` THEN FULL_SIMP_TAC (srw_ss()) []) 1620 1621val LAST_MAP = store_thm( 1622 "LAST_MAP[simp]", 1623 ``!l f. l <> [] ==> (LAST (MAP f l) = f (LAST l))``, 1624 rpt strip_tac >> `?h t. l = h::t` by METIS_TAC[list_CASES] >> 1625 srw_tac[][MAP] >> Q.ID_SPEC_TAC `h` >> Induct_on `t` >> 1626 asm_simp_tac (srw_ss()) []); 1627 1628val FRONT_CONS = store_thm( 1629 "FRONT_CONS", 1630 ``(!x:'a. FRONT [x] = []) /\ 1631 (!x:'a y z. FRONT (x::y::z) = x :: FRONT (y::z))``, 1632 REWRITE_TAC [FRONT_DEF, NOT_CONS_NIL]); 1633val _ = export_rewrites ["FRONT_CONS"] 1634 1635val LENGTH_FRONT_CONS = store_thm ("LENGTH_FRONT_CONS", 1636``!x xs. LENGTH (FRONT (x::xs)) = LENGTH xs``, 1637Induct_on `xs` THEN ASM_SIMP_TAC bool_ss [FRONT_CONS, LENGTH]) 1638val _ = export_rewrites ["LENGTH_FRONT_CONS"] 1639 1640val FRONT_CONS_EQ_NIL = store_thm ("FRONT_CONS_EQ_NIL", 1641``(!x:'a xs. (FRONT (x::xs) = []) = (xs = [])) /\ 1642 (!x:'a xs. ([] = FRONT (x::xs)) = (xs = [])) /\ 1643 (!x:'a xs. NULL (FRONT (x::xs)) = NULL xs)``, 1644SIMP_TAC bool_ss [GSYM FORALL_AND_THM] THEN 1645Cases_on `xs` THEN SIMP_TAC bool_ss [FRONT_CONS, NOT_NIL_CONS, NULL_DEF]); 1646val _ = export_rewrites ["FRONT_CONS_EQ_NIL"] 1647 1648val APPEND_FRONT_LAST = store_thm( 1649 "APPEND_FRONT_LAST", 1650 ``!l:'a list. ~(l = []) ==> (APPEND (FRONT l) [LAST l] = l)``, 1651 LIST_INDUCT_TAC THEN REWRITE_TAC [NOT_CONS_NIL] THEN 1652 POP_ASSUM MP_TAC THEN Q.SPEC_THEN `l` STRUCT_CASES_TAC list_CASES THEN 1653 REWRITE_TAC [NOT_CONS_NIL] THEN STRIP_TAC THEN 1654 ASM_REWRITE_TAC [FRONT_CONS, LAST_CONS, APPEND]); 1655 1656val LAST_CONS_cond = store_thm( 1657 "LAST_CONS_cond", 1658 ``LAST (h::t) = if t = [] then h else LAST t``, 1659 Cases_on `t` THEN SRW_TAC [] []); 1660 1661val LAST_APPEND_CONS = store_thm( 1662 "LAST_APPEND_CONS", 1663 ``!h l1 l2. LAST (l1 ++ h::l2) = LAST (h::l2)``, 1664 Induct_on `l1` THEN SRW_TAC [] [LAST_CONS_cond]); 1665val _ = export_rewrites ["LAST_APPEND_CONS"] 1666 1667 1668(* ---------------------------------------------------------------------- 1669 TAKE and DROP 1670 ---------------------------------------------------------------------- *) 1671 1672(* these are FIRSTN and BUTFIRSTN from rich_listTheory, but made total *) 1673 1674val TAKE_def = zDefine` 1675 (TAKE n [] = []) /\ 1676 (TAKE n (x::xs) = if n = 0 then [] else x :: TAKE (n - 1) xs) 1677`; 1678 1679val DROP_def = zDefine` 1680 (DROP n [] = []) /\ 1681 (DROP n (x::xs) = if n = 0 then x::xs else DROP (n - 1) xs) 1682`; 1683 1684val TAKE_nil = save_thm( 1685 "TAKE_nil", CONJUNCT1 TAKE_def) 1686val _ = export_rewrites ["TAKE_nil"]; 1687 1688val TAKE_cons = store_thm( 1689 "TAKE_cons", ``0 < n ==> (TAKE n (x::xs) = x::(TAKE (n-1) xs))``, 1690 SRW_TAC[][TAKE_def]); 1691val _ = export_rewrites ["TAKE_cons"]; 1692 1693val DROP_nil = save_thm( 1694 "DROP_nil", CONJUNCT1 DROP_def); 1695val _ = export_rewrites ["DROP_nil"]; 1696 1697val DROP_cons = store_thm( 1698 "DROP_cons",``0 < n ==> (DROP n (x::xs) = DROP (n-1) xs)``, 1699 SRW_TAC[][DROP_def]); 1700val _ = export_rewrites ["DROP_cons"]; 1701 1702val TAKE_0 = store_thm( 1703 "TAKE_0", 1704 ``TAKE 0 l = []``, 1705 Cases_on `l` THEN SRW_TAC [] [TAKE_def]); 1706val _ = export_rewrites ["TAKE_0"] 1707 1708val TAKE_LENGTH_ID = store_thm( 1709 "TAKE_LENGTH_ID", 1710 ``!l. TAKE (LENGTH l) l = l``, 1711 Induct_on `l` THEN SRW_TAC [] []); 1712val _ = export_rewrites ["TAKE_LENGTH_ID"] 1713 1714val LENGTH_TAKE = store_thm( 1715 "LENGTH_TAKE", 1716 ``!n l. n <= LENGTH l ==> (LENGTH (TAKE n l) = n)``, 1717 Induct_on `l` THEN SRW_TAC [numSimps.ARITH_ss] [TAKE_def]); 1718val _ = export_rewrites ["LENGTH_TAKE"] 1719 1720val MAP_TAKE = store_thm( 1721 "MAP_TAKE", 1722 ``!f n l. MAP f (TAKE n l) = TAKE n (MAP f l)``, 1723 Induct_on`l` THEN SRW_TAC[][TAKE_def]); 1724 1725val TAKE_APPEND1 = store_thm( 1726 "TAKE_APPEND1", 1727 ``!n. n <= LENGTH l1 ==> (TAKE n (APPEND l1 l2) = TAKE n l1)``, 1728 Induct_on `l1` THEN SRW_TAC [numSimps.ARITH_ss] [TAKE_def]); 1729 1730val TAKE_APPEND2 = store_thm( 1731 "TAKE_APPEND2", 1732 ``!n. LENGTH l1 < n ==> (TAKE n (l1 ++ l2) = l1 ++ TAKE (n - LENGTH l1) l2)``, 1733 Induct_on `l1` THEN SRW_TAC [numSimps.ARITH_ss] [arithmeticTheory.ADD1]); 1734 1735val DROP_0 = store_thm( 1736 "DROP_0", 1737 ``DROP 0 l = l``, 1738 Induct_on `l` THEN SRW_TAC [] [DROP_def]) 1739val _ = export_rewrites ["DROP_0"] 1740 1741val TAKE_DROP = store_thm( 1742 "TAKE_DROP", 1743 ``!n l. TAKE n l ++ DROP n l = l``, 1744 Induct_on `l` THEN SRW_TAC [numSimps.ARITH_ss] [TAKE_def]); 1745val _ = export_rewrites ["TAKE_DROP"] 1746 1747val LENGTH_DROP = store_thm( 1748 "LENGTH_DROP", 1749 ``!n l. LENGTH (DROP n l) = LENGTH l - n``, 1750 Induct_on `l` THEN SRW_TAC [numSimps.ARITH_ss] [DROP_def]); 1751val _ = export_rewrites ["LENGTH_DROP"] 1752 1753val MEM_DROP = store_thm( 1754"MEM_DROP", 1755``!x ls n. MEM x (DROP n ls) = (n < LENGTH ls /\ (x = (EL n ls))) \/ MEM x (DROP (SUC n) ls)``, 1756GEN_TAC THEN 1757Induct THEN1 SRW_TAC[] [] THEN 1758NTAC 2 GEN_TAC THEN 1759SIMP_TAC (srw_ss()) [] THEN 1760Cases_on `n` THEN SIMP_TAC (srw_ss()) [] THEN 1761PROVE_TAC[]) 1762 1763val DROP_NIL = store_thm( 1764"DROP_NIL", 1765``!ls n. (DROP n ls = []) = (n >= LENGTH ls)``, 1766Induct THEN SRW_TAC[] [DROP_def] THEN numLib.DECIDE_TAC) 1767 1768(* More functions for operating on pairs of lists *) 1769 1770val FOLDL2_def = Define` 1771 (FOLDL2 f a (b::bs) (c::cs) = FOLDL2 f (f a b c) bs cs) /\ 1772 (FOLDL2 f a bs cs = a)` 1773val _ = export_rewrites["FOLDL2_def"] 1774 1775val FOLDL2_cong = store_thm( 1776"FOLDL2_cong", 1777``!l1 l1' l2 l2' a a' f f'. 1778 (l1 = l1') /\ (l2 = l2') /\ (a = a') /\ 1779 (!z b c. MEM b l1' /\ MEM c l2' ==> (f z b c = f' z b c)) 1780 ==> 1781 (FOLDL2 f a l1 l2 = FOLDL2 f' a' l1' l2')``, 1782Induct THEN SIMP_TAC(srw_ss()) [FOLDL2_def] THEN 1783GEN_TAC THEN Cases THEN SRW_TAC[] [FOLDL2_def]) 1784 1785val FOLDL2_FOLDL = store_thm( 1786"FOLDL2_FOLDL", 1787``!l1 l2. (LENGTH l1 = LENGTH l2) ==> !f a. FOLDL2 f a l1 l2 = FOLDL (\a. UNCURRY (f a)) a (ZIP (l1,l2))``, 1788Induct THEN1 SRW_TAC[] [LENGTH_NIL_SYM, ZIP, FOLDL] THEN 1789GEN_TAC THEN Cases THEN SRW_TAC [] [ZIP, FOLDL]) 1790 1791val _ = overload_on ("EVERY2", ``LIST_REL``) 1792val _ = overload_on ("LIST_REL", ``LIST_REL``) 1793 1794val EVERY2_cong = store_thm( 1795"EVERY2_cong", 1796``!l1 l1' l2 l2' P P'. 1797 (l1 = l1') /\ (l2 = l2') /\ 1798 (!x y. MEM x l1' /\ MEM y l2' ==> (P x y = P' x y)) ==> 1799 (EVERY2 P l1 l2 = EVERY2 P' l1' l2')``, 1800Induct THEN SIMP_TAC (srw_ss()) [] THEN 1801GEN_TAC THEN Cases THEN SRW_TAC [] [] THEN 1802METIS_TAC[]) 1803 1804val MAP_EQ_EVERY2 = store_thm( 1805"MAP_EQ_EVERY2", 1806``!f1 f2 l1 l2. (MAP f1 l1 = MAP f2 l2) = 1807 (LENGTH l1 = LENGTH l2) /\ 1808 (EVERY2 (\x y. f1 x = f2 y) l1 l2)``, 1809NTAC 2 GEN_TAC THEN 1810Induct THEN SRW_TAC [] [LENGTH_NIL_SYM, MAP] THEN 1811Cases_on `l2` THEN SRW_TAC [] [MAP] THEN 1812PROVE_TAC[]) 1813 1814val EVERY2_EVERY = store_thm( 1815"EVERY2_EVERY", 1816``!l1 l2 f. EVERY2 f l1 l2 = (LENGTH l1 = LENGTH l2) /\ EVERY (UNCURRY f) (ZIP (l1,l2))``, 1817Induct THEN1 SRW_TAC [] [LENGTH_NIL_SYM, EQ_IMP_THM, ZIP] THEN 1818GEN_TAC THEN Cases THEN SRW_TAC [] [ZIP, EQ_IMP_THM]) 1819 1820val EVERY2_LENGTH = store_thm( 1821"EVERY2_LENGTH", 1822``!P l1 l2. EVERY2 P l1 l2 ==> (LENGTH l1 = LENGTH l2)``, 1823PROVE_TAC[EVERY2_EVERY]) 1824 1825val EVERY2_mono = save_thm("EVERY2_mono", LIST_REL_mono) 1826 1827(* ---------------------------------------------------------------------- 1828 ALL_DISTINCT 1829 ---------------------------------------------------------------------- *) 1830 1831val ALL_DISTINCT = new_recursive_definition { 1832 def = Term`(ALL_DISTINCT [] = T) /\ 1833 (ALL_DISTINCT (h::t) = ~MEM h t /\ ALL_DISTINCT t)`, 1834 name = "ALL_DISTINCT", 1835 rec_axiom = list_Axiom}; 1836val _ = export_rewrites ["ALL_DISTINCT"] 1837 1838val lemma = prove( 1839 ``!l x. (FILTER ((=) x) l = []) = ~MEM x l``, 1840 LIST_INDUCT_TAC THEN 1841 ASM_SIMP_TAC (bool_ss ++ COND_elim_ss) 1842 [FILTER, MEM, NOT_CONS_NIL, EQ_IMP_THM, 1843 LEFT_AND_OVER_OR, FORALL_AND_THM, DISJ_IMP_THM]); 1844 1845val ALL_DISTINCT_FILTER = store_thm( 1846 "ALL_DISTINCT_FILTER", 1847 ``!l. ALL_DISTINCT l = !x. MEM x l ==> (FILTER ((=) x) l = [x])``, 1848 LIST_INDUCT_TAC THEN 1849 ASM_SIMP_TAC (bool_ss ++ COND_elim_ss) 1850 [ALL_DISTINCT, MEM, FILTER, DISJ_IMP_THM, 1851 FORALL_AND_THM, CONS_11, EQ_IMP_THM, lemma] THEN 1852 metisLib.METIS_TAC []); 1853 1854val FILTER_ALL_DISTINCT = store_thm ( 1855 "FILTER_ALL_DISTINCT", 1856 ``!P l. ALL_DISTINCT l ==> ALL_DISTINCT (FILTER P l)``, 1857 Induct_on `l` THEN SRW_TAC [] [MEM_FILTER]); 1858 1859val ALL_DISTINCT_MAP = store_thm( 1860"ALL_DISTINCT_MAP", 1861``!f ls. ALL_DISTINCT (MAP f ls) ==> ALL_DISTINCT ls``, 1862GEN_TAC THEN Induct THEN SRW_TAC[][ALL_DISTINCT, MAP, MEM_MAP] THEN PROVE_TAC[]) 1863 1864val ALL_DISTINCT_EL_EQ = store_thm ( 1865 "EL_ALL_DISTINCT_EL_EQ", 1866 ``!l. ALL_DISTINCT l = 1867 (!n1 n2. n1 < LENGTH l /\ n2 < LENGTH l ==> 1868 ((EL n1 l = EL n2 l) = (n1 = n2)))``, 1869 Induct THEN SRW_TAC [] [] THEN EQ_TAC THENL [ 1870 REPEAT STRIP_TAC THEN Cases_on `n1` THEN Cases_on `n2` THEN 1871 SRW_TAC [numSimps.ARITH_ss] [] THEN PROVE_TAC [MEM_EL, LESS_MONO_EQ], 1872 1873 REPEAT STRIP_TAC THENL [ 1874 FULL_SIMP_TAC (srw_ss()) [MEM_EL] THEN 1875 FIRST_X_ASSUM (Q.SPECL_THEN [`0`, `SUC n`] MP_TAC) THEN 1876 SRW_TAC [] [], 1877 1878 FIRST_X_ASSUM (Q.SPECL_THEN [`SUC n1`, `SUC n2`] MP_TAC) THEN 1879 SRW_TAC [] [] 1880 ] 1881 ]); 1882 1883val ALL_DISTINCT_EL_IMP = store_thm ( 1884 "ALL_DISTINCT_EL_IMP", 1885 ``!l n1 n2. ALL_DISTINCT l /\ n1 < LENGTH l /\ n2 < LENGTH l ==> 1886 ((EL n1 l = EL n2 l) = (n1 = n2))``, 1887 PROVE_TAC[ALL_DISTINCT_EL_EQ]); 1888 1889 1890val ALL_DISTINCT_APPEND = store_thm ( 1891 "ALL_DISTINCT_APPEND", 1892 ``!l1 l2. ALL_DISTINCT (l1++l2) = 1893 (ALL_DISTINCT l1 /\ ALL_DISTINCT l2 /\ 1894 (!e. MEM e l1 ==> ~(MEM e l2)))``, 1895 Induct THEN SRW_TAC [] [] THEN PROVE_TAC []); 1896 1897val ALL_DISTINCT_SING = store_thm( 1898 "ALL_DISTINCT_SING", 1899 ``!x. ALL_DISTINCT [x]``, 1900 SRW_TAC [] []); 1901 1902val ALL_DISTINCT_ZIP = store_thm( 1903 "ALL_DISTINCT_ZIP", 1904 ``!l1 l2. ALL_DISTINCT l1 /\ (LENGTH l1 = LENGTH l2) ==> ALL_DISTINCT (ZIP (l1,l2))``, 1905 Induct THEN Cases_on `l2` THEN SRW_TAC [] [ZIP] THEN RES_TAC THEN 1906 FULL_SIMP_TAC (srw_ss()) [MEM_EL] THEN 1907 SRW_TAC [] [LENGTH_ZIP] THEN 1908 Q.MATCH_ABBREV_TAC `~X \/ Y` THEN 1909 Cases_on `X` THEN SRW_TAC [] [Abbr`Y`] THEN 1910 SRW_TAC [] [EL_ZIP] THEN METIS_TAC []); 1911 1912val ALL_DISTINCT_ZIP_SWAP = store_thm( 1913 "ALL_DISTINCT_ZIP_SWAP", 1914 ``!l1 l2. ALL_DISTINCT (ZIP (l1,l2)) /\ (LENGTH l1 = LENGTH l2) ==> ALL_DISTINCT (ZIP (l2,l1))``, 1915 SRW_TAC [] [ALL_DISTINCT_EL_EQ] THEN 1916 Q.PAT_X_ASSUM `X = Y` (ASSUME_TAC o SYM) THEN 1917 FULL_SIMP_TAC (srw_ss()) [EL_ZIP, LENGTH_ZIP] THEN 1918 METIS_TAC []) 1919 1920val ALL_DISTINCT_REVERSE = store_thm ( 1921 "ALL_DISTINCT_REVERSE[simp]", 1922 ``!l. ALL_DISTINCT (REVERSE l) = ALL_DISTINCT l``, 1923 SIMP_TAC bool_ss [ALL_DISTINCT_FILTER, MEM_REVERSE, FILTER_REVERSE] THEN 1924 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1925 RES_TAC THEN 1926 `(FILTER ($= x) l) = REVERSE [x]` by METIS_TAC[REVERSE_REVERSE] THEN 1927 FULL_SIMP_TAC bool_ss [REVERSE_DEF, APPEND], 1928 ASM_SIMP_TAC bool_ss [REVERSE_DEF, APPEND] 1929 ]); 1930 1931val ALL_DISTINCT_FLAT_REVERSE = store_thm("ALL_DISTINCT_FLAT_REVERSE[simp]", 1932 ``!xs. ALL_DISTINCT (FLAT (REVERSE xs)) = ALL_DISTINCT (FLAT xs)``, 1933 Induct \\ FULL_SIMP_TAC(srw_ss())[ALL_DISTINCT_APPEND] 1934 \\ FULL_SIMP_TAC(srw_ss())[MEM_FLAT,PULL_EXISTS] \\ METIS_TAC []); 1935 1936(* ---------------------------------------------------------------------- 1937 LRC 1938 Where NRC has the number of steps in a transitive path, 1939 LRC has a list of the elements in the path (excluding the rightmost) 1940 ---------------------------------------------------------------------- *) 1941 1942val LRC_def = Define` 1943 (LRC R [] x y = (x = y)) /\ 1944 (LRC R (h::t) x y = 1945 (x = h) /\ ?z. R x z /\ LRC R t z y)`; 1946 1947val NRC_LRC = Q.store_thm( 1948"NRC_LRC", 1949`NRC R n x y <=> ?ls. LRC R ls x y /\ (LENGTH ls = n)`, 1950MAP_EVERY Q.ID_SPEC_TAC [`y`,`x`] THEN 1951Induct_on `n` THEN SRW_TAC [] [] THEN1 ( 1952 SRW_TAC [] [EQ_IMP_THM] THEN1 ( 1953 SRW_TAC [] [LRC_def] ) THEN 1954 FULL_SIMP_TAC (srw_ss()) [LRC_def] 1955) THEN 1956SRW_TAC [] [arithmeticTheory.NRC, EQ_IMP_THM] THEN1 ( 1957 Q.EXISTS_TAC `x::ls` THEN 1958 SRW_TAC [] [LRC_def] THEN 1959 METIS_TAC [] ) THEN 1960Cases_on `ls` THEN FULL_SIMP_TAC (srw_ss()) [LRC_def] THEN 1961SRW_TAC [] [] THEN METIS_TAC []); 1962 1963val LRC_MEM = Q.store_thm( 1964"LRC_MEM", 1965`LRC R ls x y /\ MEM e ls ==> ?z t. R e z /\ LRC R t z y`, 1966Q_TAC SUFF_TAC 1967`!ls x y. LRC R ls x y ==> !e. MEM e ls ==> ?z t. R e z /\ LRC R t z y` 1968THEN1 METIS_TAC [] THEN 1969Induct THEN SRW_TAC [] [LRC_def] THEN METIS_TAC []); 1970 1971val LRC_MEM_right = Q.store_thm( 1972"LRC_MEM_right", 1973`LRC R (h::t) x y /\ MEM e t ==> ?z p. R z e /\ LRC R p x z`, 1974Q_TAC SUFF_TAC 1975`!ls x y. LRC R ls x y ==> !h t e. (ls = h::t) /\ MEM e t ==> ?z p. R z e /\ LRC R p x z` 1976THEN1 METIS_TAC [] THEN 1977Induct THEN SRW_TAC [] [LRC_def] THEN 1978Cases_on `ls` THEN FULL_SIMP_TAC (srw_ss()) [LRC_def] THEN 1979SRW_TAC [] [] THENL [ 1980 MAP_EVERY Q.EXISTS_TAC [`h`,`[]`] THEN SRW_TAC [] [LRC_def], 1981 RES_TAC THEN 1982 MAP_EVERY Q.EXISTS_TAC [`z''`,`h::p`] THEN 1983 SRW_TAC [] [LRC_def] THEN 1984 METIS_TAC [] 1985]); 1986 1987(* ---------------------------------------------------------------------- 1988 Theorems relating (finite) sets and lists. First 1989 1990 LIST_TO_SET : 'a list -> 'a set 1991 1992 which is overloaded to "set". 1993 ---------------------------------------------------------------------- *) 1994 1995val LIST_TO_SET_APPEND = Q.store_thm 1996("LIST_TO_SET_APPEND", 1997 `!l1 l2. set (l1 ++ l2) = set l1 UNION set l2`, 1998 Induct THEN SRW_TAC [] [INSERT_UNION_EQ]); 1999val _ = export_rewrites ["LIST_TO_SET_APPEND"] 2000 2001val UNION_APPEND = save_thm ("UNION_APPEND", GSYM LIST_TO_SET_APPEND) 2002 2003val LIST_TO_SET_EQ_EMPTY = store_thm( 2004 "LIST_TO_SET_EQ_EMPTY", 2005 ``((set l = {}) <=> (l = [])) /\ (({} = set l) <=> (l = []))``, 2006 Cases_on `l` THEN SRW_TAC [] []); 2007val _ = export_rewrites ["LIST_TO_SET_EQ_EMPTY"] 2008 2009val FINITE_LIST_TO_SET = Q.store_thm 2010("FINITE_LIST_TO_SET", 2011 `!l. FINITE (set l)`, 2012 Induct THEN SRW_TAC [] []); 2013val _ = export_rewrites ["FINITE_LIST_TO_SET"] 2014 2015val SUM_IMAGE_LIST_TO_SET_upper_bound = store_thm( 2016 "SUM_IMAGE_LIST_TO_SET_upper_bound", 2017 ``!ls. SIGMA f (set ls) <= SUM (MAP f ls)``, 2018 Induct THEN 2019 SRW_TAC [] [MAP, SUM, SUM_IMAGE_THM, SUM_IMAGE_DELETE] THEN 2020 numLib.DECIDE_TAC); 2021 2022val SUM_MAP_MEM_bound = store_thm( 2023"SUM_MAP_MEM_bound", 2024``!f x ls. MEM x ls ==> f x <= SUM (MAP f ls)``, 2025NTAC 2 GEN_TAC THEN Induct THEN SRW_TAC[] [] THEN 2026FULL_SIMP_TAC(srw_ss()++numSimps.ARITH_ss)[MEM, MAP, SUM]) 2027 2028val INJ_MAP_EQ = store_thm( 2029"INJ_MAP_EQ", 2030``!f l1 l2. (INJ f (set l1 UNION set l2) UNIV) /\ (MAP f l1 = MAP f l2) ==> (l1 = l2)``, 2031GEN_TAC THEN Induct THEN1 SRW_TAC[] [MAP] THEN 2032GEN_TAC THEN Cases THEN SRW_TAC[] [MAP] THEN1 ( 2033 IMP_RES_TAC INJ_DEF THEN 2034 FIRST_X_ASSUM (MATCH_MP_TAC o MP_CANON) THEN 2035 SRW_TAC [] [] ) THEN 2036PROVE_TAC[INJ_SUBSET, SUBSET_REFL, SUBSET_DEF, IN_UNION, IN_INSERT]) 2037 2038(* this turns out to be more useful; in particular, INJ_MAP_EQ can't 2039 be used as an introduction rule without explicit instantiation of 2040 its beta type variable, which only appears in the assumption *) 2041val INJ_MAP_EQ_IFF = store_thm( 2042 "INJ_MAP_EQ_IFF", 2043 ``!f l1 l2. 2044 INJ f (set l1 UNION set l2) UNIV ==> 2045 ((MAP f l1 = MAP f l2) <=> (l1 = l2))``, 2046 rw[] >> EQ_TAC >- metis_tac[INJ_MAP_EQ] >> rw[]) 2047 2048local open numLib in 2049val CARD_LIST_TO_SET = Q.store_thm( 2050"CARD_LIST_TO_SET", 2051`CARD (set ls) <= LENGTH ls`, 2052Induct_on `ls` THEN SRW_TAC [] [] THEN 2053DECIDE_TAC); 2054end 2055 2056val ALL_DISTINCT_CARD_LIST_TO_SET = Q.store_thm( 2057"ALL_DISTINCT_CARD_LIST_TO_SET", 2058`!ls. ALL_DISTINCT ls ==> (CARD (set ls) = LENGTH ls)`, 2059Induct THEN SRW_TAC [] []); 2060 2061val th1 = MATCH_MP arithmeticTheory.LESS_EQ_IMP_LESS_SUC CARD_LIST_TO_SET ; 2062val th2 = MATCH_MP prim_recTheory.LESS_NOT_EQ th1 ; 2063 2064val CARD_LIST_TO_SET_ALL_DISTINCT = Q.store_thm( 2065"CARD_LIST_TO_SET_ALL_DISTINCT", 2066`!ls. (CARD (set ls) = LENGTH ls) ==> ALL_DISTINCT ls`, 2067Induct THEN SRW_TAC [] [th2]); 2068 2069val LIST_TO_SET_REVERSE = store_thm( 2070 "LIST_TO_SET_REVERSE", 2071 ``!ls: 'a list. set (REVERSE ls) = set ls``, 2072 Induct THEN SRW_TAC [] [pred_setTheory.EXTENSION]); 2073val _ = export_rewrites ["LIST_TO_SET_REVERSE"] 2074 2075val LIST_TO_SET_THM = save_thm("LIST_TO_SET_THM", LIST_TO_SET) 2076val LIST_TO_SET_MAP = store_thm ("LIST_TO_SET_MAP", 2077``!f l. LIST_TO_SET (MAP f l) = IMAGE f (LIST_TO_SET l)``, 2078Induct_on `l` THEN 2079ASM_SIMP_TAC bool_ss [pred_setTheory.IMAGE_EMPTY, pred_setTheory.IMAGE_INSERT, 2080 MAP, LIST_TO_SET_THM]); 2081 2082val LIST_TO_SET_FILTER = store_thm( 2083 "LIST_TO_SET_FILTER", 2084 ``LIST_TO_SET (FILTER P l) = { x | P x } INTER LIST_TO_SET l``, 2085 SRW_TAC [] [pred_setTheory.EXTENSION, MEM_FILTER]); 2086 2087 2088(* ---------------------------------------------------------------------- 2089 SET_TO_LIST : 'a set -> 'a list 2090 2091 Only defined if the set is finite; order of elements in list is 2092 unspecified. 2093 ---------------------------------------------------------------------- *) 2094 2095val SET_TO_LIST_defn = Lib.with_flag (Defn.def_suffix, "") Defn.Hol_defn 2096 "SET_TO_LIST" 2097 `SET_TO_LIST s = 2098 if FINITE s then 2099 if s={} then [] 2100 else CHOICE s :: SET_TO_LIST (REST s) 2101 else ARB`; 2102 2103(*--------------------------------------------------------------------------- 2104 Termination of SET_TO_LIST. 2105 ---------------------------------------------------------------------------*) 2106 2107val (SET_TO_LIST_EQN, SET_TO_LIST_IND) = 2108 Defn.tprove (SET_TO_LIST_defn, 2109 TotalDefn.WF_REL_TAC `measure CARD` THEN 2110 PROVE_TAC [CARD_PSUBSET, REST_PSUBSET]); 2111 2112(*--------------------------------------------------------------------------- 2113 Desired recursion equation. 2114 2115 FINITE s |- SET_TO_LIST s = if s = {} then [] 2116 else CHOICE s::SET_TO_LIST (REST s) 2117 2118 ---------------------------------------------------------------------------*) 2119 2120val SET_TO_LIST_THM = save_thm("SET_TO_LIST_THM", 2121 DISCH_ALL (ASM_REWRITE_RULE [ASSUME ``FINITE s``] SET_TO_LIST_EQN)); 2122 2123val SET_TO_LIST_IND = save_thm("SET_TO_LIST_IND", SET_TO_LIST_IND); 2124 2125 2126 2127(*--------------------------------------------------------------------------- 2128 Some consequences 2129 ---------------------------------------------------------------------------*) 2130 2131val SET_TO_LIST_EMPTY = store_thm( 2132 "SET_TO_LIST_EMPTY", 2133 ``SET_TO_LIST {} = []``, 2134 SRW_TAC [] [SET_TO_LIST_THM]) 2135val _ = export_rewrites ["SET_TO_LIST_EMPTY"] 2136 2137val SET_TO_LIST_INV = Q.store_thm("SET_TO_LIST_INV", 2138`!s. FINITE s ==> (LIST_TO_SET(SET_TO_LIST s) = s)`, 2139 Induction.recInduct SET_TO_LIST_IND 2140 THEN RW_TAC bool_ss [] 2141 THEN ONCE_REWRITE_TAC [UNDISCH SET_TO_LIST_THM] 2142 THEN RW_TAC bool_ss [LIST_TO_SET_THM] 2143 THEN PROVE_TAC [REST_DEF, FINITE_DELETE, CHOICE_INSERT_REST]); 2144 2145val SET_TO_LIST_CARD = Q.store_thm("SET_TO_LIST_CARD", 2146`!s. FINITE s ==> (LENGTH (SET_TO_LIST s) = CARD s)`, 2147 Induction.recInduct SET_TO_LIST_IND 2148 THEN REPEAT STRIP_TAC 2149 THEN SRW_TAC [] [Once (UNDISCH SET_TO_LIST_THM)] 2150 THEN `FINITE (REST s)` by METIS_TAC [REST_DEF, FINITE_DELETE] 2151 THEN `~(CARD s = 0)` by METIS_TAC [CARD_EQ_0] 2152 THEN SRW_TAC [numSimps.ARITH_ss] [REST_DEF, CHOICE_DEF]); 2153 2154val SET_TO_LIST_IN_MEM = Q.store_thm("SET_TO_LIST_IN_MEM", 2155`!s. FINITE s ==> !x. x IN s = MEM x (SET_TO_LIST s)`, 2156 Induction.recInduct SET_TO_LIST_IND 2157 THEN RW_TAC bool_ss [] 2158 THEN ONCE_REWRITE_TAC [UNDISCH SET_TO_LIST_THM] 2159 THEN RW_TAC bool_ss [MEM, NOT_IN_EMPTY] 2160 THEN PROVE_TAC [REST_DEF, FINITE_DELETE, IN_INSERT, CHOICE_INSERT_REST]); 2161 2162(* this version of the above is a more likely rewrite: a complicated LHS 2163 turns into a simple RHS *) 2164val MEM_SET_TO_LIST = Q.store_thm("MEM_SET_TO_LIST", 2165`!s. FINITE s ==> !x. MEM x (SET_TO_LIST s) = x IN s`, 2166 METIS_TAC [SET_TO_LIST_IN_MEM]); 2167val _ = export_rewrites ["MEM_SET_TO_LIST"]; 2168 2169val SET_TO_LIST_SING = store_thm( 2170 "SET_TO_LIST_SING", 2171 ``SET_TO_LIST {x} = [x]``, 2172 SRW_TAC [] [SET_TO_LIST_THM]); 2173val _ = export_rewrites ["SET_TO_LIST_SING"] 2174 2175val ALL_DISTINCT_SET_TO_LIST = store_thm("ALL_DISTINCT_SET_TO_LIST", 2176 ``!s. FINITE s ==> ALL_DISTINCT (SET_TO_LIST s)``, 2177 Induction.recInduct SET_TO_LIST_IND THEN 2178 REPEAT STRIP_TAC THEN 2179 IMP_RES_TAC SET_TO_LIST_THM THEN 2180 `FINITE (REST s)` by PROVE_TAC[pred_setTheory.FINITE_DELETE, 2181 pred_setTheory.REST_DEF] THEN 2182 Cases_on `s = EMPTY` THEN 2183 FULL_SIMP_TAC bool_ss [ALL_DISTINCT, MEM_SET_TO_LIST, 2184 pred_setTheory.CHOICE_NOT_IN_REST]); 2185val _ = export_rewrites ["ALL_DISTINCT_SET_TO_LIST"]; 2186 2187val ITSET_eq_FOLDL_SET_TO_LIST = Q.store_thm( 2188"ITSET_eq_FOLDL_SET_TO_LIST", 2189`!s. FINITE s ==> !f a. ITSET f s a = FOLDL (combin$C f) a (SET_TO_LIST s)`, 2190HO_MATCH_MP_TAC pred_setTheory.FINITE_COMPLETE_INDUCTION THEN 2191SRW_TAC [] [pred_setTheory.ITSET_THM, SET_TO_LIST_THM, FOLDL]); 2192 2193 2194(* ---------------------------------------------------------------------- 2195 isPREFIX 2196 ---------------------------------------------------------------------- *) 2197 2198val isPREFIX = bDefine` 2199 (isPREFIX [] l = T) /\ 2200 (isPREFIX (h::t) l = case l of [] => F 2201 | h'::t' => (h = h') /\ isPREFIX t t') 2202`; 2203val _ = export_rewrites ["isPREFIX"] 2204 2205val _ = overload_on ("<<=", ``isPREFIX``) 2206 2207(* type annotations are there solely to make theorem have only one 2208 type variable; without them the theorem ends up with three (because the 2209 three clauses are independent). *) 2210val isPREFIX_THM = store_thm( 2211 "isPREFIX_THM", 2212 ``(([]:'a list) <<= l = T) /\ 2213 ((h::t:'a list) <<= [] = F) /\ 2214 ((h1::t1:'a list) <<= h2::t2 = (h1 = h2) /\ isPREFIX t1 t2)``, 2215 SRW_TAC [] []) 2216val _ = export_rewrites ["isPREFIX_THM"] 2217 2218val isPREFIX_NILR = Q.store_thm( 2219 "isPREFIX_NILR[simp]", 2220 ���x <<= [] <=> (x = [])���, 2221 Cases_on ���x��� >> simp[]); 2222 2223val isPREFIX_CONSR = Q.store_thm( 2224 "isPREFIX_CONSR", 2225 ���x <<= y::ys <=> (x = []) \/ ?xs. (x = y::xs) /\ xs <<= ys���, 2226 Cases_on ���x��� >> simp[]); 2227 2228(* ---------------------------------------------------------------------- 2229 SNOC 2230 ---------------------------------------------------------------------- *) 2231 2232(* use new_recursive_definition to get quantification and variable names 2233 exactly as they were in rich_listTheory *) 2234val SNOC = new_recursive_definition { 2235 def = ``(!x:'a. SNOC x [] = [x]) /\ 2236 (!x:'a x' l. SNOC x (CONS x' l) = CONS x' (SNOC x l))``, 2237 name = "SNOC", 2238 rec_axiom = list_Axiom 2239}; 2240val _ = BasicProvers.export_rewrites ["SNOC"] 2241 2242val LENGTH_SNOC = store_thm( 2243 "LENGTH_SNOC", 2244 ``!(x:'a) l. LENGTH (SNOC x l) = SUC (LENGTH l)``, 2245 GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [LENGTH, SNOC]); 2246val _ = export_rewrites ["LENGTH_SNOC"] 2247 2248val LAST_SNOC = store_thm( 2249 "LAST_SNOC", 2250 ``!x:'a l. LAST (SNOC x l) = x``, 2251 GEN_TAC THEN LIST_INDUCT_TAC THEN 2252 RW_TAC bool_ss [SNOC, LAST_DEF] THEN 2253 POP_ASSUM MP_TAC THEN 2254 Q.SPEC_THEN `l` STRUCT_CASES_TAC list_CASES THEN 2255 RW_TAC bool_ss [SNOC]); 2256val _ = export_rewrites ["LAST_SNOC"] 2257 2258val FRONT_SNOC = store_thm( 2259 "FRONT_SNOC", 2260 ``!x:'a l. FRONT (SNOC x l) = l``, 2261 GEN_TAC THEN LIST_INDUCT_TAC THEN 2262 RW_TAC bool_ss [SNOC, FRONT_DEF] THEN 2263 POP_ASSUM MP_TAC THEN 2264 Q.SPEC_THEN `l` STRUCT_CASES_TAC list_CASES THEN 2265 RW_TAC bool_ss [SNOC]); 2266val _ = export_rewrites ["FRONT_SNOC"] 2267 2268val SNOC_APPEND = store_thm("SNOC_APPEND", 2269 ``!x (l:('a) list). SNOC x l = APPEND l [x]``, 2270 GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [SNOC, APPEND]); 2271 2272val LIST_TO_SET_SNOC = Q.store_thm("LIST_TO_SET_SNOC", 2273 `set (SNOC x ls) = x INSERT set ls`, 2274 Induct_on `ls` THEN SRW_TAC [] [INSERT_COMM]); 2275 2276val MAP_SNOC = store_thm("MAP_SNOC", 2277 (���!(f:'a->'b) x (l:'a list). MAP f(SNOC x l) = SNOC(f x)(MAP f l)���), 2278 (REWRITE_TAC [SNOC_APPEND, MAP_APPEND, MAP])); 2279 2280val EL_SNOC = store_thm("EL_SNOC", 2281 (���!n (l:'a list). n < (LENGTH l) ==> (!x. EL n (SNOC x l) = EL n l)���), 2282 INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH, NOT_LESS_0] 2283 THENL[ 2284 REWRITE_TAC[SNOC, EL, HD], 2285 REWRITE_TAC[SNOC, EL, TL, LESS_MONO_EQ] 2286 THEN FIRST_ASSUM MATCH_ACCEPT_TAC]); 2287 2288val EL_LENGTH_SNOC = store_thm("EL_LENGTH_SNOC", 2289 (���!l:'a list. !x. EL (LENGTH l) (SNOC x l) = x���), 2290 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[EL, SNOC, HD, TL, LENGTH]); 2291 2292val APPEND_SNOC = store_thm("APPEND_SNOC", 2293 (���!l1 (x:'a) l2. APPEND l1 (SNOC x l2) = SNOC x (APPEND l1 l2)���), 2294 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[APPEND, SNOC]); 2295 2296val EVERY_SNOC = store_thm("EVERY_SNOC", 2297 (���!P (x:'a) l. EVERY P (SNOC x l) = EVERY P l /\ P x���), 2298 GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC 2299 THEN ASM_REWRITE_TAC[SNOC, EVERY_DEF, CONJ_ASSOC]); 2300 2301val EXISTS_SNOC = store_thm("EXISTS_SNOC", 2302 (���!P (x:'a) l. EXISTS P (SNOC x l) = P x \/ (EXISTS P l)���), 2303 GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC 2304 THEN ASM_REWRITE_TAC[SNOC, EXISTS_DEF] THEN GEN_TAC 2305 THEN PURE_ONCE_REWRITE_TAC[DISJ_ASSOC] 2306 THEN CONV_TAC ((RAND_CONV o RATOR_CONV o ONCE_DEPTH_CONV) 2307 (REWR_CONV DISJ_SYM)) THEN REFL_TAC); 2308 2309val MEM_SNOC = store_thm("MEM_SNOC", 2310 (���!(y:'a) x l. MEM y (SNOC x l) = (y = x) \/ MEM y l���), 2311 GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC 2312 THEN ASM_REWRITE_TAC[SNOC, MEM] THEN GEN_TAC 2313 THEN PURE_ONCE_REWRITE_TAC[DISJ_ASSOC] 2314 THEN CONV_TAC ((RAND_CONV o RATOR_CONV o ONCE_DEPTH_CONV) 2315 (REWR_CONV DISJ_SYM)) THEN REFL_TAC); 2316val _ = export_rewrites ["MEM_SNOC"] 2317 2318val SNOC_11 = store_thm( 2319 "SNOC_11", 2320 ``!x y a b. (SNOC x y = SNOC a b) <=> (x = a) /\ (y = b)``, 2321 SRW_TAC [] [EQ_IMP_THM] THENL [ 2322 POP_ASSUM (MP_TAC o Q.AP_TERM `LAST`) THEN SRW_TAC [] [LAST_SNOC], 2323 POP_ASSUM (MP_TAC o Q.AP_TERM `FRONT`) THEN SRW_TAC [] [FRONT_SNOC] 2324 ]); 2325val _ = export_rewrites ["SNOC_11"] 2326 2327val REVERSE_SNOC_DEF = store_thm ( 2328 "REVERSE_SNOC_DEF", 2329 ``(REVERSE [] = []) /\ 2330 (!x:'a l. REVERSE (x::l) = SNOC x (REVERSE l))``, 2331 REWRITE_TAC [REVERSE_DEF, SNOC_APPEND]); 2332 2333val REVERSE_SNOC = store_thm( 2334 "REVERSE_SNOC", 2335 ``!(x:'a) l. REVERSE (SNOC x l) = CONS x (REVERSE l)``, 2336 GEN_TAC THEN LIST_INDUCT_TAC 2337 THEN ASM_REWRITE_TAC[SNOC, REVERSE_SNOC_DEF]); 2338 2339val forall_REVERSE = TAC_PROOF(([], 2340 (���!P. (!l:('a)list. P(REVERSE l)) = (!l. P l)���)), 2341 GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN GEN_TAC 2342 THEN POP_ASSUM (ACCEPT_TAC o (REWRITE_RULE[REVERSE_REVERSE] 2343 o (SPEC (���REVERSE l:('a)list���))))); 2344 2345val f_REVERSE_lemma = TAC_PROOF (([], 2346 (���!f1 f2. 2347 ((\x. (f1:('a)list->'b) (REVERSE x)) = (\x. f2 (REVERSE x))) = (f1 = f2)���)), 2348 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL[ 2349 POP_ASSUM (fn x => ACCEPT_TAC (EXT (REWRITE_RULE[REVERSE_REVERSE] 2350 (GEN (���x:('a)list���) (BETA_RULE (AP_THM x (���REVERSE (x:('a)list)���))))))), 2351 ASM_REWRITE_TAC[]]); 2352 2353 2354val SNOC_Axiom_old = prove( 2355 ���!(e:'b) (f:'b -> ('a -> (('a)list -> 'b))). 2356 ?! fn1. 2357 (fn1[] = e) /\ 2358 (!x l. fn1(SNOC x l) = f(fn1 l)x l)���, 2359 2360 let val lemma = CONV_RULE (EXISTS_UNIQUE_CONV) 2361 (REWRITE_RULE[REVERSE_REVERSE] (BETA_RULE (SPECL 2362 [(���e:'b���),(���(\ft x l. f ft x (REVERSE l)):'b -> ('a -> (('a)list -> 'b))���)] 2363 (PURE_ONCE_REWRITE_RULE 2364 [SYM (CONJUNCT1 REVERSE_DEF), 2365 PURE_ONCE_REWRITE_RULE[SYM (SPEC_ALL REVERSE_SNOC)] 2366 (BETA_RULE (SPEC (���\l:('a)list.fn1(CONS x l) = 2367 (f:'b -> ('a -> (('a)list -> 'b)))(fn1 l)x l���) 2368 (CONV_RULE (ONCE_DEPTH_CONV SYM_CONV) forall_REVERSE)))] 2369 list_Axiom_old)))) 2370 in 2371 REPEAT GEN_TAC THEN CONV_TAC EXISTS_UNIQUE_CONV 2372 THEN STRIP_ASSUME_TAC lemma THEN CONJ_TAC THENL 2373 [ 2374 EXISTS_TAC (���(fn1:('a)list->'b) o REVERSE���) 2375 THEN REWRITE_TAC[o_DEF] THEN BETA_TAC THEN ASM_REWRITE_TAC[], 2376 2377 REPEAT GEN_TAC THEN POP_ASSUM (ACCEPT_TAC o SPEC_ALL o 2378 REWRITE_RULE[REVERSE_REVERSE, f_REVERSE_lemma] o 2379 BETA_RULE o REWRITE_RULE[o_DEF] o 2380 SPECL [(���(fn1' o REVERSE):('a)list->'b���),(���(fn1'' o REVERSE):('a)list->'b���)]) 2381 ] 2382 end); 2383 2384val SNOC_Axiom = store_thm( 2385 "SNOC_Axiom", 2386 ���!e f. ?fn:'a list -> 'b. 2387 (fn [] = e) /\ 2388 (!x l. fn (SNOC x l) = f x l (fn l))���, 2389 REPEAT GEN_TAC THEN 2390 STRIP_ASSUME_TAC (CONV_RULE EXISTS_UNIQUE_CONV 2391 (BETA_RULE 2392 (Q.SPECL [`e`, `\x y z. f y z x`] SNOC_Axiom_old))) THEN 2393 Q.EXISTS_TAC `fn1` THEN ASM_REWRITE_TAC []); 2394 2395val SNOC_INDUCT = save_thm("SNOC_INDUCT", prove_induction_thm SNOC_Axiom_old); 2396val SNOC_CASES = save_thm("SNOC_CASES", hd (prove_cases_thm SNOC_INDUCT)); 2397 2398(*--------------------------------------------------------------*) 2399(* List generator *) 2400(* GENLIST f n = [f 0;...; f(n-1)] *) 2401(*--------------------------------------------------------------*) 2402 2403val GENLIST = new_recursive_definition 2404 {name = "GENLIST", 2405 rec_axiom = num_Axiom, 2406 def = ���(GENLIST (f:num->'a) 0 = []) /\ 2407 (GENLIST f (SUC n) = SNOC (f n) (GENLIST f n))���}; 2408 2409val LENGTH_GENLIST = store_thm("LENGTH_GENLIST", 2410 (���!(f:num->'a) n. LENGTH(GENLIST f n) = n���), 2411 GEN_TAC THEN INDUCT_TAC 2412 THEN ASM_REWRITE_TAC[GENLIST, LENGTH, LENGTH_SNOC]); 2413val _ = export_rewrites ["LENGTH_GENLIST"] 2414 2415val GENLIST_AUX = bDefine` 2416 (GENLIST_AUX f 0 l = l) /\ 2417 (GENLIST_AUX f (SUC n) l = GENLIST_AUX f n ((f n)::l))`; 2418 2419val SUC_RULE = CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV; 2420 2421val GENLIST_AUX_compute = save_thm( 2422 "GENLIST_AUX_compute", 2423 SUC_RULE GENLIST_AUX) 2424val _ = export_rewrites ["GENLIST_AUX_compute"] 2425 2426(*--------------------------------------------------------------------------- 2427 List padding (left and right) 2428 ---------------------------------------------------------------------------*) 2429 2430val PAD_LEFT = bDefine` 2431 PAD_LEFT c n s = (GENLIST (K c) (n - LENGTH s)) ++ s`; 2432 2433val PAD_RIGHT = bDefine` 2434 PAD_RIGHT c n s = s ++ (GENLIST (K c) (n - LENGTH s))`; 2435 2436(*--------------------------------------------------------------------------- 2437 Theorems about genlist. From Anthony Fox's theories. Added by Thomas Tuerk. 2438 Moved from rich_listTheory. 2439 ---------------------------------------------------------------------------*) 2440 2441val MAP_GENLIST = store_thm("MAP_GENLIST", 2442 ``!f g n. MAP f (GENLIST g n) = GENLIST (f o g) n``, 2443 Induct_on `n` 2444 THEN ASM_SIMP_TAC arith_ss [GENLIST, MAP_SNOC, MAP, o_THM]); 2445 2446val EL_GENLIST = store_thm("EL_GENLIST", 2447 ``!f n x. x < n ==> (EL x (GENLIST f n) = f x)``, 2448 Induct_on `n` THEN1 SIMP_TAC arith_ss [] THEN 2449 REPEAT STRIP_TAC THEN REWRITE_TAC [GENLIST] THEN 2450 Cases_on `x < n` THEN 2451 POP_ASSUM (fn th => ASSUME_TAC 2452 (SUBS [(GSYM o Q.SPECL [`f`,`n`]) LENGTH_GENLIST] th) THEN 2453 ASSUME_TAC th) THEN1 ( 2454 ASM_SIMP_TAC bool_ss [EL_SNOC] 2455 ) THEN 2456 `x = LENGTH (GENLIST f n)` by FULL_SIMP_TAC arith_ss [LENGTH_GENLIST] THEN 2457 ASM_SIMP_TAC bool_ss [EL_LENGTH_SNOC] THEN 2458 REWRITE_TAC [LENGTH_GENLIST]); 2459val _ = export_rewrites ["EL_GENLIST"] 2460 2461val HD_GENLIST = save_thm("HD_GENLIST", 2462 (SIMP_RULE arith_ss [EL] o Q.SPECL [`f`,`SUC n`,`0`]) EL_GENLIST); 2463 2464val HD_GENLIST_COR = Q.store_thm("HD_GENLIST_COR", 2465 `!n f. 0 < n ==> (HD (GENLIST f n) = f 0)`, 2466 Cases THEN REWRITE_TAC [prim_recTheory.LESS_REFL, HD_GENLIST]); 2467 2468val GENLIST_FUN_EQ = store_thm("GENLIST_FUN_EQ", 2469 ``!n f g. (GENLIST f n = GENLIST g n) = (!x. x < n ==> (f x = g x))``, 2470 SIMP_TAC bool_ss [LIST_EQ_REWRITE, LENGTH_GENLIST, EL_GENLIST]); 2471 2472val GENLIST_APPEND = store_thm("GENLIST_APPEND", 2473 ``!f a b. GENLIST f (a + b) = (GENLIST f b) ++ (GENLIST (\t. f (t + b)) a)``, 2474 Induct_on `a` THEN 2475 ASM_SIMP_TAC arith_ss 2476 [GENLIST, APPEND_SNOC, APPEND_NIL, arithmeticTheory.ADD_CLAUSES] 2477); 2478 2479val EVERY_GENLIST = store_thm("EVERY_GENLIST", 2480 ``!n. EVERY P (GENLIST f n) = (!i. i < n ==> P (f i))``, 2481 Induct_on `n` THEN ASM_SIMP_TAC arith_ss [GENLIST, EVERY_SNOC, EVERY_DEF] 2482 THEN metisLib.METIS_TAC [prim_recTheory.LESS_THM]); 2483 2484val EXISTS_GENLIST = store_thm ("EXISTS_GENLIST", 2485 ``!n. EXISTS P (GENLIST f n) = (?i. i < n /\ P (f i))``, 2486 Induct_on `n` THEN RW_TAC arith_ss [GENLIST, EXISTS_SNOC, EXISTS_DEF] 2487 THEN metisLib.METIS_TAC [prim_recTheory.LESS_THM]); 2488 2489val TL_GENLIST = Q.store_thm ("TL_GENLIST", 2490 `!f n. TL (GENLIST f (SUC n)) = GENLIST (f o SUC) n`, 2491 REPEAT STRIP_TAC THEN MATCH_MP_TAC LIST_EQ 2492 THEN SRW_TAC [] [EL_GENLIST, LENGTH_GENLIST, LENGTH_TL] 2493 THEN ONCE_REWRITE_TAC [EL |> CONJUNCT2 |> GSYM] 2494 THEN `SUC x < SUC n` by numLib.DECIDE_TAC 2495 THEN IMP_RES_TAC EL_GENLIST 2496 THEN ASM_SIMP_TAC arith_ss []); 2497 2498val ZIP_GENLIST = store_thm("ZIP_GENLIST", 2499 ``!l f n. (LENGTH l = n) ==> 2500 (ZIP (l,GENLIST f n) = GENLIST (\x. (EL x l,f x)) n)``, 2501 REPEAT STRIP_TAC THEN 2502 `LENGTH (ZIP (l,GENLIST f n)) = LENGTH (GENLIST (\x. (EL x l,f x)) n)` 2503 by ASM_SIMP_TAC arith_ss [LENGTH_GENLIST, LENGTH_ZIP] THEN 2504 ASM_SIMP_TAC arith_ss [LIST_EQ_REWRITE, LENGTH_GENLIST, LENGTH_ZIP, 2505 EL_ZIP, EL_GENLIST]); 2506 2507val GENLIST_CONS = store_thm( 2508 "GENLIST_CONS", 2509 ``GENLIST f (SUC n) = f 0 :: (GENLIST (f o SUC) n)``, 2510 Induct_on `n` THEN SRW_TAC [] [GENLIST, SNOC]); 2511 2512val NULL_GENLIST = Q.store_thm("NULL_GENLIST", 2513 `!n f. NULL (GENLIST f n) = (n = 0)`, 2514 Cases THEN 2515 REWRITE_TAC [numTheory.NOT_SUC, NULL_DEF, CONJUNCT1 GENLIST, GENLIST_CONS]); 2516 2517val GENLIST_AUX_lem = Q.prove( 2518 `!n l1 l2. GENLIST_AUX f n l1 ++ l2 = GENLIST_AUX f n (l1 ++ l2)`, 2519 Induct_on `n` THEN SRW_TAC [] [GENLIST_AUX]); 2520 2521val GENLIST_GENLIST_AUX = Q.store_thm("GENLIST_GENLIST_AUX", 2522 `!n. GENLIST f n = GENLIST_AUX f n []`, 2523 Induct_on `n` 2524 THEN RW_TAC bool_ss 2525 [SNOC_APPEND, APPEND, GENLIST_AUX, GENLIST_AUX_lem, GENLIST]); 2526 2527val GENLIST_NUMERALS = store_thm( 2528 "GENLIST_NUMERALS", 2529 ``(GENLIST f 0 = []) /\ 2530 (GENLIST f (NUMERAL n) = GENLIST_AUX f (NUMERAL n) [])``, 2531 REWRITE_TAC [GENLIST_GENLIST_AUX, GENLIST_AUX]); 2532val _ = export_rewrites ["GENLIST_NUMERALS"] 2533 2534val MEM_GENLIST = Q.store_thm( 2535"MEM_GENLIST", 2536`MEM x (GENLIST f n) <=> ?m. m < n /\ (x = f m)`, 2537SRW_TAC [] [MEM_EL, EL_GENLIST, EQ_IMP_THM] THEN 2538PROVE_TAC [EL_GENLIST] ) 2539 2540val ALL_DISTINCT_SNOC = store_thm ( 2541 "ALL_DISTINCT_SNOC", 2542 ``!x l. ALL_DISTINCT (SNOC x l) = 2543 ~(MEM x l) /\ (ALL_DISTINCT l)``, 2544SRW_TAC [] [SNOC_APPEND, ALL_DISTINCT_APPEND] THEN PROVE_TAC[]); 2545 2546local open prim_recTheory in 2547val ALL_DISTINCT_GENLIST = Q.store_thm( 2548"ALL_DISTINCT_GENLIST", 2549`ALL_DISTINCT (GENLIST f n) <=> 2550 (!m1 m2. m1 < n /\ m2 < n /\ (f m1 = f m2) ==> (m1 = m2))`, 2551Induct_on `n` THEN 2552SRW_TAC [] [GENLIST, ALL_DISTINCT_SNOC, MEM_EL] THEN 2553SRW_TAC [] [EQ_IMP_THM] THEN1 ( 2554 IMP_RES_TAC LESS_SUC_IMP THEN 2555 Cases_on `m1 = n` THEN Cases_on `m2 = n` THEN SRW_TAC [] [] THEN 2556 FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2557 NTAC 2 (FIRST_X_ASSUM (Q.SPEC_THEN `m2` MP_TAC)) THEN 2558 SRW_TAC [] [] ) THEN 2559 NTAC 2 (FIRST_X_ASSUM (Q.SPEC_THEN `m1` MP_TAC)) THEN 2560 SRW_TAC [] [] ) THEN1 ( 2561 Q.MATCH_RENAME_TAC `~(m < n) \/ f n <> EL m (GENLIST f n)` THEN 2562 Cases_on `m < n` THEN SRW_TAC [] [] THEN 2563 FIRST_X_ASSUM (Q.SPECL_THEN [`m`,`n`] MP_TAC) THEN 2564 SRW_TAC [] [LESS_SUC] THEN 2565 METIS_TAC [LESS_REFL] ) THEN 2566METIS_TAC [LESS_SUC] ) 2567end 2568 2569(* ---------------------------------------------------------------------- *) 2570 2571val FOLDL_SNOC = store_thm("FOLDL_SNOC", 2572 (���!(f:'b->'a->'b) e x l. FOLDL f e (SNOC x l) = f (FOLDL f e l) x���), 2573 let val lem = prove( 2574 (���!l (f:'b->'a->'b) e x. FOLDL f e (SNOC x l) = f (FOLDL f e l) x���), 2575 LIST_INDUCT_TAC THEN REWRITE_TAC[SNOC, FOLDL] 2576 THEN REPEAT GEN_TAC THEN ASM_REWRITE_TAC[]) 2577 in 2578 MATCH_ACCEPT_TAC lem 2579 end); 2580 2581local open arithmeticTheory in 2582val SUM_SNOC = store_thm("SUM_SNOC", 2583 (���!x l. SUM (SNOC x l) = (SUM l) + x���), 2584 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[SUM, SNOC, ADD, ADD_0] 2585 THEN GEN_TAC THEN ASM_REWRITE_TAC[ADD_ASSOC]); 2586 2587val SUM_APPEND = store_thm("SUM_APPEND", 2588 (���!l1 l2. SUM (APPEND l1 l2) = SUM l1 + SUM l2���), 2589 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[SUM, APPEND, ADD, ADD_0, ADD_ASSOC]); 2590end 2591 2592val SUM_MAP_FOLDL = Q.store_thm( 2593"SUM_MAP_FOLDL", 2594`!ls. SUM (MAP f ls) = FOLDL (\a e. a + f e) 0 ls`, 2595HO_MATCH_MP_TAC SNOC_INDUCT THEN 2596SRW_TAC [] [FOLDL_SNOC, MAP_SNOC, SUM_SNOC, MAP, SUM, FOLDL]); 2597 2598val SUM_IMAGE_eq_SUM_MAP_SET_TO_LIST = Q.store_thm( 2599"SUM_IMAGE_eq_SUM_MAP_SET_TO_LIST", 2600`FINITE s ==> (SIGMA f s = SUM (MAP f (SET_TO_LIST s)))`, 2601SRW_TAC [] [SUM_IMAGE_DEF] THEN 2602SRW_TAC [] [ITSET_eq_FOLDL_SET_TO_LIST, SUM_MAP_FOLDL] THEN 2603AP_THM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN 2604SRW_TAC [] [FUN_EQ_THM, arithmeticTheory.ADD_COMM]); 2605 2606val SNOC_INDUCT_TAC = INDUCT_THEN SNOC_INDUCT ASSUME_TAC; 2607 2608local open arithmeticTheory prim_recTheory in 2609val EL_REVERSE = store_thm("EL_REVERSE", 2610 ���!n (l:'a list). n < (LENGTH l) ==> 2611 (EL n (REVERSE l) = EL (PRE(LENGTH l - n)) l)���, 2612 INDUCT_TAC THEN SNOC_INDUCT_TAC 2613 THEN ASM_REWRITE_TAC[LENGTH, LENGTH_SNOC, 2614 EL, HD, TL, NOT_LESS_0, LESS_MONO_EQ, SUB_0] THENL[ 2615 REWRITE_TAC[REVERSE_SNOC, PRE, EL_LENGTH_SNOC, HD], 2616 REWRITE_TAC[REVERSE_SNOC, SUB_MONO_EQ, TL] 2617 THEN REPEAT STRIP_TAC THEN RES_THEN SUBST1_TAC 2618 THEN MATCH_MP_TAC (GSYM EL_SNOC) 2619 THEN REWRITE_TAC(PRE_SUB1 :: (map GSYM [SUB_PLUS, ADD1])) 2620 THEN numLib.DECIDE_TAC]); 2621end 2622 2623val REVERSE_GENLIST = Q.store_thm("REVERSE_GENLIST", 2624`REVERSE (GENLIST f n) = GENLIST (\m. f (PRE n - m)) n`, 2625 MATCH_MP_TAC LIST_EQ THEN 2626 SRW_TAC [] [EL_REVERSE] THEN 2627 `PRE (n - x) < n` by numLib.DECIDE_TAC THEN 2628 SRW_TAC [] [EL_GENLIST] THEN 2629 AP_TERM_TAC THEN numLib.DECIDE_TAC) 2630 2631val FOLDL_UNION_BIGUNION = store_thm( 2632"FOLDL_UNION_BIGUNION", 2633``!f ls s. FOLDL (\s x. s UNION f x) s ls = s UNION BIGUNION (IMAGE f (set ls))``, 2634GEN_TAC THEN Induct THEN SRW_TAC[] [FOLDL, UNION_ASSOC]) 2635 2636val FOLDL_UNION_BIGUNION_paired = store_thm( 2637"FOLDL_UNION_BIGUNION_paired", 2638``!f ls s. FOLDL (\s (x,y). s UNION f x y) s ls = s UNION BIGUNION (IMAGE (UNCURRY f) (set ls))``, 2639GEN_TAC THEN Induct THEN1 SRW_TAC[] [FOLDL] THEN 2640Cases THEN SRW_TAC[] [FOLDL, UNION_ASSOC, GSYM pairTheory.LAMBDA_PROD]) 2641 2642val FOLDL_ZIP_SAME = store_thm( 2643"FOLDL_ZIP_SAME", 2644``!ls f e. FOLDL f e (ZIP (ls,ls)) = FOLDL (\x y. f x (y,y)) e ls``, 2645Induct THEN SRW_TAC[] [FOLDL, ZIP]) 2646val _ = export_rewrites["FOLDL_ZIP_SAME"] 2647 2648val MAP_ZIP_SAME = store_thm( 2649"MAP_ZIP_SAME", 2650``!ls f. MAP f (ZIP (ls,ls)) = MAP (\x. f (x,x)) ls``, 2651Induct THEN SRW_TAC [] [MAP, ZIP]) 2652val _ = export_rewrites["MAP_ZIP_SAME"] 2653 2654(* ---------------------------------------------------------------------- 2655 All lists have infinite universes 2656 ---------------------------------------------------------------------- *) 2657 2658val INFINITE_LIST_UNIV = store_thm( 2659 "INFINITE_LIST_UNIV", 2660 ``INFINITE univ(:'a list)``, 2661 REWRITE_TAC [] THEN 2662 SRW_TAC [] [INFINITE_UNIV] THEN 2663 Q.EXISTS_TAC `\l. x::l` THEN SRW_TAC [] [] THEN 2664 Q.EXISTS_TAC `[]` THEN SRW_TAC [] []) 2665val _ = export_rewrites ["INFINITE_LIST_UNIV"] 2666 2667 2668(*---------------------------------------------------------------------------*) 2669(* Tail recursive versions for better memory usage when applied in ML *) 2670(*---------------------------------------------------------------------------*) 2671 2672(* EVAL performance of LEN seems to be worse than of LENGTH *) 2673 2674val LEN_DEF = dDefine 2675 `(LEN [] n = n) /\ 2676 (LEN (h::t) n = LEN t (n+1))`; 2677 2678val REV_DEF = dDefine 2679 `(REV [] acc = acc) /\ 2680 (REV (h::t) acc = REV t (h::acc))`; 2681 2682val LEN_LENGTH_LEM = Q.store_thm 2683("LEN_LENGTH_LEM", 2684 `!L n. LEN L n = LENGTH L + n`, 2685 Induct THEN RW_TAC arith_ss [LEN_DEF, LENGTH]); 2686 2687val REV_REVERSE_LEM = Q.store_thm 2688("REV_REVERSE_LEM", 2689 `!L1 L2. REV L1 L2 = (REVERSE L1) ++ L2`, 2690 Induct THEN RW_TAC arith_ss [REV_DEF, REVERSE_DEF, APPEND] 2691 THEN REWRITE_TAC [GSYM APPEND_ASSOC] 2692 THEN RW_TAC bool_ss [APPEND]); 2693 2694val LENGTH_LEN = Q.store_thm 2695("LENGTH_LEN", 2696 `!L. LENGTH L = LEN L 0`, 2697 RW_TAC arith_ss [LEN_LENGTH_LEM]); 2698 2699val REVERSE_REV = Q.store_thm 2700("REVERSE_REV", 2701 `!L. REVERSE L = REV L []`, 2702 PROVE_TAC [REV_REVERSE_LEM, APPEND_NIL]); 2703 2704val SUM_ACC_DEF = dDefine 2705 `(SUM_ACC [] acc = acc) /\ 2706 (SUM_ACC (h::t) acc = SUM_ACC t (h+acc))` 2707 2708val SUM_ACC_SUM_LEM = store_thm 2709("SUM_ACC_SUM_LEM", 2710 ``!L n. SUM_ACC L n = SUM L + n``, 2711 Induct THEN RW_TAC arith_ss [SUM_ACC_DEF, SUM]); 2712 2713val SUM_SUM_ACC = store_thm 2714("SUM_SUM_ACC", 2715 ``!L. SUM L = SUM_ACC L 0``, 2716 PROVE_TAC [SUM_ACC_SUM_LEM, arithmeticTheory.ADD_0]) 2717 2718(* ---------------------------------------------------------------------- 2719 List "splitting" results 2720 ---------------------------------------------------------------------- *) 2721 2722(* These loop! Use with care *) 2723val EXISTS_LIST = store_thm( 2724 "EXISTS_LIST", 2725 ``(?l. P l) <=> P [] \/ ?h t. P (h::t)``, 2726 METIS_TAC [list_CASES]); 2727 2728val FORALL_LIST = store_thm( 2729 "FORALL_LIST", 2730 ``(!l. P l) <=> P [] /\ !h t. P (h::t)``, 2731 METIS_TAC [list_CASES]); 2732 2733(* now on with the show *) 2734val MEM_SPLIT_APPEND_first = store_thm( 2735 "MEM_SPLIT_APPEND_first", 2736 ``MEM e l <=> ?pfx sfx. (l = pfx ++ [e] ++ sfx) /\ ~MEM e pfx``, 2737 Induct_on `l` THEN SRW_TAC [] [] THEN Cases_on `e = a` THEN 2738 SRW_TAC [] [] THENL[ 2739 MAP_EVERY Q.EXISTS_TAC [`[]`, `l`] THEN SRW_TAC [] [], 2740 SRW_TAC [] [SimpRHS, Once EXISTS_LIST] 2741 ]); 2742 2743val MEM_SPLIT_APPEND_last = store_thm( 2744 "MEM_SPLIT_APPEND_last", 2745 ``MEM e l <=> ?pfx sfx. (l = pfx ++ [e] ++ sfx) /\ ~MEM e sfx``, 2746 Q.ID_SPEC_TAC `l` THEN SNOC_INDUCT_TAC THEN SRW_TAC [] [] THEN 2747 Cases_on `e = x` THEN SRW_TAC [] [] THENL [ 2748 MAP_EVERY Q.EXISTS_TAC [`l`, `[]`] THEN SRW_TAC [] [SNOC_APPEND], 2749 SRW_TAC [] [EQ_IMP_THM] THENL [ 2750 MAP_EVERY Q.EXISTS_TAC [`pfx`, `SNOC x sfx`] THEN 2751 SRW_TAC [] [APPEND_ASSOC, APPEND_SNOC], 2752 Q.SPEC_THEN `sfx` STRIP_ASSUME_TAC SNOC_CASES THEN 2753 SRW_TAC [] [] THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 2754 FULL_SIMP_TAC (srw_ss()) [GSYM SNOC_APPEND] THEN 2755 FULL_SIMP_TAC (srw_ss()) [APPEND_SNOC] THEN SRW_TAC [] [] THEN 2756 METIS_TAC [] 2757 ] 2758 ]); 2759 2760val APPEND_EQ_APPEND = store_thm( 2761 "APPEND_EQ_APPEND", 2762 ``(l1 ++ l2 = m1 ++ m2) <=> 2763 (?l. (l1 = m1 ++ l) /\ (m2 = l ++ l2)) \/ 2764 (?l. (m1 = l1 ++ l) /\ (l2 = l ++ m2))``, 2765 MAP_EVERY Q.ID_SPEC_TAC [`m2`, `m1`, `l2`, `l1`] THEN Induct_on `l1` THEN 2766 SRW_TAC [] [] THEN 2767 Cases_on `m1` THEN SRW_TAC [] [] THEN METIS_TAC []); 2768 2769val APPEND_EQ_CONS = store_thm( 2770 "APPEND_EQ_CONS", 2771 ``(l1 ++ l2 = h::t) <=> 2772 ((l1 = []) /\ (l2 = h::t)) \/ 2773 ?lt. (l1 = h::lt) /\ (t = lt ++ l2)``, 2774 MAP_EVERY Q.ID_SPEC_TAC [`t`, `h`, `l2`, `l1`] THEN Induct_on `l1` THEN 2775 SRW_TAC [] [] THEN METIS_TAC []); 2776 2777(* could just use APPEND_EQ_APPEND and APPEND_EQ_SING, but this gives you 2778 four possibilities 2779 |- (x ++ [e] ++ y = a ++ b) <=> 2780 (?l'. (x = a ++ l') /\ (b = l' ++ [e] ++ y)) \/ 2781 (a = x ++ [e]) /\ (b = y) \/ 2782 (a = x) /\ (b = e::y) \/ 2783 ?l. (a = x ++ [e] ++ l) /\ (y = l ++ b) 2784 Note that the middle two are instances of the outer two with the 2785 existentially quantified l set to [] 2786*) 2787val APPEND_EQ_APPEND_MID = store_thm( 2788 "APPEND_EQ_APPEND_MID", 2789 ``(l1 ++ [e] ++ l2 = m1 ++ m2) <=> 2790 (?l. (m1 = l1 ++ [e] ++ l) /\ (l2 = l ++ m2)) \/ 2791 (?l. (l1 = m1 ++ l) /\ (m2 = l ++ [e] ++ l2))``, 2792 MAP_EVERY Q.ID_SPEC_TAC [`m2`, `m1`, `l2`, `e`, `l1`] THEN Induct THEN 2793 Cases_on `m1` THEN SRW_TAC [] [] THEN METIS_TAC []); 2794 2795(* --------------------------------------------------------------------- *) 2796 2797local 2798 val lupdate_exists = prove( 2799 ``?lupdate. 2800 (!e: 'a n: num. lupdate e n ([]: 'a list) = []: 'a list) /\ 2801 (!e x l. lupdate e 0 (x::l) = e::l) /\ 2802 (!e n x l. lupdate e (SUC n) (x::l) = 2803 CONS x (lupdate e n l))``, 2804 REPEAT STRIP_TAC 2805 THEN STRIP_ASSUME_TAC 2806 (Q.ISPECL 2807 [`(\x1 x2. []): 'a -> num -> 'a list`, 2808 `\(x: 'a) (l: 'a list) (r: 'a -> num -> 'a list) (e: 'a) 2809 (n: num). 2810 if n = 0 then 2811 e::l 2812 else 2813 (CONS x (r e (PRE n)):'a list)`] list_Axiom) 2814 THEN Q.EXISTS_TAC `\x1 x2 x3. fn x3 x1 x2` 2815 THEN ASM_SIMP_TAC arith_ss []) 2816in 2817 val LUPDATE_def = 2818 Definition.new_specification 2819 ("LUPDATE_def", ["LUPDATE"], lupdate_exists) 2820end; 2821 2822val LUPDATE_NIL = store_thm("LUPDATE_NIL[simp]", 2823 ``!xs n x. (LUPDATE x n xs = []) <=> (xs = [])``, 2824 Cases \\ Cases_on `n` \\ FULL_SIMP_TAC (srw_ss()) [LUPDATE_def]); 2825 2826val LUPDATE_SEM = store_thm ("LUPDATE_SEM", 2827 ``(!e:'a n l. LENGTH (LUPDATE e n l) = LENGTH l) /\ 2828 (!e:'a n l p. 2829 p < LENGTH l ==> 2830 (EL p (LUPDATE e n l) = if p = n then e else EL p l))``, 2831 CONJ_TAC 2832 THEN Induct_on `n` 2833 THEN Cases_on `l` 2834 THEN ASM_SIMP_TAC arith_ss [LUPDATE_def, LENGTH] 2835 THEN Cases_on `p` 2836 THEN ASM_SIMP_TAC arith_ss [EL, HD, TL]); 2837 2838val EL_LUPDATE = store_thm("EL_LUPDATE", 2839 ``!ys (x:'a) i k. 2840 EL i (LUPDATE x k ys) = 2841 if (i = k) /\ k < LENGTH ys then x else EL i ys``, 2842 Induct_on `ys` THEN Cases_on `k` THEN REPEAT STRIP_TAC 2843 THEN ASM_SIMP_TAC arith_ss [LUPDATE_def, LENGTH] 2844 THEN Cases_on `i` 2845 THEN FULL_SIMP_TAC arith_ss [LUPDATE_def, LENGTH, EL, HD, TL]); 2846 2847val LENGTH_LUPDATE = store_thm("LENGTH_LUPDATE", 2848 ``!(x:'a) n ys. LENGTH (LUPDATE x n ys) = LENGTH ys``, 2849 SIMP_TAC bool_ss [LUPDATE_SEM]); 2850val _ = export_rewrites ["LENGTH_LUPDATE"] 2851 2852val LUPDATE_LENGTH = store_thm("LUPDATE_LENGTH", 2853 ``!xs x (y:'a) ys. LUPDATE x (LENGTH xs) (xs ++ y::ys) = xs ++ x::ys``, 2854 Induct THEN FULL_SIMP_TAC bool_ss [LENGTH, APPEND, LUPDATE_def, 2855 NOT_SUC, PRE, INV_SUC_EQ]); 2856 2857val LUPDATE_SNOC = store_thm("LUPDATE_SNOC", 2858 ``!ys k x (y:'a). 2859 LUPDATE x k (SNOC y ys) = 2860 if k = LENGTH ys then SNOC x ys else SNOC y (LUPDATE x k ys)``, 2861 Induct THEN Cases_on `k` THEN Cases_on `n = LENGTH ys` 2862 THEN FULL_SIMP_TAC bool_ss [SNOC, LUPDATE_def, LENGTH, NOT_SUC, 2863 PRE, INV_SUC_EQ]); 2864 2865val MEM_LUPDATE_E = store_thm("MEM_LUPDATE_E", 2866 ``!l x y i. MEM x (LUPDATE y i l) ==> (x = y) \/ MEM x l``, 2867 Induct THEN SRW_TAC [] [LUPDATE_def] THEN 2868 Cases_on`i`THEN FULL_SIMP_TAC(srw_ss())[LUPDATE_def] THEN 2869 PROVE_TAC[]) 2870 2871val MEM_LUPDATE = store_thm( 2872 "MEM_LUPDATE", 2873 ``!l x y i. MEM x (LUPDATE y i l) <=> 2874 i < LENGTH l /\ (x = y) \/ 2875 ?j. j < LENGTH l /\ i <> j /\ (EL j l = x)``, 2876 Induct THEN SRW_TAC [] [LUPDATE_def] THEN 2877 Cases_on `i` THEN SRW_TAC [] [LUPDATE_def] THENL [ 2878 SRW_TAC [] [Once arithmeticTheory.EXISTS_NUM] THEN 2879 METIS_TAC [MEM_EL], 2880 EQ_TAC THEN SRW_TAC [] [] THENL [ 2881 DISJ2_TAC THEN Q.EXISTS_TAC `0` THEN SRW_TAC [] [], 2882 DISJ2_TAC THEN Q.EXISTS_TAC `SUC j` THEN SRW_TAC [] [], 2883 Cases_on `j` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2884 METIS_TAC[] 2885 ] 2886 ]); 2887 2888val LUPDATE_compute = save_thm("LUPDATE_compute", 2889 numLib.SUC_RULE LUPDATE_def) 2890 2891val LUPDATE_MAP = store_thm("LUPDATE_MAP", 2892``!x n l f. MAP f (LUPDATE x n l) = LUPDATE (f x) n (MAP f l)``, 2893 Induct_on `l` THEN SRW_TAC [] [LUPDATE_def] THEN Cases_on `n` THEN 2894 FULL_SIMP_TAC (srw_ss()) [LUPDATE_def]); 2895 2896val EVERYi_def = Define` 2897 (EVERYi P [] = T) /\ 2898 (EVERYi P (h::t) = P 0 h /\ EVERYi (P o SUC) t) 2899` 2900 2901val splitAtPki_def = Define` 2902 (splitAtPki P k [] = k [] []) /\ 2903 (splitAtPki P k (h::t) = 2904 if P 0 h then k [] (h::t) 2905 else splitAtPki (P o SUC) (\p s. k (h::p) s) t) 2906` 2907 2908val splitAtPki_APPEND = store_thm( 2909 "splitAtPki_APPEND", 2910 ``!l1 l2 P k. 2911 EVERYi (\i. $~ o P i) l1 /\ (0 < LENGTH l2 ==> P (LENGTH l1) (HD l2)) ==> 2912 (splitAtPki P k (l1 ++ l2) = k l1 l2)``, 2913 Induct THEN SRW_TAC [] [EVERYi_def, splitAtPki_def] THEN1 2914 (Cases_on `l2` THEN FULL_SIMP_TAC (srw_ss())[splitAtPki_def]) THEN 2915 FULL_SIMP_TAC (srw_ss()) [o_DEF]); 2916 2917val splitAtPki_EQN = store_thm( 2918 "splitAtPki_EQN", 2919 ``splitAtPki P k l = 2920 case OLEAST i. i < LENGTH l /\ P i (EL i l) of 2921 NONE => k l [] 2922 | SOME i => k (TAKE i l) (DROP i l)``, 2923 MAP_EVERY Q.ID_SPEC_TAC [`P`, `k`, `l`] THEN Induct THEN 2924 ASM_SIMP_TAC (srw_ss()) [splitAtPki_def] THEN POP_ASSUM (K ALL_TAC) THEN 2925 MAP_EVERY Q.X_GEN_TAC [`h`, `k`, `P`] THEN Cases_on `P 0 h` THEN1 2926 (ASM_SIMP_TAC (srw_ss()) [] THEN 2927 `(OLEAST i. i < SUC (LENGTH l) /\ P i (EL i (h::l))) = SOME 0` 2928 suffices_by SRW_TAC [] [] THEN 2929 ASM_SIMP_TAC (srw_ss()) [whileTheory.OLEAST_EQ_SOME]) THEN 2930 SRW_TAC [] [] THEN 2931 Cases_on ���OLEAST i. i < LENGTH l /\ P (SUC i) (EL i l)��� >> fs[] 2932 >- (`(OLEAST i. i < SUC (LENGTH l) /\ P i (EL i (h::l))) = NONE` 2933 suffices_by (DISCH_THEN SUBST1_TAC THEN SRW_TAC[][]) THEN 2934 SRW_TAC[][] >> Q.RENAME_TAC [���EL i (h::t)���] >> Cases_on ���i��� >> 2935 SRW_TAC[][]) THEN 2936 Q.RENAME_TAC [���h::TAKE i t���] >> 2937 ���(OLEAST i. i < SUC (LENGTH t) /\ P i (EL i (h::t))) = SOME (SUC i)��� 2938 suffices_by SRW_TAC [] [] THEN 2939 fs[whileTheory.OLEAST_EQ_SOME] >> Cases >> SRW_TAC[][]); 2940 2941val TAKE_LENGTH_TOO_LONG = store_thm( 2942 "TAKE_LENGTH_TOO_LONG", 2943 ``!l n. LENGTH l <= n ==> (TAKE n l = l)``, 2944 Induct THEN SRW_TAC [numSimps.ARITH_ss] []); 2945 2946val DROP_LENGTH_TOO_LONG = store_thm( 2947 "DROP_LENGTH_TOO_LONG", 2948 ``!l n. LENGTH l <= n ==> (DROP n l = [])``, 2949 Induct THEN SRW_TAC [numSimps.ARITH_ss] []); 2950 2951val TAKE_splitAtPki = store_thm( 2952 "TAKE_splitAtPki", 2953 ``TAKE n l = splitAtPki (K o (=) n) K l``, 2954 SRW_TAC [] [splitAtPki_EQN] THEN 2955 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO THEN 2956 SRW_TAC[numSimps.ARITH_ss] [TAKE_LENGTH_TOO_LONG]) 2957 2958val DROP_splitAtPki = store_thm( 2959 "DROP_splitAtPki", 2960 ``DROP n l = splitAtPki (K o (=) n) (K I) l``, 2961 SRW_TAC [] [splitAtPki_EQN] THEN 2962 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO THEN 2963 SRW_TAC[numSimps.ARITH_ss] [DROP_LENGTH_TOO_LONG]); 2964 2965(* ---------------------------------------------------------------------- 2966 List monad related stuff 2967 ---------------------------------------------------------------------- *) 2968 2969(* the bind function is flatMap with arguments in a different order *) 2970val LIST_BIND_def = Define` 2971 LIST_BIND l f = FLAT (MAP f l) 2972` 2973 2974val LIST_BIND_THM = store_thm( 2975 "LIST_BIND_THM", 2976 ``(LIST_BIND [] f = []) /\ 2977 (LIST_BIND (h::t) f = f h ++ LIST_BIND t f)``, 2978 SIMP_TAC (srw_ss()) [LIST_BIND_def]); 2979val _ = export_rewrites ["LIST_BIND_THM"] 2980 2981val LIST_IGNORE_BIND_def = Define` 2982 LIST_IGNORE_BIND m1 m2 = LIST_BIND m1 (K m2) 2983`; 2984 2985val LIST_BIND_ID = store_thm( 2986 "LIST_BIND_ID", 2987 ``(LIST_BIND l (\x.x) = FLAT l) /\ 2988 (LIST_BIND l I = FLAT l)``, 2989 SIMP_TAC (srw_ss()) [LIST_BIND_def]); 2990 2991val LIST_BIND_APPEND = store_thm( 2992 "LIST_BIND_APPEND", 2993 ``LIST_BIND (l1 ++ l2) f = LIST_BIND l1 f ++ LIST_BIND l2 f``, 2994 Induct_on `l1` THEN ASM_SIMP_TAC (srw_ss()) [APPEND_ASSOC]); 2995 2996val LIST_BIND_MAP = store_thm( 2997 "LIST_BIND_MAP", 2998 ``LIST_BIND (MAP f l) g = LIST_BIND l (g o f)``, 2999 Induct_on `l` THEN ASM_SIMP_TAC (srw_ss()) []); 3000 3001val MAP_LIST_BIND = store_thm( 3002 "MAP_LIST_BIND", 3003 ``MAP f (LIST_BIND l g) = LIST_BIND l (MAP f o g)``, 3004 Induct_on `l` THEN ASM_SIMP_TAC (srw_ss()) [MAP_APPEND]); 3005 3006(* monad associativity *) 3007val LIST_BIND_LIST_BIND = store_thm( 3008 "LIST_BIND_LIST_BIND", 3009 ``LIST_BIND (LIST_BIND l g) f = LIST_BIND l (combin$C LIST_BIND f o g)``, 3010 Induct_on `l` THEN ASM_SIMP_TAC (srw_ss()) [LIST_BIND_APPEND]); 3011 3012val LIST_GUARD_def = Define���LIST_GUARD b = if b then [()] else []���; 3013 3014(* the "return" or "pure" constant for lists isn't an existing one, unlike 3015 the situation with 'a option, where SOME fits the bill. *) 3016val _ = overload_on("SINGL", ``\x:'a. [x]``) 3017val _ = overload_on("", ``\x:'a. [x]``) 3018 3019val SINGL_LIST_APPLY_L = store_thm( 3020 "SINGL_LIST_APPLY_L", 3021 ``LIST_BIND (SINGL x) f = f x``, 3022 SIMP_TAC (srw_ss()) []); 3023val _ = export_rewrites ["SINGL_LIST_APPLY_L"] 3024 3025val SINGL_LIST_APPLY_R = store_thm( 3026 "SINGL_LIST_APPLY_R", 3027 ``LIST_BIND l SINGL = l``, 3028 Induct_on `l` THEN ASM_SIMP_TAC (srw_ss()) [LIST_BIND_def]); 3029 3030(* shows that lists are what Haskell would call Applicative *) 3031(* in 'a option, the apply applies a function to an argument if both are 3032 SOME, and otherwise returns NONE. In lists, there is a cross-product 3033 created - this makes sense when you think of the list monad as being 3034 the non-determinism thing: you'd want every possible combination of 3035 the possibilities in fs and xs *) 3036val LIST_APPLY_def = Define` 3037 LIST_APPLY fs xs = LIST_BIND fs (combin$C MAP xs) 3038` 3039 3040(* pick up the <*> syntax *) 3041val _ = overload_on("APPLICATIVE_FAPPLY", ``LIST_APPLY``) 3042 3043(* derives the lift2 function to boot *) 3044val LIST_LIFT2_def = Define` 3045 LIST_LIFT2 f xs ys = LIST_APPLY (MAP f xs) ys 3046` 3047(* e.g., 3048 > EVAL ``LIST_LIFT2 (+) [1;3;4] [10;5]`` 3049 |- ... = [11;6;13;8;14;9] 3050 i.e., the sums of all possible pairs 3051*) 3052 3053 3054(* proofs of the relevant "laws" *) 3055val SINGL_APPLY_MAP = store_thm( 3056 "SINGL_APPLY_MAP", 3057 ``LIST_APPLY (SINGL f) l = MAP f l``, 3058 SIMP_TAC (srw_ss()) [LIST_APPLY_def, LIST_BIND_def]); 3059 3060val SINGL_SINGL_APPLY = store_thm( 3061 "SINGL_SINGL_APPLY", 3062 ``LIST_APPLY (SINGL f) (SINGL x) = SINGL (f x)``, 3063 SIMP_TAC (srw_ss()) [LIST_APPLY_def, LIST_BIND_def]); 3064val _ = export_rewrites ["SINGL_SINGL_APPLY"] 3065 3066val SINGL_APPLY_PERMUTE = store_thm( 3067 "SINGL_APPLY_PERMUTE", 3068 ``LIST_APPLY fs (SINGL x) = LIST_APPLY (SINGL (\f. f x)) fs``, 3069 SIMP_TAC (srw_ss()) [LIST_APPLY_def, LIST_BIND_def] THEN 3070 Induct_on `fs` THEN ASM_SIMP_TAC (srw_ss()) []); 3071 3072val MAP_FLAT = store_thm( 3073 "MAP_FLAT", 3074 ``MAP f (FLAT l) = FLAT (MAP (MAP f) l)``, 3075 Induct_on `l` THEN ASM_SIMP_TAC (srw_ss()) [MAP_APPEND]) 3076 3077val LIST_APPLY_o = store_thm( 3078 "LIST_APPLY_o", 3079 ``LIST_APPLY (LIST_APPLY (LIST_APPLY (SINGL (o)) fs) gs) xs = 3080 LIST_APPLY fs (LIST_APPLY gs xs)``, 3081 ASM_SIMP_TAC (srw_ss()) [LIST_APPLY_def] THEN 3082 Induct_on `fs` THEN 3083 ASM_SIMP_TAC (srw_ss()) [LIST_BIND_APPEND, MAP_LIST_BIND, 3084 APPEND_11] THEN 3085 SIMP_TAC (srw_ss()) [o_DEF, MAP_MAP_o, LIST_BIND_MAP]); 3086 3087(* ---------------------------------------------------------------------- 3088 Various lexicographic orderings on lists 3089 ---------------------------------------------------------------------- *) 3090 3091val SHORTLEX_def = Define��� 3092 (SHORTLEX R [] l2 <=> l2 <> []) /\ 3093 (SHORTLEX R (h1::t1) l2 <=> 3094 case l2 of 3095 [] => F 3096 | h2::t2 => if LENGTH t1 < LENGTH t2 then T 3097 else if LENGTH t1 = LENGTH t2 then 3098 if R h1 h2 then T 3099 else if h1 = h2 then SHORTLEX R t1 t2 3100 else F 3101 else F) 3102���; 3103 3104fun pmap f (a, b) = (f a, f b) 3105val def' = uncurry CONJ (pmap SPEC_ALL (CONJ_PAIR SHORTLEX_def)) 3106val SHORTLEX_THM = save_thm( 3107 "SHORTLEX_THM[simp]", 3108 CONJ (def' |> Q.INST [`l2` |-> `[]`] 3109 |> SIMP_RULE (srw_ss()) []) 3110 (def' |> Q.INST [`l2` |-> `h2::t2`] 3111 |> SIMP_RULE (srw_ss()) [])) 3112 3113val SHORTLEX_MONO = store_thm( 3114 "SHORTLEX_MONO[mono]", 3115 ``(!x y. R1 x y ==> R2 x y) ==> SHORTLEX R1 x y ==> SHORTLEX R2 x y``, 3116 STRIP_TAC THEN Q.ID_SPEC_TAC`y` THEN Induct_on`x` THEN Cases_on`y` THEN 3117 SRW_TAC[][SHORTLEX_THM] THEN PROVE_TAC[]); 3118 3119val SHORTLEX_NIL2 = store_thm( 3120 "SHORTLEX_NIL2[simp]", 3121 ``~SHORTLEX R l []``, 3122 Cases_on `l` THEN SIMP_TAC (srw_ss()) [SHORTLEX_def]); 3123 3124val SHORTLEX_transitive = store_thm( 3125 "SHORTLEX_transitive", 3126 ``transitive R ==> transitive (SHORTLEX R)``, 3127 SIMP_TAC(srw_ss()) [transitive_def] THEN STRIP_TAC THEN Induct THEN 3128 SIMP_TAC (srw_ss()) [SHORTLEX_def] THEN 3129 MAP_EVERY Q.X_GEN_TAC [`h`, `y`, `z`] THEN Cases_on `y` THEN 3130 SIMP_TAC (srw_ss()) [] THEN Cases_on `z` THEN 3131 SIMP_TAC (srw_ss()) [] THEN 3132 METIS_TAC[arithmeticTheory.LESS_TRANS]); 3133 3134val LENGTH_LT_SHORTLEX = Q.store_thm( 3135 "LENGTH_LT_SHORTLEX", 3136 ���!l1 l2. LENGTH l1 < LENGTH l2 ==> SHORTLEX R l1 l2���, 3137 Induct >> simp[SHORTLEX_def] >> rpt gen_tac >> Cases_on ���l2��� >> simp[]); 3138 3139val SHORTLEX_LENGTH_LE = Q.store_thm( 3140 "SHORTLEX_LENGTH_LE", 3141 ���!l1 l2. SHORTLEX R l1 l2 ==> LENGTH l1 <= LENGTH l2���, 3142 Induct >> simp[SHORTLEX_def] >> rpt gen_tac >> Cases_on ���l2��� >> simp[] >> 3143 rw[] >> simp[]); 3144 3145val SHORTLEX_total = store_thm( 3146 "SHORTLEX_total", 3147 ``total (RC R) ==> total (RC (SHORTLEX R))``, 3148 SIMP_TAC (srw_ss()) [total_def, RC_DEF] THEN STRIP_TAC THEN Induct THEN 3149 SIMP_TAC (srw_ss()) [SHORTLEX_def] THEN MAP_EVERY Q.X_GEN_TAC [`h`, `y`] THEN 3150 Cases_on `y` THEN SIMP_TAC (srw_ss()) [] THEN 3151 Q.RENAME_TAC [���LENGTH l1 < LENGTH l2���, ���SHORTLEX R l1 l2���, ���R h1 h2���] >> 3152 MAP_EVERY Cases_on [���LENGTH l1 < LENGTH l2���, ���h1 = h2���, ���l1 = l2���] >> 3153 simp[] >> metis_tac[arithmeticTheory.LESS_LESS_CASES]); 3154 3155val WF_SHORTLEX_same_lengths = Q.store_thm( 3156 "WF_SHORTLEX_same_lengths", 3157 ���WF R ==> 3158 !l s. (!d. d IN s ==> (LENGTH d = l)) /\ (?a. a IN s) ==> 3159 ?b. b IN s /\ !c. SHORTLEX R c b ==> c NOTIN s���, 3160 strip_tac >> ho_match_mp_tac (TypeBase.induction_of ���:num���) >> 3161 simp[] >> rw[] >- (Q.EXISTS_TAC ���[]��� >> simp[] >> metis_tac[]) >> 3162 Q.RENAME_TAC [���LENGTH _ = SUC N���] >> 3163 ���[] NOTIN s��� by (strip_tac >> ���LENGTH [] = SUC N��� by metis_tac[] >> fs[]) >> 3164 Q.ABBREV_TAC ���hds = IMAGE HD s��� >> 3165 ���?ah. hds ah��� by 3166 (���?ah. ah IN hds��� suffices_by simp[IN_DEF] >> 3167 simp[Abbr���hds���] >> metis_tac[]) >> 3168 ���?m. hds m /\ !n. R n m ==> n NOTIN hds��� 3169 by (simp[IN_DEF] >> metis_tac[relationTheory.WF_DEF]) >> 3170 Q.ABBREV_TAC ���ms = { a | a IN s /\ (HD a = m) }��� >> 3171 ���?b. b IN ms /\ !c. SHORTLEX R c b ==> c NOTIN ms��� suffices_by 3172 (strip_tac >> Q.EXISTS_TAC ���b��� >> 3173 ���b IN s��� by fs[Abbr���ms���] >> simp[] >> rpt strip_tac >> 3174 ���c NOTIN ms��� by metis_tac[] >> 3175 ���HD c <> m��� 3176 by (pop_assum mp_tac >> simp_tac (srw_ss()) [Abbr���ms���] >> simp[]) >> 3177 ���(LENGTH c = SUC N) /\ (LENGTH b = SUC N)��� by simp[] >> 3178 ���?ch ct. c = ch :: ct��� by (Cases_on ���c��� >> fs[]) >> 3179 ���?bh bt. b = bh :: bt��� by (Cases_on ���b��� >> fs[]) >> 3180 fs[Abbr���ms���] 3181 >- (���ch IN hds��� by (simp[Abbr���hds���] >> metis_tac[HD]) >> 3182 metis_tac[]) >> 3183 metis_tac[]) >> 3184 CONV_TAC (HO_REWR_CONV EXISTS_LIST) >> DISJ2_TAC >> 3185 Q.EXISTS_TAC ���m��� >> 3186 ONCE_REWRITE_TAC [tautLib.TAUT ���(p ==> q) <=> (~q ==> ~p)���] >> 3187 simp[] >> simp[Once FORALL_LIST] >> 3188 Q.ABBREV_TAC ���mts = { t | m::t IN s }��� >> 3189 ���!d. d IN mts ==> (LENGTH d = N)��� 3190 by (simp[Abbr���mts���] >> rw[] >> first_x_assum drule >> simp[]) >> 3191 ���?a0. a0 IN mts��� 3192 by (simp[Abbr���mts���] >> 3193 ���m IN hds��� by simp[IN_DEF] >> pop_assum mp_tac >> 3194 simp[Abbr���hds���] >> fs[] >> 3195 Q.RENAME_TAC [���R _ m���, ���m = HD e���, ���e IN s���] >> Cases_on ���e��� >> 3196 fs[] >> metis_tac[]) >> 3197 ���?t. t IN mts /\ !u. SHORTLEX R u t ==> u NOTIN mts��� by metis_tac[] >> 3198 Q.EXISTS_TAC ���t��� >> rw[] 3199 >- fs[Abbr���mts���, Abbr���ms���] 3200 >- fs[Abbr���mts���, Abbr���ms���] 3201 >- (fs[Abbr���mts���, Abbr���ms���] >> rw[]) >> 3202 fs[Abbr���mts���, Abbr���ms���] >> rw[] >> metis_tac[IN_DEF]); 3203 3204val WF_SHORTLEX = Q.store_thm( 3205 "WF_SHORTLEX[simp]", 3206 ���WF R ==> WF (SHORTLEX R)���, 3207 simp[relationTheory.WF_DEF] >> rpt strip_tac >> 3208 Q.ABBREV_TAC ���minlen = (LEAST) (IMAGE LENGTH B)��� >> 3209 ���?a. B a /\ (LENGTH a = minlen) /\ !b. B b ==> LENGTH a <= LENGTH b��� 3210 by (simp[Abbr`minlen`] >> numLib.LEAST_ELIM_TAC >> 3211 simp[IMAGE_applied] >> simp[IN_DEF] >> 3212 metis_tac[arithmeticTheory.NOT_LESS]) >> 3213 markerLib.RM_ABBREV_TAC "minlen" >> rw[] >> 3214 Q.ABBREV_TAC `as = { l | B l /\ (LENGTH l = LENGTH a)}` >> 3215 ���!d. d IN as ==> (LENGTH d = LENGTH a)��� by simp[Abbr���as���] >> 3216 ���a IN as��� by simp[Abbr���as���] >> 3217 ���?a0. a0 IN as /\ !c. SHORTLEX R c a0 ==> c NOTIN as��� 3218 by metis_tac[WF_SHORTLEX_same_lengths, relationTheory.WF_DEF] >> 3219 Q.EXISTS_TAC ���a0��� >> conj_tac 3220 >- fs[Abbr���as���] >> 3221 Q.X_GEN_TAC ���bb��� >> rpt strip_tac >> 3222 ���bb NOTIN as��� by simp[] >> 3223 ���LENGTH bb <> LENGTH a��� by (fs[Abbr���as���] >> fs[]) >> 3224 ���LENGTH a < LENGTH bb��� by metis_tac[arithmeticTheory.LESS_OR_EQ] >> 3225 ���LENGTH bb <= LENGTH a0��� by metis_tac[SHORTLEX_LENGTH_LE] >> 3226 ���LENGTH a0 = LENGTH a��� by metis_tac[] >> 3227 full_simp_tac (srw_ss() ++ numSimps.ARITH_ss) []); 3228 3229val LLEX_def = Define` 3230 (LLEX R [] l2 <=> l2 <> []) /\ 3231 (LLEX R (h1::t1) l2 <=> 3232 case l2 of 3233 [] => F 3234 | h2::t2 => if R h1 h2 then T 3235 else if h1 = h2 then LLEX R t1 t2 3236 else F) 3237`; 3238 3239fun pmap f (a, b) = (f a, f b) 3240val def' = uncurry CONJ (pmap SPEC_ALL (CONJ_PAIR LLEX_def)) 3241val LLEX_THM = save_thm( 3242 "LLEX_THM[simp]", 3243 CONJ (def' |> Q.INST [`l2` |-> `[]`] 3244 |> SIMP_RULE (srw_ss()) []) 3245 (def' |> Q.INST [`l2` |-> `h2::t2`] 3246 |> SIMP_RULE (srw_ss()) [])) 3247 3248val LLEX_MONO = store_thm("LLEX_MONO[mono]", 3249 ``(!x y. R1 x y ==> R2 x y) ==> LLEX R1 x y ==> LLEX R2 x y``, 3250 STRIP_TAC THEN 3251 Q.ID_SPEC_TAC`y` THEN 3252 Induct_on`x` THEN 3253 Cases_on`y` THEN 3254 SRW_TAC[][LLEX_THM] THEN 3255 PROVE_TAC[]) 3256 3257val LLEX_CONG = store_thm 3258("LLEX_CONG[defncong]", 3259 ``!R l1 l2 R' l1' l2'. 3260 (l1 = l1') /\ (l2 = l2') /\ 3261 (!a b. MEM a l1' /\ MEM b l2' ==> (R a b = R' a b)) 3262 ==> 3263 (LLEX R l1 l2 = LLEX R' l1' l2')``, 3264 GEN_TAC THEN Induct 3265 THENL [ALL_TAC, GEN_TAC] 3266 THEN Induct 3267 THEN SRW_TAC [] [] 3268 THEN SRW_TAC [] [LLEX_THM] 3269 THEN METIS_TAC[MEM]); 3270 3271val LLEX_NIL2 = store_thm( 3272 "LLEX_NIL2[simp]", 3273 ``~LLEX R l []``, 3274 Cases_on `l` THEN SIMP_TAC (srw_ss()) [LLEX_def]); 3275 3276val LLEX_transitive = store_thm( 3277 "LLEX_transitive", 3278 ``transitive R ==> transitive (LLEX R)``, 3279 SIMP_TAC(srw_ss()) [transitive_def] THEN STRIP_TAC THEN Induct THEN 3280 SIMP_TAC (srw_ss()) [LLEX_def] THEN 3281 MAP_EVERY Q.X_GEN_TAC [`h`, `y`, `z`] THEN Cases_on `y` THEN 3282 SIMP_TAC (srw_ss()) [] THEN Cases_on `z` THEN 3283 SIMP_TAC (srw_ss()) [] THEN METIS_TAC[]); 3284 3285val LLEX_total = store_thm( 3286 "LLEX_total", 3287 ``total (RC R) ==> total (RC (LLEX R))``, 3288 SIMP_TAC (srw_ss()) [total_def, RC_DEF] THEN STRIP_TAC THEN Induct THEN 3289 SIMP_TAC (srw_ss()) [LLEX_def] THEN MAP_EVERY Q.X_GEN_TAC [`h`, `y`] THEN 3290 Cases_on `y` THEN SIMP_TAC (srw_ss()) [] THEN METIS_TAC[]); 3291 3292val LLEX_not_WF = store_thm( 3293 "LLEX_not_WF", 3294 ``(?a b. R a b) ==> ~WF (LLEX R)``, 3295 STRIP_TAC THEN SIMP_TAC (srw_ss()) [WF_DEF] THEN 3296 Q.EXISTS_TAC `\s. ?n. s = GENLIST (K a) n ++ [b]` THEN CONJ_TAC 3297 THEN1 (Q.EXISTS_TAC `[b]` THEN SIMP_TAC (srw_ss()) [] THEN 3298 Q.EXISTS_TAC `0` THEN SIMP_TAC (srw_ss()) []) THEN 3299 REWRITE_TAC [GSYM IMP_DISJ_THM] THEN 3300 SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [SKOLEM_THM] THEN 3301 Q.EXISTS_TAC `SUC` THEN Induct_on `n` THEN 3302 ONCE_REWRITE_TAC [GENLIST_CONS] THEN 3303 ASM_SIMP_TAC (srw_ss()) [LLEX_def]); 3304 3305val LLEX_EL_THM = store_thm("LLEX_EL_THM", 3306 ``!R l1 l2. LLEX R l1 l2 <=> 3307 ?n. n <= LENGTH l1 /\ n < LENGTH l2 /\ 3308 (TAKE n l1 = TAKE n l2) /\ 3309 (n < LENGTH l1 ==> R (EL n l1) (EL n l2))``, 3310 GEN_TAC THEN Induct THEN Cases_on`l2` THEN SRW_TAC[][] THEN 3311 SRW_TAC[][EQ_IMP_THM] THEN1 ( 3312 Q.EXISTS_TAC`0` THEN SRW_TAC[][] ) 3313 THEN1 ( 3314 Q.EXISTS_TAC`SUC n` THEN SRW_TAC[][] ) THEN 3315 Cases_on`n` THEN FULL_SIMP_TAC(srw_ss())[] THEN 3316 METIS_TAC[]) 3317 3318(*---------------------------------------------------------------------------*) 3319(* Various lemmas from the CakeML project https://cakeml.org *) 3320(*---------------------------------------------------------------------------*) 3321 3322(* nub *) 3323 3324val nub_def = Define ` 3325 (nub [] = []) /\ 3326 (nub (x::l) = if MEM x l then nub l else x :: nub l)`; 3327 3328val nub_set = Q.store_thm ("nub_set[simp]", 3329 `!l. set (nub l) = set l`, 3330 Induct 3331 >> rw [nub_def, EXTENSION] 3332 >> metis_tac []); 3333 3334val all_distinct_nub = Q.store_thm ("all_distinct_nub", 3335 `!l. ALL_DISTINCT (nub l)`, 3336 Induct 3337 >> rw [nub_def] 3338 >> metis_tac [nub_set]); 3339 3340val filter_helper = Q.prove ( 3341 `!x l1 l2. 3342 ~MEM x l2 ==> (MEM x (FILTER (\x. x NOTIN set l2) l1) = MEM x l1)`, 3343 Induct_on `l1` 3344 >> rw [] 3345 >> metis_tac []); 3346 3347val nub_append = Q.store_thm ("nub_append", 3348 `!l1 l2. nub (l1++l2) = nub (FILTER (\x. ~MEM x l2) l1) ++ nub l2`, 3349 Induct_on `l1` 3350 >> rw [nub_def] 3351 >> fs [] 3352 >> BasicProvers.FULL_CASE_TAC 3353 >> rw [] 3354 >> metis_tac [filter_helper]); 3355 3356val list_to_set_diff = Q.store_thm ("list_to_set_diff", 3357 `!l1 l2. set l2 DIFF set l1 = set (FILTER (\x. x NOTIN set l1) l2)`, 3358 Induct_on `l2` >> rw []); 3359 3360val card_eqn_help = Q.prove ( 3361 `!l1 l2. CARD (set l2) - CARD (set l1 INTER set l2) = 3362 CARD (set (FILTER (\x. x NOTIN set l1) l2))`, 3363 rw [Once INTER_COMM] 3364 >> SIMP_TAC bool_ss [GSYM CARD_DIFF, FINITE_LIST_TO_SET] 3365 >> metis_tac [list_to_set_diff]); 3366 3367val length_nub_append = Q.store_thm ("length_nub_append", 3368 `!l1 l2. LENGTH (nub (l1 ++ l2)) = 3369 LENGTH (nub l1) + LENGTH (nub (FILTER (\x. ~MEM x l1) l2))`, 3370 rw [GSYM ALL_DISTINCT_CARD_LIST_TO_SET, all_distinct_nub] 3371 >> fs [FINITE_LIST_TO_SET, CARD_UNION_EQN] 3372 >> ASSUME_TAC (Q.SPECL [`l1`, `l2`] card_eqn_help) 3373 >> `CARD (set l1 INTER set l2) <= CARD (set l2)` 3374 by metis_tac [CARD_INTER_LESS_EQ, FINITE_LIST_TO_SET, INTER_COMM] 3375 >> RW_TAC arith_ss []); 3376 3377val ALL_DISTINCT_DROP = Q.store_thm("ALL_DISTINCT_DROP", 3378 `!ls n. ALL_DISTINCT ls ==> ALL_DISTINCT (DROP n ls)`, 3379 Induct >> SIMP_TAC (srw_ss()) [] >> rw [DROP_def]) 3380 3381val EXISTS_LIST_EQ_MAP = Q.store_thm("EXISTS_LIST_EQ_MAP", 3382 `!ls f. EVERY (\x. ?y. x = f y) ls ==> ?l. ls = MAP f l`, 3383 Induct 3384 >> ASM_SIMP_TAC (srw_ss()) [] 3385 >> rw [] 3386 >> RES_TAC 3387 >> Q.EXISTS_TAC`y::l` 3388 >> ASM_SIMP_TAC (srw_ss()) []) 3389 3390val LIST_TO_SET_FLAT = Q.store_thm("LIST_TO_SET_FLAT", 3391 `!ls. set (FLAT ls) = BIGUNION (set (MAP set ls))`, 3392 Induct >> ASM_SIMP_TAC (srw_ss()) []) 3393 3394val MEM_APPEND_lemma = Q.store_thm("MEM_APPEND_lemma", 3395 `!a b c d x. 3396 (a ++ [x] ++ b = c ++ [x] ++ d) /\ x NOTIN set b /\ x NOTIN set a ==> 3397 (a = c) /\ (b = d)`, 3398 rw [APPEND_EQ_APPEND_MID] 3399 >> fs [] 3400 >> fs [APPEND_EQ_SING]) 3401 3402val EVERY2_REVERSE = Q.store_thm("EVERY2_REVERSE", 3403 `!R l1 l2. EVERY2 R l1 l2 ==> EVERY2 R (REVERSE l1) (REVERSE l2)`, 3404 rw [EVERY2_EVERY, EVERY_MEM, FORALL_PROD] 3405 >> REV_FULL_SIMP_TAC (srw_ss()) 3406 [MEM_ZIP, GSYM LEFT_FORALL_IMP_THM, EL_REVERSE] 3407 >> FIRST_X_ASSUM MATCH_MP_TAC 3408 >> ASM_SIMP_TAC (arith_ss) []); 3409 3410val SUM_MAP_PLUS = Q.store_thm("SUM_MAP_PLUS", 3411 `!f g ls. SUM (MAP (\x. f x + g x) ls) = SUM (MAP f ls) + SUM (MAP g ls)`, 3412 NTAC 2 GEN_TAC >> Induct >> simp [SUM]) 3413 3414val TAKE_LENGTH_ID_rwt = Q.store_thm("TAKE_LENGTH_ID_rwt", 3415 `!l m. (m = LENGTH l) ==> (TAKE m l = l)`, 3416 rw [TAKE_LENGTH_ID]) 3417 3418val TAKE_LENGTH_ID_rwt = Q.store_thm("TAKE_LENGTH_ID_rwt", 3419 `!l m. (m = LENGTH l) ==> (TAKE m l = l)`, 3420 rw [TAKE_LENGTH_ID]) 3421 3422val ZIP_DROP = Q.store_thm("ZIP_DROP", 3423 `!a b n. n <= LENGTH a /\ (LENGTH a = LENGTH b) ==> 3424 (ZIP (DROP n a,DROP n b) = DROP n (ZIP (a,b)))`, 3425 Induct 3426 THEN SRW_TAC [] [LENGTH_NIL_SYM, arithmeticTheory.ADD1] 3427 THEN Cases_on`b` 3428 THEN FULL_SIMP_TAC (srw_ss()) [ZIP] 3429 THEN Cases_on`0<n` THEN FULL_SIMP_TAC (srw_ss()) [ZIP] 3430 THEN FIRST_X_ASSUM MATCH_MP_TAC 3431 THEN FULL_SIMP_TAC arith_ss []) 3432 3433val GENLIST_EL = Q.store_thm("GENLIST_EL", 3434 `!ls f n. (n = LENGTH ls) /\ (!i. i < n ==> (f i = EL i ls)) ==> 3435 (GENLIST f n = ls)`, 3436 rw [LIST_EQ_REWRITE]) 3437 3438val EVERY2_trans = Q.store_thm("EVERY2_trans", 3439 `(!x y z. R x y /\ R y z ==> R x z) ==> 3440 !x y z. EVERY2 R x y /\ EVERY2 R y z ==> EVERY2 R x z`, 3441 SRW_TAC [] [EVERY2_EVERY, EVERY_MEM, FORALL_PROD] 3442 THEN REPEAT (Q.PAT_X_ASSUM `LENGTH X = Y` MP_TAC) 3443 THEN REPEAT STRIP_TAC 3444 THEN FULL_SIMP_TAC (srw_ss()++DNF_ss) [MEM_ZIP] 3445 THEN METIS_TAC []) 3446 3447val EVERY2_sym = Q.store_thm("EVERY2_sym", 3448 `(!x y. R1 x y ==> R2 y x) ==> !x y. EVERY2 R1 x y ==> EVERY2 R2 y x`, 3449 SRW_TAC [] [EVERY2_EVERY, EVERY_MEM, FORALL_PROD] 3450 THEN Q.PAT_X_ASSUM `LENGTH X = Y` MP_TAC 3451 THEN STRIP_TAC 3452 THEN FULL_SIMP_TAC (srw_ss()++DNF_ss) [MEM_ZIP]) 3453 3454val EVERY2_LUPDATE_same = Q.store_thm("EVERY2_LUPDATE_same", 3455 `!P l1 l2 v1 v2 n. 3456 P v1 v2 /\ EVERY2 P l1 l2 ==> 3457 EVERY2 P (LUPDATE v1 n l1) (LUPDATE v2 n l2)`, 3458 GEN_TAC 3459 THEN Induct 3460 THEN SRW_TAC [] [LUPDATE_def] 3461 THEN Cases_on`n` 3462 THEN SRW_TAC [] [LUPDATE_def] 3463 THEN Cases_on`l2` 3464 THEN FULL_SIMP_TAC (srw_ss()) [LUPDATE_def]) 3465 3466val EVERY2_refl = Q.store_thm("EVERY2_refl", 3467 `(!x. MEM x ls ==> R x x) ==> (EVERY2 R ls ls)`, 3468 Induct_on`ls` >> rw []) 3469 3470val EVERY2_THM = Q.store_thm("EVERY2_THM[simp]", 3471 `(!P ys. EVERY2 P [] ys = (ys = [])) /\ 3472 (!P yys x xs. EVERY2 P (x::xs) yys = 3473 ?y ys. (yys = y::ys) /\ (P x y) /\ (EVERY2 P xs ys)) /\ 3474 (!P xs. EVERY2 P xs [] = (xs = [])) /\ 3475 (!P xxs y ys. EVERY2 P xxs (y::ys) = 3476 ?x xs. (xxs = x::xs) /\ (P x y) /\ (EVERY2 P xs ys))`, 3477 REPEAT CONJ_TAC 3478 THEN GEN_TAC 3479 THEN TRY (SRW_TAC [] [EVERY2_EVERY, LENGTH_NIL] 3480 THEN SRW_TAC [] [EQ_IMP_THM] 3481 THEN NO_TAC) 3482 THEN Cases 3483 THEN SRW_TAC [] [EVERY2_EVERY]) 3484 3485val LIST_REL_trans = Q.store_thm("LIST_REL_trans", 3486 `!l1 l2 l3. 3487 (!n. n < LENGTH l1 /\ R (EL n l1) (EL n l2) /\ 3488 R (EL n l2) (EL n l3) ==> R (EL n l1) (EL n l3)) /\ 3489 LIST_REL R l1 l2 /\ LIST_REL R l2 l3 ==> LIST_REL R l1 l3`, 3490 Induct 3491 >> simp [] 3492 >> rw [LIST_REL_CONS1] 3493 >> fs [LIST_REL_CONS1] 3494 >> rw [] 3495 THEN1 (FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) >> rw []) 3496 >> FIRST_X_ASSUM MATCH_MP_TAC 3497 >> Q.RENAME_TAC [`LIST_REL _ l1 l2`, `LIST_REL _ l2 l3`] 3498 >> Q.EXISTS_TAC`l2` 3499 >> rw [] 3500 >> FIRST_X_ASSUM (Q.SPEC_THEN `SUC n` MP_TAC) 3501 >> simp []); 3502 3503val SWAP_REVERSE = Q.store_thm("SWAP_REVERSE", 3504 `!l1 l2. (l1 = REVERSE l2) = (l2 = REVERSE l1)`, 3505 SRW_TAC [] [EQ_IMP_THM]) 3506 3507val SWAP_REVERSE_SYM = Q.store_thm("SWAP_REVERSE_SYM", 3508 `!l1 l2. (REVERSE l1 = l2) = (l1 = REVERSE l2)`, 3509 metis_tac [SWAP_REVERSE]) 3510 3511val BIGUNION_IMAGE_set_SUBSET = Q.store_thm("BIGUNION_IMAGE_set_SUBSET", 3512 `(BIGUNION (IMAGE f (set ls)) SUBSET s) = (!x. MEM x ls ==> f x SUBSET s)`, 3513 SRW_TAC [DNF_ss] [SUBSET_DEF] THEN METIS_TAC []) 3514 3515val IMAGE_EL_count_LENGTH = Q.store_thm("IMAGE_EL_count_LENGTH", 3516 `!f ls. IMAGE (\n. f (EL n ls)) (count (LENGTH ls)) = IMAGE f (set ls)`, 3517 rw [EXTENSION, MEM_EL] >> PROVE_TAC []) 3518 3519val GENLIST_EL_MAP = Q.store_thm("GENLIST_EL_MAP", 3520 `!f ls. GENLIST (\n. f (EL n ls)) (LENGTH ls) = MAP f ls`, 3521 GEN_TAC >> Induct >> rw [GENLIST_CONS, o_DEF]) 3522 3523val LENGTH_FILTER_LEQ_MONO = Q.store_thm("LENGTH_FILTER_LEQ_MONO", 3524 `!P Q. (!x. P x ==> Q x) ==> 3525 !ls. (LENGTH (FILTER P ls) <= LENGTH (FILTER Q ls))`, 3526 REPEAT GEN_TAC 3527 >> STRIP_TAC 3528 >> Induct 3529 >> rw [] 3530 >> FULL_SIMP_TAC arith_ss [] 3531 >> PROVE_TAC []) 3532 3533val LIST_EQ_MAP_PAIR = Q.store_thm("LIST_EQ_MAP_PAIR", 3534 `!l1 l2. 3535 (MAP FST l1 = MAP FST l2) /\ (MAP SND l1 = MAP SND l2) ==> (l1 = l2)`, 3536 SRW_TAC [] 3537 [MAP_EQ_EVERY2, EVERY2_EVERY, EVERY_MEM, LIST_EQ_REWRITE, FORALL_PROD] 3538 THEN REV_FULL_SIMP_TAC (srw_ss()++DNF_ss) [MEM_ZIP] 3539 THEN METIS_TAC [pair_CASES, PAIR_EQ]) 3540 3541val TAKE_SUM = Q.store_thm("TAKE_SUM", 3542 `!n m l. TAKE (n + m) l = TAKE n l ++ TAKE m (DROP n l)`, 3543 Induct_on `l` >> simp[TAKE_def] >> rw[] >> simp[] >> 3544 `m + n - 1 = (n - 1) + m` by simp[] >> 3545 ASM_REWRITE_TAC[]); 3546 3547val ALL_DISTINCT_FILTER_EL_IMP = Q.store_thm("ALL_DISTINCT_FILTER_EL_IMP", 3548 `!P l n1 n2. 3549 ALL_DISTINCT (FILTER P l) /\ n1 < LENGTH l /\ n2 < LENGTH l /\ 3550 (P (EL n1 l)) /\ (EL n1 l = EL n2 l) ==> (n1 = n2)`, 3551 GEN_TAC 3552 THEN Induct 3553 THEN1 SRW_TAC [] [] 3554 THEN SRW_TAC [] [] 3555 THEN FULL_SIMP_TAC (srw_ss()) [MEM_FILTER] 3556 THEN1 PROVE_TAC [] 3557 THEN Cases_on `n1` 3558 THEN Cases_on `n2` 3559 THEN FULL_SIMP_TAC (srw_ss()) [MEM_EL] 3560 THEN PROVE_TAC []) 3561 3562val FLAT_EQ_NIL = Q.store_thm("FLAT_EQ_NIL", 3563 `!ls. (FLAT ls = []) = (EVERY ($= []) ls)`, 3564 Induct >> SRW_TAC [] [EQ_IMP_THM] >> rw [APPEND]); 3565 3566val ALL_DISTINCT_MAP_INJ = Q.store_thm("ALL_DISTINCT_MAP_INJ", 3567 `!ls f. (!x y. MEM x ls /\ MEM y ls /\ (f x = f y) ==> (x = y)) /\ 3568 ALL_DISTINCT ls ==> ALL_DISTINCT (MAP f ls)`, 3569 Induct THEN SRW_TAC [] [MEM_MAP] THEN PROVE_TAC []) 3570 3571val LENGTH_o_REVERSE = Q.store_thm("LENGTH_o_REVERSE", 3572 `(LENGTH o REVERSE = LENGTH) /\ 3573 (LENGTH o REVERSE o f = LENGTH o f)`, 3574 SRW_TAC [] [FUN_EQ_THM]) 3575 3576val REVERSE_o_REVERSE = Q.store_thm("REVERSE_o_REVERSE", 3577 `(REVERSE o REVERSE o f = f)`, 3578 SRW_TAC [] [FUN_EQ_THM]) 3579 3580val GENLIST_PLUS_APPEND = Q.store_thm("GENLIST_PLUS_APPEND", 3581 `GENLIST ($+ a) n1 ++ GENLIST ($+ (n1 + a)) n2 = GENLIST ($+ a) (n1 + n2)`, 3582 rw [Once arithmeticTheory.ADD_SYM, SimpRHS] 3583 >> RW_TAC arith_ss [GENLIST_APPEND] 3584 >> SRW_TAC [ETA_ss] [arithmeticTheory.ADD_ASSOC]) 3585 3586val LIST_TO_SET_GENLIST = Q.store_thm("LIST_TO_SET_GENLIST", 3587 `!f n. LIST_TO_SET (GENLIST f n) = IMAGE f (count n)`, 3588 SRW_TAC [] [EXTENSION, MEM_GENLIST] THEN PROVE_TAC []) 3589 3590val MEM_ZIP_MEM_MAP = Q.store_thm("MEM_ZIP_MEM_MAP", 3591 `(LENGTH (FST ps) = LENGTH (SND ps)) /\ 3592 MEM p (ZIP ps) ==> MEM (FST p) (FST ps) /\ MEM (SND p) (SND ps)`, 3593 Cases_on `p` 3594 >> Cases_on `ps` 3595 >> SRW_TAC [] [] 3596 >> REV_FULL_SIMP_TAC (srw_ss()) [MEM_ZIP, MEM_EL] 3597 >> PROVE_TAC []) 3598 3599val DISJOINT_GENLIST_PLUS = Q.store_thm("DISJOINT_GENLIST_PLUS", 3600 `DISJOINT x (set (GENLIST ($+ n) (a + b))) ==> 3601 DISJOINT x (set (GENLIST ($+ n) a)) /\ 3602 DISJOINT x (set (GENLIST ($+ (n + a)) b))`, 3603 rw [GSYM GENLIST_PLUS_APPEND] 3604 >> metis_tac [DISJOINT_SYM, arithmeticTheory.ADD_SYM]) 3605 3606val EVERY2_MAP = Q.store_thm("EVERY2_MAP", 3607 `(EVERY2 P (MAP f l1) l2 = EVERY2 (\x y. P (f x) y) l1 l2) /\ 3608 (EVERY2 Q l1 (MAP g l2) = EVERY2 (\x y. Q x (g y)) l1 l2)`, 3609 rw [EVERY2_EVERY] 3610 >> Cases_on `LENGTH l1 = LENGTH l2` 3611 >> fs [] 3612 >> rw [ZIP_MAP, EVERY_MEM, MEM_MAP] 3613 >> SRW_TAC [DNF_ss] [pairTheory.FORALL_PROD, LENGTH_MAP] 3614 >> PROVE_TAC []); 3615 3616val exists_list_GENLIST = Q.store_thm("exists_list_GENLIST", 3617 `(?ls. P ls) = (?n f. P (GENLIST f n))`, 3618 rw [EQ_IMP_THM] 3619 THEN1 (MAP_EVERY Q.EXISTS_TAC [`LENGTH ls`,`combin$C EL ls`] 3620 >> Q.MATCH_ABBREV_TAC `P ls2` 3621 >> Q_TAC SUFF_TAC `ls2 = ls` 3622 THEN1 rw [] 3623 >> rw [LIST_EQ_REWRITE, Abbr`ls2`]) 3624 >> PROVE_TAC []) 3625 3626val EVERY_MEM_MONO = Q.store_thm("EVERY_MEM_MONO", 3627 `!P Q l. (!x. MEM x l /\ P x ==> Q x) /\ EVERY P l ==> EVERY Q l`, 3628 NTAC 2 GEN_TAC >> Induct >> rw []) 3629 3630val EVERY2_MEM_MONO = Q.store_thm("EVERY2_MEM_MONO", 3631 `!P Q l1 l2. (!x. MEM x (ZIP (l1,l2)) /\ UNCURRY P x ==> UNCURRY Q x) /\ 3632 EVERY2 P l1 l2 ==> EVERY2 Q l1 l2`, 3633 rw [EVERY2_EVERY] >> MATCH_MP_TAC EVERY_MEM_MONO >> PROVE_TAC []) 3634 3635val mem_exists_set = Q.store_thm ("mem_exists_set", 3636 `!x y l. MEM (x,y) l ==> ?z. (x = FST z) /\ z IN set l`, 3637 Induct_on `l` 3638 >> rw [] 3639 >> metis_tac [FST]); 3640 3641val every_zip_snd = Q.store_thm ("every_zip_snd", 3642 `!l1 l2 P. 3643 (LENGTH l1 = LENGTH l2) ==> 3644 (EVERY (\x. P (SND x)) (ZIP (l1,l2)) = EVERY P l2)`, 3645 Induct_on `l1` 3646 >> rw [] 3647 >> TRY(Cases_on `l2`) 3648 >> fs [ZIP]); 3649 3650val every_zip_fst = Q.store_thm ("every_zip_fst", 3651 `!l1 l2 P. (LENGTH l1 = LENGTH l2) ==> 3652 (EVERY (\x. P (FST x)) (ZIP (l1,l2)) = EVERY P l1)`, 3653 Induct_on `l1` 3654 >> rw [] 3655 >> TRY(Cases_on `l2`) 3656 >> fs [ZIP]); 3657 3658val el_append3 = Q.store_thm ("el_append3", 3659 `!l1 x l2. EL (LENGTH l1) (l1++ [x] ++ l2) = x`, 3660 Induct_on `l1` 3661 >> rw [] 3662 >> rw []); 3663 3664val lupdate_append = Q.store_thm ("lupdate_append", 3665 `!x n l1 l2. 3666 n < LENGTH l1 ==> (LUPDATE x n (l1++l2) = LUPDATE x n l1 ++ l2)`, 3667 Induct_on `l1` 3668 >> rw [] 3669 >> Cases_on `n` 3670 >> rw [LUPDATE_def] 3671 >> fs []); 3672 3673val lupdate_append2 = Q.store_thm ("lupdate_append2", 3674 `!v l1 x l2 l3. LUPDATE v (LENGTH l1) (l1++[x]++l2) = l1++[v]++l2`, 3675 Induct_on `l1` >> rw [LUPDATE_def]) 3676 3677val HD_REVERSE = store_thm ("HD_REVERSE", 3678 ``!x. x <> [] ==> (HD (REVERSE x) = LAST x)``, 3679 REPEAT strip_tac >> 3680 Induct_on `x` THEN1 fs[] >> 3681 rw[LAST_DEF] >> 3682 Cases_on `REVERSE x` THEN1 fs[] >> 3683 fs[]); 3684 3685val LAST_REVERSE = Q.store_thm("LAST_REVERSE", 3686 `!ls. ls <> [] ==> (LAST (REVERSE ls) = HD ls)`, 3687 Induct >> simp []) 3688 3689val NOT_NIL_EQ_LENGTH_NOT_0 = store_thm ( "NOT_NIL_EQ_LENGTH_NOT_0", 3690 ``x <> [] <=> (0 < LENGTH x)``, 3691 Cases_on `x` >> rw[]); 3692 3693val last_drop = Q.store_thm ("last_drop", 3694 `!l n. n < LENGTH l ==> (LAST (DROP n l) = LAST l)`, 3695 Induct >> rw [DROP_def] >> 3696 Q.SPEC_THEN`l`FULL_STRUCT_CASES_TAC list_CASES >> fs [] >> 3697 FULL_SIMP_TAC (srw_ss()++numSimps.ARITH_ss) [] >> SRW_TAC[] [] >> 3698 FIRST_X_ASSUM (Q.SPEC_THEN `n - 1` MP_TAC) >> 3699 simp[]); 3700 3701val dropWhile_def = Define` 3702 (dropWhile P [] = []) /\ 3703 (dropWhile P (h::t) = if P h then dropWhile P t else (h::t))` 3704val _ = export_rewrites ["dropWhile_def"] 3705 3706val dropWhile_splitAtPki = Q.store_thm("dropWhile_splitAtPki", 3707 `!P. dropWhile P = splitAtPki (combin$C (K o $~ o P)) (K I)`, 3708 GEN_TAC 3709 >> simp [FUN_EQ_THM] 3710 >> Induct 3711 >> simp [splitAtPki_def] 3712 >> rw [] 3713 >> AP_THM_TAC 3714 >> Q.MATCH_ABBREV_TAC `f a b = f a' b'` 3715 >> `b = b'` by (markerLib.UNABBREV_ALL_TAC >> simp [FUN_EQ_THM]) 3716 >> `a = a'` by (markerLib.UNABBREV_ALL_TAC >> simp [FUN_EQ_THM]) 3717 >> REV_FULL_SIMP_TAC (srw_ss()) []) 3718 3719val dropWhile_eq_nil = Q.store_thm("dropWhile_eq_nil", 3720 `!P ls. (dropWhile P ls = []) <=> EVERY P ls`, 3721 GEN_TAC >> Induct >> simp [] >> rw []) 3722 3723val MEM_dropWhile_IMP = Q.store_thm("MEM_dropWhile_IMP", 3724 `!P ls x. MEM x (dropWhile P ls) ==> MEM x ls`, 3725 GEN_TAC >> Induct >> simp [] >> rw []) 3726 3727val HD_dropWhile = Q.store_thm("HD_dropWhile", 3728 `!P ls. EXISTS ($~ o P) ls ==> ~ P (HD (dropWhile P ls))`, 3729 GEN_TAC >> Induct >> simp [] >> rw []) 3730 3731val LENGTH_dropWhile_LESS_EQ = Q.store_thm("LENGTH_dropWhile_LESS_EQ", 3732 `!P ls. LENGTH (dropWhile P ls) <= LENGTH ls`, 3733 GEN_TAC >> Induct >> simp [] >> rw [] >> simp []) 3734 3735val dropWhile_APPEND_EVERY = Q.store_thm("dropWhile_APPEND_EVERY", 3736 `!P l1 l2. EVERY P l1 ==> (dropWhile P (l1 ++ l2) = dropWhile P l2)`, 3737 GEN_TAC >> Induct >> simp [dropWhile_def]) 3738 3739val dropWhile_APPEND_EXISTS = Q.store_thm("dropWhile_APPEND_EXISTS", 3740 `!P l1 l2. EXISTS ($~ o P) l1 ==> 3741 (dropWhile P (l1 ++ l2) = dropWhile P l1 ++ l2)`, 3742 GEN_TAC >> Induct >> simp [dropWhile_def] >> rw []) 3743 3744local 3745 val fs = FULL_SIMP_TAC (srw_ss()++numSimps.ARITH_ss) 3746 val rw = SRW_TAC [numSimps.ARITH_ss] 3747in 3748val EL_LENGTH_dropWhile_REVERSE = Q.store_thm("EL_LENGTH_dropWhile_REVERSE", 3749 `!P ls k. LENGTH (dropWhile P (REVERSE ls)) <= k /\ k < LENGTH ls ==> 3750 P (EL k ls)`, 3751 GEN_TAC 3752 >> Induct 3753 >> simp [LENGTH] 3754 >> rw [] 3755 >> Cases_on `k` 3756 >> fs [LENGTH_NIL, dropWhile_eq_nil, EVERY_APPEND] 3757 >> FIRST_X_ASSUM MATCH_MP_TAC 3758 >> simp [] 3759 >> Cases_on `EVERY P (REVERSE ls)` 3760 THEN1 (fs [dropWhile_APPEND_EVERY, GSYM dropWhile_eq_nil]) 3761 >> fs [NOT_EVERY, dropWhile_APPEND_EXISTS, arithmeticTheory.ADD1]) 3762end 3763 3764val LENGTH_TAKE_EQ = store_thm("LENGTH_TAKE_EQ", 3765 ``LENGTH (TAKE n xs) = if n <= LENGTH xs then n else LENGTH xs``, 3766 SRW_TAC [] [] THEN fs [GSYM NOT_LESS] THEN AP_TERM_TAC 3767 THEN MATCH_MP_TAC TAKE_LENGTH_TOO_LONG THEN numLib.DECIDE_TAC); 3768 3769val IMP_EVERY_LUPDATE = store_thm("IMP_EVERY_LUPDATE", 3770 ``!xs h i. P h /\ EVERY P xs ==> EVERY P (LUPDATE h i xs)``, 3771 Induct THEN fs [LUPDATE_def] THEN REPEAT STRIP_TAC 3772 THEN Cases_on `i` THEN fs [LUPDATE_def]); 3773 3774val MAP_APPEND_MAP_EQ = store_thm("MAP_APPEND_MAP_EQ", 3775 ``!xs ys. 3776 ((MAP f1 xs ++ MAP g1 ys) = (MAP f2 xs ++ MAP g2 ys)) <=> 3777 (MAP f1 xs = MAP f2 xs) /\ (MAP g1 ys = MAP g2 ys)``, 3778 Induct THEN fs [] THEN METIS_TAC []); 3779 3780val LUPDATE_SOME_MAP = store_thm("LUPDATE_SOME_MAP", 3781 ``!xs n f h. 3782 LUPDATE (SOME (f h)) n (MAP (OPTION_MAP f) xs) = 3783 MAP (OPTION_MAP f) (LUPDATE (SOME h) n xs)``, 3784 Induct THEN1 (fs [LUPDATE_def]) THEN 3785 Cases_on `n` THEN fs [LUPDATE_def]); 3786 3787val ZIP_EQ_NIL = store_thm("ZIP_EQ_NIL", 3788 ``!l1 l2. (LENGTH l1 = LENGTH l2) ==> 3789 ((ZIP (l1,l2) = []) <=> ((l1 = []) /\ (l2 = [])))``, 3790 REPEAT GEN_TAC >> Cases_on`l1` >> rw[LENGTH_NIL_SYM,ZIP] >> Cases_on`l2` >> 3791 fs[ZIP]) 3792 3793val LUPDATE_SAME = store_thm("LUPDATE_SAME", 3794 ``!n ls. n < LENGTH ls ==> (LUPDATE (EL n ls) n ls = ls)``, 3795 rw[LIST_EQ_REWRITE,EL_LUPDATE]>>rw[]) 3796 3797(* end CakeML lemmas *) 3798 3799(* u is unique in L, learnt from Robert Beers <robert@beers.org> *) 3800val UNIQUE_DEF = new_definition ("UNIQUE_DEF", 3801 ``UNIQUE e L = ?L1 L2. (L1 ++ [e] ++ L2 = L) /\ ~MEM e L1 /\ ~MEM e L2``); 3802 3803local 3804 fun take ts = MAP_EVERY Q.EXISTS_TAC ts; (* from HOL mizar mode *) 3805 val Know = Q_TAC KNOW_TAC; (* from util_prob *) 3806 val Suff = Q_TAC SUFF_TAC; (* from util_prob *) 3807 fun K_TAC _ = ALL_TAC; (* from util_prob *) 3808 val KILL_TAC = POP_ASSUM_LIST K_TAC; (* from util_prob *) 3809 fun wrap a = [a]; (* from util_prob *) 3810 val Rewr = DISCH_THEN (REWRITE_TAC o wrap); (* from util_prob *) 3811in 3812(* alternative definition of UNIQUE, by Chun Tian (binghe) *) 3813val UNIQUE_FILTER = store_thm ( 3814 "UNIQUE_FILTER", ``!e L. UNIQUE e L = (FILTER ($= e) L = [e])``, 3815 rpt GEN_TAC 3816 >> REWRITE_TAC [UNIQUE_DEF] 3817 >> EQ_TAC >> rpt STRIP_TAC (* 2 sub-goals here *) 3818 >| [ (* goal 1 (of 2) *) 3819 Q.PAT_X_ASSUM `P = L` (REWRITE_TAC o wrap o SYM) \\ 3820 REWRITE_TAC [FILTER_APPEND_DISTRIB] \\ 3821 Know `((FILTER ($= e) L1) = []) /\ ((FILTER ($= e) L2) = [])` 3822 >- ( REWRITE_TAC [GSYM NULL_EQ] \\ 3823 REWRITE_TAC [NULL_FILTER] \\ 3824 rpt STRIP_TAC >> FULL_SIMP_TAC arith_ss [] ) \\ 3825 Rewr \\ 3826 REWRITE_TAC [APPEND, APPEND_NIL, FILTER], 3827 (* goal 2 (of 2) *) 3828 Know `MEM e L` 3829 >- ( `FILTER ($= e) L <> []` by PROVE_TAC [NOT_CONS_NIL] \\ 3830 FULL_SIMP_TAC arith_ss [FILTER_NEQ_NIL] ) \\ 3831 REWRITE_TAC [MEM_SPLIT] >> rpt STRIP_TAC \\ 3832 take [`l1`, `l2`] >> FULL_SIMP_TAC arith_ss [] \\ 3833 CONJ_TAC >- ( KILL_TAC >> REWRITE_TAC [GSYM APPEND_ASSOC] \\ 3834 SIMP_TAC arith_ss [APPEND, APPEND_11] ) \\ 3835 POP_ASSUM K_TAC \\ 3836 POP_ASSUM MP_TAC \\ 3837 SIMP_TAC arith_ss [FILTER_APPEND_DISTRIB, FILTER] \\ 3838 REWRITE_TAC [APPEND_EQ_SING] \\ 3839 rpt STRIP_TAC \\ 3840 FULL_SIMP_TAC arith_ss [NOT_CONS_NIL, FILTER_APPEND_DISTRIB, FILTER, APPEND_eq_NIL, CONS_11] ]); 3841 3842(* alternative definition of UNIQUE, learnt from Scott Owens and Anthony Fox *) 3843val UNIQUE_LENGTH_FILTER = store_thm ( 3844 "UNIQUE_LENGTH_FILTER", ``!e L. UNIQUE e L = (LENGTH (FILTER ($= e) L) = 1)``, 3845 rpt GEN_TAC 3846 >> REWRITE_TAC [UNIQUE_FILTER] 3847 >> EQ_TAC >> DISCH_TAC 3848 >- ( ASM_REWRITE_TAC [] >> REWRITE_TAC [LENGTH] >> ACCEPT_TAC (SYM ONE) ) 3849 >> POP_ASSUM MP_TAC 3850 >> REWRITE_TAC [ONE, LENGTH_EQ_NUM] 3851 >> SIMP_TAC arith_ss [] 3852 >> rpt STRIP_TAC 3853 >> Cases_on `e = h` >- ASM_REWRITE_TAC [] 3854 >> ASM_REWRITE_TAC [] 3855 >> FULL_SIMP_TAC arith_ss [CONS_11] 3856 >> Suff `MEM e (FILTER ($= e) L)` 3857 >- ( DISCH_TAC \\ 3858 REV_FULL_SIMP_TAC (arith_ss ++ pred_setSimps.PRED_SET_ss) [LIST_TO_SET] ) 3859 >> REWRITE_TAC [MEM_FILTER] 3860 >> Know `FILTER ($= e) L <> []` >- FULL_SIMP_TAC arith_ss [NOT_CONS_NIL] 3861 >> KILL_TAC 3862 >> REWRITE_TAC [FILTER_NEQ_NIL] 3863 >> rpt STRIP_TAC 3864 >> ASM_REWRITE_TAC []); 3865end; (* local *) 3866 3867(* OPT_MMAP : ('a -> 'b option) -> 'a list -> 'b list option *) 3868val OPT_MMAP_def = Define` 3869 (OPT_MMAP f [] = SOME []) /\ 3870 (OPT_MMAP f (h0::t0) = 3871 OPTION_BIND (f h0) (\h. OPTION_BIND (OPT_MMAP f t0) (\t. SOME (h::t)))) 3872`; 3873 3874val OPT_MMAP_cong = Q.store_thm("OPT_MMAP_cong[defncong]", 3875 `!f1 f2 x1 x2. 3876 (x1 = x2) /\ (!a. MEM a x2 ==> (f1 a = f2 a)) 3877 ==> (OPT_MMAP f1 x1 = OPT_MMAP f2 x2)`, 3878 ntac 2 gen_tac \\ Induct \\ rw[] \\ computeLib.EVAL_TAC 3879 \\ FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) []); 3880 3881val LAST_compute = Q.store_thm("LAST_compute", 3882 `(!x. LAST [x] = x) /\ 3883 (!h1 h2 t. LAST (h1::h2::t) = LAST (h2::t))`, 3884 SRW_TAC [] [LAST_DEF]); 3885 3886val TAKE_compute = Q.prove( 3887 `(!l. TAKE 0 l = []) /\ 3888 (!n. TAKE (SUC n) [] = []) /\ 3889 (!n h t. TAKE (SUC n) (h::t) = h :: TAKE n t)`, 3890 SRW_TAC [] []); 3891 3892val DROP_compute = Q.prove( 3893 `(!l. DROP 0 l = l) /\ 3894 (!n. DROP (SUC n) [] = []) /\ 3895 (!n h t. DROP (SUC n) (h::t) = DROP n t)`, 3896 SRW_TAC [] []); 3897 3898val TAKE_compute = 3899 Theory.save_thm("TAKE_compute", numLib.SUC_RULE TAKE_compute); 3900 3901val DROP_compute = 3902 Theory.save_thm("DROP_compute", numLib.SUC_RULE DROP_compute); 3903 3904(* ---------------------------------------------------------------------- 3905 versions of constants with option outputs rather than unspecified 3906 3907 oHD : 'a list -> 'a option 3908 oEL : num -> 'a list -> 'a option 3909 3910 ---------------------------------------------------------------------- *) 3911 3912val oHD_def = Define`oHD l = case l of [] => NONE | h::_ => SOME h` 3913val oHD_thm = Q.store_thm("oHD_thm[simp]", 3914 `(oHD [] = NONE) /\ (oHD (h::t) = SOME h)`, 3915 rw[oHD_def]); 3916 3917val oEL_def = Define` 3918 (oEL n [] = NONE) /\ 3919 (oEL n (x::xs) = if n = 0 then SOME x else oEL (n - 1) xs) 3920`; 3921 3922val oEL_THM = Q.store_thm( 3923 "oEL_THM", 3924 `!xs n. oEL n xs = if n < LENGTH xs then SOME (EL n xs) else NONE`, 3925 Induct >> fs[oEL_def] >> rw[] >> fs[] 3926 >- (Q.RENAME_TAC [���n < SUC (LENGTH xs)���] >> Cases_on ���n��� >> fs[]) >> 3927 rw[] >> ASSUME_TAC (numLib.DECIDE ���!x. 1 + x = SUC x���) >> 3928 fs[arithmeticTheory.NOT_ZERO_LT_ZERO] >> 3929 METIS_TAC[ONE, arithmeticTheory.LESS_LESS_SUC]); 3930 3931val oEL_EQ_EL = Q.store_thm( 3932 "oEL_EQ_EL", 3933 ���!xs n y. (oEL n xs = SOME y) <=> n < LENGTH xs /\ (y = EL n xs)���, 3934 simp[oEL_THM] >> METIS_TAC[]); 3935 3936val oEL_DROP = Q.store_thm( 3937 "oEL_DROP", 3938 ���oEL n (DROP m xs) = oEL (m + n) xs���, 3939 MAP_EVERY Q.ID_SPEC_TAC [���n���, ���m���, ���xs���] >> Induct_on ���xs��� >> 3940 simp[DROP_def, oEL_def] >> rw[oEL_def] >> fs[] >> 3941 Q.RENAME_TAC [���m - 1 + n���] >> 3942 ���m - 1 + n = m + n - 1��� suffices_by simp[] >> 3943 Q.UNDISCH_THEN ���m <> 0��� MP_TAC >> numLib.ARITH_TAC); 3944 3945val oEL_TAKE_E = Q.store_thm( 3946 "oEL_TAKE_E", 3947 ���(oEL n (TAKE m xs) = SOME x) ==> (oEL n xs = SOME x)���, 3948 MAP_EVERY Q.ID_SPEC_TAC [���n���, ���m���, ���xs���] >> Induct_on ���xs��� >> 3949 simp[TAKE_def, oEL_def] >> rw[oEL_def] >> RES_TAC); 3950 3951val oEL_LUPDATE = Q.store_thm( 3952 "oEL_LUPDATE", 3953 ���!xs i n x. oEL n (LUPDATE x i xs) = 3954 if i <> n then oEL n xs else 3955 if i < LENGTH xs then SOME x else NONE���, 3956 Induct >> fs[oEL_def,LUPDATE_def] >> 3957 Cases_on ���i��� >> rw[oEL_def,LUPDATE_def] >> fs[] >> rw[] >> 3958 fs[numLib.DECIDE ���!x. SUC (x - 1) <> x <=> (x = 0)���, 3959 numLib.DECIDE ���!x. 1 + x = SUC x���]); 3960 3961(* ---------------------------------------------------------------------- *) 3962 3963val _ = app DefnBase.export_cong ["EXISTS_CONG", "EVERY_CONG", "MAP_CONG", 3964 "MAP2_CONG", "EVERY2_cong", "FOLDL2_cong", 3965 "FOLDL_CONG", "FOLDR_CONG", "list_size_cong"] 3966 3967val lazy_list_case_compute = save_thm( 3968 "lazy_list_case_compute[compute]", 3969 computeLib.lazyfy_thm list_case_compute); 3970 3971val _ = computeLib.add_persistent_funs [ 3972 "APPEND", "APPEND_NIL", "FLAT", "HD", "TL", "LENGTH", "MAP", "MAP2", 3973 "NULL_DEF", "MEM", "EXISTS_DEF", "DROP_compute", "EVERY_DEF", "ZIP", 3974 "UNZIP", "FILTER", "FOLDL", "FOLDR", 3975 "TAKE_compute", "FOLDL", "REVERSE_REV", "SUM_SUM_ACC", "ALL_DISTINCT", 3976 "GENLIST_AUX", "EL_restricted", "EL_simp_restricted", "SNOC", 3977 "LUPDATE_compute", "GENLIST_NUMERALS", "list_size_def", "FRONT_DEF", 3978 "LAST_compute", "isPREFIX" 3979 ] 3980 3981val _ = 3982 let 3983 val list_info = Option.valOf (TypeBase.read {Thy = "list", Tyop="list"}) 3984 val lift_list = 3985 mk_var ("listSyntax.lift_list", 3986 ���:'type -> ('a -> 'term) -> 'a list -> 'term���) 3987 val list_info' = 3988 list_info |> TypeBasePure.put_lift lift_list 3989 |> TypeBasePure.put_induction 3990 (TypeBasePure.ORIG list_induction) 3991 |> TypeBasePure.put_nchotomy list_nchotomy 3992 in 3993 TypeBase.export [list_info'] 3994 end; 3995 3996val _ = export_rewrites 3997 ["APPEND_11", 3998 "MAP2", "NULL_DEF", 3999 "SUM", "APPEND_ASSOC", "CONS", "CONS_11", 4000 "LENGTH_MAP", "MAP_APPEND", 4001 "NOT_CONS_NIL", "NOT_NIL_CONS", 4002 "CONS_ACYCLIC", "list_case_def", 4003 "ZIP", "UNZIP", "ZIP_UNZIP", "UNZIP_ZIP", 4004 "LENGTH_ZIP", "LENGTH_UNZIP", 4005 "EVERY_APPEND", "EXISTS_APPEND", "EVERY_SIMP", 4006 "EXISTS_SIMP", "NOT_EVERY", "NOT_EXISTS", 4007 "FOLDL", "FOLDR", "LENGTH_LUPDATE", 4008 "LUPDATE_LENGTH"]; 4009 4010val nil_tm = Term.prim_mk_const{Name="NIL",Thy="list"}; 4011val cons_tm = Term.prim_mk_const{Name="CONS",Thy="list"}; 4012 4013fun dest_cons M = 4014 case strip_comb M 4015 of (c,[p,q]) => if Term.same_const c cons_tm then (p,q) 4016 else raise ERR "listScript" "dest_cons" 4017 | otherwise => raise ERR "listScript" "dest_cons" ; 4018 4019fun dest_list M = 4020 case total dest_cons M 4021 of NONE => if same_const nil_tm M then [] 4022 else raise ERR "dest_list" "not terminated with nil" 4023 | SOME(h,t) => h::dest_list t 4024 4025val _ = 4026 monadsyntax.declare_monad ( 4027 "list", 4028 { bind = ���LIST_BIND���, ignorebind = SOME ���LIST_IGNORE_BIND���, 4029 unit = ���SINGL���, choice = SOME ���APPEND���, fail = SOME ���[]���, 4030 guard = SOME ���LIST_GUARD��� } 4031 ) 4032 4033val _ = export_theory(); 4034