let rec DISJ_TAC thm = DISJ_CASES_TAC thm THENL[ALL_TAC;TRY (POP_ASSUM DISJ_TAC)];;
let INTERPSIGNS_CONJ = prove_by_refinement(
`!P Q eqs l.
interpsigns eqs (\x. P x) l /\
interpsigns eqs (\x. Q x) l ==>
interpsigns eqs (\x. P x \/ Q x) l`,
(* {{{ Proof *)
[
STRIP_TAC THEN STRIP_TAC;
REPEAT LIST_INDUCT_TAC THEN REWRITE_TAC[interpsigns;
ALL2;interpsign];
REPEAT (POP_ASSUM MP_TAC);
DISJ_TAC (ISPEC `h':sign`
SIGN_CASES) THEN ASM_REWRITE_TAC[interpsign;interpsigns] THEN REPEAT STRIP_TAC THEN ASM_MESON_TAC[];
]);;
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
let SUBLIST_MATCH = prove_by_refinement(
`!h t l.
SUBLIST (CONS h t) l ==>
?(l1:A list) l2. (l =
APPEND l1 (CONS h l2)) /\
SUBLIST t l2`,
(* {{{ Proof *)
[
STRIP_TAC;
REPEAT LIST_INDUCT_TAC;
REWRITE_TAC[
SUBLIST;
NOT_CONS_NIL;];
CASES_ON `h = h'`;
POP_ASSUM (REWRITE_ALL o list);
STRIP_TAC;
EXISTS_TAC `[]`;
REWRITE_TAC[
APPEND;
SUBLIST_NIL];
ASM_MESON_TAC[];
REWRITE_TAC[
SUBLIST_NIL];
STRIP_TAC;
CLAIM `
SUBLIST [h] t`;
ASM_MESON_TAC[
SUBLIST_NEQ];
DISCH_THEN (REWRITE_ASSUMS o list);
REPEAT (POP_ASSUM MP_TAC);
REPEAT STRIP_TAC;
EXISTS_TAC `CONS h' l1`;
EXISTS_TAC `l2`;
REWRITE_TAC[
APPEND];
AP_TERM_TAC;
ASM_MESON_TAC[];
REWRITE_TAC[
SUBLIST;
NOT_CONS_NIL;];
(* save *)
CASES_ON `h = h''`;
POP_ASSUM (REWRITE_ALL o list);
STRIP_TAC;
REWRITE_ASSUMS[
SUBLIST_CONS_CONS];
EXISTS_TAC `[]:A list`;
EXISTS_TAC `t'`;
ASM_MESON_TAC[
APPEND];
(* save *)
STRIP_TAC;
CLAIM `
SUBLIST (CONS h (CONS h' t)) t'`;
ASM_MESON_TAC[
SUBLIST_NEQ];
DISCH_THEN (REWRITE_ASSUMS o list);
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
EXISTS_TAC `CONS h'' l1`;
EXISTS_TAC `l2`;
ASM_REWRITE_TAC[
APPEND];
]);;
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
let SUBLIST_TRANS2 = REWRITE_RULE[IMP_AND_THM] SUBLIST_TRANS;;
(* }}} *)
(* }}} *)
let SUBLIST_APPEND2 = REWRITE_RULE[IMP_AND_THM] SUBLIST_APPEND;;
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
let rec LENGTH_N n ty =
let zero = `0` in
let neg = `(~)` in
let imp_thm = TAUT `(a ==> b) ==> (b ==> a) ==> (a <=> b)` in
match n with
0 -> CONJUNCT1 LENGTH
| 1 -> LENGTH_SING
| n ->
let len_tm = mk_const ("LENGTH",[ty,aty]) in
let tl_tm = mk_const ("TL",[ty,aty]) in
let hd_tm = mk_const ("HD",[ty,aty]) in
let t = mk_var("t",mk_type("list",[ty])) in
let n_tm = mk_small_numeral n in
let pren_tm = mk_small_numeral (n - 1) in
let len_thm = ASSUME (mk_eq(mk_comb(len_tm,t),n_tm)) in
let pre_thm = LENGTH_N (n - 1) ty in
let n_nz = prove(mk_neg(mk_eq(n_tm,zero)),ARITH_TAC) in
let not_nil_thm = EQ_MP (REWRITE_RULE[len_thm] (AP_TERM neg (ISPEC t LENGTH_0))) n_nz in
let n_suc = prove(mk_eq(n_tm,mk_comb(`SUC`,pren_tm)),ARITH_TAC) in
let len_tl = REWRITE_RULE[n_suc;PRE;ISPEC (mk_comb(tl_tm,t)) pre_thm;len_thm] (MATCH_MP LENGTH_TL not_nil_thm) in
let cons_thm = MATCH_MP (ISPEC t HD_TL) not_nil_thm in
let hd_thm = ONCE_REWRITE_RULE[HD_LEM] len_tl in
let thm = REWRITE_RULE[GSYM cons_thm] hd_thm in
let x0 = mk_var("x" ^ string_of_int n,ty) in
let hdt = mk_comb(hd_tm,t) in
let ex_thm = EXISTS (mk_exists(x0,subst[x0,hdt] (concl thm)),mk_comb(hd_tm,t)) thm in
let left = DISCH (concl len_thm) ex_thm in
let right = prove(mk_imp(concl ex_thm,concl len_thm),REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC) in
GEN_ALL(MATCH_MPL[imp_thm;left;right]);;
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
let INFERISIGN_POS_POS_POS = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Unknown (CONS Pos r2))
(CONS (CONS Pos r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Pos (CONS Pos r2))
(CONS (CONS Pos r3) rgns))))`,
(* }}} *)
let INFERISIGN_POS_POS_NEG = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Unknown (CONS Neg r2))
(CONS (CONS Pos r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Pos (CONS Neg r2))
(CONS (CONS Pos r3) rgns))))`,
(* }}} *)
let INFERISIGN_NEG_NEG_POS = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Unknown (CONS Pos r2))
(CONS (CONS Neg r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Neg (CONS Pos r2))
(CONS (CONS Neg r3) rgns))))`,
(* }}} *)
let INFERISIGN_NEG_NEG_NEG = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Unknown (CONS Neg r2))
(CONS (CONS Neg r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Neg (CONS Neg r2))
(CONS (CONS Neg r3) rgns))))`,
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
let INFERISIGN_POS_NEG_POS = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Unknown (CONS Pos r2))
(CONS (CONS Neg r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
?w. interpmat (
APPEND pts (CONS y (CONS w (CONS z qts))))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Pos (CONS Pos r2))
(CONS (CONS Zero (CONS Pos r2))
(CONS (CONS Neg (CONS Pos r2))
(CONS (CONS Neg r3) rgns))))))`,
(* }}} *)
let INFERISIGN_POS_NEG_NEG = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Unknown (CONS Neg r2))
(CONS (CONS Neg r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
?w. interpmat (
APPEND pts (CONS y (CONS w (CONS z qts))))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Pos (CONS Neg r2))
(CONS (CONS Zero (CONS Neg r2))
(CONS (CONS Neg (CONS Neg r2))
(CONS (CONS Neg r3) rgns))))))`,
(* }}} *)
let INFERISIGN_NEG_POS_NEG = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Unknown (CONS Neg r2))
(CONS (CONS Pos r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
?w. interpmat (
APPEND pts (CONS y (CONS w (CONS z qts))))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Neg (CONS Neg r2))
(CONS (CONS Zero (CONS Neg r2))
(CONS (CONS Pos (CONS Neg r2))
(CONS (CONS Pos r3) rgns))))))`,
(* }}} *)
let INFERISIGN_NEG_POS_POS = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Unknown (CONS Pos r2))
(CONS (CONS Pos r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
?w. interpmat (
APPEND pts (CONS y (CONS w (CONS z qts))))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Neg (CONS Pos r2))
(CONS (CONS Zero (CONS Pos r2))
(CONS (CONS Pos (CONS Pos r2))
(CONS (CONS Pos r3) rgns))))))`,
(* }}} *)
let INFERISIGN_ZERO_POS_POS = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Zero r1)
(CONS (CONS Unknown (CONS Pos r2))
(CONS (CONS Pos r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Zero r1)
(CONS (CONS Pos (CONS Pos r2))
(CONS (CONS Pos r3) rgns))))`,
(* }}} *)
let INFERISIGN_ZERO_POS_NEG = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Zero r1)
(CONS (CONS Unknown (CONS Neg r2))
(CONS (CONS Pos r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Zero r1)
(CONS (CONS Pos (CONS Neg r2))
(CONS (CONS Pos r3) rgns))))`,
(* }}} *)
let INFERISIGN_POS_ZERO_POS = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Unknown (CONS Pos r2))
(CONS (CONS Zero r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Pos (CONS Pos r2))
(CONS (CONS Zero r3) rgns))))`,
(* }}} *)
let INFERISIGN_POS_ZERO_NEG = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Unknown (CONS Neg r2))
(CONS (CONS Zero r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Pos r1)
(CONS (CONS Pos (CONS Neg r2))
(CONS (CONS Zero r3) rgns))))`,
(* }}} *)
let INFERISIGN_ZERO_NEG_POS = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Zero r1)
(CONS (CONS Unknown (CONS Pos r2))
(CONS (CONS Neg r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Zero r1)
(CONS (CONS Neg (CONS Pos r2))
(CONS (CONS Neg r3) rgns))))`,
(* }}} *)
let INFERISIGN_ZERO_NEG_NEG = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Zero r1)
(CONS (CONS Unknown (CONS Neg r2))
(CONS (CONS Neg r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Zero r1)
(CONS (CONS Neg (CONS Neg r2))
(CONS (CONS Neg r3) rgns))))`,
(* }}} *)
let INFERISIGN_NEG_ZERO_NEG = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Unknown (CONS Neg r2))
(CONS (CONS Zero r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Neg (CONS Neg r2))
(CONS (CONS Zero r3) rgns))))`,
(* }}} *)
let INFERISIGN_NEG_ZERO_POS = prove_by_refinement(
`!y z p pts qts eqs sgns rgns r1 r2 r3.
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Unknown (CONS Pos r2))
(CONS (CONS Zero r3) rgns)))) ==>
(
LENGTH sgns = 2 *
LENGTH pts + 1) ==>
interpmat (
APPEND pts (CONS y (CONS z qts)))
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) eqs))
(
APPEND sgns
(CONS (CONS Neg r1)
(CONS (CONS Neg (CONS Pos r2))
(CONS (CONS Zero r3) rgns))))`,
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
let INFIN_HD_POS_LEM = prove_by_refinement(
`!pts p ps r1 sgns.
interpmat pts
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(CONS (CONS Unknown (CONS Pos r1)) sgns) ==>
nonconstant p ==>
?xminf.
interpmat (CONS xminf pts)
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(CONS (CONS Neg (CONS Pos r1))
(CONS (CONS Neg (CONS Pos r1))
(CONS (CONS Unknown (CONS Pos r1)) sgns)))`,
(* }}} *)
let INFIN_TL_POS_LEM = prove_by_refinement(
`!pts p ps r1 sgns r2.
interpmat pts
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND sgns [a; b; CONS Unknown (CONS Pos r2)]) ==>
nonconstant p ==>
?xinf.
interpmat (
APPEND pts [xinf])
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND sgns
[a; b; CONS Unknown (CONS Pos r2);
CONS Pos (CONS Pos r2);
CONS Pos (CONS Pos r2)])`,
(* }}} *)
let INFIN_HD_NEG_LEM = prove_by_refinement(
`!pts p ps r1 sgns.
interpmat pts
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(CONS (CONS Unknown (CONS Neg r1)) sgns) ==>
nonconstant p ==>
?xminf.
interpmat (CONS xminf pts)
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(CONS (CONS Pos (CONS Neg r1))
(CONS (CONS Pos (CONS Neg r1))
(CONS (CONS Unknown (CONS Neg r1)) sgns)))`,
(* }}} *)
let INFIN_TL_NEG_LEM = prove_by_refinement(
`!pts p ps r1 sgns r2.
interpmat pts
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND sgns [a; b; CONS Unknown (CONS Neg r2)]) ==>
nonconstant p ==>
?xinf.
interpmat (
APPEND pts [xinf])
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND sgns
[a; b; CONS Unknown (CONS Neg r2);
CONS Neg (CONS Neg r2);
CONS Neg (CONS Neg r2)])`,
(* }}} *)
let INFIN_POS_POS = prove_by_refinement(
`!pts p ps r1 sgns r2.
interpmat pts
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND (CONS (CONS Unknown (CONS Pos r1)) sgns)
[a; b; CONS Unknown (CONS Pos r2)]) ==>
nonconstant p ==>
?xminf xinf.
interpmat (
APPEND (CONS xminf pts) [xinf])
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND
(CONS (CONS Neg (CONS Pos r1))
(CONS (CONS Neg (CONS Pos r1))
(CONS (CONS Unknown (CONS Pos r1)) sgns)))
[a; b; CONS Unknown (CONS Pos r2);
CONS Pos (CONS Pos r2);
CONS Pos (CONS Pos r2)])`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
REWRITE_ASSUMS[
APPEND];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_HD_POS_LEM);
ASM_REWRITE_TAC[];
STRIP_TAC;
EXISTS_TAC `xminf`;
MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFIN_TL_POS_LEM);
ASM_REWRITE_TAC[
APPEND;];
]);;
(* }}} *)
let INFIN_POS_NEG = prove_by_refinement(
`!pts p ps r1 sgns r2.
interpmat pts
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND (CONS (CONS Unknown (CONS Pos r1)) sgns)
[a; b; CONS Unknown (CONS Neg r2)]) ==>
nonconstant p ==>
?xminf xinf.
interpmat (
APPEND (CONS xminf pts) [xinf])
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND
(CONS (CONS Neg (CONS Pos r1))
(CONS (CONS Neg (CONS Pos r1))
(CONS (CONS Unknown (CONS Pos r1)) sgns)))
[a; b; CONS Unknown (CONS Neg r2);
CONS Neg (CONS Neg r2);
CONS Neg (CONS Neg r2)])`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
REWRITE_ASSUMS[
APPEND];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_HD_POS_LEM);
ASM_REWRITE_TAC[];
STRIP_TAC;
EXISTS_TAC `xminf`;
MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFIN_TL_NEG_LEM);
ASM_REWRITE_TAC[
APPEND;];
]);;
(* }}} *)
let INFIN_NEG_POS = prove_by_refinement(
`!pts p ps r1 sgns r2.
interpmat pts
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND (CONS (CONS Unknown (CONS Neg r1)) sgns)
[a; b; CONS Unknown (CONS Pos r2)]) ==>
nonconstant p ==>
?xminf xinf.
interpmat (
APPEND (CONS xminf pts) [xinf])
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND
(CONS (CONS Pos (CONS Neg r1))
(CONS (CONS Pos (CONS Neg r1))
(CONS (CONS Unknown (CONS Neg r1)) sgns)))
[a; b; CONS Unknown (CONS Pos r2);
CONS Pos (CONS Pos r2);
CONS Pos (CONS Pos r2)])`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
REWRITE_ASSUMS[
APPEND];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_HD_NEG_LEM);
ASM_REWRITE_TAC[];
STRIP_TAC;
EXISTS_TAC `xminf`;
MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFIN_TL_POS_LEM);
ASM_REWRITE_TAC[
APPEND;];
]);;
(* }}} *)
let INFIN_NEG_NEG = prove_by_refinement(
`!pts p ps r1 sgns r2.
interpmat pts
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND (CONS (CONS Unknown (CONS Neg r1)) sgns)
[a; b; CONS Unknown (CONS Neg r2)]) ==>
nonconstant p ==>
?xminf xinf.
interpmat (
APPEND (CONS xminf pts) [xinf])
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
(
APPEND
(CONS (CONS Pos (CONS Neg r1))
(CONS (CONS Pos (CONS Neg r1))
(CONS (CONS Unknown (CONS Neg r1)) sgns)))
[a; b; CONS Unknown (CONS Neg r2);
CONS Neg (CONS Neg r2);
CONS Neg (CONS Neg r2)])`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
REWRITE_ASSUMS[
APPEND];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_HD_NEG_LEM);
ASM_REWRITE_TAC[];
STRIP_TAC;
EXISTS_TAC `xminf`;
MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFIN_TL_NEG_LEM);
ASM_REWRITE_TAC[
APPEND;];
]);;
(* }}} *)
let INFIN_NIL_POS = prove_by_refinement(
`!p ps r1.
interpmat []
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Unknown (CONS Pos r1)] ==>
nonconstant p ==>
?xminf xinf.
interpmat [xminf; xinf]
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Neg (CONS Pos r1);
CONS Neg (CONS Pos r1);
CONS Unknown (CONS Pos r1);
CONS Pos (CONS Pos r1);
CONS Pos (CONS Pos r1)]`,
(* }}} *)
let INFIN_NIL_NEG = prove_by_refinement(
`!p ps r1.
interpmat []
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Unknown (CONS Neg r1)] ==>
nonconstant p ==>
?xminf xinf.
interpmat [xminf; xinf]
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Pos (CONS Neg r1);
CONS Pos (CONS Neg r1);
CONS Unknown (CONS Neg r1);
CONS Neg (CONS Neg r1);
CONS Neg (CONS Neg r1)]`,
(* }}} *)
let INFIN_SING_POS_POS = prove_by_refinement(
`!p ps r1 x s2 r2 r3.
interpmat [x]
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Unknown (CONS Pos r1);CONS s2 r2;CONS Unknown (CONS Pos r3)] ==>
nonconstant p ==>
?xminf xinf.
interpmat [xminf; x; xinf]
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Neg (CONS Pos r1);
CONS Neg (CONS Pos r1);
CONS Unknown (CONS Pos r1);
CONS s2 r2;
CONS Unknown (CONS Pos r3);
CONS Pos (CONS Pos r3);
CONS Pos (CONS Pos r3)]`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
ONCE_REWRITE_ASSUMS[
prove(`[x; y; z] =
APPEND [] [x; y; z]`,REWRITE_TAC[
APPEND])];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_TL_POS_LEM);
ASM_REWRITE_TAC[];
STRIP_TAC;
MATCH_MP_TAC (
prove(`(?y x. P x y) ==> (?x y. P x y)`,MESON_TAC[]));
EXISTS_TAC `xinf`;
REWRITE_ALL[
APPEND];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_HD_POS_LEM);
ASM_REWRITE_TAC[];
]);;
(* }}} *)
let INFIN_SING_POS_NEG = prove_by_refinement(
`!p ps r1 x s2 r2 r3.
interpmat [x]
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Unknown (CONS Pos r1);CONS s2 r2;CONS Unknown (CONS Neg r3)] ==>
nonconstant p ==>
?xminf xinf.
interpmat [xminf; x; xinf]
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Neg (CONS Pos r1);
CONS Neg (CONS Pos r1);
CONS Unknown (CONS Pos r1);
CONS s2 r2;
CONS Unknown (CONS Neg r3);
CONS Neg (CONS Neg r3);
CONS Neg (CONS Neg r3)]`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
ONCE_REWRITE_ASSUMS[
prove(`[x; y; z] =
APPEND [] [x; y; z]`,REWRITE_TAC[
APPEND])];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_TL_NEG_LEM);
ASM_REWRITE_TAC[];
STRIP_TAC;
MATCH_MP_TAC (
prove(`(?y x. P x y) ==> (?x y. P x y)`,MESON_TAC[]));
EXISTS_TAC `xinf`;
REWRITE_ALL[
APPEND];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_HD_POS_LEM);
ASM_REWRITE_TAC[];
]);;
(* }}} *)
let INFIN_SING_NEG_POS = prove_by_refinement(
`!p ps r1 x s2 r2 r3.
interpmat [x]
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Unknown (CONS Neg r1);CONS s2 r2;CONS Unknown (CONS Pos r3)] ==>
nonconstant p ==>
?xminf xinf.
interpmat [xminf; x; xinf]
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Pos (CONS Neg r1);
CONS Pos (CONS Neg r1);
CONS Unknown (CONS Neg r1);
CONS s2 r2;
CONS Unknown (CONS Pos r3);
CONS Pos (CONS Pos r3);
CONS Pos (CONS Pos r3)]`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
ONCE_REWRITE_ASSUMS[
prove(`[x; y; z] =
APPEND [] [x; y; z]`,REWRITE_TAC[
APPEND])];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_TL_POS_LEM);
ASM_REWRITE_TAC[];
STRIP_TAC;
MATCH_MP_TAC (
prove(`(?y x. P x y) ==> (?x y. P x y)`,MESON_TAC[]));
EXISTS_TAC `xinf`;
REWRITE_ALL[
APPEND];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_HD_NEG_LEM);
ASM_REWRITE_TAC[];
]);;
(* }}} *)
let INFIN_SING_NEG_NEG = prove_by_refinement(
`!p ps r1 x s2 r2 r3.
interpmat [x]
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Unknown (CONS Neg r1);CONS s2 r2;CONS Unknown (CONS Neg r3)] ==>
nonconstant p ==>
?xminf xinf.
interpmat [xminf; x; xinf]
(CONS (\x. poly p x) (CONS (\x. poly (
poly_diff p) x) ps))
[CONS Pos (CONS Neg r1);
CONS Pos (CONS Neg r1);
CONS Unknown (CONS Neg r1);
CONS s2 r2;
CONS Unknown (CONS Neg r3);
CONS Neg (CONS Neg r3);
CONS Neg (CONS Neg r3)]`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
ONCE_REWRITE_ASSUMS[
prove(`[x; y; z] =
APPEND [] [x; y; z]`,REWRITE_TAC[
APPEND])];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_TL_NEG_LEM);
ASM_REWRITE_TAC[];
STRIP_TAC;
MATCH_MP_TAC (
prove(`(?y x. P x y) ==> (?x y. P x y)`,MESON_TAC[]));
EXISTS_TAC `xinf`;
REWRITE_ALL[
APPEND];
FIRST_ASSUM (MP_TAC o MATCH_MP
INFIN_HD_NEG_LEM);
ASM_REWRITE_TAC[];
]);;
(* }}} *)
(* }}} *)
(* }}} *)
let ALL2_EL_LT_LEM = prove_by_refinement(
`!k P l1 l2 n.
(k =
LENGTH l1) /\
ALL2 P l1 l2 /\ n < k ==>
P (
EL n l1) (
EL n l2)`,
(* {{{ Proof *)
[
INDUCT_TAC;
REPEAT STRIP_TAC;
POP_ASSUM MP_TAC THEN ARITH_TAC;
REPEAT STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
STRIP_TAC;
CLAIM `~(l1 = [])`;
REWRITE_TAC[GSYM
LENGTH_0];
REPEAT_N 3 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
REWRITE_TAC[
NOT_NIL;];
STRIP_TAC;
CLAIM `~(l2 = [])`;
REWRITE_TAC[GSYM
LENGTH_0];
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (SUBST1_TAC o GSYM);
REPEAT_N 2 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
REWRITE_TAC[
NOT_NIL;];
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ASSUMS[
LENGTH;
SUC_INJ;
ALL2;];
REPEAT_N 3 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list);
REPEAT STRIP_TAC;
(* save *)
DISJ_CASES_TAC (ISPEC `n:num`
num_CASES);
POP_ASSUM (REWRITE_ALL o list);
ASM_REWRITE_TAC[
EL;
HD];
POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
EL;
TL;];
REWRITE_ASSUMS[
LENGTH;
SUC_INJ;
ALL2;
LT_SUC];
FIRST_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
]);;
(* }}} *)
(* }}} *)
let ALL2_EL_LEM = prove_by_refinement(
`!k P (l1:A list) (l2:B list). (k =
LENGTH l1) /\ (k =
LENGTH l2) /\
~(?i. i <
LENGTH l1 /\ ~(P (
EL i l1) (
EL i l2))) ==>
ALL2 P l1 l2`,
(* {{{ Proof *)
[
INDUCT_TAC;
REPEAT STRIP_TAC;
EVERY_ASSUM (MP_TAC o GSYM);
ASM_MESON_TAC[
LENGTH_0;
ALL2];
REPEAT STRIP_TAC;
CLAIM `~(l1 = [])`;
REWRITE_TAC[GSYM
LENGTH_0];
REPEAT_N 2 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
REWRITE_TAC[
NOT_NIL;];
STRIP_TAC;
CLAIM `~(l2 = [])`;
REWRITE_TAC[GSYM
LENGTH_0];
REPEAT_N 2 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
REWRITE_TAC[
NOT_NIL;];
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
LENGTH;
SUC_INJ;
ALL2;];
STRIP_TAC;
ASM_MESON_TAC[
LT_0;
EL;
HD;];
(* save *)
FIRST_ASSUM MATCH_MP_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_MESON_TAC[];
REPEAT STRIP_TAC;
CLAIM `SUC i < SUC (
LENGTH t)`;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
REPEAT_N 3 (POP_ASSUM MP_TAC);
REWRITE_ASSUMS[
NOT_EXISTS_THM];
POP_ASSUM (ASSUME_TAC o ISPEC `SUC i`);
REWRITE_ALL[
LT_SUC];
REWRITE_ALL[
EL;
TL;];
ASM_MESON_TAC[];
]);;
(* }}} *)
(* }}} *)
(* }}} *)
let REMOVE_HD_COL = prove_by_refinement(
`!p ps sgns pts.
interpmat pts (CONS p ps) sgns ==> interpmat pts ps (
MAP TL sgns)`,
(* {{{ Proof *)
[
REWRITE_TAC[interpmat;
ALL2_EL];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[
ALL2_EL];
ASM_MESON_TAC[
LENGTH_MAP];
REWRITE_ASSUMS[
NOT_EXISTS_THM];
REPEAT_N 2 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `i:num`);
REWRITE_TAC[DE_MORGAN_THM];
REPEAT STRIP_TAC;
ASM_MESON_TAC[];
REWRITE_ALL[interpsigns];
CLAIM `i <
LENGTH sgns`;
ASM_MESON_TAC[];
STRIP_TAC;
ASM_SIMP_TAC[
EL_MAP];
REWRITE_ALL[interpsigns];
CLAIM `~(
EL i sgns = [])`;
REWRITE_TAC[GSYM
LENGTH_0];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
REWRITE_TAC[
LENGTH];
ARITH_TAC;
(* save *)
DISCH_THEN (MP_TAC o MATCH_MP
HD_TL);
DISCH_THEN (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN SUBST1_TAC x);
REWRITE_TAC[
ALL2;
TL;];
REPEAT STRIP_TAC;
FIRST_ASSUM MATCH_ACCEPT_TAC;
]);;
(* }}} *)
let REMOVE_COL1 = prove_by_refinement(
`!sgns pts p1 p2 ps.
interpmat pts (CONS p1 (CONS p2 ps)) sgns ==>
interpmat pts (CONS p1 ps) (
MAP (\x. CONS (
HD x) (
TL (
TL x))) sgns)`,
(* {{{ Proof *)
[
REWRITE_TAC[interpmat;
ALL2_EL];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
ASM_MESON_TAC[
LENGTH_MAP];
REWRITE_ASSUMS[
NOT_EXISTS_THM];
REPEAT_N 2 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `i:num`);
REWRITE_TAC[DE_MORGAN_THM];
REPEAT STRIP_TAC;
ASM_MESON_TAC[];
REWRITE_ALL[interpsigns];
CLAIM `i <
LENGTH sgns`;
ASM_MESON_TAC[];
STRIP_TAC;
ASM_SIMP_TAC[
EL_MAP];
REWRITE_ALL[interpsigns];
CLAIM `~(
EL i sgns = [])`;
REWRITE_TAC[GSYM
LENGTH_0];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
REWRITE_TAC[
LENGTH];
ARITH_TAC;
(* save *)
DISCH_THEN (MP_TAC o MATCH_MP
HD_TL);
DISCH_THEN (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN SUBST1_TAC x);
REWRITE_TAC[
ALL2;
TL;];
REPEAT STRIP_TAC;
ASM_MESON_TAC[
HD;];
CLAIM `~(
TL (
EL i sgns) = [])`;
REWRITE_TAC[GSYM
LENGTH_0];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
REWRITE_TAC[
LENGTH];
ARITH_TAC;
(* save *)
DISCH_THEN (MP_TAC o MATCH_MP
HD_TL);
DISCH_THEN (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN SUBST1_TAC x);
REWRITE_TAC[
ALL2;
TL;];
REPEAT STRIP_TAC;
ASM_MESON_TAC[
HD;];
]);;
(* }}} *)
let ALL_EL = prove_by_refinement(
`!P l.
ALL P l <=> !n. n <
LENGTH l ==> P (
EL n l)`,
(* {{{ Proof *)
[
STRIP_TAC;
LIST_INDUCT_TAC;
REWRITE_TAC[
ALL;
LENGTH];
ARITH_TAC;
ASM_REWRITE_TAC[
ALL];
POP_ASSUM (fun x -> ALL_TAC);
EQ_TAC;
REPEAT STRIP_TAC;
CASES_ON `n = 0`;
POP_ASSUM (REWRITE_ALL o list);
ASM_REWRITE_TAC[
EL;
HD;];
REWRITE_ASSUMS[
LENGTH];
CLAIM `
PRE n <
LENGTH t`;
POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
DISCH_THEN (fun x -> FIRST_ASSUM (MP_TAC o C MATCH_MP x));
ASM_MESON_TAC[
EL_PRE];
(* save *)
REPEAT STRIP_TAC;
REWRITE_ASSUMS[
LENGTH];
FIRST_ASSUM (MP_TAC o ISPEC `0`);
REWRITE_TAC[
EL;
HD;];
MESON_TAC[
LT_0];
REWRITE_ASSUMS[
LENGTH];
CLAIM `SUC n < SUC (
LENGTH t)`;
ASM_MESON_TAC[
LT_SUC];
DISCH_THEN (fun x -> FIRST_ASSUM (MP_TAC o C MATCH_MP x));
REWRITE_TAC[
EL_SUC];
]);;
(* }}} *)
(* }}} *)
(* }}} *)
let RESTRIP_TAC = REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;;
(* }}} *)
let REMOVE_LAST = prove_by_refinement(
`!pts pols sgns .
interpmat pts pols sgns ==>
interpmat pts (
BUTLAST pols) (
MAP BUTLAST sgns)`,
(* {{{ Proof *)
[
REWRITE_TAC[interpmat;
ALL2_EL];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
ASM_MESON_TAC[
LENGTH_MAP];
REWRITE_ASSUMS[
NOT_EXISTS_THM];
REPEAT_N 2 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `i:num`);
REWRITE_TAC[DE_MORGAN_THM];
REPEAT STRIP_TAC;
ASM_MESON_TAC[];
REWRITE_ALL[interpsigns];
CLAIM `i <
LENGTH sgns`;
ASM_MESON_TAC[];
STRIP_TAC;
(* save *)
ASM_SIMP_TAC[
EL_MAP];
ASM_MESON_TAC[
ALL2_BUTLAST];
]);;
(* }}} *)
let MAP2_EL_LEM = prove_by_refinement(
`!f k l1 l2 i. (
LENGTH l1 =
LENGTH l2) ==> i <
LENGTH l1 ==>
(k =
LENGTH l1) ==>
(
EL i (
MAP2 f l1 l2) = f (
EL i l1) (
EL i l2))`,
(* {{{ Proof *)
[
STRIP_TAC;
INDUCT_TAC;
REPEAT STRIP_TAC;
POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
REPEAT STRIP_TAC;
CLAIM `~(l1 = [])`;
ASM_MESON_TAC[
LENGTH_0;
NOT_SUC];
CLAIM `~(l2 = [])`;
ASM_MESON_TAC[
LENGTH_0;
NOT_SUC];
REWRITE_TAC[
NOT_NIL];
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
MAP2];
REWRITE_ALL[
LENGTH;
SUC_INJ];
DISJ_CASES_TAC (ISPEC `i:num`
num_CASES);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
EL;
HD;];
POP_ASSUM MP_TAC THEN STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
EL;
TL;];
REWRITE_ASSUMS[
LT_SUC];
ASM_MESON_TAC[];
]);;
(* }}} *)
(* }}} *)
(* }}} *)
let NUM_CASES_TAC = TYPE_TAC (fun x -> DISJ_CASES_TAC (ISPEC x num_CASES));;
(* }}} *)
let INSERTAT_EL = prove_by_refinement(
`!n (x:A) i l. n <=
LENGTH l ==> i <=
LENGTH l ==>
((i < n ==> (
EL i (
INSERTAT n x l) =
EL i l)) /\
((i = n) ==> (
EL i (
INSERTAT n x l) = x)) /\
(i > n ==> (
EL i (
INSERTAT n x l) =
EL (
PRE i) l)))`,
(* {{{ Proof *)
[
INDUCT_TAC;
REPEAT STRIP_TAC;
POP_ASSUM MP_TAC THEN ARITH_TAC;
ASM_REWRITE_TAC[
INSERTAT;
EL;
HD;];
ASM_REWRITE_TAC[
INSERTAT;
EL;
HD;];
DISJ_CASES_TAC (ISPEC `i:num`
num_CASES);
EVERY_ASSUM MP_TAC THEN ARITH_TAC;
POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
EL;
TL;
PRE];
(* save *)
REPEAT_N 5 STRIP_TAC;
CLAIM `~(l = [])`;
ASM_MESON_TAC[
LENGTH_0;
NOT_LE;ARITH_RULE `~(SUC n <= 0)`];
STRIP_TAC;
CLAIM `n <=
LENGTH (
TL l)`;
ASM_SIMP_TAC[
LENGTH_TL];
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
(* save *)
REPEAT STRIP_TAC;
REWRITE_TAC[
INSERTAT];
NUM_CASES_TAC `i`;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
EL;
HD;];
POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
EL;
TL;];
CLAIM `n' <=
LENGTH (
TL l)`;
REWRITE_ASSUMS[
LT_SUC];
ASM_MESON_TAC[
LTE_TRANS;
LT_TRANS;
LET_TRANS;
LT_IMP_LE];
STRIP_TAC;
REWRITE_ASSUMS[
LT_SUC];
ASM_MESON_TAC[];
(* save *)
POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
EL;
INSERTAT;
TL;];
ASM_MESON_TAC[];
REWRITE_TAC[
INSERTAT];
NUM_CASES_TAC `i`;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
EL;
HD;
PRE];
(* save *)
POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
EL;
TL;
PRE];
CLAIM `n' <=
LENGTH (
TL l)`;
ASM_SIMP_TAC[
LENGTH_TL];
REPEAT_N 3 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
REWRITE_ASSUMS[
GT;
LT_SUC];
FIRST_X_ASSUM (MP_TAC o ISPECL[`x:A`;`n':num`;`
TL l:A list`]);
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
NUM_CASES_TAC `n'`;
ASM_MESON_TAC[ARITH_RULE `x < y ==> ~(y = 0)`];
POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
PRE;
EL];
]);;
(* }}} *)
let USE_X_ASSUM lab ttac =
USE_THEN lab (fun th -> UNDISCH_THEN (concl th) ttac);;
let MATINSERT_THM = prove_by_refinement(
`!pts p pols n psgns sgns.
interpmat pts pols sgns ==>
ALL2 (\x y. interpsign x p y) (
partition_line pts) psgns ==>
n <=
LENGTH pols ==>
interpmat pts (
INSERTAT n p pols) (
MAP2 (
INSERTAT n) psgns sgns)`,
(* {{{ Proof *)
[
REWRITE_TAC[interpmat;
ALL2_EL;
NOT_EXISTS_THM;DE_MORGAN_THM;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[];
CLAIM `
LENGTH (psgns:sign list) =
LENGTH sgns`;
ASM_MESON_TAC[
LENGTH_MAP2];
ASM_MESON_TAC[
LENGTH_MAP2];
DISJ_LCASE;
REWRITE_ASSUMS[];
(* save *)
REWRITE_ALL[interpsigns];
CLAIM `
LENGTH psgns =
LENGTH sgns`;
ASM_MESON_TAC[];
STRIP_TAC;
CLAIM `i <
LENGTH psgns`;
ASM_MESON_TAC[];
STRIP_TAC;
ASM_SIMP_TAC[
MAP2_EL];
(* save *)
REWRITE_TAC[
ALL2_EL];
REWRITE_TAC[
NOT_EXISTS_THM;DE_MORGAN_THM];
REPEAT STRIP_TAC;
ASM_SIMP_TAC[
INSERTAT_LENGTH];
CLAIM `
LENGTH (
EL i (sgns:(sign list) list)) =
LENGTH pols`;
ASM_MESON_TAC[
ALL2_LENGTH];
STRIP_TAC;
ASM_SIMP_TAC[
INSERTAT_LENGTH];
(* save *)
DISJ_LCASE;
REWRITE_ASSUMS[];
MP_TAC (ARITH_RULE `i' < n \/ (i' = n) \/ i' > (n:num)`);
REPEAT STRIP_TAC;
CLAIM `
LENGTH (
EL i sgns) =
LENGTH pols`;
ASM_MESON_TAC[
ALL2_LENGTH];
STRIP_TAC;
CLAIM `n <=
LENGTH (
EL i sgns)`;
ASM_MESON_TAC[];
STRIP_TAC;
CLAIM `i' <=
LENGTH (
EL i sgns)`;
ASM_MESON_TAC[
LTE_TRANS;
LET_TRANS;
LT_TRANS;
LT_IMP_LE];
STRIP_TAC;
ASM_SIMP_TAC[
INSERTAT_EL];
CLAIM `i' <=
LENGTH pols`;
ASM_MESON_TAC[
LTE_TRANS;
LET_TRANS;
LT_TRANS;
LT_IMP_LE];
STRIP_TAC;
ASM_SIMP_TAC[
INSERTAT_EL];
REPEAT_N 12 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `i:num`);
REPEAT STRIP_TAC;
ASM_MESON_TAC[];
LABEL_ALL_TAC;
USE_THEN "Z-12" MP_TAC;
REWRITE_TAC[
ALL2_EL];
REWRITE_TAC[
NOT_EXISTS_THM;DE_MORGAN_THM];
STRIP_TAC;
POP_ASSUM (MP_TAC o ISPEC `i':num`);
POP_ASSUM (fun x -> ALL_TAC);
ASM_REWRITE_TAC[];
POP_ASSUM (fun x -> ALL_TAC);
STRIP_TAC;
ASM_MESON_TAC[ARITH_RULE `x <= y /\ z < x ==> z < (y:num)`];
(* save *)
POP_ASSUM (REWRITE_ALL o list);
CLAIM `
LENGTH (
EL i sgns) =
LENGTH pols`;
ASM_MESON_TAC[
ALL2_LENGTH];
STRIP_TAC;
CLAIM `n <=
LENGTH (
EL i sgns)`;
ASM_MESON_TAC[];
STRIP_TAC;
ASM_SIMP_TAC[
INSERTAT_EL];
ASM_MESON_TAC[
ALL2_EL];
(* save *)
CLAIM `
LENGTH (
EL i sgns) =
LENGTH pols`;
ASM_MESON_TAC[
ALL2_LENGTH];
STRIP_TAC;
CLAIM `n <=
LENGTH (
EL i sgns)`;
ASM_MESON_TAC[];
STRIP_TAC;
CLAIM `i' <=
LENGTH (
EL i sgns)`;
ASM_REWRITE_TAC[];
LABEL_ALL_TAC;
USE_THEN "Z-7" (MP_TAC o MATCH_MP
INSERTAT_LENGTH);
TYPE_TAC (fun x -> DISCH_THEN (MP_TAC o ISPEC x)) `p`;
USE_THEN "Z-3" MP_TAC THEN ARITH_TAC;
STRIP_TAC;
CLAIM `i' <=
LENGTH pols`;
ASM_MESON_TAC[];
STRIP_TAC;
ASM_SIMP_TAC[
INSERTAT_EL];
LABEL_ALL_TAC;
(* save *)
USE_X_ASSUM "Z-12" (MP_TAC o ISPEC `i:num`);
ASM_REWRITE_TAC[];
REWRITE_TAC[
ALL2_EL];
ASM_REWRITE_TAC[
NOT_EXISTS_THM;DE_MORGAN_THM;];
DISCH_THEN (MP_TAC o ISPEC `
PRE i':num`);
STRIP_TAC;
CLAIM `~(i' = 0)`;
USE_THEN "Z-4" MP_TAC THEN ARITH_TAC;
POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
]);;
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
let QUANT_CONV conv = RAND_CONV(ABS_CONV conv);;
let rec PATH_CONV2 s cnv =
match s with
[] -> cnv
| "l"::t -> RATOR_CONV (PATH_CONV2 t cnv)
| "r"::t -> RAND_CONV (PATH_CONV2 t cnv)
| "q"::t -> QUANT_CONV (PATH_CONV2 t cnv)
| "a"::t -> ABS_CONV (PATH_CONV2 t cnv)
| _ -> failwith "PATH_CONV2: unknown direction";;
let EL_REPLICATE = prove_by_refinement(
`!n x i. i < n ==> (
EL i (
REPLICATE n x) = x)`,
(* {{{ Proof *)
[
INDUCT_TAC;
ARITH_TAC;
REPEAT STRIP_TAC;
REWRITE_TAC[
REPLICATE];
NUM_CASES_TAC `i`;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
EL;
HD;];
POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
REWRITE_TAC[
EL;
TL;];
ASM_MESON_TAC[
LT_SUC];
]);;
(* }}} *)
(* }}} *)
(* }}} *)
let FUN_EQ_TAC = MATCH_EQ_MP_TAC (GSYM FUN_EQ_THM);;
(* }}} *)
(* }}} *)
let INFERPSIGN_POS = prove_by_refinement(
`!p ps q qs r rs s x pts1 pts2 s1 s2 s3 rest sgns.
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(
LENGTH sgns = 2 *
LENGTH pts1 + 1) ==>
(!x. p x = s x * q x + r x) ==>
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Pos s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest))`,
(* {{{ Proof *)
[
REWRITE_TAC[interpmat];
REPEAT STRIP_TAC;
FIRST_ASSUM MATCH_ACCEPT_TAC;
CASES_ON `pts1 = []`;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;];
COND_CASES_TAC;
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 5 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
FIRST_ASSUM MATCH_MP_TAC;
REWRITE_TAC[];
ASM_REWRITE_TAC[];
(* save *)
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 6 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
FIRST_ASSUM MATCH_MP_TAC;
REWRITE_TAC[];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
REPEAT STRIP_TAC;
CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
(CONS (\x'.
LAST pts1 < x' /\ x' < x)
(
TL (
partition_line (CONS x pts2))))) =
(
APPEND
(
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x])
(
TL (
partition_line (CONS x pts2))))`;
ASM_MESON_TAC[
APPEND_CONS];
DISCH_THEN (REWRITE_ALL o list);
REPEAT (POP_ASSUM MP_TAC);
REWRITE_ALL[
partition_line];
COND_CASES_TAC;
POP_ASSUM (REWRITE_ALL o list);
REPEAT STRIP_TAC;
REWRITE_ALL[
TL;];
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REPEAT_N 6 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
RESTRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
FIRST_ASSUM MATCH_MP_TAC;
REWRITE_TAC[];
(* save *)
REPEAT STRIP_TAC;
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 7 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
FIRST_ASSUM MATCH_MP_TAC;
REWRITE_TAC[];
]);;
(* }}} *)
let INFERPSIGN_NEG = prove_by_refinement(
`!p ps q qs r rs s x pts1 pts2 s1 s2 s3 rest sgns.
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(
LENGTH sgns = 2 *
LENGTH pts1 + 1) ==>
(!x. p x = s x * q x + r x) ==>
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Neg s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest))`,
(* {{{ Proof *)
[
REWRITE_TAC[interpmat];
REPEAT STRIP_TAC;
FIRST_ASSUM MATCH_ACCEPT_TAC;
CASES_ON `pts1 = []`;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;];
COND_CASES_TAC;
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 5 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
FIRST_ASSUM MATCH_MP_TAC;
REWRITE_TAC[];
ASM_REWRITE_TAC[];
(* save *)
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 6 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
FIRST_ASSUM MATCH_MP_TAC;
REWRITE_TAC[];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
REPEAT STRIP_TAC;
CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
(CONS (\x'.
LAST pts1 < x' /\ x' < x)
(
TL (
partition_line (CONS x pts2))))) =
(
APPEND
(
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x])
(
TL (
partition_line (CONS x pts2))))`;
ASM_MESON_TAC[
APPEND_CONS];
DISCH_THEN (REWRITE_ALL o list);
REPEAT (POP_ASSUM MP_TAC);
REWRITE_ALL[
partition_line];
COND_CASES_TAC;
POP_ASSUM (REWRITE_ALL o list);
REPEAT STRIP_TAC;
REWRITE_ALL[
TL;];
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REPEAT_N 6 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
RESTRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
FIRST_ASSUM MATCH_MP_TAC;
REWRITE_TAC[];
(* save *)
REPEAT STRIP_TAC;
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 7 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
REWRITE_TAC[
REAL_MUL_RZERO;REAL_ADD_LID;];
FIRST_ASSUM MATCH_MP_TAC;
REWRITE_TAC[];
]);;
(* }}} *)
let INFERPSIGN_POS_EVEN_LEM = prove_by_refinement(
`!a n p ps q qs r rs s x pts1 pts2 s1 s2 s3 rest sgns.
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(
LENGTH sgns = 2 *
LENGTH pts1 + 1) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a <> &0) ==>
EVEN n ==>
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Pos s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `a pow n > &0`;
ASM_MESON_TAC[
EVEN_ODD_POW];
STRIP_TAC;
REPEAT (POP_ASSUM MP_TAC);
REWRITE_TAC[interpmat];
REPEAT STRIP_TAC;
FIRST_ASSUM MATCH_ACCEPT_TAC;
CASES_ON `pts1 = []`;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;];
COND_CASES_TAC;
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 8 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x > &0`;
ASM_MESON_TAC[];
REPEAT_N 6 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 7 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 9 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x > &0`;
ASM_MESON_TAC[];
REPEAT_N 8 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 9 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
REPEAT STRIP_TAC;
CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
(CONS (\x'.
LAST pts1 < x' /\ x' < x)
(
TL (
partition_line (CONS x pts2))))) =
(
APPEND
(
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x])
(
TL (
partition_line (CONS x pts2))))`;
ASM_MESON_TAC[
APPEND_CONS];
DISCH_THEN (REWRITE_ALL o list);
REPEAT (POP_ASSUM MP_TAC);
REWRITE_ALL[
partition_line];
COND_CASES_TAC;
POP_ASSUM (REWRITE_ALL o list);
REPEAT STRIP_TAC;
REWRITE_ALL[
TL;];
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REPEAT_N 9 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
RESTRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x > &0`;
ASM_MESON_TAC[];
REPEAT_N 15 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
(* save *)
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 10 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x > &0`;
ASM_MESON_TAC[];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 17 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`];
]);;
(* }}} *)
let SPLIT_LIST_THM = prove_by_refinement(
`!n (l:A list). n <
LENGTH l ==>
?l1 l2. (l =
APPEND l1 l2) /\ (
LENGTH l1 = n)`,
(* {{{ Proof *)
[
INDUCT_TAC;
REPEAT STRIP_TAC;
EXISTS_TAC `[]:A list`;
EXISTS_TAC `l`;
REWRITE_TAC[
APPEND;
LENGTH];
REPEAT STRIP_TAC;
CLAIM `n <
LENGTH l`;
POP_ASSUM MP_TAC THEN ARITH_TAC;
DISCH_THEN (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x)));
STRIP_TAC;
EXISTS_TAC `
APPEND l1 [
HD l2]`;
EXISTS_TAC `
TL (l2:A list)`;
CLAIM `~((l2:A list) = [])`;
REWRITE_TAC[GSYM
LENGTH_0];
STRIP_TAC;
POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC;
POP_ASSUM (MP_TAC o AP_TERM `LENGTH:A list -> num`);
REWRITE_TAC[
LENGTH_APPEND];
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
REWRITE_TAC[
NOT_NIL;];
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
ASM_REWRITE_TAC[
TL;
HD;
LENGTH_APPEND;
LENGTH;];
STRIP_TAC;
REWRITE_TAC[
APPEND_APPEND;
APPEND;];
ARITH_TAC;
]);;
(* }}} *)
let rec EXISTS_TACL =
(fun l ->
match l with
[] -> ALL_TAC
| h::t -> TYPE_TAC EXISTS_TAC h THEN EXISTS_TACL t);;
let DIV_EVEN = prove_by_refinement(
`!x.
EVEN x ==> (2 * x DIV 2 = x)`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
TYPE_TACL (fun l -> MP_TAC (ISPECL l
DIVISION)) [`x`;`2`];
ARITH_SIMP_TAC[];
REWRITE_ASSUMS[
EVEN_MOD];
ASM_REWRITE_TAC[];
ARITH_SIMP_TAC[];
STRIP_TAC;
REWRITE_ASSUMS[ARITH_RULE `x + 0 = x`];
ONCE_REWRITE_ASSUMS[ARITH_RULE `x * y = y * x:num`];
ASM_MESON_TAC[];
]);;
(* }}} *)
(* }}} *)
let EVEN_PRE = GEN_ALL (CONJUNCT1 (SPEC_ALL PRE_LEM));;
let ODD_PRE = GEN_ALL (CONJUNCT2 (SPEC_ALL PRE_LEM));;
let INFERPSIGN_POS_EVEN = prove_by_refinement(
`!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a <> &0) ==>
EVEN n ==>
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Pos s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `
LENGTH (
APPEND sgns (CONS
(
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) =
LENGTH (
partition_line pts)`;
REWRITE_ALL[interpmat];
ASM_MESON_TAC[
ALL2_LENGTH];
REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
STRIP_TAC;
TYPE_TACL (fun l -> MP_TAC (ISPECL l
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
STRIP_TAC;
LABEL_ALL_TAC;
PROVE_ASSUM_ANTECEDENT_TAC 0;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
ARITH_TAC;
POP_ASSUM MP_TAC THEN STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `~(l2 = [])`;
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
REWRITE_ALL[
APPEND_NIL];
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
REWRITE_TAC[
NOT_NIL];
STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFERPSIGN_POS_EVEN_LEM);
ASM_REWRITE_TAC[];
EXISTS_TACL [`a`;`n`;`s`];
(* save *)
ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_MESON_TAC[];
LABEL_ALL_TAC;
CLAIM `
EVEN (
LENGTH sgns - 1)`;
ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 =
PRE x`];
STRIP_TAC;
ASM_SIMP_TAC[
DIV_EVEN];
USE_THEN "Z-5" MP_TAC THEN ARITH_TAC;
]);;
(* }}} *)
let INFERPSIGN_NEG_EVEN_LEM = prove_by_refinement(
`!a n p ps q qs r rs s x pts1 pts2 s1 s2 s3 rest sgns.
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(
LENGTH sgns = 2 *
LENGTH pts1 + 1) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a <> &0) ==>
EVEN n ==>
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Neg s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `a pow n > &0`;
ASM_MESON_TAC[
EVEN_ODD_POW];
STRIP_TAC;
REPEAT (POP_ASSUM MP_TAC);
REWRITE_TAC[interpmat];
REPEAT STRIP_TAC;
FIRST_ASSUM MATCH_ACCEPT_TAC;
CASES_ON `pts1 = []`;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;];
COND_CASES_TAC;
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 8 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x < &0`;
ASM_MESON_TAC[];
REPEAT_N 6 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 7 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 9 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x < &0`;
ASM_MESON_TAC[];
REPEAT_N 8 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 9 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
REPEAT STRIP_TAC;
CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
(CONS (\x'.
LAST pts1 < x' /\ x' < x)
(
TL (
partition_line (CONS x pts2))))) =
(
APPEND
(
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x])
(
TL (
partition_line (CONS x pts2))))`;
ASM_MESON_TAC[
APPEND_CONS];
DISCH_THEN (REWRITE_ALL o list);
REPEAT (POP_ASSUM MP_TAC);
REWRITE_ALL[
partition_line];
COND_CASES_TAC;
POP_ASSUM (REWRITE_ALL o list);
REPEAT STRIP_TAC;
REWRITE_ALL[
TL;];
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REPEAT_N 9 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
RESTRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x < &0`;
ASM_MESON_TAC[];
REPEAT_N 15 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
(* save *)
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 10 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x < &0`;
ASM_MESON_TAC[];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 17 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT];
]);;
(* }}} *)
let INFERPSIGN_NEG_EVEN = prove_by_refinement(
`!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a <> &0) ==>
EVEN n ==>
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Neg s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `
LENGTH (
APPEND sgns (CONS
(
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) =
LENGTH (
partition_line pts)`;
REWRITE_ALL[interpmat];
ASM_MESON_TAC[
ALL2_LENGTH];
REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
STRIP_TAC;
TYPE_TACL (fun l -> MP_TAC (ISPECL l
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
STRIP_TAC;
LABEL_ALL_TAC;
PROVE_ASSUM_ANTECEDENT_TAC 0;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
ARITH_TAC;
POP_ASSUM MP_TAC THEN STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `~(l2 = [])`;
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
REWRITE_ALL[
APPEND_NIL];
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
REWRITE_TAC[
NOT_NIL];
STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFERPSIGN_NEG_EVEN_LEM);
ASM_REWRITE_TAC[];
EXISTS_TACL [`a`;`n`;`s`];
(* save *)
ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_MESON_TAC[];
LABEL_ALL_TAC;
CLAIM `
EVEN (
LENGTH sgns - 1)`;
ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 =
PRE x`];
STRIP_TAC;
ASM_SIMP_TAC[
DIV_EVEN];
USE_THEN "Z-5" MP_TAC THEN ARITH_TAC;
]);;
(* }}} *)
let INFERPSIGN_ZERO_EVEN_LEM = prove_by_refinement(
`!a n p ps q qs r rs s x pts1 pts2 s1 s2 s3 rest sgns.
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(
LENGTH sgns = 2 *
LENGTH pts1 + 1) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a <> &0) ==>
EVEN n ==>
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Zero s1)
(
APPEND (CONS Zero s2) (CONS Zero s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `a pow n > &0`;
ASM_MESON_TAC[
EVEN_ODD_POW];
STRIP_TAC;
REPEAT (POP_ASSUM MP_TAC);
REWRITE_TAC[interpmat];
REPEAT STRIP_TAC;
FIRST_ASSUM MATCH_ACCEPT_TAC;
CASES_ON `pts1 = []`;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;];
COND_CASES_TAC;
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 8 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x = &0`;
ASM_MESON_TAC[];
REPEAT_N 6 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 7 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 5 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 9 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x = &0`;
ASM_MESON_TAC[];
REPEAT_N 8 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 9 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
REPEAT STRIP_TAC;
CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
(CONS (\x'.
LAST pts1 < x' /\ x' < x)
(
TL (
partition_line (CONS x pts2))))) =
(
APPEND
(
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x])
(
TL (
partition_line (CONS x pts2))))`;
ASM_MESON_TAC[
APPEND_CONS];
DISCH_THEN (REWRITE_ALL o list);
REPEAT (POP_ASSUM MP_TAC);
REWRITE_ALL[
partition_line];
COND_CASES_TAC;
POP_ASSUM (REWRITE_ALL o list);
REPEAT STRIP_TAC;
REWRITE_ALL[
TL;];
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REPEAT_N 9 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
RESTRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x = &0`;
ASM_MESON_TAC[];
REPEAT_N 15 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
(* save *)
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 10 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x = &0`;
ASM_MESON_TAC[];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 17 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
]);;
(* }}} *)
let INFERPSIGN_ZERO_EVEN = prove_by_refinement(
`!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a <> &0) ==>
EVEN n ==>
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Zero s1)
(
APPEND (CONS Zero s2) (CONS Zero s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `
LENGTH (
APPEND sgns (CONS
(
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) =
LENGTH (
partition_line pts)`;
REWRITE_ALL[interpmat];
ASM_MESON_TAC[
ALL2_LENGTH];
REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
STRIP_TAC;
TYPE_TACL (fun l -> MP_TAC (ISPECL l
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
STRIP_TAC;
LABEL_ALL_TAC;
PROVE_ASSUM_ANTECEDENT_TAC 0;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
ARITH_TAC;
POP_ASSUM MP_TAC THEN STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `~(l2 = [])`;
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
REWRITE_ALL[
APPEND_NIL];
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
REWRITE_TAC[
NOT_NIL];
STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFERPSIGN_ZERO_EVEN_LEM);
ASM_REWRITE_TAC[];
EXISTS_TACL [`a`;`n`;`s`];
(* save *)
ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_MESON_TAC[];
LABEL_ALL_TAC;
CLAIM `
EVEN (
LENGTH sgns - 1)`;
ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 =
PRE x`];
STRIP_TAC;
ASM_SIMP_TAC[
DIV_EVEN];
USE_THEN "Z-5" MP_TAC THEN ARITH_TAC;
]);;
(* }}} *)
let INFERPSIGN_POS_ODD_POS_LEM = prove_by_refinement(
`!a n p ps q qs r rs s x pts1 pts2 s1 s2 s3 rest sgns.
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(
LENGTH sgns = 2 *
LENGTH pts1 + 1) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a > &0) ==>
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Pos s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `a pow n > &0`;
ASM_MESON_TAC[
REAL_POW_LT;
real_gt;];
STRIP_TAC;
REPEAT (POP_ASSUM MP_TAC);
REWRITE_TAC[interpmat];
REPEAT STRIP_TAC;
FIRST_ASSUM MATCH_ACCEPT_TAC;
CASES_ON `pts1 = []`;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;];
COND_CASES_TAC;
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 7 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x > &0`;
ASM_MESON_TAC[];
REPEAT_N 5 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 6 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 8 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x > &0`;
ASM_MESON_TAC[];
REPEAT_N 7 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 8 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
REPEAT STRIP_TAC;
CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
(CONS (\x'.
LAST pts1 < x' /\ x' < x)
(
TL (
partition_line (CONS x pts2))))) =
(
APPEND
(
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x])
(
TL (
partition_line (CONS x pts2))))`;
ASM_MESON_TAC[
APPEND_CONS];
DISCH_THEN (REWRITE_ALL o list);
REPEAT (POP_ASSUM MP_TAC);
REWRITE_ALL[
partition_line];
COND_CASES_TAC;
POP_ASSUM (REWRITE_ALL o list);
REPEAT STRIP_TAC;
REWRITE_ALL[
TL;];
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REPEAT_N 8 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
RESTRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x > &0`;
ASM_MESON_TAC[];
REPEAT_N 14 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`;
REAL_MUL_GT];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
(* save *)
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 9 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x > &0`;
ASM_MESON_TAC[];
REPEAT_N 15 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
]);;
(* }}} *)
let INFERPSIGN_POS_ODD_POS = prove_by_refinement(
`!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a > &0) ==>
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Pos s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `
LENGTH (
APPEND sgns (CONS
(
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Pos s3))) rest)) =
LENGTH (
partition_line pts)`;
REWRITE_ALL[interpmat];
ASM_MESON_TAC[
ALL2_LENGTH];
REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
STRIP_TAC;
TYPE_TACL (fun l -> MP_TAC (ISPECL l
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
STRIP_TAC;
LABEL_ALL_TAC;
PROVE_ASSUM_ANTECEDENT_TAC 0;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
ARITH_TAC;
POP_ASSUM MP_TAC THEN STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `~(l2 = [])`;
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
REWRITE_ALL[
APPEND_NIL];
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
REWRITE_TAC[
NOT_NIL];
STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFERPSIGN_POS_ODD_POS_LEM);
ASM_REWRITE_TAC[];
EXISTS_TACL [`a`;`n`;`s`];
(* save *)
ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_MESON_TAC[];
LABEL_ALL_TAC;
CLAIM `
EVEN (
LENGTH sgns - 1)`;
ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 =
PRE x`];
STRIP_TAC;
ASM_SIMP_TAC[
DIV_EVEN];
USE_THEN "Z-4" MP_TAC THEN ARITH_TAC;
]);;
(* }}} *)
let INFERPSIGN_NEG_ODD_POS_LEM = prove_by_refinement(
`!a n p ps q qs r rs s x pts1 pts2 s1 s2 s3 rest sgns.
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(
LENGTH sgns = 2 *
LENGTH pts1 + 1) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a > &0) ==>
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Neg s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `a pow n > &0`;
ASM_MESON_TAC[
REAL_POW_LT;
real_gt;];
STRIP_TAC;
REPEAT (POP_ASSUM MP_TAC);
REWRITE_TAC[interpmat];
REPEAT STRIP_TAC;
FIRST_ASSUM MATCH_ACCEPT_TAC;
CASES_ON `pts1 = []`;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;];
COND_CASES_TAC;
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 7 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x < &0`;
ASM_MESON_TAC[
real_gt];
REPEAT_N 5 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 6 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 8 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x < &0`;
ASM_MESON_TAC[];
REPEAT_N 7 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 8 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
REPEAT STRIP_TAC;
CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
(CONS (\x'.
LAST pts1 < x' /\ x' < x)
(
TL (
partition_line (CONS x pts2))))) =
(
APPEND
(
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x])
(
TL (
partition_line (CONS x pts2))))`;
ASM_MESON_TAC[
APPEND_CONS];
DISCH_THEN (REWRITE_ALL o list);
REPEAT (POP_ASSUM MP_TAC);
REWRITE_ALL[
partition_line];
COND_CASES_TAC;
POP_ASSUM (REWRITE_ALL o list);
REPEAT STRIP_TAC;
REWRITE_ALL[
TL;];
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REPEAT_N 8 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
RESTRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x < &0`;
ASM_MESON_TAC[];
REPEAT_N 14 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`;
REAL_MUL_GT];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
(* save *)
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 9 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x < &0`;
ASM_MESON_TAC[];
REPEAT_N 15 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
]);;
(* }}} *)
let INFERPSIGN_NEG_ODD_POS = prove_by_refinement(
`!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a > &0) ==>
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Neg s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `
LENGTH (
APPEND sgns (CONS
(
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Neg s3))) rest)) =
LENGTH (
partition_line pts)`;
REWRITE_ALL[interpmat];
ASM_MESON_TAC[
ALL2_LENGTH];
REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
STRIP_TAC;
TYPE_TACL (fun l -> MP_TAC (ISPECL l
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
STRIP_TAC;
LABEL_ALL_TAC;
PROVE_ASSUM_ANTECEDENT_TAC 0;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
ARITH_TAC;
POP_ASSUM MP_TAC THEN STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `~(l2 = [])`;
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
REWRITE_ALL[
APPEND_NIL];
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
REWRITE_TAC[
NOT_NIL];
STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFERPSIGN_NEG_ODD_POS_LEM);
ASM_REWRITE_TAC[];
EXISTS_TACL [`a`;`n`;`s`];
(* save *)
ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_MESON_TAC[];
LABEL_ALL_TAC;
CLAIM `
EVEN (
LENGTH sgns - 1)`;
ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 =
PRE x`];
STRIP_TAC;
ASM_SIMP_TAC[
DIV_EVEN];
USE_THEN "Z-4" MP_TAC THEN ARITH_TAC;
]);;
(* }}} *)
let INFERPSIGN_ZERO_ODD_POS_LEM = prove_by_refinement(
`!a n p ps q qs r rs s x pts1 pts2 s1 s2 s3 rest sgns.
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(
LENGTH sgns = 2 *
LENGTH pts1 + 1) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a > &0) ==>
interpmat (
APPEND pts1 (CONS x pts2))
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Zero s1)
(
APPEND (CONS Zero s2) (CONS Zero s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `a pow n > &0`;
ASM_MESON_TAC[
REAL_POW_LT;
real_gt;];
STRIP_TAC;
REPEAT (POP_ASSUM MP_TAC);
REWRITE_TAC[interpmat];
REPEAT STRIP_TAC;
FIRST_ASSUM MATCH_ACCEPT_TAC;
CASES_ON `pts1 = []`;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;];
COND_CASES_TAC;
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 7 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x = &0`;
ASM_MESON_TAC[
real_gt];
REPEAT_N 5 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 6 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
CLAIM `?k. sgns = [k]`;
MATCH_EQ_MP_TAC (GSYM
LENGTH_1);
REWRITE_ALL[
LENGTH];
REPEAT_N 4 (POP_ASSUM (fun x -> ALL_TAC));
POP_ASSUM MP_TAC THEN ARITH_TAC;
STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
APPEND;
partition_line;
ALL2;];
REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
REWRITE_ALL[interpsigns;interpsign;
ALL2;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 8 (POP_ASSUM MP_TAC);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x = &0`;
ASM_MESON_TAC[];
REPEAT_N 7 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 8 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`];
ASM_REWRITE_TAC[];
(* save *)
POP_ASSUM (fun x -> REPEAT (POP_ASSUM MP_TAC) THEN ASSUME_TAC x);
ASM_SIMP_TAC[
PARTITION_LINE_APPEND];
REPEAT STRIP_TAC;
CLAIM `(
APPEND (
BUTLAST (
partition_line pts1))
(CONS (\x'.
LAST pts1 < x' /\ x' < x)
(
TL (
partition_line (CONS x pts2))))) =
(
APPEND
(
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x])
(
TL (
partition_line (CONS x pts2))))`;
ASM_MESON_TAC[
APPEND_CONS];
DISCH_THEN (REWRITE_ALL o list);
REPEAT (POP_ASSUM MP_TAC);
REWRITE_ALL[
partition_line];
COND_CASES_TAC;
POP_ASSUM (REWRITE_ALL o list);
REPEAT STRIP_TAC;
REWRITE_ALL[
TL;];
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REPEAT_N 8 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
RESTRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x = &0`;
ASM_MESON_TAC[];
REPEAT_N 14 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`;
REAL_MUL_GT;
REAL_LT_IMP_NZ];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
(* save *)
CLAIM `
LENGTH (
APPEND (
BUTLAST (
partition_line pts1))
[\x'.
LAST pts1 < x' /\ x' < x]) =
LENGTH sgns`;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_LENGTH);
ASM_SIMP_TAC[
LENGTH_APPEND;
PARTITION_LINE_NOT_NIL;
BUTLAST_LENGTH;
PARTITION_LINE_LENGTH;
LENGTH;];
ARITH_TAC;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REPEAT STRIP_TAC;
MATCH_MP_TAC
ALL2_APPEND;
ASM_REWRITE_TAC[];
(* save *)
REWRITE_ALL[
TL;
ALL2;interpsign;interpsigns;
APPEND];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
REPEAT_N 9 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> POP_ASSUM (fun y -> REPEAT STRIP_TAC THEN ASSUME_TAC x THEN ASSUME_TAC y));
REWRITE_ALL[
ALL2;interpsigns;
APPEND;interpsign;];
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
REPEAT_N 4 (POP_ASSUM MP_TAC);
POP_ASSUM (fun x -> REPEAT STRIP_TAC THEN ASSUME_TAC x);
FIRST_ASSUM (MP_TAC o MATCH_MP
ALL2_APPEND_LENGTH);
FIRST_ASSUM (fun x -> DISCH_THEN (fun y -> MP_TAC (MATCH_MP y x)));
REWRITE_TAC[
ALL2;interpsign;];
REPEAT STRIP_TAC;
REWRITE_ALL[interpsigns;
ALL2;interpsign;];
ASM_REWRITE_TAC[];
CLAIM `q x = &0`;
ASM_MESON_TAC[];
CLAIM `r x = &0`;
ASM_MESON_TAC[];
REPEAT_N 15 (POP_ASSUM MP_TAC);
POP_ASSUM (MP_TAC o ISPEC `x:real`);
REPEAT STRIP_TAC;
POP_ASSUM (REWRITE_ALL o list);
REWRITE_ALL[
REAL_MUL_RZERO;REAL_ADD_LID;];
REPEAT_N 16 (POP_ASSUM MP_TAC);
POP_ASSUM (REWRITE_ALL o list o GSYM);
REWRITE_TAC[
real_gt;
REAL_MUL_GT];
REPEAT STRIP_TAC;
ASM_MESON_TAC[REAL_ARITH `~(x < y /\ y < x)`;
REAL_MUL_LT;
REAL_ENTIRE;ARITH_RULE `x < y ==> ~(x = y)`;
REAL_MUL_GT;
REAL_LT_IMP_NZ];
]);;
(* }}} *)
let INFERPSIGN_ZERO_ODD_POS = prove_by_refinement(
`!a n p ps q qs pts r rs s s1 s2 s3 rest sgns.
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) ==>
(
LENGTH ps =
LENGTH s1) ==>
(
LENGTH qs =
LENGTH s2) ==>
ODD (
LENGTH sgns) ==>
(!x. a pow n * p x = s x * q x + r x) ==>
(a > &0) ==>
interpmat pts
(
APPEND (CONS p ps) (
APPEND (CONS q qs) (CONS r rs)))
(
APPEND sgns
(CONS (
APPEND (CONS Zero s1)
(
APPEND (CONS Zero s2) (CONS Zero s3))) rest))`,
(* {{{ Proof *)
[
REPEAT STRIP_TAC;
CLAIM `
LENGTH (
APPEND sgns (CONS
(
APPEND (CONS Unknown s1)
(
APPEND (CONS Zero s2) (CONS Zero s3))) rest)) =
LENGTH (
partition_line pts)`;
REWRITE_ALL[interpmat];
ASM_MESON_TAC[
ALL2_LENGTH];
REWRITE_TAC[
LENGTH_APPEND;
PARTITION_LINE_LENGTH;
LENGTH;];
STRIP_TAC;
TYPE_TACL (fun l -> MP_TAC (ISPECL l
SPLIT_LIST_THM)) [`(
LENGTH sgns - 1) DIV 2`;`pts`];
STRIP_TAC;
LABEL_ALL_TAC;
PROVE_ASSUM_ANTECEDENT_TAC 0;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC;
ARITH_TAC;
POP_ASSUM MP_TAC THEN STRIP_TAC;
ASM_REWRITE_TAC[];
CLAIM `~(l2 = [])`;
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
REWRITE_ALL[
APPEND_NIL];
POP_ASSUM (REWRITE_ALL o list);
POP_ASSUM (fun x -> ALL_TAC);
DISCH_THEN (REWRITE_ALL o list);
POP_ASSUM MP_TAC;
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM (fun x -> ALL_TAC);
POP_ASSUM MP_TAC THEN ARITH_TAC;
REWRITE_TAC[
NOT_NIL];
STRIP_TAC THEN POP_ASSUM (REWRITE_ALL o list);
MATCH_MP_TAC (REWRITE_RULE[IMP_AND_THM]
INFERPSIGN_ZERO_ODD_POS_LEM);
ASM_REWRITE_TAC[];
EXISTS_TACL [`a`;`n`;`s`];
(* save *)
ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_MESON_TAC[];
LABEL_ALL_TAC;
CLAIM `
EVEN (
LENGTH sgns - 1)`;
ASM_MESON_TAC[EVEN_PRE;ARITH_RULE `x - 1 =
PRE x`];
STRIP_TAC;
ASM_SIMP_TAC[
DIV_EVEN];
USE_THEN "Z-4" MP_TAC THEN ARITH_TAC;
]);;
(* }}} *)