exponent_props.pvs

exponent_props : THEORY
%-------------------------------------------------------------------------
%  More properties of expt  
%
%      by Bruno Dutertre    Royal Holloway & Bedford New College
%
%     9/10/00  -- removed duplications with prelude  RWB
%                 changed names of 
%
%                    expt_mult --> expt_of_mult
%                    expt_div  --> expt_of_div 
%                    expt_inv  --> expt_of_inv 
%                 
%                 to eliminate duplications with prelude
%
%  Note. This library is retained for upward compatibility only.  New 
%        users should use the prelude theorems.
%-------------------------------------------------------------------------
BEGIN

  n, m: VAR nat
  p: VAR posnat
  x, y: VAR real
  z: VAR nzreal
  n0x, n0y: VAR nzreal

%  JUDGEMENT expt(z: nzreal, m: nat) HAS_TYPE nzreal

  abs_expt    : LEMMA abs(expt(x, n)) = expt(abs(x), n)

  expt_ne_0:    LEMMA expt(z, n) /= 0;

%% The following is named abs_of_expt_inv in prelude

  abs_expt_inv: LEMMA abs(1 / expt(z, n)) = 1 / expt(abs(z),n)


  i:  VAR int
  pn: VAR posnat

% The following all appear in the prelude under different names

  zero_hat : LEMMA 0^pn = 0

  mult_hat : LEMMA (n0x * n0y) ^i = n0x^i * n0y^i

  div_hat  : LEMMA (n0x / n0y)^i = n0x^i / n0y^i

  inv_hat  : LEMMA (1 / n0x)^i = 1 / n0x^i

  abs_hat  : LEMMA abs(n0x^i) = abs(n0x)^i

  AUTO_REWRITE+ expt_x0         % LEMMA x^0 = 1
  AUTO_REWRITE+ expt_x1         % LEMMA x^1 = x
  AUTO_REWRITE+ expt_1i         % LEMMA 1^i = 1
  AUTO_REWRITE+ zero_hat        % LEMMA 0^p = 0


%%  a, b: VAR posreal
%%  lt1x: VAR { a | a < 1}
%%  gt1x: VAR { a | 1 < a }
%%  expt_lt1_bound1 : LEMMA  expt(lt1x, n) <= 1   %%  In Prelude
%%  expt_lt1_bound2 : LEMMA  expt(lt1x, p) < 1    %%  In Prelude
%%  expt_gt1_bound1 : LEMMA  1 <= expt(gt1x, n)  %%  In Prelude
%%  expt_gt1_bound2 : LEMMA  1 < expt(gt1x, p)   %%  In Prelude
%%  nnx: VAR nonneg_real
%%  expt_lt1_le     : LEMMA nnx < 1 => nnx^pn <= nnx %%  In Prelude
%%  large_expt      : LEMMA 1 < a  IMPLIES (FORALL b: EXISTS n: b < expt(a, n))
%%  small_expt      : LEMMA a < 1  IMPLIES (FORALL b: EXISTS n: expt(a, n) < b)
END exponent_props