From 3221b16a1b96ea58f1ad86d74d4d3a6318b01548 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 22 Apr 2020 16:17:25 +0200
Subject: [PATCH] builtins

---
 encodings/builtins.lp | 17 +++++++++++++++++
 prelude/logic.lp      |  3 +--
 2 files changed, 18 insertions(+), 2 deletions(-)
 create mode 100644 encodings/builtins.lp

diff --git a/encodings/builtins.lp b/encodings/builtins.lp
new file mode 100644
index 0000000..2d2c299
--- /dev/null
+++ b/encodings/builtins.lp
@@ -0,0 +1,17 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_hol
+
+constant symbol {|!Number!|}: θ {|set|}
+
+constant symbol zero: η {|!Number!|}
+constant symbol succ: η ({|!Number!|} ~> {|!Number!|})
+
+set builtin "0" ≔ zero
+set builtin "+1" ≔ succ
+
+// In PVS, the axipms 1 ≠ 2, 1≠3, ... are built in
+// Here we use the decidable equality
+rule ε (succ $n = succ $m) ↪ ε ($n = $m)
+with ε (zero = succ _) ↪ ε false
+with ε (zero = zero) ↪ ε true
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 101208f..12bd0ff 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -49,9 +49,8 @@ theorem xor_def
 proof
 admit
 
-
 //
-// Quantifier props[t: TYPE]
+// Quantifier props[t: TYPE], built in
 //
 set declared "∃"
 definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))
-- 
GitLab