From 00c5cb46bba5fc0470fb7049db84c1ed0b62e024 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Mon, 11 May 2020 16:50:24 +0200
Subject: [PATCH] redoing numbers

---
 prelude/numbers.lp | 23 ++++++++++++++---------
 1 file changed, 14 insertions(+), 9 deletions(-)

diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index 9f47ebe..1978de6 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -3,11 +3,14 @@ require open personoj.encodings.pvs_cert
 require open personoj.encodings.bool_hol
 require open personoj.encodings.prenex
 require open personoj.prelude.logic
+require open personoj.encodings.builtins
+require open personoj.encodings.subtype2
 
 //
 // Theory numbers
 //
 constant symbol number: θ {|set|}
+rule η (μ number) ↪ η number
 
 //
 // Theory number_fields
@@ -17,6 +20,8 @@ definition number_field ≔ psub field_pred
 // number_field is an uninterpreted subtype
 definition numfield ≔ number_field
 
+symbol insertnum: η {|!Number!|} → η numfield
+
 symbol {|+|}: η (numfield ~> numfield ~> numfield)
 set infix left 6 "+" ≔ {|+|}
 symbol {|-|}: η (numfield ~> numfield ~> numfield)
@@ -43,17 +48,17 @@ symbol associative_add
 //
 constant symbol real_pred: η (pred numfield)
 definition real ≔ psub real_pred
-// theorem real_not_empty: Term (∃ real_pred)
-// proof admit
 
-// constant symbol zero : Term real
-// // Built in the PVS typechecker
+set debug +u
+set flag "print_implicits" on
+symbol Num_real: ε (∀ (λx: η {|!Number!|}, real_pred (insertnum x)))
 
-// definition nonzero_real_pred ≔ neq zero
-// definition nonzero_real ≔ Psub nonzero_real_pred
-// theorem nonzero_real_not_empty: Term (∃ nonzero_real_pred)
-// proof admit
-// definition nzreal ≔ nonzero_real
+// Built in the PVS typechecker
+
+definition nonzero_real ≔
+  psub {real}
+       (λx: η real,
+        neq _ x (cast {_} {real} (λx, x) (insertnum 0) _))
 
 // symbol closed_plus_real: Π(x y: Term real),
 //   let pr ≔ S.restr numfield real_pred in
-- 
GitLab