diff options
Diffstat (limited to 'backends/hol4/ilistTheory.sig')
| -rw-r--r-- | backends/hol4/ilistTheory.sig | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig index 9612f063..249b362c 100644 --- a/backends/hol4/ilistTheory.sig +++ b/backends/hol4/ilistTheory.sig @@ -9,9 +9,11 @@ sig (* Theorems *) val append_len_eq : thm + val index_eq : thm val index_eq_EL : thm val len_append : thm val len_eq_LENGTH : thm + val update_eq : thm val ilist_grammars : type_grammar.grammar * term_grammar.grammar (* @@ -21,8 +23,7 @@ sig [index_def] Definition - ⊢ (∀i. index i [] = EL (Num i) []) ∧ - ∀i x ls. + ⊢ ∀i x ls. index i (x::ls) = if i = 0 then x else if 0 < i then index (i − 1) ls else ARB @@ -46,6 +47,15 @@ sig ∀l1 l2 l1' l2'. len l2 = len l2' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2') + [index_eq] Theorem + + ⊢ (∀x ls. index 0 (x::ls) = x) ∧ + ∀i x ls. + index i (x::ls) = + if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then index (i − 1) ls + else if i = 0 then x + else ARB + [index_eq_EL] Theorem ⊢ ∀i ls. 0 ≤ i ⇒ i < len ls ⇒ index i ls = EL (Num i) ls @@ -58,6 +68,16 @@ sig ⊢ ∀ls. len ls = &LENGTH ls + [update_eq] Theorem + + ⊢ (∀i y. update [] i y = []) ∧ + (∀x ls y. update (x::ls) 0 y = y::ls) ∧ + ∀x ls i y. + update (x::ls) i y = + if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then x::update ls (i − 1) y + else if i < 0 then x::ls + else y::ls + *) end |