More proofs in bitvector example

examples/bitvectors/double_of_int.why

@@ -113,6 +113,33 @@ theory DoubleOfInt
 
   lemma jpxorx_pos: forall x:int. x>=0 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = True
 
+  lemma from_int2c_to_nat_sub_pos:
+  	forall i:int. 0 <= i <= 31 -> 
+          forall x:int. 0 <= x <  Pow2int.pow2 i -> 
+           BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = x
+
+  lemma lemma1_pos : forall x:int. is_int32 x /\ x >= 0 -> 
+  	BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x
+
+  (* case x < 0 *)
+
+  lemma jpxorx_neg: forall x:int. x<0 -> 
+  	BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = False
+
+  lemma from_int2c_to_nat_sub_neg:
+  	forall i:int. 0 <= i <= 31 -> 
+          forall x:int. -Pow2int.pow2 i <= x <  0 -> 
+           BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = Pow2int.pow2 i + x
+	
+  lemma lemma1_neg : forall x:int. is_int32 x /\ x < 0 -> 
+  	BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x
+
+(**** old
+
+  (* case x >= 0 *)
+
+  lemma jpxorx_pos: forall x:int. x>=0 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = True
+
 (*
   lemma from_int2c_to_nat_sub31:
   	forall x:int. x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = x
@@ -138,9 +165,12 @@ theory DoubleOfInt
 
   lemma lemma1_neg : forall x:int. is_int32 x /\ x < 0 -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x
 
-  (* final lemma *)
+****)
 
-  lemma lemma1 : forall x:int. is_int32 x -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x
+
+  (* final lemma *)
+  lemma lemma1 : forall x:int. is_int32 x ->
+    BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x
 
 
   (*********************************************************************)

examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_lemma2_1.v

@@ -715,10 +715,9 @@ Axiom nth_var32to63 : forall (x:Z) (k:Z), ((32%Z <= k)%Z /\ (k <= 63%Z)%Z) ->
 Axiom nth_var3 : forall (x:Z), forall (i:Z), ((32%Z <= i)%Z /\
   (i <= 51%Z)%Z) -> ((nth1 (var x) i) = false).
 
-
 Open Scope Z_scope.
 Require Import Why3.
-Ltac ae := why3 "alt-ergo" timelimit 3.
+Ltac ae := why3 "alt-ergo" timelimit 5.
 
 (* Why3 goal *)
 Theorem lemma2 : forall (x:Z), (is_int32 x) -> ((to_nat_sub1 (var x) 51%Z

examples/bitvectors/power2.why

@@ -80,6 +80,15 @@ theory Pow2int
   lemma pow2_62: pow2 62 =  4611686018427387904
   lemma pow2_63: pow2 63 =  9223372036854775808
 
+
+  use import int.EuclideanDivision
+
+  lemma Div_pow: forall x i:int. pow2 (i-1) <= x < pow2 i ->
+		 div x (pow2 (i-1)) = 1
+
+  lemma Div_pow2: forall x i:int. -pow2 i <= x < -pow2 (i-1) ->
+  		 div x (pow2 (i-1)) = -2
+
 end