From e0a0d5c18c8874c72f0cf1fce551a9fed243c03e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 1 Jun 2023 23:19:27 +0200
Subject: Finish the proofs of the hashmap

---
 backends/hol4/primitivesArithTheory.sig | 35 +++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

(limited to 'backends/hol4/primitivesArithTheory.sig')

diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index 84b9b67a..85a627d2 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -15,13 +15,16 @@ sig
     val le_eq_ge : thm
     val lt_eq_gt : thm
     val mul_pos_left_le : thm
+    val mul_pos_left_lt : thm
     val mul_pos_right_le : thm
+    val mul_pos_right_lt : 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_ge : thm
     val pos_div_pos_is_pos : thm
     val pos_div_pos_le : thm
     val pos_div_pos_le_init : thm
@@ -30,9 +33,13 @@ sig
     val pos_mod_pos_is_pos : thm
     val pos_mod_pos_le_init : thm
     val pos_mod_pos_lt : thm
+    val pos_mul_2_div_pos_decompose : thm
     val pos_mul_left_pos_le : thm
+    val pos_mul_left_pos_lt : thm
+    val pos_mul_pos_div_pos_decompose : thm
     val pos_mul_pos_is_pos : thm
     val pos_mul_right_pos_le : thm
+    val pos_mul_right_pos_lt : thm
   
   val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -88,10 +95,18 @@ sig
       
       ⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ a * x ≤ a * y
    
+   [mul_pos_left_lt]  Theorem
+      
+      ⊢ ∀a x y. 0 < a ⇒ x < y ⇒ a * x < a * y
+   
    [mul_pos_right_le]  Theorem
       
       ⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ x * a ≤ y * a
    
+   [mul_pos_right_lt]  Theorem
+      
+      ⊢ ∀a x y. 0 < a ⇒ x < y ⇒ x * a < y * a
+   
    [not_ge_eq_lt]  Theorem
       
       ⊢ ∀x y. ¬(x ≥ y) ⇔ x < y
@@ -116,6 +131,10 @@ sig
       
       ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x
    
+   [pos_div_pos_ge]  Theorem
+      
+      ⊢ ∀x y d. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < d ⇒ x ≥ y ⇒ x / d ≥ y / d
+   
    [pos_div_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x / y
@@ -148,10 +167,22 @@ sig
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y
    
+   [pos_mul_2_div_pos_decompose]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y + x / y ≤ x * 2 / y
+   
    [pos_mul_left_pos_le]  Theorem
       
       ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ a * x
    
+   [pos_mul_left_pos_lt]  Theorem
+      
+      ⊢ ∀a x. 1 < a ⇒ 0 < x ⇒ x < a * x
+   
+   [pos_mul_pos_div_pos_decompose]  Theorem
+      
+      ⊢ ∀x y z. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < z ⇒ x / z + y / z ≤ (x + y) / z
+   
    [pos_mul_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
@@ -160,6 +191,10 @@ sig
       
       ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ x * a
    
+   [pos_mul_right_pos_lt]  Theorem
+      
+      ⊢ ∀a x. 1 < a ⇒ 0 < x ⇒ x < x * a
+   
    
 *)
 end
-- 
cgit v1.2.3