src/real/transcScript.sml

65 (* The three functions we define by series are exp, sin, cos                 *)
77 val exp = new_definition("exp",
78   ���exp(x) = suminf(\n. (^exp_ser) n * (x pow n))���);
87 (* Show the series for exp converges, using the ratio test                   *)
91   ���!x. (\n. (^exp_ser) n * (x pow n)) sums exp(x)���,
95   GEN_TAC THEN REWRITE_TAC[exp] THEN MATCH_MP_TAC SUMMABLE_SUM THEN
222 (* Now at last we can get the derivatives of exp, sin and cos                *)
232   ���!x. (exp diffl exp(x))(x)���,
233   GEN_TAC THEN REWRITE_TAC[HALF_MK_ABS exp] THEN
307    ((g diffl m)(x) ==> ((\x. exp(g x)) diffl (exp(g x) * m))(x)) /\
325   ���exp(&0) = &1���,
326   REWRITE_TAC[exp] THEN CONV_TAC SYM_CONV THEN
339 ���!x. &0 <= x ==> (&1 + x) <= exp(x)���,
343     REWRITE_TAC[GSYM exp] THEN BETA_TAC THEN
364   ���!x. &0 < x ==> &1 < exp(x)���,
371   ���!x y. exp(x + y) * exp(~x) = exp(y)���,
374   SUBGOAL_THEN ���exp(y) = (\x. exp(x + y) * exp(~x))(&0)��� SUBST1_TAC THENL
386   ���!x. exp(x) * exp(~x) = &1���,
391   ���!x. exp(~x) * exp(x) = &1���,
395   ���!x. exp(~x) = inv(exp(x))���,
400   ���!x y. exp(x + y) = exp(x) * exp(y)���,
403   DISCH_THEN(MP_TAC o C AP_THM ���exp(x)��� o AP_TERM ���$*���) THEN
409   ���!x. &0 <= exp(x)���,
415   ���!x. ~(exp(x) = &0)���,
423   ���!x. &0 < exp(x)���,
429   ���!n x. exp(&n * x) = exp(x) pow n���,
436   ���!x y. exp(x - y) = exp(x) / exp(y)���,
441   ���!x y. x < y ==> exp(x) < exp(y)���,
445   SUBGOAL_THEN ���&1 < exp(y) / exp(x) =
446                  (&1 * exp(x)) < ((exp(y) / exp(x)) * exp(x))��� SUBST1_TAC THENL
453   ���!x y. exp(x) < exp(y) = x < y���,
463   ���!x y. exp(x) <= exp(y) = x <= y���,
468   ���!x y. (exp(x) = exp(y)) = (x = y)���,
473   ���!y. &1 <= y ==> ?x. &0 <= x /\ x <= y - &1 /\ (exp(x) = y)���,
479     MATCH_MP_TAC DIFF_CONT THEN EXISTS_TAC ���exp(x)��� THEN
483   ���!y. &0 < y ==> ?x. exp(x) = y���,
497  (`!x. &0 <= x /\ x <= inv(&2) ==> exp(x) <= &1 + &2 * x`,
501    [REWRITE_TAC[exp; BETA_THM] THEN MATCH_MP_TAC SER_LE THEN
510       EXISTS_TAC `exp x` THEN REWRITE_TAC[BETA_RULE REAL_EXP_CONVERGES];
550   ���ln x = @u. exp(u) = x���);
553   ���!x. ln(exp x) = x���,
560   ���!x. (exp(ln x) = x) = &0 < x���,
631   MP_TAC(SPECL [Term`&1 + x`, Term`exp x`] LN_MONO_LE) THEN
693   ���!n x. &0 < x ==> (exp(ln(x) / &(SUC n)) pow (SUC n) = x)���,
702   ���!n x. &0 < x ==> (root(SUC n) x = exp(ln(x) / &(SUC n)))���,
707     SUBGOAL_THEN ���!z. &0 < y /\ &0 < exp(z)��� MP_TAC THENL
2122   SUBGOAL_THEN ���(ln diffl (inv x))(exp(ln(x)))��� MP_TAC THENL
3534 (* Version for exp.                                                          *)
3538  (Term`((\n:num. exp) 0 = exp) /\
3539    (!m x. (((\n:num. exp) m) diffl ((\n:num. exp) (SUC m) x)) x)`,
3546                  (exp(x) = sum(0,n)(\m. x pow m / &(FACT m)) +
3547                            (exp(t) / &(FACT n)) * x pow n)`,
3558              (exp(x) = sum(0,n)(\m. x pow m / &(FACT m)) +
3559                        (exp(t) / &(FACT n)) * x pow n)`,
3607 val rpow = Define `a rpow b = exp (b * ln a)`;
3620         KNOW_TAC ``exp(ln a)= a`` THEN1
3623         KNOW_TAC ``a* exp (&n * ln a) = exp (&n * ln a)*a`` THEN1
3718  KNOW_TAC`` exp (b * ln a) < exp (c * ln a)= (b*ln a < c*ln a)``  THEN1
3723       KNOW_TAC``0 < ln a = exp (0) < exp (ln a)``  THEN1
3734              KNOW_TAC``exp (ln a)=(a:real)``  THEN1
3743  KNOW_TAC`` exp ((b:real) * ln a) <= exp ((c:real) * ln a)= ((b:real)*ln a <= (c:real)*ln a)`` THEN1
3748      KNOW_TAC``0 < ln a = exp (0) < exp (ln a)`` THEN1
3759           KNOW_TAC``exp (ln a)=(a:real)`` THEN1
3795  KNOW_TAC`` (exp (b * ln a) = exp (b * ln c)) = (ln (exp (b * ln a)) = ln (exp (b * ln c)))``THEN1
3808  KNOW_TAC`` (exp (b * ln a) = exp (c * ln a)) = (ln (exp (b * ln a)) = ln (exp (c * ln a)))`` THEN1
3815       KNOW_TAC``0 < ln a = exp (0) < exp (ln a)`` THEN1
3826                    KNOW_TAC``exp (ln a)=(a:real)`` THEN1
3835 KNOW_TAC``exp(ln x)= (x:real)`` THEN1
3845         ``!g m x. ((g diffl m) x ==> ((\x. exp (g x)) diffl (exp (g x) * m)) x)``,
3854 KNOW_TAC ``!x'. exp ((y * ln x')) = exp ((\x'. y *ln x') x')`` THEN1
3857 KNOW_TAC `` ((y / x) * exp ((\x'. y * ln x') x))= ( exp ((\x'. y * ln x') x)*(y/x) ) `` THEN1