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