blob: 157b5c00a3daaebedc457835fe828a68c9488769 (
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
|
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
’
(* 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
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
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
(* TODO: prove more theorems, and add rewriting theorems *)
val _ = export_theory ()
|
