Make progress on the proofs of the hash map

1 files changed, 19 insertions, 0 deletions

diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml
index 157b5c00..2183ef77 100644
--- a/backends/hol4/ilistScript.sml
+++ b/backends/hol4/ilistScript.sml
@@ -64,6 +64,25 @@ Proof
   exfalso >> cooper_tac
 QED
 
+Definition drop_def:
+  drop (i : int) ([] : 'a list) = [] ∧
+  drop (i : int) (x :: ls) =
+    if i < 0 then x :: ls
+    else if i = 0 then x :: ls
+    else drop (i - 1) ls
+End
+
+Theorem drop_eq:
+  (∀ i. drop i [] = []) ∧
+  (∀ ls. drop 0 ls = ls) ∧
+  (∀ i x ls. drop i (x :: ls) =
+    if (0 < i) ∨ (0 ≤ i ∧ i ≠ 0) then drop (i - 1) ls
+    else x :: ls)
+Proof
+  rw [drop_def] >> fs [] >> try_tac int_tac >>
+  Cases_on ‘ls’ >> fs [drop_def]
+QED
+
 Theorem len_eq_LENGTH:
   ∀ls. len ls = &(LENGTH ls)
 Proof