streamScript.sml

1Theory stream
2(* coalgebraic streams (infinite lists); bisimulation and BNF theorems proved *)
3
4Ancestors hol arithmetic pair pred_set
5Libs numLib
6
7Type stream = “:num -> 'a”
8
9Definition scons_def[simp]:
10  scons a s 0 = a ∧
11  scons a s (SUC n) = s n
12End
13
14Theorem scons_alt:
15  scons a s = λn. case n of
16                    0 => a
17                  | SUC m => s m
18Proof
19  simp[FUN_EQ_THM] >> Induct>> simp[]
20QED
21
22Overload shd[inferior] = “λs. s 0”
23Overload "" = “shd”
24
25Definition stl_def: stl s = λn. s (n + 1)
26End
27
28Theorem stl_cons[simp]:
29  stl (scons a s) = s
30Proof
31  simp[stl_def, scons_alt, GSYM ADD1, FUN_EQ_THM]
32QED
33
34Theorem shd_cons[simp]:
35  shd (scons a s) = a
36Proof
37  simp[scons_alt]
38QED
39
40Theorem scons_11[simp]:
41  scons a s = scons b t ⇔ a = b ∧ s = t
42Proof
43  simp[FUN_EQ_THM, scons_alt, AllCaseEqs(), SF CONJ_ss] >>
44  Cases_on ‘a = b’ >> simp[]
45  >- (rw[EQ_IMP_THM] >~
46      [‘s i = t i (* g *)’]
47      >- (first_x_assum $ qspec_then ‘SUC i’ mp_tac >> simp[]) >>
48      metis_tac[TypeBase.nchotomy_of “:num”]) >>
49  qexists ‘0’ >> simp[]
50QED
51
52Theorem scons_hdtl[simp]:
53  scons (shd s) (stl s) = s
54Proof
55  simp[FUN_EQ_THM, scons_alt, AllCaseEqs(), SF CONJ_ss, stl_def, ADD1] >>
56  metis_tac[TypeBase.nchotomy_of “:num”, ADD1]
57QED
58
59Theorem stream_cases:
60  ∀s. ∃h t. s = scons h t
61Proof
62  metis_tac[scons_hdtl]
63QED
64
65Theorem sbisimulation:
66  (s1 = s2) ⇔
67  ∃R. R s1 s2 ∧
68      ∀t1 t2.
69        R t1 t2 ⇒ shd t1 = shd t2 ∧ (R (stl t1) (stl t2) ∨ stl t1 = stl t2)
70Proof
71  iff_tac
72  >- (rw[] >> qexists ‘$=’ >> simp[]) >>
73  strip_tac >> simp[FUN_EQ_THM] >> qx_gen_tac ‘n’ >>
74  qpat_x_assum ‘R s1 s2’ mp_tac >> map_every Q.ID_SPEC_TAC [‘s1’, ‘s2’] >>
75  simp[PULL_FORALL] >> Induct_on ‘n’
76  >- (rpt strip_tac >> first_x_assum drule >> simp[]) >>
77  rpt strip_tac >> last_x_assum $ drule_then strip_assume_tac
78  >- (gvs[stl_def] >> first_x_assum drule >> simp[ADD1]) >>
79  gvs[stl_def, ADD1, FUN_EQ_THM]
80QED
81
82Definition siterate_def:
83  siterate f x = λn. FUNPOW f n x
84End
85
86Theorem shd_siterate[simp]:
87  shd (siterate f sd) = sd
88Proof
89  simp[siterate_def]
90QED
91
92Theorem stl_siterate[simp]:
93  stl (siterate f sd) = siterate f (f sd)
94Proof
95  simp[stl_def, siterate_def, FUN_EQ_THM, GSYM ADD1, FUNPOW]
96QED
97
98Theorem siterate_scons_eqn:
99  siterate f sd = scons sd (siterate f (f sd))
100Proof
101  simp[Once sbisimulation] >>
102  qexists
103    ‘λs1 s2. ∃sd. s1 = siterate f sd ∧ s2 = scons sd (siterate f (f sd))’ >>
104  rw[]>> simp[]
105QED
106
107Definition sunfold_def:
108  sunfold hd tl sd = λn. hd (siterate tl sd n)
109End
110
111Theorem sunfold_thm:
112  sunfold hd tl sd0 =
113  let a = hd sd0;
114      sd = tl sd0;
115  in
116    scons a (sunfold hd tl sd)
117Proof
118  simp[FUN_EQ_THM,sunfold_def,scons_alt] >> Cases >> simp[] >>
119  simp[siterate_def, FUNPOW]
120QED
121
122Definition smap_def:
123  smap f s = sunfold (f o shd) stl s
124End
125
126Theorem smap_thm[simp]:
127  smap f (scons a s) = scons (f a) (smap f s)
128Proof
129  simp[smap_def, SimpLHS, Once sunfold_thm] >>
130  simp[GSYM smap_def]
131QED
132
133Definition sset_def:
134  sset s = { a | ∃i. s i = a }
135End
136
137Theorem smapO:
138  smap f s = f o s
139Proof
140  simp[Once sbisimulation] >>
141  qexists ‘λs1 s2. ∃s. s1 = smap f s ∧ s2 = f o s’ >>
142  simp[] >> conj_tac >- metis_tac[] >>
143  simp[PULL_EXISTS] >> rw[]
144  >- (Cases_on ‘s’ using stream_cases >> simp[]) >>
145  ‘stl (smap f s) = smap f (stl s)’
146    by (Cases_on ‘s’ using stream_cases >> simp[]) >>
147  simp[] >> disj1_tac >> irule_at Any EQ_REFL>>
148  simp[stl_def, combinTheory.o_ABS_R]
149QED
150
151Theorem sset_map:
152  sset (smap f s) = IMAGE f (sset s)
153Proof
154  simp[smapO, EXTENSION, PULL_EXISTS, sset_def] >> metis_tac[]
155QED
156
157Theorem smap_smap_o:
158  smap f (smap g s) = smap (f o g) s
159Proof
160  simp[smapO]
161QED
162
163Theorem smap_ID:
164  smap (λx. x) s = s
165Proof
166  simp[smapO, FUN_EQ_THM]
167QED
168
169Theorem smap_CONG:
170  s1 = s2 ∧ (∀x. x ∈ sset s2 ⇒ f x = g x) ⇒ smap f s1 = smap g s2
171Proof
172  rw[] >> simp[smapO, FUN_EQ_THM] >> gvs[sset_def, PULL_EXISTS]
173QED
174
175Definition liftBin_def:
176  liftBin f (s1:'a stream) (s2:'b stream) = λi. f (s1 i) (s2 i)
177End
178
179Theorem liftBin_comm:
180  (∀x y. f x y = f y x) ⇒ liftBin f s1 s2 = liftBin f s2 s1
181Proof
182  strip_tac >> simp[Once sbisimulation] >>
183  qexists ‘λt1 t2. ∃s1 s2. t1 = liftBin f s1 s2 ∧ t2 = liftBin f s2 s1’ >>
184  simp[] >> conj_tac
185  >- metis_tac[] >>
186  simp[PULL_EXISTS] >> simp[liftBin_def, stl_def]
187QED
188
189Theorem shd_liftBin[simp]:
190  shd (liftBin f s1 s2) = f (shd s1) (shd s2)
191Proof
192  simp[liftBin_def]
193QED
194
195Theorem stl_liftBin[simp]:
196  stl (liftBin f s1 s2) = liftBin f (stl s1) (stl s2)
197Proof
198  simp[stl_def, liftBin_def]
199QED
200
201Definition szip_def: szip = liftBin (,)
202End
203
204Theorem szip_alt:
205  szip s1 s2 = λi. (s1 i, s2 i)
206Proof
207  simp[szip_def, liftBin_def]
208QED
209
210Theorem szip_thm[simp]:
211  szip (scons a s1) s2 = scons (a, shd s2) (szip s1 (stl s2)) ∧
212  szip s1 (scons b s2) = scons (shd s1, b) (szip (stl s1) s2)
213Proof
214  simp[szip_alt, FUN_EQ_THM] >> conj_tac >> Cases >> simp[stl_def, ADD1]
215QED
216
217Definition sunzip_def:
218  sunzip s = (smap FST s, smap SND s)
219End
220
221Theorem szip_unzip[simp]:
222  UNCURRY szip (sunzip s) = s ∧ sunzip (szip s1 s2) = (s1,s2)
223Proof
224  simp[sunzip_def, szip_alt] >>
225  simp[smapO, FUN_EQ_THM]
226QED
227
228Definition srel_def:
229  srel R s1 s2 ⇔ ∀i. R (s1 i) (s2 i)
230End
231
232Theorem srelpair_characterisation:
233  srel R s1 s2 ⇔ ∃sps. (∀a b. (a,b) ∈ sset sps ⇒ R a b) ∧
234                       smap FST sps = s1 ∧ smap SND sps = s2
235Proof
236  simp[srel_def, smapO, sset_def, PULL_EXISTS] >>
237  simp[EQ_IMP_THM, PULL_EXISTS] >> rw[] >> simp[]
238  >- (qexists ‘szip s1 s2’ >>
239      simp[combinTheory.o_ABS_R, FUN_EQ_THM, szip_alt])
240  >- (Cases_on ‘sps i’ >> simp[] >> metis_tac[])
241QED
242
243Theorem cardinality_bound:
244  countable (sset (s:'a stream))
245Proof
246  simp[countable_def] >> qexists ‘λa. LEAST i. s i = a’ >>
247  simp[INJ_IFF] >> rw[] >> gvs[sset_def] >> simp[EQ_IMP_THM] >>
248  LEAST_ELIM_TAC >> conj_tac >- metis_tac[] >> simp[] >>
249  LEAST_ELIM_TAC >> conj_tac >- metis_tac[] >> rw[]
250QED
251
252Definition sconst_def:
253  sconst x = λi. x
254End
255
256Theorem sconst_scons_eqn[simp]:
257  sconst x = scons x (sconst x)
258Proof
259  simp[sconst_def, scons_alt, FUN_EQ_THM] >> Cases >> simp[]
260QED
261
262Definition sdrop_def:
263  sdrop n s = FUNPOW stl n s
264End
265
266Theorem sdrop_thm[simp]:
267  sdrop 0 s = s ∧
268  sdrop (SUC n) s = stl (sdrop n s) ∧
269  sdrop (NUMERAL (BIT2 n)) s = stl (sdrop (NUMERAL (BIT1 n)) s) ∧
270  sdrop (NUMERAL (BIT1 n)) s = stl (sdrop (NUMERAL (BIT1 n) - 1) s)
271Proof
272  simp[sdrop_def, numeralTheory.numeral_funpow, PRE_SUB1] >>
273  simp[GSYM FUNPOW_SUC] >> simp[FUNPOW]
274QED
275
276Theorem sdrop_eq_mono:
277  ∀m n s t. sdrop m s = sdrop m t ∧ m ≤ n ⇒ sdrop n s = sdrop n t
278Proof
279  simp[sdrop_def, LESS_EQ_EXISTS, PULL_EXISTS] >> ONCE_REWRITE_TAC[ADD_COMM] >>
280  simp[FUNPOW_ADD]
281QED
282
283Theorem stl_sdrop:
284  stl (sdrop i s) = sdrop i (stl s)
285Proof
286  simp[sdrop_def, GSYM FUNPOW_SUC, FUNPOW]
287QED
288
289Definition sexists_def:
290  sexists P s = ∃i. P (s i)
291End
292
293Theorem sexists_thm[simp]:
294  sexists P (scons h t) ⇔ P h ∨ sexists P t
295Proof
296  simp[sexists_def, scons_alt] >>
297  simp[SimpLHS, Once EXISTS_NUM]
298QED
299
300Theorem sexists_ind:
301  ∀P.
302    (∀h t. P h ⇒ Q (scons h t)) ∧
303    (∀h t. Q t ∧ sexists P t ⇒ Q (scons h t)) ⇒
304    ∀s. sexists P s ⇒ Q s
305Proof
306  simp[sexists_def, PULL_EXISTS] >> gen_tac >> strip_tac >>
307  Induct_on ‘i’
308  >- (rpt strip_tac >> first_x_assum drule >>
309      disch_then $ qspec_then ‘stl s’ mp_tac >> simp[]) >>
310  rw[] >>
311  first_x_assum $ qspec_then ‘stl s’ mp_tac >>
312  ‘P (stl s i)’ by simp[stl_def, GSYM ADD1] >>
313  simp[] >> strip_tac >> first_x_assum drule_all >>
314  disch_then $ qspec_then ‘shd s’ mp_tac >> simp[]
315QED
316
317(* eventually two sequences exactly coincide *)
318Definition seventuallyeq_def:
319  seventuallyeq s t ⇔ ∃i. sdrop i s = sdrop i t
320End
321
322Theorem seventuallyeq_REFL:
323  seventuallyeq s s
324Proof
325  simp[seventuallyeq_def]
326QED
327
328Theorem seventuallyeq_SYM:
329  seventuallyeq s t ⇔ seventuallyeq t s
330Proof
331  metis_tac[seventuallyeq_def]
332QED
333
334Theorem seventuallyeq_TRANS:
335  seventuallyeq s t ∧ seventuallyeq t u ⇒ seventuallyeq s u
336Proof
337  simp[seventuallyeq_def, PULL_EXISTS] >> qx_genl_tac [‘i’, ‘j’] >>
338  strip_tac >> qexists ‘MAX i j’ >>
339  rpt (dxrule_then assume_tac sdrop_eq_mono) >>
340  rpt (first_x_assum (resolve_then Any assume_tac (iffRL $ cj 1 MAX_LE))) >>
341  metis_tac[LESS_EQ_REFL]
342QED
343
344Theorem seventuallyeq_ind:
345  ∀P.
346    (∀s. P s s) ∧
347    (∀h1 h2 s t. P s t ∧ seventuallyeq s t ⇒ P (scons h1 s) (scons h2 t)) ⇒
348    ∀s t. seventuallyeq s t ⇒ P s t
349Proof
350  simp[seventuallyeq_def, PULL_EXISTS] >> gen_tac >> strip_tac >>
351  Induct_on ‘i’ >> simp[] >> rw[] >>
352  Cases_on ‘s’ using stream_cases >>
353  Cases_on ‘t’ using stream_cases >>
354  last_x_assum irule >> gvs[stl_sdrop] >> metis_tac[]
355QED