PVS realizations

.gitignore

@@ -129,6 +129,7 @@ why3.conf
 
 # PVS
 .pvscontext
+orphaned-proofs.prf
 /lib/pvs/*/*.summary
 pvsbin/
 

Makefile.in

@@ -970,13 +970,13 @@ clean::
 
 ifeq (@enable_pvs_libs@,yes)
 
-PVSLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
+PVSLIBS_INT_FILES = Int Abs MinMax ComputerDivision EuclideanDivision
 PVSLIBS_INT = $(addprefix lib/pvs/int/, $(PVSLIBS_INT_FILES))
 
-PVSLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square RealInfix
+PVSLIBS_REAL_FILES = Abs FromInt MinMax Real # ExpLog Square RealInfix
 PVSLIBS_REAL = $(addprefix lib/pvs/real/, $(PVSLIBS_REAL_FILES))
 
-PVSLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime
+PVSLIBS_NUMBER_FILES = # Divisibility Gcd Parity Prime
 PVSLIBS_NUMBER = $(addprefix lib/pvs/number/, $(PVSLIBS_NUMBER_FILES))
 
 ifeq (@enable_pvs_fp_libs@,yes)

bin/why3-call-pvs

+#!/bin/bash
+
+export PVS_LIBRARY_PATH=$1/pvs
+exec pvs $2
+
+
+

bin/why3-check-pvs

+#!/bin/bash
+
+export PVS_LIBRARY_PATH=$1/pvs
+cd `dirname $2`
+exec proveit -q `basename $2`
+
+
+

drivers/pvs-common.gen

 
-valid 0
-unknown "Error: \\(.*\\)$" "\\1"
-fail "Syntax error: \\(.*\\)$" "\\1"
+unknown "unfinished" "\"\\0\""
+unknown "untried" "\"\\0\""
+valid "succeeded"
 time "why3cpulimit time : %s s"
 
 (*transformation "inline_trivial"*)

examples/my_cosine/my_cosine_CosineSingle_MethodError_1.v

@@ -11,8 +11,6 @@ Require real.Abs.
 Require real.FromInt.
 Require int.Int.
 Require real.Square.
-Require floating_point.Rounding.
-Require floating_point.Single.
 
 Axiom Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R < PI)%R /\
   (PI < (314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R)%R.
@@ -44,8 +42,111 @@ Parameter atan: R -> R.
 
 Axiom Tan_atan : forall (x:R), ((Rtrigo.tan (atan x)) = x).
 
+(* Why3 assumption *)
+Inductive mode  :=
+  | NearestTiesToEven : mode 
+  | ToZero : mode 
+  | Up : mode 
+  | Down : mode 
+  | NearestTiesToAway : mode .
+
 Parameter single : Type.
 
+Parameter round: mode -> R -> R.
+
+Parameter round_logic: mode -> R -> single.
+
+Parameter value: single -> R.
+
+Parameter exact: single -> R.
+
+Parameter model: single -> R.
+
+(* Why3 assumption *)
+Definition round_error(x:single): R := (Rabs ((value x) - (exact x))%R).
+
+(* Why3 assumption *)
+Definition total_error(x:single): R := (Rabs ((value x) - (model x))%R).
+
+(* Why3 assumption *)
+Definition no_overflow(m:mode) (x:R): Prop := ((Rabs (round m
+  x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
+
+Axiom Bounded_real_no_overflow : forall (m:mode) (x:R),
+  ((Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R ->
+  (no_overflow m x).
+
+Axiom Round_monotonic : forall (m:mode) (x:R) (y:R), (x <= y)%R -> ((round m
+  x) <= (round m y))%R.
+
+Axiom Round_idempotent : forall (m1:mode) (m2:mode) (x:R), ((round m1
+  (round m2 x)) = (round m2 x)).
+
+Axiom Round_value : forall (m:mode) (x:single), ((round m
+  (value x)) = (value x)).
+
+Axiom Bounded_value : forall (x:single),
+  ((Rabs (value x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
+
+Axiom Exact_rounding_for_integers : forall (m:mode) (i:Z),
+  (((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z) -> ((round m
+  (IZR i)) = (IZR i)).
+
+Axiom Round_down_le : forall (x:R), ((round Down x) <= x)%R.
+
+Axiom Round_up_ge : forall (x:R), (x <= (round Up x))%R.
+
+Axiom Round_down_neg : forall (x:R), ((round Down (-x)%R) = (-(round Up
+  x))%R).
+
+Axiom Round_up_neg : forall (x:R), ((round Up (-x)%R) = (-(round Down x))%R).
+
+(* Why3 assumption *)
+Definition of_real_post(m:mode) (x:R) (res:single): Prop :=
+  ((value res) = (round m x)) /\ (((exact res) = x) /\ ((model res) = x)).
+
+(* Why3 assumption *)
+Definition add_post(m:mode) (x:single) (y:single) (res:single): Prop :=
+  ((value res) = (round m ((value x) + (value y))%R)) /\
+  (((exact res) = ((exact x) + (exact y))%R) /\
+  ((model res) = ((model x) + (model y))%R)).
+
+(* Why3 assumption *)
+Definition sub_post(m:mode) (x:single) (y:single) (res:single): Prop :=
+  ((value res) = (round m ((value x) - (value y))%R)) /\
+  (((exact res) = ((exact x) - (exact y))%R) /\
+  ((model res) = ((model x) - (model y))%R)).
+
+(* Why3 assumption *)
+Definition mul_post(m:mode) (x:single) (y:single) (res:single): Prop :=
+  ((value res) = (round m ((value x) * (value y))%R)) /\
+  (((exact res) = ((exact x) * (exact y))%R) /\
+  ((model res) = ((model x) * (model y))%R)).
+
+(* Why3 assumption *)
+Definition div_post(m:mode) (x:single) (y:single) (res:single): Prop :=
+  ((value res) = (round m (Rdiv (value x) (value y))%R)) /\
+  (((exact res) = (Rdiv (exact x) (exact y))%R) /\
+  ((model res) = (Rdiv (model x) (model y))%R)).
+
+(* Why3 assumption *)
+Definition neg_post(x:single) (res:single): Prop :=
+  ((value res) = (-(value x))%R) /\ (((exact res) = (-(exact x))%R) /\
+  ((model res) = (-(model x))%R)).
+
+(* Why3 assumption *)
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+(* Why3 assumption *)
+Definition lt(x:single) (y:single): Prop := ((value x) < (value y))%R.
+
+(* Why3 assumption *)
+Definition gt(x:single) (y:single): Prop := ((value y) < (value x))%R.
+
 Require Import Interval_tactic.
 
 (* Why3 goal *)

examples/my_cosine/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/jc/why3/share/why3session.dtd">
 <why3session
- name="examples/my_cosine/why3session.xml">
+ name="my_cosine/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -16,20 +16,20 @@
   version="0.16.0"/>
  <file
   name="../my_cosine.why"
-  verified="true"
+  verified="false"
   expanded="true">
   <theory
    name="CosineSingle"
-   locfile="examples/my_cosine/../my_cosine.why"
+   locfile="my_cosine/../my_cosine.why"
    loclnum="1" loccnumb="7" loccnume="19"
-   verified="true"
+   verified="false"
    expanded="true">
    <goal
     name="MethodError"
-    locfile="examples/my_cosine/../my_cosine.why"
+    locfile="my_cosine/../my_cosine.why"
     loclnum="13" loccnumb="6" loccnume="17"
     sum="5654505132d0df95fb8d98d86e9154f0"
-    proved="true"
+    proved="false"
     expanded="true"
     shape="ainfix &lt;=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix &lt;=aabsV0c0x1.p-5F">
     <proof
@@ -37,14 +37,14 @@
      timelimit="13"
      memlimit="0"
      edited="my_cosine_CosineSingle_MethodError_1.v"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="3.68"/>
+     obsolete="true"
+     archived="false"><undone/>
+     
     </proof>
    </goal>
    <goal
     name="TotalErrorFullyExpanded"
-    locfile="examples/my_cosine/../my_cosine.why"
+    locfile="my_cosine/../my_cosine.why"
     loclnum="20" loccnumb="6" loccnume="29"
     sum="b272d2bbaa334f583a44d792f1e66da2"
     proved="true"
@@ -61,7 +61,7 @@
    </goal>
    <goal
     name="TotalErrorExpanded"
-    locfile="examples/my_cosine/../my_cosine.why"
+    locfile="my_cosine/../my_cosine.why"
     loclnum="31" loccnumb="6" loccnume="24"
     sum="e8eb30517031d5f9aa29e249a13fcaaf"
     proved="true"
@@ -78,7 +78,7 @@
    </goal>
    <goal
     name="TotalError"
-    locfile="examples/my_cosine/../my_cosine.why"
+    locfile="my_cosine/../my_cosine.why"
     loclnum="51" loccnumb="6" loccnume="16"
     sum="0457c10047c2e650ca89f0b4f6c924e4"
     proved="true"

lib/pvs/int/Abs.prf

+(Abs
+ (abs_le 0
+  (abs_le-1 nil 3551211503 ("" (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)
+    (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))
+   shostak)))
+

lib/pvs/int/Abs.pvs

@@ -9,11 +9,11 @@ Abs: THEORY
   abs(x:int): int = IF (x >= 0) THEN x ELSE (-x) ENDIF
   
   % Why3 abs_le
-  abs_le: AXIOM FORALL (x:int, y:int): (abs(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: AXIOM FORALL (x:int): (abs(x) >= 0)
+  abs_pos: LEMMA FORALL (x:int): (abs(x) >= 0)
   
   
  END Abs

lib/pvs/int/ComputerDivision.pvs

@@ -13,57 +13,57 @@ ComputerDivision: THEORY
   mod(x:int, x1:int): int
   
   % Why3 div_mod
-  div_mod: AXIOM FORALL (x:int, y:int): (NOT (y = 0)) => (x = ((y * div(x,
+  div_mod: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) => (x = ((y * div(x,
     y)) + mod(x, y)))
   
   % Why3 div_bound
-  div_bound: AXIOM FORALL (x:int, y:int): ((x >= 0) AND (y >  0)) =>
+  div_bound: LEMMA FORALL (x:int, y:int): ((x >= 0) AND (y >  0)) =>
     ((0 <= div(x, y)) AND (div(x, y) <= x))
   
   % Why3 mod_bound
-  mod_bound: AXIOM FORALL (x:int, y:int): (NOT (y = 0)) =>
+  mod_bound: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) =>
     (((-abs(y)) <  mod(x, y)) AND (mod(x, y) <  abs(y)))
   
   % Why3 div_sign_pos
-  div_sign_pos: AXIOM FORALL (x:int, y:int): ((x >= 0) AND (y >  0)) =>
+  div_sign_pos: LEMMA FORALL (x:int, y:int): ((x >= 0) AND (y >  0)) =>
     (div(x, y) >= 0)
   
   % Why3 div_sign_neg
-  div_sign_neg: AXIOM FORALL (x:int, y:int): ((x <= 0) AND (y >  0)) =>
+  div_sign_neg: LEMMA FORALL (x:int, y:int): ((x <= 0) AND (y >  0)) =>
     (div(x, y) <= 0)
   
   % Why3 mod_sign_pos
-  mod_sign_pos: AXIOM FORALL (x:int, y:int): ((x >= 0) AND NOT (y = 0)) =>
+  mod_sign_pos: LEMMA FORALL (x:int, y:int): ((x >= 0) AND NOT (y = 0)) =>
     (mod(x, y) >= 0)
   
   % Why3 mod_sign_neg
-  mod_sign_neg: AXIOM FORALL (x:int, y:int): ((x <= 0) AND NOT (y = 0)) =>
+  mod_sign_neg: LEMMA FORALL (x:int, y:int): ((x <= 0) AND NOT (y = 0)) =>
     (mod(x, y) <= 0)
   
   % Why3 rounds_toward_zero
-  rounds_toward_zero: AXIOM FORALL (x:int, y:int): (NOT (y = 0)) =>
+  rounds_toward_zero: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) =>
     (abs((div(x, y) * y)) <= abs(x))
   
   % Why3 div_1
-  div_1: AXIOM FORALL (x:int): (div(x, 1) = x)
+  div_1: LEMMA FORALL (x:int): (div(x, 1) = x)
   
   % Why3 mod_1
-  mod_1: AXIOM FORALL (x:int): (mod(x, 1) = 0)
+  mod_1: LEMMA FORALL (x:int): (mod(x, 1) = 0)
   
   % Why3 div_inf
-  div_inf: AXIOM FORALL (x:int, y:int): ((0 <= x) AND (x <  y)) => (div(x,
+  div_inf: LEMMA FORALL (x:int, y:int): ((0 <= x) AND (x <  y)) => (div(x,
     y) = 0)
   
   % Why3 mod_inf
-  mod_inf: AXIOM FORALL (x:int, y:int): ((0 <= x) AND (x <  y)) => (mod(x,
+  mod_inf: LEMMA FORALL (x:int, y:int): ((0 <= x) AND (x <  y)) => (mod(x,
     y) = x)
   
   % Why3 div_mult
-  div_mult: AXIOM FORALL (x:int, y:int, z:int): ((x >  0) AND ((y >= 0) AND
+  div_mult: LEMMA FORALL (x:int, y:int, z:int): ((x >  0) AND ((y >= 0) AND
     (z >= 0))) => (div(((x * y) + z), x) = (y + div(z, x)))
   
   % Why3 mod_mult
-  mod_mult: AXIOM FORALL (x:int, y:int, z:int): ((x >  0) AND ((y >= 0) AND
+  mod_mult: LEMMA FORALL (x:int, y:int, z:int): ((x >  0) AND ((y >= 0) AND
     (z >= 0))) => (mod(((x * y) + z), x) = mod(z, x))
   
   

lib/pvs/int/EuclideanDivision.pvs

+EuclideanDivision: THEORY
+ BEGIN
+  IMPORTING Int
+  IMPORTING Abs
+  
+  % Why3 tuple0
+  tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
+  
+  % Why3 div
+  div(x:int, x1:int): int
+  
+  % Why3 mod
+  mod(x:int, x1:int): int
+  
+  % Why3 div_mod
+  div_mod: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) => (x = ((y * div(x,
+    y)) + mod(x, y)))
+  
+  % Why3 div_bound
+  div_bound: LEMMA FORALL (x:int, y:int): ((x >= 0) AND (y >  0)) =>
+    ((0 <= div(x, y)) AND (div(x, y) <= x))
+  
+  % Why3 mod_bound
+  mod_bound: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) => ((0 <= mod(x,
+    y)) AND (mod(x, y) <  abs(y)))
+  
+  % Why3 mod_1
+  mod_1: LEMMA FORALL (x:int): (mod(x, 1) = 0)
+  
+  % Why3 div_1
+  div_1: LEMMA FORALL (x:int): (div(x, 1) = x)
+  
+  % Why3 div_inf
+  div_inf: LEMMA FORALL (x:int, y:int): ((0 <= x) AND (x <  y)) => (div(x,
+    y) = 0)
+  
+  % Why3 div_inf_neg
+  div_inf_neg: LEMMA FORALL (x:int, y:int): ((0 <  x) AND (x <= y)) =>
+    (div((-x), y) = (-1))
+  
+  % Why3 mod_0
+  mod_0: LEMMA FORALL (y:int): (NOT (y = 0)) => (mod(0, y) = 0)
+  
+  % Why3 div_1_left
+  div_1_left: LEMMA FORALL (y:int): (y >  1) => (div(1, y) = 0)
+  
+  % Why3 div_minus1_left
+  div_minus1_left: LEMMA FORALL (y:int): (y >  1) => (div((-1), y) = (-1))
+  
+  % Why3 mod_1_left
+  mod_1_left: LEMMA FORALL (y:int): (y >  1) => (mod(1, y) = 1)
+  
+  % Why3 mod_minus1_left
+  mod_minus1_left: LEMMA FORALL (y:int): (y >  1) => (mod((-1), y) = (y - 1))
+  
+  
+ END EuclideanDivision
+ 
\ No newline at end of file

lib/pvs/int/MinMax.prf

+(MinMax
+ (max_is_ge 0
+  (max_is_ge-1 nil 3551211318 ("" (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_lt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
+   shostak))
+ (max_is_some 0
+  (max_is_some-1 nil 3551211339 ("" (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_lt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
+   shostak))
+ (min_is_le 0
+  (min_is_le-1 nil 3551211351 ("" (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_gt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
+   shostak))
+ (min_is_some 0
+  (min_is_some-1 nil 3551211366 ("" (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_gt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
+   shostak))
+ (max_x 0
+  (max_x-1 nil 3551211390 ("" (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)
+    (real_lt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
+   shostak))
+ (max_y 0
+  (max_y-1 nil 3551211393 ("" (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)
+    (real_lt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
+   shostak))
+ (min_x 0
+  (min_x-1 nil 3551211397 ("" (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)
+    (real_gt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
+   shostak))
+ (min_y 0
+  (min_y-1 nil 3551211425 ("" (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)
+    (real_gt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
+   shostak))
+ (max_sym 0
+  (max_sym-1 nil 3551211430 ("" (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)
+    (real_lt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
+   shostak))
+ (min_sym 0
+  (min_sym-1 nil 3551211433 ("" (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)
+    (real_gt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
+   shostak)))
+

lib/pvs/int/MinMax.pvs

+MinMax: THEORY
+ BEGIN
+  IMPORTING Int
+  
+  % Why3 tuple0
+  tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
+  
+  % Why3 min
+  min(x:int, x1:int): MACRO int = min(x, x1)
+  
+  % Why3 max
+  max(x:int, x1:int): MACRO int = max(x, x1)
+  
+  % Why3 max_is_ge
+  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): (max(x, y) = x) OR (max(x,
+    y) = y)
+  
+  % Why3 min_is_le
+  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): (min(x, y) = x) OR (min(x,
+    y) = y)
+  
+  % Why3 max_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) => (max(x, y) = y)
+  
+  % Why3 min_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) => (min(x, y) = y)
+  
+  % Why3 max_sym
+  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) => (min(x, y) = min(y, x))
+