lemmas: THEORY
BEGIN
   %%%% some simple lemmas faster to prove than to 
   %%%% find in the prelude
   exp2_neg: Lemma
     Forall (i: posint): 2^-i <= 1/2;

   alph_eq_trans: LEMMA forall (a:posreal, q1,q2:int, y: real):
		q1*a < y AND q2*a<y AND y<(q1+1)*a AND y<(q2+1)*a IMPLIES
			q1 = q2;

   q_mul_exists: LEMMA forall(a:posreal, x:real): exists (q:int):
					q*a <= x AND x < (q+1)*a;

   abs_minus: LEMMA forall(x,y: real): abs(x-y)=abs(y-x);

   %%%% a generalization of a prelude-lemma
   floor_val_real: LEMMA FORALL (i:real, j:posreal, k:int):
						i >= k*j AND i < (k+1)*j IMPLIES floor(i/j) = k ;

   ceil_val_real: LEMMA FORALL (i:real, j:posreal, k:int):
						i > (k-1)*j AND i <= k*j IMPLIES ceiling(i/j) = k;

   %%%% some lemmas i did not find in the prelude 
   %%%% (i did not search too long)
   int_ineq1: LEMMA forall(i,j:int): i>j IFF i>j+1/2;
   int_ineq2: LEMMA forall(i,j:int): i<1+j IFF i<=j;

%   int_is_rat: LEMMA forall(x:real): integer_pred(x) IMPLIES rational_pred(x)

   %%%% some lemmas about composition of ceilings
   ceil_ceil_1_l1: LEMMA FORALL (i:nat, x:{ x:real | i<=x AND x<i+1}):
					ceiling(x) = ceiling(ceiling(2*x)/2 - 1/4);
   ceil_ceil_1_l2: LEMMA FORALL (i:nat, x:{ x:real | i <= -x  AND -x < i+1}):
					ceiling(x) = ceiling(ceiling(2*x)/2 - 1/4);
   ceil_ceil_1: LEMMA FORALL (x: real):
					ceiling(x) = ceiling(ceiling(2*x)/2 - 1/4);
    floor_lemma: Lemma
    Forall (n: posnat, y: below(2^n)):
      Not n = 1 Implies
        floor(y / 2 ^ ceiling(n / 2)) < 2 ^ (n - ceiling(n / 2));

   %%%% some obvious lemmas, important is the last one
   int_times_ge: LEMMA forall (k,l,m:nat): k/=0 AND l>m IMPLIES l*k > m;
   quarter_not_int: LEMMA
   			 FORALL (i:int): NOT integer?(i/2+1/4);

   %%%% lemmas about exponantiation
   expt_int: LEMMA forall (i: int, j:nat): integer?(i^j);

   abs_mult_pos: Lemma  %% cb
     Forall(x: real, p: posreal):
       abs(x) * p = abs(x * p);

   floor_small_real: Lemma  %% cb
     Forall (s,t: posreal): s<t Implies floor(s/t) = 0;

END lemmas




int_closed: THEORY
BEGIN
	i,j,k: VAR real;

	int_closed_plus: LEMMA integer?(i) AND integer?(j) IMPLIES integer?(i+j);
	int_closed_minus: LEMMA integer?(i) AND integer?(j) IMPLIES integer?(i-j);
	int_closed_times: LEMMA integer?(i) AND integer?(j) IMPLIES integer?(i*j);
	int_closed_neg: LEMMA integer?(i) IMPLIES integer?(-i);

END int_closed


%%% lemmas on floor and ceiling
%%% some lemmas are in the above theory for historical reasons
floor_ceil_lems: THEORY
BEGIN
	IMPORTING int_closed

	ceil_abs: LEMMA forall (k:int, x: { x:real | abs(x)<=k }): abs(ceiling(x))<=k;
	floor_abs: LEMMA forall (k:int, x: { x:real | abs(x)<=k }): abs(floor(x))<=k;

	ceil_abs_ge: LEMMA forall (k:int, x: { x:real | abs(x)>=k }): abs(ceiling(x))>=k;
	floor_abs_ge: LEMMA forall (k:int, x: { x:real | abs(x)>=k }): abs(floor(x))>=k;

	int_ge_ceil: LEMMA forall (x: real, k: { k: int | k>=x }): k >= ceiling(x);
	int_le_floor: LEMMA forall (x: real, k: { k: int | k<=x }): k <= floor(x);

	fractional_0: LEMMA forall (x: real): fractional(x)=0 IFF integer?(x);

	fract_floor: LEMMA forall (x: real): fractional(abs(x)/2) = 0 IMPLIES floor(x) = x;
END floor_ceil_lems





exp_lems: THEORY
BEGIN
   n: VAR int;
   x,y: VAR real;
 
   exp_add1: LEMMA 2^(n-1) + y*2^n = 2^n*(y+1/2);
   exp2_0:  LEMMA 2^0 = 1;
   exp2_1:  LEMMA 2^1 = 2;
   exp2_2:  LEMMA 2^2 = 4;
   exp2_3:  LEMMA 2^3 = 8;
   exp2_4:  LEMMA 2^4 = 16;
   exp2_5:  LEMMA 2^5 = 32;
   exp2_6:  LEMMA 2^6 = 64;
   exp2_7:  LEMMA 2^7 = 128;
   exp2_8:  LEMMA 2^8 = 256;
   exp2_9:  LEMMA 2^9 = 512;
   exp2_10: LEMMA 2^10 = 1024;
   exp2_11: LEMMA 2^11 = 2048;
   exp2_12: LEMMA 2^12 = 4096;
   exp2_13: LEMMA 2^13 = 8192;
   exp2_23: LEMMA 2^23 = 8388608;
   exp2_25: LEMMA 2^25 = 4*8388608;
   exp2_28: LEMMA 2^28 = 268435456;
   exp2_29: LEMMA 2^29 = 2 * 268435456;
   exp2_44: LEMMA 2^44 = 17592186044416;
   exp2_52: LEMMA 2^52 = 9007199254740992/2;
   exp2_53: LEMMA 2^53 = 9007199254740992;
   exp2_54: LEMMA 2^54 = 2* 9007199254740992;
   exp2_55: LEMMA 2^55 = 4* 9007199254740992;
   exp2_56: LEMMA 2^56 = 8* 9007199254740992;
   exp2_57: LEMMA 2^57 = 144115188075855872;
   exp2_58: LEMMA 2^58 = 2*144115188075855872;
   exp2_62: LEMMA 2^62 = 9223372036854775808/2;
   exp2_63: LEMMA 2^63 = 9223372036854775808;
   exp2_64: LEMMA 2^64 = 18446744073709551616;
   exp2_71: LEMMA 2^71 = 2361183241434822606848;
   exp2_114: LEMMA 2^114 = 83076749736557242056487941267521536/4;
   exp2_115: LEMMA 2^115 = 83076749736557242056487941267521536/2;
   exp2_116: LEMMA 2^116 = 83076749736557242056487941267521536;
   exp2_117: LEMMA 2^117 = 83076749736557242056487941267521536*2;
   exp2_127: LEMMA 2^127 = 170141183460469231731687303715884105728;
   exp2_128: LEMMA 2^128 = 2 * 170141183460469231731687303715884105728;
   exp2_192: LEMMA 2^192 = 2^128 * 2^64;
   exp2_320: LEMMA 2^320 = 2135987035920910082395021706169552114602704522356652769947041607822219725780640550022962086936576;
   exp2_512: LEMMA 2^512 = 2^128 * 2^128 * 2^128 * 2^128;
   exp2_1024: LEMMA 2^1024 = 2^512 * 2^512;
   exp2_1536: LEMMA 2^1536 = 2^512 * 2^512 * 2^512;
END exp_lems



%% a collection of the above theories
liblemmas: Theory
Begin

  Importing lemmas, exp_lems, floor_ceil_lems

End liblemmas



int_induction: THEORY
BEGIN
 p: VAR pred[int];
 j: VAR nat;
 i: VAR int;

 int_induction: LEMMA
 (p(0) AND (FORALL j: (p(j) IMPLIES p(j+1)) AND (p(-j) IMPLIES p(-j-1))))
        IMPLIES (FORALL i: p(i));

END int_induction



evenodd: THEORY
  BEGIN
    i: VAR integer;

    even_xor_odd_nat: LEMMA
      FORALL (j: nat): even?(j) XOR odd?(j);

    even_xor_odd: LEMMA
      even?(i) XOR odd?(i);

    % the above lemma in a more convenient form (sbeyer)
    even_iff_not_odd: LEMMA
      even?(i) IFF NOT odd?(i);

    even_div_2_is_int: LEMMA
      even?(i) IMPLIES integer_pred(i/2);

    odd_minus_1_div_2_is_int: LEMMA
      odd?(i) IMPLIES integer_pred((i-1)/2);

  END evenodd


mul_pow2: theory
begin
  importing evenodd,lemmas

  a, b: VAR posnat;
  l: VAR posnat;

  mul_pow2_aux1: LEMMA
    a*b=2 IMPLIES (a=1 OR b=1);

  mul_pow2_aux2: LEMMA
    a*b=2^l AND a/=1 IMPLIES
    even?(a) OR even?(b);

  mul_pow2: LEMMA
    a*b=2^l
    IMPLIES EXISTS (i, j: nat): a=2^i AND b=2^j;

end mul_pow2