(* ---------------------------------------------------------------------- *)
(* Util *)
(* ---------------------------------------------------------------------- *)
(* ---------------------------------------------------------------------- *)
(* Real Ordered Lists *)
(* ---------------------------------------------------------------------- *)
let ROL_EMPTY = EQT_ELIM (CONJUNCT1 real_ordered_list);;
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(*
CHOP_REAL_LIST 1 `[&1; &2; &3]` --> |- [&1; &2; &3] = APPEND [&1; &2] [&3]
let n,l = 1,`[&1; &2; &3]`
*)
let CHOP_REAL_LIST n l =
let l' = dest_list l in
let l1',l2' = chop_list n l' in
let l1,l2 = mk_list (l1',real_ty),mk_list (l2',real_ty) in
let tm = mk_binop rappend l1 l2 in
GSYM (REWRITE_CONV [APPEND] tm);;
(*
ROL_CHOP_LT 2
let n = 1
*)
let ROL_CHOP_LT n thm =
let thm' = funpow (n - 1) (MATCH_MP ROL_CONS) thm in
CONJUNCT2 (PURE_REWRITE_RULE[ROL_CONS_CONS] thm');;
(*
ROL_CHOP_LIST 2 |- real_ordered_list [&1; &2; &3; &4] -->
|- real_ordered_list [&1; &2; &3],
|- real_ordered_list [&4],
|- &3 < &4
let thm = ASSUME `real_ordered_list [&1; &2; &3; &4]`
let n = 2
ROL_CHOP_LIST 2 thm
*)
let ROL_CHOP_LIST n thm =
let _,l = dest_comb (concl thm) in
let lthm = CHOP_REAL_LIST n l in
let thm' = REWRITE_RULE[lthm] thm in
let thm'' = MATCH_MP ROL_APPEND thm' in
let [lthm;rthm] = CONJUNCTS thm'' in
let lt_thm = ROL_CHOP_LT n thm in
lthm,rthm,lt_thm;;
(*
rol_insert (|- x1 < x4 /\ x4 < x2)
(|- real_ordered_list [x1; x2; x3]) -->
(|- real_ordered_list [x1; x4; x2; x3]);
rol_insert (|- &2 < &5 /\ &5 < &6) (|- real_ordered_list [&1; &2; &6]) -->
(|- real_ordered_list [&1; &2; &5; &6]);
rol_insert (|- x4 < x1)
(|- real_ordered_list [x1; x2; x3]) -->
(|- real_ordered_list [x4; x1; x2; x3]);
rol_insert (|- x1 < x4)
(|- real_ordered_list [x1; x2; x3]) -->
(|- real_ordered_list [x1; x2; x3; x4]);
*)
let ROL_INSERT_MIDDLE place_thm rol_thm =
let [pl1;pl2] = CONJUNCTS place_thm in
let list = snd(dest_comb(concl rol_thm)) in
let new_x,slot =
let ltl,ltr = dest_conj (concl place_thm) in
let x1,x4 = dest_binop rlt ltl in
let _,x2 = dest_binop rlt ltr in
let n = (index x1 (dest_list list)) + 1 in
x4,n in
let lthm,rthm,lt_thm = ROL_CHOP_LIST slot rol_thm in
let llist = snd(dest_comb(concl lthm)) in
let hllist = hd (dest_list llist) in
let tllist = mk_rlist (tl (dest_list llist)) in
let rlist = snd(dest_comb(concl rthm)) in
let hrlist = hd (dest_list rlist) in
let trlist = mk_rlist (tl (dest_list rlist)) in
let gthm = REWRITE_RULE[AND_IMP_THM] ROL_INSERT_THM in
let a1 = lthm in
let a2 = rthm in
let a3 = ISPECL [hllist;tllist] NOT_CONS_NIL in
let a4 = ISPECL [hrlist;trlist] NOT_CONS_NIL in
let l,r = dest_binop rlt (concl pl1) in
let a5_aux = prove(mk_eq (mk_comb(rlast,llist),l),REWRITE_TAC[LAST;COND_CLAUSES;NOT_CONS_NIL]) in
let a5 = MATCH_MPL [ISPECL [l;r;llist] (REWRITE_RULE[AND_IMP_THM] lem1);pl1;a5_aux] in
let a6_aux = ISPECL [trlist;hrlist] (GEN_ALL HD) in
let a6 = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV[GSYM a6_aux])) pl2 in
let thm = MATCH_MPL [gthm;a1;a2;a3;a4;a5;a6] in
REWRITE_RULE[APPEND] thm;;let a3_aux = prove(mk_eq (mk_comb(rlast,rlist),lst),
REWRITE_TAC[LAST;COND_CLAUSES;NOT_CONS_NIL]) in
let a3 = MATCH_MPL [ISPECL [lst;x;rlist]
(REWRITE_RULE[AND_IMP_THM] lem1);place_thm;a3_aux] in
REWRITE_RULE[APPEND] (MATCH_MPL[imp_thm;a1;a2;a3]);;let lem1 = prove_by_refinement(
`!x. (?y. y < x) /\ (?y. y = x) /\ (?y. x < y)`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
EXISTS_TAC `x - &1`;
REAL_ARITH_TAC;
MESON_TAC[];
EXISTS_TAC `x + &1`;
REAL_ARITH_TAC;
]);;
let lem = prove(
`!y x. x < y \/ (x = y) \/ y < x`,
(* {{{ Proof *)
REAL_ARITH_TAC);;
let lem2 = prove(
`!x y z. y < z ==> (y < x <=> (y < x /\ x < z) \/ (x = z) \/ z < x)`,
(* {{{ Proof *)
REAL_ARITH_TAC);;