%------------------------------------------------------------------------------
% Various auxilliary results
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

prelude_aux: THEORY

BEGIN

  IMPORTING reals@sqrt,
            lnexp_fnd@ln_exp

  i:               VAR int
  m, n:            VAR nat
  pn,pm:           VAR posnat
  px:              VAR posreal
  nnx,nnz:         VAR nnreal
  x,y,z,w:         VAR real
  lt1x,lt1y:       VAR {r:posreal | r < 1}
  npx,npy,npz,npw: VAR npreal
  n0x,n0y:         VAR nzreal
  N:               VAR (nonempty?[nat])

  smallreal: NONEMPTY_TYPE = {x | -1 < x AND x < 1} CONTAINING 0

  lt_times_lt_nn1: LEMMA nnx < y AND nnz < w => nnx*nnz < y*w
  lt_times_lt_np1: LEMMA x < npy AND z < npw => npy*npw < x*z
  both_sides_times_nonneg_le1: LEMMA x <= y => x*nnz <= y*nnz
  both_sides_times_nonpos_le1: LEMMA y <= x => x*npz <= y*npz

  abs_nonneg: LEMMA abs(nnx) =  nnx
  abs_nonpos: LEMMA abs(npx) = -npx

  odd_even: LEMMA FORALL (z:int): even?(z) <=> NOT odd?(z)
  odd_or_even: LEMMA FORALL (z:int): odd?(z) OR even?(z)

  expt_product_aux:  LEMMA (n0x*n0y)^n = n0x^n*n0y^n
  expt_product:      LEMMA (n0x*n0y)^i = n0x^i*n0y^i
  expt_division_aux: LEMMA (n0x/n0y)^n = n0x^n/n0y^n
  expt_division:     LEMMA (n0x/n0y)^i = n0x^i/n0y^i

  expt_minus1: LEMMA (even?(i) => (-1)^i = 1) AND (odd?(i) => (-1)^i = -1)

  lt_equiv_not_le: LEMMA x <  y <=> NOT y <= x
  le_equiv_not_lt: LEMMA x <= y <=> NOT y <  x

  lt_equiv_le_plus_one: LEMMA FORALL (x,y:int): x < y <=> x+1 <= y
  lt_plus_one_equiv_le: LEMMA FORALL (x,y:int): x < 1+y <=> x <= y

  lt_le_transitivity: LEMMA x <= y AND y < z => x < z
  le_lt_transitivity: LEMMA x < y AND y <= z => x < z

  exp_of2_exists_aux: LEMMA lt1x < 1-2^-pn => (EXISTS n: lt1x^n < 1/2)
  exp_of2_exists: LEMMA EXISTS n: lt1x^n < 1/2
  exp_of_exists2: LEMMA EXISTS n: lt1x^n < lt1y

  round(x): int = floor(x+1/2)

  floor_sqrt_val:   LEMMA (m*m <= n AND n < (m+1)*(m+1)) <=> floor(sqrt(n)) = m
  ceiling_sqrt_0:   LEMMA ceiling(sqrt(0)) = 0
  ceiling_sqrt_val: LEMMA (pn <= pm*pm AND (pm-1)*(pm-1) < pn) <=>
                                                         ceiling(sqrt(pn)) = pm

  log2(px:posreal):real = ln(px)/ln(2)

  log2_2_expt_i: LEMMA log2(2^i) = i

  log2_strict_increasing: LEMMA strict_increasing?(log2)

END prelude_aux