(* ========================================================================= *)
(* Implementation of Cooper's algorithm via proforma theorems. *)
(* ========================================================================= *)
prioritize_int();;
(* ------------------------------------------------------------------------- *)
(* Basic syntax on integer terms. *)
(* ------------------------------------------------------------------------- *)
let dest_mul = dest_binop `(*)`;;
let dest_add = dest_binop `(+)`;;
(* ------------------------------------------------------------------------- *)
(* Divisibility. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("divides",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* Trivial lemmas about integers. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Trivial lemmas about divisibility. *)
(* ------------------------------------------------------------------------- *)
let DIVIDES_LMUL = prove
(`!d a x. d divides a ==> d divides (x * a)`,
ASM_MESON_TAC[divides; INT_ARITH `a * b * c = b * a * c`]);;
let INT_MOD_LEMMA = prove
(`!d x. &0 < d ==> ?c. &1 <= x + c * d /\ x + c * d <= d`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(MP_TAC o SPECL [`x:int`; `&0`] o MATCH_MP
INT_DOWN_MUL_LT) THEN
DISCH_THEN(X_CHOOSE_TAC `c0:int`) THEN
SUBGOAL_THEN `?c1. &0 <= c1 /\ --(x + c0 * d) < c1 * d` MP_TAC THENL
[SUBGOAL_THEN `?c1. --(x + c0 * d) < c1 * d` MP_TAC THENL
[ASM_MESON_TAC[
INT_ARCH; INT_ARITH `&0 < d ==> ~(d = &0)`]; ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN SIMP_TAC[] THEN
MATCH_MP_TAC(INT_ARITH
`(&0 < --c1 ==> &0 < --cd) /\ xcod < &0
==> --xcod < cd ==> &0 <= c1`) THEN
ASM_SIMP_TAC[GSYM
INT_MUL_LNEG;
INT_LT_MUL]; ALL_TAC] THEN
REWRITE_TAC[TAUT `a /\ b <=> ~(a ==> ~b)`; GSYM
NOT_FORALL_THM] THEN
REWRITE_TAC[GSYM
INT_FORALL_POS] THEN
REWRITE_TAC[
NOT_FORALL_THM] THEN GEN_REWRITE_TAC LAND_CONV [
num_WOP] THEN
REWRITE_TAC[INT_ARITH `--(x + a * d) < b * d <=> &1 <= x + (a + b) * d`] THEN
DISCH_THEN(X_CHOOSE_THEN `n:num` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `c0 + &n` THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
UNDISCH_TAC `&1 <= x + (c0 + &n) * d` THEN SPEC_TAC(`n:num`,`n:num`) THEN
INDUCT_TAC THEN REWRITE_TAC[ARITH_RULE `SUC n - 1 = n`] THENL
[REWRITE_TAC[
SUB_0;
LT_REFL;
INT_ADD_RID] THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN INT_ARITH_TAC;
REWRITE_TAC[GSYM
INT_OF_NUM_SUC;
LT] THEN INT_ARITH_TAC]);;
let interp = new_recursive_definition cform_RECURSION
`(interp x (Lt e) <=> x + e < &0) /\
(interp x (Gt e) <=> x + e > &0) /\
(interp x (Eq e) <=> (x + e = &0)) /\
(interp x (Ne e) <=> ~(x + e = &0)) /\
(interp x (Divides c e) <=> c divides (x + e)) /\
(interp x (Ndivides c e) <=> ~(c divides (x + e))) /\
(interp x (And p q) <=> interp x p /\ interp x q) /\
(interp x (Or p q) <=> interp x p \/ interp x q) /\
(interp x (Nox P) <=> P)`;;
let minusinf = new_recursive_definition cform_RECURSION
`(minusinf (Lt e) = Nox T) /\
(minusinf (Gt e) = Nox F) /\
(minusinf (Eq e) = Nox F) /\
(minusinf (Ne e) = Nox T) /\
(minusinf (Divides c e) = Divides c e) /\
(minusinf (Ndivides c e) = Ndivides c e) /\
(minusinf (And p q) = And (minusinf p) (minusinf q)) /\
(minusinf (Or p q) = Or (minusinf p) (minusinf q)) /\
(minusinf (Nox P) = Nox P)`;;
let plusinf = new_recursive_definition cform_RECURSION
`(plusinf (Lt e) = Nox F) /\
(plusinf (Gt e) = Nox T) /\
(plusinf (Eq e) = Nox F) /\
(plusinf (Ne e) = Nox T) /\
(plusinf (Divides c e) = Divides c e) /\
(plusinf (Ndivides c e) = Ndivides c e) /\
(plusinf (And p q) = And (plusinf p) (plusinf q)) /\
(plusinf (Or p q) = Or (plusinf p) (plusinf q)) /\
(plusinf (Nox P) = Nox P)`;;
let alldivide = new_recursive_definition cform_RECURSION
`(alldivide d (Lt e) <=> T) /\
(alldivide d (Gt e) <=> T) /\
(alldivide d (Eq e) <=> T) /\
(alldivide d (Ne e) <=> T) /\
(alldivide d (Divides c e) <=> c divides d) /\
(alldivide d (Ndivides c e) <=> c divides d) /\
(alldivide d (And p q) <=> alldivide d p /\ alldivide d q) /\
(alldivide d (Or p q) <=> alldivide d p /\ alldivide d q) /\
(alldivide d (Nox P) <=> T)`;;
let aset = new_recursive_definition cform_RECURSION
`(aset (Lt e) = {(--e)}) /\
(aset (Gt e) = {}) /\
(aset (Eq e) = {(--e + &1)}) /\
(aset (Ne e) = {(--e)}) /\
(aset (Divides c e) = {}) /\
(aset (Ndivides c e) = {}) /\
(aset (And p q) = (aset p) UNION (aset q)) /\
(aset (Or p q) = (aset p) UNION (aset q)) /\
(aset (Nox P) = {})`;;let bset = new_recursive_definition cform_RECURSION
`(bset (Lt e) = {}) /\
(bset (Gt e) = {(--e)}) /\
(bset (Eq e) = {(--(e + &1))}) /\
(bset (Ne e) = {(--e)}) /\
(bset (Divides c e) = {}) /\
(bset (Ndivides c e) = {}) /\
(bset (And p q) = (bset p) UNION (bset q)) /\
(bset (Or p q) = (bset p) UNION (bset q)) /\
(bset (Nox P) = {})`;;let INT_EXISTS_CASES = prove
(`(?x. P x) <=> (!y. ?x. x < y /\ P x) \/ (?x. P x /\ !y. y < x ==> ~P y)`,
EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
DISCH_THEN(X_CHOOSE_TAC `x:int`) THEN
MATCH_MP_TAC(TAUT `(~b ==> a) ==> a \/ b`) THEN
REWRITE_TAC[
NOT_EXISTS_THM; TAUT `~(p /\ q) <=> p ==> ~q`;
NOT_FORALL_THM;
NOT_IMP] THEN
STRIP_TAC THEN X_GEN_TAC `y:int` THEN
DISJ_CASES_TAC(INT_ARITH `x < y \/ &0 <= x - y`) THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `!n. ?y. y < x - &n /\ P y` MP_TAC THENL
[ALL_TAC;
REWRITE_TAC[
INT_FORALL_POS] THEN
DISCH_THEN(MP_TAC o SPEC `x - y`) THEN
ASM_REWRITE_TAC[INT_ARITH `x - (x - y) = y`]] THEN
INDUCT_TAC THEN
REWRITE_TAC[
INT_SUB_RZERO; GSYM
INT_OF_NUM_SUC] THEN
ASM_MESON_TAC[INT_ARITH `z < y /\ y < x - &n ==> z < x - (&n + &1)`]);;
let MINUSINF_REPEATS = prove
(`!p c d x. alldivide d p
==> (interp x (minusinf p) <=> interp (x + c * d) (minusinf p))`,
CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN MATCH_MP_TAC cform_INDUCT THEN
SIMP_TAC[interp; minusinf; alldivide] THEN
ONCE_REWRITE_TAC[INT_ARITH `(x + d) + y = (x + y) + d`] THEN
MESON_TAC[
DIVIDES_LMUL;
DIVIDES_ADD_REVL;
DIVIDES_ADD]);;
let NOMINIMAL_EQUIV = prove
(`alldivide d p /\ &0 < d
==> ((!y. ?x. x < y /\ interp x p) <=>
?j. &1 <= j /\ j <= d /\ interp j (minusinf p))`,
let BDISJ_REPEATS_LEMMA = prove
(`!d p. alldivide d p /\ &0 < d
==> !x. interp x p /\ ~(interp (x - d) p)
==> ?j b. &1 <= j /\ j <= d /\ b
IN bset p /\ (x = b + j)`,
GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `a /\ b ==> c <=> b ==> a ==> c`] THEN
REWRITE_TAC[
RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
MATCH_MP_TAC cform_INDUCT THEN
REWRITE_TAC[interp; alldivide; bset;
NOT_IN_EMPTY] THEN
MATCH_MP_TAC(TAUT `(a /\ b /\ c /\ d /\ e /\ f) /\ g /\ h
==> a /\ b /\ c /\ d /\ e /\ f /\ g /\ h`) THEN
CONJ_TAC THENL
[ALL_TAC;
SIMP_TAC[TAUT `~a \/ a`;
TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`;
TAUT `a /\ (b \/ c) <=> a /\ b \/ a /\ c`;
TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`;
DE_MORGAN_THM;
IN_UNION;
EXISTS_OR_THM;
FORALL_AND_THM]] THEN
REPEAT STRIP_TAC THENL
[ALL_TAC;
MAP_EVERY EXISTS_TAC [`x + a`; `--a`];
MAP_EVERY EXISTS_TAC [`&1`; `--a - &1`];
MAP_EVERY EXISTS_TAC [`d:int`; `--a`];
ASM_MESON_TAC[INT_ARITH `(x - y) + z = (x + z) - y`;
DIVIDES_SUB];
ASM_MESON_TAC[INT_ARITH `(x - y) + z = (x + z) - y`;
INT_ARITH `(x - y) + y = x`;
DIVIDES_ADD]] THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
REWRITE_TAC[
IN_SING] THEN INT_ARITH_TAC);;
let MAINTHM_B = prove
(`!p d. alldivide d p /\ &0 < d
==> ((?x. interp x p) <=>
?j. &1 <= j /\ j <= d /\
(interp j (minusinf p) \/
?b. b
IN bset p /\ interp (b + j) p))`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
REWRITE_TAC[TAUT `a /\ (b \/ c) <=> a /\ b \/ a /\ c`;
EXISTS_OR_THM] THEN
MATCH_MP_TAC(TAUT
`!a1 a2. (a <=> a1 \/ a2) /\ (a1 <=> b) /\ (a2 ==> c) /\ (c ==> a)
==> (a <=> b \/ c)`) THEN
EXISTS_TAC `!y. ?x. x < y /\ interp x p` THEN
EXISTS_TAC `?x. interp x p /\ !y. y < x ==> ~(interp y p)` THEN
REPEAT CONJ_TAC THENL
[REWRITE_TAC[GSYM
INT_EXISTS_CASES];
ASM_MESON_TAC[
NOMINIMAL_EQUIV];
ALL_TAC;
MESON_TAC[]] THEN
DISCH_THEN(X_CHOOSE_THEN `x:int`
(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `x - d`))) THEN
ASM_SIMP_TAC[INT_ARITH `&0 < d ==> x - d < x`] THEN
DISCH_TAC THEN
MP_TAC(SPECL [`d:int`; `p:cform`]
BDISJ_REPEATS_LEMMA) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPEC `x:int`) THEN ASM_MESON_TAC[]);;
let mirror = new_recursive_definition cform_RECURSION
`(mirror (Lt e) = Gt(--e)) /\
(mirror (Gt e) = Lt(--e)) /\
(mirror (Eq e) = Eq(--e)) /\
(mirror (Ne e) = Ne(--e)) /\
(mirror (Divides c e) = Divides c (--e)) /\
(mirror (Ndivides c e) = Ndivides c (--e)) /\
(mirror (And p q) = And (mirror p) (mirror q)) /\
(mirror (Or p q) = Or (mirror p) (mirror q)) /\
(mirror (Nox P) = Nox P)`;;
let MINUSINF_MIRROR = prove
(`!p. minusinf (mirror p) = mirror (plusinf p)`,
MATCH_MP_TAC cform_INDUCT THEN SIMP_TAC[plusinf; minusinf; mirror]);;
let ALLDIVIDE_MIRROR = prove
(`!p d. alldivide d (mirror p) = alldivide d p`,
MATCH_MP_TAC cform_INDUCT THEN SIMP_TAC[mirror; alldivide]);;
let EXISTS_MOD_IMP = prove
(`!P d. (!c x. P(x + c * d) <=> P(x)) /\ (?j. &1 <= j /\ j <= d /\ P(--j))
==> ?j. &1 <= j /\ j <= d /\ P(j)`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `d:int = j` THENL
[FIRST_X_ASSUM(MP_TAC o SPECL [`--(&2)`; `d:int`]) THEN
ASM_REWRITE_TAC[INT_ARITH `d + --(&2) * d = --d`] THEN
ASM_MESON_TAC[
INT_LE_REFL];
FIRST_X_ASSUM(MP_TAC o SPECL [`&1`; `--j`]) THEN
ASM_REWRITE_TAC[INT_ARITH `--j + &1 * d = d - j`] THEN
DISCH_TAC THEN EXISTS_TAC `d - j` THEN ASM_REWRITE_TAC[] THEN
MAP_EVERY UNDISCH_TAC [`&1 <= j`; `j <= d`; `~(d:int = j)`] THEN
INT_ARITH_TAC]);;
let EXISTS_MOD_EQ = prove
(`!P d. (!c x. P(x + c * d) <=> P(x))
==> ((?j. &1 <= j /\ j <= d /\ P(--j)) <=>
(?j. &1 <= j /\ j <= d /\ P(j)))`,
REPEAT STRIP_TAC THEN EQ_TAC THENL
[MP_TAC(SPEC `P:int->bool`
EXISTS_MOD_IMP);
MP_TAC(SPEC `\x. P(--x):bool`
EXISTS_MOD_IMP)] THEN
DISCH_THEN(MP_TAC o SPEC `d:int`) THEN ASM_REWRITE_TAC[
INT_NEG_NEG] THEN
ASM_REWRITE_TAC[INT_ARITH `--(x + c * d) = --x + --c * d`;
FORALL_NEG] THEN
MESON_TAC[]);;
let MAINTHM_A = prove
(`!p d. alldivide d p /\ &0 < d
==> ((?x. interp x p) <=>
?j. &1 <= j /\ j <= d /\
(interp j (plusinf p) \/
?a. a
IN aset p /\ interp (a - j) p))`,
let pth0 = prove
(`(&0 * &x = &0) /\
(&0 * --(&x) = &0) /\
(&x * &0 = &0) /\
(--(&x) * &0 = &0)`,
REWRITE_TAC[
INT_MUL_LZERO;
INT_MUL_RZERO])
and pth1,pth2 = (CONJ_PAIR o
prove)
(`((&m * &n = &(m * n)) /\
(--(&m) * --(&n) = &(m * n))) /\
((--(&m) * &n = --(&(m * n))) /\
(&m * --(&n) = --(&(m * n))))`,
REWRITE_TAC[
INT_MUL_LNEG;
INT_MUL_RNEG;
INT_NEG_NEG] THEN
REWRITE_TAC[
INT_OF_NUM_MUL]) in
FIRST_CONV
[GEN_REWRITE_CONV I [pth0];
GEN_REWRITE_CONV I [pth1] THENC RAND_CONV NUM_MULT_CONV;
GEN_REWRITE_CONV I [pth2] THENC RAND_CONV(RAND_CONV NUM_MULT_CONV)];;
let pth0 = prove
(`(--(&m) + &m = &0) /\
(&m + --(&m) = &0)`,
REWRITE_TAC[
INT_ADD_LINV;
INT_ADD_RINV]) in
let [pth1; pth2; pth3; pth4; pth5; pth6] = (CONJUNCTS o
prove)
(`(--(&m) + --(&n) = --(&(m + n))) /\
(--(&m) + &(m + n) = &n) /\
(--(&(m + n)) + &m = --(&n)) /\
(&(m + n) + --(&m) = &n) /\
(&m + --(&(m + n)) = --(&n)) /\
(&m + &n = &(m + n))`,
REWRITE_TAC[GSYM
INT_OF_NUM_ADD;
INT_NEG_ADD] THEN
REWRITE_TAC[
INT_ADD_ASSOC;
INT_ADD_LINV;
INT_ADD_LID] THEN
REWRITE_TAC[
INT_ADD_RINV;
INT_ADD_LID] THEN
ONCE_REWRITE_TAC[
INT_ADD_SYM] THEN
REWRITE_TAC[
INT_ADD_ASSOC;
INT_ADD_LINV;
INT_ADD_LID] THEN
REWRITE_TAC[
INT_ADD_RINV;
INT_ADD_LID]) in
GEN_REWRITE_CONV I [pth0] ORELSEC
(fun tm ->
try let l,r = dest tm in
if rator l = neg_tm then
if rator r = neg_tm then
let th1 = INST [rand(rand l),m_tm; rand(rand r),n_tm] pth1 in
let tm1 = rand(rand(rand(concl th1))) in
let th2 = AP_TERM neg_tm (AP_TERM amp_tm (NUM_ADD_CONV tm1)) in
TRANS th1 th2
else
let m = rand(rand l) and n = rand r in
let m' = dest_numeral m and n' = dest_numeral n in
if m' <=/ n' then
let p = mk_numeral (n' -/ m') in
let th1 = INST [m,m_tm; p,n_tm] pth2 in
let th2 = NUM_ADD_CONV (rand(rand(lhand(concl th1)))) in
let th3 = AP_TERM (rator tm) (AP_TERM amp_tm (SYM th2)) in
TRANS th3 th1
else
let p = mk_numeral (m' -/ n') in
let th1 = INST [n,m_tm; p,n_tm] pth3 in
let th2 = NUM_ADD_CONV (rand(rand(lhand(lhand(concl th1))))) in
let th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) in
let th4 = AP_THM (AP_TERM add_tm th3) (rand tm) in
TRANS th4 th1
else
if rator r = neg_tm then
let m = rand l and n = rand(rand r) in
let m' = dest_numeral m and n' = dest_numeral n in
if n' <=/ m' then
let p = mk_numeral (m' -/ n') in
let th1 = INST [n,m_tm; p,n_tm] pth4 in
let th2 = NUM_ADD_CONV (rand(lhand(lhand(concl th1)))) in
let th3 = AP_TERM add_tm (AP_TERM amp_tm (SYM th2)) in
let th4 = AP_THM th3 (rand tm) in
TRANS th4 th1
else
let p = mk_numeral (n' -/ m') in
let th1 = INST [m,m_tm; p,n_tm] pth5 in
let th2 = NUM_ADD_CONV (rand(rand(rand(lhand(concl th1))))) in
let th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) in
let th4 = AP_TERM (rator tm) th3 in
TRANS th4 th1
else
let th1 = INST [rand l,m_tm; rand r,n_tm] pth6 in
let tm1 = rand(rand(concl th1)) in
let th2 = AP_TERM amp_tm (NUM_ADD_CONV tm1) in
TRANS th1 th2
with Failure _ -> failwith "INT_ADD_CONV");;
let tth = prove
(`((if T then x:int else y) = x) /\ ((if F then x:int else y) = y)`,
REWRITE_TAC[]) in
let neg_tm = `(--)` in
(GEN_REWRITE_CONV I [pth1] THENC RAND_CONV NUM_EXP_CONV) ORELSEC
(GEN_REWRITE_CONV I [pth2] THENC
RATOR_CONV(RATOR_CONV(RAND_CONV NUM_EVEN_CONV)) THENC
GEN_REWRITE_CONV I [tth] THENC
(fun tm -> if rator tm = neg_tm then RAND_CONV(RAND_CONV NUM_EXP_CONV) tm
else RAND_CONV NUM_EXP_CONV tm));;
let sth = prove
(`(!x y z. x + (y + z) = (x + y) + z) /\
(!x y. x + y = y + x) /\
(!x. &0 + x = x) /\
(!x y z. x * (y * z) = (x * y) * z) /\
(!x y. x * y = y * x) /\
(!x. &1 * x = x) /\
(!x. &0 * x = &0) /\
(!x y z. x * (y + z) = x * y + x * z) /\
(!x. x pow 0 = &1) /\
(!x n. x pow (SUC n) = x * x pow n)`,
REWRITE_TAC[
INT_POW] THEN INT_ARITH_TAC)
and rth =
prove
(`(!x. --x = --(&1) * x) /\
(!x y. x - y = x + --(&1) * y)`,
INT_ARITH_TAC)
and is_semiring_constant = is_int_const
and SEMIRING_ADD_CONV = INT_ADD_CONV
and SEMIRING_MUL_CONV = INT_MUL_CONV
and SEMIRING_POW_CONV = INT_POW_CONV in
let NORMALIZERS =
SEMIRING_NORMALIZERS_CONV sth rth
(is_semiring_constant,
SEMIRING_ADD_CONV,SEMIRING_MUL_CONV,SEMIRING_POW_CONV) in
fun vars -> NORMALIZERS(earlier vars);;
let pth_divides = prove
(`~(d = &0) ==> (c divides e <=> (d * c) divides (d * e))`,
SIMP_TAC[divides; GSYM
INT_MUL_ASSOC;
INT_EQ_MUL_LCANCEL])
and pth_eq =
prove
(`~(d = &0) ==> ((&0 = e) <=> (&0 = d * e))`,
DISCH_TAC THEN CONV_TAC(BINOP_CONV SYM_CONV) THEN
ASM_REWRITE_TAC[
INT_ENTIRE])
and pth_lt_pos =
prove
(`&0 < d ==> (&0 < e <=> &0 < d * e)`,
DISCH_TAC THEN SUBGOAL_THEN `&0 < e <=> d * &0 < d * e` SUBST1_TAC THENL
[ASM_SIMP_TAC[
INT_LT_LMUL_EQ]; REWRITE_TAC[
INT_MUL_RZERO]])
and pth_gt_pos =
prove
(`&0 < d ==> (&0 > e <=> &0 > d * e)`,
DISCH_TAC THEN REWRITE_TAC[
INT_GT] THEN
SUBGOAL_THEN `e < &0 <=> d * e < d * &0` SUBST1_TAC THENL
[ASM_SIMP_TAC[
INT_LT_LMUL_EQ]; REWRITE_TAC[
INT_MUL_RZERO]])
and true_tm = `T` and false_tm = `F` in
let pth_lt_neg = prove
(`d < &0 ==> (&0 < e <=> &0 > d * e)`,
REWRITE_TAC[INT_ARITH `&0 > d * e <=> &0 < --d * e`;
INT_ARITH `d < &0 <=> &0 < --d`; pth_lt_pos])
and pth_gt_neg = prove
(`d < &0 ==> (&0 > e <=> &0 < d * e)`,
REWRITE_TAC[INT_ARITH `&0 < d * e <=> &0 > --d * e`;
INT_ARITH `d < &0 <=> &0 < --d`; pth_gt_pos]) in
let rec ADJUSTCOEFF_CONV vars l tm =
if tm = true_tm or tm = false_tm then REFL tm
else if is_exists tm or is_forall tm then
BINDER_CONV (ADJUSTCOEFF_CONV vars l) tm
else if is_neg tm then
RAND_CONV (ADJUSTCOEFF_CONV vars l) tm
else if is_conj tm or is_disj tm or is_imp tm or is_iff tm then
BINOP_CONV (ADJUSTCOEFF_CONV vars l) tm
else
let lop,t = dest_comb tm in
let op,z = dest_comb lop in
let c = coefficient (hd vars) t in
if c =/ Int 0 then REFL tm else
let th1 =
if c =/ l then REFL tm else
let m = l // c in
let th0 = if op = op_eq then pth_eq
else if op = op_divides then pth_divides
else if op = op_lt then
if m >/ Int 0 then pth_lt_pos else pth_lt_neg
else if op = op_gt then
if m >/ Int 0 then pth_gt_pos else pth_gt_neg
else failwith "ADJUSTCOEFF_CONV: unknown predicate" in
let th1 = INST [mk_int_const m,d_tm; z,c_tm; t,e_tm] th0 in
let tm1 = lhand(concl th1) in
let th2 = if is_neg tm1 then EQF_ELIM(INT_EQ_CONV(rand tm1))
else EQT_ELIM(INT_LT_CONV tm1) in
let th3 = MP th1 th2 in
if op = op_divides then
let th3 = MP th1 th2 in
let tm2 = rand(concl th3) in
let l,r = dest_comb tm2 in
let th4 = AP_TERM (rator l) (INT_MUL_CONV (rand l)) in
let th5 = AP_THM th4 r in
let tm3 = rator(rand(concl th5)) in
let th6 = TRANS th5 (AP_TERM tm3 (LINEAR_CMUL vars m t)) in
TRANS th3 th6
else
let tm2 = rator(rand(concl th3)) in
TRANS th3 (AP_TERM tm2 (LINEAR_CMUL vars m t)) in
if l =/ Int 1 then
CONV_RULE(funpow 2 RAND_CONV (MULTIPLY_1_CONV vars)) th1
else th1 in
ADJUSTCOEFF_CONV;;
let pth_trivial = prove
(`P = interp x (Nox P)`,
REWRITE_TAC[interp])
and pth_composite =
prove
(`(interp x p /\ interp x q <=> interp x (And p q)) /\
(interp x p \/ interp x q <=> interp x (Or p q))`,
REWRITE_TAC[interp])
and pth_literal_nontrivial =
prove
(`(&0 > x + e <=> interp x (Lt e)) /\
(&0 < x + e <=> interp x (Gt e)) /\
((&0 = x + e) <=> interp x (Eq e)) /\
(~(&0 = x + e) <=> interp x (Ne e)) /\
(c divides (x + e) <=> interp x (Divides c e)) /\
(~(c divides (x + e)) <=> interp x (Ndivides c e))`,
REWRITE_TAC[interp;
INT_ADD_RID] THEN INT_ARITH_TAC)
and pth_literal_trivial =
prove
(`(&0 > x <=> interp x (Lt(&0))) /\
(&0 < x <=> interp x (Gt(&0))) /\
((&0 = x) <=> interp x (Eq(&0))) /\
(~(&0 = x) <=> interp x (Ne(&0))) /\
(c divides x <=> interp x (Divides c (&0))) /\
(~(c divides x) <=> interp x (Ndivides c (&0)))`,
REWRITE_TAC[interp;
INT_ADD_RID] THEN INT_ARITH_TAC) in
let rewr_composite = GEN_REWRITE_CONV I [pth_composite]
and rewr_literal = GEN_REWRITE_CONV I [pth_literal_nontrivial] ORELSEC
GEN_REWRITE_CONV I [pth_literal_trivial]
and x_tm = `x:int` and p_tm = `P:bool` in
let rec SHADOW_CONV x tm =
if not (mem x (frees tm)) then
INST [tm,p_tm; x,x_tm]
pth_trivial
else if is_conj tm or is_disj tm then
let l,r = try dest_conj tm with Failure _ -> dest_disj tm in
let thl = SHADOW_CONV x l and thr = SHADOW_CONV x r in
let th1 = MK_COMB(AP_TERM (rator(rator tm)) thl,thr) in
TRANS th1 (rewr_composite(rand(concl th1)))
else rewr_literal tm in
fun tm ->
let x,bod = dest_exists tm in
MK_EXISTS x (SHADOW_CONV x bod);;
let pth = prove
(`(p * m = n) ==> &p divides &n`,
DISCH_THEN(SUBST1_TAC o SYM) THEN
REWRITE_TAC[divides] THEN EXISTS_TAC `&m` THEN
REWRITE_TAC[
INT_OF_NUM_MUL])
and m_tm = `m:num` and n_tm = `n:num` and p_tm = `p:num` in
fun tm ->
let n = rand(rand tm)
and p = rand(lhand tm) in
let m = mk_numeral(dest_numeral n // dest_numeral p) in
let th1 = INST [m,m_tm; n,n_tm; p,p_tm] pth in
EQT_INTRO(MP th1 (NUM_MULT_CONV (lhand(lhand(concl th1)))));;
let pth = prove
(`(&p divides &n) <=> (p = 0) /\ (n = 0) \/ ~(p = 0) /\ (n MOD p = 0)`,
REWRITE_TAC[
INT_DIVIDES_NUM] THEN
ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[
MULT_CLAUSES] THEN EQ_TAC THENL
[ASM_MESON_TAC[MOD_MULT];
DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP
DIVISION) THEN
ASM_REWRITE_TAC[
ADD_CLAUSES] THEN MESON_TAC[
MULT_SYM]]) in
GEN_REWRITE_CONV I [pth] THENC NUM_REDUCE_CONV;;
let pth_atom = prove
(`(alldivide d (Lt e) <=> T) /\
(alldivide d (Gt e) <=> T) /\
(alldivide d (Eq e) <=> T) /\
(alldivide d (Ne e) <=> T) /\
(alldivide d (Nox P) <=> T)`,
REWRITE_TAC[alldivide])
and pth_div =
prove
(`(alldivide d (Divides c e) <=> c divides d) /\
(alldivide d (Ndivides c e) <=> c divides d)`,
REWRITE_TAC[alldivide])
and pth_comp =
prove
(`(alldivide d (And p q) <=> alldivide d p /\ alldivide d q) /\
(alldivide d (Or p q) <=> alldivide d p /\ alldivide d q)`,
REWRITE_TAC[alldivide])
and pth_taut = TAUT `(T /\ T <=> T)` in
let basnet =
itlist (fun th -> enter [] (lhand(concl th),REWR_CONV th))
(CONJUNCTS
pth_atom)
(itlist (fun th -> enter [] (lhand(concl th),
REWR_CONV th THENC PROVE_DIVIDES_CONV))
(CONJUNCTS pth_div) empty_net)
and comp_rewr = GEN_REWRITE_CONV I [pth_comp] in
let rec alldivide_conv tm =
try tryfind (fun f -> f tm) (lookup tm basnet) with Failure _ ->
let th = (comp_rewr THENC BINOP_CONV alldivide_conv) tm in
TRANS th pth_taut in
alldivide_conv;;
let pth_false = prove
(`((?b. b
IN bset (Lt e) /\ P b) <=> F) /\
((?b. b
IN bset (Divides c e) /\ P b) <=> F) /\
((?b. b
IN bset (Ndivides c e) /\ P b) <=> F) /\
((?b. b
IN bset(Nox Q) /\ P b) <=> F)`,
REWRITE_TAC[bset;
NOT_IN_EMPTY])
and pth_neg =
prove
(`((?b. b
IN bset (Gt e) /\ P b) <=> P(--e)) /\
((?b. b
IN bset (Ne e) /\ P b) <=> P(--e))`,
REWRITE_TAC[bset;
IN_SING;
INT_MUL_LID;
UNWIND_THM2])
and pth_add =
prove
(`(?b. b
IN bset (Eq e) /\ P b) <=> P(--(e + &1))`,
REWRITE_TAC[bset;
IN_SING;
INT_MUL_LID;
UNWIND_THM2])
and pth_comp =
prove
(`((?b. b
IN bset (And p q) /\ P b) <=>
(?b. b
IN bset p /\ P b) \/
(?b. b
IN bset q /\ P b)) /\
((?b. b
IN bset (Or p q) /\ P b) <=>
(?b. b
IN bset p /\ P b) \/
(?b. b
IN bset q /\ P b))`,
REWRITE_TAC[bset;
IN_UNION] THEN MESON_TAC[])
and taut = TAUT `(F \/ P <=> P) /\ (P \/ F <=> P)` in
let conv_neg vars =
LAND_CONV(LAND_CONV(POLYNOMIAL_NEG_CONV vars))
and conv_add vars =
LAND_CONV(LAND_CONV(RAND_CONV(POLYNOMIAL_ADD_CONV vars) THENC
POLYNOMIAL_NEG_CONV vars))
and conv_comp = GEN_REWRITE_CONV I [pth_comp] in
let net1 =
itlist (fun th -> enter [] (lhand(concl th),K (REWR_CONV th)))
(CONJUNCTS
pth_false) empty_net in
let net2 =
itlist (fun th -> enter [] (lhand(concl th),
let cnv = K (REWR_CONV th) in fun v -> cnv v THENC conv_neg v))
(CONJUNCTS pth_neg) net1 in
let basnet =
enter [] (lhand(concl pth_add),
let cnv = K (REWR_CONV pth_add) in fun v -> cnv v THENC conv_add v)
net2 in
let rec baseconv vars tm =
try tryfind (fun f -> f vars tm) (lookup tm basnet) with Failure _ ->
(conv_comp THENC BINOP_CONV (baseconv vars)) tm in
let finconv =
GEN_REWRITE_CONV DEPTH_CONV [taut] THENC
PURE_REWRITE_CONV [
DISJ_ACI] in
fun vars tm -> (baseconv vars THENC finconv) tm;;
let pth_trivial = prove
(`interp x (Nox P) <=> P`,
REWRITE_TAC[interp])
and pth_comp =
prove
(`(interp x (And p q) <=> interp x p /\ interp x q) /\
(interp x (Or p q) <=> interp x p \/ interp x q)`,
REWRITE_TAC[interp])
and pth_pos,pth_neg = (CONJ_PAIR o
prove)
(`((interp x (Lt e) <=> &0 > x + e) /\
(interp x (Gt e) <=> &0 < x + e) /\
(interp x (Eq e) <=> (&0 = x + e)) /\
(interp x (Divides c e) <=> c divides (x + e))) /\
((interp x (Ne e) <=> ~(&0 = x + e)) /\
(interp x (Ndivides c e) <=> ~(c divides (x + e))))`,
REWRITE_TAC[interp] THEN INT_ARITH_TAC) in
let conv_pos vars = RAND_CONV(POLYNOMIAL_ADD_CONV vars)
and conv_neg vars = RAND_CONV(RAND_CONV(POLYNOMIAL_ADD_CONV vars))
and conv_comp = GEN_REWRITE_CONV I [pth_comp] in
let net1 =
itlist (fun th -> enter [] (lhand(concl th),K (REWR_CONV th)))
(CONJUNCTS
pth_trivial) empty_net in
let net2 =
itlist (fun th -> enter [] (lhand(concl th),
let cnv = K (REWR_CONV th) in fun v -> cnv v THENC conv_pos v))
(CONJUNCTS pth_pos) net1 in
let basnet =
itlist (fun th -> enter [] (lhand(concl th),
let cnv = K (REWR_CONV th) in fun v -> cnv v THENC conv_neg v))
(CONJUNCTS pth_neg) net2 in
let rec baseconv vars tm =
try tryfind (fun f -> f vars tm) (lookup tm basnet) with Failure _ ->
(conv_comp THENC BINOP_CONV (baseconv vars)) tm in
baseconv;;
let pth_base = prove
(`(?j. n <= j /\ j <= n /\ P(j)) <=> P(n)`,
MESON_TAC[
INT_LE_ANTISYM])
and
pth_step =
prove
(`(?j. &1 <= j /\ j <= &(SUC n) /\ P(j)) <=>
(?j. &1 <= j /\ j <= &n /\ P(j)) \/ P(&(SUC n))`,
REWRITE_TAC[GSYM
INT_OF_NUM_SUC] THEN
REWRITE_TAC[INT_ARITH `x <= y + &1 <=> (x = y + &1) \/ x < y + &1`] THEN
REWRITE_TAC[
INT_LT_DISCRETE;
INT_LE_RADD] THEN
MESON_TAC[INT_ARITH `&0 <= x ==> &1 <= x + &1`;
INT_POS;
INT_LE_REFL]) in
let base_conv = REWR_CONV
pth_base
and step_conv =
BINDER_CONV(RAND_CONV(LAND_CONV(funpow 2 RAND_CONV num_CONV))) THENC
REWR_CONV
pth_step THENC
RAND_CONV(ONCE_DEPTH_CONV NUM_SUC_CONV) in
let rec conv tm =
try base_conv tm with Failure _ ->
(step_conv THENC LAND_CONV conv) tm in
conv;;
let pth = prove
(`(~(&0 < x) <=> &0 < &1 - x) /\
(~(&0 > x) <=> &0 < &1 + x)`,
REWRITE_TAC[
INT_NOT_LT;
INT_GT] THEN
REWRITE_TAC[
INT_LT_DISCRETE;
INT_GT_DISCRETE] THEN
INT_ARITH_TAC) in
let conv1 vars = REWR_CONV(CONJUNCT1 pth) THENC
RAND_CONV (POLYNOMIAL_SUB_CONV vars)
and conv2 vars = REWR_CONV(CONJUNCT2 pth) THENC
RAND_CONV (POLYNOMIAL_ADD_CONV vars)
and pat1 = `~(&0 < x)` and pat2 = `~(&0 > x)`
and net = itlist (fun t -> net_of_conv (lhand t) (REWR_CONV(TAUT t)))
[`~(~ p) <=> p`; `~(p /\ q) <=> ~p \/ ~q`;
`~(p \/ q) <=> ~p /\ ~q`] empty_net in
fun vars ->
let net' = net_of_conv pat1 (conv1 vars)
(net_of_conv pat2 (conv2 vars) net) in
TOP_SWEEP_CONV(REWRITES_CONV net');;