(* ---------------------------------------------------------------------- *)
(*  Util                                                                  *)
(* ---------------------------------------------------------------------- *)

(* ---------------------------------------------------------------------- *)
(*  Real Ordered Lists                                                    *)
(* ---------------------------------------------------------------------- *)

let real_ordered_list = new_recursive_definition list_RECURSION
  `(real_ordered_list [] <=> T) /\
   (real_ordered_list (CONS h t) <=>
      real_ordered_list t /\
      ((t = []) \/ (h < HD t)))`;;
let ROL_EMPTY = EQT_ELIM (CONJUNCT1 real_ordered_list);;
let ROL_SING = 
prove_by_refinement( `!x. real_ordered_list [x]`,
(* {{{ Proof *) [ REWRITE_TAC[real_ordered_list]; ]);;
(* }}} *)
let ROL_TAIL = 
prove( `!l. ~(l = []) /\ real_ordered_list l ==> real_ordered_list (TL l)`,
(* {{{ Proof *) LIST_INDUCT_TAC THEN MESON_TAC[real_ordered_list;TL]; );;
(* }}} *)
let EL_CONS = 
prove_by_refinement( `!l h n. EL n t = EL (SUC n) (CONS h t)`,
(* {{{ Proof *) [ MESON_TAC[TL;EL]; ]);;
(* }}} *)
let NOT_ROL = 
prove_by_refinement( `!l. ~(real_ordered_list l) ==> ?n. EL n l >= EL (SUC n) l`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[real_ordered_list]; REWRITE_TAC[real_ordered_list;DE_MORGAN_THM]; STRIP_TAC; POP_ASSUM (fun x -> POP_ASSUM (fun y -> MP_TAC (MATCH_MP y x))); STRIP_TAC; EXISTS_TAC `SUC n`; ASM_MESON_TAC[EL_CONS]; EXISTS_TAC `0`; REWRITE_TAC[EL;HD;TL;real_ge]; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let ROL_CONS = 
prove_by_refinement( `!h t. real_ordered_list (CONS h t) ==> real_ordered_list t`,
(* {{{ Proof *) [ REWRITE_TAC[real_ordered_list]; REPEAT STRIP_TAC; ]);;
(* }}} *)
let ROL_CONS_CONS = 
prove_by_refinement( `!h t. real_ordered_list (CONS h1 (CONS h2 t)) <=> real_ordered_list (CONS h2 t) /\ h1 < h2`,
(* {{{ Proof *) [ REPEAT GEN_TAC; EQ_TAC; REWRITE_TAC[real_ordered_list]; REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[NOT_CONS_NIL;HD]; ASM_MESON_TAC[NOT_CONS_NIL]; ASM_MESON_TAC[HD]; ASM_MESON_TAC[NOT_CONS_NIL]; ASM_MESON_TAC[HD]; REWRITE_TAC[real_ordered_list]; REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[NOT_CONS_NIL;HD]; ]);;
(* }}} *)
let ROL_APPEND = 
prove_by_refinement( `!l1 l2. real_ordered_list (APPEND l1 l2) ==> real_ordered_list l1 /\ real_ordered_list l2`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; MESON_TAC[APPEND;real_ordered_list]; GEN_TAC; REWRITE_TAC[APPEND]; STRIP_TAC; CLAIM `real_ordered_list (APPEND t l2)`; ASM_MESON_TAC[ROL_CONS]; STRIP_TAC; CLAIM `real_ordered_list t /\ real_ordered_list l2`; ASM_MESON_TAC[]; STRIP_TAC; ASM_REWRITE_TAC[]; CASES_ON `t = []`; ASM_MESON_TAC[real_ordered_list]; POP_ASSUM MP_TAC; REWRITE_TAC[NOT_NIL]; STRIP_TAC; ASM_REWRITE_TAC[ROL_CONS_CONS]; CONJ_TAC; ASM_MESON_TAC[]; LABEL_ALL_TAC; USE_THEN "Z-4" MP_TAC; POP_ASSUM SUBST1_TAC; REWRITE_TAC[APPEND]; ASM_MESON_TAC[ROL_CONS_CONS]; ]);;
(* }}} *)
let ROL_CONS_CONS_LT = 
prove_by_refinement( `!h1 h2 t. real_ordered_list (CONS h1 (CONS h2 t)) ==> h1 < h2`,
(* {{{ Proof *) [ REWRITE_TAC[real_ordered_list]; REPEAT STRIP_TAC THEN ASM_MESON_TAC[NOT_CONS_NIL;HD]; ]);;
(* }}} *)
let ROL_INSERT_THM = 
prove_by_refinement( `!x l1 l2. real_ordered_list l1 /\ real_ordered_list l2 /\ ~(l1 = []) /\ ~(l2 = []) /\ LAST l1 < x /\ x < HD l2 ==> real_ordered_list (APPEND l1 (CONS x l2))`,
(* {{{ Proof *) [ GEN_TAC; LIST_INDUCT_TAC; REWRITE_TAC[APPEND]; CASES_ON `t = []`; ASM_REWRITE_TAC[APPEND;LAST_SING;NOT_CONS_NIL]; REPEAT STRIP_TAC; ASM_REWRITE_TAC[ROL_CONS_CONS;real_ordered_list]; POP_ASSUM MP_TAC; REWRITE_TAC[NOT_NIL]; STRIP_TAC; ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; CLAIM `real_ordered_list (APPEND t (CONS x l2))`; REWRITE_ASSUMS[TAUT `(p ==> q ==> r) <=> (p /\ q ==> r)`]; FIRST_ASSUM MATCH_MP_TAC; REPEAT STRIP_TAC; ASM_MESON_TAC[ROL_CONS]; FIRST_ASSUM MATCH_ACCEPT_TAC; ASM_MESON_TAC[NOT_CONS_NIL]; ASM_MESON_TAC[NOT_CONS_NIL]; ASM_MESON_TAC[LAST_CONS;NOT_CONS_NIL]; FIRST_ASSUM MATCH_ACCEPT_TAC; ASM_REWRITE_TAC[]; LABEL_ALL_TAC; USE_THEN "Z-3" (SUBST1_TAC o GSYM); REWRITE_TAC[APPEND]; STRIP_TAC; REWRITE_TAC[ROL_CONS_CONS]; STRIP_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; ASM_MESON_TAC[ROL_CONS_CONS]; ]);;
(* }}} *)
let ROL_INSERT_FRONT_THM = 
prove_by_refinement( `!x l. real_ordered_list l /\ ~(l = []) /\ x < HD l ==> real_ordered_list (CONS x l)`,
(* {{{ Proof *) [ REWRITE_TAC[NOT_NIL;AND_IMP_THM]; REPEAT STRIP_TAC; ASM_REWRITE_TAC[]; ASM_MESON_TAC[ROL_CONS_CONS;HD]; ]);;
(* }}} *)
let ROL_CONS_CONS_DELETE = 
prove_by_refinement( `!h1 h2 t. real_ordered_list (CONS h1 (CONS h2 t)) ==> real_ordered_list (CONS h1 t)`,
(* {{{ Proof *) [ REWRITE_TAC[real_ordered_list]; REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]; ASM_MESON_TAC[NOT_CONS_NIL]; REWRITE_ASSUMS[HD]; ASM_MESON_TAC[REAL_LT_TRANS]; ]);;
(* }}} *)
let LAST_CONS_LT = 
prove_by_refinement( `!x t h. real_ordered_list (CONS h t) /\ LAST (CONS h t) < x ==> h < x`,
(* {{{ Proof *) [ GEN_TAC; LIST_INDUCT_TAC; REWRITE_TAC[LAST]; REPEAT STRIP_TAC; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; CONJ_TAC; ASM_MESON_TAC[ROL_CONS_CONS_DELETE]; CASES_ON `t = []`; ASM_REWRITE_TAC[LAST]; ASM_MESON_TAC[LAST;ROL_CONS_CONS;REAL_LT_TRANS]; ASM_MESON_TAC[LAST_CONS;ROL_CONS_CONS_DELETE;LAST_CONS_CONS]; ]);;
(* }}} *)
let ROL_INSERT_BACK_THM = 
prove_by_refinement( `!x l. real_ordered_list l /\ ~(l = []) /\ LAST l < x ==> real_ordered_list (APPEND l [x])`,
(* {{{ Proof *) [ STRIP_TAC; LIST_INDUCT_TAC; REWRITE_TAC[APPEND;ROL_SING]; LABEL_ALL_TAC; STRIP_TAC; CASES_ON `t = []`; ASM_REWRITE_TAC[APPEND;ROL_CONS_CONS;ROL_SING]; ASM_MESON_TAC[LAST;COND_CLAUSES]; PROVE_ASSUM_ANTECEDENT_TAC 0; REPEAT STRIP_TAC; ASM_MESON_TAC[ROL_CONS]; ASM_MESON_TAC[]; ASM_MESON_TAC[LAST_CONS]; REWRITE_TAC[APPEND]; REWRITE_TAC[real_ordered_list]; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; DISJ2_TAC; REWRITE_ASSUMS[NOT_NIL]; LABEL_ALL_TAC; USE_IASSUM 2 MP_TAC; STRIP_TAC; ASM_REWRITE_TAC[HD_APPEND]; ASM_MESON_TAC[ROL_CONS_CONS]; ]);;
(* }}} *) (* 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');;
let t1 = 
prove_by_refinement( `real_ordered_list [&1; &2; &3; &4]`,
[ REWRITE_TAC[HD;real_ordered_list]; REAL_ARITH_TAC; ]);;
(* 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 lem1 = 
prove( `!e x l. e < x /\ (LAST l = e) ==> LAST l < x`,
MESON_TAC[]);;
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;;
(* ROL_INSERT_MIDDLE (ASSUME `x1 < x4 /\ x4 < x2`) (ASSUME `real_ordered_list [x1; x2; x3]`);; ROL_INSERT_MIDDLE (ASSUME `x1 < x6 /\ x6 < x2`) (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`);; ROL_INSERT_MIDDLE (ASSUME `x2 < x6 /\ x6 < x3`) (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`);; ROL_INSERT_MIDDLE (ASSUME `x4 < x6 /\ x6 < x5`) (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`);; ROL_INSERT_MIDDLE (ASSUME `x2 < x4 /\ x4 < x3`) (ASSUME `real_ordered_list [x1; x2; x3]`);; *) let ROL_INSERT_FRONT place_thm rol_thm = let _,rlist = dest_comb (concl rol_thm) in let h,t = hd (dest_list rlist),mk_rlist (tl (dest_list rlist)) in let imp_thm = ISPECL [h;t] (GSYM ROL_CONS_CONS) in let imp_thm' = REWRITE_RULE[AND_IMP_THM] (fst (EQ_IMP_RULE imp_thm)) in MATCH_MPL[imp_thm';rol_thm;place_thm];; (* ROL_INSERT_FRONT (ASSUME `x4 < x1`) (ASSUME `real_ordered_list [x1; x2; x3]`);; ROL_INSERT_FRONT (ASSUME `x4 < x1`) (ASSUME `real_ordered_list [x1]`);; *) let ROL_INSERT_BACK place_thm rol_thm = let _,rlist = dest_comb (concl rol_thm) in let rlist' = dest_list rlist in let h,t = hd rlist',mk_rlist (tl rlist') in let lst = last rlist' in let b,x = dest_binop rlt (concl place_thm) in let imp_thm = REWRITE_RULE[AND_IMP_THM] (ISPECL [x;rlist] ROL_INSERT_BACK_THM) in let a1 = rol_thm in let a2 = ISPECL [h;t] NOT_CONS_NIL in
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]);;
(* ROL_INSERT_BACK (ASSUME `x3 < x4`) (ASSUME `real_ordered_list [x1; x2; x3]`);; *) let ROL_INSERT place_thm rol_thm = let place_thm' = REWRITE_RULE[real_gt] place_thm in if is_conj (concl place_thm') then ROL_INSERT_MIDDLE place_thm' rol_thm else let _,rlist = dest_comb (concl rol_thm) in let rlist' = dest_list rlist in let h = hd rlist' in let l,r = dest_binop rlt (concl place_thm') in if r = h then ROL_INSERT_FRONT place_thm' rol_thm else ROL_INSERT_BACK place_thm' rol_thm;; (* let k00 = ROL_INSERT (ASSUME `x1 < x4 /\ x4 < x2`) (ASSUME `real_ordered_list [x1; x2; x3]`);; rol_thms k00 PARTITION_LINE_CONV `[x1; x4; x2; x3:real]` ROL_INSERT (ASSUME `x4 < x1`) (ASSUME `real_ordered_list [x1]`);; ROL_INSERT (ASSUME `x3 < x4`) (ASSUME `real_ordered_list [x1; x2; x3]`);; *) (* rol_thms |- real_ordered_list [x;y;z] ---> |- x < y; |- y < z *) let rol_thms rol_thm = let thm = REWRITE_RULE[real_ordered_list;NOT_CONS_NIL;HD] rol_thm in rev(CONJUNCTS thm);; (* let rol_thm = ASSUME `real_ordered_list [x;y;z]` rol_thms rol_thm *)
let lem = 
prove(`!x. ?y. y = x`,
MESON_TAC[]);;
let rec interleave l1 l2 = match l1 with [] -> l2 | h::t -> match l2 with [] -> l1 | h1::t1 -> h::h1::(interleave t t1);;
let lem0 = 
prove(`?x:real. T`,
MESON_TAC[]);;
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 rol_nonempty_thms rol_thm = let pts = dest_list (snd(dest_comb(concl rol_thm))) in if length pts = 0 then [lem0] else if length pts = 1 then CONJUNCTS (ISPEC (hd pts) lem1) else let rthms = rol_thms rol_thm in let pt_thms = map (C ISPEC lem) pts in let left_thm = ISPEC (hd pts) REAL_GT_EXISTS in let right_thm = ISPEC (last pts) REAL_LT_EXISTS in let int_thms = map (MATCH_MP REAL_DENSE) rthms in let thms = interleave pt_thms int_thms in left_thm::thms @ [right_thm];; (* rol_nonempty_thms (ASSUME `real_ordered_list [y]`) *)
let lem0 = 
prove_by_refinement( `real_ordered_list []`,
(* {{{ Proof *) [REWRITE_TAC[real_ordered_list]]);;
(* }}} *)
let lem1 = 
prove_by_refinement( `!x y. x < y ==> real_ordered_list [x; y]`,
(* {{{ Proof *) [ REWRITE_TAC[real_ordered_list;NOT_CONS_NIL;HD]; ]);;
(* }}} *)
let lem2 = 
prove_by_refinement( `!x y. x < y ==> real_ordered_list (CONS y t) ==> real_ordered_list (CONS x (CONS y t))`,
(* {{{ Proof *) [ ASM_MESON_TAC[real_ordered_list;NOT_CONS_NIL;HD;TL]; ]);;
(* }}} *) let mk_rol ord_thms = match ord_thms with [] -> lem0 | [x] -> MATCH_MP lem1 x | h1::h2::rest -> itlist (fun x y -> MATCH_MPL[lem2;x;y]) (butlast ord_thms) (MATCH_MP lem1 (last ord_thms));; (* let k0 = rol_thms (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`) mk_rol k0 *) let real_nil = `[]:real list`;;
let ROL_NIL = 
prove (`real_ordered_list ([]:real list)`,
REWRITE_TAC[real_ordered_list]);;
let ROL_REMOVE x rol_thm = let list = dest_list (snd (dest_comb (concl rol_thm))) in if length list = 0 then failwith "ROL_REMOVE: 0" else if length list = 1 then if x = hd list then ROL_NIL else failwith "ROL_REMOVE: Not an elem" else if length list = 2 then let l::r::[] = list in if l = x then ISPEC r ROL_SING else if r = x then ISPEC l ROL_SING else failwith "ROL_REMOVE: Not an elem" else let ord_thms = rol_thms rol_thm in let partition_fun thm = let l,r = dest_binop rlt (concl thm) in not (x = l) && not (x = r) in let ord_thms',elim_thms = partition partition_fun ord_thms in if length elim_thms = 1 then mk_rol ord_thms' else let [xy_thm; yz_thm] = elim_thms in let connect_thm = MATCH_MP REAL_LT_TRANS (CONJ xy_thm yz_thm) in let rec insert xz_thm thms = match thms with [] -> [connect_thm] | h::t -> let l,r = dest_binop rlt (concl h) in let l1,r1 = dest_binop rlt (concl xz_thm) in if (r1 = l) then xz_thm::h::t else h::insert xz_thm t in let ord_thms'' = insert connect_thm ord_thms' in mk_rol ord_thms'';; (* ROL_REMOVE `x1:real` (ASSUME `real_ordered_list [x1]`) ROL_REMOVE `x1:real` (ASSUME `real_ordered_list [x1; x3]`) ROL_REMOVE `x3:real` (ASSUME `real_ordered_list [x1; x3]`) ROL_REMOVE `x3:real` (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`) ROL_REMOVE `x1:real` (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`) ROL_REMOVE `x5:real` (ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`) ROL_REMOVE `-- &1` (ASSUME `real_ordered_list [-- &1; &0; &1]`) let rol_thm = (ASSUME `real_ordered_list [-- &1; &0; &1]`) let x = `&0` *)
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);;
(* }}} *) let ROL_COVERS rol_thm = let pts = dest_list (snd(dest_comb(concl rol_thm))) in if length pts = 1 then ISPEC (hd pts) lem else let thms = rol_thms rol_thm in let thms' = map (MATCH_MP lem2) thms in let base = ISPEC (hd pts) lem in itlist (fun x y -> ONCE_REWRITE_RULE[MATCH_MP lem2 x] y) (rev thms) base;; (* ROL_COVERS (ASSUME `real_ordered_list [x; y; z]`) ROL_COVERS (ASSUME `real_ordered_list [x; y]`) ROL_COVERS (ASSUME `real_ordered_list [x]`) *)