text_formalization/leg/basics.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Author: Thomas C. Hales                                                    *)
   5 (* Date: 2013-02-11 *)
   6 (* ========================================================================== *)
   7
   8 (* General lemmas *)
   9
  10
  11
  12
  13 module Basics = struct
  14
  15   open Hales_tactic;;
  16
  17 (* SECTION: LOGIC *)
  18
  19 let BETA_ORDERED_PAIR_THM = prove_by_refinement(
  20  `!(g:A->B->C) x.
  21     ((\ ( u, v). g u v) x = g (FST x) (SND x))`,
  22   (* {{{ proof *)
  23   [
  24   REPEAT GEN_TAC;
  25   INTRO_TAC (GSYM PAIR) [`x`];
  26   DISCH_THEN SUBST1_TAC;
  27   BY(REWRITE_TAC[GABS_DEF;GEQ_DEF])
  28   ]);;
  29   (* }}} *)
  30
  31 (* SECTION: SETS *)
  32
  33 let SURJ_IMAGE = prove_by_refinement(
  34   `!(f:A->B) a b. SURJ f a b ==> (b = (IMAGE f a))`,
  35 (* {{{ proof *)
  36   [
  37   REWRITE_TAC[SURJ;IMAGE];
  38   REPEAT WEAKER_STRIP_TAC;
  39   REWRITE_TAC[EXTENSION;IN_ELIM_THM];
  40   BY(ASM_MESON_TAC[])
  41  ]
  42 (* }}} *)
  43 );;
  44
  45 let SURJ_FINITE = prove_by_refinement(
  46   `!a b (f:A->B). FINITE a /\ (SURJ f a b) ==> FINITE b`,
  47 (* {{{ *)
  48   [
  49   ASM_MESON_TAC[SURJ_IMAGE;FINITE_IMAGE]
  50   ]);;
  51 (* }}} *)
  52
  53 let BIJ_INVERSE = prove_by_refinement(
  54   `!a b (f:A->B). (SURJ f a b) ==> (?(g:B->A). (INJ g b a))`,
  55 (* {{{ proof *)
  56   [
  57   REPEAT WEAKER_STRIP_TAC;
  58   TYPIFY `!y. ?u. ((y IN b) ==> ((u IN a) /\ ((f:A->B) u = y)))` (C SUBGOAL_THEN ASSUME_TAC);
  59     BY(ASM_MESON_TAC[SURJ]);
  60   FIRST_X_ASSUM (MP_TAC o (REWRITE_RULE[SKOLEM_THM]));
  61   REPEAT WEAKER_STRIP_TAC;
  62   EXISTS_TAC `u:B->A`;
  63   REWRITE_TAC[INJ];
  64   BY(ASM_MESON_TAC[])
  65   ]
  66 (* }}} *)
  67 );;
  68
  69 let BIJ_SUM = prove_by_refinement(
  70   `!(A:A->bool) (B:B->bool) f ab.
  71     BIJ ab A B ==> (sum A (f o ab) = sum B f)`,
  72   (* {{{ proof *)
  73   [
  74   REWRITE_TAC[BIJ;INJ];
  75   BY(ASM_MESON_TAC[ SUM_IMAGE ; SURJ_IMAGE ])
  76   ]);;
  77   (* }}} *)
  78
  79 (* SECTION: LISTS *)
  80
  81 let EL_EXPLICIT = prove_by_refinement(
  82   `!h t. EL 0 (CONS (h:a) t) = h /\
  83    EL 1 (CONS h t) = EL 0 t /\
  84    EL 2 (CONS h t) = EL 1 t /\
  85    EL 3 (CONS h t) = EL 2 t /\
  86    EL 4 (CONS h t) = EL 3 t /\
  87    EL 5 (CONS h t) = EL 4 t /\
  88    EL 6 (CONS h t) = EL 5 t`,
  89   (* {{{ proof *)
  90   [
  91   BY(REWRITE_TAC[EL;HD;TL;arith `6 = SUC 5 /\ 5 = SUC 4 /\ 4 = SUC 3 /\ 3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`])
  92   ]);;
  93   (* }}} *)
  94
  95 let LENGTH1 = prove_by_refinement(
  96   `!ul:(A) list. LENGTH ul = 1 ==> ul = [EL 0 ul]`,
  97   (* {{{ proof *)
  98   [
  99   REWRITE_TAC[LENGTH_EQ_CONS;arith `1 = SUC 0`;LENGTH_EQ_NIL];
 100   REPEAT WEAK_STRIP_TAC;
 101   BY(ASM_REWRITE_TAC[EL;HD])
 102   ]);;
 103   (* }}} *)
 104
 105 let LENGTH2 = prove_by_refinement(
 106   `!ul:(A) list. LENGTH ul = 2 ==> ul = [EL 0 ul;EL 1 ul]`,
 107   (* {{{ proof *)
 108   [
 109   REWRITE_TAC[LENGTH_EQ_CONS;arith `2 = SUC 1`];
 110   REPEAT WEAK_STRIP_TAC;
 111   ASM_REWRITE_TAC[];
 112   FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH1));
 113   BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;TL])
 114   ]);;
 115   (* }}} *)
 116
 117 let LENGTH3 = prove_by_refinement(
 118   `!(ul:(A)list). LENGTH ul = 3 ==> ul = [EL 0 ul; EL 1 ul; EL 2 ul]`,
 119   (* {{{ proof *)
 120   [
 121   REWRITE_TAC[LENGTH_EQ_CONS;arith `3 = SUC 2`];
 122   REPEAT WEAK_STRIP_TAC;
 123   ASM_REWRITE_TAC[];
 124   FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH2));
 125   BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;arith `2 = SUC 1`;TL])
 126   ]);;
 127   (* }}} *)
 128
 129 let LENGTH4 = prove_by_refinement(
 130   `!(ul:(A)list). LENGTH ul = 4 ==> ul = [EL 0 ul; EL 1 ul; EL 2 ul; EL 3 ul]`,
 131   (* {{{ proof *)
 132   [
 133   REWRITE_TAC[LENGTH_EQ_CONS;arith `4 = SUC 3`];
 134   REPEAT WEAK_STRIP_TAC;
 135   ASM_REWRITE_TAC[];
 136   FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH3));
 137   BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;arith `2 = SUC 1`;arith `3 = SUC 2`;TL])
 138   ]);;
 139   (* }}} *)
 140
 141 let set_of_list2_explicit = prove_by_refinement(
 142   `!(a:A) b. set_of_list [a;b] = {a,b}`,
 143   (* {{{ proof *)
 144   [
 145     BY(REWRITE_TAC[set_of_list])
 146   ]);;
 147   (* }}} *)
 148
 149 let set_of_list2 = prove_by_refinement(
 150   `!(ul:(A) list). LENGTH ul = 2 ==> set_of_list ul = {EL 0 ul, EL 1 ul}`,
 151   (* {{{ proof *)
 152   [
 153   REPEAT WEAK_STRIP_TAC;
 154   FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH2));
 155   ABBREV_TAC `a:A = EL 0 ul`;
 156   ABBREV_TAC `b:A = EL 1 ul`;
 157   DISCH_THEN SUBST1_TAC;
 158   BY(REWRITE_TAC[set_of_list])
 159   ]);;
 160   (* }}} *)
 161
 162 let set_of_list3_explicit = prove_by_refinement(
 163   `!(a:A) b c. set_of_list [a;b;c] = {a,b,c}`,
 164   (* {{{ proof *)
 165   [
 166     BY(REWRITE_TAC[set_of_list])
 167   ]);;
 168   (* }}} *)
 169
 170 let set_of_list3 = prove_by_refinement(
 171   `!(ul:(A) list). LENGTH ul = 3 ==> set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul}`,
 172   (* {{{ proof *)
 173   [
 174   REPEAT WEAK_STRIP_TAC;
 175   FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH3));
 176   ABBREV_TAC `a:A = EL 0 ul`;
 177   ABBREV_TAC `b:A = EL 1 ul`;
 178   ABBREV_TAC `c:A = EL 2 ul`;
 179   DISCH_THEN SUBST1_TAC;
 180   BY(REWRITE_TAC[set_of_list])
 181   ]);;
 182   (* }}} *)
 183
 184 let set_of_list4_explicit = prove_by_refinement(
 185   `!(a:A) b c d. set_of_list [a;b;c;d] = {a,b,c,d}`,
 186   (* {{{ proof *)
 187   [
 188     BY(REWRITE_TAC[set_of_list])
 189   ]);;
 190   (* }}} *)
 191
 192 let set_of_list4 = prove_by_refinement(
 193   `!(ul:(A) list). LENGTH ul = 4 ==> set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul}`,
 194   (* {{{ proof *)
 195   [
 196   REPEAT WEAK_STRIP_TAC;
 197   FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH4));
 198   ABBREV_TAC `a:A = EL 0 ul`;
 199   ABBREV_TAC `b:A = EL 1 ul`;
 200   ABBREV_TAC `c:A = EL 2 ul`;
 201   ABBREV_TAC `d:A = EL 3 ul`;
 202   DISCH_THEN SUBST1_TAC;
 203   BY(REWRITE_TAC[set_of_list])
 204   ]);;
 205   (* }}} *)
 206
 207 let INITIAL_SUBLIST_NIL = prove(`!(zl:(A)list). initial_sublist [] zl`,
 208    REWRITE_TAC[Sphere.INITIAL_SUBLIST; APPEND] THEN MESON_TAC[]);;
 209
 210 let INITIAL_SUBLIST_CONS = prove_by_refinement(
 211   `!(a:A) b x y. initial_sublist (CONS a x) (CONS b y) <=> (a = b) /\ initial_sublist x y`,
 212   (* {{{ proof *)
 213   [
 214   REWRITE_TAC[Sphere.INITIAL_SUBLIST];
 215   REPEAT WEAKER_STRIP_TAC;
 216   REWRITE_TAC[APPEND];
 217   REWRITE_TAC[CONS_11];
 218   BY(MESON_TAC[])
 219   ]);;
 220   (* }}} *)
 221
 222 let INITIAL_SUBLIST_TRANS = prove(`!(xl:(A)list) yl zl. initial_sublist xl yl /\ initial_sublist yl zl ==> initial_sublist xl zl`,
 223    REWRITE_TAC[Sphere.INITIAL_SUBLIST] THEN
 224      REPEAT STRIP_TAC THEN
 225      ASM_MESON_TAC[APPEND_ASSOC]);;
 226
 227
 228 (* truncate simplex *)
 229
 230
 231 let BUTLAST_INITIAL_SUBLIST = prove(`!ul:(A)list. 1 <= LENGTH ul ==> initial_sublist (BUTLAST ul) ul`,
 232    REPEAT STRIP_TAC THEN
 233      MP_TAC (ISPEC `ul:(A)list` APPEND_BUTLAST_LAST) THEN
 234      REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
 235      ASM_SIMP_TAC[ARITH_RULE `1 <= a ==> ~(a = 0)`] THEN
 236      REWRITE_TAC[Sphere.INITIAL_SUBLIST] THEN
 237      DISCH_TAC THEN
 238      EXISTS_TAC `[LAST ul:A]` THEN
 239      ASM_REWRITE_TAC[]);;
 240
 241 let LENGTH_BUTLAST = prove(`!ul:(A)list. 1 <= LENGTH ul ==> LENGTH (BUTLAST ul) = LENGTH ul - 1`,
 242    REPEAT STRIP_TAC THEN
 243      MP_TAC (ISPEC `ul:(A)list` APPEND_BUTLAST_LAST) THEN
 244      REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
 245      ASM_SIMP_TAC[ARITH_RULE `1 <= a ==> ~(a = 0)`] THEN
 246      DISCH_THEN (fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [GSYM th]) THEN
 247      REWRITE_TAC[LENGTH_APPEND; LENGTH] THEN
 248      ARITH_TAC);;
 249
 250 let LENGTH_IMP_CONS = prove(`!l:(A)list. 1 <= LENGTH l ==> ?h t. l = CONS h t`,
 251    REPEAT STRIP_TAC THEN
 252      MP_TAC (ISPECL [`l:(A)list`; `PRE (LENGTH (l:(A)list))`] LENGTH_EQ_CONS) THEN
 253      ASM_SIMP_TAC[ARITH_RULE `1 <= n ==> SUC (PRE n) = n`] THEN
 254      STRIP_TAC THEN
 255      MAP_EVERY EXISTS_TAC [`h:A`; `t:(A)list`] THEN
 256      ASM_REWRITE_TAC[]);;
 257
 258 let INITIAL_SUBLIST_REFL = prove(`!ul. initial_sublist ul ul`, MESON_TAC[Sphere.INITIAL_SUBLIST; APPEND_NIL]);;
 259
 260 let TRUNCATE_SIMPLEX_EXISTS = prove_by_refinement(
 261   `!k ul:(A)list.  k+1 <= LENGTH ul ==> (?vl.
 262     LENGTH vl = k+1 /\ initial_sublist vl ul)`,
 263   (* {{{ proof *)
 264   [
 265   TYPIFY `!r k (ul:(A)list). k + 1 <= LENGTH ul /\ LENGTH ul = r ==> (?vl. LENGTH vl = k + 1 /\ initial_sublist vl ul)` ENOUGH_TO_SHOW_TAC;
 266     BY(MESON_TAC[]);
 267   INDUCT_TAC;
 268     REPEAT WEAKER_STRIP_TAC;
 269     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 270   REPEAT WEAKER_STRIP_TAC;
 271   TYPIFY `SUC r = k + 1` ASM_CASES_TAC;
 272     TYPIFY `ul` EXISTS_TAC;
 273     REWRITE_TAC[INITIAL_SUBLIST_REFL];
 274     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 275   FIRST_X_ASSUM (C INTRO_TAC [`k`;`BUTLAST ul`]);
 276   ANTS_TAC;
 277     INTRO_TAC LENGTH_BUTLAST [`ul`];
 278     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 279   REPEAT WEAKER_STRIP_TAC;
 280   TYPIFY `vl` EXISTS_TAC;
 281   ASM_REWRITE_TAC[];
 282   MATCH_MP_TAC INITIAL_SUBLIST_TRANS;
 283   TYPIFY `BUTLAST ul` EXISTS_TAC;
 284   ASM_REWRITE_TAC[];
 285   MATCH_MP_TAC BUTLAST_INITIAL_SUBLIST;
 286   BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
 287   ]);;
 288   (* }}} *)
 289
 290 let TRUNCATE_SIMPLEX_PROP = prove_by_refinement(
 291   `!k ul:(A)list. k + 1 <= LENGTH ul ==>
 292     LENGTH (truncate_simplex k ul) = k + 1 /\ initial_sublist (truncate_simplex k ul) ul`,
 293   (* {{{ proof *)
 294   [
 295   REPEAT WEAKER_STRIP_TAC;
 296   INTRO_TAC TRUNCATE_SIMPLEX_EXISTS [`k`;`ul`];
 297   ASM_REWRITE_TAC[];
 298   REPEAT WEAKER_STRIP_TAC;
 299   REWRITE_TAC[Sphere.TRUNCATE_SIMPLEX];
 300   SELECT_TAC THEN ASM_REWRITE_TAC[];
 301     BY(ASM_MESON_TAC[]);
 302   BY(ASM_MESON_TAC[])
 303   ]);;
 304   (* }}} *)
 305
 306 let LENGTH_TRUNCATE_SIMPLEX = prove_by_refinement(
 307   `!k ul. k + 1 <= LENGTH ul ==> LENGTH (truncate_simplex k ul) = k + 1`,
 308   (* {{{ proof *)
 309   [
 310     BY(ASM_MESON_TAC[TRUNCATE_SIMPLEX_PROP])
 311   ]);;
 312   (* }}} *)
 313
 314 let INITIAL_SUBLIST_OF_NIL = prove_by_refinement(
 315   `!ul:(A) list. initial_sublist ul [] <=> (ul = [])`,
 316   (* {{{ proof *)
 317   [
 318   REWRITE_TAC[Sphere.INITIAL_SUBLIST];
 319   BY(MESON_TAC[APPEND_EQ_NIL])
 320   ]);;
 321   (* }}} *)
 322
 323 let INITIAL_SUBLIST_INJ = prove_by_refinement(
 324   `!ul:(A) list vl wl. LENGTH ul = LENGTH vl /\ initial_sublist ul wl /\ initial_sublist vl wl ==>
 325     (ul = vl)`,
 326   (* {{{ proof *)
 327   [
 328   TYPIFY `!k (ul:(A) list) vl wl. k = LENGTH ul /\ k = LENGTH vl /\ initial_sublist ul wl /\ initial_sublist vl wl ==> (ul = vl)` ENOUGH_TO_SHOW_TAC;
 329     BY(MESON_TAC[]);
 330   INDUCT_TAC;
 331     BY(MESON_TAC[LENGTH_EQ_NIL]);
 332   REPEAT WEAKER_STRIP_TAC;
 333   INTRO_TAC LENGTH_IMP_CONS [`ul`];
 334   INTRO_TAC LENGTH_IMP_CONS [`vl`];
 335   ANTS_TAC;
 336     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 337   STRIP_TAC;
 338   ANTS_TAC;
 339     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 340   STRIP_TAC;
 341   TYPIFY `LENGTH wl = 0` ASM_CASES_TAC;
 342     BY(ASM_MESON_TAC[LENGTH_EQ_NIL;INITIAL_SUBLIST_OF_NIL;NOT_CONS_NIL]);
 343   INTRO_TAC LENGTH_IMP_CONS [`wl`];
 344   ANTS_TAC;
 345     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 346   REPEAT WEAKER_STRIP_TAC;
 347   ASM_REWRITE_TAC[CONS_11];
 348   PROOF_BY_CONTR_TAC;
 349   REPEAT (FIRST_X_ASSUM_ST `initial_sublist` MP_TAC);
 350   ASM_REWRITE_TAC[INITIAL_SUBLIST_CONS];
 351   REPEAT WEAKER_STRIP_TAC;
 352   FIRST_X_ASSUM (C INTRO_TAC [`t`;`t'`;`t''`]);
 353   ANTS_TAC;
 354     ASM_REWRITE_TAC[];
 355     REPEAT (FIRST_X_ASSUM_ST `LENGTH` MP_TAC);
 356     ASM_REWRITE_TAC[LENGTH;SUC_INJ];
 357     BY(MESON_TAC[]);
 358   DISCH_TAC;
 359   FIRST_X_ASSUM_ST `~` MP_TAC;
 360   BY(ASM_REWRITE_TAC[])
 361   ]);;
 362   (* }}} *)
 363
 364 let TRUNCATE_SIMPLEX_UNIQUE = prove_by_refinement(
 365   `!k ul:(A) list vl.  k+1 <= LENGTH ul /\ LENGTH vl = k+ 1 /\ initial_sublist vl ul ==>
 366       vl = truncate_simplex k ul`,
 367   (* {{{ proof *)
 368   [
 369     BY(ASM_MESON_TAC[INITIAL_SUBLIST_INJ;TRUNCATE_SIMPLEX_PROP])
 370   ]);;
 371   (* }}} *)
 372
 373 let INITIAL_SUBLIST_LENGTH_LE = prove_by_refinement(
 374  `!xl:(A)list zl. initial_sublist xl zl ==> LENGTH xl <= LENGTH zl`,
 375   (* {{{ proof *)
 376   [
 377   REWRITE_TAC[Sphere.INITIAL_SUBLIST];
 378   REPEAT WEAKER_STRIP_TAC;
 379   ASM_REWRITE_TAC[LENGTH_APPEND];
 380   BY(ARITH_TAC)
 381   ]);;
 382   (* }}} *)
 383
 384 let TRUNCATE_SIMPLEX_INITIAL_SUBLIST = prove_by_refinement(
 385   `!k (xl:(A)list) zl.
 386          truncate_simplex k zl = xl /\ k + 1 <= LENGTH zl <=>
 387          initial_sublist xl zl /\ LENGTH xl = k + 1`,
 388   (* {{{ proof *)
 389   [
 390   REPEAT WEAKER_STRIP_TAC;
 391   MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a = b)`);
 392   CONJ_TAC;
 393     BY(ASM_MESON_TAC[TRUNCATE_SIMPLEX_PROP]);
 394   REPEAT WEAKER_STRIP_TAC;
 395   INTRO_TAC TRUNCATE_SIMPLEX_PROP [`k`;`zl`];
 396   ANTS_TAC;
 397     BY(ASM_MESON_TAC[INITIAL_SUBLIST_LENGTH_LE]);
 398   REPEAT WEAKER_STRIP_TAC;
 399   TYPIFY `k + 1 <= LENGTH zl` (C SUBGOAL_THEN ASSUME_TAC);
 400     BY(ASM_MESON_TAC[INITIAL_SUBLIST_LENGTH_LE]);
 401   ASM_REWRITE_TAC[];
 402   MATCH_MP_TAC EQ_SYM;
 403   MATCH_MP_TAC TRUNCATE_SIMPLEX_UNIQUE;
 404   BY(ASM_MESON_TAC[])
 405   ]);;
 406   (* }}} *)
 407
 408 let TRUNCATE_SIMPLEX0 = prove_by_refinement(
 409   `!(x:A) y. truncate_simplex 0 (CONS x y) = [x]`,
 410   (* {{{ proof *)
 411   [
 412   REPEAT WEAKER_STRIP_TAC;
 413   INTRO_TAC TRUNCATE_SIMPLEX_INITIAL_SUBLIST [`0`;`[x]`;`(CONS x y)`];
 414   REWRITE_TAC[LENGTH (* _CONS *);INITIAL_SUBLIST_CONS;INITIAL_SUBLIST_NIL];
 415   BY(REWRITE_TAC[arith `SUC 0  = 0 + 1`;arith `0 + 1 <= SUC i`])
 416   ]);;
 417   (* }}} *)
 418
 419 let LENGTH_TRUNCATE_SIMPLEX = prove_by_refinement(
 420   `!k (ul:(A)list). SUC k <= LENGTH ul ==> LENGTH (truncate_simplex k ul) = SUC k`,
 421   (* {{{ proof *)
 422   [
 423   BY(ASM_MESON_TAC[LENGTH_TRUNCATE_SIMPLEX;arith `SUC k = k + 1`])
 424   ]);;
 425   (* }}} *)
 426
 427 let TRUNCATE_SIMPLEX_CONS = prove_by_refinement(
 428   `!(x:A) y k. SUC k <= LENGTH y ==> truncate_simplex (SUC k) (CONS x y) = CONS x  (truncate_simplex k y)`,
 429   (* {{{ proof *)
 430   [
 431   REPEAT WEAKER_STRIP_TAC;
 432   INTRO_TAC TRUNCATE_SIMPLEX_INITIAL_SUBLIST [`SUC k`;`CONS x (truncate_simplex k y)`;`(CONS x y)`];
 433   REWRITE_TAC[LENGTH (* _CONS *);INITIAL_SUBLIST_CONS];
 434   ASM_SIMP_TAC[arith `SUC k <= n ==> SUC k + 1 <= SUC n`];
 435   ASM_SIMP_TAC[ LENGTH_TRUNCATE_SIMPLEX];
 436   DISCH_THEN kill;
 437   REWRITE_TAC[arith `SUC (SUC k) = SUC k + 1`];
 438   INTRO_TAC TRUNCATE_SIMPLEX_INITIAL_SUBLIST [`k`;`truncate_simplex k y`;`y`];
 439   BY(ASM_SIMP_TAC[LENGTH_TRUNCATE_SIMPLEX;arith `k+1 = SUC k`])
 440   ]);;
 441   (* }}} *)
 442
 443 let TRUNCATE_SIMPLEX_EXPLICIT = prove_by_refinement(
 444   `!(x1:A) x2 x3 x4. truncate_simplex 3 [x1;x2;x3;x4] = [x1;x2;x3;x4] /\
 445     truncate_simplex 2 [x1;x2;x3;x4] = [x1;x2;x3] /\
 446     truncate_simplex 2 [x1;x2;x3] = [x1;x2;x3] /\
 447     truncate_simplex 1 [x1;x2;x3;x4] = [x1;x2] /\
 448     truncate_simplex 1 [x1;x2;x3] = [x1;x2] /\
 449     truncate_simplex 1 [x1;x2] = [x1;x2]`,
 450   (* {{{ proof *)
 451   [
 452   REPEAT WEAKER_STRIP_TAC;
 453   REWRITE_TAC[arith `3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`];
 454   REPEAT (GMATCH_SIMP_TAC TRUNCATE_SIMPLEX_CONS);
 455   REWRITE_TAC[LENGTH;TRUNCATE_SIMPLEX0];
 456   BY(ARITH_TAC)
 457   ]);;
 458   (* }}} *)
 459
 460 let ADD_C_UNIV = prove_by_refinement(
 461   `(:A) +_c (:B) = (:A+B)`,
 462   (* {{{ proof *)
 463   [
 464   REWRITE_TAC[add_c];
 465   REWRITE_TAC[EXTENSION;IN_UNION;IN_UNIV;IN_ELIM_THM];
 466   BY(MESON_TAC[sum_CASES])
 467   ]);;
 468   (* }}} *)
 469
 470 let SUM_HAS_SIZE = prove_by_refinement(
 471   `!a b. (:A) HAS_SIZE a /\ (:B) HAS_SIZE b ==>
 472     (:A+B) HAS_SIZE (a+b)`,
 473   (* {{{ proof *)
 474   [
 475   REWRITE_TAC[HAS_SIZE];
 476   REPEAT WEAKER_STRIP_TAC;
 477   REWRITE_TAC[GSYM ADD_C_UNIV];
 478   CONJ2_TAC;
 479     BY(ASM_MESON_TAC[CARD_ADD_C]);
 480   BY(ASM_MESON_TAC[CARD_ADD_FINITE])
 481   ]);;
 482   (* }}} *)
 483
 484 let DIMINDEX_4 = prove_by_refinement(
 485   `dimindex(:2 + 2) = 4`,
 486   (* {{{ proof *)
 487   [
 488   MATCH_MP_TAC DIMINDEX_UNIQUE;
 489   REWRITE_TAC[arith `4 = 2+ 2`];
 490   MATCH_MP_TAC SUM_HAS_SIZE;
 491   BY(REWRITE_TAC[HAS_SIZE_2])
 492   ]);;
 493   (* }}} *)
 494
 495 let DIMINDEX_5 = prove_by_refinement(
 496   `dimindex(:2 + 3) = 5`,
 497   (* {{{ proof *)
 498   [
 499   MATCH_MP_TAC DIMINDEX_UNIQUE;
 500   REWRITE_TAC[arith `5 = 2+ 3`];
 501   REPEAT (GMATCH_SIMP_TAC SUM_HAS_SIZE);
 502   BY(REWRITE_TAC[HAS_SIZE_2;HAS_SIZE_3])
 503   ]);;
 504   (* }}} *)
 505
 506 let DIMINDEX_6 = prove_by_refinement(
 507   `dimindex(:3 + 3) = 6`,
 508   (* {{{ proof *)
 509   [
 510   MATCH_MP_TAC DIMINDEX_UNIQUE;
 511   REWRITE_TAC[arith `6 = 3+ 3`];
 512   REPEAT (GMATCH_SIMP_TAC SUM_HAS_SIZE);
 513   BY(REWRITE_TAC[HAS_SIZE_2;HAS_SIZE_3])
 514   ]);;
 515   (* }}} *)
 516
 517
 518 end;;