more PVS realizations

Makefile.in

@@ -973,7 +973,9 @@ ifeq (@enable_pvs_libs@,yes)
 PVSLIBS_INT_FILES = Int Abs MinMax ComputerDivision EuclideanDivision
 PVSLIBS_INT = $(addprefix lib/pvs/int/, $(PVSLIBS_INT_FILES))
 
-PVSLIBS_REAL_FILES = Abs FromInt MinMax Real # ExpLog Square RealInfix
+PVSLIBS_REAL_FILES = Abs FromInt MinMax Real Square ExpLog Trigonometry \
+                     PowerInt
+ # RealInfix
 PVSLIBS_REAL = $(addprefix lib/pvs/real/, $(PVSLIBS_REAL_FILES))
 
 PVSLIBS_LIST_FILES =

drivers/pvs-common.gen

@@ -25,11 +25,6 @@ theory BuiltIn
   syntax predicate  (=)   "(%1 = %2)"
 end
 
-theory Tuple0
-  syntax type     tuple0 "tuple0"
-  syntax function Tuple0 "Tuple0"
-end
-
 theory map.Map
   syntax type  map "[%1 -> %2]"
 
@@ -202,6 +197,17 @@ theory real.FromInt
 
 end
 
+theory real.PowerReal
+
+  syntax function pow "(%1 ^ %2)"
+
+  remove prop Pow_x_zero
+  remove prop Pow_x_one
+  remove prop Pow_one_y
+
+end
+
+(***
 theory real.Square
 
   syntax function sqrt "SQRT(%1)"
@@ -215,16 +221,6 @@ theory real.ExpLog
 
 end
 
-theory real.PowerReal
-
-  syntax function pow "(%1 ^ %2)"
-
-  remove prop Pow_x_zero
-  remove prop Pow_x_one
-  remove prop Pow_one_y
-
-end
-
 theory real.Trigonometry
 
   syntax function cos "COS(%1)"
@@ -235,6 +231,7 @@ theory real.Trigonometry
   syntax function tan "TAN(%1)"
 
 end
+***)
 
 theory option.Option
   syntax type option "lift[%1]"
@@ -260,6 +257,7 @@ end
 
 theory list.Mem
   syntax predicate mem "member(%1, %2)"
+  
 end
 
 theory list.Nth
@@ -273,6 +271,9 @@ theory list.Append
   remove prop Append_assoc
   remove prop Append_l_nil
   remove prop Append_length
+  (* FIXME? the following are not part of PVS prelude *)
+  remove prop mem_append
+  remove prop mem_decomp
 end
 
 theory list.Reverse

examples/my_cosine/my_cosine_CosineSingle_MethodError_1.v

@@ -11,6 +11,9 @@ Require real.Abs.
 Require real.FromInt.
 Require int.Int.
 Require real.Square.
+Require floating_point.Rounding.
+Require floating_point.SingleFormat.
+Require floating_point.Single.
 
 Axiom Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R < PI)%R /\
   (PI < (314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R)%R.
@@ -42,111 +45,6 @@ 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 *)

lib/pvs/floating_point/Double.pvs

@@ -114,5 +114,6 @@ Double: THEORY
   gt(x:DoubleFormat.double, y:DoubleFormat.double): bool =
     (value(x) >  value(y))
   
+  
  END Double
  
\ No newline at end of file

lib/pvs/floating_point/DoubleFormat.pvs

@@ -12,5 +12,6 @@ DoubleFormat: THEORY
   % Why3 max_int
   max_int: int = 9007199254740992
   
+  
  END DoubleFormat
  
\ No newline at end of file

lib/pvs/floating_point/Rounding.pvs

@@ -12,5 +12,6 @@ Rounding: THEORY
     nearesttiestoaway: nearesttiestoaway?
    END mode
   
+  
  END Rounding
  
\ No newline at end of file

lib/pvs/floating_point/Single.pvs

@@ -114,5 +114,6 @@ Single: THEORY
   gt(x:SingleFormat.single, y:SingleFormat.single): bool =
     (value(x) >  value(y))
   
+  
  END Single
  
\ No newline at end of file

lib/pvs/floating_point/SingleFormat.pvs

@@ -11,5 +11,6 @@ SingleFormat: THEORY
   % Why3 max_int
   max_int: int = 16777216
   
+  
  END SingleFormat
  
\ No newline at end of file

lib/pvs/int/Abs.pvs

@@ -13,5 +13,6 @@ Abs: THEORY
   % Why3 abs_pos
   abs_pos: LEMMA FORALL (x:int): (abs1(x) >= 0)
   
+  
  END Abs
  
\ No newline at end of file

lib/pvs/int/ComputerDivision.pvs

@@ -71,5 +71,6 @@ ComputerDivision: THEORY
   mod_mult: LEMMA FORALL (x:int, y:int, z:int): ((x >  0) AND ((y >= 0) AND
     (z >= 0))) => (mod1(((x * y) + z), x) = mod1(z, x))
   
+  
  END ComputerDivision
  
\ No newline at end of file

lib/pvs/int/EuclideanDivision.pvs

@@ -59,5 +59,6 @@ EuclideanDivision: THEORY
   mod_minus1_left: LEMMA FORALL (y:int): (y >  1) => (mod1((-1),
     y) = (y - 1))
   
+  
  END EuclideanDivision
  
\ No newline at end of file

lib/pvs/int/Int.pvs

@@ -87,5 +87,6 @@ Int: THEORY
   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

lib/pvs/int/MinMax.pvs

@@ -43,5 +43,6 @@ MinMax: THEORY
   % Why3 min_sym
   min_sym: LEMMA FORALL (x:int, y:int): (x >= y) => (min1(x, y) = min1(y, x))
   
+  
  END MinMax
  
\ No newline at end of file

lib/pvs/real/Abs.prf

 (Abs
  (abs_le 0
   (abs_le-1 nil 3551212620 ("" (default-strategy))
-   ((abs const-decl "real" Abs nil)
+   ((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)
@@ -14,12 +14,11 @@
      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_pos 0
   (abs_pos-1 nil 3551212620 ("" (default-strategy))
-   ((abs const-decl "real" Abs nil)
+   ((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)
@@ -29,12 +28,11 @@
      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_sum 0
   (abs_sum-1 nil 3551212620 ("" (default-strategy))
-   ((abs const-decl "real" Abs nil)
+   ((abs1 const-decl "real" Abs nil)
     (minus_real_is_real application-judgement "real" reals nil)
     (real_ge_is_total_order name-judgement "(total_order?[real])"
      real_props nil)
@@ -46,7 +44,6 @@
      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
@@ -63,7 +60,7 @@
  (triangular_inequality 0
   (triangular_inequality-1 nil 3551212620 ("" (default-strategy))
    ((minus_odd_is_odd application-judgement "odd_int" integers nil)
-    (abs const-decl "real" Abs nil)
+    (abs1 const-decl "real" Abs nil)
     (minus_real_is_real application-judgement "real" reals nil)
     (real_ge_is_total_order name-judgement "(total_order?[real])"
      real_props nil)
@@ -75,7 +72,6 @@
      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)))
 

lib/pvs/real/Abs.pvs

@@ -25,5 +25,6 @@ Abs: THEORY
   triangular_inequality: LEMMA FORALL (x:real, y:real, z:real):
     (abs1((x - z)) <= (abs1((x - y)) + abs1((y - z))))
   
+  
  END Abs
  
\ No newline at end of file

lib/pvs/real/ExpLog.prf

+(ExpLog
+ (exp_zero 0
+  (exp_zero-1 nil 3552165298 ("" (default-strategy))
+   ((exp_0 formula-decl nil ln_exp "lnexp/")) shostak))
+ (exp_sum 0
+  (exp_sum-1 nil 3552165298 ("" (grind) (("" (postpone) nil nil)) nil)
+   nil shostak))
+ (log_TCC1 0
+  (log_TCC1-1 nil 3552164963 ("" (grind) nil nil)
+   ((boolean nonempty-type-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)
+    (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))
+   nil))
+ (log_one 0
+  (log_one-1 nil 3552165298 ("" (default-strategy))
+   ((real_gt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (ln_1 formula-decl nil ln_exp "lnexp/"))
+   shostak))
+ (log_mul_TCC1 0
+  (log_mul_TCC1-1 nil 3552164963 ("" (grind) nil nil)
+   ((boolean nonempty-type-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)
+    (real_ge_is_total_order name-judgement "(total_order?[real])"
+     real_props nil)
+    (real_times_real_is_real application-judgement "real" reals nil)
+    (real_gt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil))
+   nil))
+ (log_mul_TCC2 0
+  (log_mul_TCC2-1 nil 3552164963 ("" (subtype-tcc) nil nil)
+   ((boolean nonempty-type-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)
+    (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))
+   nil))
+ (log_mul 0
+  (log_mul-1 nil 3552165298 ("" (default-strategy)) nil shostak))
+ (log_exp_TCC1 0
+  (log_exp_TCC1-1 nil 3552164963 ("" (subtype-tcc) nil nil)
+   ((boolean nonempty-type-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)
+    (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))
+   nil))
+ (log_exp 0
+  (log_exp-1 nil 3552165298 ("" (default-strategy))
+   ((real_gt_is_strict_total_order name-judgement
+     "(strict_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))
+ (exp_log 0
+  (exp_log-1 nil 3552165298 ("" (default-strategy)) nil shostak)))
+

lib/pvs/real/ExpLog.pvs

+ExpLog: THEORY
+ BEGIN
+  IMPORTING Real
+  % do not edit above this line
+  
+  IMPORTING lnexp@ln_exp
+  
+  % Why3 exp
+  exp(x:real): MACRO real = exp(x)
+  
+  % Why3 exp_zero
+  exp_zero: LEMMA (exp(0) = 1)
+  
+  % Why3 exp_sum
+  exp_sum: LEMMA FORALL (x:real, y:real): (exp((x + y)) = (exp(x) * exp(y)))
+  
+  % Why3 e
+  e: real = exp(1)
+  
+  % Why3 log
+  log(x:real): MACRO real = IF x > 0 THEN ln(x) ELSE log_total(x) ENDIF
+  
+  % Why3 log_one
+  log_one: LEMMA (log(1) = 0)
+  
+  % Why3 log_mul
+  log_mul: LEMMA FORALL (x:real, y:real): ((x >  0) AND (y >  0)) =>
+    (log((x * y)) = (log(x) + log(y)))
+  
+  % Why3 log_exp
+  log_exp: LEMMA FORALL (x:real): (log(exp(x)) = x)
+  
+  % Why3 exp_log
+  exp_log: LEMMA FORALL (x:real): (x >  0) => (exp(log(x)) = x)
+  
+  % Why3 log2
+  log2(x:real): real = Real.infix_sl(log(x), log(2))
+  
+  % Why3 log10
+  log10(x:real): real = Real.infix_sl(log(x), log(10))
+  
+  
+ END ExpLog
+ 
\ No newline at end of file

lib/pvs/real/FromInt.prf

 (FromInt
  (zero 0 (zero-1 nil 3551213833 ("" (default-strategy)) nil shostak))
  (one 0 (one-1 nil 3551213833 ("" (default-strategy)) nil shostak))
- (add 0 (add-1 nil 3551213833 ("" (default-strategy)) nil shostak))
  (sub 0
   (sub-1 nil 3551213833 ("" (default-strategy))
    ((minus_odd_is_odd application-judgement "odd_int" integers nil))

lib/pvs/real/FromInt.pvs

@@ -28,5 +28,6 @@ FromInt: THEORY
   % Why3 neg
   neg: LEMMA FORALL (x:int): (from_int((-x)) = (-from_int(x)))
   
+  
  END FromInt
  
\ No newline at end of file

lib/pvs/real/MinMax.pvs

@@ -25,5 +25,6 @@ MinMax: THEORY
   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

lib/pvs/real/PowerInt.pvs

+PowerInt: THEORY
+ BEGIN
+  IMPORTING int@Int
+  IMPORTING Real
+  % do not edit above this line
+  
+  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
+  
+  % Why3 power_0
+  power_0: LEMMA FORALL (x:real): (power(x, 0) = 1)
+  
+  % Why3 power_s
+  power_s: LEMMA FORALL (x:real, n:int): (n >= 0) => (power(x,
+    (n + 1)) = (x * power(x, n)))
+  
+  % 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)))
+  
+  % 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)))
+  
+  
+ END PowerInt
+ 

lib/pvs/real/Real.pvs

@@ -123,5 +123,6 @@ Real: THEORY
   compatordermult: LEMMA FORALL (x:real, y:real, z:real): infix_lseq(x, y) =>
     (infix_lseq(zero, z) => infix_lseq(infix_as(x, z), infix_as(y, z)))
   
+  
  END Real
  
\ No newline at end of file

lib/pvs/real/Square.prf

+(Square
+ (sqrt_positive 0
+  (sqrt_positive-1 nil 3552163066 ("" (default-strategy))
+   ((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))
+ (sqrt_square 0
+  (sqrt_square-1 nil 3552163066 ("" (default-strategy))
+   ((sqr const-decl "real" Square nil)
+    (real_ge_is_total_order name-judgement "(total_order?[real])"
+     real_props nil)
+    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
+     real_types 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))
+ (square_sqrt 0
+  (square_sqrt-1 nil 3552163066 ("" (default-strategy))
+   ((real_ge_is_total_order name-judgement "(total_order?[real])"
+     real_props nil)
+    (real_times_real_is_real application-judgement "real" reals nil)
+    (sqrt_square formula-decl nil sqrt "reals/")
+    (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))
+ (sqrt_mul 0
+  (sqrt_mul-1 nil 3552163067
+   ("" (default-strategy) (("" (postpone) nil nil)) nil) nil shostak))
+ (sqrt_le 0
+  (sqrt_le-1 nil 3552163067 ("" (default-strategy)) nil shostak)))
+

lib/pvs/real/Square.pvs

+Square: THEORY
+ BEGIN
+  IMPORTING Real
+  % do not edit above this line
+  
+  IMPORTING reals@sqrt
+  
+  % Why3 sqr
+  sqr(x:real): real = (x * x)
+  
+  sqrt_total(x:real): real
+  
+  % Why3 sqrt
+  sqrt(x:real): MACRO real = IF x >= 0 THEN sqrt(x) ELSE sqrt_total(x) ENDIF
+  
+  % Why3 sqrt_positive
+  sqrt_positive: LEMMA FORALL (x:real): (x >= 0) => (sqrt(x) >= 0)
+  
+  % Why3 sqrt_square
+  sqrt_square: LEMMA FORALL (x:real): (x >= 0) => (sqr(sqrt(x)) = x)
+  
+  % Why3 square_sqrt
+  square_sqrt: LEMMA FORALL (x:real): (x >= 0) => (sqrt((x * x)) = x)
+  
+  % Why3 sqrt_mul
+  sqrt_mul: LEMMA FORALL (x:real, y:real): ((x >= 0) AND (y >= 0)) =>
+    (sqrt((x * y)) = (sqrt(x) * sqrt(y)))
+  
+  % Why3 sqrt_le
+  sqrt_le: LEMMA FORALL (x:real, y:real): ((0 <= x) AND (x <= y)) =>
+    (sqrt(x) <= sqrt(y))
+  
+  
+ END Square
+ 
\ No newline at end of file

lib/pvs/real/Trigonometry.prf

+(Trigonometry
+ (pythagorean_identity 0
+  (pythagorean_identity-1 nil 3552164504 ("" (default-strategy)) nil
+   shostak))
+ (cos_le_one 0
+  (cos_le_one-1 nil 3552164504 ("" (default-strategy))
+   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
+         nil)
+    (real_le_is_total_order name-judgement "(total_order?[real])"
+     real_props nil)
+    (minus_real_is_real application-judgement "real" reals nil)
+    (real_lt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (cos_range application-judgement "trig_range" trig_basic "trig/")
+    (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))
+ (sin_le_one 0
+  (sin_le_one-1 nil 3552164505 ("" (default-strategy))
+   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
+         nil)
+    (real_le_is_total_order name-judgement "(total_order?[real])"
+     real_props nil)
+    (minus_real_is_real application-judgement "real" reals nil)
+    (real_lt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (sin_range application-judgement "trig_range" trig_basic "trig/")
+    (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))
+ (cos_0 0 (cos_0-1 nil 3552164505 ("" (default-strategy)) nil shostak))
+ (sin_0 0 (sin_0-1 nil 3552164505 ("" (default-strategy)) nil shostak))
+ (pi_interval 0
+  (pi_interval-1 nil 3552164505 ("" (default-strategy)) nil shostak))
+ (cos_pi 0
+  (cos_pi-1 nil 3552164505 ("" (default-strategy)) nil shostak))
+ (sin_pi 0
+  (sin_pi-1 nil 3552164505 ("" (default-strategy)) nil shostak))
+ (cos_pi2 0
+  (cos_pi2-1 nil 3552164505 ("" (default-strategy)) nil shostak))
+ (sin_pi2 0
+  (sin_pi2-1 nil 3552164505 ("" (default-strategy)) nil shostak))
+ (cos_plus_pi 0
+  (cos_plus_pi-1 nil 3552164505 ("" (default-strategy)) nil shostak))
+ (sin_plus_pi 0
+  (sin_plus_pi-1 nil 3552164505 ("" (default-strategy)) nil shostak))
+ (cos_plus_pi2 0
+  (cos_plus_pi2-1 nil 3552164505 ("" (default-strategy)) nil shostak))
+ (sin_plus_pi2 0
+  (sin_plus_pi2-1 nil 3552164506 ("" (default-strategy)) nil shostak))
+ (cos_neg 0
+  (cos_neg-1 nil 3552164506 ("" (default-strategy)) nil shostak))
+ (sin_neg 0
+  (sin_neg-1 nil 3552164506 ("" (default-strategy)) nil shostak))
+ (cos_sum 0
+  (cos_sum-1 nil 3552164506 ("" (default-strategy)) nil shostak))
+ (sin_sum 0
+  (sin_sum-1 nil 3552164506 ("" (default-strategy)) nil shostak))
+ (tan_atan 0
+  (tan_atan-1 nil 3552164506 ("" (default-strategy)) nil shostak)))
+

lib/pvs/real/Trigonometry.pvs

+Trigonometry: THEORY
+ BEGIN
+  IMPORTING Real
+  IMPORTING Abs
+  IMPORTING Square
+  % do not edit above this line
+  
+  IMPORTING trig@trig_basic
+  
+  % Why3 cos
+  cos(x:real): MACRO real = cos(x)
+  
+  % Why3 sin
+  sin(x:real): MACRO real = sin(x)
+  
+  % Why3 pythagorean_identity
+  pythagorean_identity: LEMMA FORALL (x:real):
+    ((Square.sqr(cos(x)) + Square.sqr(sin(x))) = 1)
+  
+  % Why3 cos_le_one
+  cos_le_one: LEMMA FORALL (x:real): (abs(cos(x)) <= 1)
+  
+  % Why3 sin_le_one
+  sin_le_one: LEMMA FORALL (x:real): (abs(sin(x)) <= 1)
+  
+  % Why3 cos_0
+  cos_0: LEMMA (cos(0) = 1)
+  
+  % Why3 sin_0
+  sin_0: LEMMA (sin(0) = 0)
+  
+  % Why3 pi
+  pi: MACRO real = pi
+