diff options
| author | Son Ho | 2023-05-26 17:28:15 +0200 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | 446bbc0bdbb4a03d78636ec71f85e13e66b61e08 (patch) | |
| tree | eddf6f7013f76e507498742e4d60e0709c2cd960 /backends/hol4/primitivesArithTheory.sig | |
| parent | 27f98ddd67c3c80db947ab257fcce7a30244e813 (diff) | |
Make good progress on the proofs of the hashmap in HOL4
Diffstat (limited to 'backends/hol4/primitivesArithTheory.sig')
| -rw-r--r-- | backends/hol4/primitivesArithTheory.sig | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig index f7ecccab..531797ac 100644 --- a/backends/hol4/primitivesArithTheory.sig +++ b/backends/hol4/primitivesArithTheory.sig @@ -23,8 +23,10 @@ sig val pos_div_pos_is_pos : thm val pos_div_pos_le : thm val pos_div_pos_le_init : thm + val pos_mod_pos_ineqs : thm val pos_mod_pos_is_pos : thm val pos_mod_pos_le_init : thm + val pos_mod_pos_lt : thm val pos_mul_pos_is_pos : thm val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar @@ -113,6 +115,10 @@ sig ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x + [pos_mod_pos_ineqs] Theorem + + ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y ∧ x % y < y + [pos_mod_pos_is_pos] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y @@ -121,6 +127,10 @@ sig ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y ≤ x + [pos_mod_pos_lt] Theorem + + ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y + [pos_mul_pos_is_pos] Theorem ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y |