blob: f155a3288560b017a116289efbb9e8de326eb3a8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
signature ilistTheory =
sig
type thm = Thm.thm
(* Definitions *)
val index_def : thm
val len_def : thm
val update_def : thm
(* 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 len_pos : thm
val update_eq : thm
val ilist_grammars : type_grammar.grammar * term_grammar.grammar
(*
[primitivesArith] Parent theory of "ilist"
[string] Parent theory of "ilist"
[index_def] Definition
⊢ ∀i x ls.
index i (x::ls) =
if i = 0 then x else if 0 < i then index (i − 1) ls else ARB
[len_def] Definition
⊢ len [] = 0 ∧ ∀x ls. len (x::ls) = 1 + len ls
[update_def] Definition
⊢ (∀i y. update [] i y = []) ∧
∀x ls i y.
update (x::ls) i y =
if i = 0 then y::ls
else if 0 < i then x::update ls (i − 1) y
else x::ls
[append_len_eq] Theorem
⊢ (∀l1 l2 l1' l2'.
len l1 = len l1' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')) ∧
∀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
[len_append] Theorem
⊢ ∀l1 l2. len (l1 ⧺ l2) = len l1 + len l2
[len_eq_LENGTH] Theorem
⊢ ∀ls. len ls = &LENGTH ls
[len_pos] Theorem
⊢ ∀ls. 0 ≤ len 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
|
