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