lists.ml

   1 (* ========================================================================= *)
   2 (* Theory of lists, plus characters and strings as lists of characters.      *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "ind_types.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Standard tactic for list induction using MATCH_MP_TAC list_INDUCT         *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let LIST_INDUCT_TAC =
  17   let list_INDUCT = prove
  18    (`!P:(A)list->bool. P [] /\ (!h t. P t ==> P (CONS h t)) ==> !l. P l`,
  19     MATCH_ACCEPT_TAC list_INDUCT) in
  20   MATCH_MP_TAC list_INDUCT THEN
  21   CONJ_TAC THENL [ALL_TAC; GEN_TAC THEN GEN_TAC THEN DISCH_TAC];;
  22
  23 (* ------------------------------------------------------------------------- *)
  24 (* Basic definitions.                                                        *)
  25 (* ------------------------------------------------------------------------- *)
  26
  27 let HD = new_recursive_definition list_RECURSION
  28   `HD(CONS (h:A) t) = h`;;
  29
  30 let TL = new_recursive_definition list_RECURSION
  31   `TL(CONS (h:A) t) = t`;;
  32
  33 let APPEND = new_recursive_definition list_RECURSION
  34   `(!l:(A)list. APPEND [] l = l) /\
  35    (!h t l. APPEND (CONS h t) l = CONS h (APPEND t l))`;;
  36
  37 let REVERSE = new_recursive_definition list_RECURSION
  38   `(REVERSE [] = []) /\
  39    (REVERSE (CONS (x:A) l) = APPEND (REVERSE l) [x])`;;
  40
  41 let LENGTH = new_recursive_definition list_RECURSION
  42   `(LENGTH [] = 0) /\
  43    (!h:A. !t. LENGTH (CONS h t) = SUC (LENGTH t))`;;
  44
  45 let MAP = new_recursive_definition list_RECURSION
  46   `(!f:A->B. MAP f NIL = NIL) /\
  47    (!f h t. MAP f (CONS h t) = CONS (f h) (MAP f t))`;;
  48
  49 let LAST = new_recursive_definition list_RECURSION
  50   `LAST (CONS (h:A) t) = if t = [] then h else LAST t`;;
  51
  52 let BUTLAST = new_recursive_definition list_RECURSION
  53  `(BUTLAST [] = []) /\
  54   (BUTLAST (CONS h t) = if t = [] then [] else CONS h (BUTLAST t))`;;
  55
  56 let REPLICATE = new_recursive_definition num_RECURSION
  57   `(REPLICATE 0 x = []) /\
  58    (REPLICATE (SUC n) x = CONS x (REPLICATE n x))`;;
  59
  60 let NULL = new_recursive_definition list_RECURSION
  61   `(NULL [] = T) /\
  62    (NULL (CONS h t) = F)`;;
  63
  64 let ALL = new_recursive_definition list_RECURSION
  65   `(ALL P [] = T) /\
  66    (ALL P (CONS h t) <=> P h /\ ALL P t)`;;
  67
  68 let EX = new_recursive_definition list_RECURSION
  69   `(EX P [] = F) /\
  70    (EX P (CONS h t) <=> P h \/ EX P t)`;;
  71
  72 let ITLIST = new_recursive_definition list_RECURSION
  73   `(ITLIST f [] b = b) /\
  74    (ITLIST f (CONS h t) b = f h (ITLIST f t b))`;;
  75
  76 let MEM = new_recursive_definition list_RECURSION
  77   `(MEM x [] <=> F) /\
  78    (MEM x (CONS h t) <=> (x = h) \/ MEM x t)`;;
  79
  80 let ALL2_DEF = new_recursive_definition list_RECURSION
  81   `(ALL2 P [] l2 <=> (l2 = [])) /\
  82    (ALL2 P (CONS h1 t1) l2 <=>
  83         if l2 = [] then F
  84         else P h1 (HD l2) /\ ALL2 P t1 (TL l2))`;;
  85
  86 let ALL2 = prove
  87  (`(ALL2 P [] [] <=> T) /\
  88    (ALL2 P (CONS h1 t1) [] <=> F) /\
  89    (ALL2 P [] (CONS h2 t2) <=> F) /\
  90    (ALL2 P (CONS h1 t1) (CONS h2 t2) <=> P h1 h2 /\ ALL2 P t1 t2)`,
  91   REWRITE_TAC[distinctness "list"; ALL2_DEF; HD; TL]);;
  92
  93 let MAP2_DEF = new_recursive_definition list_RECURSION
  94   `(MAP2 f [] l = []) /\
  95    (MAP2 f (CONS h1 t1) l = CONS (f h1 (HD l)) (MAP2 f t1 (TL l)))`;;
  96
  97 let MAP2 = prove
  98  (`(MAP2 f [] [] = []) /\
  99    (MAP2 f (CONS h1 t1) (CONS h2 t2) = CONS (f h1 h2) (MAP2 f t1 t2))`,
 100   REWRITE_TAC[MAP2_DEF; HD; TL]);;
 101
 102 let EL = new_recursive_definition num_RECURSION
 103   `(EL 0 l = HD l) /\
 104    (EL (SUC n) l = EL n (TL l))`;;
 105
 106 let FILTER = new_recursive_definition list_RECURSION
 107   `(FILTER P [] = []) /\
 108    (FILTER P (CONS h t) = if P h then CONS h (FILTER P t) else FILTER P t)`;;
 109
 110 let ASSOC = new_recursive_definition list_RECURSION
 111   `ASSOC a (CONS h t) = if FST h = a then SND h else ASSOC a t`;;
 112
 113 let ITLIST2_DEF = new_recursive_definition list_RECURSION
 114   `(ITLIST2 f [] l2 b = b) /\
 115    (ITLIST2 f (CONS h1 t1) l2 b = f h1 (HD l2) (ITLIST2 f t1 (TL l2) b))`;;
 116
 117 let ITLIST2 = prove
 118  (`(ITLIST2 f [] [] b = b) /\
 119    (ITLIST2 f (CONS h1 t1) (CONS h2 t2) b = f h1 h2 (ITLIST2 f t1 t2 b))`,
 120   REWRITE_TAC[ITLIST2_DEF; HD; TL]);;
 121
 122 let ZIP_DEF = new_recursive_definition list_RECURSION
 123   `(ZIP [] l2 = []) /\
 124    (ZIP (CONS h1 t1) l2 = CONS (h1,HD l2) (ZIP t1 (TL l2)))`;;
 125
 126 let ZIP = prove
 127  (`(ZIP [] [] = []) /\
 128    (ZIP (CONS h1 t1) (CONS h2 t2) = CONS (h1,h2) (ZIP t1 t2))`,
 129   REWRITE_TAC[ZIP_DEF; HD; TL]);;
 130
 131 (* ------------------------------------------------------------------------- *)
 132 (* Various trivial theorems.                                                 *)
 133 (* ------------------------------------------------------------------------- *)
 134
 135 let NOT_CONS_NIL = prove
 136  (`!(h:A) t. ~(CONS h t = [])`,
 137   REWRITE_TAC[distinctness "list"]);;
 138
 139 let LAST_CLAUSES = prove
 140  (`(LAST [h:A] = h) /\
 141    (LAST (CONS h (CONS k t)) = LAST (CONS k t))`,
 142   REWRITE_TAC[LAST; NOT_CONS_NIL]);;
 143
 144 let APPEND_NIL = prove
 145  (`!l:A list. APPEND l [] = l`,
 146   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[APPEND]);;
 147
 148 let APPEND_ASSOC = prove
 149  (`!(l:A list) m n. APPEND l (APPEND m n) = APPEND (APPEND l m) n`,
 150   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[APPEND]);;
 151
 152 let REVERSE_APPEND = prove
 153  (`!(l:A list) m. REVERSE (APPEND l m) = APPEND (REVERSE m) (REVERSE l)`,
 154   LIST_INDUCT_TAC THEN
 155   ASM_REWRITE_TAC[APPEND; REVERSE; APPEND_NIL; APPEND_ASSOC]);;
 156
 157 let REVERSE_REVERSE = prove
 158  (`!l:A list. REVERSE(REVERSE l) = l`,
 159   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[REVERSE; REVERSE_APPEND; APPEND]);;
 160
 161 let CONS_11 = prove
 162  (`!(h1:A) h2 t1 t2. (CONS h1 t1 = CONS h2 t2) <=> (h1 = h2) /\ (t1 = t2)`,
 163   REWRITE_TAC[injectivity "list"]);;
 164
 165 let list_CASES = prove
 166  (`!l:(A)list. (l = []) \/ ?h t. l = CONS h t`,
 167   LIST_INDUCT_TAC THEN REWRITE_TAC[CONS_11; NOT_CONS_NIL] THEN
 168   MESON_TAC[]);;
 169
 170 let LENGTH_APPEND = prove
 171  (`!(l:A list) m. LENGTH(APPEND l m) = LENGTH l + LENGTH m`,
 172   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[APPEND; LENGTH; ADD_CLAUSES]);;
 173
 174 let MAP_APPEND = prove
 175  (`!f:A->B. !l1 l2. MAP f (APPEND l1 l2) = APPEND (MAP f l1) (MAP f l2)`,
 176   GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[MAP; APPEND]);;
 177
 178 let LENGTH_MAP = prove
 179  (`!l. !f:A->B. LENGTH (MAP f l) = LENGTH l`,
 180   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[MAP; LENGTH]);;
 181
 182 let LENGTH_EQ_NIL = prove
 183  (`!l:A list. (LENGTH l = 0) <=> (l = [])`,
 184   LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; NOT_CONS_NIL; NOT_SUC]);;
 185
 186 let LENGTH_EQ_CONS = prove
 187  (`!l n. (LENGTH l = SUC n) <=> ?h t. (l = CONS h t) /\ (LENGTH t = n)`,
 188   LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; NOT_SUC; NOT_CONS_NIL] THEN
 189   ASM_REWRITE_TAC[SUC_INJ; CONS_11] THEN MESON_TAC[]);;
 190
 191 let MAP_o = prove
 192  (`!f:A->B. !g:B->C. !l. MAP (g o f) l = MAP g (MAP f l)`,
 193   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
 194   ASM_REWRITE_TAC[MAP; o_THM]);;
 195
 196 let MAP_EQ = prove
 197  (`!f g l. ALL (\x. f x = g x) l ==> (MAP f l = MAP g l)`,
 198   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
 199   REWRITE_TAC[MAP; ALL] THEN ASM_MESON_TAC[]);;
 200
 201 let ALL_IMP = prove
 202  (`!P Q l. (!x. MEM x l /\ P x ==> Q x) /\ ALL P l ==> ALL Q l`,
 203   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
 204   REWRITE_TAC[MEM; ALL] THEN ASM_MESON_TAC[]);;
 205
 206 let NOT_EX = prove
 207  (`!P l. ~(EX P l) <=> ALL (\x. ~(P x)) l`,
 208   GEN_TAC THEN LIST_INDUCT_TAC THEN
 209   ASM_REWRITE_TAC[EX; ALL; DE_MORGAN_THM]);;
 210
 211 let NOT_ALL = prove
 212  (`!P l. ~(ALL P l) <=> EX (\x. ~(P x)) l`,
 213   GEN_TAC THEN LIST_INDUCT_TAC THEN
 214   ASM_REWRITE_TAC[EX; ALL; DE_MORGAN_THM]);;
 215
 216 let ALL_MAP = prove
 217  (`!P f l. ALL P (MAP f l) <=> ALL (P o f) l`,
 218   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
 219   ASM_REWRITE_TAC[ALL; MAP; o_THM]);;
 220
 221 let ALL_T = prove
 222  (`!l. ALL (\x. T) l`,
 223   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL]);;
 224
 225 let MAP_EQ_ALL2 = prove
 226  (`!l m. ALL2 (\x y. f x = f y) l m ==> (MAP f l = MAP f m)`,
 227   REPEAT LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[MAP; ALL2; CONS_11] THEN
 228   ASM_MESON_TAC[]);;
 229
 230 let ALL2_MAP = prove
 231  (`!P f l. ALL2 P (MAP f l) l <=> ALL (\a. P (f a) a) l`,
 232   GEN_TAC THEN GEN_TAC THEN
 233   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL2; MAP; ALL]);;
 234
 235 let MAP_EQ_DEGEN = prove
 236  (`!l f. ALL (\x. f(x) = x) l ==> (MAP f l = l)`,
 237   LIST_INDUCT_TAC THEN REWRITE_TAC[ALL; MAP; CONS_11] THEN
 238   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 239   FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 240
 241 let ALL2_AND_RIGHT = prove
 242  (`!l m P Q. ALL2 (\x y. P x /\ Q x y) l m <=> ALL P l /\ ALL2 Q l m`,
 243   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL; ALL2] THEN
 244   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL; ALL2] THEN
 245   REWRITE_TAC[CONJ_ACI]);;
 246
 247 let ITLIST_APPEND = prove
 248  (`!f a l1 l2. ITLIST f (APPEND l1 l2) a = ITLIST f l1 (ITLIST f l2 a)`,
 249   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
 250   ASM_REWRITE_TAC[ITLIST; APPEND]);;
 251
 252 let ITLIST_EXTRA = prove
 253  (`!l. ITLIST f (APPEND l [a]) b = ITLIST f l (f a b)`,
 254   REWRITE_TAC[ITLIST_APPEND; ITLIST]);;
 255
 256 let ALL_MP = prove
 257  (`!P Q l. ALL (\x. P x ==> Q x) l /\ ALL P l ==> ALL Q l`,
 258   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
 259   REWRITE_TAC[ALL] THEN ASM_MESON_TAC[]);;
 260
 261 let AND_ALL = prove
 262  (`!l. ALL P l /\ ALL Q l <=> ALL (\x. P x /\ Q x) l`,
 263   CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
 264   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL; CONJ_ACI]);;
 265
 266 let EX_IMP = prove
 267  (`!P Q l. (!x. MEM x l /\ P x ==> Q x) /\ EX P l ==> EX Q l`,
 268   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
 269   REWRITE_TAC[MEM; EX] THEN ASM_MESON_TAC[]);;
 270
 271 let ALL_MEM = prove
 272  (`!P l. (!x. MEM x l ==> P x) <=> ALL P l`,
 273   GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[ALL; MEM] THEN
 274   ASM_MESON_TAC[]);;
 275
 276 let LENGTH_REPLICATE = prove
 277  (`!n x. LENGTH(REPLICATE n x) = n`,
 278   INDUCT_TAC THEN ASM_REWRITE_TAC[LENGTH; REPLICATE]);;
 279
 280 let EX_MAP = prove
 281  (`!P f l. EX P (MAP f l) <=> EX (P o f) l`,
 282   GEN_TAC THEN GEN_TAC THEN
 283   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[MAP; EX; o_THM]);;
 284
 285 let EXISTS_EX = prove
 286  (`!P l. (?x. EX (P x) l) <=> EX (\s. ?x. P x s) l`,
 287   GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[EX] THEN
 288   ASM_MESON_TAC[]);;
 289
 290 let FORALL_ALL = prove
 291  (`!P l. (!x. ALL (P x) l) <=> ALL (\s. !x. P x s) l`,
 292   GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL] THEN
 293   ASM_MESON_TAC[]);;
 294
 295 let MEM_APPEND = prove
 296  (`!x l1 l2. MEM x (APPEND l1 l2) <=> MEM x l1 \/ MEM x l2`,
 297   GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[MEM; APPEND; DISJ_ACI]);;
 298
 299 let MEM_MAP = prove
 300  (`!f y l. MEM y (MAP f l) <=> ?x. MEM x l /\ (y = f x)`,
 301   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
 302   ASM_REWRITE_TAC[MEM; MAP] THEN MESON_TAC[]);;
 303
 304 let FILTER_APPEND = prove
 305  (`!P l1 l2. FILTER P (APPEND l1 l2) = APPEND (FILTER P l1) (FILTER P l2)`,
 306   GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[FILTER; APPEND] THEN
 307   GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[APPEND]);;
 308
 309 let FILTER_MAP = prove
 310  (`!P f l. FILTER P (MAP f l) = MAP f (FILTER (P o f) l)`,
 311   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
 312   ASM_REWRITE_TAC[MAP; FILTER; o_THM] THEN COND_CASES_TAC THEN
 313   REWRITE_TAC[MAP]);;
 314
 315 let MEM_FILTER = prove
 316  (`!P l x. MEM x (FILTER P l) <=> P x /\ MEM x l`,
 317   GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[MEM; FILTER] THEN
 318   GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[MEM] THEN
 319   ASM_MESON_TAC[]);;
 320
 321 let EX_MEM = prove
 322  (`!P l. (?x. P x /\ MEM x l) <=> EX P l`,
 323   GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[EX; MEM] THEN
 324   ASM_MESON_TAC[]);;
 325
 326 let MAP_FST_ZIP = prove
 327  (`!l1 l2. (LENGTH l1 = LENGTH l2) ==> (MAP FST (ZIP l1 l2) = l1)`,
 328   LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN
 329   ASM_SIMP_TAC[LENGTH; SUC_INJ; MAP; FST; ZIP; NOT_SUC]);;
 330
 331 let MAP_SND_ZIP = prove
 332  (`!l1 l2. (LENGTH l1 = LENGTH l2) ==> (MAP SND (ZIP l1 l2) = l2)`,
 333   LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN
 334   ASM_SIMP_TAC[LENGTH; SUC_INJ; MAP; FST; ZIP; NOT_SUC]);;
 335
 336 let MEM_ASSOC = prove
 337  (`!l x. MEM (x,ASSOC x l) l <=> MEM x (MAP FST l)`,
 338   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[MEM; MAP; ASSOC] THEN
 339   GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 340   ASM_MESON_TAC[PAIR; FST]);;
 341
 342 let ALL_APPEND = prove
 343  (`!P l1 l2. ALL P (APPEND l1 l2) <=> ALL P l1 /\ ALL P l2`,
 344   GEN_TAC THEN LIST_INDUCT_TAC THEN
 345   ASM_REWRITE_TAC[ALL; APPEND; GSYM CONJ_ASSOC]);;
 346
 347 let MEM_EL = prove
 348  (`!l n. n < LENGTH l ==> MEM (EL n l) l`,
 349   LIST_INDUCT_TAC THEN REWRITE_TAC[MEM; CONJUNCT1 LT; LENGTH] THEN
 350   INDUCT_TAC THEN ASM_SIMP_TAC[EL; HD; LT_SUC; TL]);;
 351
 352 let MEM_EXISTS_EL = prove
 353  (`!l x. MEM x l <=> ?i. i < LENGTH l /\ x = EL i l`,
 354   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[LENGTH; EL; MEM; CONJUNCT1 LT] THEN
 355   GEN_TAC THEN GEN_REWRITE_TAC RAND_CONV
 356    [MESON[num_CASES] `(?i. P i) <=> P 0 \/ (?i. P(SUC i))`] THEN
 357   REWRITE_TAC[LT_SUC; LT_0; EL; HD; TL]);;
 358
 359 let ALL_EL = prove
 360  (`!P l. (!i. i < LENGTH l ==> P (EL i l)) <=> ALL P l`,
 361   REWRITE_TAC[GSYM ALL_MEM; MEM_EXISTS_EL] THEN MESON_TAC[]);;
 362
 363 let ALL2_MAP2 = prove
 364  (`!l m. ALL2 P (MAP f l) (MAP g m) = ALL2 (\x y. P (f x) (g y)) l m`,
 365   LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL2; MAP]);;
 366
 367 let AND_ALL2 = prove
 368  (`!P Q l m. ALL2 P l m /\ ALL2 Q l m <=> ALL2 (\x y. P x y /\ Q x y) l m`,
 369   GEN_TAC THEN GEN_TAC THEN CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
 370   LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL2] THEN
 371   REWRITE_TAC[CONJ_ACI]);;
 372
 373 let ALL2_ALL = prove
 374  (`!P l. ALL2 P l l <=> ALL (\x. P x x) l`,
 375   GEN_TAC THEN LIST_INDUCT_TAC THEN
 376   ASM_REWRITE_TAC[ALL2; ALL]);;
 377
 378 let APPEND_EQ_NIL = prove
 379  (`!l m. (APPEND l m = []) <=> (l = []) /\ (m = [])`,
 380   REWRITE_TAC[GSYM LENGTH_EQ_NIL; LENGTH_APPEND; ADD_EQ_0]);;
 381
 382 let LENGTH_MAP2 = prove
 383  (`!f l m. (LENGTH l = LENGTH m) ==> (LENGTH(MAP2 f l m) = LENGTH m)`,
 384   GEN_TAC THEN LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN
 385   ASM_SIMP_TAC[LENGTH; NOT_CONS_NIL; NOT_SUC; MAP2; SUC_INJ]);;
 386
 387 let MAP_EQ_NIL  = prove
 388  (`!f l. MAP f l = [] <=> l = []`,
 389   GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[MAP; NOT_CONS_NIL]);;
 390
 391 let INJECTIVE_MAP = prove
 392  (`!f:A->B. (!l m. MAP f l = MAP f m ==> l = m) <=>
 393             (!x y. f x = f y ==> x = y)`,
 394   GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
 395    [MAP_EVERY X_GEN_TAC [`x:A`; `y:A`] THEN DISCH_TAC THEN
 396     FIRST_X_ASSUM(MP_TAC o SPECL [`[x:A]`; `[y:A]`]) THEN
 397     ASM_REWRITE_TAC[MAP; CONS_11];
 398     REPEAT LIST_INDUCT_TAC THEN ASM_SIMP_TAC[MAP; NOT_CONS_NIL; CONS_11] THEN
 399     ASM_MESON_TAC[]]);;
 400
 401 let SURJECTIVE_MAP = prove
 402  (`!f:A->B. (!m. ?l. MAP f l = m) <=> (!y. ?x. f x = y)`,
 403   GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
 404    [X_GEN_TAC `y:B` THEN FIRST_X_ASSUM(MP_TAC o SPEC `[y:B]`) THEN
 405     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 406     LIST_INDUCT_TAC THEN REWRITE_TAC[MAP; CONS_11; NOT_CONS_NIL; MAP_EQ_NIL];
 407     MATCH_MP_TAC list_INDUCT] THEN
 408   ASM_MESON_TAC[MAP]);;
 409
 410 let MAP_ID = prove
 411  (`!l. MAP (\x. x) l = l`,
 412   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[MAP]);;
 413
 414 let MAP_I = prove
 415  (`MAP I = I`,
 416   REWRITE_TAC[FUN_EQ_THM; I_DEF; MAP_ID]);;
 417
 418 let APPEND_BUTLAST_LAST = prove
 419  (`!l. ~(l = []) ==> APPEND (BUTLAST l) [LAST l] = l`,
 420   LIST_INDUCT_TAC THEN REWRITE_TAC[LAST; BUTLAST; NOT_CONS_NIL] THEN
 421   COND_CASES_TAC THEN ASM_SIMP_TAC[APPEND]);;
 422
 423 let LAST_APPEND = prove
 424  (`!p q. LAST(APPEND p q) = if q = [] then LAST p else LAST q`,
 425   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[APPEND; LAST; APPEND_EQ_NIL] THEN
 426   MESON_TAC[]);;
 427
 428 let LENGTH_TL = prove
 429  (`!l. ~(l = []) ==> LENGTH(TL l) = LENGTH l - 1`,
 430   LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; TL; ARITH; SUC_SUB1]);;
 431
 432 let EL_APPEND = prove
 433  (`!k l m. EL k (APPEND l m) = if k < LENGTH l then EL k l
 434                                else EL (k - LENGTH l) m`,
 435   INDUCT_TAC THEN REWRITE_TAC[EL] THEN
 436   LIST_INDUCT_TAC THEN
 437   REWRITE_TAC[HD; APPEND; LENGTH; SUB_0; EL; LT_0; CONJUNCT1 LT] THEN
 438   ASM_REWRITE_TAC[TL; LT_SUC; SUB_SUC]);;
 439
 440 let EL_TL = prove
 441  (`!n. EL n (TL l) = EL (n + 1) l`,
 442   REWRITE_TAC[GSYM ADD1; EL]);;
 443
 444 let EL_CONS = prove
 445  (`!n h t. EL n (CONS h t) = if n = 0 then h else EL (n - 1) t`,
 446   INDUCT_TAC THEN REWRITE_TAC[EL; HD; TL; NOT_SUC; SUC_SUB1]);;
 447
 448 let LAST_EL = prove
 449  (`!l. ~(l = []) ==> LAST l = EL (LENGTH l - 1) l`,
 450   LIST_INDUCT_TAC THEN REWRITE_TAC[LAST; LENGTH; SUC_SUB1] THEN
 451   DISCH_TAC THEN COND_CASES_TAC THEN
 452   ASM_SIMP_TAC[LENGTH; EL; HD; EL_CONS; LENGTH_EQ_NIL]);;
 453
 454 let HD_APPEND = prove
 455  (`!l m:A list. HD(APPEND l m) = if l = [] then HD m else HD l`,
 456   LIST_INDUCT_TAC THEN REWRITE_TAC[HD; APPEND; NOT_CONS_NIL]);;
 457
 458 let CONS_HD_TL = prove
 459  (`!l. ~(l = []) ==> l = CONS (HD l) (TL l)`,
 460   LIST_INDUCT_TAC THEN REWRITE_TAC[NOT_CONS_NIL;HD;TL]);;
 461
 462 let EL_MAP = prove
 463  (`!f n l. n < LENGTH l ==> EL n (MAP f l) = f(EL n l)`,
 464   GEN_TAC THEN INDUCT_TAC THEN LIST_INDUCT_TAC THEN
 465   ASM_REWRITE_TAC[LENGTH; CONJUNCT1 LT; LT_0; EL; HD; TL; MAP; LT_SUC]);;
 466
 467 let MAP_REVERSE = prove
 468  (`!f l. REVERSE(MAP f l) = MAP f (REVERSE l)`,
 469   GEN_TAC THEN LIST_INDUCT_TAC THEN
 470   ASM_REWRITE_TAC[MAP; REVERSE; MAP_APPEND]);;
 471
 472 let ALL_FILTER = prove
 473  (`!P Q l:A list. ALL P (FILTER Q l) <=> ALL (\x. Q x ==> P x) l`,
 474   GEN_TAC THEN GEN_TAC THEN
 475   LIST_INDUCT_TAC THEN REWRITE_TAC[ALL; FILTER] THEN
 476   COND_CASES_TAC THEN ASM_REWRITE_TAC[ALL]);;
 477
 478 let APPEND_SING = prove
 479  (`!h t. APPEND [h] t = CONS h t`,
 480   REWRITE_TAC[APPEND]);;
 481
 482 let MEM_APPEND_DECOMPOSE_LEFT = prove
 483  (`!x:A l. MEM x l <=> ?l1 l2. ~(MEM x l1) /\ l = APPEND l1 (CONS x l2)`,
 484   REWRITE_TAC[TAUT `(p <=> q) <=> (p ==> q) /\ (q ==> p)`] THEN
 485   SIMP_TAC[LEFT_IMP_EXISTS_THM; MEM_APPEND; MEM] THEN X_GEN_TAC `x:A` THEN
 486   MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[MEM] THEN
 487   MAP_EVERY X_GEN_TAC [`y:A`; `l:A list`] THEN
 488   ASM_CASES_TAC `x:A = y` THEN ASM_MESON_TAC[MEM; APPEND]);;
 489
 490 let MEM_APPEND_DECOMPOSE = prove
 491  (`!x:A l. MEM x l <=> ?l1 l2. l = APPEND l1 (CONS x l2)`,
 492   REWRITE_TAC[TAUT `(p <=> q) <=> (p ==> q) /\ (q ==> p)`] THEN
 493   SIMP_TAC[LEFT_IMP_EXISTS_THM; MEM_APPEND; MEM] THEN
 494   ONCE_REWRITE_TAC[MEM_APPEND_DECOMPOSE_LEFT] THEN MESON_TAC[]);;
 495
 496 (* ------------------------------------------------------------------------- *)
 497 (* Syntax.                                                                   *)
 498 (* ------------------------------------------------------------------------- *)
 499
 500 let mk_cons h t =
 501   try let cons = mk_const("CONS",[type_of h,aty]) in
 502       mk_comb(mk_comb(cons,h),t)
 503   with Failure _ -> failwith "mk_cons";;
 504
 505 let mk_list (tms,ty) =
 506   try let nil = mk_const("NIL",[ty,aty]) in
 507       if tms = [] then nil else
 508       let cons = mk_const("CONS",[ty,aty]) in
 509       itlist (mk_binop cons) tms nil
 510   with Failure _ -> failwith "mk_list";;
 511
 512 let mk_flist tms =
 513   try mk_list(tms,type_of(hd tms))
 514   with Failure _ -> failwith "mk_flist";;
 515
 516 (* ------------------------------------------------------------------------- *)
 517 (* Extra monotonicity theorems for inductive definitions.                    *)
 518 (* ------------------------------------------------------------------------- *)
 519
 520 let MONO_ALL = prove
 521  (`(!x:A. P x ==> Q x) ==> ALL P l ==> ALL Q l`,
 522   DISCH_TAC THEN SPEC_TAC(`l:A list`,`l:A list`) THEN
 523   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL] THEN ASM_MESON_TAC[]);;
 524
 525 let MONO_ALL2 = prove
 526  (`(!x y. (P:A->B->bool) x y ==> Q x y) ==> ALL2 P l l' ==> ALL2 Q l l'`,
 527   DISCH_TAC THEN
 528   SPEC_TAC(`l':B list`,`l':B list`) THEN SPEC_TAC(`l:A list`,`l:A list`) THEN
 529   LIST_INDUCT_TAC THEN REWRITE_TAC[ALL2_DEF] THEN
 530   GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN ASM_MESON_TAC[]);;
 531
 532 monotonicity_theorems := [MONO_ALL; MONO_ALL2] @ !monotonicity_theorems;;
 533
 534 (* ------------------------------------------------------------------------- *)
 535 (* Apply a conversion down a list.                                           *)
 536 (* ------------------------------------------------------------------------- *)
 537
 538 let rec LIST_CONV conv tm =
 539   if is_cons tm then
 540     COMB2_CONV (RAND_CONV conv) (LIST_CONV conv) tm
 541   else if fst(dest_const tm) = "NIL" then REFL tm
 542   else failwith "LIST_CONV";;
 543
 544 (* ------------------------------------------------------------------------- *)
 545 (* Type of characters, like the HOL88 "ascii" type.                          *)
 546 (* ------------------------------------------------------------------------- *)
 547
 548 let char_INDUCT,char_RECURSION = define_type
 549  "char = ASCII bool bool bool bool bool bool bool bool";;
 550
 551 new_type_abbrev("string",`:char list`);;