PVS realizations updated

parent 552d1606
......@@ -14,30 +14,12 @@
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs const-decl "int" Abs nil))
shostak))
(abs_pos 0
(abs_pos-1 nil 3551211508 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs const-decl "int" Abs nil))
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil))
shostak)))
......@@ -3,16 +3,12 @@ Abs: THEORY
IMPORTING Int
% do not edit above this line
% Why3 abs1
abs1(x:int): int = IF (x >= 0) THEN x ELSE (-x) ENDIF
% Why3 abs_le
abs_le: LEMMA FORALL (x:int, y:int): (abs1(x) <= y) <=> (((-y) <= x) AND
abs_le: LEMMA FORALL (x:int, y:int): (abs(x) <= y) <=> (((-y) <= x) AND
(x <= y))
% Why3 abs_pos
abs_pos: LEMMA FORALL (x:int): (abs1(x) >= 0)
% Obsolete chunk abs_pos
% abs_pos: LEMMA FORALL (x:int): (abs1(x) >= 0)
END Abs
\ No newline at end of file
(EuclideanDivision
(div_mod 0
(div_mod-1 nil 3551625869 ("" (default-strategy))
((mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod "ints/")
(tdiv const-decl "integer" tdiv "ints/")
(/= const-decl "boolean" notequal nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
((mod const-decl "{k | abs(k) < abs(j)}" tmod "ints/")
(tdiv const-decl "integer" tdiv "ints/"))
shostak))
(div_bound 0
(div_bound-1 nil 3551625870 ("" (default-strategy)) nil shostak))
......@@ -35,24 +15,8 @@
nil shostak))
(mod_1 0
(mod_1-1 nil 3551625870 ("" (default-strategy))
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod "ints/")
(tdiv const-decl "integer" tdiv "ints/")
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
((mod const-decl "{k | abs(k) < abs(j)}" tmod "ints/")
(tdiv const-decl "integer" tdiv "ints/"))
shostak))
(div_1 0
(div_1-1 nil 3551625870 ("" (default-strategy))
......@@ -79,25 +43,7 @@
(mod_0 0
(mod_0-1 nil 3551625871 ("" (default-strategy))
((mod const-decl "{k | abs(k) < abs(j)}" tmod "ints/")
(tdiv const-decl "integer" tdiv "ints/")
(/= const-decl "boolean" notequal nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
(tdiv const-decl "integer" tdiv "ints/"))
shostak))
(div_1_left 0
(div_1_left-1 nil 3551625871 ("" (default-strategy)) nil shostak))
......
......@@ -59,6 +59,14 @@ EuclideanDivision: THEORY
mod_minus1_left: LEMMA FORALL (y:int): (y > 1) => (mod1((-1),
y) = (y - 1))
% Why3 div_mult
div_mult: LEMMA FORALL (x:int, y:int, z:int): (x > 0) =>
(div(((x * y) + z), x) = (y + div(z, x)))
% Why3 mod_mult
mod_mult: LEMMA FORALL (x:int, y:int, z:int): (x > 0) =>
(mod1(((x * y) + z), x) = mod1(z, x))
END EuclideanDivision
\ No newline at end of file
......@@ -2,91 +2,60 @@ Int: THEORY
BEGIN
% do not edit above this line
% Why3 zero
zero: int = 0
% Obsolete chunk unit_def
% unit_def: LEMMA FORALL (x:int): (infix_pl(x, zero) = x)
% Why3 one
one: int = 1
% Obsolete chunk assoc
% assoc: LEMMA FORALL (x:int, y:int, z:int): (infix_pl(infix_pl(x, y),
% z) = infix_pl(x, infix_pl(y, z)))
% Why3 infix_ls
infix_ls(x:int, x1:int): MACRO bool = x<x1
% Obsolete chunk inv_def
% inv_def: LEMMA FORALL (x:int): (infix_pl(x, prefix_mn(x)) = zero)
% Why3 infix_gt
infix_gt(x:int, y:int): bool = infix_ls(y, x)
% Obsolete chunk comm
% comm: LEMMA FORALL (x:int, y:int): (infix_pl(x, y) = infix_pl(y, x))
% Why3 infix_lseq
infix_lseq(x:int, y:int): bool = infix_ls(x, y) OR (x = y)
% Obsolete chunk assoc1
% assoc1: LEMMA FORALL (x:int, y:int, z:int): (infix_as(infix_as(x, y),
% z) = infix_as(x, infix_as(y, z)))
% Why3 infix_pl
infix_pl(x:int, x1:int): MACRO int = x+x1
% Obsolete chunk mul_distr
% mul_distr: LEMMA FORALL (x:int, y:int, z:int): (infix_as(x, infix_pl(y,
% z)) = infix_pl(infix_as(x, y), infix_as(x, z)))
% Why3 prefix_mn
prefix_mn(x:int): MACRO int = -x
% Obsolete chunk comm1
% comm1: LEMMA FORALL (x:int, y:int): (infix_as(x, y) = infix_as(y, x))
% Why3 infix_as
infix_as(x:int, x1:int): MACRO int = x*x1
% Obsolete chunk unitary
% unitary: LEMMA FORALL (x:int): (infix_as(one, x) = x)
% Why3 unit_def
unit_def: LEMMA FORALL (x:int): (infix_pl(x, zero) = x)
% Obsolete chunk nontrivialring
% nontrivialring: LEMMA NOT (zero = one)
% Why3 assoc
assoc: LEMMA FORALL (x:int, y:int, z:int): (infix_pl(infix_pl(x, y),
z) = infix_pl(x, infix_pl(y, z)))
% Obsolete chunk refl
% refl: LEMMA FORALL (x:int): infix_lseq(x, x)
% Why3 inv_def
inv_def: LEMMA FORALL (x:int): (infix_pl(x, prefix_mn(x)) = zero)
% Obsolete chunk trans
% trans: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
% (infix_lseq(y, z) => infix_lseq(x, z))
% Why3 comm
comm: LEMMA FORALL (x:int, y:int): (infix_pl(x, y) = infix_pl(y, x))
% Obsolete chunk antisymm
% antisymm: LEMMA FORALL (x:int, y:int): infix_lseq(x, y) => (infix_lseq(y,
% x) => (x = y))
% Why3 assoc1
assoc1: LEMMA FORALL (x:int, y:int, z:int): (infix_as(infix_as(x, y),
z) = infix_as(x, infix_as(y, z)))
% Obsolete chunk total
% total: LEMMA FORALL (x:int, y:int): infix_lseq(x, y) OR infix_lseq(y, x)
% Why3 mul_distr
mul_distr: LEMMA FORALL (x:int, y:int, z:int): (infix_as(x, infix_pl(y,
z)) = infix_pl(infix_as(x, y), infix_as(x, z)))
% Obsolete chunk zerolessone
% zerolessone: LEMMA infix_lseq(zero, one)
% Why3 infix_mn
infix_mn(x:int, y:int): int = infix_pl(x, prefix_mn(y))
% Why3 comm1
comm1: LEMMA FORALL (x:int, y:int): (infix_as(x, y) = infix_as(y, x))
% Why3 unitary
unitary: LEMMA FORALL (x:int): (infix_as(one, x) = x)
% Why3 nontrivialring
nontrivialring: LEMMA NOT (zero = one)
% Why3 infix_gteq
infix_gteq(x:int, y:int): bool = infix_lseq(y, x)
% Why3 refl
refl: LEMMA FORALL (x:int): infix_lseq(x, x)
% Why3 trans
trans: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
(infix_lseq(y, z) => infix_lseq(x, z))
% Why3 antisymm
antisymm: LEMMA FORALL (x:int, y:int): infix_lseq(x, y) => (infix_lseq(y,
x) => (x = y))
% Why3 total
total: LEMMA FORALL (x:int, y:int): infix_lseq(x, y) OR infix_lseq(y, x)
% Why3 zerolessone
zerolessone: LEMMA infix_lseq(zero, one)
% Why3 compatorderadd
compatorderadd: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
infix_lseq(infix_pl(x, z), infix_pl(y, z))
% Why3 compatordermult
compatordermult: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
(infix_lseq(zero, z) => infix_lseq(infix_as(x, z), infix_as(y, z)))
% Obsolete chunk compatorderadd
% compatorderadd: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
% infix_lseq(infix_pl(x, z), infix_pl(y, z))
% Obsolete chunk compatordermult
% compatordermult: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
% (infix_lseq(zero, z) => infix_lseq(infix_as(x, z), infix_as(y, z)))
END Int
\ No newline at end of file
......@@ -3,45 +3,39 @@ MinMax: THEORY
IMPORTING Int
% do not edit above this line
% Why3 min1
min1(x:int, x1:int): int
% Why3 max1
max1(x:int, x1:int): int
% Why3 max_is_ge
max_is_ge: LEMMA FORALL (x:int, y:int): (max1(x, y) >= x) AND (max1(x,
y) >= y)
max_is_ge: LEMMA FORALL (x:int, y:int): (max(x, y) >= x) AND
(max(x, y) >= y)
% Why3 max_is_some
max_is_some: LEMMA FORALL (x:int, y:int): (max1(x, y) = x) OR (max1(x,
y) = y)
max_is_some: LEMMA FORALL (x:int, y:int): (max(x, y) = x) OR
(max(x, y) = y)
% Why3 min_is_le
min_is_le: LEMMA FORALL (x:int, y:int): (x >= min1(x, y)) AND (y >= min1(x,
y))
min_is_le: LEMMA FORALL (x:int, y:int): (x >= min(x, y)) AND
(y >= min(x, y))
% Why3 min_is_some
min_is_some: LEMMA FORALL (x:int, y:int): (min1(x, y) = x) OR (min1(x,
y) = y)
min_is_some: LEMMA FORALL (x:int, y:int): (min(x, y) = x) OR
(min(x, y) = y)
% Why3 max_x
max_x: LEMMA FORALL (x:int, y:int): (x >= y) => (max1(x, y) = x)
max_x: LEMMA FORALL (x:int, y:int): (x >= y) => (max(x, y) = x)
% Why3 max_y
max_y: LEMMA FORALL (x:int, y:int): (y >= x) => (max1(x, y) = y)
max_y: LEMMA FORALL (x:int, y:int): (y >= x) => (max(x, y) = y)
% Why3 min_x
min_x: LEMMA FORALL (x:int, y:int): (y >= x) => (min1(x, y) = x)
min_x: LEMMA FORALL (x:int, y:int): (y >= x) => (min(x, y) = x)
% Why3 min_y
min_y: LEMMA FORALL (x:int, y:int): (x >= y) => (min1(x, y) = y)
min_y: LEMMA FORALL (x:int, y:int): (x >= y) => (min(x, y) = y)
% Why3 max_sym
max_sym: LEMMA FORALL (x:int, y:int): (x >= y) => (max1(x, y) = max1(y, x))
max_sym: LEMMA FORALL (x:int, y:int): (x >= y) => (max(x, y) = max(y, x))
% Why3 min_sym
min_sym: LEMMA FORALL (x:int, y:int): (x >= y) => (min1(x, y) = min1(y, x))
min_sym: LEMMA FORALL (x:int, y:int): (x >= y) => (min(x, y) = min(y, x))
END MinMax
(Abs
(abs_le 0
(abs_le-1 nil 3551212620 ("" (default-strategy))
((abs1 const-decl "real" Abs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(abs_pos 0
(abs_pos-1 nil 3551212620 ("" (default-strategy))
((abs1 const-decl "real" Abs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(abs_sum 0
(abs_sum-1 nil 3551212620 ("" (default-strategy))
((abs1 const-decl "real" Abs nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
......@@ -44,6 +14,7 @@
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(abs_prod 0
......@@ -59,11 +30,11 @@
nil shostak))
(triangular_inequality 0
(triangular_inequality-1 nil 3551212620 ("" (default-strategy))
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(abs1 const-decl "real" Abs nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
......@@ -72,6 +43,7 @@
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak)))
......@@ -3,28 +3,22 @@ Abs: THEORY
IMPORTING Real
% do not edit above this line
% Why3 abs1
abs1(x:real): real = IF (x >= 0) THEN x ELSE (-x) ENDIF
% Why3 abs_le
abs_le: LEMMA FORALL (x:real, y:real): (abs1(x) <= y) <=> (((-y) <= x) AND
(x <= y))
% Why3 abs_pos
abs_pos: LEMMA FORALL (x:real): (abs1(x) >= 0)
% Why3 abs_sum
abs_sum: LEMMA FORALL (x:real, y:real):
(abs1((x + y)) <= (abs1(x) + abs1(y)))
abs_sum: LEMMA FORALL (x:real, y:real): (abs((x + y)) <= (abs(x) + abs(y)))
% Why3 abs_prod
abs_prod: LEMMA FORALL (x:real, y:real):
(abs1((x * y)) = (abs1(x) * abs1(y)))
abs_prod: LEMMA FORALL (x:real, y:real): (abs((x * y)) = (abs(x) * abs(y)))
% Why3 triangular_inequality
triangular_inequality: LEMMA FORALL (x:real, y:real, z:real):
(abs1((x - z)) <= (abs1((x - y)) + abs1((y - z))))
(abs((x - z)) <= (abs((x - y)) + abs((y - z))))
% Obsolete chunk abs_le
% abs_le: LEMMA FORALL (x:real, y:real): (abs1(x) <= y) <=> (((-y) <= x) AND
% (x <= y))
% Obsolete chunk abs_pos
% abs_pos: LEMMA FORALL (x:real): (abs1(x) >= 0)
END Abs
\ No newline at end of file
......@@ -8,6 +8,7 @@
(log_TCC1 0
(log_TCC1-1 nil 3552164963 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
......@@ -29,6 +30,7 @@
(log_mul_TCC1 0
(log_mul_TCC1-1 nil 3552164963 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
......@@ -45,6 +47,7 @@
(log_mul_TCC2 0
(log_mul_TCC2-1 nil 3552164963 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
......@@ -62,6 +65,7 @@
(log_exp_TCC1 0
(log_exp_TCC1-1 nil 3552164963 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
......@@ -85,6 +89,7 @@
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(exp_log 0
......
......@@ -17,6 +17,8 @@ ExpLog: THEORY
% Why3 e
e: real = exp(1)
log_total(x: real): real
% Why3 log
log(x:real): MACRO real = IF x > 0 THEN ln(x) ELSE log_total(x) ENDIF
......@@ -41,4 +43,4 @@ ExpLog: THEORY
END ExpLog
\ No newline at end of file
......@@ -4,30 +4,26 @@ FromInt: THEORY
IMPORTING Real
% do not edit above this line
% Why3 from_int
from_int(x:int): MACRO real = x
% Obsolete chunk zero
% zero: LEMMA (from_int(0) = 0)
% Why3 zero
zero: LEMMA (from_int(0) = 0)
% Obsolete chunk one
% one: LEMMA (from_int(1) = 1)
% Why3 one
one: LEMMA (from_int(1) = 1)
% Obsolete chunk add1
% add1: LEMMA FORALL (x:int, y:int):
% (from_int((x + y)) = (from_int(x) + from_int(y)))
% Why3 add1
add1: LEMMA FORALL (x:int, y:int):
(from_int((x + y)) = (from_int(x) + from_int(y)))
% Obsolete chunk sub
% sub: LEMMA FORALL (x:int, y:int):
% (from_int((x - y)) = (from_int(x) - from_int(y)))
% Why3 sub
sub: LEMMA FORALL (x:int, y:int):
(from_int((x - y)) = (from_int(x) - from_int(y)))
% Why3 mul
mul: LEMMA FORALL (x:int, y:int):
(from_int((x * y)) = (from_int(x) * from_int(y)))
% Why3 neg
neg: LEMMA FORALL (x:int): (from_int((-x)) = (-from_int(x)))
% Obsolete chunk mul
% mul: LEMMA FORALL (x:int, y:int):
% (from_int((x * y)) = (from_int(x) * from_int(y)))
% Obsolete chunk neg
% neg: LEMMA FORALL (x:int): (from_int((-x)) = (-from_int(x)))
END FromInt
\ No newline at end of file
......@@ -3,28 +3,21 @@ MinMax: THEORY
IMPORTING Real
% do not edit above this line
% Why3 min1
min1(x:real, x1:real): real
% Obsolete chunk max_is_ge
% max_is_ge: LEMMA FORALL (x:real, y:real): (max1(x, y) >= x) AND (max1(x,
% y) >= y)
% Why3 max1
max1(x:real, x1:real): real
% Obsolete chunk max_is_some
% max_is_some: LEMMA FORALL (x:real, y:real): (max1(x, y) = x) OR (max1(x,
% y) = y)
% Why3 max_is_ge
max_is_ge: LEMMA FORALL (x:real, y:real): (max1(x, y) >= x) AND (max1(x,
y) >= y)
% Why3 max_is_some
max_is_some: LEMMA FORALL (x:real, y:real): (max1(x, y) = x) OR (max1(x,
y) = y)
% Why3 min_is_le
min_is_le: LEMMA FORALL (x:real, y:real): (min1(x, y) <= x) AND (min1(x,
y) <= y)
% Why3 min_is_some
min_is_some: LEMMA FORALL (x:real, y:real): (min1(x, y) = x) OR (min1(x,
y) = y)
% Obsolete chunk min_is_le
% min_is_le: LEMMA FORALL (x:real, y:real): (min1(x, y) <= x) AND (min1(x,
% y) <= y)
% Obsolete chunk min_is_some
% min_is_some: LEMMA FORALL (x:real, y:real): (min1(x, y) = x) OR (min1(x,
% y) = y)
END MinMax
\ No newline at end of file
This diff is collapsed.
......@@ -4,11 +4,17 @@ PowerInt: THEORY
IMPORTING Real
% do not edit above this line
% Why3 infix_sldt
infix_sldt(x:real, y:real): real = Real.infix_sl(x, y)
% Why3 inv
inv(x:real): real = Real.inv(x)
power_total(x: int) : real
% Why3 power
power(x:real, x1:int): MACRO real =
IF x = 0 AND x1 < 0 THEN power_total(x1) ELSE x^x1 ENDIF
power(x:real,
x1:int): MACRO real = IF x = 0 AND x1 < 0 THEN power_total(x1) ELSE x^x1 ENDIF
% Why3 power_0
power_0: LEMMA FORALL (x:real): (power(x, 0) = 1)
......@@ -17,17 +23,29 @@ PowerInt: THEORY
power_s: LEMMA FORALL (x:real, n:int): (n >= 0) => (power(x,
(n + 1)) = (x * power(x, n)))
% Why3 power_s_alt
power_s_alt: LEMMA FORALL (x:real, n:int): (n > 0) => (power(x,
n) = (x * power(x, (n - 1))))
% Why3 power_1
power_1: LEMMA FORALL (x:real): (power(x, 1) = x)
% Why3 power_sum
power_sum: LEMMA FORALL (x:real, n:int, m:int): ((n >= 0) AND (m >= 0)) =>
(power(x, (n + m)) = (power(x, n) * power(x, m)))
power_sum: LEMMA FORALL (x:real, n:int, m:int): (0 <= n) => ((0 <= m) =>
(power(x, (n + m)) = (power(x, n) * power(x, m))))
% Why3 power_mult
power_mult: LEMMA FORALL (x:real, n:int, m:int): (0 <= n) => ((0 <= m) =>
(power(x, (n * m)) = power(power(x, n), m)))
% Why3 power_mult2
power_mult2: LEMMA FORALL (x:real, y:real, n:int): (0 <= n) =>
(power((x * y), n) = (power(x, n) * power(y, n)))
% Why3 pow_ge_one
pow_ge_one: LEMMA FORALL (x:real, n:int): ((0 <= n) AND (1 <= x)) =>
(1 <= power(x, n))
END PowerInt
\ No newline at end of file
This diff is collapsed.
......@@ -2,127 +2,96 @@ Real: THEORY
BEGIN
% do not edit above this line
% Why3 zero
zero: real = 0
% Why3 one
one: real = 1
% Why3 infix_ls
infix_ls(x:real, x1:real): MACRO bool = x<x1
% Why3 infix_gt
infix_gt(x:real, y:real): bool = infix_ls(y, x)
% Why3 infix_lseq
infix_lseq(x:real, y:real): bool = infix_ls(x, y) OR (x = y)
% Why3 infix_pl
infix_pl(x:real, x1:real): MACRO real = x+x1
% Why3 prefix_mn
prefix_mn(x:real): MACRO real = -x
% Why3 infix_as
infix_as(x:real, x1:real): MACRO real = x*x1
% Why3 unit_def
unit_def: LEMMA FORALL (x:real): (infix_pl(x, zero) = x)
% Why3 assoc
assoc: LEMMA FORALL (x:real, y:real, z:real): (infix_pl(infix_pl(x, y),
z) = infix_pl(x, infix_pl(y, z)))
% Why3 inv_def
inv_def: LEMMA FORALL (x:real): (infix_pl(x, prefix_mn(x)) = zero)
% Why3 comm
comm: LEMMA FORALL (x:real, y:real): (infix_pl(x, y) = infix_pl(y, x))
% Why3 inv
inv(x:real): MACRO real = IF x /= 0 THEN 1/x ELSE 0 ENDIF % make it total using 0
% Why3 assoc1
assoc1: LEMMA FORALL (x:real, y:real, z:real): (infix_as(infix_as(x, y),
z) = infix_as(x, infix_as(y, z)))
% Why3 infix_sl
infix_sl(x:real, y:real): real = (x * inv(y))
% Why3 mul_distr
mul_distr: LEMMA FORALL (x:real, y:real, z:real): (infix_as(x, infix_pl(y,
z)) = infix_pl(infix_as(x, y), infix_as(x, z)))
% Why3 add_div
add_div: LEMMA FORALL (x:real, y:real, z:real): (NOT (z = 0)) =>
(infix_sl((x + y), z) = (infix_sl(x, z) + infix_sl(y, z)))
% Why3 infix_mn
infix_mn(x:real, y:real): real = infix_pl(x, prefix_mn(y))
% Why3 sub_div
sub_div: LEMMA FORALL (x:real, y:real, z:real): (NOT (z = 0)) =>
(infix_sl((x - y), z) = (infix_sl(x, z) - infix_sl(y, z)))
% Why3 comm1
comm1: LEMMA FORALL (x:real, y:real): (infix_as(x, y) = infix_as(y, x))
% Why3 neg_div
neg_div: LEMMA FORALL (x:real, y:real): (NOT (y = 0)) => (infix_sl((-x),
y) = (-infix_sl(x, y)))
% Why3 unitary
unitary: LEMMA FORALL (x:real): (infix_as(one, x) = x)
% Obsolete chunk unit_def
% unit_def: LEMMA FORALL (x:real): (infix_pl(x, zero) = x)
% Why3 nontrivialring
nontrivialring: LEMMA NOT (zero = one)
% Obsolete chunk assoc
% assoc: LEMMA FORALL (x:real, y:real, z:real): (infix_pl(infix_pl(x, y),
% z) = infix_pl(x, infix_pl(y, z)))
% Why3 inv
inv(x:real): MACRO real = IF x /= 0 THEN 1/x ELSE 0 ENDIF % make it total using 0
% Obsolete chunk inv_def
% inv_def: LEMMA FORALL (x:real): (infix_pl(x, prefix_mn(x)) = zero)
% Why3 inverse
inverse: LEMMA FORALL (x:real): (NOT (x = zero)) => (infix_as(x,
inv(x)) = one)
% Obsolete chunk comm
% comm: LEMMA FORALL (x:real, y:real): (infix_pl(x, y) = infix_pl(y, x))
% Why3 infix_sl
infix_sl(x:real, y:real): real = infix_as(x, inv(y))
% Obsolete chunk assoc1
% assoc1: LEMMA FORALL (x:real, y:real, z:real): (infix_as(infix_as(x, y),
% z) = infix_as(x, infix_as(y, z)))
% Why3 add_div
add_div: LEMMA FORALL (x:real, y:real, z:real): (NOT (z = zero)) =>
(infix_sl(infix_pl(x, y), z) = infix_pl(infix_sl(x, z), infix_sl(y, z)))
% Obsolete chunk mul_distr
% mul_distr: LEMMA FORALL (x:real, y:real, z:real): (infix_as(x, infix_pl(y,
% z)) = infix_pl(infix_as(x, y), infix_as(x, z)))
% Why3 sub_div
sub_div: LEMMA FORALL (x:real, y:real, z:real): (NOT (z = zero)) =>
(infix_sl(infix_mn(x, y), z) = infix_mn(infix_sl(x, z), infix_sl(y, z)))
% Obsolete chunk comm1
% comm1: LEMMA FORALL (x:real, y:real): (infix_as(x, y) = infix_as(y, x))
% Why3 neg_div
neg_div: LEMMA FORALL (x:real, y:real): (NOT (y = zero)) =>
(infix_sl(prefix_mn(x), y) = prefix_mn(infix_sl(x, y)))
% Obsolete chunk unitary
% unitary: LEMMA FORALL (x:real): (infix_as(one, x) = x)
% Why3 assoc_mul_div
assoc_mul_div: LEMMA FORALL (x:real, y:real, z:real): (NOT (z = zero)) =>
(infix_sl(infix_as(x, y), z) = infix_as(x, infix_sl(y, z)))
% Obsolete chunk nontrivialring
% nontrivialring: LEMMA NOT (zero = one)
% Why3 assoc_div_mul
assoc_div_mul: LEMMA FORALL (x:real, y:real, z:real): ((NOT (y = zero)) AND