Rqe/rol.ml

   1 (* ---------------------------------------------------------------------- *)
   2 (*  Util                                                                  *)
   3 (* ---------------------------------------------------------------------- *)
   4
   5 (* ---------------------------------------------------------------------- *)
   6 (*  Real Ordered Lists                                                    *)
   7 (* ---------------------------------------------------------------------- *)
   8
   9 let real_ordered_list = new_recursive_definition list_RECURSION
  10   `(real_ordered_list [] <=> T) /\
  11    (real_ordered_list (CONS h t) <=>
  12       real_ordered_list t /\
  13       ((t = []) \/ (h < HD t)))`;;
  14
  15 let ROL_EMPTY = EQT_ELIM (CONJUNCT1 real_ordered_list);;
  16
  17 let ROL_SING = prove_by_refinement(
  18   `!x. real_ordered_list [x]`,
  19 (* {{{ Proof *)
  20 [
  21   REWRITE_TAC[real_ordered_list];
  22 ]);;
  23 (* }}} *)
  24
  25 let ROL_TAIL = prove(
  26   `!l. ~(l = []) /\ real_ordered_list l ==> real_ordered_list (TL l)`,
  27 (* {{{ Proof *)
  28   LIST_INDUCT_TAC THEN
  29   MESON_TAC[real_ordered_list;TL];
  30 );;
  31 (* }}} *)
  32
  33 let EL_CONS = prove_by_refinement(
  34   `!l h n. EL n t = EL (SUC n) (CONS h t)`,
  35 (* {{{ Proof *)
  36 [
  37   MESON_TAC[TL;EL];
  38 ]);;
  39 (* }}} *)
  40
  41 let NOT_ROL = prove_by_refinement(
  42   `!l. ~(real_ordered_list l) ==> ?n. EL n l >= EL (SUC n) l`,
  43 (* {{{ Proof *)
  44
  45 [
  46   LIST_INDUCT_TAC;
  47   REWRITE_TAC[real_ordered_list];
  48   REWRITE_TAC[real_ordered_list;DE_MORGAN_THM];
  49   STRIP_TAC;
  50   POP_ASSUM (fun x -> POP_ASSUM (fun y -> MP_TAC (MATCH_MP y x)));
  51   STRIP_TAC;
  52   EXISTS_TAC `SUC n`;
  53   ASM_MESON_TAC[EL_CONS];
  54   EXISTS_TAC `0`;
  55   REWRITE_TAC[EL;HD;TL;real_ge];
  56   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  57 ]);;
  58
  59 (* }}} *)
  60
  61 let ROL_CONS = prove_by_refinement(
  62   `!h t. real_ordered_list (CONS h t) ==> real_ordered_list t`,
  63 (* {{{ Proof *)
  64 [
  65   REWRITE_TAC[real_ordered_list];
  66   REPEAT STRIP_TAC;
  67 ]);;
  68 (* }}} *)
  69
  70 let ROL_CONS_CONS = prove_by_refinement(
  71   `!h t. real_ordered_list (CONS h1 (CONS h2 t)) <=>
  72      real_ordered_list (CONS h2 t) /\ h1 < h2`,
  73 (* {{{ Proof *)
  74
  75 [
  76   REPEAT GEN_TAC;
  77   EQ_TAC;
  78   REWRITE_TAC[real_ordered_list];
  79   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[NOT_CONS_NIL;HD];
  80   ASM_MESON_TAC[NOT_CONS_NIL];
  81   ASM_MESON_TAC[HD];
  82   ASM_MESON_TAC[NOT_CONS_NIL];
  83   ASM_MESON_TAC[HD];
  84   REWRITE_TAC[real_ordered_list];
  85   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[NOT_CONS_NIL;HD];
  86 ]);;
  87
  88 (* }}} *)
  89
  90 let ROL_APPEND = prove_by_refinement(
  91   `!l1 l2. real_ordered_list (APPEND l1 l2) ==>
  92     real_ordered_list l1 /\ real_ordered_list l2`,
  93 (* {{{ Proof *)
  94
  95 [
  96   LIST_INDUCT_TAC;
  97   MESON_TAC[APPEND;real_ordered_list];
  98   GEN_TAC;
  99   REWRITE_TAC[APPEND];
 100   STRIP_TAC;
 101   CLAIM `real_ordered_list (APPEND t l2)`;
 102   ASM_MESON_TAC[ROL_CONS];
 103   STRIP_TAC;
 104   CLAIM `real_ordered_list t /\ real_ordered_list l2`;
 105   ASM_MESON_TAC[];
 106   STRIP_TAC;
 107   ASM_REWRITE_TAC[];
 108   CASES_ON `t = []`;
 109   ASM_MESON_TAC[real_ordered_list];
 110   POP_ASSUM MP_TAC;
 111   REWRITE_TAC[NOT_NIL];
 112   STRIP_TAC;
 113   ASM_REWRITE_TAC[ROL_CONS_CONS];
 114   CONJ_TAC;
 115   ASM_MESON_TAC[];
 116   LABEL_ALL_TAC;
 117   USE_THEN "Z-4" MP_TAC;
 118   POP_ASSUM SUBST1_TAC;
 119   REWRITE_TAC[APPEND];
 120   ASM_MESON_TAC[ROL_CONS_CONS];
 121 ]);;
 122
 123 (* }}} *)
 124
 125 let ROL_CONS_CONS_LT = prove_by_refinement(
 126   `!h1 h2 t. real_ordered_list (CONS h1 (CONS h2 t)) ==> h1 < h2`,
 127 (* {{{ Proof *)
 128 [
 129   REWRITE_TAC[real_ordered_list];
 130   REPEAT STRIP_TAC THEN
 131   ASM_MESON_TAC[NOT_CONS_NIL;HD];
 132 ]);;
 133 (* }}} *)
 134
 135 let ROL_INSERT_THM = prove_by_refinement(
 136   `!x l1 l2.
 137     real_ordered_list l1 /\ real_ordered_list l2 /\
 138     ~(l1 = []) /\ ~(l2 = []) /\ LAST l1 < x /\ x < HD l2 ==>
 139       real_ordered_list (APPEND l1 (CONS x l2))`,
 140 (* {{{ Proof *)
 141
 142 [
 143   GEN_TAC;
 144   LIST_INDUCT_TAC;
 145   REWRITE_TAC[APPEND];
 146   CASES_ON `t = []`;
 147   ASM_REWRITE_TAC[APPEND;LAST_SING;NOT_CONS_NIL];
 148   REPEAT STRIP_TAC;
 149   ASM_REWRITE_TAC[ROL_CONS_CONS;real_ordered_list];
 150   POP_ASSUM MP_TAC;
 151   REWRITE_TAC[NOT_NIL];
 152   STRIP_TAC;
 153   ASM_REWRITE_TAC[];
 154   REPEAT STRIP_TAC;
 155   CLAIM `real_ordered_list (APPEND t (CONS x l2))`;
 156   REWRITE_ASSUMS[TAUT `(p ==> q ==> r) <=> (p /\ q ==> r)`];
 157   FIRST_ASSUM MATCH_MP_TAC;
 158   REPEAT STRIP_TAC;
 159   ASM_MESON_TAC[ROL_CONS];
 160   FIRST_ASSUM MATCH_ACCEPT_TAC;
 161   ASM_MESON_TAC[NOT_CONS_NIL];
 162   ASM_MESON_TAC[NOT_CONS_NIL];
 163   ASM_MESON_TAC[LAST_CONS;NOT_CONS_NIL];
 164   FIRST_ASSUM MATCH_ACCEPT_TAC;
 165   ASM_REWRITE_TAC[];
 166   LABEL_ALL_TAC;
 167   USE_THEN "Z-3" (SUBST1_TAC o GSYM);
 168   REWRITE_TAC[APPEND];
 169   STRIP_TAC;
 170   REWRITE_TAC[ROL_CONS_CONS];
 171   STRIP_TAC;
 172   FIRST_ASSUM MATCH_ACCEPT_TAC;
 173   ASM_MESON_TAC[ROL_CONS_CONS];
 174 ]);;
 175
 176 (* }}} *)
 177
 178 let ROL_INSERT_FRONT_THM = prove_by_refinement(
 179   `!x l. real_ordered_list l /\ ~(l = []) /\ x < HD l ==>
 180     real_ordered_list (CONS x l)`,
 181 (* {{{ Proof *)
 182
 183 [
 184   REWRITE_TAC[NOT_NIL;AND_IMP_THM];
 185   REPEAT STRIP_TAC;
 186   ASM_REWRITE_TAC[];
 187   ASM_MESON_TAC[ROL_CONS_CONS;HD];
 188 ]);;
 189
 190 (* }}} *)
 191
 192 let ROL_CONS_CONS_DELETE = prove_by_refinement(
 193   `!h1 h2 t. real_ordered_list (CONS h1 (CONS h2 t)) ==>
 194      real_ordered_list (CONS h1 t)`,
 195 (* {{{ Proof *)
 196 [
 197   REWRITE_TAC[real_ordered_list];
 198   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
 199   ASM_MESON_TAC[NOT_CONS_NIL];
 200   REWRITE_ASSUMS[HD];
 201   ASM_MESON_TAC[REAL_LT_TRANS];
 202 ]);;
 203 (* }}} *)
 204
 205 let LAST_CONS_LT = prove_by_refinement(
 206   `!x t h. real_ordered_list (CONS h t) /\ LAST (CONS h t) < x ==> h < x`,
 207 (* {{{ Proof *)
 208
 209 [
 210   GEN_TAC;
 211   LIST_INDUCT_TAC;
 212   REWRITE_TAC[LAST];
 213   REPEAT STRIP_TAC;
 214   REPEAT STRIP_TAC;
 215   FIRST_ASSUM MATCH_MP_TAC;
 216   CONJ_TAC;
 217   ASM_MESON_TAC[ROL_CONS_CONS_DELETE];
 218   CASES_ON `t = []`;
 219   ASM_REWRITE_TAC[LAST];
 220   ASM_MESON_TAC[LAST;ROL_CONS_CONS;REAL_LT_TRANS];
 221   ASM_MESON_TAC[LAST_CONS;ROL_CONS_CONS_DELETE;LAST_CONS_CONS];
 222 ]);;
 223
 224 (* }}} *)
 225
 226 let ROL_INSERT_BACK_THM = prove_by_refinement(
 227   `!x l. real_ordered_list l /\ ~(l = []) /\ LAST l < x ==>
 228     real_ordered_list (APPEND l [x])`,
 229 (* {{{ Proof *)
 230
 231 [
 232   STRIP_TAC;
 233   LIST_INDUCT_TAC;
 234   REWRITE_TAC[APPEND;ROL_SING];
 235   LABEL_ALL_TAC;
 236   STRIP_TAC;
 237   CASES_ON `t = []`;
 238   ASM_REWRITE_TAC[APPEND;ROL_CONS_CONS;ROL_SING];
 239   ASM_MESON_TAC[LAST;COND_CLAUSES];
 240   PROVE_ASSUM_ANTECEDENT_TAC 0;
 241   REPEAT STRIP_TAC;
 242   ASM_MESON_TAC[ROL_CONS];
 243   ASM_MESON_TAC[];
 244   ASM_MESON_TAC[LAST_CONS];
 245   REWRITE_TAC[APPEND];
 246   REWRITE_TAC[real_ordered_list];
 247   REPEAT STRIP_TAC;
 248   FIRST_ASSUM MATCH_ACCEPT_TAC;
 249   DISJ2_TAC;
 250   REWRITE_ASSUMS[NOT_NIL];
 251   LABEL_ALL_TAC;
 252   USE_IASSUM 2 MP_TAC;
 253   STRIP_TAC;
 254   ASM_REWRITE_TAC[HD_APPEND];
 255   ASM_MESON_TAC[ROL_CONS_CONS];
 256 ]);;
 257
 258 (* }}} *)
 259
 260 (*
 261   CHOP_REAL_LIST 1 `[&1; &2; &3]` --> |- [&1; &2; &3] = APPEND [&1; &2] [&3]
 262   let n,l = 1,`[&1; &2; &3]`
 263 *)
 264 let CHOP_REAL_LIST n l =
 265   let l' = dest_list l in
 266   let l1',l2' = chop_list n l' in
 267   let l1,l2 = mk_list (l1',real_ty),mk_list (l2',real_ty) in
 268   let tm = mk_binop rappend l1 l2 in
 269     GSYM (REWRITE_CONV [APPEND] tm);;
 270
 271
 272 (*
 273   ROL_CHOP_LT 2
 274   let n = 1
 275 *)
 276 let ROL_CHOP_LT n thm =
 277   let thm' = funpow (n - 1) (MATCH_MP ROL_CONS) thm in
 278     CONJUNCT2 (PURE_REWRITE_RULE[ROL_CONS_CONS] thm');;
 279
 280 let t1 = prove_by_refinement(
 281   `real_ordered_list [&1; &2; &3; &4]`,
 282 [
 283   REWRITE_TAC[HD;real_ordered_list];
 284   REAL_ARITH_TAC;
 285 ]);;
 286
 287 (*
 288 ROL_CHOP_LIST 2 |- real_ordered_list [&1; &2; &3; &4] -->
 289                    |- real_ordered_list [&1; &2; &3],
 290                    |- real_ordered_list [&4],
 291                    |- &3 < &4
 292 let thm = ASSUME `real_ordered_list [&1; &2; &3; &4]`
 293 let n = 2
 294 ROL_CHOP_LIST 2 thm
 295 *)
 296 let ROL_CHOP_LIST n thm =
 297   let _,l = dest_comb (concl thm) in
 298   let lthm = CHOP_REAL_LIST n l in
 299   let thm' = REWRITE_RULE[lthm] thm in
 300   let thm'' = MATCH_MP ROL_APPEND thm' in
 301   let [lthm;rthm] = CONJUNCTS thm'' in
 302   let lt_thm = ROL_CHOP_LT n thm in
 303     lthm,rthm,lt_thm;;
 304
 305 (*
 306 rol_insert (|- x1 < x4 /\ x4 < x2)
 307            (|- real_ordered_list [x1; x2; x3]) -->
 308   (|- real_ordered_list [x1; x4; x2; x3]);
 309
 310 rol_insert (|- &2 < &5 /\ &5 < &6) (|- real_ordered_list [&1; &2; &6]) -->
 311   (|- real_ordered_list [&1; &2; &5; &6]);
 312
 313 rol_insert (|- x4 < x1)
 314            (|- real_ordered_list [x1; x2; x3]) -->
 315   (|- real_ordered_list [x4; x1; x2; x3]);
 316
 317 rol_insert (|- x1 < x4)
 318            (|- real_ordered_list [x1; x2; x3]) -->
 319   (|- real_ordered_list [x1; x2; x3; x4]);
 320 *)
 321
 322 let lem1 = prove(
 323   `!e x l. e < x /\ (LAST l = e) ==> LAST l < x`,
 324   MESON_TAC[]);;
 325
 326 let ROL_INSERT_MIDDLE place_thm rol_thm =
 327   let [pl1;pl2] = CONJUNCTS place_thm in
 328   let list = snd(dest_comb(concl rol_thm)) in
 329   let new_x,slot =
 330     let ltl,ltr = dest_conj (concl place_thm) in
 331     let x1,x4 = dest_binop rlt ltl in
 332     let _,x2 = dest_binop rlt ltr in
 333     let n = (index x1 (dest_list list)) + 1 in
 334       x4,n in
 335   let lthm,rthm,lt_thm = ROL_CHOP_LIST slot rol_thm in
 336   let llist = snd(dest_comb(concl lthm)) in
 337   let hllist = hd (dest_list llist) in
 338   let tllist = mk_rlist (tl (dest_list llist)) in
 339   let rlist = snd(dest_comb(concl rthm)) in
 340   let hrlist = hd (dest_list rlist) in
 341   let trlist = mk_rlist (tl (dest_list rlist)) in
 342   let gthm = REWRITE_RULE[AND_IMP_THM] ROL_INSERT_THM in
 343   let a1 = lthm in
 344   let a2 = rthm in
 345   let a3 = ISPECL [hllist;tllist] NOT_CONS_NIL in
 346   let a4 = ISPECL [hrlist;trlist] NOT_CONS_NIL in
 347   let l,r = dest_binop rlt (concl pl1) in
 348   let a5_aux = prove(mk_eq (mk_comb(rlast,llist),l),REWRITE_TAC[LAST;COND_CLAUSES;NOT_CONS_NIL]) in
 349   let a5 = MATCH_MPL [ISPECL [l;r;llist] (REWRITE_RULE[AND_IMP_THM] lem1);pl1;a5_aux] in
 350   let a6_aux = ISPECL [trlist;hrlist] (GEN_ALL HD) in
 351   let a6 = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV[GSYM a6_aux])) pl2 in
 352   let thm = MATCH_MPL [gthm;a1;a2;a3;a4;a5;a6] in
 353     REWRITE_RULE[APPEND] thm;;
 354
 355 (*
 356 ROL_INSERT_MIDDLE (ASSUME `x1 < x4 /\ x4 < x2`)
 357                       (ASSUME `real_ordered_list [x1; x2; x3]`);;
 358
 359 ROL_INSERT_MIDDLE (ASSUME `x1 < x6 /\ x6 < x2`)
 360                       (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`);;
 361
 362 ROL_INSERT_MIDDLE (ASSUME `x2 < x6 /\ x6 < x3`)
 363                       (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`);;
 364
 365 ROL_INSERT_MIDDLE (ASSUME `x4 < x6 /\ x6 < x5`)
 366                       (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`);;
 367
 368 ROL_INSERT_MIDDLE (ASSUME `x2 < x4 /\ x4 < x3`)
 369                       (ASSUME `real_ordered_list [x1; x2; x3]`);;
 370
 371 *)
 372
 373
 374 let ROL_INSERT_FRONT place_thm rol_thm =
 375   let _,rlist = dest_comb (concl rol_thm) in
 376   let h,t = hd (dest_list rlist),mk_rlist (tl (dest_list rlist)) in
 377   let imp_thm = ISPECL [h;t] (GSYM ROL_CONS_CONS) in
 378   let imp_thm' = REWRITE_RULE[AND_IMP_THM] (fst (EQ_IMP_RULE imp_thm)) in
 379     MATCH_MPL[imp_thm';rol_thm;place_thm];;
 380
 381 (*
 382 ROL_INSERT_FRONT (ASSUME `x4 < x1`)
 383                      (ASSUME `real_ordered_list [x1; x2; x3]`);;
 384 ROL_INSERT_FRONT (ASSUME `x4 < x1`)
 385                      (ASSUME `real_ordered_list [x1]`);;
 386 *)
 387
 388 let ROL_INSERT_BACK place_thm rol_thm =
 389   let _,rlist = dest_comb (concl rol_thm) in
 390   let rlist' = dest_list rlist in
 391   let h,t = hd rlist',mk_rlist (tl rlist') in
 392   let lst = last rlist' in
 393   let b,x = dest_binop rlt (concl place_thm) in
 394   let imp_thm = REWRITE_RULE[AND_IMP_THM]
 395                   (ISPECL [x;rlist]  ROL_INSERT_BACK_THM) in
 396   let a1 = rol_thm in
 397   let a2 = ISPECL [h;t] NOT_CONS_NIL in
 398   let a3_aux = prove(mk_eq (mk_comb(rlast,rlist),lst),
 399                      REWRITE_TAC[LAST;COND_CLAUSES;NOT_CONS_NIL]) in
 400   let a3 = MATCH_MPL [ISPECL [lst;x;rlist]
 401                         (REWRITE_RULE[AND_IMP_THM] lem1);place_thm;a3_aux] in
 402     REWRITE_RULE[APPEND] (MATCH_MPL[imp_thm;a1;a2;a3]);;
 403
 404 (*
 405 ROL_INSERT_BACK (ASSUME `x3 < x4`)
 406                 (ASSUME `real_ordered_list [x1; x2; x3]`);;
 407 *)
 408
 409 let ROL_INSERT place_thm rol_thm =
 410   let place_thm' = REWRITE_RULE[real_gt] place_thm in
 411   if is_conj (concl place_thm') then ROL_INSERT_MIDDLE place_thm' rol_thm
 412   else
 413     let _,rlist = dest_comb (concl rol_thm) in
 414     let rlist' = dest_list rlist in
 415     let h = hd rlist' in
 416     let l,r = dest_binop rlt (concl place_thm') in
 417       if r = h then ROL_INSERT_FRONT place_thm' rol_thm
 418       else ROL_INSERT_BACK place_thm' rol_thm;;
 419
 420 (*
 421 let k00 = ROL_INSERT (ASSUME `x1 < x4 /\ x4 < x2`)
 422            (ASSUME `real_ordered_list [x1; x2; x3]`);;
 423
 424 rol_thms k00
 425
 426 PARTITION_LINE_CONV `[x1; x4; x2; x3:real]`
 427
 428 ROL_INSERT (ASSUME `x4 < x1`)
 429            (ASSUME `real_ordered_list [x1]`);;
 430
 431 ROL_INSERT (ASSUME `x3 < x4`)
 432            (ASSUME `real_ordered_list [x1; x2; x3]`);;
 433
 434 *)
 435
 436
 437 (*
 438   rol_thms |- real_ordered_list [x;y;z]
 439
 440   --->
 441
 442   |- x < y; |- y < z
 443
 444 *)
 445 let rol_thms rol_thm =
 446   let thm = REWRITE_RULE[real_ordered_list;NOT_CONS_NIL;HD] rol_thm in
 447     rev(CONJUNCTS thm);;
 448 (*
 449 let rol_thm = ASSUME `real_ordered_list [x;y;z]`
 450 rol_thms rol_thm
 451 *)
 452
 453 let lem = prove(`!x. ?y. y = x`,MESON_TAC[]);;
 454
 455 let rec interleave l1 l2 =
 456   match l1 with
 457       [] -> l2
 458     | h::t ->
 459         match l2 with
 460             [] -> l1
 461           | h1::t1 -> h::h1::(interleave t t1);;
 462
 463
 464 let lem0 = prove(`?x:real. T`,MESON_TAC[]);;
 465
 466 let lem1 = prove_by_refinement(
 467   `!x. (?y. y < x) /\ (?y. y = x) /\ (?y. x < y)`,
 468 (* {{{ Proof *)
 469 [
 470   REPEAT STRIP_TAC;
 471   EXISTS_TAC `x - &1`;
 472   REAL_ARITH_TAC;
 473   MESON_TAC[];
 474   EXISTS_TAC `x + &1`;
 475   REAL_ARITH_TAC;
 476 ]);;
 477 (* }}} *)
 478
 479 let rol_nonempty_thms rol_thm =
 480   let pts = dest_list (snd(dest_comb(concl rol_thm))) in
 481   if length pts = 0 then [lem0] else
 482   if length pts = 1 then CONJUNCTS (ISPEC (hd pts) lem1) else
 483   let rthms = rol_thms rol_thm in
 484   let pt_thms = map (C ISPEC lem) pts in
 485   let left_thm = ISPEC (hd pts) REAL_GT_EXISTS in
 486   let right_thm = ISPEC (last pts) REAL_LT_EXISTS in
 487   let int_thms = map (MATCH_MP REAL_DENSE) rthms in
 488   let thms = interleave pt_thms int_thms in
 489     left_thm::thms @ [right_thm];;
 490
 491
 492 (*
 493   rol_nonempty_thms (ASSUME `real_ordered_list [y]`)
 494 *)
 495
 496 let lem0 = prove_by_refinement(
 497   `real_ordered_list []`,
 498 (* {{{ Proof *)
 499 [REWRITE_TAC[real_ordered_list]]);;
 500 (* }}} *)
 501
 502 let lem1 = prove_by_refinement(
 503   `!x y. x < y ==> real_ordered_list [x; y]`,
 504 (* {{{ Proof *)
 505 [
 506   REWRITE_TAC[real_ordered_list;NOT_CONS_NIL;HD];
 507 ]);;
 508 (* }}} *)
 509
 510 let lem2 = prove_by_refinement(
 511   `!x y. x < y ==> real_ordered_list (CONS y t) ==>
 512      real_ordered_list (CONS x (CONS y t))`,
 513 (* {{{ Proof *)
 514 [
 515   ASM_MESON_TAC[real_ordered_list;NOT_CONS_NIL;HD;TL];
 516 ]);;
 517 (* }}} *)
 518
 519 let mk_rol ord_thms =
 520   match ord_thms with
 521       [] -> lem0
 522     | [x] -> MATCH_MP lem1 x
 523     | h1::h2::rest ->
 524         itlist (fun x y -> MATCH_MPL[lem2;x;y]) (butlast ord_thms) (MATCH_MP lem1 (last ord_thms));;
 525
 526 (*
 527 let k0 = rol_thms (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`)
 528 mk_rol k0
 529 *)
 530
 531 let real_nil = `[]:real list`;;
 532 let ROL_NIL = prove
 533   (`real_ordered_list ([]:real list)`,
 534    REWRITE_TAC[real_ordered_list]);;
 535
 536 let ROL_REMOVE x rol_thm =
 537   let list = dest_list (snd (dest_comb (concl rol_thm))) in
 538   if length list = 0 then failwith "ROL_REMOVE: 0"
 539   else if length list = 1 then
 540     if x = hd list then ROL_NIL
 541     else failwith "ROL_REMOVE: Not an elem"
 542   else if length list = 2 then
 543     let l::r::[] = list in
 544       if l = x then ISPEC r ROL_SING
 545       else if r = x then ISPEC l ROL_SING
 546       else failwith "ROL_REMOVE: Not an elem"
 547   else
 548   let ord_thms = rol_thms rol_thm in
 549   let partition_fun thm =
 550     let l,r = dest_binop rlt (concl thm) in
 551       not (x = l) && not (x = r) in
 552   let ord_thms',elim_thms = partition partition_fun ord_thms in
 553   if length elim_thms = 1 then mk_rol ord_thms' else
 554   let [xy_thm; yz_thm] = elim_thms in
 555   let connect_thm = MATCH_MP REAL_LT_TRANS (CONJ xy_thm yz_thm) in
 556   let rec insert xz_thm thms =
 557     match thms with
 558         [] -> [connect_thm]
 559       | h::t ->
 560           let l,r = dest_binop rlt (concl h) in
 561           let l1,r1 = dest_binop rlt (concl xz_thm) in
 562           if (r1 = l) then xz_thm::h::t else h::insert xz_thm t in
 563   let ord_thms'' = insert connect_thm ord_thms' in
 564     mk_rol ord_thms'';;
 565
 566
 567 (*
 568 ROL_REMOVE `x1:real` (ASSUME `real_ordered_list [x1]`)
 569 ROL_REMOVE `x1:real` (ASSUME `real_ordered_list [x1; x3]`)
 570 ROL_REMOVE `x3:real` (ASSUME `real_ordered_list [x1; x3]`)
 571 ROL_REMOVE `x3:real` (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`)
 572 ROL_REMOVE `x1:real` (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`)
 573 ROL_REMOVE `x5:real` (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`)
 574
 575 ROL_REMOVE `-- &1` (ASSUME `real_ordered_list [-- &1; &0; &1]`)
 576 let rol_thm =  (ASSUME `real_ordered_list [-- &1; &0; &1]`)
 577 let x = `&0`
 578 *)
 579
 580 let lem = prove(
 581   `!y x. x < y \/ (x = y) \/ y < x`,
 582 (* {{{ Proof *)
 583 REAL_ARITH_TAC);;
 584 (* }}} *)
 585
 586 let lem2 = prove(
 587   `!x y z. y < z ==> (y < x <=> (y < x /\ x < z) \/ (x = z) \/ z < x)`,
 588 (* {{{ Proof *)
 589   REAL_ARITH_TAC);;
 590 (* }}} *)
 591
 592
 593 let ROL_COVERS rol_thm =
 594   let pts = dest_list (snd(dest_comb(concl rol_thm))) in
 595   if length pts = 1 then ISPEC (hd pts) lem else
 596   let thms = rol_thms rol_thm in
 597   let thms' = map (MATCH_MP lem2) thms in
 598   let base = ISPEC (hd pts) lem in
 599     itlist (fun x y -> ONCE_REWRITE_RULE[MATCH_MP lem2 x] y) (rev thms) base;;
 600
 601 (*
 602 ROL_COVERS (ASSUME `real_ordered_list [x; y; z]`)
 603 ROL_COVERS (ASSUME `real_ordered_list [x; y]`)
 604 ROL_COVERS (ASSUME `real_ordered_list [x]`)
 605
 606 *)