diff options
Diffstat (limited to 'backends/hol4/ilistScript.sml')
| -rw-r--r-- | backends/hol4/ilistScript.sml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml index c871ba04..f382d95d 100644 --- a/backends/hol4/ilistScript.sml +++ b/backends/hol4/ilistScript.sml @@ -72,6 +72,14 @@ Proof Induct_on ‘ls’ >> fs [len_def] >> cooper_tac QED +Theorem len_pos: + ∀ls. 0 ≤ len ls +Proof + strip_tac >> + qspec_assume ‘ls’ len_eq_LENGTH >> + cooper_tac +QED + Theorem index_eq_EL: ∀(i: int) ls. 0 ≤ i ⇒ |