Commit 74208e03 by MARCHE Claude

### upgrade provers in (part of) the sessions

parent a0c76576
 ... ... @@ -3,16 +3,16 @@ "http://why3.lri.fr/why3session.dtd"> ... ...
 ... ... @@ -2,9 +2,9 @@ ... ... @@ -37,7 +37,7 @@ ... ... @@ -61,11 +61,11 @@ ... ...
 ... ... @@ -3,11 +3,11 @@ "http://why3.lri.fr/why3session.dtd"> ... ...
 ... ... @@ -2,87 +2,87 @@ ... ...
This diff is collapsed.
 ... ... @@ -149,15 +149,19 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z). Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z). Axiom Div_double : forall (x:Z) (y:Z), (((0%Z < y)%Z /\ (y <= x)%Z) /\ (x < (2%Z * y)%Z)%Z) -> ((int.EuclideanDivision.div x y) = 1%Z). Axiom Div_mult_inst : forall (x:Z) (z:Z), (0%Z < x)%Z -> ((int.EuclideanDivision.div ((x * 1%Z)%Z + z)%Z x) = (1%Z + (int.EuclideanDivision.div z x))%Z). Axiom Div_double : forall (x:Z) (y:Z), ((0%Z < y)%Z /\ ((y <= x)%Z /\ (x < (2%Z * y)%Z)%Z)) -> ((int.EuclideanDivision.div x y) = 1%Z). Axiom Div_pow : forall (x:Z) (i:Z), (0%Z < i)%Z -> ((((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z)). Axiom Div_double_neg : forall (x:Z) (y:Z), (((((-2%Z)%Z * y)%Z <= x)%Z /\ (x < (-y)%Z)%Z) /\ ((-y)%Z < 0%Z)%Z) -> ((int.EuclideanDivision.div x Axiom Div_double_neg : forall (x:Z) (y:Z), ((((-2%Z)%Z * y)%Z <= x)%Z /\ ((x < (-y)%Z)%Z /\ ((-y)%Z < 0%Z)%Z)) -> ((int.EuclideanDivision.div x y) = (-2%Z)%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (0%Z < i)%Z -> ... ... @@ -198,21 +202,24 @@ Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2). Parameter bw_and: bv -> bv -> bv. Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))). (n < size)%Z) -> ((nth (bw_and v1 v2) n) = (Init.Datatypes.andb (nth v1 n) (nth v2 n))). Parameter bw_or: bv -> bv -> bv. Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))). (n < size)%Z) -> ((nth (bw_or v1 v2) n) = (Init.Datatypes.orb (nth v1 n) (nth v2 n))). Parameter bw_xor: bv -> bv -> bv. Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))). (n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (Init.Datatypes.xorb (nth v1 n) (nth v2 n))). Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ (n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2) n) = (negb (nth v2 n))). n) = (Init.Datatypes.negb (nth v2 n))). Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ (n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2 ... ... @@ -220,7 +227,7 @@ Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ (n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2) n) = (negb (nth v1 n))). n) = (Init.Datatypes.negb (nth v1 n))). Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ (n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1 ... ... @@ -229,7 +236,7 @@ Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ Parameter bw_not: bv -> bv. Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_not v) n) = (negb (nth v n))). ((nth (bw_not v) n) = (Init.Datatypes.negb (nth v n))). Parameter lsr: bv -> Z -> bv. ... ... @@ -263,19 +270,19 @@ Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ Parameter to_nat_sub: bv -> Z -> Z -> Z. Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), ((0%Z <= i)%Z /\ ((i <= j)%Z /\ (j < size)%Z)) -> (((nth b j) = false) -> ((to_nat_sub b j i) = (to_nat_sub b (j - 1%Z)%Z i))). Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), ((0%Z <= i)%Z /\ ((i <= j)%Z /\ (j < size)%Z)) -> (((nth b j) = true) -> ((to_nat_sub b j i) = ((pow2 (j - i)%Z) + (to_nat_sub b (j - 1%Z)%Z i))%Z)). Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z -> ((to_nat_sub b j i) = 0%Z). Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\ (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\ ((i <= j)%Z /\ (0%Z <= i)%Z)) -> ((forall (k:Z), ((k <= j)%Z /\ (i < k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j 0%Z) = (to_nat_sub b i 0%Z))). ... ... @@ -286,14 +293,14 @@ Open Scope Z_scope. Theorem to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j i) = 0%Z)). (* Why3 intros b i j (h1,h2) h3. *) (* intros b i j (h1,h2) h3. *) intros b i j (Hj & Hi). assert (h:(i>j)\/(i<=j)) by omega; destruct h. why3 "Alt-Ergo,0.95.1," timelimit 2. why3 "Alt-Ergo,0.99.1," timelimit 2. generalize Hj. pattern j. apply Zlt_lower_bound_ind with (z:=i); auto. why3 "CVC3,2.4.1,". Qed.
This diff is collapsed.
This diff is collapsed.
 ... ... @@ -2,14 +2,14 @@ ... ... @@ -18,35 +18,35 @@ ... ... @@ -62,36 +62,36 @@ ... ... @@ -100,8 +100,8 @@ ... ...
 ... ... @@ -2,44 +2,44 @@ ... ...
 ... ... @@ -2,11 +2,11 @@ ... ...
 ... ... @@ -2,13 +2,13 @@ ... ...
 ... ... @@ -2,11 +2,11 @@ ... ...
 ... ... @@ -2,14 +2,14 @@ ... ...
 ... ... @@ -3,43 +3,43 @@ "http://why3.lri.fr/why3session.dtd">