diff options
| author | Son Ho | 2023-06-01 23:19:27 +0200 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | e0a0d5c18c8874c72f0cf1fce551a9fed243c03e (patch) | |
| tree | 50cee0fe1527d76ddb20e64948b2ef04daa359ac /backends/hol4/primitivesArithTheory.sig | |
| parent | 03cab42f960860b39108b410c2ca8a06c44186d3 (diff) | |
Finish the proofs of the hashmap
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/primitivesArithTheory.sig | 35 |
1 files changed, 35 insertions, 0 deletions
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 |