added files to pvs theories folder

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@7027 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

PVS_theories/double.pvs

+double: THEORY
+
+BEGIN
+IMPORTING float@enumerated_type_defs
+IMPORTING overload[2,53,192,1023,-1022,to_nearest]
+
+double: TYPE = {fp:fp_num|finite?(fp) OR infinite?(fp)}
+double_finite: TYPE = {fp:fp_num|finite?(fp)}
+
+END double

PVS_theories/fp_lemmas.pvs

+fp_lemmas
+ [b,p:above(1),
+   alpha,E_max:integer,
+   E_min:{i:integer|E_max>i}]:THEORY
+
+BEGIN
+
+
+IMPORTING float@IEEE_854_defs[b,p,alpha,E_max,E_min]
+
+infinite_not_zero: LEMMA FORALL (x:fp_num): infinite?(x) => NOT zero?(x)
+
+%finite_mul_1: LEMMA FORALL(x:{fp:fp_num|finite?(fp)},mode:rounding_mode): finite?(fp_mul(x,real_to_fp(1),mode))
+
+op_fin_inf: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp)}, y:{fp:fp_num| finite?(fp)},op:{op:fp_ops|zero?(y) OR (zero?(x) AND zero?(y)) => NOT div?(op)}):
+finite?(fp_op(op,x,y,mode)) OR infinite?(fp_op(op,x,y,mode))
+
+op_add_inf_fin: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) OR infinite?(fp)}): infinite?(x) XOR infinite?(y) => finite?(fp_add(x,y,mode)) OR infinite?(fp_add(x,y,mode)) 
+
+op_add_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_add(x,y,mode)) OR infinite?(fp_add(x,y,mode)) 
+
+op_add_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_add(y,x,mode)) OR infinite?(fp_add(y,x,mode)) 
+
+op_sub_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_sub(x,y,mode)) OR infinite?(fp_sub(x,y,mode)) 
+
+op_sub_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_sub(y,x,mode)) OR infinite?(fp_sub(y,x,mode))
+
+op_mul_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND (infinite?(x) => NOT zero?(fp))}): finite?(fp_mul(y,x,mode)) OR infinite?(fp_mul(y,x,mode))
+
+op_mul_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND (infinite?(x) => NOT zero?(fp))}): finite?(fp_mul(x,y,mode)) OR infinite?(fp_mul(x,y,mode))
+
+op_div_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND NOT zero?(fp)}): finite?(fp_div(x,y,mode)) OR infinite?(fp_div(x,y,mode))
+
+op_div_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) AND NOT zero?(fp)},y:{fp:fp_num| finite?(fp) OR infinite?(fp)}): finite?(fp_div(y,x,mode)) OR infinite?(fp_div(y,x,mode))
+
+op_sqrt_inf_fin: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|(finite?(fp) AND sign(fp) = pos) OR (infinite?(fp) AND i_sign(fp) = pos)}): finite?(fp_sqrt(x,mode)) OR infinite?(fp_sqrt(x,mode))
+
+
+END fp_lemmas

PVS_theories/overload.prf

+(overload
+ (lessp_TCC1 0
+  (lessp_TCC1-1 nil 3508513172 3508513284
+   ("" (skolem!) (("" (grind) nil nil)) nil) proved
+   ((posrat_exp application-judgement "posrat" exponentiation nil)
+    (nnrat_exp application-judgement "nnrat" exponentiation nil)
+    (minus_odd_is_odd application-judgement "odd_int" integers nil)
+    (minus_real_is_real application-judgement "real" reals nil)
+    (real_to_fp const-decl "fp_num" real_to_fp "float/")
+    (number nonempty-type-decl nil numbers nil)
+    (boolean nonempty-type-decl nil booleans nil)
+    (number_field_pred const-decl "[number -> boolean]" number_fields
+     nil)
+    (numfield nonempty-type-eq-decl nil number_fields nil)
+    (- const-decl "[numfield -> numfield]" number_fields nil)
+    (sign_of const-decl "sign_rep" fp_round_aux "float/")
+    (pos const-decl "sign_rep" enumerated_type_defs "float/")
+    (neg const-decl "sign_rep" enumerated_type_defs "float/")
+    (^ const-decl "real" exponentiation nil)
+    (expt def-decl "real" exponentiation nil)
+    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
+         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)
+    (posint_exp application-judgement "posint" exponentiation nil)
+    (posint_plus_nnint_is_posint application-judgement "posint"
+     integers nil)
+    (odd_plus_odd_is_even application-judgement "even_int" integers
+     nil)
+    (posnat_expt application-judgement "posnat" exponentiation nil)
+    (posrat_div_posrat_is_posrat application-judgement "posrat"
+     rationals nil)
+    (posint_times_posint_is_posint application-judgement "posint"
+     integers nil)
+    (even_times_int_is_even application-judgement "even_int" integers
+     nil)
+    (mult_divides1 application-judgement "(divides(n))" divides nil)
+    (mult_divides2 application-judgement "(divides(m))" divides nil)
+    (even_minus_odd_is_odd application-judgement "odd_int" integers
+     nil)
+    (odd_minus_odd_is_even application-judgement "even_int" integers
+     nil)
+    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
+    (minus_even_is_even application-judgement "even_int" integers nil))
+   18355 5670 t nil))
+ (expt_TCC1 0
+  (expt_TCC1-1 nil 3508513172 3508513172 ("" (subtype-tcc) nil nil)
+   proved
+   ((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)
+    (>= const-decl "bool" 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)
+    (nat nonempty-type-eq-decl nil naturalnumbers nil)
+    (int_minus_int_is_int application-judgement "int" integers nil)
+    (real_ge_is_total_order name-judgement "(total_order?[real])"
+     real_props nil))
+   17 20 nil nil))
+ (expt_TCC2 0
+  (expt_TCC2-1 nil 3508513172 3508513172 ("" (termination-tcc) nil nil)
+   proved nil 6 0 nil nil))
+ (caret_TCC1 0
+  (caret_TCC1-1 nil 3508513172 3508513172 ("" (subtype-tcc) nil nil)
+   proved
+   ((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)
+    (minus_int_is_int application-judgement "int" integers nil)
+    (real_ge_is_total_order name-judgement "(total_order?[real])"
+     real_props nil))
+   16 20 nil nil)))
+

PVS_theories/overload.pvs

+overload[b,p:above(1),
+   alpha,E_max:integer,
+   E_min:{i:integer|E_max>i},
+(IMPORTING float@enumerated_type_defs)r_mode:rounding_mode]:THEORY
+
+BEGIN
+
+IMPORTING fp_lemmas[b,p,alpha,E_max,E_min]
+
+x,y: VAR fp_num
+n:VAR nat
+
+-(x,y):fp_num = fp_sub(x,y,r_mode);
++(x,y):fp_num = fp_add(x,y,r_mode);
+*(x,y):fp_num = fp_mul(x,y,r_mode);
+/(x,y):fp_num = fp_div(x,y,r_mode);
+sqrt(x):fp_num = fp_sqrt(x,r_mode);
+-(x):fp_num = toggle_sign(x);
+
+-(x:fp_num,y:real):fp_num = x-real_to_fp(y);
++(x:fp_num,y:real):fp_num = x+real_to_fp(y);
+*(x:fp_num,y:real):fp_num = x*real_to_fp(y);
+/(x:fp_num,y:real):fp_num = x/real_to_fp(y);
+
+-(x:real,y:fp_num):fp_num = real_to_fp(x)-y;
++(x:real,y:fp_num):fp_num = real_to_fp(x)+y;
+*(x:real,y:fp_num):fp_num = real_to_fp(x)*y;
+/(x:real,y:fp_num):fp_num = real_to_fp(x)/y;
+
+
+<(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) < n_value(y);
+<=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) <= n_value(y);
+>(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) > n_value(y);
+>=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) >= n_value(y);
+=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) = n_value(y);
+/=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) /= n_value(y);
+
+<(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) < y;
+<=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) <= y;
+>(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) > y;
+>=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) >= y;
+=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) = y;
+/=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) /= y;
+
+<(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x < real_to_fp(y);
+<=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x <= real_to_fp(y);
+>(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x > real_to_fp(y);
+>=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x >= real_to_fp(y);
+=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x = real_to_fp(y);
+/=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x /= real_to_fp(y);
+
+expt(x,n): RECURSIVE fp_num =
+  IF n = 0 THEN real_to_fp(1)
+  ELSE x * expt(x, n-1)
+  ENDIF
+MEASURE n;
+
+^(x: fp_num, i:int): fp_num
+    = IF i >= 0 THEN expt(x, i) ELSE real_to_fp(1)/expt(x, -i) ENDIF
+END overload

PVS_theories/single.pvs

+single: THEORY
+
+BEGIN
+ 
+IMPORTING float@enumerated_type_defs
+IMPORTING overload[2,24,192,127,-126,to_nearest]
+
+single: TYPE = {fp:fp_num|finite?(fp) OR infinite?(fp)}
+single_finite: TYPE = {fp:fp_num|finite?(fp)}
+
+END single