-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathtame_defs_unrolled.hl
160 lines (149 loc) · 8.75 KB
/
tame_defs_unrolled.hl
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
149
150
151
152
153
154
155
156
157
158
needs "tame/tame_defs.hl";;
let APPEND_UNROLL8 = prove
(`APPEND [] xs = xs
/\ APPEND [a] xs = a :: xs
/\ APPEND [a; b] xs = a :: b :: xs
/\ APPEND [a; b; c] xs = a :: b :: c :: xs
/\ APPEND [a; b; c; d] xs = a :: b :: c :: d :: xs
/\ APPEND [a; b; c; d; e] xs = a :: b :: c :: d :: e :: xs
/\ APPEND [a; b; c; d; e; f] xs = a :: b :: c :: d :: e :: f :: xs
/\ APPEND [a; b; c; d; e; f; g] xs = a :: b :: c :: d :: e :: f :: g :: xs
/\ APPEND [a; b; c; d; e; f; g; h] xs = a :: b :: c :: d :: e :: f :: g :: h :: xs
/\ APPEND (a :: b :: c :: d :: e :: f :: g :: h :: i :: ys) xs =
a :: b :: c :: d :: e :: f :: g :: h :: i :: APPEND ys xs`,
REWRITE_TAC[APPEND]);;
let funpow_UNROLL5 = prove
(`funpow 0 f x = x
/\ funpow 1 f x = f x
/\ funpow 2 f x = f (f x)
/\ funpow 3 f x = f (f (f x))
/\ funpow 4 f x = f (f (f (f x)))
/\ funpow 5 f x = f (f (f (f (f x))))
/\ funpow n f x =
if n > 5 then funpow (n - 6) f (f (f (f (f (f (f x))))))
else funpow n f x`,
REPLICATE_TAC 6 (CONJ_TAC THENL [
REPEAT (ONCE_REWRITE_TAC[funpow_ALT] THEN REWRITE_TAC[ARITH]); ALL_TAC]) THEN
COND_CASES_TAC THEN REWRITE_TAC[] THEN POP_ASSUM (LABEL_TAC "h") THEN
REPLICATE_TAC 6 (GEN_REWRITE_TAC LAND_CONV [funpow_ALT] THEN COND_CASES_TAC THENL [
POP_ASSUM MP_TAC THEN USE_THEN "h" MP_TAC THEN TRY ARITH_TAC;
ALL_TAC
]) THEN
REPEAT (FIRST [AP_THM_TAC; AP_TERM_TAC]) THEN
REWRITE_TAC[ARITH_RULE `PRE n = n - 1`; ARITH_RULE `n - a - b = n - (a + b)`; ARITH]);;
let nth_UNROLL15 = prove
(`nth (a :: xs) 0 = a
/\ nth (a :: b :: xs) 1 = b
/\ nth (a :: b :: c :: xs) 2 = c
/\ nth (a :: b :: c :: d :: xs) 3 = d
/\ nth (a :: b :: c :: d :: e :: xs) 4 = e
/\ nth (a :: b :: c :: d :: e :: f :: xs) 5 = f
/\ nth (a :: b :: c :: d :: e :: f :: g :: xs) 6 = g
/\ nth (a :: b :: c :: d :: e :: f :: g :: h :: xs) 7 = h
/\ nth (a :: b :: c :: d :: e :: f :: g :: h :: i :: xs) 8 = i
/\ nth (a :: b :: c :: d :: e :: f :: g :: h :: i :: j :: xs) 9 = j
/\ nth (a :: b :: c :: d :: e :: f :: g :: h :: i :: j :: k :: xs) 10 = k
/\ nth (a :: b :: c :: d :: e :: f :: g :: h :: i :: j :: k :: l :: xs) 11 = l
/\ nth (a :: b :: c :: d :: e :: f :: g :: h :: i :: j :: k :: l :: m :: xs) 12 = m
/\ nth (a :: b :: c :: d :: e :: f :: g :: h :: i :: j :: k :: l :: m :: n :: xs) 13 = n
/\ nth (a :: b :: c :: d :: e :: f :: g :: h :: i :: j :: k :: l :: m :: n :: p :: xs) 14 = p
/\ nth (a :: b :: c :: d :: e :: f :: g :: h :: i :: j :: k :: l :: m :: n :: p :: q :: xs) 15 = q
/\ nth (a :: b :: c :: d :: e :: f :: g :: h :: i :: j :: k :: l :: m :: n :: p :: q :: xs) nn =
if nn > 15 then nth xs (nn - 16) else nth (a :: b :: c :: d :: e :: f :: g :: h :: i :: j :: k :: l :: m :: n :: p :: q :: xs) nn`,
REPLICATE_TAC 16 (CONJ_TAC THENL [REWRITE_TAC[nth_DEF; ARITH]; ALL_TAC]) THEN
COND_CASES_TAC THEN REWRITE_TAC[] THEN
POP_ASSUM (LABEL_TAC "h") THEN
REPEAT (ONCE_REWRITE_TAC[nth_DEF] THEN COND_CASES_TAC THENL [
POP_ASSUM MP_TAC THEN USE_THEN "h" MP_TAC THEN
REWRITE_TAC[ARITH_RULE `n - a - b = n - (a + b)`; ARITH] THEN ARITH_TAC;
ALL_TAC
]) THEN
REPEAT AP_TERM_TAC THEN
REWRITE_TAC[ARITH_RULE `n - a - b = n - (a + b)`; ARITH]);;
let maps_UNROLL7 = prove
(`maps f [] = []
/\ maps f [a] = f a
/\ maps f [a; b] = APPEND (f a) (f b)
/\ maps f [a; b; c] = APPEND (f a) (APPEND (f b) (f c))
/\ maps f [a; b; c; d] = APPEND (f a) (APPEND (f b) (APPEND (f c) (f d)))
/\ maps f [a; b; c; d; e] = APPEND (f a) (APPEND (f b) (APPEND (f c) (APPEND (f d) (f e))))
/\ maps f [a; b; c; d; e; g] = APPEND (f a) (APPEND (f b) (APPEND (f c) (APPEND (f d) (APPEND (f e) (f g)))))
/\ maps f [a; b; c; d; e; g; h] = APPEND (f a) (APPEND (f b) (APPEND (f c) (APPEND (f d) (APPEND (f e) (APPEND (f g) (f h))))))
/\ maps f (a :: b :: c :: d :: e :: g :: h :: i :: xs) =
APPEND (f a) (APPEND (f b) (APPEND (f c) (APPEND (f d) (APPEND (f e) (APPEND (f g) (APPEND (f h) (APPEND (f i) (maps f xs))))))))`,
REPEAT (CONJ_TAC THENL [REWRITE_TAC[maps_DEF; APPEND_NIL]; ALL_TAC]) THEN
REPEAT (GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [maps_DEF] THEN REWRITE_TAC[]));;
let count_UNROLL7 = prove
(`count p [] = 0
/\ count p [a] = bool_to_num (p a)
/\ count p [a; b] = bool_to_num (p a) + bool_to_num (p b)
/\ count p [a; b; c] = bool_to_num (p a) + bool_to_num (p b) + bool_to_num (p c)
/\ count p [a; b; c; d] = bool_to_num (p a) + bool_to_num (p b) + bool_to_num (p c) + bool_to_num (p d)
/\ count p [a; b; c; d; e] = bool_to_num (p a) + bool_to_num (p b) + bool_to_num (p c) + bool_to_num (p d) + bool_to_num (p e)
/\ count p [a; b; c; d; e; f] = bool_to_num (p a) + bool_to_num (p b) + bool_to_num (p c) + bool_to_num (p d) + bool_to_num (p e) + bool_to_num (p f)
/\ count p [a; b; c; d; e; f; g] = bool_to_num (p a) + bool_to_num (p b) + bool_to_num (p c) + bool_to_num (p d) + bool_to_num (p e) + bool_to_num (p f) + bool_to_num (p g)
/\ count p (a :: b :: c :: d :: e :: f :: g :: h :: xs) =
bool_to_num (p a) + bool_to_num (p b) + bool_to_num (p c) + bool_to_num (p d) + bool_to_num (p e) + bool_to_num (p f) + bool_to_num (p g) + bool_to_num (p h) + count p xs`,
REWRITE_TAC[count_CASES] THEN REPEAT CONJ_TAC THEN
REPEAT COND_CASES_TAC THEN REWRITE_TAC[bool_to_num_DEF] THEN
ARITH_TAC);;
let map_UNROLL11 = prove
(`map f [] = []
/\ map f [a] = [f a]
/\ map f [a; b] = [f a; f b]
/\ map f [a; b; c] = [f a; f b; f c]
/\ map f [a; b; c; d] = [f a; f b; f c; f d]
/\ map f [a; b; c; d; e] = [f a; f b; f c; f d; f e]
/\ map f [a; b; c; d; e; g] = [f a; f b; f c; f d; f e; f g]
/\ map f [a; b; c; d; e; g; h] = [f a; f b; f c; f d; f e; f g; f h]
/\ map f [a; b; c; d; e; g; h; i] = [f a; f b; f c; f d; f e; f g; f h; f i]
/\ map f [a; b; c; d; e; g; h; i; j] = [f a; f b; f c; f d; f e; f g; f h; f i; f j]
/\ map f [a; b; c; d; e; g; h; i; j; k] = [f a; f b; f c; f d; f e; f g; f h; f i; f j; f k]
/\ map f [a; b; c; d; e; g; h; i; j; k; l] = [f a; f b; f c; f d; f e; f g; f h; f i; f j; f k; f l]
/\ map f (a :: b :: c :: d :: e :: g :: h :: i :: j :: k :: l :: m :: xs) =
(f a :: f b :: f c :: f d :: f e :: f g :: f h :: f i :: f j :: f k :: f l :: f m :: map f xs)`,
REWRITE_TAC[map_CASES]);;
let pred_list_UNROLL11 = prove
(`pred_list p [] = T
/\ pred_list p [a] = p a
/\ pred_list p [a; b] = (p a /\ p b)
/\ pred_list p [a; b; c] = (p a /\ p b /\ p c)
/\ pred_list p [a; b; c; d] = (p a /\ p b /\ p c /\ p d)
/\ pred_list p [a; b; c; d; e] = (p a /\ p b /\ p c /\ p d /\ p e)
/\ pred_list p [a; b; c; d; e; g] = (p a /\ p b /\ p c /\ p d /\ p e /\ p g)
/\ pred_list p [a; b; c; d; e; g; h] = (p a /\ p b /\ p c /\ p d /\ p e /\ p g /\ p h)
/\ pred_list p [a; b; c; d; e; g; h; i] = (p a /\ p b /\ p c /\ p d /\ p e /\ p g /\ p h /\ p i)
/\ pred_list p [a; b; c; d; e; g; h; i; j] = (p a /\ p b /\ p c /\ p d /\ p e /\ p g /\ p h /\ p i /\ p j)
/\ pred_list p [a; b; c; d; e; g; h; i; j; k] = (p a /\ p b /\ p c /\ p d /\ p e /\ p g /\ p h /\ p i /\ p j /\ p k)
/\ pred_list p [a; b; c; d; e; g; h; i; j; k; l] = (p a /\ p b /\ p c /\ p d /\ p e /\ p g /\ p h /\ p i /\ p j /\ p k /\ p l)
/\ pred_list p (a :: b :: c :: d :: e :: g :: h :: i :: j :: k :: l :: m :: xs) =
(p a /\ p b /\ p c /\ p d /\ p e /\ p g /\ p h /\ p i /\ p j /\ p k /\ p l /\ p m /\ pred_list p xs)`,
REWRITE_TAC[pred_list_CASES]);;
let size_list_UNROLL15 = prove
(`size_list ([]:(A)list) = 0
/\ size_list [a:A] = 1
/\ size_list [a:A; b] = 2
/\ size_list [a:A; b; c] = 3
/\ size_list [a:A; b; c; d] = 4
/\ size_list [a:A; b; c; d; e] = 5
/\ size_list [a:A; b; c; d; e; f] = 6
/\ size_list [a:A; b; c; d; e; f; g] = 7
/\ size_list [a:A; b; c; d; e; f; g; h] = 8
/\ size_list [a:A; b; c; d; e; f; g; h; i] = 9
/\ size_list [a:A; b; c; d; e; f; g; h; i; j] = 10
/\ size_list [a:A; b; c; d; e; f; g; h; i; j; k] = 11
/\ size_list [a:A; b; c; d; e; f; g; h; i; j; k; l] = 12
/\ size_list [a:A; b; c; d; e; f; g; h; i; j; k; l; m] = 13
/\ size_list [a:A; b; c; d; e; f; g; h; i; j; k; l; m; n] = 14
/\ size_list [a:A; b; c; d; e; f; g; h; i; j; k; l; m; n; p] = 15
/\ size_list ((a:A)::b::c::d::e::f::g::h::i::j::k::l::m::n::p::q::rest) = gen_length 16 rest`,
REWRITE_TAC[size_list_DEF; gen_length_LENGTH; LENGTH] THEN ARITH_TAC);;
let size_list_UNROLL5 = prove
(`size_list ([]:(A)list) = 0
/\ size_list [a:A] = 1
/\ size_list [a:A; b] = 2
/\ size_list [a:A; b; c] = 3
/\ size_list [a:A; b; c; d] = 4
/\ size_list [a:A; b; c; d; e] = 5
/\ size_list ((a:A)::b::c::d::e::f::rest) = gen_length 6 rest`,
REWRITE_TAC[size_list_DEF; gen_length_LENGTH; LENGTH] THEN ARITH_TAC);;