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/ilistScript.sml | |
| parent | 03cab42f960860b39108b410c2ca8a06c44186d3 (diff) | |
Finish the proofs of the hashmap
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/ilistScript.sml | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml index 2183ef77..fb0c7688 100644 --- a/backends/hol4/ilistScript.sml +++ b/backends/hol4/ilistScript.sml @@ -16,6 +16,7 @@ val len_def = Define ‘ len [] : int = 0 /\ len (x :: ls) : int = 1 + len ls ’ +val _ = BasicProvers.export_rewrites ["len_def"] (* Return the ith element of a list. @@ -117,6 +118,7 @@ Theorem len_append: Proof rw [len_eq_LENGTH] >> cooper_tac QED +val _ = BasicProvers.export_rewrites ["len_append"] Theorem append_len_eq: (∀l1 l2 l1' l2'. @@ -129,6 +131,18 @@ Proof rw [len_eq_LENGTH] >> fs [APPEND_11_LENGTH] QED +Theorem drop_more_than_length: + ∀ ls i. + len ls ≤ i ⇒ + drop i ls = [] +Proof + Induct_on ‘ls’ >> + rw [drop_def] >> + qspec_assume ‘ls’ len_pos >> try_tac int_tac >> + last_x_assum irule >> + int_tac +QED + (* TODO: prove more theorems, and add rewriting theorems *) val _ = export_theory () |