From ed5a56b7b9847688ab77688a6382b0b41223310f Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Wed, 3 Apr 2024 16:12:51 -0500 Subject: [PATCH] Replace Int constructor with num_of_int This replaces the Num.Int constructor with Num.num_of_int function. This is to prepare removing dependency on Num and using Zarith. The script which was used for this patch is as follows (in bash, Linux): ``` set -x replace_all () { find . -not \( -path "./_opam" -type d -prune \) \ -not \( -type f -wholename "./RichterHilbertAxiomGeometry/Topology.ml" \) \ -type f -name "*.ml" -print0 | \ xargs --no-run-if-empty -0 sed -i -e "$1" find . -not \( -path "./_opam" -type d -prune \) \ -type f -name "*.hl" -print0 | \ xargs --no-run-if-empty -0 sed -i -e "$1" } replace_all 's/module Int /MODULE_INT_SAVED/g' replace_all 's/ Int / Num.num_of_int /g' replace_all 's/ Int(/ Num.num_of_int(/g' replace_all 's/(Int /(Num.num_of_int /g' replace_all 's/(Int(/(Num.num_of_int(/g' replace_all 's/[Int /[Num.num_of_int /g' replace_all 's/[Int(/[Num.num_of_int(/g' replace_all 's/,Int /,Num.num_of_int /g' replace_all 's/,Int(/,Num.num_of_int(/g' replace_all 's/=Int /=Num.num_of_int /g' replace_all 's/=Int(/=Num.num_of_int(/g' replace_all 's/(Num.Int /(Num.num_of_int /g' replace_all 's/(Num.Int(/(Num.num_of_int(/g' replace_all 's/MODULE_INT_SAVED/module Int /g' ``` --- 100/bertrand.ml | 34 ++-- Complex/complex_grobner.ml | 10 +- EC/excluderoots.ml | 2 +- Examples/cooper.ml | 26 +-- Examples/lucas_lehmer.ml | 8 +- Examples/machin.ml | 46 +++--- Examples/sos.ml | 158 +++++++++---------- Formal_ineqs/arith/arith_float.hl | 4 +- Formal_ineqs/arith/arith_num.hl | 8 +- Formal_ineqs/arith/more_float.hl | 6 +- Formal_ineqs/informal/informal_atn.hl | 4 +- Formal_ineqs/informal/informal_exp.hl | 8 +- Formal_ineqs/informal/informal_float.hl | 12 +- Formal_ineqs/informal/informal_search.hl | 8 +- Formal_ineqs/informal/informal_sin_cos.hl | 16 +- Formal_ineqs/taylor/m_taylor.hl | 2 +- Formal_ineqs/trig/cos_eval.hl | 4 +- Jordan/float.ml | 108 ++++++------- Jordan/misc_defs_and_lemmas.ml | 6 +- Jordan/num_ext_gcd.ml | 18 +-- Jordan/tactics_ext2.ml | 4 +- LP_arith/lp_arith.ml | 8 +- Library/binomial.ml | 6 +- Library/bitmatch.ml | 24 +-- Library/calc_real.ml | 184 +++++++++++----------- Library/pocklington.ml | 12 +- Library/pratt.ml | 14 +- Library/prime.ml | 12 +- Library/words.ml | 2 +- Multivariate/vectors.ml | 34 ++-- Rqe/poly_ext.ml | 4 +- Rqe/signs.ml | 2 +- Rqe/simplify.ml | 2 +- Tutorial/Real_analysis.ml | 2 +- Tutorial/all.ml | 2 +- calc_num.ml | 20 +-- calc_rat.ml | 2 +- int.ml | 2 +- lib.ml | 18 +-- nums.ml | 4 +- parser.ml | 2 +- printer.ml | 8 +- realarith.ml | 10 +- 43 files changed, 433 insertions(+), 433 deletions(-) diff --git a/100/bertrand.ml b/100/bertrand.ml index 1591b286..f4be87e8 100644 --- a/100/bertrand.ml +++ b/100/bertrand.ml @@ -29,7 +29,7 @@ let num_of_float = let u2 = int_of_float(y2 *. p22) in let y3 = p22 *. y2 -. float_of_int u2 in if y3 <> 0.0 then failwith "num_of_float: inexactness!" else - (Int u0 // q22 +/ Int u1 // q44 +/ Int u2 // q66) */ pow2 n;; + (Num.num_of_int u0 // q22 +/ Num.num_of_int u1 // q44 +/ Num.num_of_int u2 // q66) */ pow2 n;; (* ------------------------------------------------------------------------- *) (* Integer truncated square root *) @@ -126,9 +126,9 @@ let LN_N_CONV = if ltm <> ln_tm then failwith "expected ln(ratconst)" else let x = rat_of_term tm in let rec dlog n y = - let y' = y +/ y // Int 8 in + let y' = y +/ y // Num.num_of_int 8 in if y' ln_tm then failwith "expected ln(ratconst)" else let x = rat_of_term tm in let rec dlog n y = - let y' = y */ Int 2 in + let y' = y */ Num.num_of_int 2 in if y' primepow_tm then failwith "expected primepow(numeral)" else let q = dest_numeral tm in - if q =/ Int 0 then pth0 - else if q =/ Int 1 then pth1 else + if q =/ Num.num_of_int 0 then pth0 + else if q =/ Num.num_of_int 1 then pth1 else match factor q with [] -> failwith "internal failure in PRIMEPOW_CONV" | [p,k] -> let th1 = INST [mk_numeral q,q_tm; @@ -425,7 +425,7 @@ let PRIMEPOW_CONV = let d = q // (p */ r) in let (x,y) = bezout(p,r) in let p,r,x,y = - if x aprimedivisor_tm then failwith "expected primepow(numeral)" else let q = dest_numeral tm in - if q =/ Int 0 then failwith "APRIMEDIVISOR_CONV: not a prime power" else + if q =/ Num.num_of_int 0 then failwith "APRIMEDIVISOR_CONV: not a prime power" else match factor q with [p,k] -> let th1 = INST [mk_numeral q,q_tm; mk_numeral p,p_tm; @@ -1027,8 +1027,8 @@ let MANGOLDT_CONV = let ptm,tm = dest_comb tm0 in if ptm <> mangoldt_tm then failwith "expected mangoldt(numeral)" else let q = dest_numeral tm in - if q =/ Int 0 then pth0 - else if q =/ Int 1 then pth1 else + if q =/ Num.num_of_int 0 then pth0 + else if q =/ Num.num_of_int 1 then pth1 else match factor q with [] -> failwith "internal failure in MANGOLDT_CONV" | [p,k] -> let th1 = INST [mk_numeral q,q_tm; @@ -1040,7 +1040,7 @@ let MANGOLDT_CONV = let d = q // (p */ r) in let (x,y) = bezout(p,r) in let p,r,x,y = - if x 0) vars] + if x =/ Num.num_of_int 0 then [] else [x,map (fun v -> 0) vars] else failwith "" with Failure _ -> failwith "grob_const";; @@ -89,7 +89,7 @@ let rec grob_add l1 l2 = | ((c1,m1)::o1,(c2,m2)::o2) -> if m1 = m2 then let c = c1+/c2 and rest = grob_add o1 o2 in - if c =/ Int 0 then rest else (c,m1)::rest + if c =/ Num.num_of_int 0 then rest else (c,m1)::rest else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2) else (c2,m2)::(grob_add l1 o2);; @@ -121,7 +121,7 @@ let mdiv (c1,m1) (c2,m2) = (* Lowest common multiple of two monomials. *) (* ------------------------------------------------------------------------- *) -let mlcm (c1,m1) (c2,m2) = (Int 1,map2 max m1 m2);; +let mlcm (c1,m1) (c2,m2) = (Num.num_of_int 1,map2 max m1 m2);; (* ------------------------------------------------------------------------- *) (* Reduce monomial cm by polynomial pol, returning replacement for cm. *) @@ -183,7 +183,7 @@ let monic (pol,hist) = if pol = [] then (pol,hist) else let c',m' = hd pol in (map (fun (c,m) -> (c//c',m)) pol, - Mmul((Int 1 // c',map (K 0) m'),hist));; + Mmul((Num.num_of_int 1 // c',map (K 0) m'),hist));; (* ------------------------------------------------------------------------- *) (* The most popular heuristic is to order critical pairs by LCM monomial. *) @@ -344,7 +344,7 @@ let string_of_monomial vars (c,m) = let xnstrs = map (fun (x,n) -> x^(if n = 1 then "" else "^"^(string_of_int n))) xns in if xns = [] then Num.string_of_num c else - let basstr = if c =/ Int 1 then "" else (Num.string_of_num c)^" * " in + let basstr = if c =/ Num.num_of_int 1 then "" else (Num.string_of_num c)^" * " in basstr ^ end_itlist (fun s t -> s^" * "^t) xnstrs;; let string_of_polynomial vars l = diff --git a/EC/excluderoots.ml b/EC/excluderoots.ml index c719f9d3..d6b42e60 100644 --- a/EC/excluderoots.ml +++ b/EC/excluderoots.ml @@ -13,7 +13,7 @@ needs "Library/pocklington.ml";; let num_modinv = let rec gcdex(m,n) = if n if n if n if try rator tm = ptm with Failure _ -> false then minus_num (dest_num_const(rand tm)) @@ -767,13 +767,13 @@ let LINEARIZE_CONV = let coefficient x tm = try let l,r = dest_add tm in - if l = x then Int 1 else + if l = x then Num.num_of_int 1 else let c,y = dest_mul l in - if y = x then dest_int_const c else Int 0 + if y = x then dest_int_const c else Num.num_of_int 0 with Failure _ -> try let c,y = dest_mul tm in - if y = x then dest_int_const c else Int 0 - with Failure _ -> Int 1;; + if y = x then dest_int_const c else Num.num_of_int 0 + with Failure _ -> Num.num_of_int 1;; (* ------------------------------------------------------------------------- *) (* Find (always positive) LCM of all the multiples of x in formula tm. *) @@ -787,9 +787,9 @@ let rec formlcm x tm = lcm_num (formlcm x (lhand tm)) (formlcm x (rand tm)) else if is_forall tm || is_exists tm then formlcm x (body(rand tm)) - else if not(mem x (frees tm)) then Int 1 + else if not(mem x (frees tm)) then Num.num_of_int 1 else let c = coefficient x (rand tm) in - if c =/ Int 0 then Int 1 else c;; + if c =/ Num.num_of_int 0 then Num.num_of_int 1 else c;; (* ------------------------------------------------------------------------- *) (* Switch from "x [+ ...]" to "&1 * x [+ ...]" to suit later proforma. *) @@ -853,16 +853,16 @@ let ADJUSTCOEFF_CONV = let lop,t = dest_comb tm in let op,z = dest_comb lop in let c = coefficient (hd vars) t in - if c =/ Int 0 then REFL tm else + if c =/ Num.num_of_int 0 then REFL tm else let th1 = if c =/ l then REFL tm else let m = l // c in let th0 = if op = op_eq then pth_eq else if op = op_divides then pth_divides else if op = op_lt then - if m >/ Int 0 then pth_lt_pos else pth_lt_neg + if m >/ Num.num_of_int 0 then pth_lt_pos else pth_lt_neg else if op = op_gt then - if m >/ Int 0 then pth_gt_pos else pth_gt_neg + if m >/ Num.num_of_int 0 then pth_gt_pos else pth_gt_neg else failwith "ADJUSTCOEFF_CONV: unknown predicate" in let th1 = INST [mk_int_const m,d_tm; z,c_tm; t,e_tm] th0 in let tm1 = lhand(concl th1) in @@ -881,7 +881,7 @@ let ADJUSTCOEFF_CONV = else let tm2 = rator(rand(concl th3)) in TRANS th3 (AP_TERM tm2 (LINEAR_CMUL vars m t)) in - if l =/ Int 1 then + if l =/ Num.num_of_int 1 then CONV_RULE(funpow 2 RAND_CONV (MULTIPLY_1_CONV vars)) th1 else th1 in ADJUSTCOEFF_CONV;; @@ -899,7 +899,7 @@ let NORMALIZE_COEFF_CONV = let x,bod = dest_exists tm in let l = formlcm x tm in let th1 = ADJUSTCOEFF_CONV (x::vars) l tm in - let th2 = if l =/ Int 1 then EXISTS_MULTIPLE_THM_1 + let th2 = if l =/ Num.num_of_int 1 then EXISTS_MULTIPLE_THM_1 else INST [mk_int_const l,c_tm] pth in TRANS th1 (REWR_CONV th2 (rand(concl th1))) in NORMALIZE_COEFF_CONV;; @@ -963,7 +963,7 @@ let dplcm = if hop = divides_tm || hop = ndivides_tm then dest_int_const (hd args) else if hop = and_tm || hop = or_tm then end_itlist lcm_num (map dplcm args) - else Int 1 in + else Num.num_of_int 1 in dplcm;; (* ------------------------------------------------------------------------- *) diff --git a/Examples/lucas_lehmer.ml b/Examples/lucas_lehmer.ml index 223c8b75..6caef7eb 100644 --- a/Examples/lucas_lehmer.ml +++ b/Examples/lucas_lehmer.ml @@ -324,14 +324,14 @@ let LUCAS_LEHMER_RULE = (INST [mk_small_numeral p,p_tm] pth_base) and th_step = CONV_RULE(RAND_CONV(LAND_CONV NUM_REDUCE_CONV)) (INST [mk_small_numeral p,p_tm] pth_step) - and pp1 = pow2 p -/ Int 1 in + and pp1 = pow2 p -/ Num.num_of_int 1 in let rec lucas_lehmer k = if k = 0 then th_base,dest_numeral(rand(concl th_base)) else let th1,mval = lucas_lehmer (k - 1) in let gofer() = let mtm = rand(concl th1) in - let yval = power_num mval (Int 2) in - let qval = quo_num yval pp1 and rval = mod_num yval pp1 -/ Int 2 in + let yval = power_num mval (Num.num_of_int 2) in + let qval = quo_num yval pp1 and rval = mod_num yval pp1 -/ Num.num_of_int 2 in let th3 = INST [mk_small_numeral(k - 1),n_tm; mtm,m_tm; mk_numeral qval,q_tm; mk_numeral rval,r_tm] th_step in let th4 = MP th3 th1 in @@ -344,7 +344,7 @@ let LUCAS_LEHMER_RULE = time gofer()) else gofer() in let th1,y = lucas_lehmer (p - 2) in - if y <>/ Int 0 then failwith "LUCAS_LEHMER_RULE: not a prime" else + if y <>/ Num.num_of_int 0 then failwith "LUCAS_LEHMER_RULE: not a prime" else let th2 = SPEC(mk_small_numeral p) LUCAS_LEHMER in let th3 = CONV_RULE (LAND_CONV(RAND_CONV(LAND_CONV diff --git a/Examples/machin.ml b/Examples/machin.ml index 46e0c818..b2e3199e 100644 --- a/Examples/machin.ml +++ b/Examples/machin.ml @@ -478,21 +478,21 @@ let mclaurin_atn_rule,MCLAURIN_ATN_RULE = let pth = SPECL [x_tm; n_tm; k_tm] MCLAURIN_ATN_APPROX and CLEAN_RULE = REWRITE_RULE[real_pow] and MATCH_REAL_LE_TRANS = MATCH_MP REAL_LE_TRANS - and num_0 = Int 0 - and num_1 = Int 1 in + and num_0 = Num.num_of_int 0 + and num_1 = Num.num_of_int 1 in let mclaurin_atn_rule k0 p0 = if k0 = 0 then failwith "mclaurin_atn_rule: must have |x| <= 1/2" else - let k = Int k0 - and p = Int p0 in + let k = Num.num_of_int k0 + and p = Num.num_of_int p0 in let n = Num.int_of_num(ceiling_num ((p +/ k) // k)) in let ns = if n mod 2 = 0 then 0--(n - 1) else 0--(n - 2) in map (fun m -> if m mod 2 = 0 then num_0 else (if (m - 1) mod 4 = 0 then I else minus_num) - (num_1 // Int m)) ns + (num_1 // Num.num_of_int m)) ns and MCLAURIN_ATN_RULE k0 p0 = if k0 = 0 then failwith "MCLAURIN_ATN_RULE: must have |x| <= 1/2" else - let k = Int k0 - and p = Int p0 in + let k = Num.num_of_int k0 + and p = Num.num_of_int p0 in let n = ceiling_num ((p +/ k) // k) in let th1 = INST [mk_numeral k,k_tm; mk_numeral n,n_tm] pth in let th2 = ASSUME (lhand(lhand(concl th1))) @@ -684,9 +684,9 @@ let rec POLY l x = let atn_approx_conv,ATN_APPROX_CONV = let atn_tm = `atn` - and num_0 = Int 0 - and num_1 = Int 1 - and num_2 = Int 2 in + and num_0 = Num.num_of_int 0 + and num_1 = Num.num_of_int 1 + and num_2 = Num.num_of_int 2 in let rec log_2 x = if x <=/ num_1 then log_2 (num_2 */ x) -/ num_1 else if x >/ num_2 then log_2 (x // num_2) +/ num_1 else num_1 in @@ -718,12 +718,12 @@ let atn_approx_conv,ATN_APPROX_CONV = (* ------------------------------------------------------------------------- *) let pi_approx_rule,PI_APPROX_RULE = - let const_1_8 = Int 1 // Int 8 - and const_1_57 = Int 1 // Int 57 - and const_1_239 = Int 1 // Int 239 - and const_24 = Int 24 - and const_8 = Int 8 - and const_4 = Int 4 + let const_1_8 = Num.num_of_int 1 // Num.num_of_int 8 + and const_1_57 = Num.num_of_int 1 // Num.num_of_int 57 + and const_1_239 = Num.num_of_int 1 // Num.num_of_int 239 + and const_24 = Num.num_of_int 24 + and const_8 = Num.num_of_int 8 + and const_4 = Num.num_of_int 4 and tm_1_8 = `atn(&1 / &8)` and tm_1_57 = `atn(&1 / &57)` and tm_1_239 = `atn(&1 / &239)` @@ -802,14 +802,14 @@ let pi_approx_binary_rule,PI_APPROX_BINARY_RULE = ARITH_RULE `SUC p - p = 1`; SUB_REFL] THEN UNDISCH_TAC `abs (&2 pow p * r - a) <= inv (&2)` THEN CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV) - and num_2 = Int 2 in + and num_2 = Num.num_of_int 2 in let pi_approx_binary_rule p = - let ppow = power_num num_2 (Int p) in + let ppow = power_num num_2 (Num.num_of_int p) in let r = pi_approx_rule (p + 1) in let a = round_num (ppow */ r) in a // ppow and PI_APPROX_BINARY_RULE p = - let ppow = power_num num_2 (Int p) in + let ppow = power_num num_2 (Num.num_of_int p) in let th1 = PI_APPROX_RULE (p + 1) in let th2 = CONV_RULE(funpow 3 RAND_CONV num_CONV) th1 in let r = rat_of_term(rand(rand(lhand(concl th2)))) in @@ -823,10 +823,10 @@ let pi_approx_binary_rule,PI_APPROX_BINARY_RULE = (* ------------------------------------------------------------------------- *) let ATN_EXPAND_CONV = - let num_0 = Int 0 - and num_1 = Int 1 - and num_2 = Int 2 - and eighth = Int 1 // Int 8 + let num_0 = Num.num_of_int 0 + and num_1 = Num.num_of_int 1 + and num_2 = Num.num_of_int 2 + and eighth = Num.num_of_int 1 // Num.num_of_int 8 and atn_tm = `atn` and eighth_tm = `&1 / &8` and mk_mul = mk_binop `(*)` diff --git a/Examples/sos.ml b/Examples/sos.ml index b69361b9..46c7f634 100644 --- a/Examples/sos.ml +++ b/Examples/sos.ml @@ -16,16 +16,16 @@ exception Unsolvable;; let decimalize = let rec normalize y = - if abs_num y =/ Int 1 then normalize (y // Int 10) + 1 + if abs_num y =/ Num.num_of_int 1 then normalize (y // Num.num_of_int 10) + 1 else 0 in fun d x -> - if x =/ Int 0 then "0.0" else + if x =/ Num.num_of_int 0 then "0.0" else let y = abs_num x in let e = normalize y in - let z = pow10(-e) */ y +/ Int 1 in + let z = pow10(-e) */ y +/ Num.num_of_int 1 in let k = round_num(pow10 d */ z) in - (if x ) x y a = if y =/ Int 0 then a else (x |-> y) a;; +let (|-->) x y a = if y =/ Num.num_of_int 0 then a else (x |-> y) a;; (* ------------------------------------------------------------------------- *) (* This can be generic. *) (* ------------------------------------------------------------------------- *) -let element (d,v) i = tryapplyd v i (Int 0);; +let element (d,v) i = tryapplyd v i (Num.num_of_int 0);; let mapa f (d,v) = d,foldl (fun a i c -> (i |--> f(c)) a) undefined v;; @@ -80,14 +80,14 @@ let vec_0 n = (n,undefined:vector);; let vec_dim (v:vector) = fst v;; let vec_const c n = - if c =/ Int 0 then vec_0 n + if c =/ Num.num_of_int 0 then vec_0 n else (n,itlist (fun k -> k |-> c) (1--n) undefined :vector);; -let vec_1 = vec_const (Int 1);; +let vec_1 = vec_const (Num.num_of_int 1);; let vec_cmul c (v:vector) = let n = vec_dim v in - if c =/ Int 0 then vec_0 n + if c =/ Num.num_of_int 0 then vec_0 n else n,mapf (fun x -> c */ x) (snd v) let vec_neg (v:vector) = (fst v,mapf minus_num (snd v) :vector);; @@ -95,15 +95,15 @@ let vec_neg (v:vector) = (fst v,mapf minus_num (snd v) :vector);; let vec_add (v1:vector) (v2:vector) = let m = vec_dim v1 and n = vec_dim v2 in if m <> n then failwith "vec_add: incompatible dimensions" else - (n,combine (+/) (fun x -> x =/ Int 0) (snd v1) (snd v2) :vector);; + (n,combine (+/) (fun x -> x =/ Num.num_of_int 0) (snd v1) (snd v2) :vector);; let vec_sub v1 v2 = vec_add v1 (vec_neg v2);; let vec_dot (v1:vector) (v2:vector) = let m = vec_dim v1 and n = vec_dim v2 in if m <> n then failwith "vec_add: incompatible dimensions" else - foldl (fun a i x -> x +/ a) (Int 0) - (combine ( */ ) (fun x -> x =/ Int 0) (snd v1) (snd v2));; + foldl (fun a i x -> x +/ a) (Num.num_of_int 0) + (combine ( */ ) (fun x -> x =/ Num.num_of_int 0) (snd v1) (snd v2));; let vec_of_list l = let n = length l in @@ -119,14 +119,14 @@ let dimensions (m:matrix) = fst m;; let matrix_const c (m,n as mn) = if m <> n then failwith "matrix_const: needs to be square" - else if c =/ Int 0 then matrix_0 mn + else if c =/ Num.num_of_int 0 then matrix_0 mn else (mn,itlist (fun k -> (k,k) |-> c) (1--n) undefined :matrix);; -let matrix_1 = matrix_const (Int 1);; +let matrix_1 = matrix_const (Num.num_of_int 1);; let matrix_cmul c (m:matrix) = let (i,j) = dimensions m in - if c =/ Int 0 then matrix_0 (i,j) + if c =/ Num.num_of_int 0 then matrix_0 (i,j) else (i,j),mapf (fun x -> c */ x) (snd m);; let matrix_neg (m:matrix) = (dimensions m,mapf minus_num (snd m) :matrix);; @@ -134,7 +134,7 @@ let matrix_neg (m:matrix) = (dimensions m,mapf minus_num (snd m) :matrix);; let matrix_add (m1:matrix) (m2:matrix) = let d1 = dimensions m1 and d2 = dimensions m2 in if d1 <> d2 then failwith "matrix_add: incompatible dimensions" - else (d1,combine (+/) (fun x -> x =/ Int 0) (snd m1) (snd m2) :matrix);; + else (d1,combine (+/) (fun x -> x =/ Num.num_of_int 0) (snd m1) (snd m2) :matrix);; let matrix_sub m1 m2 = matrix_add m1 (matrix_neg m2);; @@ -169,8 +169,8 @@ let matrix_of_list l = (* ------------------------------------------------------------------------- *) let monomial_eval assig (m:monomial) = - foldl (fun a x k -> a */ power_num (apply assig x) (Int k)) - (Int 1) m;; + foldl (fun a x k -> a */ power_num (apply assig x) (Num.num_of_int k)) + (Num.num_of_int 1) m;; let monomial_1 = (undefined:monomial);; @@ -206,30 +206,30 @@ let monomial_variables m = dom m;; (* ------------------------------------------------------------------------- *) let eval assig (p:poly) = - foldl (fun a m c -> a +/ c */ monomial_eval assig m) (Int 0) p;; + foldl (fun a m c -> a +/ c */ monomial_eval assig m) (Num.num_of_int 0) p;; let poly_0 = (undefined:poly);; let poly_isconst (p:poly) = foldl (fun a m c -> m = monomial_1 && a) true p;; -let poly_var x = ((monomial_var x) |=> Int 1 :poly);; +let poly_var x = ((monomial_var x) |=> Num.num_of_int 1 :poly);; let poly_const c = - if c =/ Int 0 then poly_0 else (monomial_1 |=> c);; + if c =/ Num.num_of_int 0 then poly_0 else (monomial_1 |=> c);; let poly_cmul c (p:poly) = - if c =/ Int 0 then poly_0 + if c =/ Num.num_of_int 0 then poly_0 else mapf (fun x -> c */ x) p;; let poly_neg (p:poly) = (mapf minus_num p :poly);; let poly_add (p1:poly) (p2:poly) = - (combine (+/) (fun x -> x =/ Int 0) p1 p2 :poly);; + (combine (+/) (fun x -> x =/ Num.num_of_int 0) p1 p2 :poly);; let poly_sub p1 p2 = poly_add p1 (poly_neg p2);; let poly_cmmul (c,m) (p:poly) = - if c =/ Int 0 then poly_0 + if c =/ Num.num_of_int 0 then poly_0 else if m = monomial_1 then mapf (fun d -> c */ d) p else foldl (fun a m' d -> (monomial_mul m m' |-> c */ d) a) poly_0 p;; @@ -239,13 +239,13 @@ let poly_mul (p1:poly) (p2:poly) = let poly_div (p1:poly) (p2:poly) = if not(poly_isconst p2) then failwith "poly_div: non-constant" else let c = eval undefined p2 in - if c =/ Int 0 then failwith "poly_div: division by zero" - else poly_cmul (Int 1 // c) p1;; + if c =/ Num.num_of_int 0 then failwith "poly_div: division by zero" + else poly_cmul (Num.num_of_int 1 // c) p1;; let poly_square p = poly_mul p p;; let rec poly_pow p k = - if k = 0 then poly_const (Int 1) + if k = 0 then poly_const (Num.num_of_int 1) else if k = 1 then p else let q = poly_square(poly_pow p (k / 2)) in if k mod 2 = 1 then poly_mul p q else q;; @@ -320,7 +320,7 @@ let string_of_monomial m = let string_of_cmonomial (c,m) = if m = monomial_1 then string_of_num c - else if c =/ Int 1 then string_of_monomial m + else if c =/ Num.num_of_int 1 then string_of_monomial m else string_of_num c ^ "*" ^ string_of_monomial m;; let string_of_poly (p:poly) = @@ -328,7 +328,7 @@ let string_of_poly (p:poly) = let cms = sort (fun (m1,_) (m2,_) -> humanorder_monomial m1 m2) (graph p) in let s = List.fold_left (fun a (m,c) -> - if c if type_of tm = real_ty then poly_of_term tm @@ -469,7 +469,7 @@ let decimal = ||| prs in let exponent = (a "e" ||| a "E") ++ signed decimalint >> snd in signed decimalsig ++ possibly exponent - >> (function (h,[]) -> h | (h,[x]) -> h */ power_num (Int 10) x);; + >> (function (h,[]) -> h | (h,[x]) -> h */ power_num (Num.num_of_int 10) x);; let mkparser p s = let x,rst = p(explode s) in @@ -637,12 +637,12 @@ let scale_then = and maximal_element amat acc = foldl (fun maxa m c -> max_num maxa (abs_num c)) acc amat in fun solver obj mats -> - let cd1 = itlist common_denominator mats (Int 1) - and cd2 = common_denominator (snd obj) (Int 1) in + let cd1 = itlist common_denominator mats (Num.num_of_int 1) + and cd2 = common_denominator (snd obj) (Num.num_of_int 1) in let mats' = map (mapf (fun x -> cd1 */ x)) mats and obj' = vec_cmul cd2 obj in - let max1 = itlist maximal_element mats' (Int 0) - and max2 = maximal_element (snd obj') (Int 0) in + let max1 = itlist maximal_element mats' (Num.num_of_int 0) + and max2 = maximal_element (snd obj') (Num.num_of_int 0) in let scal1 = pow2 (20-int_of_float(log(float_of_num max1) /. log 2.0)) and scal2 = pow2 (20-int_of_float(log(float_of_num max2) /. log 2.0)) in let mats'' = map (mapf (fun x -> x */ scal1)) mats' @@ -665,7 +665,7 @@ let nice_vector n = mapa (nice_rational n);; let linear_program_basic a = let m,n = dimensions a in let mats = map (fun j -> diagonal (column j a)) (1--n) - and obj = vec_const (Int 1) m in + and obj = vec_const (Num.num_of_int 1) m in let rv,res = run_csdp false obj mats in if rv = 1 || rv = 2 then false else if rv = 0 then true @@ -679,7 +679,7 @@ let linear_program a b = let m,n = dimensions a in if vec_dim b <> m then failwith "linear_program: incompatible dimensions" else let mats = diagonal b :: map (fun j -> diagonal (column j a)) (1--n) - and obj = vec_const (Int 1) m in + and obj = vec_const (Num.num_of_int 1) m in let rv,res = run_csdp false obj mats in if rv = 1 || rv = 2 then false else if rv = 0 then true @@ -699,8 +699,8 @@ let in_convex_hull pts pt = let m = v + n - 1 in let mat = (m,n), - itern 1 pts2 (fun pts j -> itern 1 pts (fun x i -> (i,j) |-> Int x)) - (iter (1,n) (fun i -> (v + i,i+1) |-> Int 1) undefined) in + itern 1 pts2 (fun pts j -> itern 1 pts (fun x i -> (i,j) |-> Num.num_of_int x)) + (iter (1,n) (fun i -> (v + i,i+1) |-> Num.num_of_int 1) undefined) in linear_program_basic mat;; (* ------------------------------------------------------------------------- *) @@ -719,13 +719,13 @@ let minimal_convex_hull = (* ------------------------------------------------------------------------- *) let equation_cmul c eq = - if c =/ Int 0 then undefined else mapf (fun d -> c */ d) eq;; + if c =/ Num.num_of_int 0 then undefined else mapf (fun d -> c */ d) eq;; -let equation_add eq1 eq2 = combine (+/) (fun x -> x =/ Int 0) eq1 eq2;; +let equation_add eq1 eq2 = combine (+/) (fun x -> x =/ Num.num_of_int 0) eq1 eq2;; let equation_eval assig eq = let value v = apply assig v in - foldl (fun a v c -> a +/ value(v) */ c) (Int 0) eq;; + foldl (fun a v c -> a +/ value(v) */ c) (Num.num_of_int 0) eq;; (* ------------------------------------------------------------------------- *) (* Eliminate among linear equations: return unconstrained variables and *) @@ -748,10 +748,10 @@ else raise Unsolvable | v::vs -> try let eq,oeqs = extract_first (fun e -> defined e v) eqs in let a = apply eq v in - let eq' = equation_cmul (Int(-1) // a) (undefine v eq) in + let eq' = equation_cmul (Num.num_of_int(-1) // a) (undefine v eq) in let elim e = - let b = tryapplyd e v (Int 0) in - if b =/ Int 0 then e else + let b = tryapplyd e v (Num.num_of_int 0) in + if b =/ Num.num_of_int 0 then e else equation_add e (equation_cmul (minus_num b // a) eq) in eliminate vs ((v |-> eq') (mapf elim dun)) (map elim oeqs) with Failure _ -> eliminate vs dun eqs in @@ -779,10 +779,10 @@ let eliminate_all_equations one = if is_undefined eq then eliminate dun oeqs else let v = choose_variable eq in let a = apply eq v in - let eq' = equation_cmul (Int(-1) // a) (undefine v eq) in + let eq' = equation_cmul (Num.num_of_int(-1) // a) (undefine v eq) in let elim e = - let b = tryapplyd e v (Int 0) in - if b =/ Int 0 then e else + let b = tryapplyd e v (Num.num_of_int 0) in + if b =/ Num.num_of_int 0 then e else equation_add e (equation_cmul (minus_num b // a) eq) in eliminate ((v |-> eq') (mapf elim dun)) (map elim oeqs) in fun eqs -> @@ -796,10 +796,10 @@ let eliminate_all_equations one = let solve_equations one eqs = let vars,assigs = eliminate_all_equations one eqs in - let vfn = itlist (fun v -> (v |-> Int 0)) vars (one |=> Int(-1)) in + let vfn = itlist (fun v -> (v |-> Num.num_of_int 0)) vars (one |=> Num.num_of_int(-1)) in let ass = combine (+/) (fun c -> false) (mapf (equation_eval vfn) assigs) vfn in - if forall (fun e -> equation_eval ass e =/ Int 0) eqs + if forall (fun e -> equation_eval ass e =/ Num.num_of_int 0) eqs then undefine one ass else raise Sanity;; (* ------------------------------------------------------------------------- *) @@ -835,8 +835,8 @@ let diag m = let rec diagonalize i m = if is_zero m then [] else let a11 = element m (i,i) in - if a11 lcm_num a (denominator c)) (Int 1) (snd l) // - foldl (fun a i c -> gcd_num a (numerator c)) (Int 0) (snd l) in + let a = foldl (fun a i c -> lcm_num a (denominator c)) (Num.num_of_int 1) (snd l) // + foldl (fun a i c -> gcd_num a (numerator c)) (Num.num_of_int 0) (snd l) in (c // (a */ a)),mapa (fun x -> a */ x) l in let d' = map adj d in - let a = itlist (lcm_num o denominator o fst) d' (Int 1) // - itlist (gcd_num o numerator o fst) d' (Int 0) in - (Int 1 // a),map (fun (c,l) -> (a */ c,l)) d';; + let a = itlist (lcm_num o denominator o fst) d' (Num.num_of_int 1) // + itlist (gcd_num o numerator o fst) d' (Num.num_of_int 0) in + (Num.num_of_int 1 // a),map (fun (c,l) -> (a */ c,l)) d';; (* ------------------------------------------------------------------------- *) (* Enumeration of monomials with given multidegree bound. *) @@ -913,7 +913,7 @@ let epoly_pmul p q acc = (* ------------------------------------------------------------------------- *) let epoly_cmul c l = - if c =/ Int 0 then undefined else mapf (equation_cmul c) l;; + if c =/ Num.num_of_int 0 then undefined else mapf (equation_cmul c) l;; @@ -988,13 +988,13 @@ let csdp nblocks blocksizes obj mats = (* 3D versions of matrix operations to consider blocks separately. *) (* ------------------------------------------------------------------------- *) -let bmatrix_add = combine (+/) (fun x -> x =/ Int 0);; +let bmatrix_add = combine (+/) (fun x -> x =/ Num.num_of_int 0);; let bmatrix_cmul c bm = - if c =/ Int 0 then undefined + if c =/ Num.num_of_int 0 then undefined else mapf (fun x -> c */ x) bm;; -let bmatrix_neg = bmatrix_cmul (Int(-1));; +let bmatrix_neg = bmatrix_cmul (Num.num_of_int(-1));; let bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);; @@ -1028,7 +1028,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = let mons = enumerate_monomials e vars in let nons = zip mons (1--length mons) in mons, - itlist (fun (m,n) -> (m |-> ((-k,-n,n) |=> Int 1))) nons undefined in + itlist (fun (m,n) -> (m |-> ((-k,-n,n) |=> Num.num_of_int 1))) nons undefined in let mk_sqmultiplier k (p,c) = let e = (d - multidegree p) / 2 in let mons = enumerate_monomials e vars in @@ -1038,7 +1038,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = itlist (fun (m2,n2) a -> let m = monomial_mul m1 m2 in if n1 > n2 then a else - let c = if n1 = n2 then Int 1 else Int 2 in + let c = if n1 = n2 then Num.num_of_int 1 else Num.num_of_int 2 in let e = tryapplyd a m undefined in (m |-> equation_add ((k,n1,n2) |=> c) e) a) nons) @@ -1053,11 +1053,11 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = let eqns = foldl (fun a m e -> e::a) [] bigsum in let pvs,assig = eliminate_all_equations (0,0,0) eqns in let qvars = (0,0,0)::pvs in - let allassig = itlist (fun v -> (v |-> (v |=> Int 1))) pvs assig in + let allassig = itlist (fun v -> (v |-> (v |=> Num.num_of_int 1))) pvs assig in let mk_matrix v = foldl (fun m (b,i,j) ass -> if b < 0 then m else - let c = tryapplyd ass v (Int 0) in - if c =/ Int 0 then m else + let c = tryapplyd ass v (Num.num_of_int 0) in + if c =/ Num.num_of_int 0 then m else ((b,j,i) |-> c) (((b,i,j) |-> c) m)) undefined allassig in let diagents = foldl @@ -1065,7 +1065,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = undefined allassig in let mats = map mk_matrix qvars and obj = length pvs, - itern 1 pvs (fun v i -> (i |--> tryapplyd diagents v (Int 0))) + itern 1 pvs (fun v i -> (i |--> tryapplyd diagents v (Num.num_of_int 0))) undefined in let raw_vec = if pvs = [] then vec_0 0 else scale_then (csdp nblocks blocksizes) obj mats in @@ -1086,7 +1086,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = map pow2 (5--66)) in let newassigs = itlist (fun k -> el (k - 1) pvs |-> element vec k) - (1--vec_dim vec) ((0,0,0) |=> Int(-1)) in + (1--vec_dim vec) ((0,0,0) |=> Num.num_of_int(-1)) in let finalassigs = foldl (fun a v e -> (v |-> equation_eval newassigs e) a) newassigs allassig in @@ -1248,7 +1248,7 @@ let REAL_NONLINEAR_SUBST_PROVER = CONV_RULE(REWR_CONV(REAL_ARITH `x + a = (y:real) <=> x = y - a`)) in let rec substitutable_monomial fvs tm = match tm with - Var(_,Tyapp("real",[])) when not (mem tm fvs) -> Int 1,tm + Var(_,Tyapp("real",[])) when not (mem tm fvs) -> Num.num_of_int 1,tm | Comb(Comb(Const("real_mul",_),c),(Var(_,_) as t)) when is_ratconst c && not (mem t fvs) -> rat_of_term c,t @@ -1265,7 +1265,7 @@ let REAL_NONLINEAR_SUBST_PROVER = isolate_variable v(shuffle1 th) in let make_substitution th = let (c,v) = substitutable_monomial [] (lhs(concl th)) in - let th1 = AP_TERM (mk_comb(mul_tm,term_of_rat(Int 1 // c))) th in + let th1 = AP_TERM (mk_comb(mul_tm,term_of_rat(Num.num_of_int 1 // c))) th in let th2 = CONV_RULE(BINOP_CONV REAL_POLY_MUL_CONV) th1 in CONV_RULE (RAND_CONV REAL_POLY_CONV) (isolate_variable v th2) in fun translator -> @@ -1518,32 +1518,32 @@ let sumofsquares_general_symmetry tool pol = match cls with [] -> raise Sanity | [h] -> acc - | h::t -> map (fun k -> (k |-> Int(-1)) (h |=> Int 1)) t @ acc in + | h::t -> map (fun k -> (k |-> Num.num_of_int(-1)) (h |=> Num.num_of_int 1)) t @ acc in itlist mk_eq eqvcls [] in let eqs = foldl (fun a x y -> y::a) [] (itern 1 lpps (fun m1 n1 -> itern 1 lpps (fun m2 n2 f -> let m = monomial_mul m1 m2 in if n1 > n2 then f else - let c = if n1 = n2 then Int 1 else Int 2 in + let c = if n1 = n2 then Num.num_of_int 1 else Num.num_of_int 2 in (m |-> ((n1,n2) |-> c) (tryapplyd f m undefined)) f)) (foldl (fun a m c -> (m |-> ((0,0)|=>c)) a) undefined pol)) @ sym_eqs in let pvs,assig = eliminate_all_equations (0,0) eqs in - let allassig = itlist (fun v -> (v |-> (v |=> Int 1))) pvs assig in + let allassig = itlist (fun v -> (v |-> (v |=> Num.num_of_int 1))) pvs assig in let qvars = (0,0)::pvs in let diagents = end_itlist equation_add (map (fun i -> apply allassig (i,i)) (1--n)) in let mk_matrix v = ((n,n), - foldl (fun m (i,j) ass -> let c = tryapplyd ass v (Int 0) in - if c =/ Int 0 then m else + foldl (fun m (i,j) ass -> let c = tryapplyd ass v (Num.num_of_int 0) in + if c =/ Num.num_of_int 0 then m else ((j,i) |-> c) (((i,j) |-> c) m)) undefined allassig :matrix) in let mats = map mk_matrix qvars and obj = length pvs, - itern 1 pvs (fun v i -> (i |--> tryapplyd diagents v (Int 0))) + itern 1 pvs (fun v i -> (i |--> tryapplyd diagents v (Num.num_of_int 0))) undefined in let raw_vec = if pvs = [] then vec_0 0 else tool obj mats in let find_rounding d = diff --git a/Formal_ineqs/arith/arith_float.hl b/Formal_ineqs/arith/arith_float.hl index 59c96044..a4acf162 100644 --- a/Formal_ineqs/arith/arith_float.hl +++ b/Formal_ineqs/arith/arith_float.hl @@ -2411,7 +2411,7 @@ let init_logs () = let float_to_log_string tm = let s, n_tm, e_tm = dest_float tm in let n = (if s = "T" then minus_num else I) (raw_dest_hash n_tm) in - let e = raw_dest_hash e_tm -/ Int Float_theory.min_exp in + let e = raw_dest_hash e_tm -/ Num.num_of_int Float_theory.min_exp in string_of_num n ^ "," ^ string_of_num e;; let log_binop name pp tm1 tm2 = @@ -2829,7 +2829,7 @@ let dest_float_raw f_tm = (* Compares raw representations of two floating-point numbers f1 and f2. *) (* Returns -1 if f1 < f2, 0 if f1 = f2, and 1 if f1 > f2. *) let compare_floats_raw = - let denorm n e = n */ (Int Arith_num.arith_base **/ e) in + let denorm n e = n */ (Num.num_of_int Arith_num.arith_base **/ e) in let cmp n1 e1 n2 e2 = if e1 <= e2 then compare_num n1 (denorm n2 (e2 -/ e1)) diff --git a/Formal_ineqs/arith/arith_num.hl b/Formal_ineqs/arith/arith_num.hl index bc281f35..ec25afab 100644 --- a/Formal_ineqs/arith/arith_num.hl +++ b/Formal_ineqs/arith/arith_num.hl @@ -167,11 +167,11 @@ let B0_EXPLICIT = prove(mk_eq(mk_comb(b0_const, n_var_num), let mk_table = Hashtbl.create maximum;; for i = 0 to maximum - 1 do - Hashtbl.add mk_table (Int i) const_array.(i) + Hashtbl.add mk_table (Num.num_of_int i) const_array.(i) done;; (* mk_numeral *) -let max_num = Int maximum;; +let max_num = Num.num_of_int maximum;; let mk_numeral_hash = let rec mk_num n = @@ -209,12 +209,12 @@ let mk_small_numeral_array = let dest_table_num = Hashtbl.create maximum;; for i = 0 to maximum - 1 do - Hashtbl.add dest_table_num names_array.(i) (Int i) + Hashtbl.add dest_table_num names_array.(i) (Num.num_of_int i) done;; (* dest_numeral *) -let max_num = Int maximum;; +let max_num = Num.num_of_int maximum;; let rec raw_dest_hash tm = if tm = zero_const then diff --git a/Formal_ineqs/arith/more_float.hl b/Formal_ineqs/arith/more_float.hl index f150e382..9d0749ea 100644 --- a/Formal_ineqs/arith/more_float.hl +++ b/Formal_ineqs/arith/more_float.hl @@ -62,14 +62,14 @@ let float_tm_of_float = s, t, n and extract = let b = float_of_int Arith_num.arith_base in - let nb = Int Arith_num.arith_base in + let nb = Num.num_of_int Arith_num.arith_base in let rec step k f acc = if k <= 0 then acc else let d = int_of_float f in - step (k - 1) ((f -. float_of_int d) *. b) (Int d +/ (nb */ acc)) in + step (k - 1) ((f -. float_of_int d) *. b) (Num.num_of_int d +/ (nb */ acc)) in fun pp f -> - step pp f (Int 0) + step pp f (Num.num_of_int 0) in fun pp f -> let s, x, k = split f in diff --git a/Formal_ineqs/informal/informal_atn.hl b/Formal_ineqs/informal/informal_atn.hl index 170b3500..9a4c464f 100644 --- a/Formal_ineqs/informal/informal_atn.hl +++ b/Formal_ineqs/informal/informal_atn.hl @@ -54,13 +54,13 @@ let halfatn4_pos_lo pp t = f (f (f (f t)));; let rec fact n = - if sign_num n <= 0 then Int 1 else + if sign_num n <= 0 then Num.num_of_int 1 else n */ fact (pred_num n);; let atn_tables pp n = let t1 = map (fun i -> 4 * i + 1) (0 -- (n / 2)) and t2 = map (fun i -> 4 * i + 3) (0 -- ((n + 1) / 2 - 1)) in - let f n = if n = 1 then mk_num_interval (Int n) else inv_interval pp (mk_num_interval (Int n)) in + let f n = if n = 1 then mk_num_interval (Num.num_of_int n) else inv_interval pp (mk_num_interval (Num.num_of_int n)) in map f t1, map f t2;; (* Computes x^k / k! *) diff --git a/Formal_ineqs/informal/informal_exp.hl b/Formal_ineqs/informal/informal_exp.hl index 4a1ab749..30d3346a 100644 --- a/Formal_ineqs/informal/informal_exp.hl +++ b/Formal_ineqs/informal/informal_exp.hl @@ -27,17 +27,17 @@ open Informal_poly;; let exp_max_x = 1.0;; let rec fact n = - if sign_num n <= 0 then Int 1 else + if sign_num n <= 0 then Num.num_of_int 1 else n */ fact (pred_num n);; let exp_pos_tables pp n = - let t1 = map (fun i -> fact (Int i)) (0 -- n) in + let t1 = map (fun i -> fact (Num.num_of_int i)) (0 -- n) in let f n = inv_interval pp (mk_num_interval n) in map f t1;; let exp_neg_tables pp n = - let t1 = map (fun i -> fact (Int (2 * i))) (0 -- (n / 2)) and - t2 = map (fun i -> fact (Int (2 * i + 1))) (0 -- ((n + 1) / 2 - 1)) in + let t1 = map (fun i -> fact (Num.num_of_int (2 * i))) (0 -- (n / 2)) and + t2 = map (fun i -> fact (Num.num_of_int (2 * i + 1))) (0 -- ((n + 1) / 2 - 1)) in let f n = inv_interval pp (mk_num_interval n) in map f t1, map f t2;; diff --git a/Formal_ineqs/informal/informal_float.hl b/Formal_ineqs/informal/informal_float.hl index 9e76ce44..b2cda492 100644 --- a/Formal_ineqs/informal/informal_float.hl +++ b/Formal_ineqs/informal/informal_float.hl @@ -86,9 +86,9 @@ let print_ifloat = print_ifloat_fmt Format.std_formatter;; (* Creates a floating-point value *) let mk_float n e : ifloat = if n < 0 then - true, mk_nat (minus_num (Int n)), e + min_exp + true, mk_nat (minus_num (Num.num_of_int n)), e + min_exp else - false, mk_nat (Int n), e + min_exp;; + false, mk_nat (Num.num_of_int n), e + min_exp;; let mk_num_float n = false, mk_nat n, min_exp;; @@ -107,7 +107,7 @@ let make_float s n e : ifloat = s, mk_nat n, e;; let num_of_ifloat = let b = num_of_int arith_base in fun ((s, n, e) : ifloat) -> - let r = (dest_nat n) */ (b **/ Int (e - min_exp)) in + let r = (dest_nat n) */ (b **/ Num.num_of_int (e - min_exp)) in if s then minus_num r else r;; let float_of_ifloat f = @@ -139,14 +139,14 @@ let ifloat_of_float = s, t, n and extract = let b = float_of_int arith_base in - let nb = Int arith_base in + let nb = Num.num_of_int arith_base in let rec step k f acc = if k <= 0 then acc else let d = int_of_float f in - step (k - 1) ((f -. float_of_int d) *. b) (Int d +/ (nb */ acc)) in + step (k - 1) ((f -. float_of_int d) *. b) (Num.num_of_int d +/ (nb */ acc)) in fun pp f -> - step pp f (Int 0) + step pp f (Num.num_of_int 0) in fun pp f -> let s, x, k = split f in diff --git a/Formal_ineqs/informal/informal_search.hl b/Formal_ineqs/informal/informal_search.hl index d567fb66..60ad68c0 100644 --- a/Formal_ineqs/informal/informal_search.hl +++ b/Formal_ineqs/informal/informal_search.hl @@ -243,8 +243,8 @@ let opt = { let x_list = mk_list ([mk_float (-10) 0; mk_float (-10) 0; mk_float (-10) 0], `:real`);; let z_list = mk_list ([mk_float 10 0; mk_float 10 0; mk_float 10 0], `:real`);; -let x_inf = [Informal_float.mk_float (Int (-10)) 0; Informal_float.mk_float (Int (-10)) 0; Informal_float.mk_float (Int (-10)) 0];; -let z_inf = [Informal_float.mk_float (Int 10) 0; Informal_float.mk_float (Int 10) 0; Informal_float.mk_float (Int 10) 0];; +let x_inf = [Informal_float.mk_float (Num.num_of_int (-10)) 0; Informal_float.mk_float (Num.num_of_int (-10)) 0; Informal_float.mk_float (Num.num_of_int (-10)) 0];; +let z_inf = [Informal_float.mk_float (Num.num_of_int 10) 0; Informal_float.mk_float (Num.num_of_int 10) 0; Informal_float.mk_float (Num.num_of_int 10) 0];; let dom_th = mk_m_center_domain 3 5 x_list z_list;; let dom_inf = Informal_taylor.mk_m_center_domain 5 x_inf z_inf;; @@ -268,8 +268,8 @@ result_stats c;; (***) -let x_inf = [Informal_float.mk_float (Int 1) 0];; -let y_inf = [Informal_float.mk_float (Int 3) 0];; +let x_inf = [Informal_float.mk_float (Num.num_of_int 1) 0];; +let y_inf = [Informal_float.mk_float (Num.num_of_int 3) 0];; let dom_inf = Informal_taylor.mk_m_center_domain 5 x_inf y_inf;; diff --git a/Formal_ineqs/informal/informal_sin_cos.hl b/Formal_ineqs/informal/informal_sin_cos.hl index 3b8dd9f4..b7a24eee 100644 --- a/Formal_ineqs/informal/informal_sin_cos.hl +++ b/Formal_ineqs/informal/informal_sin_cos.hl @@ -24,15 +24,15 @@ open Informal_poly;; open Informal_atn;; let rec fact n = - if sign_num n <= 0 then Int 1 else + if sign_num n <= 0 then Num.num_of_int 1 else n */ fact (pred_num n);; let one = mk_small_num_float 1 and neg_one = neg_float (mk_small_num_float 1);; let cos_tables pp n = - let t1 = map (fun i -> fact (Int (4 * i))) (0 -- (n / 2)) and - t2 = map (fun i -> fact (Int (4 * i + 2))) (0 -- ((n + 1) / 2 - 1)) in + let t1 = map (fun i -> fact (Num.num_of_int (4 * i))) (0 -- (n / 2)) and + t2 = map (fun i -> fact (Num.num_of_int (4 * i + 2))) (0 -- ((n + 1) / 2 - 1)) in let f n = inv_interval pp (mk_num_interval n) in map f t1, map f t2;; @@ -366,17 +366,17 @@ let n = -10000;; let a = 3 and b = 5;; -let x = mk_interval (mk_float (Int a) 0, mk_float (Int b) 0);; -let y = mk_interval (mk_float (Int (-a)) 0, mk_float (Int b) 0);; -let z = mk_interval (mk_float (Int (-b)) 0, mk_float (Int a) 0);; -let u = mk_interval (mk_float (Int (-3)) 0, mk_float (Int (-2)) 0);; +let x = mk_interval (mk_float (Num.num_of_int a) 0, mk_float (Num.num_of_int b) 0);; +let y = mk_interval (mk_float (Num.num_of_int (-a)) 0, mk_float (Num.num_of_int b) 0);; +let z = mk_interval (mk_float (Num.num_of_int (-b)) 0, mk_float (Num.num_of_int a) 0);; +let u = mk_interval (mk_float (Num.num_of_int (-3)) 0, mk_float (Num.num_of_int (-2)) 0);; abs_interval x;; abs_interval y;; abs_interval z;; abs_interval u;; -let x = mk_interval (mk_float (Int a) 0, mk_float (Int b) 0);; +let x = mk_interval (mk_float (Num.num_of_int a) 0, mk_float (Num.num_of_int b) 0);; let x_th = (ASSUME o Interval_arith.mk_interval `x:real` o mk_pair) (More_float.mk_float a 0, More_float.mk_float b 0);; diff --git a/Formal_ineqs/taylor/m_taylor.hl b/Formal_ineqs/taylor/m_taylor.hl index 1fe5d544..13775d83 100644 --- a/Formal_ineqs/taylor/m_taylor.hl +++ b/Formal_ineqs/taylor/m_taylor.hl @@ -59,7 +59,7 @@ let has_size_array = Array.init (max_dim + 1) (fun i -> match i with | 0 -> TRUTH | 1 -> HAS_SIZE_1 - | _ -> HAS_SIZE_DIMINDEX_RULE(mk_finty(Int i)));; + | _ -> HAS_SIZE_DIMINDEX_RULE(mk_finty(Num.num_of_int i)));; let dimindex_array = Array.init (max_dim + 1) (fun i -> if i < 1 then TRUTH else MATCH_MP DIMINDEX_UNIQUE has_size_array.(i));; diff --git a/Formal_ineqs/trig/cos_eval.hl b/Formal_ineqs/trig/cos_eval.hl index fc68868d..4027607d 100644 --- a/Formal_ineqs/trig/cos_eval.hl +++ b/Formal_ineqs/trig/cos_eval.hl @@ -727,7 +727,7 @@ let reduction_zero a_tm b_tm = (* i < 0 *) let reduction_neg pp i a_tm b_tm = - let i_eq_th, i_num_tm = float_eq_th_of_num (Int (-i)) in + let i_eq_th, i_num_tm = float_eq_th_of_num (Num.num_of_int (-i)) in let z_tm = rand (concl i_eq_th) in let two_pi_th, _, (lo_tm, hi_tm) = two_pi_array.(pp) in let lo_ge0_th = two_pi_low.(pp) in @@ -750,7 +750,7 @@ let reduction_neg pp i a_tm b_tm = (* i > 0 *) let reduction_pos pp i a_tm b_tm = - let i_eq_th, i_num_tm = float_eq_th_of_num (Int i) in + let i_eq_th, i_num_tm = float_eq_th_of_num (Num.num_of_int i) in let z_tm = rand (concl i_eq_th) in let two_pi_th, _, (lo_tm, hi_tm) = two_pi_array.(pp) in let lo_ge0_th = two_pi_low.(pp) in diff --git a/Jordan/float.ml b/Jordan/float.ml index 22c2f115..51e5a8d2 100644 --- a/Jordan/float.ml +++ b/Jordan/float.ml @@ -67,8 +67,8 @@ let (mk_int:Num.num -> term) = Failure _ -> failwith ("dest_int "^(string_of_num a));; add_test("mk_int", - (mk_int (Int (-1443)) = `--: (&:1443)`) && - (mk_int (Int 37) = `(&:37)`));; + (mk_int (Num.num_of_int (-1443)) = `--: (&:1443)`) && + (mk_int (Num.num_of_int 37) = `(&:37)`));; (* ------------------------------------------------------------------ *) @@ -76,39 +76,39 @@ 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));; + u -> (u,(Num.num_of_int 1));; add_test("split_ratio", - let (a,b) = split_ratio ((Int 4)//(Int 20)) in - (a =/ (Int 1)) && (b =/ (Int 5)));; + let (a,b) = split_ratio ((Num.num_of_int 4)//(Num.num_of_int 20)) in + (a =/ (Num.num_of_int 1)) && (b =/ (Num.num_of_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 intC = (Num.num_of_int c) in let rec divC (a,b) = - if ((Int 0) =/ mod_num a intC) then (divC (a//intC,b+/(Int 1))) + if ((Num.num_of_int 0) =/ mod_num a intC) then (divC (a//intC,b+/(Num.num_of_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";; + divC (r,(Num.num_of_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))));; + (factor_C 2 (Num.num_of_int (4096+32)) = (Num.num_of_int 129,Num.num_of_int 5)) && + (factor_C 10 (Num.num_of_int (5000)) = (Num.num_of_int 5,Num.num_of_int 3)) && + (cannot (factor_C 2) ((Num.num_of_int 50)//(Num.num_of_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));; + (dest_int a)*/ ((Num.num_of_int 2) **/ (dest_int b));; add_test("dest_float", - dest_float `float (&:3) (&:17)` = (Int 393216));; + dest_float `float (&:3) (&:17)` = (Num.num_of_int 393216));; add_test("dest_float2", (* must express as numeral first *) cannot dest_float `float ((&:3)+:(&:1)) (&:17)`);; @@ -118,7 +118,7 @@ add_test("dest_float2", (* must express as numeral first *) 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 (a',exp_a) = if (a=/(Num.num_of_int 0)) then ((Num.num_of_int 0),(Num.num_of_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 @@ -126,13 +126,13 @@ let (mk_float:Num.num -> term) = else failwith "mk_float";; add_test("mk_float", - mk_float (Int (4096+32)) = `float (&:129) (&:5)` && - (mk_float (Int 0) = `float (&:0) (&:0)`));; + mk_float (Num.num_of_int (4096+32)) = `float (&:129) (&:5)` && + (mk_float (Num.num_of_int 0) = `float (&:0) (&: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))));; + rtest ((Num.num_of_int 3)//(Num.num_of_int 1024)) && + (cannot rtest ((Num.num_of_int 1)//(Num.num_of_int 3))));; add_test("mk_float dest_float", (* constructs canonical form of float *) mk_float (dest_float `float (&:4) (&:3)`) = `float (&:1) (&:5)`);; @@ -141,27 +141,27 @@ add_test("mk_float dest_float", (* constructs canonical form of float *) (* creates decimal of the form `DECIMAL a b` with a prime to 10 *) let (mk_pos_decimal:Num.num -> term) = function r -> - let _ = assert (r >=/ (Int 0)) in + let _ = assert (r >=/ (Num.num_of_int 0)) in let (a,b) = split_ratio r in - if (a=/(Int 0)) then `#0` else + if (a=/(Num.num_of_int 0)) then `#0` 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 + let _ = assert(b2 =/ (Num.num_of_int 1)) in + let c = end_itlist Num.max_num [exp_b5-/exp_a5;exp_b2-/exp_a2;(Num.num_of_int 0)] in + let a' = a2*/((Num.num_of_int 2)**/ (c +/ exp_a2 -/ exp_b2))*/ + ((Num.num_of_int 5)**/(c +/ exp_a5 -/ exp_b5)) in + let b' = (Num.num_of_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`));; + mk_pos_decimal (Num.num_of_int (5000)) = `#5000` && + (mk_pos_decimal ((Num.num_of_int 30)//(Num.num_of_int 40)) = `#0.75`) && + (mk_pos_decimal (Num.num_of_int 0) = `#0`) && + (mk_pos_decimal ((Num.num_of_int 15)//(Num.num_of_int 25)) = `#0.6`) && + (mk_pos_decimal ((Num.num_of_int 25)//(Num.num_of_int 4)) = `#6.25`) && + (mk_pos_decimal ((Num.num_of_int 2)//(Num.num_of_int 25)) = `#0.08`));; let (mk_decimal:Num.num->term) = function r -> @@ -170,8 +170,8 @@ let (mk_decimal:Num.num->term) = if (a < 0) then (mk_comb (`--.`, b)) else b;; add_test("mk_decimal", - (mk_decimal (Int 3) = `#3`) && - (mk_decimal (Int (-3)) = `--. (#3)`));; + (mk_decimal (Num.num_of_int 3) = `#3`) && + (mk_decimal (Num.num_of_int (-3)) = `--. (#3)`));; @@ -185,7 +185,7 @@ let (dest_decimal:term -> Num.num) = a1//b1;; add_test("dest_decimal", - dest_decimal `#3.4` =/ ((Int 34)//(Int 10)));; + dest_decimal `#3.4` =/ ((Num.num_of_int 34)//(Num.num_of_int 10)));; add_test("dest_decimal2", cannot dest_decimal `--. (#3.4)`);; @@ -1084,18 +1084,18 @@ let add_test,test = new_test_suite();; Write it as a*2^k, where 1 <= a < 2, return k. Except: - num_exponent (Int 0) is -1. + num_exponent (Num.num_of_int 0) is -1. *) let (num_exponent:Num.num -> Num.num) = fun a -> let afloat = float_of_num (abs_num a) in - Int ((snd (frexp afloat)) - 1);; + Num.num_of_int ((snd (frexp afloat)) - 1);; -(*test*)let f (u,v) = ((num_exponent u) =(Int v)) in +(*test*)let f (u,v) = ((num_exponent u) =(Num.num_of_int v)) in add_test("num_exponenwt", forall f - [Int 1,0; Int 65,6; Int (-65),6; - Int 0,-1; (Int 3)//(Int 4),-1]);; + [Int 1,0; Num.num_of_int 65,6; Num.num_of_int (-65),6; + Num.num_of_int 0,-1; (Num.num_of_int 3)//(Num.num_of_int 4),-1]);; (* ------------------------------------------------------------------ *) let dest_unary op tm = @@ -1107,49 +1107,49 @@ let dest_unary op tm = (* ------------------------------------------------------------------ *) -(* finds a nearby (outward-rounded) Int with only prec_b significant bits *) +(* finds a nearby (outward-rounded) Num.num_of_int with only prec_b significant bits *) let (round_outward: int -> Num.num -> Num.num) = fun prec_b a -> let b = abs_num a in let sign = if (a =/ b) then I else minus_num in - let throw_bits = Num.max_num (Int 0) ((num_exponent b)-/ (Int prec_b)) in - let twoexp = power_num (Int 2) throw_bits in + let throw_bits = Num.max_num (Num.num_of_int 0) ((num_exponent b)-/ (Num.num_of_int prec_b)) in + let twoexp = power_num (Num.num_of_int 2) throw_bits in (sign (ceiling_num (b // twoexp)))*/twoexp;; let (round_inward: int-> Num.num -> Num.num) = fun prec_b a -> let b = abs_num a in let sign = if (a=/b) then I else minus_num in - let throw_bits = Num.max_num (Int 0) ((num_exponent b)-/ (Int prec_b)) in - let twoexp = power_num (Int 2) throw_bits in + let throw_bits = Num.max_num (Num.num_of_int 0) ((num_exponent b)-/ (Num.num_of_int prec_b)) in + let twoexp = power_num (Num.num_of_int 2) throw_bits in (sign (floor_num (b // twoexp)))*/twoexp;; let round_rat bprec n = let b = abs_num n in let sign = if (b =/ n) then I else minus_num in - let powt = ((Int 2) **/ (Int bprec)) in + let powt = ((Num.num_of_int 2) **/ (Num.num_of_int bprec)) in sign ((round_outward bprec (Num.ceiling_num (b */ powt)))//powt);; let round_inward_rat bprec n = let b = abs_num n in let sign = if (b =/ n) then I else minus_num in - let powt = ((Int 2) **/ (Int bprec)) in + let powt = ((Num.num_of_int 2) **/ (Num.num_of_int bprec)) in sign ((round_inward bprec (Num.floor_num (b */ powt)))//powt);; let (round_outward_float: int -> float -> Num.num) = fun bprec f -> - if (f=0.0) then (Int 0) else + if (f=0.0) then (Num.num_of_int 0) else begin let b = abs_float f in let sign = if (f >= 0.0) then I else minus_num in let (x,n) = frexp b in let u = int_of_float( ceil (ldexp x bprec)) in - sign ((Int u)*/ ((Int 2) **/ (Int (n - bprec)))) + sign ((Num.num_of_int u)*/ ((Num.num_of_int 2) **/ (Num.num_of_int (n - bprec)))) end;; let (round_inward_float: int -> float -> Num.num) = fun bprec f -> - if (f=0.0) then (Int 0) else + if (f=0.0) then (Num.num_of_int 0) else begin (* avoid overflow on 30 bit integers *) let bprec = if (bprec > 25) then 25 else bprec in @@ -1157,7 +1157,7 @@ let (round_inward_float: int -> float -> Num.num) = let sign = if (f >= 0.0) then I else minus_num in let (x,n) = frexp b in let u = int_of_float( floor (ldexp x bprec)) in - sign ((Int u)*/ ((Int 2) **/ (Int (n - bprec)))) + sign ((Num.num_of_int u)*/ ((Num.num_of_int 2) **/ (Num.num_of_int (n - bprec)))) end;; (* ------------------------------------------------------------------ *) @@ -1626,7 +1626,7 @@ let is_comb_of t u = and such that abs (x - A/x ) < epsilon *) let rec heron_sqrt depth A x eps = - let half = (Int 1)//(Int 2) in + let half = (Num.num_of_int 1)//(Num.num_of_int 2) in if (depth <= 0) then raise (Failure "sqrt recursion depth exceeded") else if (Num.abs_num (x -/ (A//x) ) =/ A) then (A//x) else let x' = half */ (x +/ (A//x)) in @@ -1754,7 +1754,7 @@ let rec INTERVAL_OF_TERM bprec tm = let ez_rat = (ex_num +/ abs_num (f_num -/ (h_num*/ g_num)) +/ (abs_num h_num */ ey_num))//((abs_num g_num) -/ (ey_num)) in let ez_num = round_rat bprec (ez_rat) in - let _ = assert((ez_num >=/ (Int 0))) in + let _ = assert((ez_num >=/ (Num.num_of_int 0))) in let ez = mk_float ez_num in let hyp1 = a_int in let hyp2 = b_int in @@ -1782,11 +1782,11 @@ let rec INTERVAL_OF_TERM bprec tm = (* put in heron's formula *) let v_num1 = round_inward_float 25 (apprx_sqrt) in let v_num = round_inward_rat bprec - (heron_sqrt 10 fd_num v_num1 ((Int 2) **/ (Int (-bprec-4)))) in + (heron_sqrt 10 fd_num v_num1 ((Num.num_of_int 2) **/ (Num.num_of_int (-bprec-4)))) in let u_num1 = round_inward_float 25 (Pervasives.sqrt (float_of_num f_num)) in let u_num = round_inward_rat bprec - (heron_sqrt 10 f_num u_num1 ((Int 2) **/ (Int (-bprec-4)))) in + (heron_sqrt 10 f_num u_num1 ((Num.num_of_int 2) **/ (Num.num_of_int (-bprec-4)))) in let ey_num = round_rat bprec (abs_num (f_num -/ (u_num */ u_num))) in let ez_num = round_rat bprec ((ex_num +/ ey_num)//(u_num +/ v_num)) in let (v,u) = (mk_float v_num,mk_float u_num) in diff --git a/Jordan/misc_defs_and_lemmas.ml b/Jordan/misc_defs_and_lemmas.ml index af43e93e..0bf120b2 100644 --- a/Jordan/misc_defs_and_lemmas.ml +++ b/Jordan/misc_defs_and_lemmas.ml @@ -2243,8 +2243,8 @@ let PI_SER = prove_by_refinement( let SUC_EXPAND_CONV tm = let count = dest_numeral tm in let rec add_suc i r = - if (i <=/ (Int 0)) then r - else add_suc (i -/ (Int 1)) (mk_comb (`SUC`,r)) in + if (i <=/ (Num.num_of_int 0)) then r + else add_suc (i -/ (Num.num_of_int 1)) (mk_comb (`SUC`,r)) in let tm' = add_suc count `0` in REWRITE_RULE[] (ARITH_REWRITE_CONV[] (mk_eq (tm,tm')));; @@ -2266,7 +2266,7 @@ let PI_SERn n = (* abs(pi - u ) < e *) let recompute_pi bprec = let n = (bprec /4) in - let pi_ser = PI_SERn (mk_numeral (Int n)) in + let pi_ser = PI_SERn (mk_numeral (Num.num_of_int n)) in let _ = remove_real_constant `pi` in (add_real_constant pi_ser; INTERVAL_OF_TERM bprec `pi`);; diff --git a/Jordan/num_ext_gcd.ml b/Jordan/num_ext_gcd.ml index ffc5a715..28fca87a 100644 --- a/Jordan/num_ext_gcd.ml +++ b/Jordan/num_ext_gcd.ml @@ -136,37 +136,37 @@ let gcd_certificate = prove(`!a b g. ((? r s r' s' a' b'. then check the answer in HOL-light *) let gcd_num x1 x2 = let rec gcd_data (a1,b1,x1,a2,b2,x2) = - if (x1 < (Int 0)) then + if (x1 < (Num.num_of_int 0)) then gcd_data(minus_num a1,minus_num b1,minus_num x1,a2,b2,x2) - else if (x2 < (Int 0)) then gcd_data(a1,b1,x1,minus_num a2,minus_num + else if (x2 < (Num.num_of_int 0)) then gcd_data(a1,b1,x1,minus_num a2,minus_num b2,minus_num x2) - else if (x1 = (Int 0)) then (a2,b2,x2) + else if (x1 = (Num.num_of_int 0)) then (a2,b2,x2) else if (x1>x2) then gcd_data (a2,b2,x2,a1,b1,x1) else ( let r = (quo_num x2 x1) in gcd_data (a1,b1,x1,a2 -/ r*/ a1,b2 -/ r*/ b1, x2 -/ r*/ x1) ) in - gcd_data ((Int 1),(Int 0),x1,(Int 0),(Int 1),x2);; + gcd_data ((Num.num_of_int 1),(Num.num_of_int 0),x1,(Num.num_of_int 0),(Num.num_of_int 1),x2);; let gcd_num x1 x2 = let rec gcd_data (a1,b1,x1,a2,b2,x2) = - if (x1 < (Int 0)) then + if (x1 < (Num.num_of_int 0)) then gcd_data(minus_num a1,minus_num b1,minus_num x1,a2,b2,x2) - else if (x2 < (Int 0)) then gcd_data(a1,b1,x1,minus_num a2,minus_num + else if (x2 < (Num.num_of_int 0)) then gcd_data(a1,b1,x1,minus_num a2,minus_num b2,minus_num x2) - else if (x1 = (Int 0)) then (a2,b2,x2) + else if (x1 = (Num.num_of_int 0)) then (a2,b2,x2) else if (x1>x2) then gcd_data (a2,b2,x2,a1,b1,x1) else ( let r = (quo_num x2 x1) in gcd_data (a1,b1,x1,a2 -/ r*/ a1,b2 -/ r*/ b1, x2 -/ r*/ x1) ) in - gcd_data ((Int 1),(Int 0),x1,(Int 0),(Int 1),x2);; + gcd_data ((Num.num_of_int 1),(Num.num_of_int 0),x1,(Num.num_of_int 0),(Num.num_of_int 1),x2);; (* g = gcd, (a',b') = (a,b)/g, g +r1'*a+s1'*b = r1*a+s1*b *) let gcd_numdata a b = let a = abs_num a in let b = abs_num b in - let Z = Int 0 in + let Z = Num.num_of_int 0 in let (r,s,g) = gcd_num a b in let a' = if (g=Z) then Z else round_num(a//g) in let b' = if (g=Z) then Z else round_num(b//g) in diff --git a/Jordan/tactics_ext2.ml b/Jordan/tactics_ext2.ml index a8e18a79..71412f2b 100644 --- a/Jordan/tactics_ext2.ml +++ b/Jordan/tactics_ext2.ml @@ -351,11 +351,11 @@ let new_factor_order2 t1 t2 = let rec mon_sz tm = if is_var tm then - Int (Hashtbl.hash tm) + Num.num_of_int (Hashtbl.hash tm) else try let (a,b) = dest_binop `( *. )` tm in (mon_sz a) */ (mon_sz b) - with Failure _ -> Int 1;; + with Failure _ -> Num.num_of_int 1;; let rec new_summand_order t1 t2 = try let t1v = fst(dest_binop `( +. )` t1) in diff --git a/LP_arith/lp_arith.ml b/LP_arith/lp_arith.ml index 76f3fcd9..b9aa62b0 100644 --- a/LP_arith/lp_arith.ml +++ b/LP_arith/lp_arith.ml @@ -16,14 +16,14 @@ let lin_of_hol = and lin_add = combine (+/) (fun x -> x =/ num_0) in let rec lin_of_hol tm = if tm = zero_tm then undefined - else if not (is_comb tm) then (tm |=> Int 1) + else if not (is_comb tm) then (tm |=> Num.num_of_int 1) else if is_ratconst tm then (one_tm |=> rat_of_term tm) else let lop,r = dest_comb tm in - if not (is_comb lop) then (tm |=> Int 1) else + if not (is_comb lop) then (tm |=> Num.num_of_int 1) else let op,l = dest_comb lop in if op = add_tm then lin_add (lin_of_hol l) (lin_of_hol r) else if op = mul_tm && is_ratconst l then (r |=> rat_of_term l) - else (tm |=> Int 1) in + else (tm |=> Num.num_of_int 1) in lin_of_hol;; let words s = @@ -115,7 +115,7 @@ let LP_PROVER = and lt_pols = map (lin_of_hol o lhand o concl) lt in let aliens = filter is_alien (itlist (union o dom) (eq_pols @ le_pols @ lt_pols) []) in - let le_pols' = le_pols @ map (fun v -> (v |=> Int 1)) aliens in + let le_pols' = le_pols @ map (fun v -> (v |=> Num.num_of_int 1)) aliens in let proof = lp_prover(eq_pols,le_pols',lt_pols) in let le' = le @ map (fun a -> INST [rand a,n_tm] pth) aliens in translator (eq,le',lt) proof;; diff --git a/Library/binomial.ml b/Library/binomial.ml index 7ff7149b..8320fe40 100644 --- a/Library/binomial.ml +++ b/Library/binomial.ml @@ -346,16 +346,16 @@ let NUM_BINOM_CONV = MP_CONV NUM_LT_CONV th else if n =/ k then INST [mk_numeral n,n_tm] pth_1 - else if Int 2 */ k - if dest_numeral a < power_num (Int 2) (dest_finty i) + if dest_numeral a < power_num (Num.num_of_int 2) (dest_finty i) then a else failwith "numeral out of range" | a -> a in @@ -567,7 +567,7 @@ let bm_build_tree' = match r with | None -> Leaf_dt eqth | Some(_,i) -> - let ii = mk_numeral (Int i) in + let ii = mk_numeral (Num.num_of_int i) in let bit = bit_tm ii e in let skip_th sc th = let sm, rs' = dest_comb (lhs (concl th)) in @@ -772,11 +772,11 @@ let rec bitpat_matches p i = match p with | Comb(Comb(Const("CONSPAT",_),p),a) -> let N = dest_word_ty (type_of a) in let n = Num.int_of_num (dest_finty N) in - let m = power_num (Int 2) (Int n) in + let m = power_num (Num.num_of_int 2) (Num.num_of_int n) in let i' = quo_num i m and a' = mod_num i m in let r = match a with - | Comb(Const("word1",_),Const("T",_)) -> if a' = Int 1 then None else Some 0 - | Comb(Const("word1",_),Const("F",_)) -> if a' = Int 0 then None else Some 0 + | Comb(Const("word1",_),Const("T",_)) -> if a' = Num.num_of_int 1 then None else Some 0 + | Comb(Const("word1",_),Const("F",_)) -> if a' = Num.num_of_int 0 then None else Some 0 | Comb(Const("word1",_),Var(_,_)) -> None | Comb(Const("word",_),n) -> let n' = dest_numeral n in @@ -791,7 +791,7 @@ let rec bitpat_matches p i = match p with match bitpat_matches p i' with | Some j -> Some (j + n) | None -> None) -| Const("NILPAT",_) -> if i = Int 0 then None else +| Const("NILPAT",_) -> if i = Num.num_of_int 0 then None else failwith "bitpat_matches: out of range" | Abs(_,c) -> bitpat_matches c i | Comb(Const("?",_),c) -> bitpat_matches c i @@ -851,7 +851,7 @@ let inst_bitpat_numeral = | Comb(Comb(Const("CONSPAT",_),p),a) -> let N = dest_word_ty (type_of a) in let n = Num.int_of_num (dest_finty N) in - let m = power_num (Int 2) (Int n) in + let m = power_num (Num.num_of_int 2) (Num.num_of_int n) in let i' = quo_num i m and a' = mod_num i m in let ls, th' = go i' p in let p',x = dest_comb (concl th') in let p' = rand p' in @@ -860,11 +860,11 @@ let inst_bitpat_numeral = let ls, b = match a with | Const("T",_) -> ls,true | Const("F",_) -> ls,false - | Var(_,_) -> let b = a' = Int 1 in ((if b then T else F),a)::ls, b + | Var(_,_) -> let b = a' = Num.num_of_int 1 in ((if b then T else F),a)::ls, b | _ -> failwith "inst_bitpat_numeral" in ls, PROVE_HYP th' ( if b then INST [x,ex; p',ep] w1T - else if i = Int 0 then INST [p',ep] w1F0 + else if i = Num.num_of_int 0 then INST [p',ep] w1F0 else INST [x,ex; p',ep] w1F) | _ -> let thd = dim N in @@ -936,7 +936,7 @@ let BITMATCH_CONV = (match snd (snd (get_dt a tr)) with | th::_ -> let ps = hd (hyp th) in - let ls, th' = inst_bitpat_numeral ps (Int n) in + let ls, th' = inst_bitpat_numeral ps (Num.num_of_int n) in PROVE_HYP th' (INST ls th) | _ -> failwith "BITMATCH_CONV") | _ -> failwith "BITMATCH_CONV";; @@ -992,7 +992,7 @@ let BITMATCH_SIMP_CONV asl = | Some b, Some c, None when b != c -> r := Some i | _ -> ()) a; let i = match !r with - | Some i -> mk_numeral (Int i) + | Some i -> mk_numeral (Num.num_of_int i) | _ -> fail () in let th' = PROVE_HYP th (PROVE_HYP (pat_to_bit true i h) (bm_skip_clause (pat_to_bit false i) tm)) in @@ -1141,7 +1141,7 @@ let bm_seq_numeral = function | Comb(Comb(Const("_SEQPATTERN",_),c),cs') -> let ps = hd (hyp th) in let pats = Array.init sz (fun i -> try - Some (bm_skip_clause (pat_to_bit false (mk_numeral (Int i))) tm) + Some (bm_skip_clause (pat_to_bit false (mk_numeral (Num.num_of_int i))) tm) with Failure _ -> None) in let f = mk_fun cs' in fun n e' -> diff --git a/Library/calc_real.ml b/Library/calc_real.ml index 8619ff8e..5099bb4f 100644 --- a/Library/calc_real.ml +++ b/Library/calc_real.ml @@ -134,9 +134,9 @@ let REAL_NDIV_LEMMA3 = prove let log2 = (*** least p >= 0 with x <= 2^p ***) let rec log2 x y = - if x log2 (x -/ Int 1) (Int 0);; + if x log2 (x -/ Num.num_of_int 1) (Num.num_of_int 0);; (* ------------------------------------------------------------------------- *) (* Theorems justifying the steps. *) @@ -1756,17 +1756,17 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = let ndiv x y = let q = quo_num x y in let r = x -/ (q */ y) in - if le_num (abs_num(Int 2 */ r)) (abs_num y) then q - else if le_num (abs_num(Int 2 */ (r -/ y))) (abs_num y) then q +/ Int 1 - else if le_num (abs_num(Int 2 */ (r +/ y))) (abs_num y) then q -/ Int 1 + if le_num (abs_num(Num.num_of_int 2 */ r)) (abs_num y) then q + else if le_num (abs_num(Num.num_of_int 2 */ (r -/ y))) (abs_num y) then q +/ Num.num_of_int 1 + else if le_num (abs_num(Num.num_of_int 2 */ (r +/ y))) (abs_num y) then q -/ Num.num_of_int 1 else let s = (string_of_num x)^" and "^(string_of_num y) in failwith ("ndiv: "^s) in - let raw_wrap (f:num->num) = (ref(Int(-1),Int 0),f) in + let raw_wrap (f:num->num) = (ref(Num.num_of_int(-1),Num.num_of_int 0),f) in let raw_eval(r,(f:num->num)) n = let (n0,y0) = !r in - if le_num n n0 then ndiv y0 (power_num (Int 2) (n0 -/ n)) + if le_num n n0 then ndiv y0 (power_num (Num.num_of_int 2) (n0 -/ n)) else let y = f n in (r := (n,y); y) in let thm_eval = @@ -1777,7 +1777,7 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = if le_num n n0 then if n =/ n0 then y0th else let th1 = NUM_SUC_CONV - (mk_comb(SUC_tm,mk_numeral(n0 -/ (n +/ Int 1)))) in + (mk_comb(SUC_tm,mk_numeral(n0 -/ (n +/ Num.num_of_int 1)))) in let th2 = MATCH_MP REALCALC_DOWNGRADE th1 in let th3 = NUM_ADD_CONV(mk_add(mk_numeral(n)) (mk_numeral(n0 -/ n))) in let th4 = MATCH_MP th2 th3 in @@ -1790,7 +1790,7 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = let tm5f,tm5g = dest_comb(rand tm5d) in let tm5h = rand(rand tm5f) in let bin = mk_realintconst - (ndiv (dest_realintconst tm5e) (power_num (Int 2) (dest_numeral tm5h))) in + (ndiv (dest_realintconst tm5e) (power_num (Num.num_of_int 2) (dest_numeral tm5h))) in let th7 = AP_TERM (rator(rand tm5f)) th1 in let th8 = GEN_REWRITE_RULE LAND_CONV [CONJUNCT2 real_pow] th7 in let th9 = SYM(GEN_REWRITE_RULE (LAND_CONV o RAND_CONV) [th6] th8) in @@ -1806,24 +1806,24 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = MATCH_MP th5 (EQT_ELIM th18) else let yth = f n in (r := (n,yth); yth) in - let thm_wrap (f:num->thm) = (ref(Int(-1),TRUTH),f) in + let thm_wrap (f:num->thm) = (ref(Num.num_of_int(-1),TRUTH),f) in let find_msd = let rec find_msd n f = - if Int 1 real` @@ -1836,18 +1836,18 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = and x_tm = `x:real` in let rec calculate_m acc i r = if acc >=/ r then i else - let i' = i +/ Int 1 in + let i' = i +/ Num.num_of_int 1 in calculate_m (i' */ acc) i' r in let calculate_exp_sequence = let rec calculate_exp_sequence p2 s i = - if i let p2 = power_num (Int 2) p in - rev(calculate_exp_sequence p2 s (m -/ Int 1)) in + fun p s m -> let p2 = power_num (Num.num_of_int 2) p in + rev(calculate_exp_sequence p2 s (m -/ Num.num_of_int 1)) in let pth = prove (`abs(x) <= &1 ==> abs(s - &2 pow p * x) < &1 ==> @@ -1866,27 +1866,27 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = ONCE_REWRITE_RULE[prove(`0 + n = n`,REWRITE_TAC[ADD_CLAUSES])] in fun (fn1,fn2) -> let raw_fn n = - let m = calculate_m (Int 1) (Int 0) - (Int 3 */ (power_num (Int 2) (n +/ Int 2))) in - let e = log2 (Int 2 */ m) in - let p = n +/ e +/ Int 2 in + let m = calculate_m (Num.num_of_int 1) (Num.num_of_int 0) + (Num.num_of_int 3 */ (power_num (Num.num_of_int 2) (n +/ Num.num_of_int 2))) in + let e = log2 (Num.num_of_int 2 */ m) in + let p = n +/ e +/ Num.num_of_int 2 in let s = raw_eval fn1 p in let seq = calculate_exp_sequence p s m in - let u0 = itlist (+/) seq (Int 0) in - ndiv u0 (power_num (Int 2) (e +/ Int 2)) + let u0 = itlist (+/) seq (Num.num_of_int 0) in + ndiv u0 (power_num (Num.num_of_int 2) (e +/ Num.num_of_int 2)) and thm_fn n = - let m = calculate_m (Int 1) (Int 0) - (Int 3 */ (power_num (Int 2) (n +/ Int 2))) in - let e = log2 (Int 2 */ m) in - let p = n +/ e +/ Int 2 in + let m = calculate_m (Num.num_of_int 1) (Num.num_of_int 0) + (Num.num_of_int 3 */ (power_num (Num.num_of_int 2) (n +/ Num.num_of_int 2))) in + let e = log2 (Num.num_of_int 2 */ m) in + let p = n +/ e +/ Num.num_of_int 2 in let sth = thm_eval fn2 p in let tm1 = rand(lhand(concl sth)) in let s_num = lhand tm1 in let x_num = rand(rand tm1) in let s = dest_realintconst s_num in let seq = calculate_exp_sequence p s m in - let u0 = itlist (+/) seq (Int 0) in - let u = ndiv u0 (power_num (Int 2) (e +/ Int 2)) in + let u0 = itlist (+/) seq (Num.num_of_int 0) in + let u = ndiv u0 (power_num (Num.num_of_int 2) (e +/ Num.num_of_int 2)) in let m_num = mk_numeral m and n_num = mk_numeral n and e_num = mk_numeral e @@ -1923,18 +1923,18 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = and k_tm = `k:num` and x_tm = `x:real` in let rec calculate_m acc k2 m r = - if acc */ (m +/ Int 1) >=/ r then m else - calculate_m (k2 */ acc) k2 (m +/ Int 1) r in + if acc */ (m +/ Num.num_of_int 1) >=/ r then m else + calculate_m (k2 */ acc) k2 (m +/ Num.num_of_int 1) r in let calculate_ln_sequence = let rec calculate_ln_sequence p2 s i = - if i let p2 = power_num (Int 2) p in - rev(calculate_ln_sequence p2 s (m -/ Int 1)) in + fun p s m -> let p2 = power_num (Num.num_of_int 2) p in + rev(calculate_ln_sequence p2 s (m -/ Num.num_of_int 1)) in let pth = prove (`&0 <= x /\ x <= inv(&2 pow k) ==> abs(s - &2 pow p * x) < &1 ==> @@ -1961,30 +1961,30 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = fun (fn1,fn2) -> let raw_fn n = let k = find_ubound fn1 in - if k isolate_sqrt (Int 0,n) n in + fun n -> isolate_sqrt (Num.num_of_int 0,n) n in let MATCH_pth = MATCH_MP REALCALC_SQRT in let b_tm = `b:real` in let PROVE_1_LE_SQRT = @@ -2041,7 +2041,7 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = with Failure _ -> failwith "Need root body >= &1" in fun (fn1,fn2) -> let raw_fn n = - num_sqrt(power_num (Int 2) n */ raw_eval fn1 n) + num_sqrt(power_num (Num.num_of_int 2) n */ raw_eval fn1 n) and thm_fn n = let th1 = MATCH_pth(thm_eval fn2 n) in let th2 = MP th1 (PROVE_1_LE_SQRT(lhand(concl th1))) in @@ -2057,9 +2057,9 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = if is_ratconst tm then let x = rat_of_term tm in let raw_fn acc = - floor_num ((power_num (Int 2) acc) */ x) + floor_num ((power_num (Num.num_of_int 2) acc) */ x) and thm_fn acc = - let a = floor_num ((power_num (Int 2) acc) */ x) in + let a = floor_num ((power_num (Num.num_of_int 2) acc) */ x) in let atm = mk_realintconst a in let rtm = mk_comb(mk_comb(mul_tm,mk_comb(pow2_tm,mk_numeral acc)),tm) in let btm = mk_comb(abs_tm,mk_comb(mk_comb(sub_tm,atm),rtm)) in @@ -2091,25 +2091,25 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = REALCALC_SQRT_CONV(REALCALC_CONV r) else if lop = inv_tm then let rfn,tfn = REALCALC_CONV r in - let x0 = raw_eval rfn (Int 0) in + let x0 = raw_eval rfn (Num.num_of_int 0) in let ax0 = abs_num x0 in - let r = log2(ax0) -/ Int 1 in + let r = log2(ax0) -/ Num.num_of_int 1 in let get_ek(acc) = - if r < Int 0 then + if r < Num.num_of_int 0 then let p = find_msd rfn in - let e = acc +/ p +/ Int 1 in + let e = acc +/ p +/ Num.num_of_int 1 in let k = e +/ p in e,k else - let k = let k0 = acc +/ Int 1 -/ (Int 2 */ r) in - if k0 )`,(>/); `(>=)`,(>=/); `(=):real->real->bool`,(=/)] in let rec find_n rfn1 rfn2 n = - if n >/ Int 1000 then + if n >/ Num.num_of_int 1000 then failwith "realcalc_rel_conv: too close to discriminate" else - if abs_num(raw_eval rfn1 n -/ raw_eval rfn2 n) >=/ Int 4 then n - else find_n rfn1 rfn2 (n +/ Int 1) in + if abs_num(raw_eval rfn1 n -/ raw_eval rfn2 n) >=/ Num.num_of_int 4 then n + else find_n rfn1 rfn2 (n +/ Num.num_of_int 1) in fun tm -> let lop,r = dest_comb tm in let op,l = dest_comb lop in @@ -2265,7 +2265,7 @@ let realcalc_rel_conv = with Failure _ -> failwith "realcalc_rel_conv: unknown operator" in let rfn1,tfn1 = REALCALC_CONV l and rfn2,tfn2 = REALCALC_CONV r in - let n = find_n rfn1 rfn2 (Int 1) in + let n = find_n rfn1 rfn2 (Num.num_of_int 1) in pop (raw_eval rfn1 n) (raw_eval rfn2 n);; let REALCALC_REL_CONV = @@ -2274,10 +2274,10 @@ let REALCALC_REL_CONV = `(>)`,REALCALC_GT; `(>=)`,REALCALC_GE; `(=):real->real->bool`,REALCALC_EQ] in let rec find_n rfn1 rfn2 n = - if n >/ Int 1000 then + if n >/ Num.num_of_int 1000 then failwith "realcalc_rel_conv: too close to discriminate" else - if abs_num(raw_eval rfn1 n -/ raw_eval rfn2 n) >=/ Int 4 then n - else find_n rfn1 rfn2 (n +/ Int 1) in + if abs_num(raw_eval rfn1 n -/ raw_eval rfn2 n) >=/ Num.num_of_int 4 then n + else find_n rfn1 rfn2 (n +/ Num.num_of_int 1) in fun tm -> let lop,r = dest_comb tm in let op,l = dest_comb lop in @@ -2285,7 +2285,7 @@ let REALCALC_REL_CONV = with Failure _ -> failwith "realcalc_rel_conv: unknown operator" in let rfn1,tfn1 = REALCALC_CONV l and rfn2,tfn2 = REALCALC_CONV r in - let n = find_n rfn1 rfn2 (Int 1) in + let n = find_n rfn1 rfn2 (Num.num_of_int 1) in let th1 = thm_eval tfn1 n and th2 = thm_eval tfn2 n in let th3 = MATCH_MP pth (CONJ th1 th2) in diff --git a/Library/pocklington.ml b/Library/pocklington.ml index 5607a11e..539e1fdd 100755 --- a/Library/pocklington.ml +++ b/Library/pocklington.ml @@ -7,9 +7,9 @@ needs "Library/prime.ml";; prioritize_num();; -let num_0 = Int 0;; -let num_1 = Int 1;; -let num_2 = Int 2;; +let num_0 = Num.num_of_int 0;; +let num_1 = Num.num_of_int 1;; +let num_2 = Num.num_of_int 2;; (* ------------------------------------------------------------------------- *) (* Mostly for compatibility. Should eliminate this eventually. *) @@ -846,7 +846,7 @@ let INVERSE_MOD_INVERSION = prove let INVERSE_MOD_CONV = let rec gcdex(m,n) = if n let p = dest_numeral tm in - if p =/ Int 0 then EQF_INTRO PRIME_0 - else if p =/ Int 1 then EQF_INTRO PRIME_1 else + if p =/ Num.num_of_int 0 then EQF_INTRO PRIME_0 + else if p =/ Num.num_of_int 1 then EQF_INTRO PRIME_1 else let pfact = multifactor p in if length pfact = 1 then (remark ("proving that " ^ string_of_num p ^ " is prime"); @@ -973,9 +973,9 @@ time PRIME_TEST `65536`;; time PRIME_TEST `65537`;; -time PROVE_PRIMEFACT (Int 222);; +time PROVE_PRIMEFACT (Num.num_of_int 222);; -time PROVE_PRIMEFACT (Int 151);; +time PROVE_PRIMEFACT (Num.num_of_int 151);; (* ------------------------------------------------------------------------- *) (* The "Landau trick" in Erdos's proof of Chebyshev-Bertrand theorem. *) diff --git a/Library/prime.ml b/Library/prime.ml index a8231a42..3b51ddb9 100755 --- a/Library/prime.ml +++ b/Library/prime.ml @@ -2383,7 +2383,7 @@ let COPRIME_CONV = and x_tm = `x:num` and y_tm = `y:num` and d_tm = `d:num` and coprime_tm = `coprime` in let rec bezout (m,n) = - if m =/ Int 0 then (Int 0,Int 1) else if n =/ Int 0 then (Int 1,Int 0) + if m =/ Num.num_of_int 0 then (Num.num_of_int 0,Num.num_of_int 1) else if n =/ Num.num_of_int 0 then (Num.num_of_int 1,Num.num_of_int 0) else if m <=/ n then let q = quo_num n m and r = mod_num n m in let (x,y) = bezout(m,r) in @@ -2394,12 +2394,12 @@ let COPRIME_CONV = if pop <> coprime_tm then failwith "COPRIME_CONV" else let l,r = dest_pair ptm in let m = dest_numeral l and n = dest_numeral r in - if m =/ Int 0 && n =/ Int 0 then pth_oo else + if m =/ Num.num_of_int 0 && n =/ Num.num_of_int 0 then pth_oo else let (x,y) = bezout(m,n) in let d = x */ m +/ y */ n in let th = - if d =/ Int 1 then - if x >/ Int 0 then + if d =/ Num.num_of_int 1 then + if x >/ Num.num_of_int 0 then INST [l,m_tm; r,n_tm; mk_numeral x,x_tm; mk_numeral(minus_num y),y_tm] pth_yes_l else @@ -2430,7 +2430,7 @@ let GCD_CONV = MESON_TAC[pth1; GCD_SYM]) in let gcd_tm = `gcd` in let rec bezout (m,n) = - if m =/ Int 0 then (Int 0,Int 1) else if n =/ Int 0 then (Int 1,Int 0) + if m =/ Num.num_of_int 0 then (Num.num_of_int 0,Num.num_of_int 1) else if n =/ Num.num_of_int 0 then (Num.num_of_int 1,Num.num_of_int 0) else if m <=/ n then let q = quo_num n m and r = mod_num n m in let (x,y) = bezout(m,r) in @@ -2440,7 +2440,7 @@ let GCD_CONV = if gt <> gcd_tm then failwith "GCD_CONV" else let mtm,ntm = dest_pair lr in let m = dest_numeral mtm and n = dest_numeral ntm in - if m =/ Int 0 && n =/ Int 0 then pth0 else + if m =/ Num.num_of_int 0 && n =/ Num.num_of_int 0 then pth0 else let x0,y0 = bezout(m,n) in let x = abs_num x0 and y = abs_num y0 in let xtm = mk_numeral x and ytm = mk_numeral y in diff --git a/Library/words.ml b/Library/words.ml index 500b28a0..a7fffbbd 100644 --- a/Library/words.ml +++ b/Library/words.ml @@ -7861,7 +7861,7 @@ let WORDIFY_CONV = let log2 = let rec log2 n m i = if n Int(log2 (abs_num n) num_1 0) in + fun n -> Num.num_of_int(log2 (abs_num n) num_1 0) in let rec conv tm = match tm with Comb(Const("bitval",_),_) -> diff --git a/Multivariate/vectors.ml b/Multivariate/vectors.ml index b9027213..baed731d 100644 --- a/Multivariate/vectors.ml +++ b/Multivariate/vectors.ml @@ -721,12 +721,12 @@ let NORM_ARITH = find_normedterms l (find_normedterms r acc) | Comb(Comb(Const("real_mul",_),c),n) -> if not (is_ratconst c) then acc else - augment_norm (rat_of_term c >=/ Int 0) n acc + augment_norm (rat_of_term c >=/ Num.num_of_int 0) n acc | _ -> augment_norm true tm acc in find_normedterms in let lincomb_neg t = mapf minus_num t in - let lincomb_cmul c t = if c =/ Int 0 then undefined else mapf (( */ ) c) t in - let lincomb_add l r = combine (+/) (fun x -> x =/ Int 0) l r in + let lincomb_cmul c t = if c =/ Num.num_of_int 0 then undefined else mapf (( */ ) c) t in + let lincomb_add l r = combine (+/) (fun x -> x =/ Num.num_of_int 0) l r in let lincomb_sub l r = lincomb_add l (lincomb_neg r) in let lincomb_eq l r = lincomb_sub l r = undefined in let rec vector_lincomb tm = @@ -739,9 +739,9 @@ let NORM_ARITH = lincomb_cmul (rat_of_term l) (vector_lincomb r) | Comb(Const("vector_neg",_),t) -> lincomb_neg (vector_lincomb t) - | Comb(Const("vec",_),n) when is_numeral n && dest_numeral n =/ Int 0 -> + | Comb(Const("vec",_),n) when is_numeral n && dest_numeral n =/ Num.num_of_int 0 -> undefined - | _ -> (tm |=> Int 1) in + | _ -> (tm |=> Num.num_of_int 1) in let vector_lincombs tms = itlist (fun t fns -> if can (assoc t) fns then fns else @@ -753,7 +753,7 @@ let NORM_ARITH = match tm with Comb(Comb(Const("real_add",_),l),r) -> BINOP_CONV (replacenegnorms fn) tm - | Comb(Comb(Const("real_mul",_),c),n) when rat_of_term c + | Comb(Comb(Const("real_mul",_),c),n) when rat_of_term c RAND_CONV fn tm | _ -> REFL tm in let flip v eq = @@ -764,14 +764,14 @@ let NORM_ARITH = | (a::t) -> let res = allsubsets t in map (fun b -> a::b) res @ res in let evaluate env lin = - foldr (fun x c s -> s +/ c */ apply env x) lin (Int 0) in + foldr (fun x c s -> s +/ c */ apply env x) lin (Num.num_of_int 0) in let rec solve (vs,eqs) = match (vs,eqs) with - [],[] -> (0 |=> Int 1) + [],[] -> (0 |=> Num.num_of_int 1) | _,eq::oeqs -> let v = hd(intersect vs (dom eq)) in let c = apply eq v in - let vdef = lincomb_cmul (Int(-1) // c) eq in + let vdef = lincomb_cmul (Num.num_of_int(-1) // c) eq in let eliminate eqn = if not(defined eqn v) then eqn else lincomb_add (lincomb_cmul (apply eqn v) vdef) eqn in @@ -786,9 +786,9 @@ let NORM_ARITH = let vertices vs eqs = let vertex cmb = let soln = solve(vs,cmb) in - map (fun v -> tryapplyd soln v (Int 0)) vs in + map (fun v -> tryapplyd soln v (Num.num_of_int 0)) vs in let rawvs = mapfilter vertex (combinations (length vs) eqs) in - let unset = filter (forall (fun c -> c >=/ Int 0)) rawvs in + let unset = filter (forall (fun c -> c >=/ Num.num_of_int 0)) rawvs in itlist (insert' (forall2 (=/))) unset [] in let subsumes l m = forall2 (fun x y -> abs_num x <=/ abs_num y) l m in let rec subsume todo dun = @@ -895,7 +895,7 @@ let NORM_ARITH = (APPLY_pth2 THENC VECTOR_CANON_CONV) tm | Comb(Const("vector_neg",_),t) -> (APPLY_pth3 THENC VECTOR_CANON_CONV) tm - | Comb(Const("vec",_),n) when is_numeral n && dest_numeral n =/ Int 0 -> + | Comb(Const("vec",_),n) when is_numeral n && dest_numeral n =/ Num.num_of_int 0 -> REFL tm | _ -> APPLY_pth1 tm in fun tm -> @@ -923,21 +923,21 @@ let NORM_ARITH = itlist (fun (f,v) g -> if defined f x then (v |-> apply f x) g else g) srccombs inp in let equations = map coefficients vvs - and inequalities = map (fun n -> (n |=> Int 1)) nvs in + and inequalities = map (fun n -> (n |=> Num.num_of_int 1)) nvs in let plausiblevertices f = let flippedequations = map (itlist flip f) equations in let constraints = flippedequations @ inequalities in let rawverts = vertices nvs constraints in let check_solution v = - let f = itlist2 (|->) nvs v (0 |=> Int 1) in - forall (fun e -> evaluate f e =/ Int 0) flippedequations in + let f = itlist2 (|->) nvs v (0 |=> Num.num_of_int 1) in + forall (fun e -> evaluate f e =/ Num.num_of_int 0) flippedequations in let goodverts = filter check_solution rawverts in let signfixups = map (fun n -> if mem n f then -1 else 1) nvs in - map (map2 (fun s c -> Int s */ c) signfixups) goodverts in + map (map2 (fun s c -> Num.num_of_int s */ c) signfixups) goodverts in let allverts = itlist (@) (map plausiblevertices (allsubsets nvs)) [] in subsume allverts [] in let compute_ineq v = - let ths = mapfilter (fun (v,t) -> if v =/ Int 0 then fail() + let ths = mapfilter (fun (v,t) -> if v =/ Num.num_of_int 0 then fail() else NORM_CMUL_RULE v t) (zip v nubs) in INEQUALITY_CANON_RULE (end_itlist NORM_ADD_RULE ths) in diff --git a/Rqe/poly_ext.ml b/Rqe/poly_ext.ml index 5fb7ace2..e6d9099c 100644 --- a/Rqe/poly_ext.ml +++ b/Rqe/poly_ext.ml @@ -515,7 +515,7 @@ let rec headconst p = let MONIC_CONV = let mul_tm = `( * ):real->real->real` in fun vars p -> - let c = Int 1 // headconst p in + let c = Num.num_of_int 1 // headconst p in POLY_MUL_CONV vars (mk_comb(mk_comb(mul_tm,term_of_rat c),p));; (* ------------------------------------------------------------------------- *) @@ -566,7 +566,7 @@ let PDIVIDE = (* ------------------------------------------------------------------------- *) let SIGN_CONST = - let zero = Int 0 + let zero = Num.num_of_int 0 and zero_tm = `&0` and eq_tm = `(=):real->real->bool` and gt_tm = `(>):real->real->bool` diff --git a/Rqe/signs.ml b/Rqe/signs.ml index ee6b2c8e..b5b1d5a6 100644 --- a/Rqe/signs.ml +++ b/Rqe/signs.ml @@ -36,7 +36,7 @@ let FINDSIGN = let p' = rand(concl mth) in let pth = find (fun th -> lhand(concl th) = p') sgns in let c = lhand(lhand(concl mth)) in - let c' = term_of_rat(Int 1 // rat_of_term c) in + let c' = term_of_rat(Num.num_of_int 1 // rat_of_term c) in let sth = SIGN_CONST c' in let rel_c = funpow 2 rator (concl sth) in let rel_p = funpow 2 rator (concl pth) in diff --git a/Rqe/simplify.ml b/Rqe/simplify.ml index 502e8656..0ca3658d 100644 --- a/Rqe/simplify.ml +++ b/Rqe/simplify.ml @@ -135,7 +135,7 @@ SIMPLIFY_CONV `T /\ T \/ F` let operations = ["=",(=/); "<",(",(>/); "<=",(<=/); ">=",(>=/); - "divides",(fun x y -> mod_num y x =/ Int 0)];; + "divides",(fun x y -> mod_num y x =/ Num.num_of_int 0)];; let evalc_atom at = match at with diff --git a/Tutorial/Real_analysis.ml b/Tutorial/Real_analysis.ml index 830d77d7..5c0fea44 100644 --- a/Tutorial/Real_analysis.ml +++ b/Tutorial/Real_analysis.ml @@ -31,7 +31,7 @@ let NUM_ADD2_CONV = let add_tm = `(+):num->num->num` and two_tm = `2` in fun tm -> - let m = mk_numeral(dest_numeral tm -/ Int 2) in + let m = mk_numeral(dest_numeral tm -/ Num.num_of_int 2) in let tm' = mk_comb(mk_comb(add_tm,m),two_tm) in SYM(NUM_ADD_CONV tm');; diff --git a/Tutorial/all.ml b/Tutorial/all.ml index 27d58487..4da98adb 100644 --- a/Tutorial/all.ml +++ b/Tutorial/all.ml @@ -1140,7 +1140,7 @@ let NUM_ADD2_CONV = let add_tm = `(+):num->num->num` and two_tm = `2` in fun tm -> - let m = mk_numeral(dest_numeral tm -/ Int 2) in + let m = mk_numeral(dest_numeral tm -/ Num.num_of_int 2) in let tm' = mk_comb(mk_comb(add_tm,m),two_tm) in SYM(NUM_ADD_CONV tm');; diff --git a/calc_num.ml b/calc_num.ml index 6c0481c9..c7f6268f 100644 --- a/calc_num.ml +++ b/calc_num.ml @@ -227,7 +227,7 @@ let NUM_SUC_CONV,NUM_ADD_CONV,NUM_MULT_CONV,NUM_EXP_CONV, and mul_tm = rator(rator(rand(snd(strip_forall(concl EXP_2))))) and exp_tm = rator(rator(lhand(snd(strip_forall(concl EXP_2))))) and eq_tm = rator(rator(concl TWO)) in - let num_0 = Int 0 and num_1 = Int 1 and num_2 = Int 2 in + let num_0 = Num.num_of_int 0 and num_1 = Num.num_of_int 1 and num_2 = Num.num_of_int 2 in let a_tm = mk_var("a",num_ty) and b_tm = mk_var("b",num_ty) and c_tm = mk_var("c",num_ty) @@ -1050,8 +1050,8 @@ let NUM_SUC_CONV,NUM_ADD_CONV,NUM_MULT_CONV,NUM_EXP_CONV, EQ_MP th1 th0 | (Comb(Const("BIT1",_),mtm),Comb(Const("BIT1",_),ntm)) -> if k <= 50 || l <= 50 || - Int k */ Int k <=/ Int l || - Int l */ Int l <= Int k then + Num.num_of_int k */ Num.num_of_int k <=/ Num.num_of_int l || + Num.num_of_int l */ Num.num_of_int l <= Num.num_of_int k then match (mtm,ntm) with (Comb(Const("BIT1",_),Comb(Const("BIT1",_),_)),_) -> let th1 = NUM_ADC_RULE zero_tm tm in @@ -1334,8 +1334,8 @@ let NUM_PRE_CONV = fun tm -> try let l,r = dest_comb tm in if not (l = pre) then fail() else let x = dest_numeral r in - if x =/ Int 0 then tth else - let tm' = mk_numeral (x -/ Int 1) in + if x =/ Num.num_of_int 0 then tth else + let tm' = mk_numeral (x -/ Num.num_of_int 1) in let th1 = NUM_SUC_CONV (mk_comb(suc,tm')) in MP (INST [tm',m; r,n] pth) th1 with Failure _ -> failwith "NUM_PRE_CONV";; @@ -1406,14 +1406,14 @@ let NUM_FACT_CONV = REWRITE_TAC[FACT]) and w = `w:num` and x = `x:num` and y = `y:num` and z = `z:num` in let mksuc n = - let n' = n -/ (Int 1) in + let n' = n -/ (Num.num_of_int 1) in NUM_SUC_CONV (mk_comb(suc,mk_numeral n')) in let rec NUM_FACT_CONV n = - if n =/ Int 0 then pth_0 else + if n =/ Num.num_of_int 0 then pth_0 else let th0 = mksuc n in let tmx = rand(lhand(concl th0)) in let tm0 = rand(concl th0) in - let th1 = NUM_FACT_CONV (n -/ Int 1) in + let th1 = NUM_FACT_CONV (n -/ Num.num_of_int 1) in let tm1 = rand(concl th1) in let th2 = NUM_MULT_CONV (mk_binop mul tm0 tm1) in let tm2 = rand(concl th2) in @@ -1484,8 +1484,8 @@ let NUM_REDUCE_TAC = CONV_TAC NUM_REDUCE_CONV;; let num_CONV = let SUC_tm = `SUC` in fun tm -> - let n = dest_numeral tm -/ Int 1 in - if n / Int 0 then x3n',y3n' + let x3n'',y3n'' = if y3n' >/ Num.num_of_int 0 then x3n',y3n' else minus_num x3n',minus_num y3n' in let x3' = mk_realintconst x3n'' and y3' = mk_realintconst y3n'' in let th0 = INST [x1',x1; y1',y1; x2',x2; y2',y2; x3',x3; y3',y3] pth in diff --git a/int.ml b/int.ml index 661e9a64..c752312a 100755 --- a/int.ml +++ b/int.ml @@ -1779,7 +1779,7 @@ let INT_DIV_CONV,INT_REM_CONV = and dtm = `(div)` and mtm = `(rem)` in let emod_num x y = let r = mod_num x y in - if r string_of_num (Int b) n;; + fun b n -> string_of_num (Num.num_of_int b) n;; let string_of_num_hex n = "0x" ^ string_of_num_nary 16 n;; @@ -820,9 +820,9 @@ let num_of_string = "c",12; "C",12; "d",13; "D",13; "e",14; "E",14; "f",15; "F",15] in let valof b s = - let v = Int(assoc s values) in + let v = Num.num_of_int(assoc s values) in if v failwith "num_of_string: no digits after base indicator" diff --git a/nums.ml b/nums.ml index 72dd9712..25875962 100644 --- a/nums.ml +++ b/nums.ml @@ -209,7 +209,7 @@ let BIT1_DEF = (* ------------------------------------------------------------------------- *) let mk_numeral = - let pow24 = pow2 24 and num_0 = Int 0 + let pow24 = pow2 24 and num_0 = Num.num_of_int 0 and zero_tm = mk_const("_0",[]) and BIT0_tm = mk_const("BIT0",[]) and BIT1_tm = mk_const("BIT1",[]) @@ -235,7 +235,7 @@ let mk_numeral = fun n -> if n true | _ -> false in let rec powerof10 n = - if abs_num n true @@ -333,7 +333,7 @@ let pp_print_term = let s_den = implode(tl(explode(string_of_num (n_den +/ (mod_num n_num n_den))))) in pp_print_string fmt - ("#"^s_num^(if n_den = Int 1 then "" else ".")^s_den) + ("#"^s_num^(if n_den = Num.num_of_int 1 then "" else ".")^s_den) with Failure _ -> try if s <> "_MATCH" || length args <> 2 then failwith "" else let cls = dest_clauses(hd(tl args)) in diff --git a/realarith.ml b/realarith.ml index e92d3f1c..951dc111 100644 --- a/realarith.ml +++ b/realarith.ml @@ -449,14 +449,14 @@ let REAL_LINEAR_PROVER = and mul_tm = `(*):real->real->real` in let rec lin_of_hol tm = if tm = zero_tm then undefined - else if not (is_comb tm) then (tm |=> Int 1) + else if not (is_comb tm) then (tm |=> Num.num_of_int 1) else if is_ratconst tm then (one_tm |=> rat_of_term tm) else let lop,r = dest_comb tm in - if not (is_comb lop) then (tm |=> Int 1) else + if not (is_comb lop) then (tm |=> Num.num_of_int 1) else let op,l = dest_comb lop in if op = add_tm then linear_add (lin_of_hol l) (lin_of_hol r) else if op = mul_tm && is_ratconst l then (r |=> rat_of_term l) - else (tm |=> Int 1) in + else (tm |=> Num.num_of_int 1) in lin_of_hol in let is_alien tm = match tm with @@ -480,8 +480,8 @@ let REAL_LINEAR_PROVER = let all_aliens = filter is_alien (itlist (union o dom) (eq_pols @ le_pols @ lt_pols) []) in let suc_aliens,aliens = partition is_suc_alien all_aliens in - let le_pols' = le_pols @ map (fun v -> (v |=> Int 1)) aliens in - let lt_pols' = lt_pols @ map (fun v -> (v |=> Int 1)) suc_aliens in + let le_pols' = le_pols @ map (fun v -> (v |=> Num.num_of_int 1)) aliens in + let lt_pols' = lt_pols @ map (fun v -> (v |=> Num.num_of_int 1)) suc_aliens in let _,proof = linear_prover(eq_pols,le_pols',lt_pols') in let le' = le @ map (fun a -> INST [rand a,n_tm] pth) aliens in let lt' = lt @ map (fun a -> INST [dest_suc_alien a,n_tm] pth_suc) suc_aliens in