examples/bitvectors/power2.why

   1 theory Pow2int
   2
   3   use int.Int
   4
   5   function pow2 (i:int) : int
   6
   7   axiom Power_0 : pow2 0 = 1
   8
   9   axiom Power_s : forall n: int. n >= 0 -> pow2 (n+1) = 2 * pow2 n
  10
  11   lemma Power_1 : pow2 1 = 2
  12
  13   lemma Power_sum :
  14     forall n m: int. n >= 0 /\ m >= 0 -> pow2 (n+m) = pow2 n * pow2 m
  15
  16   lemma pow2pos: forall i:int. i >= 0 -> pow2 i > 0
  17
  18   lemma pow2_0: pow2 0   =                    1
  19   lemma pow2_1: pow2 1   =                    2
  20   lemma pow2_2: pow2 2   =                    4
  21   lemma pow2_3: pow2 3   =                    8
  22   lemma pow2_4: pow2 4   =                   16
  23   lemma pow2_5: pow2 5   =                   32
  24   lemma pow2_6: pow2 6   =                   64
  25   lemma pow2_7: pow2 7   =                  128
  26   lemma pow2_8: pow2 8   =                  256
  27   lemma pow2_9: pow2 9   =                  512
  28   lemma pow2_10: pow2 10 =                 1024
  29   lemma pow2_11: pow2 11 =                 2048
  30   lemma pow2_12: pow2 12 =                 4096
  31   lemma pow2_13: pow2 13 =                 8192
  32   lemma pow2_14: pow2 14 =                16384
  33   lemma pow2_15: pow2 15 =                32768
  34   lemma pow2_16: pow2 16 =                65536
  35   lemma pow2_17: pow2 17 =               131072
  36   lemma pow2_18: pow2 18 =               262144
  37   lemma pow2_19: pow2 19 =               524288
  38   lemma pow2_20: pow2 20 =              1048576
  39   lemma pow2_21: pow2 21 =              2097152
  40   lemma pow2_22: pow2 22 =              4194304
  41   lemma pow2_23: pow2 23 =              8388608
  42   lemma pow2_24: pow2 24 =             16777216
  43   lemma pow2_25: pow2 25 =             33554432
  44   lemma pow2_26: pow2 26 =             67108864
  45   lemma pow2_27: pow2 27 =            134217728
  46   lemma pow2_28: pow2 28 =            268435456
  47   lemma pow2_29: pow2 29 =            536870912
  48   lemma pow2_30: pow2 30 =           1073741824
  49   lemma pow2_31: pow2 31 =           2147483648
  50   lemma pow2_32: pow2 32 =           4294967296
  51   lemma pow2_33: pow2 33 =           8589934592
  52   lemma pow2_34: pow2 34 =          17179869184
  53   lemma pow2_35: pow2 35 =          34359738368
  54   lemma pow2_36: pow2 36 =          68719476736
  55   lemma pow2_37: pow2 37 =         137438953472
  56   lemma pow2_38: pow2 38 =         274877906944
  57   lemma pow2_39: pow2 39 =         549755813888
  58   lemma pow2_40: pow2 40 =        1099511627776
  59   lemma pow2_41: pow2 41 =        2199023255552
  60   lemma pow2_42: pow2 42 =        4398046511104
  61   lemma pow2_43: pow2 43 =        8796093022208
  62   lemma pow2_44: pow2 44 =       17592186044416
  63   lemma pow2_45: pow2 45 =       35184372088832
  64   lemma pow2_46: pow2 46 =       70368744177664
  65   lemma pow2_47: pow2 47 =      140737488355328
  66   lemma pow2_48: pow2 48 =      281474976710656
  67   lemma pow2_49: pow2 49 =      562949953421312
  68   lemma pow2_50: pow2 50 =     1125899906842624
  69   lemma pow2_51: pow2 51 =     2251799813685248
  70   lemma pow2_52: pow2 52 =     4503599627370496
  71   lemma pow2_53: pow2 53 =     9007199254740992
  72   lemma pow2_54: pow2 54 =    18014398509481984
  73   lemma pow2_55: pow2 55 =    36028797018963968
  74   lemma pow2_56: pow2 56 =    72057594037927936
  75   lemma pow2_57: pow2 57 =   144115188075855872
  76   lemma pow2_58: pow2 58 =   288230376151711744
  77   lemma pow2_59: pow2 59 =   576460752303423488
  78   lemma pow2_60: pow2 60 =  1152921504606846976
  79   lemma pow2_61: pow2 61 =  2305843009213693952
  80   lemma pow2_62: pow2 62 =  4611686018427387904
  81   lemma pow2_63: pow2 63 =  9223372036854775808
  82
  83
  84   use int.EuclideanDivision
  85
  86   lemma Div_mult_inst: forall x z:int.
  87           x > 0 ->
  88           div (x * 1 + z) x = 1 + div z x
  89
  90   lemma Div_double:
  91     forall x y:int. 0 < y <= x < 2*y -> div x y = 1
  92
  93   lemma Div_pow: forall x i:int.
  94     i > 0 -> pow2 (i-1) <= x < pow2 i -> div x (pow2 (i-1)) = 1
  95
  96   lemma Div_double_neg:
  97     forall x y:int. -2*y <= x < -y < 0 -> div x y = -2
  98
  99   lemma Div_pow2: forall x i:int.
 100     i > 0 -> -pow2 i <= x < -pow2 (i-1) -> div x (pow2 (i-1)) = -2
 101
 102 (*
 103   lemma Mod_pow2: forall x i:int. mod (x + pow2 i) 2 = mod x 2
 104 *)
 105
 106   lemma Mod_pow2_gen: forall x i k :int.
 107     0 <= k < i -> mod (div (x + pow2 i) (pow2 k)) 2 = mod (div x (pow2 k)) 2
 108
 109 end
 110
 111
 112
 113 theory Pow2real
 114
 115   use int.Int
 116   use real.RealInfix
 117
 118   function pow2 (i:int) : real
 119
 120   axiom Power_0 : pow2 0 = 1.0
 121   axiom Power_s : forall n: int. n >= 0 -> pow2 (n+1) = 2.0 *. pow2 n
 122   axiom Power_p : forall n: int. n <= 0 -> pow2 (n-1) = 0.5 *. pow2 n
 123
 124   lemma Power_s_all : forall n:int. pow2 (n+1) = 2.0 *. pow2 n
 125
 126   lemma Power_p_all : forall n:int. pow2 (n-1) = 0.5 *. pow2 n
 127
 128   lemma Power_1_2: 0.5 = 1.0 /. 2.0
 129
 130   lemma Power_1 : pow2 1 = 2.0
 131
 132   lemma Power_neg1 : pow2 (-1) = 0.5
 133
 134   lemma Power_non_null_aux: forall n:int.n>=0 -> pow2 n <> 0.0
 135
 136   lemma Power_neg_aux : forall n:int. n>=0 -> pow2 (-n) = 1.0 /. pow2 n
 137
 138   lemma Power_non_null: forall n:int. pow2 n <> 0.0
 139
 140   lemma Power_neg : forall n:int. pow2 (-n) = 1.0 /. pow2 n
 141
 142   lemma Power_sum_aux : forall m n. m >= 0 -> pow2 (n+m) = pow2 n *. pow2 m
 143
 144   lemma Power_sum : forall n m: int. pow2 (n+m) = pow2 n *. pow2 m
 145
 146   use Pow2int as P2I
 147   use real.FromInt
 148
 149   lemma Pow2_int_real:
 150     forall x:int. x >= 0 -> pow2 x = from_int (P2I.pow2 x)
 151
 152 end