diff options
Diffstat (limited to 'backends/hol4/primitivesArithScript.sml')
| -rw-r--r-- | backends/hol4/primitivesArithScript.sml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml index eb2548fd..6c96c908 100644 --- a/backends/hol4/primitivesArithScript.sml +++ b/backends/hol4/primitivesArithScript.sml @@ -78,6 +78,13 @@ Proof fs [Num] QED +(* TODO: use as rewriting theorem by default? *) +Theorem add_sub_same_eq: + ∀(i j : int). i + j - j = i +Proof + cooper_tac +QED + Theorem num_sub_eq: !(x y z : int). x = y - z ==> 0 <= x ==> 0 <= z ==> Num y = Num z + Num x Proof |