diff options
author | Son Ho | 2023-05-22 17:34:08 +0200 |
---|---|---|
committer | Son HO | 2023-06-04 21:54:38 +0200 |
commit | c823ad32033904fc47cda9a9ae9f3fa3116edc6f (patch) | |
tree | 7175053afb44e006ef4800c3fb78b5063b2a0c18 /backends/hol4/primitivesScript.sml | |
parent | 1f0e5b3cb80e9334b07bf4b074c01150f4abd49d (diff) |
Make progress on extracting the HOL4 files
Diffstat (limited to '')
-rw-r--r-- | backends/hol4/primitivesScript.sml | 119 |
1 files changed, 119 insertions, 0 deletions
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index e10ce7e5..4a1f5fdd 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -504,6 +504,33 @@ val all_mk_int_defs = [ mk_u128_def ] +(* Unfolding theorems for “mk_usize” and “mk_isize”: we need specific unfolding + theorems because the isize/usize bounds are opaque, and may make the evaluation + get stuck in the unit tests *) +Theorem mk_usize_unfold: + ∀ n. mk_usize n = + if 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) then Return (int_to_usize n) + else Fail Failure +Proof + rw [mk_usize_def] >> fs [] >> + assume_tac usize_bounds >> + int_tac +QED +val _ = evalLib.add_unfold_thm "mk_usize_unfold" + +Theorem mk_isize_unfold: + ∀ n. mk_isize n = + if (i16_min ≤ n ∨ isize_min ≤ n) ∧ + (n ≤ i16_max ∨ n ≤ isize_max) + then Return (int_to_isize n) + else Fail Failure +Proof + rw [mk_isize_def] >> fs [] >> + assume_tac isize_bounds >> + int_tac +QED +val _ = evalLib.add_unfold_thm "mk_isize_unfold" + val isize_neg_def = Define ‘isize_neg x = mk_isize (- (isize_to_int x))’ val i8_neg_def = Define ‘i8_neg x = mk_i8 (- (i8_to_int x))’ val i16_neg_def = Define ‘i16_neg x = mk_i16 (- (i16_to_int x))’ @@ -1521,6 +1548,98 @@ Definition isize_ge_def: End +(* Equality theorems for the comparisons between integers - used by evalLib *) + +val prove_scalar_eq_equiv_tac = metis_tac all_scalar_to_int_to_scalar_lemmas + +Theorem isize_eq_equiv: + ∀x y. (x = y) = (isize_to_int x = isize_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem i8_eq_equiv: + ∀x y. (x = y) = (i8_to_int x = i8_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem i16_eq_equiv: + ∀x y. (x = y) = (i16_to_int x = i16_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem i32_eq_equiv: + ∀x y. (x = y) = (i32_to_int x = i32_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem i64_eq_equiv: + ∀x y. (x = y) = (i64_to_int x = i64_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem i128_eq_equiv: + ∀x y. (x = y) = (i128_to_int x = i128_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem usize_eq_equiv: + ∀x y. (x = y) = (usize_to_int x = usize_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem u8_eq_equiv: + ∀x y. (x = y) = (u8_to_int x = u8_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem u16_eq_equiv: + ∀x y. (x = y) = (u16_to_int x = u16_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem u32_eq_equiv: + ∀x y. (x = y) = (u32_to_int x = u32_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem u64_eq_equiv: + ∀x y. (x = y) = (u64_to_int x = u64_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem u128_eq_equiv: + ∀x y. (x = y) = (u128_to_int x = u128_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +(* Remark.: don't move this up, it will break some proofs *) +val _ = BasicProvers.export_rewrites [ + "isize_eq_equiv", + "i8_eq_equiv", + "i16_eq_equiv", + "i32_eq_equiv", + "i64_eq_equiv", + "i128_eq_equiv", + "usize_eq_equiv", + "u8_eq_equiv", + "u16_eq_equiv", + "u32_eq_equiv", + "u64_eq_equiv", + "u128_eq_equiv" +] + (*** * Vectors *) |