diff options
Diffstat (limited to 'backends/hol4/primitivesArithTheory.sig')
| -rw-r--r-- | backends/hol4/primitivesArithTheory.sig | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig index e32b49d4..f7ecccab 100644 --- a/backends/hol4/primitivesArithTheory.sig +++ b/backends/hol4/primitivesArithTheory.sig @@ -7,6 +7,7 @@ sig val ge_eq_le : thm val gt_eq_lt : thm val int_add : thm + val int_add_minus_same_eq : thm val int_induction : thm val int_induction_ideal : thm val int_of_num_id : thm @@ -48,6 +49,10 @@ sig ⊢ ∀m n. &(m + n) = &m + &n + [int_add_minus_same_eq] Theorem + + ⊢ ∀i j. i + j − j = i + [int_induction] Theorem ⊢ ∀P. (∀i. i < 0 ⇒ P i) ∧ P 0 ∧ (∀i. P i ⇒ P (i + 1)) ⇒ ∀i. P i |