https://github.com/JacquesCarette/hol-light
Tip revision: b27a524086caf73530b7c2c5da1b237d3539f143 authored by Jacques Carette on 24 August 2020, 14:18:07 UTC
Merge pull request #35 from sjjs7/final-changes
Merge pull request #35 from sjjs7/final-changes
Tip revision: b27a524
realax.ml
(* ========================================================================= *)
(* Theory of real numbers. *)
(* *)
(* John Harrison, University of Cambridge Computer Laboratory *)
(* *)
(* (c) Copyright, University of Cambridge 1998 *)
(* (c) Copyright, John Harrison 1998-2007 *)
(* ========================================================================= *)
needs "lists.ml";;
(* ------------------------------------------------------------------------- *)
(* The main infix overloaded operations *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("++",(16,"right"));;
parse_as_infix("**",(20,"right"));;
parse_as_infix("<<=",(12,"right"));;
parse_as_infix("===",(10,"right"));;
parse_as_infix ("treal_mul",(20,"right"));;
parse_as_infix ("treal_add",(16,"right"));;
parse_as_infix ("treal_le",(12,"right"));;
parse_as_infix ("treal_eq",(10,"right"));;
make_overloadable "+" `:A->A->A`;;
make_overloadable "-" `:A->A->A`;;
make_overloadable "*" `:A->A->A`;;
make_overloadable "/" `:A->A->A`;;
make_overloadable "<" `:A->A->bool`;;
make_overloadable "<=" `:A->A->bool`;;
make_overloadable ">" `:A->A->bool`;;
make_overloadable ">=" `:A->A->bool`;;
make_overloadable "--" `:A->A`;;
make_overloadable "pow" `:A->num->A`;;
make_overloadable "inv" `:A->A`;;
make_overloadable "abs" `:A->A`;;
make_overloadable "max" `:A->A->A`;;
make_overloadable "min" `:A->A->A`;;
make_overloadable "&" `:num->A`;;
do_list overload_interface
["+",`(+):num->num->num`; "-",`(-):num->num->num`;
"*",`(*):num->num->num`; "<",`(<):num->num->bool`;
"<=",`(<=):num->num->bool`; ">",`(>):num->num->bool`;
">=",`(>=):num->num->bool`];;
let prioritize_num() = prioritize_overload(mk_type("num",[]));;
(* ------------------------------------------------------------------------- *)
(* Absolute distance function on the naturals. *)
(* ------------------------------------------------------------------------- *)
let dist = new_definition
`dist(m,n) = (m - n) + (n - m)`;;
(* ------------------------------------------------------------------------- *)
(* Some easy theorems. *)
(* ------------------------------------------------------------------------- *)
let DIST_REFL = prove
(`!n. dist(n,n) = 0`,
REWRITE_TAC[dist; SUB_REFL; ADD_CLAUSES]);;
let DIST_LZERO = prove
(`!n. dist(0,n) = n`,
REWRITE_TAC[dist; SUB_0; ADD_CLAUSES]);;
let DIST_RZERO = prove
(`!n. dist(n,0) = n`,
REWRITE_TAC[dist; SUB_0; ADD_CLAUSES]);;
let DIST_SYM = prove
(`!m n. dist(m,n) = dist(n,m)`,
REWRITE_TAC[dist] THEN MATCH_ACCEPT_TAC ADD_SYM);;
let DIST_LADD = prove
(`!m p n. dist(m + n,m + p) = dist(n,p)`,
REWRITE_TAC[dist; SUB_ADD_LCANCEL]);;
let DIST_RADD = prove
(`!m p n. dist(m + p,n + p) = dist(m,n)`,
REWRITE_TAC[dist; SUB_ADD_RCANCEL]);;
let DIST_LADD_0 = prove
(`!m n. dist(m + n,m) = n`,
REWRITE_TAC[dist; ADD_SUB2; ADD_SUBR2; ADD_CLAUSES]);;
let DIST_RADD_0 = prove
(`!m n. dist(m,m + n) = n`,
ONCE_REWRITE_TAC[DIST_SYM] THEN MATCH_ACCEPT_TAC DIST_LADD_0);;
let DIST_LMUL = prove
(`!m n p. m * dist(n,p) = dist(m * n,m * p)`,
REWRITE_TAC[dist; LEFT_ADD_DISTRIB; LEFT_SUB_DISTRIB]);;
let DIST_RMUL = prove
(`!m n p. dist(m,n) * p = dist(m * p,n * p)`,
REWRITE_TAC[dist; RIGHT_ADD_DISTRIB; RIGHT_SUB_DISTRIB]);;
let DIST_EQ_0 = prove
(`!m n. (dist(m,n) = 0) <=> (m = n)`,
REWRITE_TAC[dist; ADD_EQ_0; SUB_EQ_0; LE_ANTISYM]);;
(* ------------------------------------------------------------------------- *)
(* Simplifying theorem about the distance operation. *)
(* ------------------------------------------------------------------------- *)
let DIST_ELIM_THM = prove
(`P(dist(x,y)) <=> !d. ((x = y + d) ==> P(d)) /\ ((y = x + d) ==> P(d))`,
DISJ_CASES_TAC(SPECL [`x:num`; `y:num`] LE_CASES) THEN
POP_ASSUM(X_CHOOSE_THEN `e:num` SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
REWRITE_TAC[dist; ADD_SUB; ADD_SUB2; ADD_SUBR; ADD_SUBR2] THEN
REWRITE_TAC[ADD_CLAUSES; EQ_ADD_LCANCEL] THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [EQ_SYM_EQ] THEN
REWRITE_TAC[GSYM ADD_ASSOC; EQ_ADD_LCANCEL_0; ADD_EQ_0] THEN
ASM_CASES_TAC `e = 0` THEN ASM_REWRITE_TAC[] THEN
EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Now some more theorems. *)
(* ------------------------------------------------------------------------- *)
let DIST_LE_CASES,DIST_ADDBOUND,DIST_TRIANGLE,DIST_ADD2,DIST_ADD2_REV =
let DIST_ELIM_TAC =
let conv =
HIGHER_REWRITE_CONV[SUB_ELIM_THM; COND_ELIM_THM; DIST_ELIM_THM] false in
CONV_TAC conv THEN TRY GEN_TAC THEN CONJ_TAC THEN
DISCH_THEN(fun th -> SUBST_ALL_TAC th THEN
(let l,r = dest_eq (concl th) in
if is_var l && not (vfree_in l r) then ALL_TAC
else ASSUME_TAC th)) in
let DIST_ELIM_TAC' =
REPEAT STRIP_TAC THEN REPEAT DIST_ELIM_TAC THEN
REWRITE_TAC[GSYM NOT_LT; LT_EXISTS] THEN
DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN POP_ASSUM MP_TAC THEN
CONV_TAC(LAND_CONV NUM_CANCEL_CONV) THEN
REWRITE_TAC[ADD_CLAUSES; NOT_SUC] in
let DIST_LE_CASES = prove
(`!m n p. dist(m,n) <= p <=> (m <= n + p) /\ (n <= m + p)`,
REPEAT GEN_TAC THEN REPEAT DIST_ELIM_TAC THEN
REWRITE_TAC[GSYM ADD_ASSOC; LE_ADD; LE_ADD_LCANCEL])
and DIST_ADDBOUND = prove
(`!m n. dist(m,n) <= m + n`,
REPEAT GEN_TAC THEN DIST_ELIM_TAC THENL
[ONCE_REWRITE_TAC[ADD_SYM]; ALL_TAC] THEN
REWRITE_TAC[ADD_ASSOC; LE_ADDR])
and [DIST_TRIANGLE; DIST_ADD2; DIST_ADD2_REV] = (CONJUNCTS o prove)
(`(!m n p. dist(m,p) <= dist(m,n) + dist(n,p)) /\
(!m n p q. dist(m + n,p + q) <= dist(m,p) + dist(n,q)) /\
(!m n p q. dist(m,p) <= dist(m + n,p + q) + dist(n,q))`,
DIST_ELIM_TAC') in
DIST_LE_CASES,DIST_ADDBOUND,DIST_TRIANGLE,DIST_ADD2,DIST_ADD2_REV;;
let DIST_TRIANGLE_LE = prove
(`!m n p q. dist(m,n) + dist(n,p) <= q ==> dist(m,p) <= q`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
EXISTS_TAC `dist(m,n) + dist(n,p)` THEN ASM_REWRITE_TAC[DIST_TRIANGLE]);;
let DIST_TRIANGLES_LE = prove
(`!m n p q r s.
dist(m,n) <= r /\ dist(p,q) <= s ==> dist(m,p) <= dist(n,q) + r + s`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC DIST_TRIANGLE_LE THEN
EXISTS_TAC `n:num` THEN GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
REWRITE_TAC[GSYM ADD_ASSOC] THEN MATCH_MP_TAC LE_ADD2 THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC DIST_TRIANGLE_LE THEN
EXISTS_TAC `q:num` THEN GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
REWRITE_TAC[LE_ADD_LCANCEL] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN
ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Useful lemmas about bounds. *)
(* ------------------------------------------------------------------------- *)
let BOUNDS_LINEAR = prove
(`!A B C. (!n. A * n <= B * n + C) <=> A <= B`,
REPEAT GEN_TAC THEN EQ_TAC THENL
[CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LE] THEN
DISCH_THEN(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LT_EXISTS]) THEN
REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
DISCH_THEN(MP_TAC o SPEC `SUC C`) THEN
REWRITE_TAC[NOT_LE; MULT_CLAUSES; ADD_CLAUSES; LT_SUC_LE] THEN
REWRITE_TAC[ADD_ASSOC; LE_ADDR];
DISCH_THEN(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC; LE_ADD]]);;
let BOUNDS_LINEAR_0 = prove
(`!A B. (!n. A * n <= B) <=> (A = 0)`,
REPEAT GEN_TAC THEN MP_TAC(SPECL [`A:num`; `0`; `B:num`] BOUNDS_LINEAR) THEN
REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; LE]);;
let BOUNDS_DIVIDED = prove
(`!P. (?B. !n. P(n) <= B) <=>
(?A B. !n. n * P(n) <= A * n + B)`,
GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
[MAP_EVERY EXISTS_TAC [`B:num`; `0`] THEN
GEN_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN
GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
ASM_REWRITE_TAC[LE_MULT_LCANCEL];
EXISTS_TAC `P(0) + A + B` THEN GEN_TAC THEN
MP_TAC(SPECL [`n:num`; `(P:num->num) n`; `P(0) + A + B`]
LE_MULT_LCANCEL) THEN
ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[LE_ADD] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * n + B` THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[LEFT_ADD_DISTRIB] THEN
GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
REWRITE_TAC[GSYM ADD_ASSOC; LE_ADD_LCANCEL] THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `B * n` THEN
REWRITE_TAC[LE_ADD] THEN UNDISCH_TAC `~(n = 0)` THEN
SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
ASM_REWRITE_TAC[MULT_CLAUSES; LE_ADD]]);;
let BOUNDS_NOTZERO = prove
(`!P A B. (P 0 0 = 0) /\ (!m n. P m n <= A * (m + n) + B) ==>
(?B. !m n. P m n <= B * (m + n))`,
REPEAT STRIP_TAC THEN EXISTS_TAC `A + B` THEN
REPEAT GEN_TAC THEN ASM_CASES_TAC `m + n = 0` THENL
[RULE_ASSUM_TAC(REWRITE_RULE[ADD_EQ_0]) THEN ASM_REWRITE_TAC[LE_0];
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * (m + n) + B` THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
UNDISCH_TAC `~(m + n = 0)` THEN SPEC_TAC(`m + n`,`p:num`) THEN
INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; LE_ADD]]);;
let BOUNDS_IGNORE = prove
(`!P Q. (?B. !i. P(i) <= Q(i) + B) <=>
(?B N. !i. N <= i ==> P(i) <= Q(i) + B)`,
REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
[EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC THEN SPEC_TAC(`B:num`,`B:num`) THEN
SPEC_TAC(`N:num`,`N:num`) THEN INDUCT_TAC THENL
[REWRITE_TAC[LE_0] THEN GEN_TAC THEN DISCH_TAC THEN
EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[];
GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
EXISTS_TAC `B + P(N:num)` THEN X_GEN_TAC `i:num` THEN
DISCH_TAC THEN ASM_CASES_TAC `SUC N <= i` THENL
[MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `Q(i:num) + B` THEN
REWRITE_TAC[LE_ADD; ADD_ASSOC] THEN FIRST_ASSUM MATCH_MP_TAC THEN
ASM_REWRITE_TAC[];
UNDISCH_TAC `~(SUC N <= i)` THEN REWRITE_TAC[NOT_LE; LT] THEN
ASM_REWRITE_TAC[GSYM NOT_LE] THEN DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
REWRITE_TAC[LE_ADD]]]]);;
(* ------------------------------------------------------------------------- *)
(* Define type of nearly additive functions. *)
(* ------------------------------------------------------------------------- *)
let is_nadd = new_definition
`is_nadd x <=> (?B. !m n. dist(m * x(n),n * x(m)) <= B * (m + n))`;;
let is_nadd_0 = prove
(`is_nadd (\n. 0)`,
REWRITE_TAC[is_nadd; MULT_CLAUSES; DIST_REFL; LE_0]);;
let nadd_abs,nadd_rep =
new_basic_type_definition "nadd" ("mk_nadd","dest_nadd") is_nadd_0;;
override_interface ("fn",`dest_nadd`);;
override_interface ("afn",`mk_nadd`);;
(* ------------------------------------------------------------------------- *)
(* Properties of nearly-additive functions. *)
(* ------------------------------------------------------------------------- *)
let NADD_CAUCHY = prove
(`!x. ?B. !m n. dist(m * fn x n,n * fn x m) <= B * (m + n)`,
REWRITE_TAC[GSYM is_nadd; nadd_rep; nadd_abs; ETA_AX]);;
let NADD_BOUND = prove
(`!x. ?A B. !n. fn x n <= A * n + B`,
GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
MAP_EVERY EXISTS_TAC [`B + fn x 1`; `B:num`] THEN GEN_TAC THEN
POP_ASSUM(MP_TAC o SPECL [`n:num`; `1`]) THEN
REWRITE_TAC[DIST_LE_CASES; MULT_CLAUSES] THEN
DISCH_THEN(MP_TAC o CONJUNCT2) THEN
REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
REWRITE_TAC[ADD_AC; MULT_AC]);;
let NADD_MULTIPLICATIVE = prove
(`!x. ?B. !m n. dist(fn x (m * n),m * fn x n) <= B * m + B`,
GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
EXISTS_TAC `B + fn x 0` THEN REPEAT GEN_TAC THEN
ASM_CASES_TAC `n = 0` THENL
[MATCH_MP_TAC (LE_IMP DIST_ADDBOUND) THEN
ASM_REWRITE_TAC[MULT_CLAUSES; RIGHT_ADD_DISTRIB; MULT_AC] THEN
REWRITE_TAC[LE_EXISTS] THEN CONV_TAC(ONCE_DEPTH_CONV NUM_CANCEL_CONV) THEN
REWRITE_TAC[GSYM EXISTS_REFL]; UNDISCH_TAC `~(n = 0)`] THEN
REWRITE_TAC[TAUT `(~a ==> b) <=> a \/ b`; GSYM LE_MULT_LCANCEL;
DIST_LMUL] THEN
REWRITE_TAC[MULT_ASSOC] THEN GEN_REWRITE_TAC
(LAND_CONV o RAND_CONV o RAND_CONV o LAND_CONV) [MULT_SYM] THEN
POP_ASSUM(MATCH_MP_TAC o LE_IMP) THEN
REWRITE_TAC[LE_EXISTS; RIGHT_ADD_DISTRIB; LEFT_ADD_DISTRIB; MULT_AC] THEN
CONV_TAC(ONCE_DEPTH_CONV NUM_CANCEL_CONV) THEN
REWRITE_TAC[GSYM EXISTS_REFL]);;
let NADD_ADDITIVE = prove
(`!x. ?B. !m n. dist(fn x (m + n),fn x m + fn x n) <= B`,
GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
EXISTS_TAC `3 * B + fn x 0` THEN REPEAT GEN_TAC THEN
ASM_CASES_TAC `m + n = 0` THENL
[RULE_ASSUM_TAC(REWRITE_RULE[ADD_EQ_0]) THEN ONCE_REWRITE_TAC[DIST_SYM] THEN
ASM_REWRITE_TAC[ADD_CLAUSES; DIST_LADD_0; LE_ADDR];
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `3 * B` THEN
REWRITE_TAC[LE_ADD] THEN UNDISCH_TAC `~(m + n = 0)`] THEN
REWRITE_TAC[TAUT `(~a ==> b) <=> a \/ b`; GSYM LE_MULT_LCANCEL] THEN
REWRITE_TAC[DIST_LMUL; LEFT_ADD_DISTRIB] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [RIGHT_ADD_DISTRIB] THEN
MATCH_MP_TAC(LE_IMP DIST_ADD2) THEN
SUBGOAL_THEN `(m + n) * 3 * B = B * (m + m + n) + B * (n + m + n)`
SUBST1_TAC THENL
[REWRITE_TAC[SYM(REWRITE_CONV [ARITH] `1 + 1 + 1`)] THEN
REWRITE_TAC[RIGHT_ADD_DISTRIB; LEFT_ADD_DISTRIB; MULT_CLAUSES] THEN
REWRITE_TAC[MULT_AC] THEN CONV_TAC NUM_CANCEL_CONV THEN REFL_TAC;
MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]]);;
let NADD_SUC = prove
(`!x. ?B. !n. dist(fn x (SUC n),fn x n) <= B`,
GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_ADDITIVE) THEN
EXISTS_TAC `B + fn x 1` THEN GEN_TAC THEN
MATCH_MP_TAC(LE_IMP DIST_TRIANGLE) THEN
EXISTS_TAC `fn x n + fn x 1` THEN
ASM_REWRITE_TAC[ADD1] THEN MATCH_MP_TAC LE_ADD2 THEN
ASM_REWRITE_TAC[DIST_LADD_0; LE_REFL]);;
let NADD_DIST_LEMMA = prove
(`!x. ?B. !m n. dist(fn x (m + n),fn x m) <= B * n`,
GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_SUC) THEN
EXISTS_TAC `B:num` THEN GEN_TAC THEN
INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; DIST_REFL; LE_0] THEN
MATCH_MP_TAC(LE_IMP DIST_TRIANGLE) THEN
EXISTS_TAC `fn x (m + n)` THEN
REWRITE_TAC[ADD1; LEFT_ADD_DISTRIB] THEN
GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[GSYM ADD1; MULT_CLAUSES]);;
let NADD_DIST = prove
(`!x. ?B. !m n. dist(fn x m,fn x n) <= B * dist(m,n)`,
GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_DIST_LEMMA) THEN
EXISTS_TAC `B:num` THEN REPEAT GEN_TAC THEN
DISJ_CASES_THEN MP_TAC (SPECL [`m:num`; `n:num`] LE_CASES) THEN
DISCH_THEN(CHOOSE_THEN SUBST1_TAC o ONCE_REWRITE_RULE[LE_EXISTS]) THENL
[ONCE_REWRITE_TAC[DIST_SYM]; ALL_TAC] THEN
ASM_REWRITE_TAC[DIST_LADD_0]);;
let NADD_ALTMUL = prove
(`!x y. ?A B. !n. dist(n * fn x (fn y n),fn x n * fn y n) <= A * n + B`,
REPEAT GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
MP_TAC(SPEC `y:nadd` NADD_BOUND) THEN
DISCH_THEN(X_CHOOSE_THEN `M:num` (X_CHOOSE_TAC `L:num`)) THEN
MAP_EVERY EXISTS_TAC [`B * (1 + M)`; `B * L`] THEN GEN_TAC THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o RAND_CONV) [MULT_SYM] THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `B * (n + fn y n)` THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
REWRITE_TAC[MULT_CLAUSES; GSYM ADD_ASSOC; LE_ADD_LCANCEL] THEN
ASM_REWRITE_TAC[GSYM LEFT_ADD_DISTRIB; GSYM MULT_ASSOC; LE_MULT_LCANCEL]);;
(* ------------------------------------------------------------------------- *)
(* Definition of the equivalence relation and proof that it *is* one. *)
(* ------------------------------------------------------------------------- *)
override_interface ("===",`(nadd_eq):nadd->nadd->bool`);;
let nadd_eq = new_definition
`x === y <=> ?B. !n. dist(fn x n,fn y n) <= B`;;
let NADD_EQ_REFL = prove
(`!x. x === x`,
GEN_TAC THEN REWRITE_TAC[nadd_eq; DIST_REFL; LE_0]);;
let NADD_EQ_SYM = prove
(`!x y. x === y <=> y === x`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq] THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [DIST_SYM] THEN REFL_TAC);;
let NADD_EQ_TRANS = prove
(`!x y z. x === y /\ y === z ==> x === z`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq] THEN
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_TAC `B1:num`) (X_CHOOSE_TAC `B2:num`)) THEN
EXISTS_TAC `B1 + B2` THEN X_GEN_TAC `n:num` THEN
MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN EXISTS_TAC `fn y n` THEN
MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Injection of the natural numbers. *)
(* ------------------------------------------------------------------------- *)
override_interface ("&",`nadd_of_num:num->nadd`);;
let nadd_of_num = new_definition
`&k = afn(\n. k * n)`;;
let NADD_OF_NUM = prove
(`!k. fn(&k) = \n. k * n`,
REWRITE_TAC[nadd_of_num; GSYM nadd_rep; is_nadd] THEN
REWRITE_TAC[DIST_REFL; LE_0; MULT_AC]);;
let NADD_OF_NUM_WELLDEF = prove
(`!m n. (m = n) ==> &m === &n`,
REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
MATCH_ACCEPT_TAC NADD_EQ_REFL);;
let NADD_OF_NUM_EQ = prove
(`!m n. (&m === &n) <=> (m = n)`,
REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[NADD_OF_NUM_WELLDEF] THEN
REWRITE_TAC[nadd_eq; NADD_OF_NUM] THEN
REWRITE_TAC[GSYM DIST_RMUL; BOUNDS_LINEAR_0; DIST_EQ_0]);;
(* ------------------------------------------------------------------------- *)
(* Definition of (reflexive) ordering and the only special property needed. *)
(* ------------------------------------------------------------------------- *)
override_interface ("<<=",`nadd_le:nadd->nadd->bool`);;
let nadd_le = new_definition
`x <<= y <=> ?B. !n. fn x n <= fn y n + B`;;
let NADD_LE_WELLDEF_LEMMA = prove
(`!x x' y y'. x === x' /\ y === y' /\ x <<= y ==> x' <<= y'`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; nadd_le] THEN
REWRITE_TAC[DIST_LE_CASES; FORALL_AND_THM] THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B1:num`) MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B2:num`) MP_TAC) THEN
DISCH_THEN(X_CHOOSE_TAC `B:num`) THEN
EXISTS_TAC `(B2 + B) + B1` THEN X_GEN_TAC `n:num` THEN
FIRST_ASSUM(MATCH_MP_TAC o LE_IMP o CONJUNCT2) THEN
REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL] THEN
FIRST_ASSUM(MATCH_MP_TAC o LE_IMP) THEN ASM_REWRITE_TAC[LE_ADD_RCANCEL]);;
let NADD_LE_WELLDEF = prove
(`!x x' y y'. x === x' /\ y === y' ==> (x <<= y <=> x' <<= y')`,
REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN
MATCH_MP_TAC NADD_LE_WELLDEF_LEMMA THEN ASM_REWRITE_TAC[] THENL
[MAP_EVERY EXISTS_TAC [`x:nadd`; `y:nadd`];
MAP_EVERY EXISTS_TAC [`x':nadd`; `y':nadd`] THEN
ONCE_REWRITE_TAC[NADD_EQ_SYM]] THEN
ASM_REWRITE_TAC[]);;
let NADD_LE_REFL = prove
(`!x. x <<= x`,
REWRITE_TAC[nadd_le; LE_ADD]);;
let NADD_LE_TRANS = prove
(`!x y z. x <<= y /\ y <<= z ==> x <<= z`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le] THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B1:num`) MP_TAC) THEN
DISCH_THEN(X_CHOOSE_TAC `B2:num`) THEN
EXISTS_TAC `B2 + B1` THEN GEN_TAC THEN
FIRST_ASSUM(MATCH_MP_TAC o LE_IMP) THEN
ASM_REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL]);;
let NADD_LE_ANTISYM = prove
(`!x y. x <<= y /\ y <<= x <=> (x === y)`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; nadd_eq; DIST_LE_CASES] THEN
EQ_TAC THENL
[DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B1:num`)
(X_CHOOSE_TAC `B2:num`)) THEN
EXISTS_TAC `B1 + B2` THEN GEN_TAC THEN CONJ_TAC THEN
FIRST_ASSUM(MATCH_MP_TAC o LE_IMP) THEN
ASM_REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL; LE_ADD; LE_ADDR];
DISCH_THEN(X_CHOOSE_TAC `B:num`) THEN
CONJ_TAC THEN EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[]]);;
let NADD_LE_TOTAL_LEMMA = prove
(`!x y. ~(x <<= y) ==> !B. ?n. ~(n = 0) /\ fn y n + B < fn x n`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NOT_FORALL_THM; NOT_EXISTS_THM] THEN
REWRITE_TAC[NOT_LE] THEN DISCH_TAC THEN GEN_TAC THEN
POP_ASSUM(X_CHOOSE_TAC `n:num` o SPEC `B + fn x 0`) THEN
EXISTS_TAC `n:num` THEN POP_ASSUM MP_TAC THEN
ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[NOT_LT; ADD_ASSOC; LE_ADDR] THEN
CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LT] THEN
DISCH_THEN(MATCH_MP_TAC o LE_IMP) THEN REWRITE_TAC[ADD_ASSOC; LE_ADD]);;
let NADD_LE_TOTAL = prove
(`!x y. x <<= y \/ y <<= x`,
REPEAT GEN_TAC THEN GEN_REWRITE_TAC I [TAUT `a <=> ~ ~ a`] THEN
X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
X_CHOOSE_TAC `B2:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
PURE_ONCE_REWRITE_TAC[DE_MORGAN_THM] THEN
DISCH_THEN(MP_TAC o end_itlist CONJ o
map (MATCH_MP NADD_LE_TOTAL_LEMMA) o CONJUNCTS) THEN
REWRITE_TAC[AND_FORALL_THM] THEN DISCH_THEN(MP_TAC o SPEC `B1 + B2`) THEN
REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` (X_CHOOSE_THEN `n:num` MP_TAC)) THEN
DISCH_THEN(MP_TAC o MATCH_MP
(ITAUT `(~a /\ b) /\ (~c /\ d) ==> ~(c \/ ~b) /\ ~(a \/ ~d)`)) THEN
REWRITE_TAC[NOT_LT; GSYM LE_MULT_LCANCEL] THEN REWRITE_TAC[NOT_LE] THEN
DISCH_THEN(MP_TAC o MATCH_MP LT_ADD2) THEN REWRITE_TAC[NOT_LT] THEN
REWRITE_TAC[LEFT_ADD_DISTRIB] THEN
ONCE_REWRITE_TAC[AC ADD_AC
`(a + b + c) + (d + e + f) = (d + b + e) + (a + c + f)`] THEN
MATCH_MP_TAC LE_ADD2 THEN REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] THEN
CONJ_TAC THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [MULT_SYM] THEN
RULE_ASSUM_TAC(REWRITE_RULE[DIST_LE_CASES]) THEN ASM_REWRITE_TAC[]);;
let NADD_ARCH = prove
(`!x. ?n. x <<= &n`,
REWRITE_TAC[nadd_le; NADD_OF_NUM; NADD_BOUND]);;
let NADD_OF_NUM_LE = prove
(`!m n. (&m <<= &n) <=> m <= n`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NADD_OF_NUM] THEN
REWRITE_TAC[BOUNDS_LINEAR]);;
(* ------------------------------------------------------------------------- *)
(* Addition. *)
(* ------------------------------------------------------------------------- *)
override_interface ("++",`nadd_add:nadd->nadd->nadd`);;
let nadd_add = new_definition
`x ++ y = afn(\n. fn x n + fn y n)`;;
let NADD_ADD = prove
(`!x y. fn(x ++ y) = \n. fn x n + fn y n`,
REPEAT GEN_TAC THEN
REWRITE_TAC[nadd_add; GSYM nadd_rep; is_nadd] THEN
X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
X_CHOOSE_TAC `B2:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
EXISTS_TAC `B1 + B2` THEN MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [LEFT_ADD_DISTRIB] THEN
MATCH_MP_TAC (LE_IMP DIST_ADD2) THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]);;
let NADD_ADD_WELLDEF = prove
(`!x x' y y'. x === x' /\ y === y' ==> (x ++ y === x' ++ y')`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_ADD] THEN
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_TAC `B1:num`) (X_CHOOSE_TAC `B2:num`)) THEN
EXISTS_TAC `B1 + B2` THEN X_GEN_TAC `n:num` THEN
MATCH_MP_TAC (LE_IMP DIST_ADD2) THEN
MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Basic properties of addition. *)
(* ------------------------------------------------------------------------- *)
let NADD_ADD_SYM = prove
(`!x y. (x ++ y) === (y ++ x)`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_add] THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ADD_SYM] THEN
REWRITE_TAC[NADD_EQ_REFL]);;
let NADD_ADD_ASSOC = prove
(`!x y z. (x ++ (y ++ z)) === ((x ++ y) ++ z)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[nadd_add] THEN
REWRITE_TAC[NADD_ADD; ADD_ASSOC; NADD_EQ_REFL]);;
let NADD_ADD_LID = prove
(`!x. (&0 ++ x) === x`,
GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_ADD; NADD_OF_NUM] THEN
REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; DIST_REFL; LE_0]);;
let NADD_ADD_LCANCEL = prove
(`!x y z. (x ++ y) === (x ++ z) ==> y === z`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_ADD; DIST_LADD]);;
let NADD_LE_ADD = prove
(`!x y. x <<= (x ++ y)`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NADD_ADD] THEN
EXISTS_TAC `0` THEN REWRITE_TAC[ADD_CLAUSES; LE_ADD]);;
let NADD_LE_EXISTS = prove
(`!x y. x <<= y ==> ?d. y === x ++ d`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le] THEN
DISCH_THEN(X_CHOOSE_THEN `B:num` MP_TAC) THEN
REWRITE_TAC[LE_EXISTS; SKOLEM_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `d:num->num` (ASSUME_TAC o GSYM)) THEN
EXISTS_TAC `afn d` THEN REWRITE_TAC[nadd_eq; NADD_ADD] THEN
EXISTS_TAC `B:num` THEN X_GEN_TAC `n:num` THEN
SUBGOAL_THEN `fn(afn d) = d` SUBST1_TAC THENL
[REWRITE_TAC[GSYM nadd_rep; is_nadd] THEN
X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
X_CHOOSE_TAC `B2:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
EXISTS_TAC `B1 + (B2 + B)` THEN REPEAT GEN_TAC THEN
MATCH_MP_TAC(LE_IMP DIST_ADD2_REV) THEN
MAP_EVERY EXISTS_TAC [`m * fn x n`; `n * fn x m`] THEN
ONCE_REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[ADD_SYM] THEN
ASM_REWRITE_TAC[GSYM LEFT_ADD_DISTRIB] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [LEFT_ADD_DISTRIB] THEN
MATCH_MP_TAC(LE_IMP DIST_ADD2) THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN MATCH_MP_TAC LE_ADD2 THEN
ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
REWRITE_TAC[GSYM DIST_LMUL; DIST_ADDBOUND; LE_MULT_LCANCEL];
ASM_REWRITE_TAC[DIST_RADD_0; LE_REFL]]);;
let NADD_OF_NUM_ADD = prove
(`!m n. &m ++ &n === &(m + n)`,
REWRITE_TAC[nadd_eq; NADD_OF_NUM; NADD_ADD] THEN
REWRITE_TAC[RIGHT_ADD_DISTRIB; DIST_REFL; LE_0]);;
(* ------------------------------------------------------------------------- *)
(* Multiplication. *)
(* ------------------------------------------------------------------------- *)
override_interface ("**",`nadd_mul:nadd->nadd->nadd`);;
let nadd_mul = new_definition
`x ** y = afn(\n. fn x (fn y n))`;;
let NADD_MUL = prove
(`!x y. fn(x ** y) = \n. fn x (fn y n)`,
REPEAT GEN_TAC THEN
REWRITE_TAC[nadd_mul; GSYM nadd_rep; is_nadd] THEN
X_CHOOSE_TAC `B:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
X_CHOOSE_TAC `C:num` (SPEC `x:nadd` NADD_DIST) THEN
X_CHOOSE_TAC `D:num` (SPEC `x:nadd` NADD_MULTIPLICATIVE) THEN
MATCH_MP_TAC BOUNDS_NOTZERO THEN
REWRITE_TAC[MULT_CLAUSES; DIST_REFL] THEN
MAP_EVERY EXISTS_TAC [`D + C * B`; `D + D`] THEN
REPEAT GEN_TAC THEN MATCH_MP_TAC LE_TRANS THEN
EXISTS_TAC `(D * m + D) + (D * n + D) + C * B * (m + n)` THEN CONJ_TAC THENL
[MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN
EXISTS_TAC `fn x (m * fn y n)` THEN
MATCH_MP_TAC LE_ADD2 THEN
ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN
EXISTS_TAC `fn x (n * fn y m)` THEN
MATCH_MP_TAC LE_ADD2 THEN
ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC LE_TRANS THEN
EXISTS_TAC `C * dist(m * fn y n,n * fn y m)` THEN
ASM_REWRITE_TAC[LE_MULT_LCANCEL];
MATCH_MP_TAC EQ_IMP_LE THEN
REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_ASSOC; ADD_AC]]);;
(* ------------------------------------------------------------------------- *)
(* Properties of multiplication. *)
(* ------------------------------------------------------------------------- *)
let NADD_MUL_SYM = prove
(`!x y. (x ** y) === (y ** x)`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_MUL] THEN
X_CHOOSE_THEN `A1:num` MP_TAC (SPECL [`x:nadd`; `y:nadd`] NADD_ALTMUL) THEN
DISCH_THEN(X_CHOOSE_TAC `B1:num`) THEN
X_CHOOSE_THEN `A2:num` MP_TAC (SPECL [`y:nadd`; `x:nadd`] NADD_ALTMUL) THEN
DISCH_THEN(X_CHOOSE_TAC `B2:num`) THEN REWRITE_TAC[BOUNDS_DIVIDED] THEN
REWRITE_TAC[DIST_LMUL] THEN MAP_EVERY EXISTS_TAC [`A1 + A2`; `B1 + B2`] THEN
GEN_TAC THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
ONCE_REWRITE_TAC[AC ADD_AC `(a + b) + (c + d) = (a + c) + (b + d)`] THEN
MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN
EXISTS_TAC `fn x n * fn y n` THEN
MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC [DIST_SYM] THEN
GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV) [MULT_SYM] THEN
ASM_REWRITE_TAC[]);;
let NADD_MUL_ASSOC = prove
(`!x y z. (x ** (y ** z)) === ((x ** y) ** z)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[nadd_mul] THEN
REWRITE_TAC[NADD_MUL; NADD_EQ_REFL]);;
let NADD_MUL_LID = prove
(`!x. (&1 ** x) === x`,
REWRITE_TAC[NADD_OF_NUM; nadd_mul; MULT_CLAUSES] THEN
REWRITE_TAC[nadd_abs; NADD_EQ_REFL; ETA_AX]);;
let NADD_LDISTRIB = prove
(`!x y z. x ** (y ++ z) === (x ** y) ++ (x ** z)`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq] THEN
REWRITE_TAC[NADD_ADD; NADD_MUL] THEN
X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_ADDITIVE) THEN
EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[]);;
let NADD_MUL_WELLDEF_LEMMA = prove
(`!x y y'. y === y' ==> (x ** y) === (x ** y')`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_MUL] THEN
DISCH_THEN(X_CHOOSE_TAC `B1:num`) THEN
X_CHOOSE_TAC `B2:num` (SPEC `x:nadd` NADD_DIST) THEN
EXISTS_TAC `B2 * B1` THEN X_GEN_TAC `n:num` THEN
MATCH_MP_TAC LE_TRANS THEN
EXISTS_TAC `B2 * dist(fn y n,fn y' n)` THEN
ASM_REWRITE_TAC[LE_MULT_LCANCEL]);;
let NADD_MUL_WELLDEF = prove
(`!x x' y y'. x === x' /\ y === y'
==> (x ** y) === (x' ** y')`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC NADD_EQ_TRANS THEN
EXISTS_TAC `x' ** y` THEN CONJ_TAC THENL
[MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC `y ** x'` THEN
REWRITE_TAC[NADD_MUL_SYM] THEN MATCH_MP_TAC NADD_EQ_TRANS THEN
EXISTS_TAC `y ** x` THEN REWRITE_TAC[NADD_MUL_SYM]; ALL_TAC] THEN
MATCH_MP_TAC NADD_MUL_WELLDEF_LEMMA THEN ASM_REWRITE_TAC[]);;
let NADD_OF_NUM_MUL = prove
(`!m n. &m ** &n === &(m * n)`,
REWRITE_TAC[nadd_eq; NADD_OF_NUM; NADD_MUL] THEN
REWRITE_TAC[MULT_ASSOC; DIST_REFL; LE_0]);;
(* ------------------------------------------------------------------------- *)
(* A few handy lemmas. *)
(* ------------------------------------------------------------------------- *)
let NADD_LE_0 = prove
(`!x. &0 <<= x`,
GEN_TAC THEN
REWRITE_TAC[nadd_le; NADD_OF_NUM; MULT_CLAUSES; LE_0]);;
let NADD_EQ_IMP_LE = prove
(`!x y. x === y ==> x <<= y`,
REPEAT GEN_TAC THEN
REWRITE_TAC[nadd_eq; nadd_le; DIST_LE_CASES] THEN
DISCH_THEN(X_CHOOSE_TAC `B:num`) THEN EXISTS_TAC `B:num` THEN
ASM_REWRITE_TAC[]);;
let NADD_LE_LMUL = prove
(`!x y z. y <<= z ==> (x ** y) <<= (x ** z)`,
REPEAT GEN_TAC THEN
DISCH_THEN(X_CHOOSE_TAC `d:nadd` o MATCH_MP NADD_LE_EXISTS) THEN
MATCH_MP_TAC NADD_LE_TRANS THEN
EXISTS_TAC `x ** y ++ x ** d` THEN REWRITE_TAC[NADD_LE_ADD] THEN
MATCH_MP_TAC NADD_EQ_IMP_LE THEN
MATCH_MP_TAC NADD_EQ_TRANS THEN
EXISTS_TAC `x ** (y ++ d)` THEN
ONCE_REWRITE_TAC[NADD_EQ_SYM] THEN
REWRITE_TAC[NADD_LDISTRIB] THEN
MATCH_MP_TAC NADD_MUL_WELLDEF THEN
ASM_REWRITE_TAC[NADD_EQ_REFL]);;
let NADD_LE_RMUL = prove
(`!x y z. x <<= y ==> (x ** z) <<= (y ** z)`,
MESON_TAC[NADD_LE_LMUL; NADD_LE_WELLDEF; NADD_MUL_SYM]);;
let NADD_LE_RADD = prove
(`!x y z. x ++ z <<= y ++ z <=> x <<= y`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NADD_ADD] THEN
GEN_REWRITE_TAC (LAND_CONV o funpow 2 BINDER_CONV o RAND_CONV)
[ADD_SYM] THEN
REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL] THEN
GEN_REWRITE_TAC (LAND_CONV o funpow 2 BINDER_CONV o RAND_CONV)
[ADD_SYM] THEN REFL_TAC);;
let NADD_LE_LADD = prove
(`!x y z. x ++ y <<= x ++ z <=> y <<= z`,
MESON_TAC[NADD_LE_RADD; NADD_ADD_SYM; NADD_LE_WELLDEF]);;
let NADD_RDISTRIB = prove
(`!x y z. (x ++ y) ** z === x ** z ++ y ** z`,
MESON_TAC[NADD_LDISTRIB; NADD_MUL_SYM; NADD_ADD_WELLDEF;
NADD_EQ_TRANS; NADD_EQ_REFL; NADD_EQ_SYM]);;
(* ------------------------------------------------------------------------- *)
(* The Archimedean property in a more useful form. *)
(* ------------------------------------------------------------------------- *)
let NADD_ARCH_MULT = prove
(`!x k. ~(x === &0) ==> ?N. &k <<= &N ** x`,
REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; nadd_le; NOT_EXISTS_THM] THEN
X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
DISCH_THEN(MP_TAC o SPEC `B + k`) THEN
REWRITE_TAC[NOT_FORALL_THM; NADD_OF_NUM] THEN
REWRITE_TAC[MULT_CLAUSES; DIST_RZERO; NOT_LE] THEN
DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN
MAP_EVERY EXISTS_TAC [`N:num`; `B * N`] THEN X_GEN_TAC `i:num` THEN
REWRITE_TAC[NADD_MUL; NADD_OF_NUM] THEN
MATCH_MP_TAC(GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL LE_ADD_RCANCEL)))) THEN
EXISTS_TAC `B * i` THEN
REWRITE_TAC[GSYM ADD_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `i * fn x N` THEN
RULE_ASSUM_TAC(REWRITE_RULE[DIST_LE_CASES]) THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] THEN
GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
MATCH_MP_TAC LT_IMP_LE THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
FIRST_ASSUM ACCEPT_TAC);;
let NADD_ARCH_ZERO = prove
(`!x k. (!n. &n ** x <<= k) ==> (x === &0)`,
REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN
REWRITE_TAC[NOT_FORALL_THM] THEN
X_CHOOSE_TAC `p:num` (SPEC `k:nadd` NADD_ARCH) THEN
FIRST_ASSUM(MP_TAC o MATCH_MP NADD_ARCH_MULT) THEN
DISCH_THEN(X_CHOOSE_TAC `N:num` o SPEC `p:num`) THEN
EXISTS_TAC `N + 1` THEN DISCH_TAC THEN UNDISCH_TAC `~(x === &0)` THEN
REWRITE_TAC[GSYM NADD_LE_ANTISYM; NADD_LE_0] THEN
MATCH_MP_TAC(GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL NADD_LE_RADD)))) THEN
EXISTS_TAC `&N ** x` THEN MATCH_MP_TAC NADD_LE_TRANS THEN
EXISTS_TAC `k:nadd` THEN CONJ_TAC THENL
[SUBGOAL_THEN `&(N + 1) ** x === x ++ &N ** x` MP_TAC THENL
[ONCE_REWRITE_TAC[ADD_SYM] THEN
MATCH_MP_TAC NADD_EQ_TRANS THEN
EXISTS_TAC `&1 ** x ++ &N ** x` THEN CONJ_TAC THENL
[MATCH_MP_TAC NADD_EQ_TRANS THEN
EXISTS_TAC `(&1 ++ &N) ** x` THEN CONJ_TAC THENL
[MESON_TAC[NADD_OF_NUM_ADD; NADD_MUL_WELLDEF; NADD_EQ_REFL;
NADD_EQ_SYM];
MESON_TAC[NADD_RDISTRIB; NADD_MUL_SYM; NADD_EQ_SYM; NADD_EQ_TRANS]];
MESON_TAC[NADD_ADD_WELLDEF; NADD_EQ_REFL; NADD_MUL_LID]];
ASM_MESON_TAC[NADD_LE_WELLDEF; NADD_EQ_REFL]];
ASM_MESON_TAC[NADD_LE_TRANS; NADD_LE_WELLDEF; NADD_EQ_REFL;
NADD_ADD_LID]]);;
let NADD_ARCH_LEMMA = prove
(`!x y z. (!n. &n ** x <<= &n ** y ++ z) ==> x <<= y`,
REPEAT STRIP_TAC THEN
DISJ_CASES_TAC(SPECL [`x:nadd`; `y:nadd`] NADD_LE_TOTAL) THEN
ASM_REWRITE_TAC[] THEN
FIRST_ASSUM(X_CHOOSE_TAC `d:nadd` o MATCH_MP NADD_LE_EXISTS) THEN
MATCH_MP_TAC NADD_EQ_IMP_LE THEN
MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC `y ++ d` THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC `y ++ &0` THEN CONJ_TAC THENL
[MATCH_MP_TAC NADD_ADD_WELLDEF THEN REWRITE_TAC[NADD_EQ_REFL] THEN
MATCH_MP_TAC NADD_ARCH_ZERO THEN EXISTS_TAC `z:nadd` THEN
ASM_MESON_TAC[NADD_MUL_WELLDEF; NADD_LE_WELLDEF; NADD_LDISTRIB;
NADD_LE_LADD; NADD_EQ_REFL];
ASM_MESON_TAC[NADD_ADD_LID; NADD_ADD_WELLDEF; NADD_EQ_TRANS;
NADD_ADD_SYM]]);;
(* ------------------------------------------------------------------------- *)
(* Completeness. *)
(* ------------------------------------------------------------------------- *)
let NADD_COMPLETE = prove
(`!P. (?x. P x) /\ (?M. !x. P x ==> x <<= M) ==>
?M. (!x. P x ==> x <<= M) /\
!M'. (!x. P x ==> x <<= M') ==> M <<= M'`,
GEN_TAC THEN DISCH_THEN
(CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:nadd`) (X_CHOOSE_TAC `m:nadd`)) THEN
SUBGOAL_THEN
`!n. ?r. (?x. P x /\ &r <<= &n ** x) /\
!r'. (?x. P x /\ &r' <<= &n ** x) ==> r' <= r` MP_TAC THENL
[GEN_TAC THEN REWRITE_TAC[GSYM num_MAX] THEN CONJ_TAC THENL
[MAP_EVERY EXISTS_TAC [`0`; `a:nadd`] THEN ASM_REWRITE_TAC[NADD_LE_0];
X_CHOOSE_TAC `N:num` (SPEC `m:nadd` NADD_ARCH) THEN
EXISTS_TAC `n * N` THEN X_GEN_TAC `p:num` THEN
DISCH_THEN(X_CHOOSE_THEN `w:nadd` STRIP_ASSUME_TAC) THEN
ONCE_REWRITE_TAC[GSYM NADD_OF_NUM_LE] THEN
MATCH_MP_TAC NADD_LE_TRANS THEN EXISTS_TAC `&n ** w` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NADD_LE_TRANS THEN
EXISTS_TAC `&n ** &N` THEN CONJ_TAC THENL
[MATCH_MP_TAC NADD_LE_LMUL THEN MATCH_MP_TAC NADD_LE_TRANS THEN
EXISTS_TAC `m:nadd` THEN ASM_REWRITE_TAC[] THEN
FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
MATCH_MP_TAC NADD_EQ_IMP_LE THEN
MATCH_ACCEPT_TAC NADD_OF_NUM_MUL]];
ONCE_REWRITE_TAC[SKOLEM_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `r:num->num`
(fun th -> let th1,th2 = CONJ_PAIR(SPEC `n:num` th) in
MAP_EVERY (MP_TAC o GEN `n:num`) [th1; th2])) THEN
DISCH_THEN(MP_TAC o GEN `n:num` o SPECL [`n:num`; `SUC(r(n:num))`]) THEN
REWRITE_TAC[LE_SUC_LT; LT_REFL; NOT_EXISTS_THM] THEN
DISCH_THEN(ASSUME_TAC o GENL [`n:num`; `x:nadd`] o MATCH_MP
(ITAUT `(a \/ b) /\ ~(c /\ b) ==> c ==> a`) o CONJ
(SPECL [`&n ** x`; `&(SUC(r(n:num)))`] NADD_LE_TOTAL) o SPEC_ALL) THEN
DISCH_TAC] THEN
SUBGOAL_THEN `!n i. i * r(n) <= n * r(i) + n` ASSUME_TAC THENL
[REPEAT GEN_TAC THEN
FIRST_ASSUM(X_CHOOSE_THEN `x:nadd` STRIP_ASSUME_TAC o SPEC `n:num`) THEN
ONCE_REWRITE_TAC[GSYM NADD_OF_NUM_LE] THEN
MATCH_MP_TAC NADD_LE_TRANS THEN
EXISTS_TAC `&i ** &n ** x` THEN CONJ_TAC THENL
[MATCH_MP_TAC NADD_LE_TRANS THEN
EXISTS_TAC `&i ** &(r(n:num))` THEN CONJ_TAC THENL
[MATCH_MP_TAC NADD_EQ_IMP_LE THEN
ONCE_REWRITE_TAC[NADD_EQ_SYM] THEN MATCH_ACCEPT_TAC NADD_OF_NUM_MUL;
MATCH_MP_TAC NADD_LE_LMUL THEN ASM_REWRITE_TAC[]];
MATCH_MP_TAC NADD_LE_TRANS THEN
EXISTS_TAC `&n ** &(SUC(r(i:num)))` THEN CONJ_TAC THENL
[MATCH_MP_TAC NADD_LE_TRANS THEN EXISTS_TAC `&n ** &i ** x` THEN
CONJ_TAC THENL
[MATCH_MP_TAC NADD_EQ_IMP_LE THEN
MATCH_MP_TAC NADD_EQ_TRANS THEN
EXISTS_TAC `(&i ** &n) ** x` THEN
REWRITE_TAC[NADD_MUL_ASSOC] THEN
MATCH_MP_TAC NADD_EQ_TRANS THEN
EXISTS_TAC `(&n ** &i) ** x` THEN
REWRITE_TAC[ONCE_REWRITE_RULE[NADD_EQ_SYM] NADD_MUL_ASSOC] THEN
MATCH_MP_TAC NADD_MUL_WELLDEF THEN
REWRITE_TAC[NADD_MUL_SYM; NADD_EQ_REFL];
MATCH_MP_TAC NADD_LE_LMUL THEN
FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]];
ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM MULT_SUC] THEN
MATCH_MP_TAC NADD_EQ_IMP_LE THEN
REWRITE_TAC[NADD_OF_NUM_MUL]]]; ALL_TAC] THEN
EXISTS_TAC `afn r` THEN SUBGOAL_THEN `fn(afn r) = r` ASSUME_TAC THENL
[REWRITE_TAC[GSYM nadd_rep] THEN REWRITE_TAC[is_nadd; DIST_LE_CASES] THEN
EXISTS_TAC `1` THEN REWRITE_TAC[MULT_CLAUSES] THEN
REWRITE_TAC[FORALL_AND_THM] THEN
GEN_REWRITE_TAC RAND_CONV [SWAP_FORALL_THM] THEN
GEN_REWRITE_TAC (LAND_CONV o funpow 2 BINDER_CONV o
funpow 2 RAND_CONV) [ADD_SYM] THEN
REWRITE_TAC[] THEN MAP_EVERY X_GEN_TAC [`i:num`; `n:num`] THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `n * r(i:num) + n` THEN
ASM_REWRITE_TAC[ADD_ASSOC; LE_ADD]; ALL_TAC] THEN
CONJ_TAC THENL
[X_GEN_TAC `x:nadd` THEN DISCH_TAC THEN
MATCH_MP_TAC NADD_ARCH_LEMMA THEN
EXISTS_TAC `&2` THEN X_GEN_TAC `n:num` THEN
MATCH_MP_TAC NADD_LE_TRANS THEN
EXISTS_TAC `&(SUC(r(n:num)))` THEN CONJ_TAC THENL
[FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[nadd_le; NADD_ADD; NADD_MUL; NADD_OF_NUM] THEN
ONCE_REWRITE_TAC[ADD_SYM] THEN
REWRITE_TAC[ADD1; RIGHT_ADD_DISTRIB] THEN
REWRITE_TAC[MULT_2; MULT_CLAUSES; ADD_ASSOC; LE_ADD_RCANCEL] THEN
REWRITE_TAC[GSYM ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
ONCE_REWRITE_TAC[BOUNDS_IGNORE] THEN
MAP_EVERY EXISTS_TAC [`0`; `n:num`] THEN
X_GEN_TAC `i:num` THEN DISCH_TAC THEN
GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `n * r(i:num) + n` THEN
ASM_REWRITE_TAC[LE_ADD_LCANCEL; ADD_CLAUSES]];
X_GEN_TAC `z:nadd` THEN DISCH_TAC THEN
MATCH_MP_TAC NADD_ARCH_LEMMA THEN EXISTS_TAC `&1` THEN
X_GEN_TAC `n:num` THEN MATCH_MP_TAC NADD_LE_TRANS THEN
EXISTS_TAC `&(r(n:num)) ++ &1` THEN CONJ_TAC THENL
[ASM_REWRITE_TAC[nadd_le; NADD_ADD; NADD_MUL; NADD_OF_NUM] THEN
EXISTS_TAC `0` THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
GEN_TAC THEN GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [MULT_SYM] THEN
ASM_REWRITE_TAC[];
REWRITE_TAC[NADD_LE_RADD] THEN
FIRST_ASSUM(X_CHOOSE_THEN `x:nadd` MP_TAC o SPEC `n:num`) THEN
DISCH_THEN STRIP_ASSUME_TAC THEN
MATCH_MP_TAC NADD_LE_TRANS THEN EXISTS_TAC `&n ** x` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NADD_LE_LMUL THEN
FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]]);;
(* ------------------------------------------------------------------------- *)
(* A bit more on nearly-multiplicative functions. *)
(* ------------------------------------------------------------------------- *)
let NADD_UBOUND = prove
(`!x. ?B N. !n. N <= n ==> fn x n <= B * n`,
GEN_TAC THEN X_CHOOSE_THEN `A1:num`
(X_CHOOSE_TAC `A2:num`) (SPEC `x:nadd` NADD_BOUND) THEN
EXISTS_TAC `A1 + A2` THEN EXISTS_TAC `1` THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
EXISTS_TAC `A1 * n + A2` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM(el 3 (CONJUNCTS MULT_CLAUSES))] THEN
ASM_REWRITE_TAC[LE_MULT_LCANCEL]);;
let NADD_NONZERO = prove
(`!x. ~(x === &0) ==> ?N. !n. N <= n ==> ~(fn x n = 0)`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_ARCH_MULT) THEN
DISCH_THEN(MP_TAC o SPEC `1`) THEN
REWRITE_TAC[nadd_le; NADD_MUL; NADD_OF_NUM; MULT_CLAUSES] THEN
DISCH_THEN(X_CHOOSE_THEN `A1:num` (X_CHOOSE_TAC `A2:num`)) THEN
EXISTS_TAC `A2 + 1` THEN X_GEN_TAC `n:num` THEN REPEAT DISCH_TAC THEN
FIRST_ASSUM(UNDISCH_TAC o check is_forall o concl) THEN
REWRITE_TAC[NOT_FORALL_THM; NOT_LE; GSYM LE_SUC_LT; ADD1] THEN
EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]);;
let NADD_LBOUND = prove
(`!x. ~(x === &0) ==> ?A N. !n. N <= n ==> n <= A * fn x n`,
GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(X_CHOOSE_TAC `N:num` o MATCH_MP NADD_NONZERO) THEN
FIRST_ASSUM(MP_TAC o MATCH_MP NADD_ARCH_MULT) THEN
DISCH_THEN(MP_TAC o SPEC `1`) THEN
REWRITE_TAC[nadd_le; NADD_MUL; NADD_OF_NUM; MULT_CLAUSES] THEN
DISCH_THEN(X_CHOOSE_THEN `A1:num` (X_CHOOSE_TAC `A2:num`)) THEN
EXISTS_TAC `A1 + A2` THEN EXISTS_TAC `N:num` THEN GEN_TAC THEN
DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A1 * fn x n + A2` THEN
ASM_REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM(el 3 (CONJUNCTS MULT_CLAUSES))] THEN
REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
REWRITE_TAC[GSYM(REWRITE_CONV[ARITH_SUC] `SUC 0`)] THEN
ASM_REWRITE_TAC[GSYM NOT_LT; LT]);;
(* ------------------------------------------------------------------------- *)
(* Auxiliary function for the multiplicative inverse. *)
(* ------------------------------------------------------------------------- *)
let nadd_rinv = new_definition
`nadd_rinv(x) = \n. (n * n) DIV (fn x n)`;;
let NADD_MUL_LINV_LEMMA0 = prove
(`!x. ~(x === &0) ==> ?A B. !n. nadd_rinv x n <= A * n + B`,
GEN_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[BOUNDS_IGNORE] THEN
FIRST_ASSUM(MP_TAC o MATCH_MP NADD_LBOUND) THEN
DISCH_THEN(X_CHOOSE_THEN `A:num` (X_CHOOSE_TAC `N:num`)) THEN
MAP_EVERY EXISTS_TAC [`A:num`; `0`; `SUC N`] THEN
GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN
MP_TAC(SPECL [`nadd_rinv x n`; `A * n`; `n:num`] LE_MULT_RCANCEL) THEN
UNDISCH_TAC `SUC N <= n` THEN ASM_CASES_TAC `n = 0` THEN
ASM_REWRITE_TAC[LE; NOT_SUC] THEN DISCH_TAC THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `nadd_rinv x n * A * fn x n` THEN
ASM_REWRITE_TAC[LE_MULT_LCANCEL] THEN CONJ_TAC THENL
[DISJ2_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
EXISTS_TAC `SUC N` THEN ASM_REWRITE_TAC[LE; LE_REFL];
GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN
REWRITE_TAC[GSYM MULT_ASSOC; LE_MULT_LCANCEL] THEN
DISJ2_TAC THEN ASM_CASES_TAC `fn x n = 0` THEN
ASM_REWRITE_TAC[MULT_CLAUSES; LE_0; nadd_rinv] THEN
FIRST_ASSUM(MP_TAC o MATCH_MP DIVISION) THEN
DISCH_THEN(fun t -> GEN_REWRITE_TAC RAND_CONV [CONJUNCT1(SPEC_ALL t)]) THEN
GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN REWRITE_TAC[LE_ADD]]);;
let NADD_MUL_LINV_LEMMA1 = prove
(`!x n. ~(fn x n = 0) ==> dist(fn x n * nadd_rinv(x) n, n * n) <= fn x n`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP DIVISION) THEN
DISCH_THEN(CONJUNCTS_THEN2 SUBST1_TAC ASSUME_TAC o SPEC `n * n`) THEN
REWRITE_TAC[nadd_rinv] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [MULT_SYM] THEN
REWRITE_TAC[DIST_RADD_0] THEN MATCH_MP_TAC LT_IMP_LE THEN
FIRST_ASSUM MATCH_ACCEPT_TAC);;
let NADD_MUL_LINV_LEMMA2 = prove
(`!x. ~(x === &0) ==> ?N. !n. N <= n ==>
dist(fn x n * nadd_rinv(x) n, n * n) <= fn x n`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_NONZERO) THEN
DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `N:num` THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC NADD_MUL_LINV_LEMMA1 THEN
FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
let NADD_MUL_LINV_LEMMA3 = prove
(`!x. ~(x === &0) ==> ?N. !m n. N <= n ==>
dist(m * fn x m * fn x n * nadd_rinv(x) n,
m * fn x m * n * n) <= m * fn x m * fn x n`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA2) THEN
DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `N:num` THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM DIST_LMUL; MULT_ASSOC] THEN
REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
let NADD_MUL_LINV_LEMMA4 = prove
(`!x. ~(x === &0) ==> ?N. !m n. N <= m /\ N <= n ==>
(fn x m * fn x n) * dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <=
(m * n) * dist(m * fn x n,n * fn x m) + (fn x m * fn x n) * (m + n)`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA3) THEN
DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `N:num` THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[DIST_LMUL; LEFT_ADD_DISTRIB] THEN
GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [DIST_SYM] THEN
MATCH_MP_TAC DIST_TRIANGLES_LE THEN CONJ_TAC THENL
[ANTE_RES_THEN(MP_TAC o SPEC `m:num`) (ASSUME `N <= n`);
ANTE_RES_THEN(MP_TAC o SPEC `n:num`) (ASSUME `N <= m`)] THEN
MATCH_MP_TAC EQ_IMP THEN REWRITE_TAC[MULT_AC]);;
let NADD_MUL_LINV_LEMMA5 = prove
(`!x. ~(x === &0) ==> ?B N. !m n. N <= m /\ N <= n ==>
(fn x m * fn x n) * dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <=
B * (m * n) * (m + n)`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA4) THEN
DISCH_THEN(X_CHOOSE_TAC `N1:num`) THEN
X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
X_CHOOSE_THEN `B2:num` (X_CHOOSE_TAC `N2:num`)
(SPEC `x:nadd` NADD_UBOUND) THEN
EXISTS_TAC `B1 + B2 * B2` THEN EXISTS_TAC `N1 + N2` THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
EXISTS_TAC `(m * n) * dist(m * fn x n,n * fn x m) +
(fn x m * fn x n) * (m + n)` THEN
CONJ_TAC THENL
[FIRST_ASSUM MATCH_MP_TAC THEN CONJ_TAC THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N1 + N2` THEN
ASM_REWRITE_TAC[LE_ADD; LE_ADDR];
REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN MATCH_MP_TAC LE_ADD2] THEN
CONJ_TAC THENL
[GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
GEN_REWRITE_TAC RAND_CONV [GSYM MULT_ASSOC] THEN
GEN_REWRITE_TAC (funpow 2 RAND_CONV) [MULT_SYM] THEN
ASM_REWRITE_TAC[LE_MULT_LCANCEL];
ONCE_REWRITE_TAC[AC MULT_AC
`(a * b) * (c * d) * e = ((a * c) * (b * d)) * e`] THEN
REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
MATCH_MP_TAC LE_MULT2 THEN CONJ_TAC THEN
FIRST_ASSUM MATCH_MP_TAC THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N1 + N2` THEN
ASM_REWRITE_TAC[LE_ADD; LE_ADDR]]);;
let NADD_MUL_LINV_LEMMA6 = prove
(`!x. ~(x === &0) ==> ?B N. !m n. N <= m /\ N <= n ==>
(m * n) * dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <=
B * (m * n) * (m + n)`,
GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA5) THEN
DISCH_THEN(X_CHOOSE_THEN `B1:num` (X_CHOOSE_TAC `N1:num`)) THEN
FIRST_ASSUM(MP_TAC o MATCH_MP NADD_LBOUND) THEN
DISCH_THEN(X_CHOOSE_THEN `B2:num` (X_CHOOSE_TAC `N2:num`)) THEN
EXISTS_TAC `B1 * B2 * B2` THEN EXISTS_TAC `N1 + N2` THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
EXISTS_TAC `(B2 * B2) * (fn x m * fn x n) *
dist (m * nadd_rinv x n,n * nadd_rinv x m)` THEN
CONJ_TAC THENL
[REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
ONCE_REWRITE_TAC[AC MULT_AC `((a * b) * c) * d = (a * c) * (b * d)`] THEN
MATCH_MP_TAC LE_MULT2 THEN CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC;
ONCE_REWRITE_TAC[AC MULT_AC
`(a * b * c) * (d * e) * f = (b * c) * (a * (d * e) * f)`] THEN
REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
FIRST_ASSUM MATCH_MP_TAC THEN CONJ_TAC] THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N1 + N2` THEN
ASM_REWRITE_TAC[LE_ADD; LE_ADDR]);;
let NADD_MUL_LINV_LEMMA7 = prove
(`!x. ~(x === &0) ==> ?B N. !m n. N <= m /\ N <= n ==>
dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <= B * (m + n)`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA6) THEN
DISCH_THEN(X_CHOOSE_THEN `B:num` (X_CHOOSE_TAC `N:num`)) THEN
MAP_EVERY EXISTS_TAC [`B:num`; `N + 1`] THEN
MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
SUBGOAL_THEN `N <= m /\ N <= n` MP_TAC THENL
[CONJ_TAC THEN MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N + 1` THEN
ASM_REWRITE_TAC[LE_ADD];
DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
ONCE_REWRITE_TAC[AC MULT_AC `a * b * c = b * a * c`] THEN
REWRITE_TAC[LE_MULT_LCANCEL] THEN
DISCH_THEN(DISJ_CASES_THEN2 MP_TAC ACCEPT_TAC) THEN
CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
ONCE_REWRITE_TAC[GSYM(CONJUNCT1 LE)] THEN
REWRITE_TAC[NOT_LE; GSYM LE_SUC_LT] THEN
REWRITE_TAC[EQT_ELIM(REWRITE_CONV[ARITH] `SUC 0 = 1 * 1`)] THEN
MATCH_MP_TAC LE_MULT2 THEN CONJ_TAC THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N + 1` THEN
ASM_REWRITE_TAC[LE_ADDR]]);;
let NADD_MUL_LINV_LEMMA7a = prove
(`!x. ~(x === &0) ==> !N. ?A B. !m n. m <= N ==>
dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <= A * n + B`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA0) THEN
DISCH_THEN(X_CHOOSE_THEN `A0:num` (X_CHOOSE_TAC `B0:num`)) THEN
INDUCT_TAC THENL
[MAP_EVERY EXISTS_TAC [`nadd_rinv x 0`; `0`] THEN
REPEAT GEN_TAC THEN REWRITE_TAC[LE] THEN DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[MULT_CLAUSES; DIST_LZERO; ADD_CLAUSES] THEN
GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN MATCH_ACCEPT_TAC LE_REFL;
FIRST_ASSUM(X_CHOOSE_THEN `A:num` (X_CHOOSE_TAC `B:num`)) THEN
EXISTS_TAC `A + (nadd_rinv(x)(SUC N) + SUC N * A0)` THEN
EXISTS_TAC `SUC N * B0 + B` THEN
REPEAT GEN_TAC THEN REWRITE_TAC[LE] THEN
DISCH_THEN(DISJ_CASES_THEN2 SUBST1_TAC ASSUME_TAC) THENL
[MATCH_MP_TAC LE_TRANS THEN
EXISTS_TAC `SUC N * nadd_rinv x n + n * nadd_rinv x (SUC N)` THEN
REWRITE_TAC[DIST_ADDBOUND] THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
ONCE_REWRITE_TAC[AC ADD_AC
`(a + b + c) + d + e = (c + d) + (b + a + e)`] THEN
MATCH_MP_TAC LE_ADD2 THEN CONJ_TAC THENL
[REWRITE_TAC[GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
ASM_REWRITE_TAC[LE_MULT_LCANCEL];
GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN
MATCH_ACCEPT_TAC LE_ADD];
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * n + B` THEN CONJ_TAC THENL
[FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL] THEN
REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC; LE_ADD]]]]);;
let NADD_MUL_LINV_LEMMA8 = prove
(`!x. ~(x === &0) ==>
?B. !m n. dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <= B * (m + n)`,
GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA7) THEN
DISCH_THEN(X_CHOOSE_THEN `B0:num` (X_CHOOSE_TAC `N:num`)) THEN
FIRST_ASSUM(MP_TAC o SPEC `N:num` o MATCH_MP NADD_MUL_LINV_LEMMA7a) THEN
DISCH_THEN(X_CHOOSE_THEN `A:num` (X_CHOOSE_TAC `B:num`)) THEN
MATCH_MP_TAC BOUNDS_NOTZERO THEN REWRITE_TAC[DIST_REFL] THEN
EXISTS_TAC `A + B0` THEN EXISTS_TAC `B:num` THEN REPEAT GEN_TAC THEN
DISJ_CASES_THEN2 ASSUME_TAC MP_TAC (SPECL [`N:num`; `m:num`] LE_CASES) THENL
[DISJ_CASES_THEN2 ASSUME_TAC MP_TAC (SPECL [`N:num`; `n:num`] LE_CASES)
THENL
[MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `B0 * (m + n)` THEN CONJ_TAC THENL
[FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
GEN_REWRITE_TAC (RAND_CONV o funpow 2 LAND_CONV) [ADD_SYM] THEN
REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC; LE_ADD]];
DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * m + B` THEN
ONCE_REWRITE_TAC[DIST_SYM] THEN
ASM_REWRITE_TAC[LE_ADD_RCANCEL] THEN
REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC;
LE_ADD]];
DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * n + B` THEN
ASM_REWRITE_TAC[LE_ADD_RCANCEL] THEN
GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [ADD_SYM] THEN
REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC;
LE_ADD]]);;
(* ------------------------------------------------------------------------- *)
(* Now the multiplicative inverse proper. *)
(* ------------------------------------------------------------------------- *)
let nadd_inv = new_definition
`nadd_inv(x) = if x === &0 then &0 else afn(nadd_rinv x)`;;
override_interface ("inv",`nadd_inv:nadd->nadd`);;
let NADD_INV = prove
(`!x. fn(nadd_inv x) = if x === &0 then (\n. 0) else nadd_rinv x`,
GEN_TAC THEN REWRITE_TAC[nadd_inv] THEN
ASM_CASES_TAC `x === &0` THEN ASM_REWRITE_TAC[NADD_OF_NUM; MULT_CLAUSES] THEN
REWRITE_TAC[GSYM nadd_rep; is_nadd] THEN
MATCH_MP_TAC NADD_MUL_LINV_LEMMA8 THEN POP_ASSUM ACCEPT_TAC);;
let NADD_MUL_LINV = prove
(`!x. ~(x === &0) ==> inv(x) ** x === &1`,
GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[nadd_eq; NADD_MUL] THEN
ONCE_REWRITE_TAC[BOUNDS_DIVIDED] THEN
X_CHOOSE_THEN `A1:num` (X_CHOOSE_TAC `B1:num`)
(SPECL [`inv(x)`; `x:nadd`] NADD_ALTMUL) THEN
REWRITE_TAC[DIST_LMUL; NADD_OF_NUM; MULT_CLAUSES] THEN
FIRST_ASSUM(X_CHOOSE_TAC `N:num` o MATCH_MP NADD_MUL_LINV_LEMMA2) THEN
X_CHOOSE_THEN `A':num` (X_CHOOSE_TAC `B':num`)
(SPEC `x:nadd` NADD_BOUND) THEN
SUBGOAL_THEN `?A2 B2. !n. dist(fn x n * nadd_rinv x n,n * n) <= A2 * n + B2`
STRIP_ASSUME_TAC THENL
[EXISTS_TAC `A':num` THEN ONCE_REWRITE_TAC[BOUNDS_IGNORE] THEN
MAP_EVERY EXISTS_TAC [`B':num`; `N:num`] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `fn x n` THEN ASM_REWRITE_TAC[] THEN
FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
MAP_EVERY EXISTS_TAC [`A1 + A2`; `B1 + B2`] THEN
GEN_TAC THEN MATCH_MP_TAC DIST_TRIANGLE_LE THEN
EXISTS_TAC `fn (inv x) n * fn x n` THEN
REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
ONCE_REWRITE_TAC[AC ADD_AC `(a + b) + c + d = (a + c) + (b + d)`] THEN
MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [MULT_SYM] THEN
ASM_REWRITE_TAC[NADD_INV]]);;
let NADD_INV_0 = prove
(`inv(&0) === &0`,
REWRITE_TAC[nadd_inv; NADD_EQ_REFL]);;
(* ------------------------------------------------------------------------- *)
(* Welldefinedness follows from already established principles because if *)
(* x = y then y' = y' 1 = y' (x' x) = y' (x' y) = (y' y) x' = 1 x' = x' *)
(* ------------------------------------------------------------------------- *)
let NADD_INV_WELLDEF = prove
(`!x y. x === y ==> inv(x) === inv(y)`,
let TAC tm ths =
MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC tm THEN
CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC ths] in
REPEAT STRIP_TAC THEN
ASM_CASES_TAC `x === &0` THENL
[SUBGOAL_THEN `y === &0` ASSUME_TAC THENL
[ASM_MESON_TAC[NADD_EQ_TRANS; NADD_EQ_SYM];
ASM_REWRITE_TAC[nadd_inv; NADD_EQ_REFL]];
SUBGOAL_THEN `~(y === &0)` ASSUME_TAC THENL
[ASM_MESON_TAC[NADD_EQ_TRANS; NADD_EQ_SYM]; ALL_TAC]] THEN
TAC `inv(y) ** &1`
[NADD_MUL_SYM; NADD_MUL_LID; NADD_EQ_TRANS] THEN
TAC `inv(y) ** (inv(x) ** x)`
[NADD_MUL_LINV; NADD_MUL_WELLDEF; NADD_EQ_REFL] THEN
TAC `inv(y) ** (inv(x) ** y)`
[NADD_MUL_WELLDEF; NADD_EQ_REFL; NADD_EQ_SYM] THEN
TAC `(inv(y) ** y) ** inv(x)`
[NADD_MUL_ASSOC; NADD_MUL_SYM; NADD_EQ_TRANS;
NADD_MUL_WELLDEF; NADD_EQ_REFL] THEN
ASM_MESON_TAC[NADD_MUL_LINV; NADD_MUL_WELLDEF; NADD_EQ_REFL;
NADD_MUL_LID; NADD_EQ_TRANS; NADD_EQ_SYM]);;
(* ------------------------------------------------------------------------- *)
(* Definition of the new type. *)
(* ------------------------------------------------------------------------- *)
let hreal_tybij =
define_quotient_type "hreal" ("mk_hreal","dest_hreal") `(===)`;;
do_list overload_interface
["+",`hreal_add:hreal->hreal->hreal`;
"*",`hreal_mul:hreal->hreal->hreal`;
"<=",`hreal_le:hreal->hreal->bool`];;
do_list override_interface
["&",`hreal_of_num:num->hreal`;
"inv",`hreal_inv:hreal->hreal`];;
let hreal_of_num,hreal_of_num_th =
lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
"hreal_of_num" NADD_OF_NUM_WELLDEF;;
let hreal_add,hreal_add_th =
lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
"hreal_add" NADD_ADD_WELLDEF;;
let hreal_mul,hreal_mul_th =
lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
"hreal_mul" NADD_MUL_WELLDEF;;
let hreal_le,hreal_le_th =
lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
"hreal_le" NADD_LE_WELLDEF;;
let hreal_inv,hreal_inv_th =
lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
"hreal_inv" NADD_INV_WELLDEF;;
let HREAL_COMPLETE =
let th1 = ASSUME `(P:nadd->bool) = (\x. Q(mk_hreal((===) x)))` in
let th2 = BETA_RULE(AP_THM th1 `x:nadd`) in
let th3 = lift_theorem hreal_tybij
(NADD_EQ_REFL,NADD_EQ_SYM,NADD_EQ_TRANS)
[hreal_of_num_th; hreal_add_th; hreal_mul_th; hreal_le_th; th2]
(SPEC_ALL NADD_COMPLETE) in
let th4 = MATCH_MP (DISCH_ALL th3) (REFL `\x. Q(mk_hreal((===) x)):bool`) in
CONV_RULE(GEN_ALPHA_CONV `P:hreal->bool`) (GEN_ALL th4);;
let [HREAL_OF_NUM_EQ; HREAL_OF_NUM_LE; HREAL_OF_NUM_ADD; HREAL_OF_NUM_MUL;
HREAL_LE_REFL; HREAL_LE_TRANS; HREAL_LE_ANTISYM; HREAL_LE_TOTAL;
HREAL_LE_ADD; HREAL_LE_EXISTS; HREAL_ARCH; HREAL_ADD_SYM; HREAL_ADD_ASSOC;
HREAL_ADD_LID; HREAL_ADD_LCANCEL; HREAL_MUL_SYM; HREAL_MUL_ASSOC;
HREAL_MUL_LID; HREAL_ADD_LDISTRIB; HREAL_MUL_LINV; HREAL_INV_0] =
map (lift_theorem hreal_tybij
(NADD_EQ_REFL,NADD_EQ_SYM,NADD_EQ_TRANS)
[hreal_of_num_th; hreal_add_th; hreal_mul_th;
hreal_le_th; hreal_inv_th])
[NADD_OF_NUM_EQ; NADD_OF_NUM_LE; NADD_OF_NUM_ADD; NADD_OF_NUM_MUL;
NADD_LE_REFL; NADD_LE_TRANS; NADD_LE_ANTISYM; NADD_LE_TOTAL; NADD_LE_ADD;
NADD_LE_EXISTS; NADD_ARCH; NADD_ADD_SYM; NADD_ADD_ASSOC; NADD_ADD_LID;
NADD_ADD_LCANCEL; NADD_MUL_SYM; NADD_MUL_ASSOC; NADD_MUL_LID; NADD_LDISTRIB;
NADD_MUL_LINV; NADD_INV_0];;
(* ------------------------------------------------------------------------- *)
(* Consequential theorems needed later. *)
(* ------------------------------------------------------------------------- *)
let HREAL_LE_EXISTS_DEF = prove
(`!m n. m <= n <=> ?d. n = m + d`,
REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[HREAL_LE_EXISTS] THEN
DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN REWRITE_TAC[HREAL_LE_ADD]);;
let HREAL_EQ_ADD_LCANCEL = prove
(`!m n p. (m + n = m + p) <=> (n = p)`,
REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[HREAL_ADD_LCANCEL] THEN
DISCH_THEN SUBST1_TAC THEN REFL_TAC);;
let HREAL_EQ_ADD_RCANCEL = prove
(`!m n p. (m + p = n + p) <=> (m = n)`,
ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN REWRITE_TAC[HREAL_EQ_ADD_LCANCEL]);;
let HREAL_LE_ADD_LCANCEL = prove
(`!m n p. (m + n <= m + p) <=> (n <= p)`,
REWRITE_TAC[HREAL_LE_EXISTS_DEF; GSYM HREAL_ADD_ASSOC;
HREAL_EQ_ADD_LCANCEL]);;
let HREAL_LE_ADD_RCANCEL = prove
(`!m n p. (m + p <= n + p) <=> (m <= n)`,
ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN MATCH_ACCEPT_TAC HREAL_LE_ADD_LCANCEL);;
let HREAL_ADD_RID = prove
(`!n. n + &0 = n`,
ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN MATCH_ACCEPT_TAC HREAL_ADD_LID);;
let HREAL_ADD_RDISTRIB = prove
(`!m n p. (m + n) * p = m * p + n * p`,
ONCE_REWRITE_TAC[HREAL_MUL_SYM] THEN MATCH_ACCEPT_TAC HREAL_ADD_LDISTRIB);;
let HREAL_MUL_LZERO = prove
(`!m. &0 * m = &0`,
GEN_TAC THEN MP_TAC(SPECL [`&0`; `&1`; `m:hreal`] HREAL_ADD_RDISTRIB) THEN
REWRITE_TAC[HREAL_ADD_LID] THEN
GEN_REWRITE_TAC (funpow 2 LAND_CONV) [GSYM HREAL_ADD_LID] THEN
REWRITE_TAC[HREAL_EQ_ADD_RCANCEL] THEN
DISCH_THEN(ACCEPT_TAC o SYM));;
let HREAL_MUL_RZERO = prove
(`!m. m * &0 = &0`,
ONCE_REWRITE_TAC[HREAL_MUL_SYM] THEN MATCH_ACCEPT_TAC HREAL_MUL_LZERO);;
let HREAL_ADD_AC = prove
(`(m + n = n + m) /\
((m + n) + p = m + (n + p)) /\
(m + (n + p) = n + (m + p))`,
REWRITE_TAC[HREAL_ADD_ASSOC; EQT_INTRO(SPEC_ALL HREAL_ADD_SYM)] THEN
AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_ACCEPT_TAC HREAL_ADD_SYM);;
let HREAL_LE_ADD2 = prove
(`!a b c d. a <= b /\ c <= d ==> a + c <= b + d`,
REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LE_EXISTS_DEF] THEN
DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `d1:hreal`)
(X_CHOOSE_TAC `d2:hreal`)) THEN
EXISTS_TAC `d1 + d2` THEN ASM_REWRITE_TAC[HREAL_ADD_AC]);;
let HREAL_LE_MUL_RCANCEL_IMP = prove
(`!a b c. a <= b ==> a * c <= b * c`,
REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LE_EXISTS_DEF] THEN
DISCH_THEN(X_CHOOSE_THEN `d:hreal` SUBST1_TAC) THEN
EXISTS_TAC `d * c` THEN REWRITE_TAC[HREAL_ADD_RDISTRIB]);;
(* ------------------------------------------------------------------------- *)
(* Define operations on representatives of signed reals. *)
(* ------------------------------------------------------------------------- *)
let treal_of_num = new_definition
`treal_of_num n = (&n, &0)`;;
let treal_neg = new_definition
`treal_neg ((x:hreal),(y:hreal)) = (y,x)`;;
let treal_add = new_definition
`(x1,y1) treal_add (x2,y2) = (x1 + x2, y1 + y2)`;;
let treal_mul = new_definition
`(x1,y1) treal_mul (x2,y2) = ((x1 * x2) + (y1 * y2),(x1 * y2) + (y1 * x2))`;;
let treal_le = new_definition
`(x1,y1) treal_le (x2,y2) <=> x1 + y2 <= x2 + y1`;;
let treal_inv = new_definition
`treal_inv(x,y) = if x = y then (&0, &0)
else if y <= x then (inv(@d. x = y + d), &0)
else (&0, inv(@d. y = x + d))`;;
(* ------------------------------------------------------------------------- *)
(* Define the equivalence relation and prove it *is* one. *)
(* ------------------------------------------------------------------------- *)
let treal_eq = new_definition
`(x1,y1) treal_eq (x2,y2) <=> (x1 + y2 = x2 + y1)`;;
let TREAL_EQ_REFL = prove
(`!x. x treal_eq x`,
REWRITE_TAC[FORALL_PAIR_THM; treal_eq]);;
let TREAL_EQ_SYM = prove
(`!x y. x treal_eq y <=> y treal_eq x`,
REWRITE_TAC[FORALL_PAIR_THM; treal_eq; EQ_SYM_EQ]);;
let TREAL_EQ_TRANS = prove
(`!x y z. x treal_eq y /\ y treal_eq z ==> x treal_eq z`,
REWRITE_TAC[FORALL_PAIR_THM; treal_eq] THEN REPEAT GEN_TAC THEN
DISCH_THEN(MP_TAC o MK_COMB o (AP_TERM `(+)` F_F I) o CONJ_PAIR) THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [HREAL_ADD_SYM] THEN
REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_EQ_ADD_LCANCEL] THEN
REWRITE_TAC[HREAL_ADD_ASSOC; HREAL_EQ_ADD_RCANCEL] THEN
DISCH_THEN(MATCH_ACCEPT_TAC o ONCE_REWRITE_RULE[HREAL_ADD_SYM]));;
(* ------------------------------------------------------------------------- *)
(* Useful to avoid unnecessary use of the equivalence relation. *)
(* ------------------------------------------------------------------------- *)
let TREAL_EQ_AP = prove
(`!x y. (x = y) ==> x treal_eq y`,
SIMP_TAC[TREAL_EQ_REFL]);;
(* ------------------------------------------------------------------------- *)
(* Commutativity properties for injector. *)
(* ------------------------------------------------------------------------- *)
let TREAL_OF_NUM_EQ = prove
(`!m n. (treal_of_num m treal_eq treal_of_num n) <=> (m = n)`,
REWRITE_TAC[treal_of_num; treal_eq; HREAL_OF_NUM_EQ; HREAL_ADD_RID]);;
let TREAL_OF_NUM_LE = prove
(`!m n. (treal_of_num m treal_le treal_of_num n) <=> m <= n`,
REWRITE_TAC[treal_of_num; treal_le; HREAL_OF_NUM_LE; HREAL_ADD_RID]);;
let TREAL_OF_NUM_ADD = prove
(`!m n. (treal_of_num m treal_add treal_of_num n) treal_eq
(treal_of_num(m + n))`,
REWRITE_TAC[treal_of_num; treal_eq; treal_add;
HREAL_OF_NUM_ADD; HREAL_ADD_RID; ADD_CLAUSES]);;
let TREAL_OF_NUM_MUL = prove
(`!m n. (treal_of_num m treal_mul treal_of_num n) treal_eq
(treal_of_num(m * n))`,
REWRITE_TAC[treal_of_num; treal_eq; treal_mul;
HREAL_OF_NUM_MUL; HREAL_MUL_RZERO; HREAL_MUL_LZERO; HREAL_ADD_RID;
HREAL_ADD_LID; HREAL_ADD_RID; MULT_CLAUSES]);;
(* ------------------------------------------------------------------------- *)
(* Strong forms of equality are useful to simplify welldefinedness proofs. *)
(* ------------------------------------------------------------------------- *)
let TREAL_ADD_SYM_EQ = prove
(`!x y. x treal_add y = y treal_add x`,
REWRITE_TAC[FORALL_PAIR_THM; treal_add; PAIR_EQ; HREAL_ADD_SYM]);;
let TREAL_MUL_SYM_EQ = prove
(`!x y. x treal_mul y = y treal_mul x`,
REWRITE_TAC[FORALL_PAIR_THM; treal_mul; HREAL_MUL_SYM; HREAL_ADD_SYM]);;
(* ------------------------------------------------------------------------- *)
(* Prove the properties of operations on representatives. *)
(* ------------------------------------------------------------------------- *)
let TREAL_ADD_SYM = prove
(`!x y. (x treal_add y) treal_eq (y treal_add x)`,
REPEAT GEN_TAC THEN MATCH_MP_TAC TREAL_EQ_AP THEN
MATCH_ACCEPT_TAC TREAL_ADD_SYM_EQ);;
let TREAL_ADD_ASSOC = prove
(`!x y z. (x treal_add (y treal_add z)) treal_eq
((x treal_add y) treal_add z)`,
SIMP_TAC[FORALL_PAIR_THM; TREAL_EQ_AP; treal_add; HREAL_ADD_ASSOC]);;
let TREAL_ADD_LID = prove
(`!x. ((treal_of_num 0) treal_add x) treal_eq x`,
REWRITE_TAC[FORALL_PAIR_THM; treal_of_num; treal_add; treal_eq;
HREAL_ADD_LID]);;
let TREAL_ADD_LINV = prove
(`!x. ((treal_neg x) treal_add x) treal_eq (treal_of_num 0)`,
REWRITE_TAC[FORALL_PAIR_THM; treal_neg; treal_add; treal_eq; treal_of_num;
HREAL_ADD_LID; HREAL_ADD_RID; HREAL_ADD_SYM]);;
let TREAL_MUL_SYM = prove
(`!x y. (x treal_mul y) treal_eq (y treal_mul x)`,
SIMP_TAC[TREAL_EQ_AP; TREAL_MUL_SYM_EQ]);;
let TREAL_MUL_ASSOC = prove
(`!x y z. (x treal_mul (y treal_mul z)) treal_eq
((x treal_mul y) treal_mul z)`,
SIMP_TAC[FORALL_PAIR_THM; TREAL_EQ_AP; treal_mul; HREAL_ADD_LDISTRIB;
HREAL_ADD_RDISTRIB; GSYM HREAL_MUL_ASSOC; HREAL_ADD_AC]);;
let TREAL_MUL_LID = prove
(`!x. ((treal_of_num 1) treal_mul x) treal_eq x`,
SIMP_TAC[FORALL_PAIR_THM; treal_of_num; treal_mul; treal_eq] THEN
REWRITE_TAC[HREAL_MUL_LZERO; HREAL_MUL_LID; HREAL_ADD_LID; HREAL_ADD_RID]);;
let TREAL_ADD_LDISTRIB = prove
(`!x y z. (x treal_mul (y treal_add z)) treal_eq
((x treal_mul y) treal_add (x treal_mul z))`,
SIMP_TAC[FORALL_PAIR_THM; TREAL_EQ_AP; treal_mul; treal_add;
HREAL_ADD_LDISTRIB; PAIR_EQ; HREAL_ADD_AC]);;
let TREAL_LE_REFL = prove
(`!x. x treal_le x`,
REWRITE_TAC[FORALL_PAIR_THM; treal_le; HREAL_LE_REFL]);;
let TREAL_LE_ANTISYM = prove
(`!x y. x treal_le y /\ y treal_le x <=> (x treal_eq y)`,
REWRITE_TAC[FORALL_PAIR_THM; treal_le; treal_eq; HREAL_LE_ANTISYM]);;
let TREAL_LE_TRANS = prove
(`!x y z. x treal_le y /\ y treal_le z ==> x treal_le z`,
REWRITE_TAC[FORALL_PAIR_THM; treal_le] THEN REPEAT GEN_TAC THEN
DISCH_THEN(MP_TAC o MATCH_MP HREAL_LE_ADD2) THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [HREAL_ADD_SYM] THEN
REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_LE_ADD_LCANCEL] THEN
REWRITE_TAC[HREAL_ADD_ASSOC; HREAL_LE_ADD_RCANCEL] THEN
DISCH_THEN(MATCH_ACCEPT_TAC o ONCE_REWRITE_RULE[HREAL_ADD_SYM]));;
let TREAL_LE_TOTAL = prove
(`!x y. x treal_le y \/ y treal_le x`,
REWRITE_TAC[FORALL_PAIR_THM; treal_le; HREAL_LE_TOTAL]);;
let TREAL_LE_LADD_IMP = prove
(`!x y z. (y treal_le z) ==> (x treal_add y) treal_le (x treal_add z)`,
REWRITE_TAC[FORALL_PAIR_THM; treal_le; treal_add] THEN
REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_LE_ADD_LCANCEL] THEN
ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN
REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_LE_ADD_LCANCEL]);;
let TREAL_LE_MUL = prove
(`!x y. (treal_of_num 0) treal_le x /\ (treal_of_num 0) treal_le y
==> (treal_of_num 0) treal_le (x treal_mul y)`,
REWRITE_TAC[FORALL_PAIR_THM; treal_of_num; treal_le; treal_mul] THEN
REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP HREAL_LE_EXISTS) THEN
REWRITE_TAC[HREAL_ADD_LDISTRIB; HREAL_LE_ADD_LCANCEL;
GSYM HREAL_ADD_ASSOC] THEN
GEN_REWRITE_TAC RAND_CONV [HREAL_ADD_SYM] THEN
ASM_REWRITE_TAC[HREAL_LE_ADD_LCANCEL] THEN
MATCH_MP_TAC HREAL_LE_MUL_RCANCEL_IMP THEN ASM_REWRITE_TAC[]);;
let TREAL_INV_0 = prove
(`treal_inv (treal_of_num 0) treal_eq (treal_of_num 0)`,
REWRITE_TAC[treal_inv; treal_eq; treal_of_num]);;
let TREAL_MUL_LINV = prove
(`!x. ~(x treal_eq treal_of_num 0) ==>
(treal_inv(x) treal_mul x) treal_eq (treal_of_num 1)`,
REWRITE_TAC[FORALL_PAIR_THM] THEN
MAP_EVERY X_GEN_TAC [`x:hreal`; `y:hreal`] THEN
PURE_REWRITE_TAC[treal_eq; treal_of_num; treal_mul; treal_inv] THEN
PURE_REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN DISCH_TAC THEN
PURE_ASM_REWRITE_TAC[COND_CLAUSES] THEN COND_CASES_TAC THEN
PURE_REWRITE_TAC[treal_mul; treal_eq] THEN
REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID;
HREAL_MUL_LZERO; HREAL_MUL_RZERO] THENL
[ALL_TAC;
DISJ_CASES_THEN MP_TAC(SPECL [`x:hreal`; `y:hreal`] HREAL_LE_TOTAL) THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC] THEN
FIRST_ASSUM(MP_TAC o MATCH_MP HREAL_LE_EXISTS) THEN
DISCH_THEN(MP_TAC o SELECT_RULE) THEN
DISCH_THEN(fun th -> ASSUME_TAC (SYM th) THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [th]) THEN
REWRITE_TAC[HREAL_ADD_LDISTRIB] THEN
GEN_REWRITE_TAC RAND_CONV [HREAL_ADD_SYM] THEN
AP_TERM_TAC THEN MATCH_MP_TAC HREAL_MUL_LINV THEN
DISCH_THEN SUBST_ALL_TAC THEN
FIRST_ASSUM(UNDISCH_TAC o check is_eq o concl) THEN
ASM_REWRITE_TAC[HREAL_ADD_RID] THEN
PURE_ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Show that the operations respect the equivalence relation. *)
(* ------------------------------------------------------------------------- *)
let TREAL_OF_NUM_WELLDEF = prove
(`!m n. (m = n) ==> (treal_of_num m) treal_eq (treal_of_num n)`,
REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
MATCH_ACCEPT_TAC TREAL_EQ_REFL);;
let TREAL_NEG_WELLDEF = prove
(`!x1 x2. x1 treal_eq x2 ==> (treal_neg x1) treal_eq (treal_neg x2)`,
REWRITE_TAC[FORALL_PAIR_THM; treal_neg; treal_eq] THEN REPEAT STRIP_TAC THEN
ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN ASM_REWRITE_TAC[]);;
let TREAL_ADD_WELLDEFR = prove
(`!x1 x2 y. x1 treal_eq x2 ==> (x1 treal_add y) treal_eq (x2 treal_add y)`,
REWRITE_TAC[FORALL_PAIR_THM; treal_add; treal_eq] THEN
REWRITE_TAC[HREAL_EQ_ADD_RCANCEL; HREAL_ADD_ASSOC] THEN
ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN
REWRITE_TAC[HREAL_EQ_ADD_RCANCEL; HREAL_ADD_ASSOC]);;
let TREAL_ADD_WELLDEF = prove
(`!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
(x1 treal_add y1) treal_eq (x2 treal_add y2)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
MATCH_MP_TAC TREAL_EQ_TRANS THEN EXISTS_TAC `x1 treal_add y2` THEN
CONJ_TAC THENL [ONCE_REWRITE_TAC[TREAL_ADD_SYM_EQ]; ALL_TAC] THEN
MATCH_MP_TAC TREAL_ADD_WELLDEFR THEN ASM_REWRITE_TAC[]);;
let TREAL_MUL_WELLDEFR = prove
(`!x1 x2 y. x1 treal_eq x2 ==> (x1 treal_mul y) treal_eq (x2 treal_mul y)`,
REWRITE_TAC[FORALL_PAIR_THM; treal_mul; treal_eq] THEN REPEAT GEN_TAC THEN
ONCE_REWRITE_TAC[AC HREAL_ADD_AC
`(a + b) + (c + d) = (a + d) + (b + c)`] THEN
REWRITE_TAC[GSYM HREAL_ADD_RDISTRIB] THEN DISCH_TAC THEN
ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN POP_ASSUM SUBST1_TAC THEN REFL_TAC);;
let TREAL_MUL_WELLDEF = prove
(`!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
(x1 treal_mul y1) treal_eq (x2 treal_mul y2)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
MATCH_MP_TAC TREAL_EQ_TRANS THEN EXISTS_TAC `x1 treal_mul y2` THEN
CONJ_TAC THENL [ONCE_REWRITE_TAC[TREAL_MUL_SYM_EQ]; ALL_TAC] THEN
MATCH_MP_TAC TREAL_MUL_WELLDEFR THEN ASM_REWRITE_TAC[]);;
let TREAL_EQ_IMP_LE = prove
(`!x y. x treal_eq y ==> x treal_le y`,
SIMP_TAC[FORALL_PAIR_THM; treal_eq; treal_le; HREAL_LE_REFL]);;
let TREAL_LE_WELLDEF = prove
(`!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
(x1 treal_le y1 <=> x2 treal_le y2)`,
REPEAT (STRIP_TAC ORELSE EQ_TAC) THENL
[MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `y1:hreal#hreal` THEN
CONJ_TAC THENL
[MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `x1:hreal#hreal` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC TREAL_EQ_IMP_LE THEN
ONCE_REWRITE_TAC[TREAL_EQ_SYM];
MATCH_MP_TAC TREAL_EQ_IMP_LE];
MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `y2:hreal#hreal` THEN
CONJ_TAC THENL
[MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `x2:hreal#hreal` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC TREAL_EQ_IMP_LE;
MATCH_MP_TAC TREAL_EQ_IMP_LE THEN ONCE_REWRITE_TAC[TREAL_EQ_SYM]]] THEN
ASM_REWRITE_TAC[]);;
let TREAL_INV_WELLDEF = prove
(`!x y. x treal_eq y ==> (treal_inv x) treal_eq (treal_inv y)`,
let lemma = prove
(`(@d. x = x + d) = &0`,
MATCH_MP_TAC SELECT_UNIQUE THEN BETA_TAC THEN
GEN_TAC THEN GEN_REWRITE_TAC (funpow 2 LAND_CONV) [GSYM HREAL_ADD_RID] THEN
REWRITE_TAC[HREAL_EQ_ADD_LCANCEL] THEN
MATCH_ACCEPT_TAC EQ_SYM_EQ) in
REWRITE_TAC[FORALL_PAIR_THM] THEN
MAP_EVERY X_GEN_TAC [`x1:hreal`; `x2:hreal`; `y1:hreal`; `y2:hreal`] THEN
PURE_REWRITE_TAC[treal_eq; treal_inv] THEN
ASM_CASES_TAC `x1 :hreal = x2` THEN
ASM_CASES_TAC `y1 :hreal = y2` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[TREAL_EQ_REFL] THEN
DISCH_THEN(MP_TAC o GEN_REWRITE_RULE RAND_CONV [HREAL_ADD_SYM]) THEN
REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; HREAL_EQ_ADD_RCANCEL] THEN DISCH_TAC THEN
ASM_REWRITE_TAC[HREAL_LE_REFL; lemma; HREAL_INV_0;TREAL_EQ_REFL] THEN
ASM_CASES_TAC `x2 <= x1` THEN ASM_REWRITE_TAC[] THENL
[FIRST_ASSUM(ASSUME_TAC o SYM o SELECT_RULE o MATCH_MP HREAL_LE_EXISTS) THEN
UNDISCH_TAC `x1 + y2 = x2 + y1` THEN
FIRST_ASSUM(SUBST1_TAC o SYM) THEN
REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; GSYM HREAL_ADD_ASSOC] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN
REWRITE_TAC[ONCE_REWRITE_RULE[HREAL_ADD_SYM] HREAL_LE_ADD] THEN
GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV o BINDER_CONV o
LAND_CONV) [HREAL_ADD_SYM] THEN
REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; TREAL_EQ_REFL];
DISJ_CASES_THEN MP_TAC
(SPECL [`x1:hreal`; `x2:hreal`] HREAL_LE_TOTAL) THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
FIRST_ASSUM(ASSUME_TAC o SYM o SELECT_RULE o MATCH_MP HREAL_LE_EXISTS) THEN
UNDISCH_TAC `x1 + y2 = x2 + y1` THEN
FIRST_ASSUM(SUBST1_TAC o SYM) THEN
REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; GSYM HREAL_ADD_ASSOC] THEN
DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[ONCE_REWRITE_RULE[HREAL_ADD_SYM] HREAL_LE_ADD] THEN
COND_CASES_TAC THENL
[UNDISCH_TAC `(@d. x2 = x1 + d) + y1 <= y1:hreal` THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM HREAL_ADD_LID] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[HREAL_ADD_SYM] HREAL_LE_ADD_LCANCEL] THEN
DISCH_TAC THEN SUBGOAL_THEN `(@d. x2 = x1 + d) = &0` MP_TAC THENL
[ASM_REWRITE_TAC[GSYM HREAL_LE_ANTISYM] THEN
GEN_REWRITE_TAC RAND_CONV [GSYM HREAL_ADD_LID] THEN
REWRITE_TAC[HREAL_LE_ADD];
DISCH_THEN SUBST_ALL_TAC THEN
UNDISCH_TAC `x1 + &0 = x2` THEN
ASM_REWRITE_TAC[HREAL_ADD_RID]];
GEN_REWRITE_TAC (funpow 3 RAND_CONV o BINDER_CONV o LAND_CONV)
[HREAL_ADD_SYM] THEN
REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; TREAL_EQ_REFL]]]);;
(* ------------------------------------------------------------------------- *)
(* Now define the quotient type -- the reals at last! *)
(* ------------------------------------------------------------------------- *)
let real_tybij =
define_quotient_type "real" ("mk_real","dest_real") `(treal_eq)`;;
let real_of_num,real_of_num_th =
lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
"real_of_num" TREAL_OF_NUM_WELLDEF;;
let real_neg,real_neg_th =
lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
"real_neg" TREAL_NEG_WELLDEF;;
let real_add,real_add_th =
lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
"real_add" TREAL_ADD_WELLDEF;;
let real_mul,real_mul_th =
lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
"real_mul" TREAL_MUL_WELLDEF;;
let real_le,real_le_th =
lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
"real_le" TREAL_LE_WELLDEF;;
let real_inv,real_inv_th =
lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
"real_inv" TREAL_INV_WELLDEF;;
let [REAL_ADD_SYM; REAL_ADD_ASSOC; REAL_ADD_LID; REAL_ADD_LINV;
REAL_MUL_SYM; REAL_MUL_ASSOC; REAL_MUL_LID;
REAL_ADD_LDISTRIB;
REAL_LE_REFL; REAL_LE_ANTISYM; REAL_LE_TRANS; REAL_LE_TOTAL;
REAL_LE_LADD_IMP; REAL_LE_MUL;
REAL_INV_0; REAL_MUL_LINV;
REAL_OF_NUM_EQ; REAL_OF_NUM_LE; REAL_OF_NUM_ADD; REAL_OF_NUM_MUL] =
map
(lift_theorem real_tybij (TREAL_EQ_REFL,TREAL_EQ_SYM,TREAL_EQ_TRANS)
[real_of_num_th; real_neg_th; real_add_th;
real_mul_th; real_le_th; real_inv_th])
[TREAL_ADD_SYM; TREAL_ADD_ASSOC; TREAL_ADD_LID; TREAL_ADD_LINV;
TREAL_MUL_SYM; TREAL_MUL_ASSOC; TREAL_MUL_LID;
TREAL_ADD_LDISTRIB;
TREAL_LE_REFL; TREAL_LE_ANTISYM; TREAL_LE_TRANS; TREAL_LE_TOTAL;
TREAL_LE_LADD_IMP; TREAL_LE_MUL;
TREAL_INV_0; TREAL_MUL_LINV;
TREAL_OF_NUM_EQ; TREAL_OF_NUM_LE; TREAL_OF_NUM_ADD; TREAL_OF_NUM_MUL];;
(* ------------------------------------------------------------------------- *)
(* Set up a friendly interface. *)
(* ------------------------------------------------------------------------- *)
parse_as_prefix "--";;
parse_as_infix ("/",(22,"left"));;
parse_as_infix ("pow",(24,"left"));;
do_list overload_interface
["+",`real_add:real->real->real`; "-",`real_sub:real->real->real`;
"*",`real_mul:real->real->real`; "/",`real_div:real->real->real`;
"<",`real_lt:real->real->bool`; "<=",`real_le:real->real->bool`;
">",`real_gt:real->real->bool`; ">=",`real_ge:real->real->bool`;
"--",`real_neg:real->real`; "pow",`real_pow:real->num->real`;
"inv",`real_inv:real->real`; "abs",`real_abs:real->real`;
"max",`real_max:real->real->real`; "min",`real_min:real->real->real`;
"&",`real_of_num:num->real`];;
let prioritize_real() = prioritize_overload(mk_type("real",[]));;
(* ------------------------------------------------------------------------- *)
(* Additional definitions. *)
(* ------------------------------------------------------------------------- *)
let real_sub = new_definition
`x - y = x + --y`;;
let real_lt = new_definition
`x < y <=> ~(y <= x)`;;
let real_ge = new_definition
`x >= y <=> y <= x`;;
let real_gt = new_definition
`x > y <=> y < x`;;
let real_abs = new_definition
`abs(x) = if &0 <= x then x else --x`;;
let real_pow = new_recursive_definition num_RECURSION
`(x pow 0 = &1) /\
(!n. x pow (SUC n) = x * (x pow n))`;;
let real_div = new_definition
`x / y = x * inv(y)`;;
let real_max = new_definition
`real_max m n = if m <= n then n else m`;;
let real_min = new_definition
`real_min m n = if m <= n then m else n`;;
(*----------------------------------------------------------------------------*)
(* Derive the supremum property for an arbitrary bounded nonempty set *)
(*----------------------------------------------------------------------------*)
let REAL_HREAL_LEMMA1 = prove
(`?r:hreal->real.
(!x. &0 <= x <=> ?y. x = r y) /\
(!y z. y <= z <=> r y <= r z)`,
EXISTS_TAC `\y. mk_real((treal_eq)(y,hreal_of_num 0))` THEN
REWRITE_TAC[GSYM real_le_th] THEN
REWRITE_TAC[treal_le; HREAL_ADD_LID; HREAL_ADD_RID] THEN
GEN_TAC THEN EQ_TAC THENL
[MP_TAC(INST [`dest_real x`,`r:hreal#hreal->bool`] (snd real_tybij)) THEN
REWRITE_TAC[fst real_tybij] THEN
DISCH_THEN(X_CHOOSE_THEN `p:hreal#hreal` MP_TAC) THEN
DISCH_THEN(MP_TAC o AP_TERM `mk_real`) THEN
REWRITE_TAC[fst real_tybij] THEN DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[GSYM real_of_num_th; GSYM real_le_th] THEN
SUBST1_TAC(GSYM(ISPEC `p:hreal#hreal` PAIR)) THEN
PURE_REWRITE_TAC[treal_of_num; treal_le] THEN
PURE_REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN
DISCH_THEN(X_CHOOSE_THEN `d:hreal` SUBST1_TAC o
MATCH_MP HREAL_LE_EXISTS) THEN
EXISTS_TAC `d:hreal` THEN AP_TERM_TAC THEN
ONCE_REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `q:hreal#hreal` THEN
SUBST1_TAC(GSYM(ISPEC `q:hreal#hreal` PAIR)) THEN
PURE_REWRITE_TAC[treal_eq] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [HREAL_ADD_SYM] THEN
REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_EQ_ADD_LCANCEL] THEN
REWRITE_TAC[HREAL_ADD_RID];
DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
REWRITE_TAC[GSYM real_of_num_th; GSYM real_le_th] THEN
REWRITE_TAC[treal_of_num; treal_le] THEN
REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN
GEN_REWRITE_TAC RAND_CONV [GSYM HREAL_ADD_LID] THEN
REWRITE_TAC[HREAL_LE_ADD]]);;
let REAL_HREAL_LEMMA2 = prove
(`?h r. (!x:hreal. h(r x) = x) /\
(!x. &0 <= x ==> (r(h x) = x)) /\
(!x:hreal. &0 <= r x) /\
(!x y. x <= y <=> r x <= r y)`,
STRIP_ASSUME_TAC REAL_HREAL_LEMMA1 THEN
EXISTS_TAC `\x:real. @y:hreal. x = r y` THEN
EXISTS_TAC `r:hreal->real` THEN
ASM_REWRITE_TAC[BETA_THM] THEN
SUBGOAL_THEN `!y z. ((r:hreal->real) y = r z) <=> (y = z)` ASSUME_TAC THENL
[ASM_REWRITE_TAC[GSYM REAL_LE_ANTISYM; GSYM HREAL_LE_ANTISYM]; ALL_TAC] THEN
ASM_REWRITE_TAC[GEN_REWRITE_RULE (LAND_CONV o BINDER_CONV) [EQ_SYM_EQ]
(SPEC_ALL SELECT_REFL); GSYM EXISTS_REFL] THEN
GEN_TAC THEN DISCH_THEN(ACCEPT_TAC o SYM o SELECT_RULE));;
let REAL_COMPLETE_SOMEPOS = prove
(`!P. (?x. P x /\ &0 <= x) /\
(?M. !x. P x ==> x <= M)
==> ?M. (!x. P x ==> x <= M) /\
!M'. (!x. P x ==> x <= M') ==> M <= M'`,
REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC REAL_HREAL_LEMMA2 THEN
MP_TAC(SPEC `\y:hreal. (P:real->bool)(r y)` HREAL_COMPLETE) THEN
BETA_TAC THEN
W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL
[CONJ_TAC THENL
[EXISTS_TAC `(h:real->hreal) x` THEN
UNDISCH_TAC `(P:real->bool) x` THEN
MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN
AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
EXISTS_TAC `(h:real->hreal) M` THEN
X_GEN_TAC `y:hreal` THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN
AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN
ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN
ASM_REWRITE_TAC[]];
MATCH_MP_TAC(TAUT `(b ==> c) ==> a ==> (a ==> b) ==> c`) THEN
DISCH_THEN(X_CHOOSE_THEN `B:hreal` STRIP_ASSUME_TAC)] THEN
EXISTS_TAC `(r:hreal->real) B` THEN CONJ_TAC THENL
[X_GEN_TAC `z:real` THEN DISCH_TAC THEN
DISJ_CASES_TAC(SPECL [`&0`; `z:real`] REAL_LE_TOTAL) THENL
[ANTE_RES_THEN(SUBST1_TAC o SYM) (ASSUME `&0 <= z`) THEN
FIRST_ASSUM(fun th -> GEN_REWRITE_TAC I [GSYM th]) THEN
FIRST_ASSUM MATCH_MP_TAC THEN
UNDISCH_TAC `(P:real->bool) z` THEN
MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN
AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
ASM_REWRITE_TAC[];
MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&0` THEN
ASM_REWRITE_TAC[]];
X_GEN_TAC `C:real` THEN DISCH_TAC THEN
SUBGOAL_THEN `B:hreal <= (h(C:real))` MP_TAC THENL
[FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `(r:hreal->real)(h C) = C` (fun th -> ASM_REWRITE_TAC[th]);
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC] THEN
FIRST_ASSUM MATCH_MP_TAC THEN
MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN
ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN
ASM_REWRITE_TAC[]]);;
let REAL_COMPLETE = prove
(`!P. (?x. P x) /\
(?M. !x. P x ==> x <= M)
==> ?M. (!x. P x ==> x <= M) /\
!M'. (!x. P x ==> x <= M') ==> M <= M'`,
let lemma = prove
(`y = (y - x) + x`,
REWRITE_TAC[real_sub; GSYM REAL_ADD_ASSOC; REAL_ADD_LINV] THEN
ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[REAL_ADD_LID]) in
REPEAT STRIP_TAC THEN
DISJ_CASES_TAC (SPECL [`&0`; `x:real`] REAL_LE_TOTAL) THENL
[MATCH_MP_TAC REAL_COMPLETE_SOMEPOS THEN CONJ_TAC THENL
[EXISTS_TAC `x:real`; EXISTS_TAC `M:real`] THEN
ASM_REWRITE_TAC[];
FIRST_ASSUM(MP_TAC o MATCH_MP REAL_LE_LADD_IMP) THEN
DISCH_THEN(MP_TAC o SPEC `--x`) THEN
REWRITE_TAC[REAL_ADD_LINV] THEN
ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[REAL_ADD_LID] THEN
DISCH_TAC THEN
MP_TAC(SPEC `\y. P(y + x) :bool` REAL_COMPLETE_SOMEPOS) THEN
BETA_TAC THEN
W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL
[CONJ_TAC THENL
[EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[REAL_LE_REFL; REAL_ADD_LID];
EXISTS_TAC `M + --x` THEN GEN_TAC THEN
DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
DISCH_THEN(MP_TAC o SPEC `--x` o MATCH_MP REAL_LE_LADD_IMP) THEN
DISCH_THEN(MP_TAC o ONCE_REWRITE_RULE[REAL_ADD_SYM]) THEN
REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LINV] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID]];
MATCH_MP_TAC(TAUT `(b ==> c) ==> a ==> (a ==> b) ==> c`) THEN
DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC)] THEN
EXISTS_TAC `B + x` THEN CONJ_TAC THENL
[GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [lemma] THEN
DISCH_THEN(ANTE_RES_THEN
(MP_TAC o SPEC `x:real` o MATCH_MP REAL_LE_LADD_IMP)) THEN
ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
REWRITE_TAC[real_sub; GSYM REAL_ADD_ASSOC; REAL_ADD_LINV] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID] THEN
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC THEN SUBGOAL_THEN `B <= M' - x` MP_TAC THENL
[FIRST_ASSUM MATCH_MP_TAC THEN X_GEN_TAC `z:real` THEN DISCH_TAC THEN
SUBGOAL_THEN `z + x <= M'` MP_TAC THENL
[FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
DISCH_THEN(MP_TAC o SPEC `--x` o MATCH_MP REAL_LE_LADD_IMP) THEN
ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
REWRITE_TAC[real_sub] THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
AP_TERM_TAC THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LINV] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID]];
DISCH_THEN(MP_TAC o SPEC `x:real` o MATCH_MP REAL_LE_LADD_IMP) THEN
MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THENL
[MATCH_ACCEPT_TAC REAL_ADD_SYM;
ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[real_sub] THEN
REWRITE_TAC[GSYM REAL_ADD_ASSOC; REAL_ADD_LINV] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID]]]]]);;
do_list reduce_interface
["+",`hreal_add:hreal->hreal->hreal`;
"*",`hreal_mul:hreal->hreal->hreal`;
"<=",`hreal_le:hreal->hreal->bool`;
"inv",`hreal_inv:hreal->hreal`];;
do_list remove_interface ["**"; "++"; "<<="; "==="; "fn"; "afn"];;