Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Thu, 4 Mar 1993 15:01:19 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA18321;
          Thu, 4 Mar 93 06:42:41 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA18316;
          Thu, 4 Mar 93 06:42:28 -0800
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Thu, 4 Mar 1993 14:42:05 +0000
To: info-hol@edu.uidaho.cs.ted
Subject: New integer and real theories
Date: Thu, 04 Mar 93 14:42:01 +0000
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.418:04.03.93.14.42.08"@cl.cam.ac.uk>


I have put up for FTP a directory containing an amalgam of:

* Yet another theory of integers. This is developed using the same
  principles, and much of the same code, as the real numbers. Whether you
  prefer one of the alternative theories is a matter of taste: I think this
  theory is far cleaner than others, but I'm biased.

  FILES NEEDED: |equiv.ml|, |int.ml|, |useful.ml|

* A preliminary revision of the reals library. The main change is the
  proof of the differentiability of inverse functions, and its use to derive
  the derivatives of |ln|, |asn|, |acs| and |atn|. In addition some extra
  lemmas about roots and powers have been added, and the proof of the Chain
  Rule tidied up using Caratheodory's definition of the derivative. A list of
  the substantially new theorems is given below.

  FILES NEEDED: All but |int.ml|. They are drop-in replacements for the files
  in |[..]/Library/reals/theories|.

The FTP site is:

  ftp.cl.cam.ac.uk [128.232.0.56]

and the directory is:

  hvg/contrib/int-real

In the future, I intend to integrate this properly into a multi-section library
of number systems. But I have a lot of other preoccupations at the moment.

John.

  DIFF_CARAT
    "!f l x. (f diffl l)(x) =
        ?g. (!z. f(z) - f(x) = g(z) * (z - x)) /\ g contl x /\ (g(x) = l)"

  CONT_COMPOSE
    "!f g x. f contl x /\ g contl (f x) ==> (\x. g(f x)) contl x"

  CONT_ATTAINS_ALL
    "!f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==>
       ?L M. L <= M /\
             (!y. L <= y /\ y <= M ==> ?x. a <= x /\ x <= b /\ (f(x) = y)) /\
             (!x. a <= x /\ x <= b ==> L <= f(x) /\ f(x) <= M)"

  INTERVAL_ABS
    "!x z d. (x - d) <= z /\ z <= (x + d) = abs(z - x) <= d"

  CONT_INJ_LEMMA
    "!f g x d. &0 < d /\
              (!z. abs(z - x) <= d ==> (g(f(z)) = z)) /\
              (!z. abs(z - x) <= d ==> f contl z) ==>
       ~(!z. abs(z - x) <= d ==> f(z) <= f(x))"

  CONT_INJ_LEMMA2
    "!f g x d. &0 < d /\
              (!z. abs(z - x) <= d ==> (g(f(z)) = z)) /\
              (!z. abs(z - x) <= d ==> f contl z) ==>
       ~(!z. abs(z - x) <= d ==> f(x) <= f(z))"

  CONT_INJ_RANGE
    "!f g x d.  &0 < d /\
              (!z. abs(z - x) <= d ==> (g(f(z)) = z)) /\
              (!z. abs(z - x) <= d ==> f contl z) ==>
          ?e. &0 < e /\
              (!y. abs(y - f(x)) <= e ==> ?z. abs(z - x) <= d /\ (f z = y))"

  CONT_INVERSE
    "!f g x d. &0 < d /\
               (!z. abs(z - x) <= d ==> (g(f(z)) = z)) /\
               (!z. abs(z - x) <= d ==> f contl z)
          ==> g contl (f x)"

  DIFF_INVERSE
    "!f g l x d. &0 < d /\
                 (!z. abs(z - x) <= d ==> (g(f(z)) = z)) /\
                 (!z. abs(z - x) <= d ==> f contl z) /\
                 (f diffl l)(x) /\
                 ~(l = &0)
          ==> (g diffl (inv l))(f x)"

  INTERVAL_CLEMMA
    "!a b x. a < x /\ x < b ==>
          ?d. &0 < d /\ !y. abs(y - x) <= d ==> a < y /\ y < b"

  DIFF_INVERSE_OPEN
    "!f g l a x b. a < x /\ x < b /\
                   (!z. a < z /\ z < b ==> (g(f(z)) = z) /\ f contl z) /\
                   (f diffl l)(x) /\
                   ~(l = &0)
          ==> (g diffl (inv l))(f x)"

  POW_LT
    "!n x y. &0 <= x /\ x < y ==> (x pow (SUC n)) < (y pow (SUC n))"

  POW_EQ
    "!n x y. &0 <= x /\ &0 <= y /\ (x pow (SUC n) = y pow (SUC n))
          ==> (x = y)"

  POW_ZERO
    "!n x. (x pow n = &0) ==> (x = &0)"

  POW_ZERO_EQ
    "!n x. (x pow (SUC n) = &0) = (x = &0)"

  LN_LT_X
    "!x. &0 < x ==> ln(x) < x"

  ROOT_POS_LT
    "!n x. &0 < x ==> &0 < root(SUC n) x"

  ROOT_POS
    "!n x. &0 <= x ==> &0 <= root(SUC n) x"

  POW_ROOT_POS
    "!n x. &0 <= x ==> (root(SUC n)(x pow (SUC n)) = x)"

  SQRT_EQ
    "!x y. (x pow 2 = y) /\ (&0 <= x) ==> (x = (sqrt(y)))"

  COS_POS_PI2_LE
    "!x. &0 <= x /\ x <= (pi / &2) ==> &0 <= cos(x)"

  COS_POS_PI_LE
    "!x. --(pi / &2) <= x /\ x <= (pi / &2) ==> &0 <= cos(x)"

  SIN_POS_PI2_LE
    "!x. &0 <= x /\ x <= (pi / &2) ==> &0 <= sin(x)"

  SIN_POS_PI_LE
    "!x. &0 <= x /\ x <= pi ==> &0 <= sin(x)"

  ASN_BOUNDS_LT
    "!y. --(&1) < y /\ y < &1 ==> --(pi / &2) < asn(y) /\ asn(y) < pi / &2"

  ACS_BOUNDS_LT
    "!y. --(&1) < y /\ y < &1 ==> &0 < acs(y) /\ acs(y) < pi"

  TAN_SEC
    "!x. ~(cos(x) = &0) ==> (&1 + (tan(x) pow 2) = inv(cos x) pow 2)"

  SIN_COS_SQ
    "!x. &0 <= x /\ x <= pi ==> (sin(x) = sqrt(&1 - (cos(x) pow 2)))"

  COS_SIN_SQ
    "!x. --(pi / &2) <= x /\ x <= (pi / &2) ==>
               (cos(x) = sqrt(&1 - (sin(x) pow 2)))"

  COS_ATN_NZ
    "!x. ~(cos(atn(x)) = &0)"

  COS_ASN_NZ
    "!x. --(&1) < x /\ x < &1 ==> ~(cos(asn(x)) = &0)"

  SIN_ACS_NZ
    "!x. --(&1) < x /\ x < &1 ==> ~(sin(acs(x)) = &0)"

  DIFF_LN
    "!x. &0 < x ==> (ln diffl (inv x))(x)"

  DIFF_ASN_LEMMA
    "!x. --(&1) < x /\ x < &1 ==> (asn diffl (inv(cos(asn x))))(x)"

  DIFF_ASN
    "!x. --(&1) < x /\ x < &1 ==> (asn diffl (inv(sqrt(&1 - (x pow 2)))))(x)"

  DIFF_ACS_LEMMA
    "!x. --(&1) < x /\ x < &1 ==> (acs diffl inv(--(sin(acs x))))(x)"

  DIFF_ACS
    "!x. --(&1) < x /\ x < &1 ==> (acs diffl --(inv(sqrt(&1 - (x pow 2)))))(x)"

  DIFF_ATN
    "!x. (atn diffl (inv(&1 + (x pow 2))))(x)"