Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* ========================================================================= *) (* From binary to decimal real numbers. *) (* *) (* Freek Wiedijk, University of Nijmegen *) (* ========================================================================= *) loadt "/opt/lib/hol-light/Examples/analysis.ml";; loadt "/opt/lib/hol-light/Examples/transc.ml";; loadt "/opt/lib/hol-light/Examples/calc_real.ml";; prioritize_real();; let LT_NE_ZERO = prove (`!n. 0 < n = ~(n = 0)`, ARITH_TAC);; let REAL_LT_TWO = prove (`&0 < &2`, REAL_ARITH_TAC);; let REAL_ABS_MUL_NUM = prove (`!n x. &n * abs(x) = abs(&n * x)`, REPEAT GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM REAL_ABS_NUM] THEN REWRITE_TAC[REAL_ABS_MUL]);; let BASECHANGE_LEMMA = prove (`!p q m n a b x. 0 < p /\ 0 < q /\ 2*(q EXP n)*a <= 2*(p EXP m)*b + p EXP m /\ 2*(p EXP m)*b <= 2*(q EXP n)*a + p EXP m /\ 2*(q EXP n) <= p EXP m /\ abs(&a - (&p pow m)*x) < &1 ==> abs(&b - (&q pow n)*x) < &1`, REPEAT STRIP_TAC THEN SUBGOAL_THEN `0 < p EXP m` ASSUME_TAC THENL [REWRITE_TAC[EXP_LT_0] THEN ASM_REWRITE_TAC[GSYM LT_NE_ZERO]; ALL_TAC] THEN SUBGOAL_THEN `0 < q EXP n` ASSUME_TAC THENL [REWRITE_TAC[EXP_LT_0] THEN ASM_REWRITE_TAC[GSYM LT_NE_ZERO]; ALL_TAC] THEN SUBGOAL_THEN `&0 < &p pow m` ASSUME_TAC THENL [ASM_REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_LT]; ALL_TAC] THEN SUBGOAL_THEN `&0 < &q pow n` ASSUME_TAC THENL [ASM_REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_LT]; ALL_TAC] THEN SUBGOAL_THEN `abs(&p pow m) = &p pow m` ASSUME_TAC THENL [ASM_REWRITE_TAC[REAL_ABS_REFL; REAL_LE_LT]; ALL_TAC] THEN SUBGOAL_THEN `abs(&q pow n) = &q pow n` ASSUME_TAC THENL [ASM_REWRITE_TAC[REAL_ABS_REFL; REAL_LE_LT]; ALL_TAC] THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&p pow m` THEN ASM_SIMP_TAC[REAL_MUL_RID] THEN FIRST_ASSUM (fun th -> GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM th]) THEN REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_SUB_LDISTRIB] THEN MATCH_MP_TAC REAL_ABS_TRIANGLE_LT THEN EXISTS_TAC `(&p pow m)* &b - (&q pow n)* &a` THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2` THEN REWRITE_TAC[REAL_LT_TWO; REAL_ADD_LDISTRIB] THEN GEN_REWRITE_TAC RAND_CONV [REAL_MUL_2] THEN REWRITE_TAC[REAL_ABS_MUL_NUM; REAL_SUB_LDISTRIB] THEN MATCH_MP_TAC REAL_LET_ADD2 THEN CONJ_TAC THENL [ASM_REWRITE_TAC[REAL_ABS_BOUNDS; REAL_OF_NUM_POW; REAL_OF_NUM_MUL; REAL_LE_LNEG; REAL_LE_SUB_RADD; REAL_SUB_LE; REAL_OF_NUM_ADD; REAL_OF_NUM_LE; ADD_AC; REAL_ARITH `!x y z. x + y - z = (x + y) - z`] ;REWRITE_TAC[REAL_ARITH `!x y z. x - y - (x - z) = z - y`] THEN REWRITE_TAC[REAL_ARITH `!x y z. x*y*z - x*w*y*v = (x*y)*(z - w*v)`] THEN ASM_REWRITE_TAC[REAL_ABS_MUL; REAL_ARITH `abs(&2) = &2`] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `(&2*(&q pow n))* &1` THEN CONJ_TAC THENL [SUBGOAL_THEN `&0 < &2*(&q pow n)` (fun th -> ASM_SIMP_TAC[th; REAL_LT_LMUL_EQ]) THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[REAL_LT_TWO] ;ASM_REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_MUL; MULT_CLAUSES; REAL_OF_NUM_LE]]]);; let REALCALC_BASE_CONV tm q n = let p = Int 2 in let rec lg f e n = if e >=/ f then n else lg f (p*/e) (n +/ (Int 1)) in let qn = power_num q n in let m = lg ((Int 2)*/qn) (Int 1) (Int 0) in let pm = power_num p m in let th = snd (snd (REALCALC_CONV tm)) m in let a' = rand (rand (rator (rand (rand (rator (concl th)))))) in let a = dest_numeral a' in let b = quo_num ((Int 2)*/qn*/a +/ pm) ((Int 2)*/pm) in let p' = mk_numeral p and q' = mk_numeral q and m' = mk_numeral m and n' = mk_numeral n and b' = mk_numeral b in let pm' = vsubst [p',`p:num`; m',`m:num`] `p EXP m` and qn' = vsubst [q',`q:num`; n',`n:num`] `q EXP n` in prove(vsubst [b',`b:num`; q',`q:num`; n',`n:num`; tm,`tm:real`] `abs(&b - (&q pow n)*tm) < &1`, MATCH_MP_TAC BASECHANGE_LEMMA THEN EXISTS_TAC p' THEN EXISTS_TAC m' THEN EXISTS_TAC a' THEN REWRITE_TAC [th; NUM_REDUCE_CONV pm'; NUM_REDUCE_CONV qn'] THEN NUM_REDUCE_TAC);;