1open HolKernel Parse boolLib;
2val _ = new_theory "sequence";
3
4open bossLib arithmeticTheory extra_numTheory combinTheory HurdUseful;
5
6infixr 0 ++ || ORELSEC;
7infix 1 >>;
8nonfix THEN ORELSE;
9
10val op++ = op THEN;
11val op|| = op ORELSE;
12val op>> = op THEN1;
13
14(* ------------------------------------------------------------------------- *)
15(* Definitions.                                                              *)
16(* ------------------------------------------------------------------------- *)
17
18val shd_def = Define `shd (f : num -> 'a) = f 0`;
19
20val stl_def = Define `stl (f : num -> 'a) n = f (SUC n)`;
21
22val scons_def = Define
23  `(scons (h : 'a) (t : num -> 'a) 0 = h) /\ (scons h t (SUC n) = t n)`;
24
25val sdest_def = Define `sdest = \s. (shd s, stl s)`;
26
27val sconst_def = Define `sconst = (K : 'a -> num -> 'a)`;
28
29val stake_def = Define
30  `(stake 0 s = []) /\ (stake (SUC n) s = shd s :: stake n (stl s))`;
31
32val sdrop_def = Define `(sdrop 0 = I) /\ (sdrop (SUC n) = sdrop n o stl)`;
33
34val eventually_def = Define `eventually x y = ?n. sdrop n x = sdrop n y`;
35
36(* ------------------------------------------------------------------------- *)
37(* Theorems.                                                                 *)
38(* ------------------------------------------------------------------------- *)
39
40val STL_PARTIAL = store_thm
41  ("STL_PARTIAL",
42   ``!f. stl f = f o SUC``,
43   FUN_EQ_TAC
44   ++ RW_TAC std_ss [stl_def, o_DEF]);
45
46val SCONS_SURJ = store_thm
47  ("SCONS_SURJ",
48   ``!x. ?h t. (x = scons h t)``,
49   STRIP_TAC
50   ++ EXISTS_TAC ``shd x``
51   ++ EXISTS_TAC ``stl x``
52   ++ FUN_EQ_TAC
53   ++ Cases >> RW_TAC std_ss [scons_def, shd_def]
54   ++ RW_TAC std_ss [scons_def, stl_def]);
55
56val SHD_STL_ISO = store_thm
57  ("SHD_STL_ISO",
58   ``!h t. ?x. (shd x = h) /\ (stl x = t)``,
59   REPEAT STRIP_TAC
60   ++ Q.EXISTS_TAC `\x. num_CASE x h t`
61   ++ RW_TAC arith_ss [shd_def]
62   ++ MATCH_MP_TAC EQ_EXT
63   ++ Cases >> RW_TAC std_ss [stl_def]
64   ++ RW_TAC std_ss [stl_def]);
65
66val SHD_SCONS = store_thm
67  ("SHD_SCONS",
68   ``!h t. shd (scons h t) = h``,
69   RW_TAC arith_ss [shd_def, scons_def]);
70
71val STL_SCONS = store_thm
72  ("STL_SCONS",
73   ``!h t. stl (scons h t) = t``,
74   Suff `!h t n. stl (scons h t) n = t n` >> PROVE_TAC [EQ_EXT]
75   ++ RW_TAC arith_ss [stl_def, scons_def]);
76
77val SHD_SCONST = store_thm
78  ("SHD_SCONST",
79   ``!b. shd (sconst b) = b``,
80   RW_TAC std_ss [sconst_def, K_DEF, shd_def]);
81
82val STL_SCONST = store_thm
83  ("STL_SCONST",
84   ``!b. stl (sconst b) = sconst b``,
85   STRIP_TAC
86   ++ FUN_EQ_TAC
87   ++ RW_TAC std_ss [sconst_def, K_DEF, stl_def]);
88
89val SCONS_SHD_STL = store_thm
90  ("SCONS_SHD_STL",
91   ``!x. scons (shd x) (stl x) = x``,
92   STRIP_TAC
93   ++ FUN_EQ_TAC
94   ++ Cases >> RW_TAC std_ss [scons_def, shd_def]
95   ++ RW_TAC std_ss [scons_def, stl_def]);
96
97val FST_o_SDEST = store_thm
98  ("FST_o_SDEST",
99   ``FST o sdest = shd``,
100   FUN_EQ_TAC
101   ++ RW_TAC std_ss [sdest_def, o_THM]);
102
103val SND_o_SDEST = store_thm
104  ("SND_o_SDEST",
105   ``SND o sdest = stl``,
106   FUN_EQ_TAC
107   ++ RW_TAC std_ss [sdest_def, o_THM]);
108
109val SEQUENCE_DEFINE = store_thm
110  ("SEQUENCE_DEFINE",
111   ``!phd ptl. ?g.
112       (!(x : 'a). shd (g x) = phd x) /\ (!(x : 'a). stl (g x) = g (ptl x))``,
113   RW_TAC std_ss []
114   ++ Q.EXISTS_TAC `\x n. phd (FUNPOW ptl n x)`
115   ++ FUN_EQ_TAC
116   ++ RW_TAC std_ss [shd_def, stl_def, FUNPOW]);
117
118val SCONS_EQ = store_thm
119  ("SCONS_EQ",
120   ``!x xs y ys. (scons x xs = scons y ys) = (x = y) /\ (xs = ys)``,
121   RW_TAC std_ss []
122   ++ REVERSE EQ_TAC >> PROVE_TAC []
123   ++ PROVE_TAC [SHD_SCONS, STL_SCONS]);
124
125val STL_o_SDROP = store_thm
126  ("STL_o_SDROP",
127   ``!n. stl o sdrop n = sdrop (SUC n)``,
128   Induct >> RW_TAC bool_ss [sdrop_def, I_o_ID]
129   ++ RW_TAC bool_ss [sdrop_def, o_ASSOC]);
130
131val SDROP_ADD = store_thm
132  ("SDROP_ADD",
133   ``!s x y. sdrop (x + y) s = sdrop x (sdrop y s)``,
134   Induct_on `y` >> RW_TAC list_ss [sdrop_def, I_THM]
135   ++ RW_TAC std_ss [ADD_CLAUSES, sdrop_def, o_THM]);
136
137val SDROP_EQ_MONO = store_thm
138  ("SDROP_EQ_MONO",
139   ``!m n x y. (sdrop m x = sdrop m y) /\ m <= n ==> (sdrop n x = sdrop n y)``,
140   RW_TAC std_ss [LESS_EQ_EXISTS]
141   ++ Induct_on `p` >> RW_TAC arith_ss []
142   ++ RW_TAC std_ss [ADD_CLAUSES, GSYM STL_o_SDROP, o_THM]);
143
144val EVENTUALLY_REFL = store_thm
145  ("EVENTUALLY_REFL",
146   ``!x. eventually x x``,
147   RW_TAC std_ss [eventually_def]);
148
149val EVENTUALLY_SYM = store_thm
150  ("EVENTUALLY_SYM",
151   ``!x y. eventually x y = eventually y x``,
152   RW_TAC std_ss [eventually_def]
153   ++ PROVE_TAC []);
154
155val EVENTUALLY_TRANS = store_thm
156  ("EVENTUALLY_TRANS",
157   ``!x y z. eventually x y /\ eventually y z ==> eventually x z``,
158   RW_TAC std_ss [eventually_def]
159   ++ Q.EXISTS_TAC `MAX n n'`
160   ++ PROVE_TAC [X_LE_MAX, LESS_EQ_REFL, SDROP_EQ_MONO]);
161
162val SEQUENCE_DEFINE_ALT = store_thm
163  ("SEQUENCE_DEFINE_ALT",
164   ``!phd ptl. ?g:'a->num->'b. !x. g x = scons (phd x) (g (ptl x))``,
165   RW_TAC std_ss []
166   ++ MP_TAC (Q.SPECL [`phd`, `ptl`] SEQUENCE_DEFINE)
167   ++ RW_TAC std_ss []
168   ++ Q.EXISTS_TAC `g`
169   ++ RW_TAC std_ss []
170   ++ MP_TAC (Q.ISPEC `(g:'a->num->'b) x` SCONS_SURJ)
171   ++ RW_TAC std_ss []
172   ++ Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`)
173   ++ Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`)
174   ++ RW_TAC std_ss [SCONS_EQ, SHD_SCONS, STL_SCONS]);
175
176local
177  val th =  prove
178    (``?s. !h t x. s h t x = scons (h x) (s h t (t x))``,
179     MP_TAC SEQUENCE_DEFINE_ALT
180     ++ RW_TAC std_ss [SKOLEM_THM])
181in
182  val siter_def = new_specification ("siter_def", ["siter"], th);
183end;
184
185val SHD_SITER = store_thm
186  ("SHD_SITER",
187   ``!h t x. shd (siter h t x) = h x``,
188   ONCE_REWRITE_TAC [siter_def]
189   ++ RW_TAC std_ss [SHD_SCONS]);
190
191val STL_SITER = store_thm
192  ("STL_SITER",
193   ``!h t x. stl (siter h t x) = siter h t (t x)``,
194   RW_TAC std_ss []
195   ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [siter_def]))
196   ++ RW_TAC std_ss [STL_SCONS]);
197
198val _ = export_theory ();
199