src/real/transcScript.sml

548 val ln = new_definition("ln",
549   ���ln x = @u. exp(u) = x���);
552   ���!x. ln(exp x) = x���,
553   GEN_TAC THEN REWRITE_TAC[ln, EXP_INJ] THEN
559   ���!x. (exp(ln x) = x) = &0 < x���,
566   ���!x y. &0 < x /\ &0 < y ==> (ln(x * y) = ln(x) + ln(y))���,
573   ���!x y. &0 < x /\ &0 < y ==> ((ln(x) = ln(y)) = (x = y))���,
580   ���ln(&1) = &0���,
585   ���!x. &0 < x ==> (ln(inv x) = ~(ln x))���,
596   ���!x y. &0 < x /\ &0 < y ==> (ln(x / y) = ln(x) - ln(y))���,
606   ���!x y. &0 < x /\ &0 < y ==> (ln(x) < ln(y) = x < y)���,
613   ���!x y. &0 < x /\ &0 < y ==> (ln(x) <= ln(y) = x <= y)���,
620   ���!n x. &0 < x ==> (ln(x pow n) = &n * ln(x))���,
627   Term `!x. &0 <= x ==> ln(&1 + x) <= x`,
639   ���!x. &0 < x ==> ln(x) < x���,
643   MP_TAC(SPEC ���ln(x)��� EXP_LE_X) THEN
644   SUBGOAL_THEN ���&0 <= ln(x)��� ASSUME_TAC THENL
650   SUBGOAL_THEN ���(&1 + ln(x)) <= ln(x)��� MP_TAC THENL
653   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���&0 + ln(x)��� THEN
658   Term `!x. &1 <= x ==> &0 <= ln(x)`,
669   Term `!x. &0 < x ==> (ln diffl (inv x))(x)`,
676   MP_TAC(SPEC (Term`ln(x)`) DIFF_EXP) THEN ASM_REWRITE_TAC[] THEN
692   ���!n x. &0 < x ==> (exp(ln(x) / &(SUC n)) pow (SUC n) = x)���,
701   ���!n x. &0 < x ==> (root(SUC n) x = exp(ln(x) / &(SUC n)))���,
711     SUBGOAL_THEN ���ln(y) * &(SUC n) = (ln(y pow(SUC n)) / &(SUC n)) * &(SUC n)���
2119   ���!x. &0 < x ==> (ln diffl (inv x))(x)���,
2121   SUBGOAL_THEN ���(ln diffl (inv x))(exp(ln(x)))��� MP_TAC THENL
2125   MAP_EVERY EXISTS_TAC [���ln(x) - &1���, ���ln(x) + &1���] THEN
2129    [MP_TAC(SPEC ���ln(x)��� DIFF_EXP) THEN
3566 (* Version for ln(1 - x).                                                    *)
3571            ==> ((\x. ln(g x)) diffl (inv(g x) * m))(x)`,
3604 val rpow = Define `a rpow b = exp (b * ln a)`;
3617         KNOW_TAC ``exp(ln a)= a`` THEN1
3620         KNOW_TAC ``a* exp (&n * ln a) = exp (&n * ln a)*a`` THEN1
3663         ``! a b. (0 < a)==> (ln (a rpow b)= (b*ln a))``,
3675  KNOW_TAC`` ((b * ln a + c * ln a + -b * ln a)=(b * ln a  -b * ln a + c*ln a)) ``THEN1
3678      KNOW_TAC``((b * ln a - b * ln a + c * ln a) = (c*ln a )) ``THEN1
3715  KNOW_TAC`` exp (b * ln a) < exp (c * ln a)= (b*ln a < c*ln a)``  THEN1
3718       KNOW_TAC``((b:real)*ln a < (c:real)*ln a)= (b < c)``  THENL   [
3720       KNOW_TAC``0 < ln a = exp (0) < exp (ln a)``  THEN1
3731              KNOW_TAC``exp (ln a)=(a:real)``  THEN1
3740  KNOW_TAC`` exp ((b:real) * ln a) <= exp ((c:real) * ln a)= ((b:real)*ln a <= (c:real)*ln a)`` THEN1
3743  KNOW_TAC``(b*ln a <= c*ln a)= ((b:real) <= (c:real))`` THENL[
3745      KNOW_TAC``0 < ln a = exp (0) < exp (ln a)`` THEN1
3756           KNOW_TAC``exp (ln a)=(a:real)`` THEN1
3766 KNOW_TAC`` (((b:real) * ln a) <= ((b:real) * ln c))= ((ln a <= ln c))`` THENL[
3778  KNOW_TAC ``((b * ln a) < (b * ln c))= ((ln a < ln c))``  THENL[
3792  KNOW_TAC`` (exp (b * ln a) = exp (b * ln c)) = (ln (exp (b * ln a)) = ln (exp (b * ln c)))``THEN1
3805  KNOW_TAC`` (exp (b * ln a) = exp (c * ln a)) = (ln (exp (b * ln a)) = ln (exp (c * ln a)))`` THEN1
3810           KNOW_TAC``(1 < (a:real))==> 0 < ln a`` THENL[
3812       KNOW_TAC``0 < ln a = exp (0) < exp (ln a)`` THEN1
3823                    KNOW_TAC``exp (ln a)=(a:real)`` THEN1
3832 KNOW_TAC``exp(ln x)= (x:real)`` THEN1
3851 KNOW_TAC ``!x'. exp ((y * ln x')) = exp ((\x'. y *ln x') x')`` THEN1
3854 KNOW_TAC `` ((y / x) * exp ((\x'. y * ln x') x))= ( exp ((\x'. y * ln x') x)*(y/x) ) `` THEN1
3858 KNOW_TAC ``((\x. y * ln x) diffl (y/x)) x = ((\x. y * (\x.ln x) x) diffl (y/x)) x`` THEN1
3873              (ln(&1 + x)
3878   MP_TAC(SPEC (Term`\x. ln(&1 + x)`) MCLAURIN) THEN
3880     (Term`\n x. (n=0) => ln(&1 + x)
3975                  (--(ln(&1 - x)) = Sum(0,n) (\m. (x pow m) / &m) +
3978   MP_TAC(SPEC `\x. --(ln(&1 - x))` MCLAURIN) THEN
3980     `\n x. if n = 0 then --(ln(&1 - x))