summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesArithTheory.sig
diff options
context:
space:
mode:
Diffstat (limited to 'backends/hol4/primitivesArithTheory.sig')
-rw-r--r--backends/hol4/primitivesArithTheory.sig100
1 files changed, 100 insertions, 0 deletions
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
new file mode 100644
index 00000000..3b157b87
--- /dev/null
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -0,0 +1,100 @@
+signature primitivesArithTheory =
+sig
+ type thm = Thm.thm
+
+ (* Theorems *)
+ val GE_EQ_LE : thm
+ val GT_EQ_LT : thm
+ val INT_OF_NUM_INJ : thm
+ val LE_EQ_GE : thm
+ val LT_EQ_GT : thm
+ val NOT_GE_EQ_LT : thm
+ val NOT_GT_EQ_LE : thm
+ val NOT_LE_EQ_GT : thm
+ val NOT_LT_EQ_GE : thm
+ val NUM_SUB_1_EQ : thm
+ val NUM_SUB_EQ : thm
+ val POS_DIV_POS_IS_POS : thm
+ val POS_DIV_POS_LE : thm
+ val POS_DIV_POS_LE_INIT : thm
+ val POS_MOD_POS_IS_POS : thm
+ val POS_MOD_POS_LE_INIT : thm
+ val POS_MUL_POS_IS_POS : thm
+
+ val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+ [Omega] Parent theory of "primitivesArith"
+
+ [int_arith] Parent theory of "primitivesArith"
+
+ [GE_EQ_LE] Theorem
+
+ ⊢ ∀x y. x ≥ y ⇔ y ≤ x
+
+ [GT_EQ_LT] Theorem
+
+ ⊢ ∀x y. x > y ⇔ y < x
+
+ [INT_OF_NUM_INJ] Theorem
+
+ ⊢ ∀n m. &n = &m ⇒ n = m
+
+ [LE_EQ_GE] Theorem
+
+ ⊢ ∀x y. x ≤ y ⇔ y ≥ x
+
+ [LT_EQ_GT] Theorem
+
+ ⊢ ∀x y. x < y ⇔ y > x
+
+ [NOT_GE_EQ_LT] Theorem
+
+ ⊢ ∀x y. ¬(x ≥ y) ⇔ x < y
+
+ [NOT_GT_EQ_LE] Theorem
+
+ ⊢ ∀x y. ¬(x > y) ⇔ x ≤ y
+
+ [NOT_LE_EQ_GT] Theorem
+
+ ⊢ ∀x y. ¬(x ≤ y) ⇔ x > y
+
+ [NOT_LT_EQ_GE] Theorem
+
+ ⊢ ∀x y. ¬(x < y) ⇔ x ≥ y
+
+ [NUM_SUB_1_EQ] Theorem
+
+ ⊢ ∀x y. x = y − 1 ⇒ 0 ≤ x ⇒ Num y = SUC (Num x)
+
+ [NUM_SUB_EQ] Theorem
+
+ ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x
+
+ [POS_DIV_POS_IS_POS] Theorem
+
+ ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x / y
+
+ [POS_DIV_POS_LE] Theorem
+
+ ⊢ ∀x y d. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < d ⇒ x ≤ y ⇒ x / d ≤ y / d
+
+ [POS_DIV_POS_LE_INIT] Theorem
+
+ ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x
+
+ [POS_MOD_POS_IS_POS] Theorem
+
+ ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y
+
+ [POS_MOD_POS_LE_INIT] Theorem
+
+ ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y ≤ x
+
+ [POS_MUL_POS_IS_POS] Theorem
+
+ ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
+
+
+*)
+end