(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Chapter: Jordan *)
(* Copied from HOL Light jordan directory *)
(* Author: Thomas C. Hales *)
(* Date: 2010-07-08 *)
(* ========================================================================== *)
(*
A handheld calculator, implemented in HOL light.
It implements + - / * sqrt, ssqrt, abs, atn, acs, pi,
The user can supply additional conversons to extend the calculator to other functions.
There is an example file float_example.hl.
*)
(* based on float.ml in hol/jordan/float.ml *)
(*
To do. Allow the user to supply theorems that carry domain constraints,
(such as ACS_ATN).
*)
flyspeck_needs "jordan/taylor_atn.hl";;
module Float = struct
open Lib_ext;;
open Num_ext_nabs;;
open Real_ext;;
open Refinement;;
open Tactics_jordan;;
open Taylor_atn;;
Parse_ext_override_interface.unambiguous_interface();;
Parse_ext_override_interface.prioritize_real();;
(* Three types of error:
Insufficient precision: the inequality might be true but there is not enough
precision to decide. Divide by zero generally lands here, because there is
no testing for exact equality.
Internal failure: a bug in this code.
User input failure: sqrt of negative numbers, false inequalities.
*)
exception Insufficient_precision;;
(*
exception Mk_comb of (term*hol_type)*(term*hol_type);;
let mk_comb(a,b) = try mk_comb(a,b) with
Failure _ -> raise (Mk_comb((a,type_of a),(b,type_of b)));;
*)
let add_test,test = new_test_suite();;
(*--------------------------------------------------------------------*)
let mk_interval a b ex =
mk_comb(mk_comb (mk_comb (`interval_eps`,a),b),ex);;
add_test("mk_interval",
mk_interval `#3` `#4` `#1` = `interval_eps #3 #4 #1`);;
let dest_interval intv =
let (h1,ex) = dest_comb intv in
let (h2,f) = dest_comb h1 in
let (h3,a) = dest_comb h2 in
let _ = (h3 = `interval_eps`) or (print_term h3; failwith "dest_interval:interval_eps") in
(a,f,ex);;
let _ = add_test("dest_interval",
let a = `#3` and b = `#4` and c = `#1` in
dest_interval (mk_interval a b c) = (a,b,c));;
(*--------------------------------------------------------------------*)
let (dest_int:term-> Num.num) =
fun b ->
let dest_pos_int a =
let (op,nat) = dest_comb a in
if (fst (dest_const op) = "int_of_num") then (dest_numeral nat)
else fail() in
let (op',u) = (dest_comb b) in
try (if (fst (dest_const op') = "int_neg") then
minus_num (dest_pos_int u) else
dest_pos_int b) with
Failure _ -> failwith "dest_int ";;
let (mk_int:Num.num -> term) =
fun a ->
let sgn = Num.sign_num a in
let abv = Num.abs_num a in
let r = mk_comb(`int_of_num`,mk_numeral abv) in
try (if (sgn<0) then mk_comb (`int_neg`,r) else r) with
Failure _ -> failwith ("dest_int "^(string_of_num a));;
add_test("mk_int",
(mk_int (Int (-1443)) = `int_neg (int_of_num 1443)`) &&
(mk_int (Int 37) = `(int_of_num 37)`));;
(* ------------------------------------------------------------------ *)
let (split_ratio:Num.num -> Num.num*Num.num) =
function
(Ratio r) -> (Big_int (Ratio.numerator_ratio r)),
(Big_int (Ratio.denominator_ratio r))|
u -> (u,(Int 1));;
add_test("split_ratio",
let (a,b) = split_ratio ((Int 4)//(Int 20)) in
(a =/ (Int 1)) && (b =/ (Int 5)));;
(* ------------------------------------------------------------------ *)
(* break nonzero int r into a*(C**b) with a prime to C . *)
let (factor_C:int -> Num.num -> Num.num*Num.num) =
function c ->
let intC = (Int c) in
let rec divC (a,b) =
if ((Int 0) =/ mod_num a intC) then (divC (a//intC,b+/(Int 1)))
else (a,b) in
function r->
if ((Num.is_integer_num r)&& not((Num.sign_num r) = 0)) then
divC (r,(Int 0)) else failwith "factor_C";;
add_test("factor_C",
(factor_C 2 (Int (4096+32)) = (Int 129,Int 5)) &&
(factor_C 10 (Int (5000)) = (Int 5,Int 3)) &&
(cannot (factor_C 2) ((Int 50)//(Int 3))));;
(*--------------------------------------------------------------------*)
let (dest_float:term -> Num.num) =
fun f ->
let (a,b) = dest_binop `float` f in
(dest_int a)*/ ((Int 2) **/ (dest_int b));;
add_test("dest_float",
dest_float `float (int_of_num 3) (int_of_num 17)` = (Int 393216));;
add_test("dest_float2", (* must express as numeral first *)
cannot dest_float `float ((int_of_num 3)+:(int_of_num 1)) (int_of_num 17)`);;
(* ------------------------------------------------------------------ *)
(* creates float of the form `float a b` with a odd *)
let (mk_float:Num.num -> term) =
function r ->
let (a,b) = split_ratio r in
let (a',exp_a) = if (a=/(Int 0)) then ((Int 0),(Int 0)) else factor_C 2 a in
let (b',exp_b) = factor_C 2 b in
let c = a'//b' in
if (Num.is_integer_num c) then
mk_binop `float` (mk_int c) (mk_int (exp_a -/ exp_b))
else failwith "mk_float";;
add_test("mk_float",
mk_float (Int (4096+32)) = `float (int_of_num 129) (int_of_num 5)` &&
(mk_float (Int 0) = `float (int_of_num 0) (int_of_num 0)`));;
add_test("mk_float2", (* throws exception exactly when denom != 2^k *)
let rtest = fun t -> (t =/ dest_float (mk_float t)) in
rtest ((Int 3)//(Int 1024)) &&
(cannot rtest ((Int 1)//(Int 3))));;
add_test("mk_float dest_float", (* constructs canonical form of float *)
mk_float (dest_float `float (int_of_num 4) (int_of_num 3)`) = `float (int_of_num 1) (int_of_num 5)`);;
(* ------------------------------------------------------------------ *)
(* creates decimal of the form `DECIMAL a b` with a prime to 10 *)
let (mk_pos_decimal:Num.num -> term) =
let zero = `#0` in
function r ->
let _ = assert (r >=/ (Int 0)) in
let (a,b) = split_ratio r in
if (a=/(Int 0)) then zero else
let (a1,exp_a5) = factor_C 5 a in
let (a2,exp_a2) = factor_C 2 a1 in
let (b1,exp_b5) = factor_C 5 b in
let (b2,exp_b2) = factor_C 2 b1 in
let _ = assert(b2 =/ (Int 1)) in
let c = end_itlist Num.max_num [exp_b5-/exp_a5;exp_b2-/exp_a2;(Int 0)] in
let a' = a2*/((Int 2)**/ (c +/ exp_a2 -/ exp_b2))*/
((Int 5)**/(c +/ exp_a5 -/ exp_b5)) in
let b' = (Int 10) **/ c in
mk_binop `DECIMAL` (mk_numeral a') (mk_numeral b');;
add_test("mk_pos_decimal",
mk_pos_decimal (Int (5000)) = `#5000` &&
(mk_pos_decimal ((Int 30)//(Int 40)) = `#0.75`) &&
(mk_pos_decimal (Int 0) = `#0`) &&
(mk_pos_decimal ((Int 15)//(Int 25)) = `#0.6`) &&
(mk_pos_decimal ((Int 25)//(Int 4)) = `#6.25`) &&
(mk_pos_decimal ((Int 2)//(Int 25)) = `#0.08`));;
let (mk_decimal:Num.num->term) =
function r ->
let a = Num.sign_num r in
let b = mk_pos_decimal (Num.abs_num r) in
if (a < 0) then (mk_comb (`real_neg`, b)) else b;;
add_test("mk_decimal",
(mk_decimal (Int 3) = `#3`) &&
(mk_decimal (Int (-3)) = `real_neg (#3)`));;
(*--------------------------------------------------------------------*)
let (dest_decimal:term -> Num.num) =
fun f ->
let (a,b) = dest_binop `DECIMAL` f in
let a1 = dest_numeral a in
let b1 = dest_numeral b in
a1//b1;;
add_test("dest_decimal",
dest_decimal `#3.4` =/ ((Int 34)//(Int 10)));;
add_test("dest_decimal2",
cannot dest_decimal `real_neg (#3.4)`);;
(*--------------------------------------------------------------------*)
(* Properties of integer powers of 2. *)
(* ------------------------------------------------------------------ *)
let TWOPOW_POS = prove(`!n. (
twopow (
int_of_num n) = (&2) pow n)`,
(REWRITE_TAC[
twopow])
THEN GEN_TAC
THEN COND_CASES_TAC
THENL [AP_TERM_TAC;ALL_TAC]
THEN (REWRITE_TAC[
NABS_POS])
THEN (UNDISCH_EL_TAC 0)
THEN (TAUT_TAC (` ( A ) ==> (~ A ==> B)`))
THEN (MESON_TAC[]));;
let TWOPOW_NEG = prove(`!n. (
twopow (--(
int_of_num n)) = inv((&2) pow n))`,
GEN_TAC
THEN (REWRITE_TAC[
twopow])
THEN (COND_CASES_TAC THENL [ALL_TAC;REWRITE_TAC[
NABS_NEG]])
THEN (POP_ASSUM CHOOSE_TAC)
THEN (REWRITE_TAC[
NABS_NEG])
THEN (UNDISCH_EL_TAC 0)
THEN (REWRITE_TAC[
int_eq;
int_neg_th;
INT_NUM_REAL])
THEN (REWRITE_TAC[prove (`! u y.((--(real_of_num u) = (real_of_num y))=
((real_of_num u) +(real_of_num y) = (&0)))`,REAL_ARITH_TAC)])
THEN (REWRITE_TAC[REAL_OF_NUM_ADD;REAL_OF_NUM_EQ;
ADD_EQ_0])
THEN (DISCH_TAC)
THEN (ASM_REWRITE_TAC[
real_pow;
REAL_INV_1]));;
let INT_REP3 = prove(`!a .(?n.( (a =
int_of_num n) \/ (a = --: (
int_of_num (n+1)))))`,
(GEN_TAC)
THEN ((ASSUME_TAC (SPEC `a:int`
INT_REP2)))
THEN ((POP_ASSUM CHOOSE_TAC))
THEN ((DISJ_CASES_TAC (prove (`((a:int) = (
int_of_num 0)) \/ ~((a:int) =(
int_of_num 0))`, MESON_TAC[]))))
(* cases *)
THENL[ ((EXISTS_TAC `0`)) THEN ((ASM_REWRITE_TAC[]));ALL_TAC]
THEN ((UNDISCH_EL_TAC 0))
THEN ((POP_ASSUM DISJ_CASES_TAC))
THENL [DISCH_TAC THEN ((ASM MESON_TAC)[]);ALL_TAC]
THEN (DISCH_TAC)
THEN ((EXISTS_TAC `
PRE n`))
THEN ((DISJ2_TAC))
THEN ((ASM_REWRITE_TAC[
INT_EQ_NEG2]))
(*** Changed by JRH, 2006/03/28 to avoid PRE_ELIM_TAC ***)
THEN (FIRST_X_ASSUM(MP_TAC o check(is_neg o concl)))
THEN (ASM_REWRITE_TAC[
INT_NEG_EQ_0;
INT_OF_NUM_EQ])
THEN (ARITH_TAC));;
let REAL_EQ_INV = prove(`!x y. ((x:real = y) <=> (inv(x) = inv (y)))`,
((REPEAT GEN_TAC))
THEN (EQ_TAC)
THENL [((DISCH_TAC THEN (ASM_REWRITE_TAC[])));
(* branch 2*) ((DISCH_TAC))
THEN ((ONCE_REWRITE_TAC [(GSYM
REAL_INV_INV)]))
THEN ((ASM_REWRITE_TAC[]))]);;
let POW_2 = prove(
`!x. x pow 2 = x * x`,
GEN_TAC THEN REWRITE_TAC[num_CONV `2`] THEN
REWRITE_TAC[pow;
POW_1]);;
let REAL_ADD_LE_SUBST_RHS = prove(
`!a b c P. ((a <=. ((P b)) /\ (!x. (P x) = x + (P (&. 0))) /\ (b <=. c)) ==> (a <=. (P c)))`,
(((REPEAT GEN_TAC)))
THEN (((REPEAT (TAUT_TAC `(b ==> a==> c) ==> (a /\ b ==> c)`))))
THEN (((REPEAT DISCH_TAC)))
THEN ((((H_RULER(ONCE_REWRITE_RULE))[HYP_INT 1] (HYP_INT 0))))
THEN ((((ASM ONCE_REWRITE_TAC)[])))
THEN ((((ASM MESON_TAC)[
REAL_LE_RADD;
REAL_LE_TRANS]))));;
let REAL_ADD_LE_SUBST_LHS = prove(
`!a b c P. (((P(a) <=. b /\ (!x. (P x) = x + (P (&. 0))) /\ (c <=. a)))
==> ((P c) <=. b))`,
(REP_GEN_TAC)
THEN (DISCH_ALL_TAC)
THEN (((H_RULER(ONCE_REWRITE_RULE)) [HYP_INT 1] (HYP_INT 0)))
THEN (((ASM ONCE_REWRITE_TAC)[]))
THEN (((ASM MESON_TAC)[
REAL_LE_RADD;
REAL_LE_TRANS])));;
let INTERVAL_ADD = prove(
`!x f ex y g ey.
interval_eps x f ex /\
interval_eps y g ey ==>
interval_eps (x +. y) (f +. g) (ex +. ey)`,
EVERY[
REPEAT GEN_TAC;
TAUT_TAC `(A==>B==>C)==>(A/\ B ==> C)`;
REWRITE_TAC[
interval_eps];
REWRITE_TAC[prove(`(x+.y) -. (f+.g) = (x-.f) +. (y-.g)`,REAL_ARITH_TAC)];
ABBREV_TAC `a = x-.f`;
ABBREV_TAC `b = y-.g`;
ASSUME_TAC (SPEC `b:real` (SPEC `a:real`
ABS_TRIANGLE));
UNDISCH_EL_TAC 0;
ABBREV_TAC `a':real = abs a`;
ABBREV_TAC `b':real = abs b`;
REPEAT DISCH_TAC;
(H_VAL2(IWRITE_REAL_LE_RHS)) (HYP_INT 0) (HYP_INT 2);
(H_VAL2(IWRITE_REAL_LE_RHS)) (HYP_INT 2) (HYP_INT 0);
ASM_REWRITE_TAC[]]);;
let REAL_LE_ABS_MUL = prove(
`!x y z w. (( x <=. y) /\ (abs z <=. w)) ==> (x*.w <=. y*.w) `,
(DISCH_ALL_TAC)
THEN ((ASSUME_TAC (REAL_ARITH `abs z <=. w ==> (&.0) <=. w`)))
THEN (((ASM MESON_TAC)[
REAL_LE_RMUL_IMP])));;
let INTERVAL_MUL = prove(
`!x f ex y g ey. (
interval_eps x f ex) /\ (
interval_eps y g ey) ==>
(
interval_eps (x *. y) (f *. g) (abs(f)*.ey +. ex*. abs(g) +. ex*.ey))`,
(REP_GEN_TAC)
THEN ((REWRITE_TAC[
interval_eps]))
THEN ((REWRITE_TAC[REAL_ARITH `(x*. y -. f*. g) = (f *.(y -. g) +. (x -. f)*.g +. (x-.f)*.(y-. g))`]))
THEN (DISCH_ALL_TAC)
THEN ((ASSUME_TAC (SPECL [`f*.(y-g)`;`(x-f)*g +. (x-f)*.(y-g)`]
ABS_TRIANGLE)))
THEN ((ASSUME_TAC (SPECL [`(x-f)*.g`;`(x-f)*.(y-g)`]
ABS_TRIANGLE)))
THEN (((H_VAL2(IWRITE_REAL_LE_RHS)) (HYP_INT 0) (HYP_INT 1)))
THEN ((H_REWRITE_RULE [THM
ABS_MUL] (HYP_INT 0)))
THEN ((H_MATCH_MP (THM (SPECL [`g:real`; `abs (x -. f)`; `ex:real`]
REAL_PROP_LE_RABS)) (HYP_INT 4)))
THEN (((H_VAL2(IWRITE_REAL_LE_RHS)) (HYP_INT 0) (HYP_INT 1)))
THEN ((H_MATCH_MP (THM (SPECL [`f:real`; `abs (y -. g)`; `ey:real`]
REAL_PROP_LE_LABS)) (HYP_INT 7)))
THEN (((H_VAL2 (IWRITE_REAL_LE_RHS)) (HYP_INT 0) (HYP_INT 1)))
THEN ((H_MATCH_MP (THM (SPECL [`x-.f`; `abs (y -. g)`; `ey:real`]
REAL_PROP_LE_LABS)) (HYP_INT 9)))
THEN (((H_VAL2(IWRITE_REAL_LE_RHS)) (HYP_INT 0) (HYP_INT 1)))
THEN ((ASSUME_TAC (SPECL [`abs(x-.f)`;`ex:real`;`y-.g`;`ey:real`]
REAL_LE_ABS_MUL)))
THEN ((H_CONJ (HYP_INT 11) (HYP_INT 12)))
THEN ((H_MATCH_MP (HYP_INT 1) (HYP_INT 0)))
THEN (((H_VAL2(IWRITE_REAL_LE_RHS)) (HYP_INT 0) (HYP_INT 3)))
THEN ((POP_ASSUM ACCEPT_TAC)));;
let INTERVAL_CENTER = prove(
`!x f ex g. (
interval_eps x f ex) ==> (
interval_eps x g (abs(f-g)+.ex))`,
((REWRITE_TAC[
interval_eps]))
THEN (DISCH_ALL_TAC)
THEN ((ASSUME_TAC (REAL_ARITH `abs(x -. g) <=. abs(f-.g) +. abs(x -. f)`)))
THEN ((H_VAL2 IWRITE_REAL_LE_RHS (HYP_INT 1) (HYP_INT 0)))
THEN ((ASM_REWRITE_TAC[])));;
let INTERVAL_DIV = prove(`!x f ex y g ey h ez.
(((
interval_eps x f ex) /\ (
interval_eps y g ey) /\ (ey <. (abs g)) /\
((ex +. (abs (f -. (h*.g))) +. (abs h)*. ey) <=. (ez*.((abs g) -. ey))))
==> (
interval_eps (x / y) h ez))`,
let lemma1 = prove( `&.0 < u /\ real_abs z <=. e*. u ==> (&.0) <=. e`,
EVERY[
DISCH_ALL_TAC;
ASSUME_TAC (SPEC `z:real` REAL_MK_NN_ABS);
H_MATCH_MP (THM REAL_LE_TRANS) (H_RULE2 CONJ (HYP_INT 0) (HYP_INT 2));
H_MATCH_MP (THM REAL_PROP_NN_RCANCEL) (H_RULE2 CONJ (HYP_INT 2) (HYP_INT 0));
ASM_REWRITE_TAC[]
]) in
EVERY[
DISCH_ALL_TAC;
SUBGOAL_MP_TAC `~(y= (&.0))`
THENL[
EVERY[
UNDISCH_LIST[1;2];
REWRITE_TAC[interval_eps];
REAL_ARITH_TAC
];
EVERY[
REWRITE_TAC[interval_eps];
DISCH_TAC THEN (H I (HYP_INT 0)) THEN (UNDISCH_EL_TAC 0);
DISCH_THEN (fun th -> (MP_TAC(MATCH_MP REAL_MK_POS_ABS_' th)));
MATCH_MP_TAC REAL_MUL_RTIMES_LE;
REWRITE_TAC[GSYM ABS_MUL;REAL_SUB_RDISTRIB;real_div;GSYM REAL_MUL_ASSOC];
ASM_SIMP_TAC[REAL_MUL_LINV;REAL_MUL_RID];
H (REWRITE_RULE[interval_eps]) (HYP_INT 1);
H (REWRITE_RULE[interval_eps]) (HYP_INT 3);
H (MATCH_MP INTERVAL_ABS_MIN) (HYP_INT 4);
POPL_TAC[3;4;5];
H_VAL2 (IWRITE_REAL_LE_LHS) (HYP_INT 2) (HYP_INT 4);
H (REWRITE_RULE[ REAL_ADD_ASSOC]) (HYP_INT 0);
H_VAL2 (IWRITE_REAL_LE_LHS) (THM (SPEC `f-. h*g` (SPEC `x-.f` ABS_TRIANGLE))) (HYP_INT 0);
H (ONCE_REWRITE_RULE[REAL_ABS_SUB]) (HYP_INT 4);
H (MATCH_MP (SPEC `h:real` REAL_PROP_LE_LABS)) (HYP_INT 0);
H (REWRITE_RULE[GSYM ABS_MUL]) (HYP_INT 0);
H_VAL2 (IWRITE_REAL_LE_LHS) (HYP_INT 0) (HYP_INT 3);
H_VAL2 (IWRITE_REAL_LE_LHS) (THM (SPEC `h*.(g-.y)` (SPEC`(x-.f)+(f-. h*g)` ABS_TRIANGLE))) (HYP_INT 0);
POPL_TAC[1;2;3;4;5;6;7;9;10;12];
H (ONCE_REWRITE_RULE[REAL_ARITH `((x-.f) +. (f -. h*. g)) +. h*.(g-. y) = x -. h*. y `]) (HYP_INT 0);
ABBREV_TAC `z = x -. h*.y`;
H (ONCE_REWRITE_RULE[GSYM REAL_SUB_LT]) (HYP_INT 4);
ABBREV_TAC `u = abs(g) -. ey`;
POPL_TAC[0;2;4;6];
H (MATCH_MP lemma1 ) (H_RULE2 CONJ (HYP_INT 0) (HYP_INT 1));
H (MATCH_MP REAL_PROP_LE_LMUL) (H_RULE2 CONJ (HYP_INT 0) (HYP_INT 3));
H (MATCH_MP REAL_LE_TRANS) (H_RULE2 CONJ (HYP_INT 3) (HYP_INT 0));
ASM_REWRITE_TAC[]
];
]]);;
let REAL_SSQRT_NEG = prove(`!x. (x <. (&.0)) ==> (
ssqrt x = (&.0))`,
EVERY[
DISCH_ALL_TAC;
REWRITE_TAC[
ssqrt];
COND_CASES_TAC
THENL[
ACCEPT_TAC (REFL `&.0`);
ASM_MESON_TAC[]
]
]);;
let INTERVAL_SSQRT = prove(`!x f ex u ey ez v. (
interval_eps x f ex) /\ (
interval_eps (u*.u) f ey) /\
(ex +.ey <=. ez*.(v+.u)) /\ (v*.v <=. f-.ex) /\ (&.0 <. u) /\ (&.0 <=. v) ==>
(
interval_eps (
ssqrt x) u ez)`,
EVERY[
DISCH_ALL_TAC;
H (MATCH_MP
REAL_LE_TRANS) (H_RULE2 CONJ (THM (SPEC `v:real` REAL_MK_NN_SQUARE)) (HYP_INT 3));
H (MATCH_MP (
INTERVAL_MIN)) (HYP_INT 1);
H (MATCH_MP
REAL_LE_TRANS) (H_RULE2 CONJ (HYP_INT 1) (HYP_INT 0));
H (MATCH_MP
INTERVAL_EPS_POS) (HYP_INT 3);
H (MATCH_MP
INTERVAL_EPS_POS) (HYP_INT 5);
H (MATCH_MP REAL_PROP_NN_ADD2) (H_RULE2 CONJ (HYP_INT 1) (HYP_INT 0));
H (MATCH_MP REAL_PROP_POS_LADD) (H_RULE2 CONJ (HYP_INT 11) (HYP_INT 10));
H (MATCH_MP REAL_PROP_POS_LADD) (H_RULE2 CONJ (THM (SPEC `x:real`
REAL_MK_NN_SSQRT)) (HYP_INT 11));
H (MATCH_MP REAL_PROP_POS_INV) (HYP_INT 0);
ASSUME_TAC (REAL_ARITH `(
ssqrt x -. u) = (
ssqrt x -. u)*.(&.1)`);
H (MATCH_MP REAL_MK_NZ_POS) (HYP_INT 2);
H (MATCH_MP
REAL_MUL_RINV) (HYP_INT 0);
H_REWRITE_RULE[(H_RULE GSYM) (HYP_INT 0)] (HYP_INT 2);
POPL_TAC[1;2;3];
H (REWRITE_RULE[REAL_MUL_ASSOC]) (HYP_INT 0);
H (REWRITE_RULE[ONCE_REWRITE_RULE[REAL_MUL_SYM]
REAL_DIFFSQ]) (HYP_INT 0);
POPL_TAC[1;2];
H_SIMP_RULE[HYP_INT 7;THM
REAL_SSQRT_SQUARE] (HYP_INT 0);
ASSUME_TAC (REAL_ARITH `abs(x -. u*.u) <=. abs(x -. f) + abs(f-. u*.u)`);
H (REWRITE_RULE[
interval_eps]) (HYP_INT 12);
H (ONCE_REWRITE_RULE[
interval_eps]) (HYP_INT 14);
H (ONCE_REWRITE_RULE[
REAL_ABS_SUB]) (HYP_INT 0);
POPL_TAC[1;5;15;16];
H (MATCH_MP
REAL_LE_ADD2) (H_RULE2 CONJ (HYP_INT 1) (HYP_INT 0));
H (MATCH_MP
REAL_LE_TRANS) (H_RULE2 CONJ (HYP_INT 3) (HYP_INT 0));
POPL_TAC[1;2;3;4];
H (AP_TERM `
real_abs `) (HYP_INT 1);
H (REWRITE_RULE[
ABS_MUL]) (HYP_INT 0);
H (MATCH_MP
REAL_LT_IMP_LE) (HYP_INT 4);
H (REWRITE_RULE[GSYM
REAL_ABS_REFL]) (HYP_INT 0);
H_REWRITE_RULE [HYP_INT 0] (HYP_INT 2);
H (MATCH_MP
REAL_LE_RMUL) (H_RULE2 CONJ (HYP_INT 5) (HYP_INT 2));
H_REWRITE_RULE [H_RULE GSYM (HYP_INT 1)] (HYP_INT 0);
POPL_TAC[1;2;3;5;6;7;8];
H (MATCH_MP
REAL_LE_TRANS) (H_RULE2 CONJ (HYP_INT 12) (HYP_INT 9));
H (MATCH_MP
REAL_SSQRT_MONO) (HYP_INT 0);
H (MATCH_MP REAL_SSQRT_SQUARE') (HYP_INT 16);
H_REWRITE_RULE [HYP_INT 0] (HYP_INT 1);
H (ONCE_REWRITE_RULE[GSYM (SPECL[`v:real`;`
ssqrt x`;`u:real`]
REAL_LE_RADD)]) (HYP_INT 0);
H (MATCH_MP
REAL_LE_INV2) (H_RULE2 CONJ (HYP_INT 9) (HYP_INT 0));
POPL_TAC[1;2;3;4;5;7;8;9;12;13];
H (MATCH_MP
REAL_LE_LMUL) (H_RULE2 CONJ (HYP_INT 3) (HYP_INT 0));
H (MATCH_MP
REAL_LE_TRANS) (H_RULE2 CONJ (HYP_INT 2) (HYP_INT 0));
H (MATCH_MP REAL_PROP_POS_INV) (HYP_INT 4);
H (MATCH_MP
REAL_LT_IMP_LE) (HYP_INT 0);
H (MATCH_MP
REAL_LE_RMUL) (H_RULE2 CONJ (HYP_INT 11) (HYP_INT 0));
H (REWRITE_RULE[GSYM REAL_MUL_ASSOC]) (HYP_INT 0);
H (MATCH_MP REAL_MK_NZ_POS) (HYP_INT 8);
H (MATCH_MP
REAL_MUL_RINV) (HYP_INT 0);
H_REWRITE_RULE[HYP_INT 0; THM
REAL_MUL_RID] (HYP_INT 2);
H (MATCH_MP
REAL_LE_TRANS) (H_RULE2 CONJ (HYP_INT 7) (HYP_INT 0));
ASM_REWRITE_TAC[
interval_eps]
]);;
let RAT_LEMMA1_SUB = prove(`~(y1 = &0) /\ ~(y2 = &0) ==>
((x1 / y1) - (x2 / y2) = (x1 * y2 - x2 * y1) * inv(y1) * inv(y2))`,
let ABS_NUM_P = prove_by_refinement(
`!m n. (m <= n) ==> (abs (&. n -. (&. m)) = &.((m-|n) + (n-|m)))`,
[
REPEAT STRIP_TAC;
ASM_SIMP_TAC[(ARITH_RULE `(m <= n ==> (m - n = 0) )/\ ( 0 + x = x)`)];
ASM_SIMP_TAC[GSYM
REAL_OF_NUM_SUB;
REAL_ABS_REFL;];
FIRST_X_ASSUM MP_TAC;
REWRITE_TAC[GSYM REAL_OF_NUM_LE];
REAL_ARITH_TAC;
])
;;
let ABS_NUM = prove_by_refinement (
`!m n. abs (&. n -. (&. m)) = &.((m-|n) + (n-|m))`,
[
REPEAT GEN_TAC ;
DISJ_CASES_TAC (SPECL [`m:num`;`n:num`]
LTE_CASES) ; (* THENL[ *)
(* first case *)
MATCH_MP_TAC
ABS_NUM_P;
FIRST_X_ASSUM MP_TAC;
ARITH_TAC;
(* second case *)
ONCE_REWRITE_TAC[REAL_ARITH `abs(x - y) = abs(y - x)`];
ONCE_REWRITE_TAC[ARITH_RULE `(a:num) + b = b + a`];
MATCH_MP_TAC
ABS_NUM_P;
ASM_REWRITE_TAC[];
]);;
let ABS_TO_INTERVAL = prove(
`!c u k. (abs (c - u) <=. k) ==> (!f g ex ey.((
interval_eps u f ex) /\ (
interval_eps k g ey) ==> (
interval_eps c f (g+.ey+.ex))))`,
EVERY[
REWRITE_TAC[
interval_eps];
DISCH_ALL_TAC;
REPEAT GEN_TAC;
DISCH_ALL_TAC;
ONCE_REWRITE_TAC [REAL_ARITH `c -. f = (c-. u) + (u-. f)`];
ONCE_REWRITE_TAC [REAL_ADD_ASSOC];
ASSUME_TAC (SPECL [`c-.u`;`u-.f`]
ABS_TRIANGLE);
IMP_RES_THEN ASSUME_TAC (REAL_ARITH `
real_abs (k-.g) <=. ey ==> (k <=. (g +. ey))`);
MATCH_MP_TAC (REAL_ARITH `(?a b.((x <=. (a+.b)) /\ (a <=. u) /\ (b <=. v))) ==> (x <=. (u +. v))`);
EXISTS_TAC `abs (c-.u)`;
EXISTS_TAC `abs(u-.f)`;
ASM_REWRITE_TAC[];
ASM_MESON_TAC[
REAL_LE_TRANS];
]);;
let lemma1 = prove(
`!n m p. ((&.p/(&.m)) <= (&.n)) <=> ((&.p/(&.m)) <= (&.n)/(&.1))`,
let lemma2 = prove(
`!n m p. ((&.p) <= ((&.n)/(&.m))) <=> ((&.p/(&.1)) <= (&.n)/(&.m))`,
let lemma3 = prove(`!a b c d. (
((0<b) /\ (0<d) /\ (a*d <=| c*b))
==> (&.a/(&.b) <=. ((&.c)/(&.d))))`,
let th = ARITH_RULE(mk_binop `(<):num->num->bool` j i) in
let th2 = MATCH_MP SUM_TRIV_NUMSEG th in
(PURE_ONCE_REWRITE_CONV[th2]) tm
else
let j_pred = mk_numeral (j'-/ Int 1) in
let j_new = mk_comb (`SUC`, j_pred) in
let th = (ISPECL [i;j_pred] (CONJUNCT2 SUM_CLAUSES_NUMSEG)) in
let rr = ARITH_RULE (mk_eq (j_new,j)) in
let th' = REWRITE_RULE[rr;ARITH_RULE (mk_binop `(<=):num->num->bool` i j)] th in
PURE_ONCE_REWRITE_CONV[th'] tm;;let thm5 = prove( hyp5,float_tac) in
let thm6 = prove( hyp6,float_tac) in
let ant = end_itlist CONJ[x_int;thm2;thm3;thm4;thm5;thm6] in
let th = MATCH_MP thm ant
in mk cache th
)
with Failure _ -> failwith "INTERVAL_OF_TERM : SSQRT"
end
else if (can (dest_unary `sqrt`) tm) then
begin
try(
let x = dest_unary `sqrt` tm in
let stm = mk_comb (`ssqrt`, x) in
let (cache,ssqrt_thm) = INTERVAL_OF_TERM convl cache bprec stm in
let (cache,int1) = INTERVAL_OF_TERM convl cache bprec`real_of_num 0` in
let (cache,int2) =INTERVAL_OF_TERM convl cache bprec x in
let ant = CONJ (INTERVAL_TO_LESS_CONV int1 int2) ssqrt_thm in
let th = MATCH_MP ssqrt_sqrt ant
in mk cache th)
with Failure _ -> failwith "INTERVAL_OF_TERM : SQRT"
end
(* treat atn *)
else if can (dest_unary `atn`) tm then
begin
let half_co = ("halfatn4_co",ARITH_SIMP_CONV[Taylor_atn.halfatn4_co]) in
let half4 = ("halfatn4",PURE_REWRITE_CONV[Taylor_atn.halfatn4;o_THM]) in
let halfatnconv = pureconv("halfatn",Taylor_atn.halfatn) in
let aconvl = (halfatnconv::half4::half_co::convl) in
let n = mk_numeral (Int (1 + (bprec - 5) / 6)) in
let x = dest_unary `atn` tm in
let sum_tm = instantiate ([],[(n,`n:num`);(x,`u:real`)],[]) `&16 * sum (0..n) (halfatn4_co u)` in
let (cache,hyp_1) = INTERVAL_OF_TERM (aconvl) cache bprec sum_tm in
let (_,_,eps2) = dest_interval (concl hyp_1) in
let eps_tm = instantiate([],[(n,`n:num`);(eps2,`eps2:real`)],[]) `float (int_of_num 1) ( -- int_of_num (6 * n + 5)) + eps2` in
let eps_thm = FLOAT_CONV eps_tm in
let eps = snd(dest_eq (concl eps_thm)) in
let hyp_2 = FLOAT_INEQ_CONV (mk_binop `(<=):real->real->bool` eps_tm eps) in (cache, MATCH_MP taylor_atn (CONJ hyp_1 hyp_2) )
end
(* treat acs *)
else if can (dest_unary `acs`) tm then
begin
let x = dest_unary `acs` tm in
let (_,int_m1) = INTERVAL_OF_TERM convl cache bprec`-- real_of_num 1` in
let (_,int_p1) = INTERVAL_OF_TERM convl cache bprec`real_of_num 1` in
let (cache,int_x) =INTERVAL_OF_TERM convl cache bprec x in
let ant1 = INTERVAL_TO_LESS_CONV int_m1 int_x in
let ant2 = INTERVAL_TO_LESS_CONV int_x int_p1 in
let th = MATCH_MP ACS_ATN (CONJ ant1 ant2) in
interval_of_conv cache bprec (PURE_ONCE_REWRITE_CONV[th]) tm
end
(* treat pi *)
else if (tm = `pi`) then
begin
interval_of_conv cache bprec (PURE_ONCE_REWRITE_CONV[pi_atn]) tm
end
(* user supplied conversions *)
else
begin
let (c,b) = strip_comb tm in
let _ = is_const c or failwith "INTERVAL_OF_TERM: case not installed" in
let (s,_) = dest_const c in
let conv = try (assoc s convl)
with Failure _ -> failwith ("INTERVAL_OF_TERM: function not found "^s) in
interval_of_conv cache bprec conv tm
end;;