blob: fb0c7688bb72580cfaeb5f134e93442e73322f6a (
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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
open listTheory
open primitivesArithTheory primitivesBaseTacLib
(* The following theory contains alternative definitions of functions operating
on lists like “EL” or “LENGTH”, but this time using integers rather than
natural numbers.
By using integers, we make sure we don't have to convert back and forth
between integers and natural numbers, which is extremely cumbersome in
the proofs.
*)
val _ = new_theory "ilist"
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.
Remark: we initially added the following case, so that we wouldn't need the
premise [i < len ls] is [index_eq_EL]:
“index (i : int) [] = EL (Num i) []”
*)
val index_def = Define ‘
index (i : int) (x :: ls) = if i = 0 then x else (if 0 < i then index (i - 1) ls else ARB)
’
(* We use the following theorem as a rewriting theorem for [index]: it performs
better with the rewritings.
TODO: we could even write:
if (0 < i) ∨ (i > 0) ∨ ((0 ≤ i ∨ i >= 0) ∧ (i ≠ 0 ∨ 0 ≠ i)) then ...
*)
Theorem index_eq:
(∀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))
Proof
rw [index_def] >> fs [] >>
exfalso >> cooper_tac
QED
val update_def = Define ‘
update ([] : 'a list) (i : int) (y : 'a) : 'a list = [] ∧
update (x :: ls) (i : int) y =
if i = 0 then y :: ls else (if 0 < i then x :: update ls (i - 1) y else x :: ls)
’
Theorem update_eq:
(∀i y. update ([] : 'a list) (i : int) (y : 'a) : 'a list = []) ∧
(∀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)
Proof
rw [update_def] >> fs [] >>
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
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 ⇒
i < len ls ⇒
index i ls = EL (Num i) ls
Proof
Induct_on ‘ls’ >> rpt strip_tac >> fs [len_def, index_eq] >- int_tac >>
Cases_on ‘i = 0’ >> fs [] >>
Cases_on ‘Num i’ >- (int_tac) >> fs [] >>
last_assum (qspec_assume ‘i - 1’) >>
pop_assum sg_premise_tac >- cooper_tac >>
sg ‘n = Num (i - 1)’ >- cooper_tac >> fs [] >>
last_assum irule >> cooper_tac
QED
Theorem len_append:
∀l1 l2. len (l1 ++ l2) = len l1 + len l2
Proof
rw [len_eq_LENGTH] >> cooper_tac
QED
val _ = BasicProvers.export_rewrites ["len_append"]
Theorem append_len_eq:
(∀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'))
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 ()
|
