llistScript.sml
1(* ===================================================================== *)
2(* FILE : llistScript.sml *)
3(* DESCRIPTION : Possibly infinite sequences (llist) *)
4(* ===================================================================== *)
5Theory llist
6Ancestors
7 option combin option pair num arithmetic prim_rec list
8 rich_list While pair pred_set set_relation arithmetic
9Libs
10 BasicProvers boolSimps markerLib hurdUtils
11
12
13val _ = temp_delsimps ["NORMEQ_CONV"]
14
15(* conflict with listTheory.EXISTS_DEF *)
16val EXISTS_DEF = boolTheory.EXISTS_DEF;
17
18(* ----------------------------------------------------------------------
19 The representing type is :num -> 'a option
20 ---------------------------------------------------------------------- *)
21
22CoInductive lrep_ok:
23 (lrep_ok (λn. NONE))
24/\ (lrep_ok t ==> lrep_ok (λn. if n = 0 then SOME h else t(n - 1)))
25End
26
27Theorem lrep_ok_alt'[local]:
28 !n f. lrep_ok f ==> IS_SOME (f (SUC n)) ==> IS_SOME (f n)
29Proof
30 let open arithmeticTheory in
31 Induct THEN REPEAT STRIP_TAC THEN
32 IMP_RES_TAC lrep_ok_cases THEN
33 FULL_SIMP_TAC bool_ss [NOT_SUC, IS_SOME_DEF,
34 ONE, SUB_EQUAL_0, SUB_MONO_EQ, SUB_0] end
35QED
36
37Theorem lrep_ok_alt:
38 lrep_ok f = (!n. IS_SOME (f (SUC n)) ==> IS_SOME (f n))
39Proof
40 EQ_TAC THEN REPEAT STRIP_TAC
41 >- (irule lrep_ok_alt' >> rpt conj_tac >> FIRST_ASSUM ACCEPT_TAC) THEN
42 irule lrep_ok_coind THEN
43 Q.EXISTS_TAC ‘λf. !n. IS_SOME (f (SUC n)) ==> IS_SOME (f n)’ THEN
44 ASM_SIMP_TAC bool_ss [] THEN
45 REPEAT STRIP_TAC THEN
46 Cases_on ‘a0 0’
47 >- (DISJ1_TAC THEN
48 SIMP_TAC bool_ss [FUN_EQ_THM] THEN
49 Induct THEN1 POP_ASSUM ACCEPT_TAC THEN
50 FULL_SIMP_TAC bool_ss [GSYM NOT_IS_SOME_EQ_NONE] THEN
51 PROVE_TAC []) >>
52 DISJ2_TAC THEN
53 Q.EXISTS_TAC ‘x’ THEN Q.EXISTS_TAC ‘a0 o SUC’ THEN
54 ASM_SIMP_TAC std_ss [FUN_EQ_THM] THEN
55 GEN_TAC THEN Cases_on ‘n’ THEN
56 ASM_SIMP_TAC bool_ss [NOT_SUC, SUC_SUB1]
57QED
58
59Theorem type_inhabited[local]:
60 ?f. lrep_ok f
61Proof Q.EXISTS_TAC `λn. NONE` THEN ACCEPT_TAC(CONJUNCT1 lrep_ok_rules)
62QED
63
64val llist_tydef = new_type_definition ("llist", type_inhabited);
65
66val repabs_fns = define_new_type_bijections {
67 name = "llist_absrep",
68 ABS = "llist_abs",
69 REP = "llist_rep",
70 tyax = llist_tydef};
71
72val llist_absrep = CONJUNCT1 repabs_fns
73val llist_repabs = CONJUNCT2 repabs_fns
74
75Theorem lrep_ok_llist_rep[local,simp]:
76 lrep_ok (llist_rep f)
77Proof
78 SRW_TAC [][llist_repabs, llist_absrep]
79QED
80
81Theorem llist_abs_11[local]:
82 lrep_ok r1 /\ lrep_ok r2 ==> ((llist_abs r1 = llist_abs r2) = (r1 = r2))
83Proof SRW_TAC [][llist_repabs, EQ_IMP_THM] THEN METIS_TAC []
84QED
85
86Theorem llist_rep_11[local]:
87 (llist_rep t1 = llist_rep t2) = (t1 = t2)
88Proof
89 SRW_TAC [][EQ_IMP_THM] THEN
90 POP_ASSUM (MP_TAC o AP_TERM ``llist_abs``) THEN SRW_TAC [][llist_absrep]
91QED
92
93val llist_repabs' = #1 (EQ_IMP_RULE (SPEC_ALL llist_repabs))
94
95Theorem llist_if_rep_abs[local]: (f = llist_rep a) ==> (a = llist_abs f)
96Proof DISCH_TAC THEN ASM_REWRITE_TAC [repabs_fns]
97QED
98
99Theorem FUNPOW_BIND_NONE[local]:
100 !n. FUNPOW (λm. OPTION_BIND m g) n NONE = NONE
101Proof Induct THEN ASM_SIMP_TAC bool_ss [FUNPOW, OPTION_BIND_def]
102QED
103
104Theorem lrep_ok_MAP:
105 lrep_ok (λn. OPTION_MAP f (g n)) = lrep_ok g
106Proof SIMP_TAC bool_ss [lrep_ok_alt, IS_SOME_MAP]
107QED
108
109Theorem lrep_ok_FUNPOW_BIND:
110 lrep_ok (λn. FUNPOW (λm. OPTION_BIND m g) n fz)
111Proof
112 SIMP_TAC bool_ss [lrep_ok_alt, FUNPOW_SUC] THEN
113 GEN_TAC THEN MATCH_ACCEPT_TAC IS_SOME_BIND
114QED
115
116Theorem lrep_ok_MAP_FUNPOW_BIND[local]:
117 lrep_ok (λn. OPTION_MAP f (FUNPOW (λm. OPTION_BIND m g) n fz))
118Proof SIMP_TAC bool_ss [lrep_ok_MAP] THEN irule lrep_ok_FUNPOW_BIND
119QED
120
121Definition LNIL[nocompute]: LNIL = llist_abs (λn. NONE)
122End
123Definition LCONS[nocompute]:
124 LCONS h t = llist_abs (λn. if n = 0 then SOME h else llist_rep t (n - 1))
125End
126
127Theorem llist_rep_LCONS:
128 llist_rep (LCONS h t) =
129 λn. if n = 0 then SOME h else llist_rep t (n - 1)
130Proof
131 SRW_TAC [][LCONS, GSYM llist_repabs] THEN
132 MATCH_MP_TAC (CONJUNCT2 lrep_ok_rules) THEN SRW_TAC [][]
133QED
134
135Theorem llist_rep_LNIL: llist_rep LNIL = \n. NONE
136Proof SIMP_TAC std_ss [LNIL, lrep_ok_rules, llist_repabs']
137QED
138
139Definition LTL_HD_def[nocompute]:
140 LTL_HD ll = case llist_rep ll 0 of
141 NONE => NONE
142 | SOME h => SOME (llist_abs (llist_rep ll o SUC), h)
143End
144
145Theorem LTL_HD_LNIL[compute,simp]:
146 LTL_HD LNIL = NONE
147Proof
148 SIMP_TAC std_ss [LTL_HD_def, llist_rep_LNIL]
149QED
150
151Theorem lr_eta[local]: (\n. llist_rep t n) = llist_rep t
152Proof irule ETA_AX
153QED
154
155Theorem LTL_HD_LCONS[compute,simp]: LTL_HD (LCONS h t) = SOME (t, h)
156Proof
157 SIMP_TAC std_ss [LTL_HD_def, llist_rep_LCONS, o_ABS_L,
158 NOT_SUC, lr_eta, llist_absrep]
159QED
160
161Definition LHD[nocompute]: LHD ll = llist_rep ll 0
162End
163Definition LTL[nocompute]:
164 LTL ll = case LHD ll of
165 NONE => NONE
166 | SOME _ => SOME (llist_abs (\n. llist_rep ll (n + 1)))
167End
168
169Theorem LTL_HD_HD: LHD ll = OPTION_MAP SND (LTL_HD ll)
170Proof
171 Cases_on `llist_rep ll 0` THEN ASM_SIMP_TAC std_ss [LTL_HD_def, LHD]
172QED
173
174Theorem LTL_HD_TL: LTL ll = OPTION_MAP FST (LTL_HD ll)
175Proof
176 Cases_on `llist_rep ll 0` THEN
177 ASM_SIMP_TAC std_ss [LTL_HD_def, LTL, LHD] THEN
178 AP_TERM_TAC THEN SIMP_TAC std_ss [FUN_EQ_THM, ADD1]
179QED
180
181Theorem LHD_LCONS: LHD (LCONS h t) = SOME h
182Proof SRW_TAC [][LHD, llist_rep_LCONS]
183QED
184
185Theorem LTL_LCONS: LTL (LCONS h t) = SOME t
186Proof SRW_TAC [ETA_ss][LTL, llist_rep_LCONS, llist_absrep, LHD_LCONS]
187QED
188
189(*---------------------------------------------------------------------------*)
190(* Syntax for lazy lists, similar to lists *)
191(*---------------------------------------------------------------------------*)
192
193val _ = add_rule {term_name = "LCONS", fixity = Infixr 490,
194 pp_elements = [TOK ":::", BreakSpace(0,2)],
195 paren_style = OnlyIfNecessary,
196 block_style = (AroundSameName, (PP.INCONSISTENT, 2))};
197
198val _ = add_listform {separator = [TOK ";", BreakSpace(1,0)],
199 leftdelim = [TOK "[|"], rightdelim = [TOK "|]"],
200 cons = "LCONS", nilstr = "LNIL",
201 block_info = (PP.INCONSISTENT, 2)};
202val _ = TeX_notation {hol = "[|", TeX = ("\\HOLTokenLeftDenote{}", 1)}
203val _ = TeX_notation {hol = "|]", TeX = ("\\HOLTokenRightDenote{}", 1)}
204
205Theorem LHDTL_CONS_THM = Q.GENL [‘h’, ‘t’] $ CONJ LHD_LCONS LTL_LCONS
206
207Theorem lrep_inversion[local]:
208 lrep_ok f ==> (f = \n. NONE) \/
209 (?h t. (f = \n. if n = 0 then SOME h else t (n - 1)) /\
210 lrep_ok t)
211Proof
212 MATCH_ACCEPT_TAC (fst (EQ_IMP_RULE (SPEC_ALL lrep_ok_cases)))
213QED
214
215Theorem forall_llist[local]:
216 (!l. P l) = (!r. lrep_ok r ==> P (llist_abs r))
217Proof
218 SRW_TAC [][EQ_IMP_THM] THEN
219 ONCE_REWRITE_TAC [GSYM llist_absrep] THEN
220 SRW_TAC [][]
221QED
222
223Theorem llist_CASES:
224 !l. (l = LNIL) \/ (?h t. l = LCONS h t)
225Proof
226 SIMP_TAC (srw_ss() ++ ETA_ss) [LNIL,LCONS,forall_llist,llist_abs_11,
227 lrep_ok_rules] THEN
228 REPEAT STRIP_TAC THEN IMP_RES_TAC lrep_inversion THENL [
229 SRW_TAC [][],
230 DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`h`, `llist_abs t`] THEN
231 SRW_TAC [][llist_repabs']
232 ]
233QED
234
235fun llist_CASE_TAC tm = STRUCT_CASES_TAC (ISPEC tm llist_CASES) ;
236
237Theorem LCONS_NOT_NIL[simp]:
238 !h t. ~(LCONS h t = LNIL) /\ ~(LNIL = LCONS h t)
239Proof
240 SRW_TAC [][LCONS, LNIL, FUN_EQ_THM] THEN STRIP_TAC THEN
241 POP_ASSUM (ASSUME_TAC o Q.AP_TERM `llist_rep`) THEN
242 FULL_SIMP_TAC (srw_ss() ++ ETA_ss) [llist_repabs', lrep_ok_rules] THEN
243 POP_ASSUM (ASSUME_TAC o C AP_THM ``0``) THEN
244 FULL_SIMP_TAC (srw_ss()) []
245QED
246
247Theorem LCONS_11[simp]:
248 !h1 t1 h2 t2. (LCONS h1 t1 = LCONS h2 t2) <=> (h1 = h2) /\ (t1 = t2)
249Proof
250 SRW_TAC [][EQ_IMP_THM, LCONS] THEN
251 POP_ASSUM (ASSUME_TAC o Q.AP_TERM `llist_rep`) THEN
252 FULL_SIMP_TAC (srw_ss() ++ ETA_ss) [llist_repabs', lrep_ok_rules] THENL [
253 POP_ASSUM (MP_TAC o C AP_THM ``0``) THEN SRW_TAC [][],
254 ALL_TAC
255 ] THEN
256 POP_ASSUM (MP_TAC o GEN ``n:num`` o SIMP_RULE (srw_ss()) [] o
257 C AP_THM ``SUC n:num``) THEN
258 SRW_TAC [ETA_ss][GSYM FUN_EQ_THM, llist_rep_11]
259QED
260
261Theorem LTL_HD_11[simp]:
262 LTL_HD ll1 = LTL_HD ll2 <=> ll1 = ll2
263Proof
264 llist_CASE_TAC ``ll1 : 'a llist`` THEN
265 llist_CASE_TAC ``ll2 : 'a llist`` THEN
266 simp[EQ_IMP_THM]
267QED
268
269Theorem LHD_THM[simp,compute]:
270 (LHD LNIL = NONE) /\ (!h t. LHD (LCONS h t) = SOME h)
271Proof
272 SRW_TAC [][LHDTL_CONS_THM] THEN
273 SRW_TAC [][LHD, LNIL, llist_repabs', lrep_ok_rules]
274QED
275
276Theorem LTL_THM[simp,compute]:
277 (LTL LNIL = NONE) /\ (!h t. LTL (LCONS h t) = SOME t)
278Proof
279 SRW_TAC [][LHDTL_CONS_THM] THEN
280 SRW_TAC [][LTL, LNIL, llist_repabs', lrep_ok_rules, LHD]
281QED
282
283Theorem LTL_HD_iff:
284 ((LTL_HD x = SOME (t, h)) = (x = LCONS h t)) /\
285 ((LTL_HD x = NONE) = (x = LNIL))
286Proof
287 llist_CASE_TAC ``x :'a llist`` THEN
288 SIMP_TAC std_ss [LTL_HD_LCONS, LTL_HD_LNIL, LCONS_NOT_NIL, LCONS_11] THEN
289 DECIDE_TAC
290QED
291
292Theorem LHD_EQ_NONE[simp]:
293 !ll. ((LHD ll = NONE) = (ll = LNIL)) /\ ((NONE = LHD ll) = (ll = LNIL))
294Proof
295 GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `ll` llist_CASES) THEN
296 SRW_TAC [][]
297QED
298
299Theorem LTL_EQ_NONE[simp]:
300 !ll. ((LTL ll = NONE) = (ll = LNIL)) /\ ((NONE = LTL ll) = (ll = LNIL))
301Proof
302 GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `ll` llist_CASES) THEN
303 SRW_TAC [][LTL_THM]
304QED
305
306Theorem LHDTL_EQ_SOME:
307 !h t ll. (ll = LCONS h t) <=> (LHD ll = SOME h) /\ (LTL ll = SOME t)
308Proof
309 REPEAT GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `ll` llist_CASES) THEN
310 SRW_TAC [][LHD_THM, LTL_THM]
311QED
312
313
314(* ----------------------------------------------------------------------
315 indexing into lazy lists
316
317 LNTH : num -> 'a llist -> 'a option
318 ---------------------------------------------------------------------- *)
319
320Definition LNTH[nocompute]:
321 (LNTH 0 ll = LHD ll) /\
322 (LNTH (SUC n) ll = OPTION_JOIN (OPTION_MAP (LNTH n) (LTL ll)))
323End
324
325Theorem LNTH_THM[simp]:
326 (!n. LNTH n LNIL = NONE) /\
327 (!h t. LNTH 0 (LCONS h t) = SOME h) /\
328 (!n h t. LNTH (SUC n) (LCONS h t) = LNTH n t)
329Proof
330 SRW_TAC [][LNTH] THEN Induct_on `n` THEN
331 SRW_TAC [][LNTH]
332QED
333
334(* ----------------------------------------------------------------------
335 LNTH is just llist_rep with arguments swapped
336 ---------------------------------------------------------------------- *)
337
338Theorem LNTH_rep:
339 !i ll. LNTH i ll = llist_rep ll i
340Proof
341 Induct THEN GEN_TAC THEN llist_CASE_TAC ``ll : 'a llist`` THEN
342 ASM_SIMP_TAC std_ss [LNTH_THM, llist_rep_LCONS, llist_rep_LNIL, NOT_SUC]
343QED
344
345(* can also prove that two lists are equal "extensionally", by showing
346 that LNTH is everywhere the same over them *)
347Theorem LNTH_llist_rep[local]:
348 !n r. lrep_ok r ==> (LNTH n (llist_abs r) = r n)
349Proof
350 SIMP_TAC bool_ss [LNTH_rep, llist_repabs']
351QED
352
353Theorem LNTH_EQ:
354 !ll1 ll2. (ll1 = ll2) = (!n. LNTH n ll1 = LNTH n ll2)
355Proof
356 SIMP_TAC (srw_ss()) [forall_llist, LNTH_llist_rep, llist_abs_11,
357 FUN_EQ_THM]
358QED
359
360(*---------------------------------------------------------------------------*)
361(* LUNFOLD by definition *)
362(* *)
363(* Formerly we got LUNFOLD by Skolemization using llist_Axiom_1 *)
364(* which was proved independently *)
365(*---------------------------------------------------------------------------*)
366
367Definition LUNFOLD_def[nocompute]: LUNFOLD f z = llist_abs (\n. OPTION_MAP SND
368 (FUNPOW (\m. OPTION_BIND m (UNCURRY (K o f))) n (f z)))
369End
370
371(* would be somewhat ok to add this presentation to compset if you'd
372 applied set_skip to option_CASE, as in:
373 computeLib.set_skip computeLib.the_compset ``option_CASE`` (SOME 1)
374 and you never had a concrete function f that actually wanted to generate
375 an infinite list.
376*)
377Theorem LUNFOLD:
378 !f x.
379 LUNFOLD f x =
380 case f x of NONE => [||] | SOME (v1,v2) => v2 ::: LUNFOLD f v1
381Proof
382 REPEAT GEN_TAC THEN
383 REWRITE_TAC [LUNFOLD_def] THEN
384 irule (GSYM llist_if_rep_abs) THEN
385 Cases_on `f x` THEN
386 ASM_SIMP_TAC std_ss [llist_rep_LCONS, llist_rep_LNIL, pair_CASE_def,
387 FUNPOW_BIND_NONE, OPTION_MAP_DEF, FUN_EQ_THM] THEN
388 GEN_TAC THEN Cases_on `n` THEN
389 SIMP_TAC std_ss [FUNPOW, OPTION_MAP_DEF, NOT_SUC, UNCURRY_VAR,
390 SUC_SUB1, OPTION_BIND_def, llist_repabs', lrep_ok_MAP_FUNPOW_BIND]
391QED
392
393(* this is the uniqueness in the definition of llist as final coalgebra *)
394Theorem LUNFOLD_UNIQUE:
395 !f g. (!x. g x = case f x of NONE => [||]
396 | SOME (v1,v2) => v2:::g v1) ==>
397 (!y. g y = LUNFOLD f y)
398Proof
399 REWRITE_TAC [LNTH_EQ] THEN
400 REPEAT GEN_TAC THEN DISCH_TAC THEN
401 Induct_on `n` THEN GEN_TAC THEN
402 ONCE_ASM_REWRITE_TAC [LUNFOLD] THEN
403 Cases_on `f y` THEN SIMP_TAC std_ss [pair_CASE_def, LNTH_THM] THEN
404 FIRST_ASSUM MATCH_ACCEPT_TAC
405QED
406
407(* LUNFOLD is a sort of inverse to LTL_HD *)
408val lu1 = BETA_RULE
409 (ISPECL [``LTL_HD``, ``(\x. x) : 'a llist -> 'a llist``] LUNFOLD_UNIQUE) ;
410
411Theorem LUNFOLD_LTL_HD: LUNFOLD LTL_HD ll = ll:'a llist
412Proof
413 irule EQ_SYM THEN irule lu1 THEN
414 qx_gen_tac ‘x’ >> llist_CASE_TAC “x:'a llist” >> simp[]
415QED
416
417Theorem LTL_HD_LUNFOLD[simp,compute]:
418 LTL_HD (LUNFOLD f x) = OPTION_MAP (LUNFOLD f ## I) (f x)
419Proof
420 ONCE_REWRITE_TAC [LUNFOLD] THEN CASE_TAC THEN
421 SIMP_TAC std_ss [OPTION_MAP_DEF, pair_CASE_def, LTL_HD_LNIL,
422 LTL_HD_LCONS, PAIR_MAP]
423QED
424
425Theorem LNTH_LUNFOLD[simp]:
426 (LNTH 0 (LUNFOLD f x) = OPTION_MAP SND (f x)) /\
427 (LNTH (SUC n) (LUNFOLD f x) =
428 case f x of NONE => NONE
429 | SOME (tx, hx) => LNTH n (LUNFOLD f tx))
430Proof
431 CONV_TAC (ONCE_DEPTH_CONV (LHS_CONV (ONCE_DEPTH_CONV (REWR_CONV LUNFOLD))))
432 THEN Cases_on `f x` THEN
433 REWRITE_TAC [LNTH, option_case_def, pair_CASE_def] THEN BETA_TAC THEN
434 REWRITE_TAC [LHD_THM, LTL_THM, OPTION_MAP_DEF, OPTION_JOIN_DEF]
435QED
436
437Theorem LNTH_LUNFOLD_compute[compute] =
438 CONJ (CONJUNCT1 LNTH_LUNFOLD)
439 (CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV
440 (LNTH_LUNFOLD |> CONJUNCT2 |> Q.GEN `n`))
441
442Theorem LHD_LUNFOLD[compute,simp]:
443 LHD (LUNFOLD f x) = OPTION_MAP SND (f x)
444Proof
445 REWRITE_TAC [GSYM LNTH, LNTH_LUNFOLD]
446QED
447
448Theorem LTL_LUNFOLD[compute,simp]:
449 LTL (LUNFOLD f x) = OPTION_MAP (LUNFOLD f o FST) (f x)
450Proof
451 REWRITE_TAC [LTL_HD_TL, LTL_HD_LUNFOLD, OPTION_MAP_COMPOSE] THEN
452 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC) THEN
453 SIMP_TAC std_ss [FUN_EQ_THM, FST_PAIR_MAP]
454QED
455
456(*---------------------------------------------------------------------------*)
457(* Co-recursion theorem for lazy lists *)
458(*---------------------------------------------------------------------------*)
459
460(*---------------------------------------------------------------------------*)
461(* Alternative version of llist_Axiom (more understandable) *)
462(*---------------------------------------------------------------------------*)
463
464Theorem llist_Axiom_1:
465 !f :'a -> ('a#'b)option.
466 ?g:'a -> 'b llist.
467 !x. g x =
468 case f x of
469 NONE => LNIL
470 | SOME (a,b) => LCONS b (g a)
471Proof
472 GEN_TAC THEN Q.EXISTS_TAC `LUNFOLD f` THEN
473 GEN_TAC THEN MATCH_ACCEPT_TAC LUNFOLD
474QED
475
476Theorem llist_Axiom_1ue:
477 !f. ?!g. !x. g x = case f x of NONE => LNIL
478 | SOME (a,b) => b ::: g a
479Proof
480 SIMP_TAC bool_ss [EXISTS_UNIQUE_THM] THEN REPEAT STRIP_TAC
481 THENL [
482 Q.EXISTS_TAC `LUNFOLD f` THEN GEN_TAC THEN MATCH_ACCEPT_TAC LUNFOLD,
483 IMP_RES_TAC LUNFOLD_UNIQUE THEN ASM_SIMP_TAC bool_ss [FUN_EQ_THM]
484 ]
485QED
486
487Theorem eq_imp_lem[local]:
488 (p = q) ==> p ==> q
489Proof DECIDE_TAC
490QED
491
492Theorem llist_ue_Axiom:
493 !f : 'a -> ('a # 'b) option.
494 ?!g : 'a -> 'b llist.
495 (!x. LHD (g x) = OPTION_MAP SND (f x)) /\
496 (!x. LTL (g x) = OPTION_MAP (g o FST) (f x))
497Proof
498 MP_TAC llist_Axiom_1ue THEN
499 MATCH_MP_TAC eq_imp_lem THEN
500 AP_TERM_TAC THEN SIMP_TAC bool_ss [FUN_EQ_THM, GSYM FORALL_AND_THM] THEN
501 Q.X_GEN_TAC `f` THEN
502 AP_TERM_TAC THEN SIMP_TAC bool_ss [FUN_EQ_THM] THEN Q.X_GEN_TAC `g` THEN
503 AP_TERM_TAC THEN SIMP_TAC bool_ss [FUN_EQ_THM] THEN GEN_TAC THEN
504 Cases_on `f x` THEN llist_CASE_TAC ``(g : 'a -> 'b llist) x`` THEN
505 SIMP_TAC std_ss [OPTION_MAP_DEF, LHD_THM, LTL_THM, pair_CASE_def,
506 LCONS_NOT_NIL, LCONS_11]
507QED
508
509Theorem llist_Axiom:
510 !f : 'a -> ('a # 'b) option.
511 ?g.
512 (!x. LHD (g x) = OPTION_MAP SND (f x)) /\
513 (!x. LTL (g x) = OPTION_MAP (g o FST) (f x))
514Proof
515 MATCH_ACCEPT_TAC
516 (CONJUNCT1
517 (SIMP_RULE bool_ss [EXISTS_UNIQUE_THM, FORALL_AND_THM] llist_ue_Axiom))
518QED
519
520(* ----------------------------------------------------------------------
521 Another consequence of the finality theorem is the principle of
522 bisimulation, including for lists unfolded from different generators
523 ---------------------------------------------------------------------- *)
524
525Theorem LUNFOLD_BISIMULATION:
526 !f1 f2 x1 x2. (LUNFOLD f1 x1 = LUNFOLD f2 x2) =
527 ?R. R x1 x2 /\
528 !y1 y2. R y1 y2 ==>
529 (f1 y1 = NONE) /\ (f2 y2 = NONE) \/
530 ?h t1 t2.
531 (f1 y1 = SOME (t1, h)) /\ (f2 y2 = SOME (t2, h)) /\ R t1 t2
532Proof
533 REPEAT GEN_TAC THEN EQ_TAC THENL [
534 DISCH_THEN (fn th =>
535 Q.EXISTS_TAC `\x1 x2. LUNFOLD f1 x1 = LUNFOLD f2 x2` THEN
536 SIMP_TAC std_ss [th]) THEN
537 REPEAT GEN_TAC THEN
538 DISCH_THEN (MP_TAC o ONCE_REWRITE_RULE [LUNFOLD]) THEN
539 REPEAT CASE_TAC THEN SIMP_TAC std_ss [LCONS_NOT_NIL, LCONS_11],
540 STRIP_TAC THEN POP_ASSUM_LIST (MAP_EVERY ASSUME_TAC) THEN
541 POP_ASSUM MP_TAC THEN
542 Q.SPEC_TAC (`x1`, `x1`) THEN Q.SPEC_TAC (`x2`, `x2`) THEN
543 Ho_Rewrite.REWRITE_TAC [LNTH_EQ, PULL_FORALL] THEN
544 Induct_on `n` THEN REPEAT STRIP_TAC THEN
545 ONCE_REWRITE_TAC [LUNFOLD] THEN RES_TAC THEN
546 ASM_SIMP_TAC std_ss [pair_CASE_def, LNTH_THM] ]
547QED
548
549Theorem LLIST_BISIMULATION0:
550 !ll1 ll2. (ll1 = ll2) =
551 ?R. R ll1 ll2 /\
552 !ll3 ll4. R ll3 ll4 ==>
553 (ll3 = LNIL) /\ (ll4 = LNIL) \/
554 ?h t1 t2.
555 (ll3 = h:::t1) /\ (ll4 = h:::t2) /\
556 R t1 t2
557Proof
558 REPEAT GEN_TAC THEN
559 CONV_TAC (LHS_CONV (ONCE_DEPTH_CONV (REWR_CONV (SYM LUNFOLD_LTL_HD)))) THEN
560 REWRITE_TAC [LUNFOLD_BISIMULATION] THEN
561 REPEAT (FIRST [AP_TERM_TAC, ABS_TAC, AP_THM_TAC]) THEN
562 SIMP_TAC std_ss [LTL_HD_iff]
563QED
564
565Theorem LLIST_BISIMULATION:
566 !ll1 ll2.
567 (ll1 = ll2) =
568 ?R. R ll1 ll2 /\
569 !ll3 ll4.
570 R ll3 ll4 ==>
571 (ll3 = [||]) /\ (ll4 = [||]) \/
572 (LHD ll3 = LHD ll4) /\ R (THE (LTL ll3)) (THE (LTL ll4))
573Proof
574 REPEAT GEN_TAC THEN EQ_TAC THENL [
575 DISCH_THEN SUBST_ALL_TAC THEN Q.EXISTS_TAC `(=)` THEN SRW_TAC [][],
576 STRIP_TAC THEN ONCE_REWRITE_TAC [LLIST_BISIMULATION0] THEN
577 Q.EXISTS_TAC `R` THEN SRW_TAC [][] THEN
578 `(ll3 = [||]) /\ (ll4 = [||]) \/
579 (LHD ll3 = LHD ll4) /\ R (THE (LTL ll3)) (THE (LTL ll4))`
580 by METIS_TAC [] THEN
581 SRW_TAC [][] THEN
582 Q.SPEC_THEN `ll3` FULL_STRUCT_CASES_TAC llist_CASES THEN
583 FULL_SIMP_TAC (srw_ss()) [] THEN
584 Q.SPEC_THEN `ll4` FULL_STRUCT_CASES_TAC llist_CASES THEN
585 FULL_SIMP_TAC (srw_ss()) []
586 ]
587QED
588
589Theorem LLIST_STRONG_BISIMULATION:
590 !ll1 ll2.
591 (ll1 = ll2) =
592 ?R. R ll1 ll2 /\
593 !ll3 ll4.
594 R ll3 ll4 ==>
595 (ll3 = ll4) \/
596 ?h t1 t2. (ll3 = h ::: t1) /\ (ll4 = h ::: t2) /\
597 R t1 t2
598Proof
599 REPEAT GEN_TAC THEN EQ_TAC THENL [
600 DISCH_THEN SUBST_ALL_TAC THEN Q.EXISTS_TAC `(=)` THEN SRW_TAC [][],
601 STRIP_TAC THEN ONCE_REWRITE_TAC [LLIST_BISIMULATION0] THEN
602 Q.EXISTS_TAC `\l1 l2. R l1 l2 \/ (l1 = l2)` THEN
603 SRW_TAC [][] THENL [
604 `(ll3 = ll4) \/
605 ?h t1 t2. (ll3 = h:::t1) /\ (ll4 = h:::t2) /\ R t1 t2`
606 by METIS_TAC [] THEN
607 Q.SPEC_THEN `ll3` FULL_STRUCT_CASES_TAC llist_CASES THEN
608 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][],
609 Q.SPEC_THEN `ll3` FULL_STRUCT_CASES_TAC llist_CASES THEN
610 SRW_TAC [][]
611 ]
612 ]
613QED
614
615(* ----------------------------------------------------------------------
616 LTAKE : num -> 'a llist -> 'a list option
617
618 returns the prefix of the given length, if the input list is at least
619 that long
620 ---------------------------------------------------------------------- *)
621
622Definition LTAKE[nocompute]:
623 (LTAKE 0 ll = SOME []) /\
624 (LTAKE (SUC n) ll =
625 case LHD ll of
626 NONE => NONE
627 | SOME hd =>
628 case LTAKE n (THE (LTL ll)) of
629 NONE => NONE
630 | SOME tl => SOME (hd::tl))
631End
632
633Theorem LTAKE_LUNFOLD:
634 (LTAKE 0 (LUNFOLD f x) = SOME []) /\
635 (LTAKE (SUC n) (LUNFOLD f x) =
636 case f x of NONE => NONE
637 | SOME (tx, hx) => OPTION_MAP (CONS hx) (LTAKE n (LUNFOLD f tx)))
638Proof
639 CONJ_TAC THEN REWRITE_TAC [LTAKE, LHD_LUNFOLD, LTL_LUNFOLD] THEN
640 Cases_on `f x` THEN
641 Ho_Rewrite.REWRITE_TAC [BETA_THM, THE_DEF,
642 OPTION_MAP_DEF, option_case_def, pair_CASE_def,
643 o_DEF, OPTION_MAP_CASE]
644QED
645
646Theorem LTAKE_THM[simp]:
647 (!l. LTAKE 0 l = SOME []) /\
648 (!n. LTAKE (SUC n) LNIL = NONE) /\
649 (!n h t. LTAKE (SUC n) (LCONS h t) = OPTION_MAP (CONS h) (LTAKE n t))
650Proof
651 SRW_TAC [][LTAKE, LHD_THM, LTL_THM] THEN REPEAT GEN_TAC THEN
652 Cases_on `LTAKE n t` THEN SRW_TAC [][]
653QED
654
655(* can also prove llist equality by proving all prefixes are the same *)
656Theorem LTAKE_SNOC_LNTH:
657 !n ll. LTAKE (SUC n) ll =
658 case LTAKE n ll of
659 NONE => NONE
660 | SOME l => (case LNTH n ll of
661 NONE => NONE
662 | SOME e => SOME (l ++ [e]))
663Proof
664 Induct THENL [
665 SRW_TAC [][LTAKE,LNTH],
666 GEN_TAC THEN
667 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [LTAKE])) THEN
668 Q.SPEC_THEN `ll` STRUCT_CASES_TAC llist_CASES THENL [
669 POP_ASSUM (K ALL_TAC) THEN SRW_TAC [][LHD_THM, LTAKE_THM],
670 SIMP_TAC (srw_ss()) [LHD_THM,LTL_THM,LTAKE_THM,LNTH_THM] THEN
671 SRW_TAC [][] THEN Cases_on `LTAKE n t` THENL [
672 SRW_TAC [][],
673 SRW_TAC [][] THEN Cases_on `LNTH n t` THEN SRW_TAC [][]
674 ]
675 ]
676 ]
677QED
678
679Theorem LTAKE_EQ_NONE_LNTH:
680 !n ll. (LTAKE n ll = NONE) ==> (LNTH n ll = NONE)
681Proof
682 Induct THEN ASM_SIMP_TAC (srw_ss()) [LTAKE,LNTH] THEN
683 Q.X_GEN_TAC `ll` THEN
684 Q.SPEC_THEN `ll` STRUCT_CASES_TAC llist_CASES THEN
685 ASM_SIMP_TAC (srw_ss()) [LHD_THM, LTL_THM] THEN
686 Cases_on `LTAKE n t` THEN SRW_TAC [][]
687QED
688
689Theorem LTAKE_NIL_EQ_SOME[simp]:
690 !l m. (LTAKE m LNIL = SOME l) <=> (m = 0) /\ (l = [])
691Proof
692 REPEAT GEN_TAC >> Cases_on `m` >> SIMP_TAC (srw_ss()) [LTAKE, LHD_THM] >>
693 PROVE_TAC []
694QED
695
696Theorem LTAKE_NIL_EQ_NONE[simp]:
697 !m. (LTAKE m LNIL = NONE) = (0 < m)
698Proof
699 GEN_TAC THEN Cases_on `m` THEN SIMP_TAC (srw_ss()) [LTAKE, LHD_THM]
700QED
701
702Theorem SNOC_11[local]:
703 !l1 l2 x y. (l1 ++ [x] = l2 ++ [y]) <=> (l1 = l2) /\ (x = y)
704Proof
705 SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM] THEN CONJ_TAC THEN
706 Induct THEN REPEAT GEN_TAC THEN SIMP_TAC (srw_ss()) [] THEN
707 Cases_on `l2` THEN SRW_TAC [][] THEN METIS_TAC []
708QED
709
710Theorem LTAKE_EQ:
711 !ll1 ll2. (ll1 = ll2) = (!n. LTAKE n ll1 = LTAKE n ll2)
712Proof
713 SRW_TAC [][EQ_IMP_THM] THEN
714 SRW_TAC [][LNTH_EQ] THEN
715 POP_ASSUM (Q.SPEC_THEN `SUC n` MP_TAC) THEN
716 SIMP_TAC (srw_ss())[LTAKE_SNOC_LNTH] THEN
717 Cases_on `LTAKE n ll1` THEN Cases_on `LTAKE n ll2` THEN
718 ASM_SIMP_TAC (srw_ss()) [] THENL [
719 METIS_TAC [LTAKE_EQ_NONE_LNTH],
720 Cases_on `LNTH n ll2` THEN SRW_TAC [][] THEN
721 METIS_TAC [LTAKE_EQ_NONE_LNTH],
722 Cases_on `LNTH n ll1` THEN SRW_TAC [][] THEN
723 METIS_TAC [LTAKE_EQ_NONE_LNTH],
724 Cases_on `LNTH n ll1` THEN Cases_on `LNTH n ll2` THEN
725 SRW_TAC [][SNOC_11]
726 ]
727QED
728
729(* more random facts about LTAKE *)
730Theorem LTAKE_CONS_EQ_NONE:
731 !m h t. (LTAKE m (LCONS h t) = NONE) =
732 (?n. (m = SUC n) /\ (LTAKE n t = NONE))
733Proof
734 GEN_TAC THEN Cases_on `m` THEN SIMP_TAC (srw_ss()) []
735QED
736
737Theorem LTAKE_CONS_EQ_SOME:
738 !m h t l.
739 (LTAKE m (LCONS h t) = SOME l) <=>
740 (m = 0) /\ (l = []) \/
741 ?n l'. (m = SUC n) /\ (LTAKE n t = SOME l') /\ (l = h::l')
742Proof
743 GEN_TAC THEN Cases_on `m` THEN
744 SIMP_TAC (srw_ss()) [] THEN PROVE_TAC []
745QED
746
747Theorem LTAKE_EQ_SOME_CONS:
748 !n l x. (LTAKE n l = SOME x) ==> !h. ?y. LTAKE n (LCONS h l) = SOME y
749Proof
750 Induct THEN SIMP_TAC (srw_ss()) [LTAKE, LHD_THM, LTL_THM] THEN
751 REPEAT GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `l` llist_CASES) THEN
752 SIMP_TAC (srw_ss()) [LHD_THM, LTL_THM] THEN
753 Cases_on `LTAKE n t` THEN SIMP_TAC (srw_ss()) [] THEN RES_TAC THEN
754 REPEAT STRIP_TAC THEN FIRST_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `h`) THEN
755 ASM_SIMP_TAC (srw_ss()) []
756QED
757
758(* ----------------------------------------------------------------------
759 Finality allows us to define MAP
760 ---------------------------------------------------------------------- *)
761
762val LMAP = new_specification
763("LMAP", ["LMAP"],
764 prove(
765 ``?LMAP. (!f. LMAP f LNIL = LNIL) /\
766 (!f h t. LMAP f (LCONS h t) = LCONS (f h) (LMAP f t))``,
767 ASSUME_TAC (GEN_ALL
768 (Q.ISPEC `\l. if l = LNIL then NONE
769 else SOME (THE (LTL l), f (THE (LHD l)))`
770 llist_Axiom_1)) THEN
771 POP_ASSUM (STRIP_ASSUME_TAC o CONV_RULE SKOLEM_CONV) THEN
772 Q.EXISTS_TAC `g` THEN
773 REPEAT STRIP_TAC THEN
774 POP_ASSUM (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [th]))) THEN
775 SRW_TAC [][LHD_THM, LTL_THM]));
776val _ = export_rewrites ["LMAP"]
777val _ = computeLib.add_persistent_funs ["LMAP"]
778
779(* and append *)
780
781val LAPPEND = new_specification
782 ("LAPPEND", ["LAPPEND"],
783 prove(
784 ``?LAPPEND. (!x. LAPPEND LNIL x = x) /\
785 (!h t x. LAPPEND (LCONS h t) x = LCONS h (LAPPEND t x))``,
786 STRIP_ASSUME_TAC
787 (Q.ISPEC `\(l1,l2).
788 if l1 = LNIL then
789 if l2 = LNIL then NONE
790 else SOME ((l1, THE (LTL l2)), THE (LHD l2))
791 else SOME ((THE (LTL l1), l2), THE (LHD l1))`
792 llist_Axiom) THEN
793 Q.EXISTS_TAC `\l1 l2. g (l1, l2)` THEN SIMP_TAC (srw_ss()) [] THEN
794 REPEAT STRIP_TAC THENL [
795 ONCE_REWRITE_TAC [LLIST_BISIMULATION] THEN
796 Q.EXISTS_TAC `\ll1 ll2. ll1 = g (LNIL, ll2)` THEN
797 SIMP_TAC (srw_ss()) [] THEN Q.X_GEN_TAC `x` THEN
798 STRUCT_CASES_TAC (Q.SPEC `x` llist_CASES) THENL [
799 DISJ1_TAC THEN
800 ASM_SIMP_TAC std_ss [GSYM LHD_EQ_NONE, LHD_THM],
801 SRW_TAC [][]
802 ],
803 SRW_TAC [][LHDTL_EQ_SOME]
804 ]));
805val _ = export_rewrites ["LAPPEND"]
806val _ = computeLib.add_persistent_funs ["LAPPEND"]
807
808(* NOTE: The last char is Latin Subscript Small Letter L (U+2097) *)
809val _ = set_mapped_fixity{fixity = Infixl 480, term_name = "LAPPEND",
810 tok = "++ₗ"};
811
812val _ = TeX_notation { hol = "LAPPEND",
813 TeX = ("\\HOLTokenDoublePlusL", 1) };
814
815(* properties of map and append *)
816
817Theorem LMAP_APPEND:
818 !f ll1 ll2.
819 LMAP f (LAPPEND ll1 ll2) = LAPPEND (LMAP f ll1) (LMAP f ll2)
820Proof
821 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC [LLIST_BISIMULATION0] THEN
822 Q.EXISTS_TAC `\ll1 ll2. ?x y. (ll1 = LMAP f (LAPPEND x y)) /\
823 (ll2 = LAPPEND (LMAP f x) (LMAP f y))` THEN
824 SRW_TAC [][] THENL [
825 PROVE_TAC [],
826 ALL_TAC
827 ] THEN
828 STRUCT_CASES_TAC (Q.SPEC `x` llist_CASES) THEN SRW_TAC [][] THENL [
829 STRUCT_CASES_TAC (Q.SPEC `y` llist_CASES) THEN
830 SRW_TAC [][] THEN
831 PROVE_TAC [LAPPEND, LMAP],
832 PROVE_TAC []
833 ]
834QED
835
836Theorem LAPPEND_EQ_LNIL[simp]:
837 (LAPPEND l1 l2 = [||]) <=> (l1 = [||]) /\ (l2 = [||])
838Proof SRW_TAC [][EQ_IMP_THM] THEN
839 Q.SPEC_THEN `l1` FULL_STRUCT_CASES_TAC llist_CASES THEN
840 FULL_SIMP_TAC (srw_ss()) []
841QED
842
843Theorem LAPPEND_ASSOC:
844 !ll1 ll2 ll3. LAPPEND (LAPPEND ll1 ll2) ll3 =
845 LAPPEND ll1 (LAPPEND ll2 ll3)
846Proof
847 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC [LLIST_STRONG_BISIMULATION] THEN
848 Q.EXISTS_TAC `\l1 l2. ?u. (l1 = LAPPEND (LAPPEND u ll2) ll3) /\
849 (l2 = LAPPEND u (LAPPEND ll2 ll3))` THEN
850 SRW_TAC [][] THENL [
851 PROVE_TAC [],
852 STRUCT_CASES_TAC (Q.SPEC `u` llist_CASES) THEN SRW_TAC [][] THEN
853 PROVE_TAC []
854 ]
855QED
856
857Theorem LMAP_MAP:
858 !(f:'a -> 'b) (g:'c -> 'a) (ll:'c llist).
859 LMAP f (LMAP g ll) = LMAP (f o g) ll
860Proof
861 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC [LLIST_BISIMULATION] THEN
862 Q.EXISTS_TAC `λll1 ll2. ?ll0. (ll1 = LMAP f (LMAP g ll0)) /\
863 (ll2 = LMAP (f o g) ll0)` THEN
864 SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THENL [
865 PROVE_TAC [],
866 STRIP_ALL_THEN SUBST_ALL_TAC
867 (Q.ISPEC `ll0:'c llist` llist_CASES) THEN
868 FULL_SIMP_TAC (srw_ss()) [LMAP, LTL_THM, LHD_THM] THEN
869 PROVE_TAC []
870 ]
871QED
872
873Theorem LAPPEND_NIL_2ND:
874 !ll. LAPPEND ll LNIL = ll
875Proof
876 GEN_TAC THEN ONCE_REWRITE_TAC [LLIST_BISIMULATION] THEN
877 Q.EXISTS_TAC `\ll1 ll2. ll1 = LAPPEND ll2 LNIL` THEN
878 SIMP_TAC (srw_ss()) [] THEN GEN_TAC THEN
879 STRUCT_CASES_TAC (Q.SPEC `ll4` llist_CASES) THEN
880 SIMP_TAC (srw_ss()) []
881QED
882
883Theorem LHD_LAPPEND:
884 LHD (LAPPEND l1 l2) = if l1 = LNIL then LHD l2 else LHD l1
885Proof
886 qspec_then`l1`FULL_STRUCT_CASES_TAC llist_CASES >> rw[]
887QED
888
889Theorem LTL_LAPPEND:
890 LTL (LAPPEND l1 l2) = if l1 = LNIL then LTL l2
891 else SOME (LAPPEND (THE (LTL l1)) l2)
892Proof
893 qspec_then`l1`FULL_STRUCT_CASES_TAC llist_CASES >> rw[]
894QED
895
896
897Theorem LTAKE_LAPPEND1:
898 !n l1 l2. IS_SOME (LTAKE n l1) ==> (LTAKE n (LAPPEND l1 l2) = LTAKE n l1)
899Proof
900 Induct >> rw[LTAKE_THM] >>
901 qspec_then`l1`FULL_STRUCT_CASES_TAC llist_CASES >> fs[] >>
902 Cases_on`LTAKE n t`>>fs[]
903QED
904
905Theorem LTAKE_LMAP:
906 !n f ll. LTAKE n (LMAP f ll) =
907 OPTION_MAP (MAP f) (LTAKE n ll)
908Proof
909 Induct_on `n` >> rw[] >>
910 qspec_then ‘ll’ strip_assume_tac llist_CASES >>
911 pop_assum SUBST_ALL_TAC >>
912 fs[OPTION_MAP_COMPOSE,o_DEF]
913QED
914
915(* ----------------------------------------------------------------------
916 finiteness and list length
917 ---------------------------------------------------------------------- *)
918
919val (LFINITE_rules,LFINITE_ind,LFINITE_cases) = Hol_reln`
920 LFINITE [||] /\
921 (!h t. LFINITE t ==> LFINITE (h:::t))
922`;
923
924Theorem LFINITE_THM[simp]:
925 (LFINITE LNIL = T) /\
926 (!h t. LFINITE (LCONS h t) = LFINITE t)
927Proof
928 REPEAT STRIP_TAC THEN
929 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [LFINITE_cases])) THEN
930 SRW_TAC [][]
931QED
932
933Theorem LFINITE:
934 LFINITE ll = ?n. LTAKE n ll = NONE
935Proof
936 EQ_TAC THENL [
937 Q.ID_SPEC_TAC `ll` THEN HO_MATCH_MP_TAC LFINITE_ind THEN
938 SRW_TAC [][] THEN Q.EXISTS_TAC `SUC n` THEN SRW_TAC [][],
939 Q_TAC SUFF_TAC `!n ll. (LTAKE n ll = NONE) ==> LFINITE ll` THEN1
940 METIS_TAC [] THEN
941 Induct THEN SRW_TAC [][] THEN
942 Q.SPEC_THEN `ll` FULL_STRUCT_CASES_TAC llist_CASES THEN
943 FULL_SIMP_TAC (srw_ss()) []
944 ]
945QED
946
947val (llength_rel_rules,llength_rel_ind,llength_rel_cases) = Hol_reln`
948 llength_rel [||] 0 /\
949 (!h n t. llength_rel t n ==> llength_rel (h:::t) (SUC n))
950`;
951
952Theorem llength_lfinite[local]:
953 !t n. llength_rel t n ==> LFINITE t
954Proof
955 HO_MATCH_MP_TAC llength_rel_ind THEN SRW_TAC [][]
956QED
957Theorem lfinite_llength[local]:
958 !t. LFINITE t ==> ?n. llength_rel t n
959Proof
960 HO_MATCH_MP_TAC LFINITE_ind THEN SRW_TAC [][] THEN
961 METIS_TAC [llength_rel_rules]
962QED
963
964Theorem llength_unique[local]:
965 !t m n. llength_rel t n /\ llength_rel t m ==> (m = n)
966Proof
967 Q_TAC SUFF_TAC `!t n. llength_rel t n ==> !m. llength_rel t m ==> (m = n)`
968 THEN1 METIS_TAC [] THEN
969 HO_MATCH_MP_TAC llength_rel_ind THEN SRW_TAC [][] THEN
970 POP_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE [llength_rel_cases]) THEN
971 FULL_SIMP_TAC (srw_ss()) []
972QED
973
974Theorem llength_rel_nil[local]:
975 llength_rel [||] n = (n = 0)
976Proof
977 ONCE_REWRITE_TAC [llength_rel_cases] THEN SRW_TAC [][]
978QED
979val _ = augment_srw_ss [rewrites [llength_rel_nil]]
980
981Definition LLENGTH[nocompute]:
982 LLENGTH ll = if LFINITE ll then SOME (@n. llength_rel ll n) else NONE
983End
984
985Theorem LLENGTH_THM[simp]:
986 (LLENGTH LNIL = SOME 0) /\
987 (!h t. LLENGTH (LCONS h t) = OPTION_MAP SUC (LLENGTH t))
988Proof
989 SRW_TAC [][LLENGTH] THEN
990 `?n. llength_rel t n` by METIS_TAC [lfinite_llength] THEN
991 `!m. llength_rel t m = (m = n)` by METIS_TAC [llength_unique] THEN
992 SRW_TAC [][] THEN
993 ONCE_REWRITE_TAC [llength_rel_cases] THEN SRW_TAC [][]
994QED
995
996Theorem LLENGTH_0[simp]:
997 (LLENGTH x = SOME 0) <=> (x = [||])
998Proof
999 llist_CASE_TAC ``x : 'a llist`` THEN
1000 SIMP_TAC bool_ss [LLENGTH_THM, LCONS_NOT_NIL] THEN
1001 Cases_on `LLENGTH t` THEN
1002 SIMP_TAC std_ss [OPTION_MAP_DEF, NOT_SUC]
1003QED
1004
1005Theorem LFINITE_HAS_LENGTH:
1006 !ll. LFINITE ll ==> ?n. LLENGTH ll = SOME n
1007Proof
1008 SRW_TAC [][LLENGTH]
1009QED
1010
1011Theorem NOT_LFINITE_NO_LENGTH:
1012 !ll. ~LFINITE ll ==> (LLENGTH ll = NONE)
1013Proof
1014 SIMP_TAC (srw_ss()) [LLENGTH]
1015QED
1016
1017Theorem LFINITE_LLENGTH:
1018 LFINITE ll <=> ?n. LLENGTH ll = SOME n
1019Proof
1020 rw[EQ_IMP_THM,LFINITE_HAS_LENGTH] >>
1021 spose_not_then strip_assume_tac >>
1022 imp_res_tac NOT_LFINITE_NO_LENGTH >>
1023 fs[]
1024QED
1025
1026Theorem LFINITE_INDUCTION =
1027 CONV_RULE (RENAME_VARS_CONV ["P"]) LFINITE_ind;
1028
1029Theorem LFINITE_STRONG_INDUCTION =
1030 SIMP_RULE (srw_ss()) [LFINITE_THM]
1031 (Q.SPEC `\ll. LFINITE ll /\ P ll` LFINITE_INDUCTION)
1032
1033Theorem LFINITE_MAP[simp]:
1034 !f (ll:'a llist). LFINITE (LMAP f ll) = LFINITE ll
1035Proof
1036 REPEAT GEN_TAC THEN EQ_TAC THENL [
1037 Q_TAC SUFF_TAC `!ll1. LFINITE ll1 ==>
1038 !ll. (ll1 = LMAP f ll) ==> LFINITE ll`
1039 THEN1 SRW_TAC [][] THEN
1040 HO_MATCH_MP_TAC LFINITE_INDUCTION THEN REPEAT STRIP_TAC THEN
1041 STRIP_ALL_THEN SUBST_ALL_TAC (Q.SPEC `ll` llist_CASES) THEN
1042 FULL_SIMP_TAC (srw_ss()) [LMAP, LFINITE_THM],
1043 Q.ID_SPEC_TAC `ll` THEN HO_MATCH_MP_TAC LFINITE_INDUCTION THEN
1044 SIMP_TAC (srw_ss()) [LFINITE_THM, LMAP]
1045 ]
1046QED
1047
1048Theorem LFINITE_APPEND[simp]:
1049 !ll1 ll2. LFINITE (LAPPEND ll1 ll2) <=> LFINITE ll1 /\ LFINITE ll2
1050Proof
1051 REPEAT GEN_TAC THEN EQ_TAC THENL [
1052 Q_TAC SUFF_TAC `!ll0. LFINITE ll0 ==>
1053 !ll1 ll2. (LAPPEND ll1 ll2 = ll0) ==>
1054 LFINITE ll1 /\ LFINITE ll2`
1055 THEN1 PROVE_TAC [] THEN
1056 HO_MATCH_MP_TAC LFINITE_STRONG_INDUCTION THEN REPEAT STRIP_TAC THEN
1057 STRIP_ALL_THEN SUBST_ALL_TAC (Q.SPEC `ll1` llist_CASES) THEN
1058 FULL_SIMP_TAC (srw_ss()) [LFINITE_THM, LAPPEND] THEN
1059 PROVE_TAC [],
1060 REWRITE_TAC [GSYM AND_IMP_INTRO] THEN
1061 Q.ID_SPEC_TAC `ll1` THEN
1062 HO_MATCH_MP_TAC LFINITE_STRONG_INDUCTION THEN
1063 SIMP_TAC (srw_ss()) [LFINITE_THM, LAPPEND]
1064 ]
1065QED
1066
1067Theorem LTAKE_LNTH_EL:
1068 !n ll m l.
1069 (LTAKE n ll = SOME l) /\
1070 m < n
1071 ==>
1072 (LNTH m ll = SOME (EL m l))
1073Proof
1074 Induct>>simp[]>>
1075 (* "Cases" *)
1076 (fn (g as(_,w)) => (gen_tac >>
1077 FULL_STRUCT_CASES_TAC(ISPEC(#1(dest_forall w))llist_CASES))g) >>
1078 simp[PULL_EXISTS] >> Cases>>simp[]
1079QED
1080
1081Theorem NOT_LFINITE_APPEND:
1082 !ll1 ll2. ~LFINITE ll1 ==> (LAPPEND ll1 ll2 = ll1)
1083Proof
1084 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC [LLIST_BISIMULATION] THEN
1085 Q.EXISTS_TAC `\ll1 ll2. ~LFINITE ll2 /\ ?ll3. ll1 = LAPPEND ll2 ll3` THEN
1086 ASM_SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THENL [
1087 PROVE_TAC [],
1088 STRIP_ALL_THEN SUBST_ALL_TAC (Q.SPEC `ll4` llist_CASES) THEN
1089 FULL_SIMP_TAC (srw_ss()) [LFINITE_THM, LAPPEND, LHD_THM, LTL_THM] THEN
1090 PROVE_TAC []
1091 ]
1092QED
1093
1094Theorem LFINITE_LAPPEND_IMP_NIL:
1095 !ll. LFINITE ll ==> !l2. (LAPPEND ll l2 = ll) ==> (l2 = [||])
1096Proof
1097 ho_match_mp_tac LFINITE_INDUCTION >> simp[]
1098QED
1099
1100Theorem LLENGTH_MAP:
1101 !ll f. LLENGTH (LMAP f ll) = LLENGTH ll
1102Proof
1103 REPEAT GEN_TAC THEN Cases_on `LFINITE ll` THENL [
1104 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `ll` THEN
1105 HO_MATCH_MP_TAC LFINITE_STRONG_INDUCTION THEN
1106 SIMP_TAC (srw_ss()) [LLENGTH_THM, LMAP],
1107 PROVE_TAC [NOT_LFINITE_NO_LENGTH, LFINITE_MAP]
1108 ]
1109QED
1110
1111Theorem LLENGTH_APPEND:
1112 !ll1 ll2.
1113 LLENGTH (LAPPEND ll1 ll2) =
1114 if LFINITE ll1 /\ LFINITE ll2 then
1115 SOME (THE (LLENGTH ll1) + THE (LLENGTH ll2))
1116 else
1117 NONE
1118Proof
1119 REPEAT GEN_TAC THEN
1120 Cases_on `LFINITE (LAPPEND ll1 ll2)` THENL [
1121 POP_ASSUM (fn th => `LFINITE ll1 /\ LFINITE ll2` by
1122 PROVE_TAC [th, LFINITE_APPEND]) THEN
1123 ASM_SIMP_TAC (srw_ss()) [] THEN
1124 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `ll2` THEN
1125 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `ll1` THEN
1126 HO_MATCH_MP_TAC LFINITE_STRONG_INDUCTION THEN
1127 SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THEN
1128 IMP_RES_TAC LFINITE_HAS_LENGTH THEN
1129 ASM_SIMP_TAC (srw_ss()) [ADD_CLAUSES],
1130 `LLENGTH (LAPPEND ll1 ll2) = NONE`
1131 by PROVE_TAC [NOT_LFINITE_NO_LENGTH] THEN
1132 FULL_SIMP_TAC (srw_ss()) []
1133 ]
1134QED
1135
1136(* ----------------------------------------------------------------------
1137 mapping in and out of ordinary (finite) lists
1138 ---------------------------------------------------------------------- *)
1139
1140Definition toList[nocompute]:
1141 toList ll = if LFINITE ll then LTAKE (THE (LLENGTH ll)) ll else NONE
1142End
1143
1144Theorem toList_THM:
1145 (toList LNIL = SOME []) /\
1146 (!h t. toList (LCONS h t) = OPTION_MAP (CONS h) (toList t))
1147Proof
1148 SIMP_TAC (srw_ss()) [toList, LFINITE_THM, LLENGTH_THM, LTAKE_THM] THEN
1149 REPEAT GEN_TAC THEN COND_CASES_TAC THEN SIMP_TAC (srw_ss()) [] THEN
1150 IMP_RES_TAC LFINITE_HAS_LENGTH THEN
1151 ASM_SIMP_TAC (srw_ss()) [LTAKE_THM, LHD_THM, LTL_THM]
1152QED
1153
1154Definition fromList_def[simp]:
1155 (fromList [] = LNIL) /\ (fromList (h::t) = LCONS h (fromList t))
1156End
1157
1158Theorem fromList_EQ_LNIL[simp]:
1159 (fromList l = LNIL) <=> (l = [])
1160Proof
1161 Cases_on `l` >> simp[]
1162QED
1163
1164Theorem LHD_fromList:
1165 LHD (fromList l) = if NULL l then NONE else SOME (HD l)
1166Proof
1167 Cases_on `l` >> simp[]
1168QED
1169
1170Theorem LTL_fromList:
1171 LTL (fromList l) = if NULL l then NONE else SOME (fromList (TL l))
1172Proof
1173 Cases_on `l` >> simp[]
1174QED
1175
1176Theorem LFINITE_fromList[simp] :
1177 !l. LFINITE (fromList l)
1178Proof
1179 Induct THEN ASM_SIMP_TAC (srw_ss()) []
1180QED
1181
1182Theorem LLENGTH_fromList[simp]:
1183 !l. LLENGTH (fromList l) = SOME (LENGTH l)
1184Proof
1185 Induct THEN ASM_SIMP_TAC (srw_ss()) []
1186QED
1187
1188Theorem LTAKE_fromList:
1189 !l. LTAKE (LENGTH l) (fromList l) = SOME l
1190Proof
1191 Induct THEN ASM_SIMP_TAC (srw_ss()) []
1192QED
1193
1194Theorem from_toList:
1195 !l. toList (fromList l) = SOME l
1196Proof
1197 Induct THEN ASM_SIMP_TAC (srw_ss()) [toList_THM]
1198QED
1199
1200Theorem LFINITE_toList:
1201 !ll. LFINITE ll ==> ?l. toList ll = SOME l
1202Proof
1203 HO_MATCH_MP_TAC LFINITE_STRONG_INDUCTION THEN
1204 REPEAT STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [toList_THM]
1205QED
1206
1207Theorem LFINITE_toList_SOME:
1208 LFINITE ll <=> IS_SOME (toList ll)
1209Proof
1210 EQ_TAC >> simp[IS_SOME_EXISTS,LFINITE_toList] >>
1211 rw[] >> fs[toList]
1212QED
1213
1214Theorem to_fromList:
1215 !ll. LFINITE ll ==> (fromList (THE (toList ll)) = ll)
1216Proof
1217 HO_MATCH_MP_TAC LFINITE_STRONG_INDUCTION THEN
1218 SIMP_TAC (srw_ss()) [toList_THM] THEN REPEAT STRIP_TAC THEN
1219 IMP_RES_TAC LFINITE_toList THEN FULL_SIMP_TAC (srw_ss()) []
1220QED
1221
1222Theorem LTAKE_LAPPEND2:
1223 !n l1 l2.
1224 LTAKE n l1 = NONE ==>
1225 LTAKE n (LAPPEND l1 l2) =
1226 OPTION_MAP (APPEND (THE(toList l1))) (LTAKE (n - THE(LLENGTH l1)) l2)
1227Proof
1228 rpt gen_tac >> strip_tac >>
1229 `LFINITE l1` by metis_tac[LFINITE] >>
1230 qpat_x_assum`_ = _`mp_tac >>
1231 map_every qid_spec_tac[`l2`,`n`] >>
1232 pop_assum mp_tac >>
1233 qid_spec_tac`l1` >>
1234 ho_match_mp_tac LFINITE_INDUCTION >>
1235 rw[toList_THM] >- (
1236 Cases_on`LTAKE n l2`>>simp[] ) >>
1237 Cases_on`n`>>fs[] >>
1238 simp[OPTION_MAP_COMPOSE] >>
1239 `LFINITE l1` by metis_tac[LFINITE] >>
1240 imp_res_tac LFINITE_toList >> simp[] >>
1241 imp_res_tac LFINITE_HAS_LENGTH >> simp[] >>
1242 rpt (AP_THM_TAC ORELSE AP_TERM_TAC) >> simp[FUN_EQ_THM]
1243QED
1244
1245Theorem LNTH_fromList:
1246 LNTH n (fromList l) = if n < LENGTH l then SOME (EL n l) else NONE
1247Proof
1248 ‘!l. LFINITE l ==>
1249 !n. LNTH n l = if n < THE(LLENGTH l) then SOME (EL n (THE(toList l)))
1250 else NONE’
1251 by (Induct_on ‘LFINITE’ >> rw[] >>
1252 imp_res_tac LFINITE_HAS_LENGTH >> simp[] >>
1253 Cases_on`n`>>simp[toList_THM] >- (
1254 imp_res_tac LFINITE_toList >> simp[] ) >>
1255 rw[] >>
1256 imp_res_tac LFINITE_toList >> simp[] ) >>
1257 metis_tac[LFINITE_fromList,LLENGTH_fromList,THE_DEF,LFINITE_toList,
1258 from_toList]
1259QED
1260
1261Theorem lnth_fromList_some:
1262 !n l. n < LENGTH l <=> (LNTH n (fromList l) = SOME (EL n l))
1263Proof
1264 Induct_on `l` >> rw [] >>
1265 Cases_on `n` >> rw [LNTH_THM] >> fs []
1266QED
1267
1268(* ----------------------------------------------------------------------
1269 LDROP : num -> 'a llist -> 'a llist option
1270
1271 drops a prefix of given length, if there are that many items to be
1272 dropped
1273 ---------------------------------------------------------------------- *)
1274
1275Definition LDROP[nocompute]:
1276 (LDROP 0 ll = SOME ll) /\
1277 (LDROP (SUC n) ll = OPTION_JOIN (OPTION_MAP (LDROP n) (LTL ll)))
1278End
1279
1280Theorem FUNPOW_BIND_NONE[local]:
1281 !n. FUNPOW (\m. OPTION_BIND m g) n NONE = NONE
1282Proof
1283 Induct THEN ASM_SIMP_TAC bool_ss [FUNPOW, OPTION_BIND_def]
1284QED
1285
1286Theorem LDROP_FUNPOW:
1287 !n ll. LDROP n ll = FUNPOW (\m. OPTION_BIND m LTL) n (SOME ll)
1288Proof
1289 Induct THEN RULE_ASSUM_TAC GSYM THEN
1290 SIMP_TAC std_ss [LDROP, FUNPOW, FUNPOW_BIND_NONE] THEN
1291 GEN_TAC THEN Cases_on `LTL ll` THEN
1292 ASM_SIMP_TAC std_ss [FUNPOW_BIND_NONE]
1293QED
1294
1295Theorem LDROP_THM[simp]:
1296 (!ll. LDROP 0 ll = SOME ll) /\
1297 (!n. LDROP (SUC n) LNIL = NONE) /\
1298 (!n h t. LDROP (SUC n) (LCONS h t) = LDROP n t)
1299Proof
1300 SIMP_TAC (srw_ss()) [LDROP, LTL_THM]
1301QED
1302
1303Theorem LDROP1_THM:
1304 LDROP 1 = LTL
1305Proof
1306 SIMP_TAC bool_ss [DECIDE ``1 = SUC 0``,
1307 LDROP_FUNPOW, FUN_EQ_THM, FUNPOW, OPTION_BIND_def]
1308QED
1309
1310Theorem LNTH_HD_LDROP:
1311 !n ll. LNTH n ll = OPTION_BIND (LDROP n ll) LHD
1312Proof
1313 REWRITE_TAC [LDROP_FUNPOW] THEN
1314 Induct THEN RULE_ASSUM_TAC GSYM THEN
1315 SIMP_TAC std_ss [LNTH, FUNPOW, FUNPOW_BIND_NONE] THEN
1316 GEN_TAC THEN Cases_on `LTL ll` THEN
1317 ASM_SIMP_TAC std_ss [FUNPOW_BIND_NONE]
1318QED
1319
1320Theorem NOT_LFINITE_TAKE:
1321 !ll. ~LFINITE ll ==> !n. ?y. LTAKE n ll = SOME y
1322Proof
1323 SIMP_TAC (srw_ss()) [LFINITE] THEN REPEAT STRIP_TAC THEN
1324 POP_ASSUM (ASSUME_TAC o Q.SPEC `n`) THEN
1325 Cases_on `LTAKE n ll` THEN FULL_SIMP_TAC (srw_ss()) []
1326QED
1327
1328Theorem LFINITE_TAKE:
1329 !n ll. LFINITE ll /\ n <= THE (LLENGTH ll) ==>
1330 ?y. LTAKE n ll = SOME y
1331Proof
1332 Induct THEN SIMP_TAC (srw_ss()) [LTAKE_THM] THEN GEN_TAC THEN
1333 STRUCT_CASES_TAC (Q.SPEC `ll` llist_CASES) THEN
1334 SIMP_TAC (srw_ss()) [] THEN
1335 REPEAT STRIP_TAC THEN IMP_RES_TAC LFINITE_HAS_LENGTH THEN
1336 FULL_SIMP_TAC (srw_ss()) [] THEN
1337 `?z. LTAKE n t = SOME z` by ASM_SIMP_TAC (srw_ss()) [] THEN
1338 ASM_SIMP_TAC (srw_ss()) []
1339QED
1340
1341Theorem NOT_LFINITE_DROP:
1342 !ll. ~LFINITE ll ==> !n. ?y. LDROP n ll = SOME y
1343Proof
1344 CONV_TAC (BINDER_CONV RIGHT_IMP_FORALL_CONV THENC
1345 SWAP_VARS_CONV) THEN
1346 Induct THEN SIMP_TAC (srw_ss()) [LDROP] THEN GEN_TAC THEN
1347 STRUCT_CASES_TAC (Q.SPEC `ll` llist_CASES) THEN
1348 ASM_SIMP_TAC (srw_ss()) []
1349QED
1350
1351Theorem LFINITE_DROP:
1352 !n ll. LFINITE ll /\ n <= THE (LLENGTH ll) ==>
1353 ?y. LDROP n ll = SOME y
1354Proof
1355 Induct THEN SIMP_TAC (srw_ss()) [LDROP_THM] THEN GEN_TAC THEN
1356 STRUCT_CASES_TAC (Q.SPEC `ll` llist_CASES) THEN
1357 SIMP_TAC (srw_ss()) [LLENGTH_THM, LFINITE_THM, LDROP_THM] THEN
1358 REPEAT STRIP_TAC THEN IMP_RES_TAC LFINITE_HAS_LENGTH THEN
1359 FULL_SIMP_TAC (srw_ss()) []
1360QED
1361
1362Theorem option_case_NONE[local]:
1363 !f x y. (option_CASE x NONE f = SOME y) =
1364 (?z. (x = SOME z) /\ (f z = SOME y))
1365Proof
1366 REPEAT GEN_TAC THEN Cases_on `x` THEN SIMP_TAC (srw_ss()) []
1367QED
1368
1369Theorem LTAKE_DROP:
1370 (!n ll:'a llist.
1371 ~LFINITE ll ==>
1372 (LAPPEND (fromList (THE (LTAKE n ll))) (THE (LDROP n ll)) = ll)) /\
1373 (!n ll:'a llist.
1374 LFINITE ll /\ n <= THE (LLENGTH ll) ==>
1375 (LAPPEND (fromList (THE (LTAKE n ll))) (THE (LDROP n ll)) = ll))
1376Proof
1377 CONJ_TAC THEN Induct THEN SRW_TAC [][] THENL [
1378 Q.SPEC_THEN `ll` FULL_STRUCT_CASES_TAC llist_CASES THEN
1379 FULL_SIMP_TAC (srw_ss()) [] THEN
1380 IMP_RES_TAC NOT_LFINITE_TAKE THEN
1381 POP_ASSUM (Q.X_CHOOSE_THEN `y` ASSUME_TAC o Q.SPEC `n`) THEN
1382 ASM_SIMP_TAC (srw_ss()) [] THEN
1383 Q_TAC SUFF_TAC `y = THE (LTAKE n t)` THEN1 METIS_TAC [] THEN
1384 ASM_SIMP_TAC (srw_ss()) [],
1385 Q.SPEC_THEN `ll` FULL_STRUCT_CASES_TAC llist_CASES THEN
1386 FULL_SIMP_TAC (srw_ss()) [] THEN
1387 IMP_RES_TAC LFINITE_HAS_LENGTH THEN
1388 FULL_SIMP_TAC (srw_ss()) [] THEN
1389 `?z. LTAKE n t = SOME z` by ASM_SIMP_TAC (srw_ss()) [LFINITE_TAKE] THEN
1390 FULL_SIMP_TAC (srw_ss()) [] THEN
1391 `z = THE (LTAKE n t)` by ASM_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][]
1392 ]
1393QED
1394
1395Theorem LDROP_ADD:
1396 !k1 k2 x.
1397 LDROP (k1 + k2) x = case LDROP k1 x of
1398 | NONE => NONE
1399 | SOME ll => LDROP k2 ll
1400Proof
1401 ONCE_REWRITE_TAC [ADD_COMM] THEN
1402 REWRITE_TAC [LDROP_FUNPOW, FUNPOW_ADD] THEN
1403 REPEAT GEN_TAC THEN CASE_TAC THEN
1404 REWRITE_TAC [FUNPOW_BIND_NONE]
1405QED
1406
1407Theorem LDROP_SOME_LLENGTH:
1408 (LDROP n ll = SOME l) /\ (LLENGTH ll = SOME m) ==>
1409 n <= m /\ (LLENGTH l = SOME (m - n))
1410Proof
1411 `!ll. LFINITE ll ==>
1412 !n m l.
1413 (LDROP n ll = SOME l) /\ (LLENGTH ll = SOME m) ==>
1414 n <= m /\ (LLENGTH l = SOME (m - n))`
1415 suffices_by (
1416 ntac 2 strip_tac >>
1417 first_assum (match_mp_tac o MP_CANON) >>
1418 qexists_tac`ll`>>simp[] >>
1419 metis_tac[NOT_LFINITE_NO_LENGTH,NOT_NONE_SOME] ) >>
1420 ho_match_mp_tac LFINITE_INDUCTION >>
1421 strip_tac >- ( Cases >> simp[] ) >>
1422 ntac 3 strip_tac >> Cases >> simp[PULL_EXISTS]
1423QED
1424
1425Theorem LFINITE_LNTH_NONE:
1426 LFINITE ll <=> ?n. LNTH n ll = NONE
1427Proof
1428 EQ_TAC >- (
1429 qid_spec_tac`ll` >>
1430 ho_match_mp_tac LFINITE_INDUCTION >>
1431 rw[] >> qexists_tac`SUC n` >> simp[] ) >>
1432 metis_tac[NOT_LFINITE_TAKE,LTAKE_LNTH_EL,
1433 NOT_SOME_NONE,
1434 LESS_SUC_REFL]
1435QED
1436
1437Theorem infinite_lnth_some:
1438 !ll. ~LFINITE ll <=> !n. ?x. LNTH n ll = SOME x
1439Proof
1440 rw [LFINITE_LNTH_NONE] >>
1441 metis_tac [NOT_SOME_NONE, option_nchotomy]
1442QED
1443
1444Theorem LNTH_LAPPEND:
1445 LNTH n (LAPPEND l1 l2) =
1446 case LLENGTH l1 of NONE => LNTH n l1
1447 | SOME m => if n < m then LNTH n l1 else LNTH (n-m) l2
1448Proof
1449 Cases_on`LFINITE l1` >- (
1450 map_every qid_spec_tac[`l2`,`n`] >>
1451 pop_assum mp_tac >> qid_spec_tac`l1` >>
1452 ho_match_mp_tac LFINITE_STRONG_INDUCTION >> rw[] >>
1453 imp_res_tac LFINITE_HAS_LENGTH >> fs[] >>
1454 Cases_on`n`>>fs[] ) >>
1455 CASE_TAC >>
1456 fs[LFINITE_LLENGTH] >>
1457 `!n. ?x. LNTH n l1 = SOME x` by (
1458 metis_tac[LFINITE_LNTH_NONE,LFINITE_LLENGTH,
1459 option_CASES,NOT_SOME_NONE] ) >>
1460 Cases_on`LTAKE (SUC n) l1` >- (
1461 metis_tac[NOT_SOME_NONE,LTAKE_EQ_NONE_LNTH] ) >>
1462 qspecl_then[`SUC n`,`l1`,`l2`]mp_tac LTAKE_LAPPEND1 >>
1463 simp[] >> strip_tac >>
1464 imp_res_tac LTAKE_LNTH_EL >>
1465 rpt(pop_assum(qspec_then`n`mp_tac)) >> simp[]
1466QED
1467
1468Theorem LNTH_ADD:
1469 !a b ll. LNTH (a + b) ll = OPTION_BIND (LDROP a ll) (LNTH b)
1470Proof
1471 Induct >> simp[] >> rpt gen_tac >>
1472 `b + SUC a = SUC (a + b)` by simp[] >>
1473 pop_assum SUBST1_TAC >>
1474 qspec_then`ll`FULL_STRUCT_CASES_TAC llist_CASES >>
1475 simp[]
1476QED
1477
1478Theorem lnth_some_down_closed:
1479 !ll x n1 n2.
1480 (LNTH n1 ll = SOME x) /\ n2 <= n1
1481 ==>
1482 ?y. (LNTH n2 ll = SOME y)
1483Proof
1484 Induct_on `n1` >> rw [] >>
1485 Q.ISPEC_THEN`ll`FULL_STRUCT_CASES_TAC llist_CASES >>
1486 fs [] >> Cases_on `n2` >> fs []
1487QED
1488
1489(* ----------------------------------------------------------------------
1490 exists : ('a -> bool) -> 'a llist -> bool
1491
1492 defined inductively
1493 ---------------------------------------------------------------------- *)
1494
1495Inductive exists:
1496 (!h t. P h ==> exists P (h ::: t)) /\
1497 (!h t. exists P t ==> exists P (h ::: t))
1498End
1499
1500Theorem exists_thm[simp]:
1501 (exists P [||] = F) /\
1502 (exists P (h:::t) <=> P h \/ exists P t)
1503Proof
1504 CONJ_TAC THEN
1505 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [exists_cases])) THEN
1506 SRW_TAC [][]
1507QED
1508
1509Theorem exists_LNTH:
1510 !l. exists P l = ?n e. (SOME e = LNTH n l) /\ P e
1511Proof
1512 SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM] THEN CONJ_TAC THENL [
1513 HO_MATCH_MP_TAC exists_ind THEN SRW_TAC [][] THENL [
1514 MAP_EVERY Q.EXISTS_TAC [`0`, `h`] THEN SRW_TAC [][],
1515 MAP_EVERY Q.EXISTS_TAC [`SUC n`, `e`] THEN SRW_TAC [][]
1516 ],
1517 Q_TAC SUFF_TAC `!n l e. (SOME e = LNTH n l) /\ P e ==> exists P l`
1518 THEN1 METIS_TAC [] THEN
1519 Induct THEN REPEAT GEN_TAC THEN
1520 Q.SPEC_THEN `l` STRUCT_CASES_TAC llist_CASES THEN
1521 SRW_TAC [][] THEN METIS_TAC []
1522 ]
1523QED
1524
1525Theorem MONO_exists:
1526 (!x. P x ==> Q x) ==> (exists P l ==> exists Q l)
1527Proof
1528 STRIP_TAC THEN Q.ID_SPEC_TAC `l` THEN HO_MATCH_MP_TAC exists_ind THEN
1529 SRW_TAC [][]
1530QED
1531val _ = IndDefLib.export_mono "MONO_exists"
1532
1533Theorem exists_strong_ind =
1534 exists_ind |> Q.SPECL [`P`, `\ll. Q ll /\ exists P ll`]
1535 |> SIMP_RULE (srw_ss()) []
1536 |> Q.GEN `Q` |> Q.GEN `P`;
1537
1538Theorem exists_LDROP:
1539 exists P ll <=> ?n a t. (LDROP n ll = SOME (a:::t)) /\ P a
1540Proof
1541 EQ_TAC THENL [
1542 Q_TAC SUFF_TAC
1543 `!ll. exists P ll ==> ?n a t. (LDROP n ll = SOME (a:::t)) /\ P a`
1544 THEN1 METIS_TAC [] THEN
1545 HO_MATCH_MP_TAC exists_strong_ind THEN SRW_TAC [][] THENL [
1546 Q.EXISTS_TAC `0` THEN SRW_TAC [][],
1547 Q.EXISTS_TAC `SUC n` THEN SRW_TAC [][]
1548 ],
1549 Q_TAC SUFF_TAC
1550 `!n ll a t. (LDROP n ll = SOME (a:::t)) /\ P a ==> exists P ll`
1551 THEN1 METIS_TAC [] THEN
1552 Induct THEN SRW_TAC [][] THEN
1553 Q.SPEC_THEN `ll` FULL_STRUCT_CASES_TAC llist_CASES THEN
1554 FULL_SIMP_TAC (srw_ss()) [LDROP]
1555 ]
1556QED
1557
1558Theorem exists_thm_strong:
1559 exists P ll <=> ?n a t l. LDROP n ll = SOME (a:::t) /\ P a /\
1560 LTAKE n ll = SOME l /\ EVERY ($~ o P) l
1561Proof
1562 simp[exists_LDROP,EQ_IMP_THM] >>
1563 reverse conj_tac >- metis_tac[] >>
1564 simp[LEAST_EXISTS, SimpL “$==>”] >> strip_tac >>
1565 goal_assum drule >>
1566 rw[] >>
1567 rpt(pop_assum mp_tac) >>
1568 rename1`LDROP n ll = SOME (a:::t)`>>
1569 MAP_EVERY qid_spec_tac [`a`,`t`,`ll`,`n`] >>
1570 Induct >- rw[] >>
1571 gen_tac >>
1572 qspec_then`ll`FULL_STRUCT_CASES_TAC llist_CASES>>
1573 rw[] >>
1574 rename1`LDROP _ (h:::_)`>>
1575 `~P h`
1576 by(first_x_assum(qspec_then `0` mp_tac) >>
1577 impl_tac >- simp[] >>
1578 rename1`h:::t`>>
1579 disch_then(qspecl_then [`h`,`t`] mp_tac) >> simp[]) >>
1580 first_x_assum (drule_then drule) >>
1581 impl_tac
1582 >- (rw[] >> rename1`n' < n` >> first_x_assum(qspec_then `SUC n'` mp_tac) >>
1583 rw[]) >>
1584 rw[PULL_EXISTS]
1585QED
1586
1587(* ----------------------------------------------------------------------
1588 companion LL_ALL/every (has a coinduction principle)
1589 ---------------------------------------------------------------------- *)
1590
1591Definition every_def: every P ll = ~exists ((~) o P) ll
1592End
1593Overload LL_ALL = ``every``
1594Overload every = ``every``
1595
1596Theorem every_coind:
1597 !P Q.
1598 (!h t. Q (h:::t) ==> P h /\ Q t) ==>
1599 !ll. Q ll ==> every P ll
1600Proof
1601 SIMP_TAC (srw_ss()) [every_def] THEN
1602 REPEAT GEN_TAC THEN STRIP_TAC THEN
1603 Q_TAC SUFF_TAC `!ll. exists ($~ o P) ll ==> ~Q ll` THEN1 METIS_TAC [] THEN
1604 HO_MATCH_MP_TAC exists_ind THEN
1605 SRW_TAC [][DECIDE ``(~p ==> ~q) = (q ==> p)``] THEN METIS_TAC []
1606QED
1607
1608Theorem every_thm[simp]:
1609 (every P [||] = T) /\
1610 (every P (h:::t) <=> P h /\ every P t)
1611Proof SRW_TAC [][every_def]
1612QED
1613Theorem LL_ALL_THM = every_thm
1614
1615Theorem MONO_every:
1616 (!x. P x ==> Q x) ==> (every P l ==> every Q l)
1617Proof
1618 STRIP_TAC THEN Q.ID_SPEC_TAC `l` THEN HO_MATCH_MP_TAC every_coind THEN
1619 SRW_TAC [][]
1620QED
1621val _ = export_mono "MONO_every"
1622
1623Theorem every_strong_coind =
1624 every_coind |> Q.SPECL [`P`, `\ll. Q ll \/ every P ll`]
1625 |> SIMP_RULE (srw_ss()) [DISJ_IMP_THM, IMP_CONJ_THM,
1626 FORALL_AND_THM]
1627 |> Q.GEN `Q` |> Q.GEN `P`;
1628
1629Theorem every_LNTH:
1630 !P ll. every P ll <=> !n e. LNTH n ll = SOME e ==> P e
1631Proof
1632 fs [every_def,exists_LNTH] \\
1633 CONV_TAC(STRIP_QUANT_CONV(LAND_CONV(PURE_ONCE_REWRITE_CONV[EQ_SYM_EQ]))) \\
1634 simp[IMP_DISJ_THM]
1635QED
1636
1637Theorem every_LDROP:
1638 !f i ll1 ll2.
1639 every f ll1 /\
1640 LDROP i ll1 = SOME ll2
1641 ==> every f ll2
1642Proof
1643 Induct_on ‘i’ >> rpt GEN_TAC >>
1644 qspec_then ‘ll1’ strip_assume_tac llist_CASES >> pop_assum SUBST_ALL_TAC >>
1645 rw[] >> rw[] >> res_tac
1646QED
1647
1648(*
1649 could alternatively take contrapositives of the exists induction principle:
1650
1651 exists_strong_ind |> Q.SPECL [`(~) o P`, `(~) o Q`]
1652 |> CONV_RULE (BINOP_CONV (ONCE_REWRITE_CONV [MONO_NOT_EQ]))
1653 |> SIMP_RULE (srw_ss()) [GSYM every_def]
1654*)
1655
1656(* ----------------------------------------------------------------------
1657 can now define LFILTER and LFLATTEN
1658 ---------------------------------------------------------------------- *)
1659
1660Theorem least_lemma[local]:
1661 (?n. P n) ==> ((LEAST) P = if P 0 then 0 else SUC ((LEAST) (P o SUC)))
1662Proof
1663 SRW_TAC [][] THENL [
1664 Q_TAC SUFF_TAC `(\n. n = 0) ($LEAST P)` THEN1 SRW_TAC [][] THEN
1665 MATCH_MP_TAC LEAST_ELIM THEN SRW_TAC [][] THENL [
1666 PROVE_TAC [],
1667 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
1668 `0 < n'` by DECIDE_TAC THEN METIS_TAC []
1669 ],
1670 Q_TAC SUFF_TAC `(\n. n = SUC ($LEAST (P o SUC))) ((LEAST) P)` THEN1
1671 SRW_TAC [][] THEN
1672 MATCH_MP_TAC LEAST_ELIM THEN CONJ_TAC THENL [
1673 PROVE_TAC [],
1674 Q.X_GEN_TAC `p` THEN SRW_TAC [][] THEN
1675 Q_TAC SUFF_TAC `(\k. p = SUC k) ($LEAST (P o SUC))` THEN1
1676 SRW_TAC [][] THEN
1677 MATCH_MP_TAC LEAST_ELIM THEN CONJ_TAC THENL [
1678 SRW_TAC [][] THEN Cases_on `n` THEN PROVE_TAC [],
1679 SRW_TAC [][] THEN
1680 `~(SUC n' < p)` by PROVE_TAC [] THEN
1681 `(p = SUC n') \/ (p < SUC n')` by DECIDE_TAC THEN
1682 `?p0. p = SUC p0` by METIS_TAC [num_CASES] THEN
1683 FULL_SIMP_TAC (srw_ss()) []
1684 ]
1685 ]
1686 ]
1687QED
1688
1689val LFILTER = new_specification
1690 ("LFILTER", ["LFILTER"],
1691 prove(
1692 ``?LFILTER.
1693 !P ll. LFILTER P ll = if ~ exists P ll then LNIL
1694 else
1695 if P (THE (LHD ll)) then
1696 LCONS (THE (LHD ll))
1697 (LFILTER P (THE (LTL ll)))
1698 else
1699 LFILTER P (THE (LTL ll))``,
1700 ASSUME_TAC (GEN_ALL
1701 (Q.ISPEC `\ll. if exists P ll then
1702 let n = LEAST n. ?e. (SOME e = LNTH n ll) /\ P e in
1703 SOME (THE (LDROP (SUC n) ll),
1704 THE (LNTH n ll))
1705 else NONE` llist_Axiom_1)) THEN
1706 POP_ASSUM (STRIP_ASSUME_TAC o CONV_RULE SKOLEM_CONV) THEN
1707 Q.EXISTS_TAC `g` THEN REPEAT GEN_TAC THEN
1708 POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `P`) THEN
1709 Cases_on `exists P ll` THENL [
1710 POP_ASSUM MP_TAC THEN
1711 POP_ASSUM
1712 (fn th => CONV_TAC
1713 (RAND_CONV (LAND_CONV (ONCE_REWRITE_CONV [th]))) THEN
1714 ASSUME_TAC (GSYM th)) THEN
1715 SIMP_TAC (srw_ss()) [] THEN
1716 SRW_TAC [][] THEN
1717 `?h t. ll = h:::t` by METIS_TAC [llist_CASES, exists_thm] THENL [
1718 Q.PAT_X_ASSUM `exists P ll` (K ALL_TAC) THEN
1719 POP_ASSUM SUBST_ALL_TAC THEN
1720 FULL_SIMP_TAC (srw_ss()) [] THEN
1721 Q_TAC SUFF_TAC `n = 0` THEN1 SRW_TAC [][] THEN
1722 CONV_TAC (UNBETA_CONV ``n:num``) THEN UNABBREV_ALL_TAC THEN
1723 MATCH_MP_TAC LEAST_ELIM THEN SRW_TAC [][] THENL [
1724 Q.EXISTS_TAC `0` THEN SRW_TAC [][],
1725 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
1726 `0 < n` by DECIDE_TAC THEN
1727 METIS_TAC [SOME_11, LNTH_THM]
1728 ],
1729 FULL_SIMP_TAC (srw_ss()) [] THEN FULL_SIMP_TAC (srw_ss()) [] THEN
1730 `n = SUC (LEAST m. ?e. (SOME e = LNTH m t) /\ P e)`
1731 by (Q.UNABBREV_TAC `n` THEN
1732 Q.HO_MATCH_ABBREV_TAC `(LEAST) Q1 = SUC ((LEAST) Q2)` THEN
1733 `Q2 = Q1 o SUC`
1734 by (UNABBREV_ALL_TAC THEN SRW_TAC [][FUN_EQ_THM]) THEN
1735 POP_ASSUM SUBST1_TAC THEN
1736 Q.MATCH_ABBREV_TAC `LHS = RHS` THEN
1737 Q.UNABBREV_TAC `LHS` THEN
1738 `RHS = if Q1 0 then 0 else RHS` by SRW_TAC [][Abbr`Q1`] THEN
1739 POP_ASSUM SUBST1_TAC THEN
1740 Q.UNABBREV_TAC `RHS` THEN
1741 MATCH_MP_TAC least_lemma THEN
1742 UNABBREV_ALL_TAC THEN
1743 SRW_TAC [][] THEN
1744 `?m e. (SOME e = LNTH m t) /\ P e`
1745 by METIS_TAC [exists_LNTH] THEN
1746 MAP_EVERY Q.EXISTS_TAC [`SUC m`, `e`] THEN
1747 SRW_TAC [][]) THEN
1748 RM_ALL_ABBREVS_TAC THEN SRW_TAC [][] THEN
1749 FIRST_X_ASSUM
1750 ((fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [GSYM th]))) o
1751 assert (is_forall o concl)) THEN
1752 SRW_TAC [][] THEN SRW_TAC [][Abbr`n`]
1753 ],
1754 POP_ASSUM MP_TAC THEN
1755 POP_ASSUM
1756 (fn th => CONV_TAC
1757 (RAND_CONV (LAND_CONV (ONCE_REWRITE_CONV [th])))) THEN
1758 SRW_TAC [][]
1759 ]));
1760
1761Theorem LFILTER_THM[simp]:
1762 (!P. LFILTER P LNIL = LNIL) /\
1763 (!P h t. LFILTER P (LCONS h t) = if P h then LCONS h (LFILTER P t)
1764 else LFILTER P t)
1765Proof
1766 REPEAT STRIP_TAC THEN CONV_TAC (LHS_CONV (REWR_CONV LFILTER)) THEN
1767 SIMP_TAC (srw_ss()) [] THEN
1768 Cases_on `P h` THEN ASM_SIMP_TAC (srw_ss()) [] THEN
1769 Cases_on `exists P t` THEN ASM_SIMP_TAC (srw_ss()) [] THEN
1770 ONCE_REWRITE_TAC [LFILTER] THEN ASM_SIMP_TAC (srw_ss()) []
1771QED
1772
1773Theorem LFILTER_NIL:
1774 !P ll. LL_ALL ($~ o P) ll ==> (LFILTER P ll = LNIL)
1775Proof
1776 ONCE_REWRITE_TAC [LFILTER, every_def] THEN
1777 `!P. $~ o $~ o P = P` by (GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN
1778 SIMP_TAC (srw_ss()) []) THEN
1779 ASM_SIMP_TAC (srw_ss()) []
1780QED
1781
1782Theorem LFILTER_EQ_NIL:
1783 !ll. (LFILTER P ll = LNIL) = every ((~) o P) ll
1784Proof
1785 SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM, LFILTER_NIL] THEN
1786 HO_MATCH_MP_TAC every_coind THEN
1787 SRW_TAC [][]
1788QED
1789
1790Theorem LFILTER_APPEND:
1791 !P ll1 ll2. LFINITE ll1 ==>
1792 (LFILTER P (LAPPEND ll1 ll2) =
1793 LAPPEND (LFILTER P ll1) (LFILTER P ll2))
1794Proof
1795 REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `ll1` THEN
1796 HO_MATCH_MP_TAC LFINITE_STRONG_INDUCTION THEN
1797 SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THEN
1798 COND_CASES_TAC THEN ASM_SIMP_TAC (srw_ss()) []
1799QED
1800
1801Theorem LFILTER_fromList[simp]:
1802 !p l. LFILTER p (fromList l) = fromList (FILTER p l)
1803Proof
1804 Induct_on ‘l’ \\ rw[]
1805QED
1806
1807Theorem LFILTER_EQ_CONS:
1808 LFILTER P ll = h:::t
1809 ==> ?l ll'. ll = LAPPEND (fromList l) (h:::ll') /\
1810 EVERY ($~ o P) l /\ P h /\
1811 LFILTER P ll' = t
1812Proof
1813 strip_tac >>
1814 rename1‘LFILTER P ll’>>
1815 ‘exists P ll’ by(fs[Once LFILTER,CaseEq "bool"]) >>
1816 fs[exists_thm_strong] >>
1817 rename1‘LDROP n ll = SOME (a:::t')’>>
1818 rename1‘LTAKE n ll = SOME l’>>
1819 ‘ll = LAPPEND (fromList l) (a:::t')’
1820 by(reverse(Cases_on ‘LFINITE ll’)
1821 >- (drule_then
1822 (qspec_then ‘n’ (fn thm => PURE_ONCE_REWRITE_TAC[GSYM thm]))
1823 (CONJUNCT1 LTAKE_DROP) >>
1824 simp[]) >>
1825 ‘n <= THE(LLENGTH ll)’
1826 by(fs[LFINITE_LLENGTH] >> metis_tac[LDROP_SOME_LLENGTH]) >>
1827 drule_all_then (fn thm => PURE_ONCE_REWRITE_TAC[GSYM thm])
1828 (cj 2 LTAKE_DROP) >>
1829 simp[]) >>
1830 VAR_EQ_TAC >>
1831 fs[LFINITE_fromList,LFILTER_APPEND,LFILTER_fromList] >>
1832 ‘FILTER P l = []’ by(fs[FILTER_EQ_NIL,o_DEF]) >>
1833 fs[] >> rpt(VAR_EQ_TAC) >>
1834 metis_tac[]
1835QED
1836
1837Theorem every_LFILTER:
1838 !ll P. every P (LFILTER P ll)
1839Proof
1840 rpt strip_tac >>
1841 rename1`every P (LFILTER P ll)`>>
1842 `!ll. (?ll'. ll = LFILTER P ll') ==> every P ll
1843 ` by(ho_match_mp_tac every_coind >>
1844 rw[] >> first_x_assum(ASSUME_TAC o GSYM) >>
1845 drule_then strip_assume_tac LFILTER_EQ_CONS >>
1846 fs[] >> metis_tac[]) >>
1847 metis_tac[]
1848QED
1849
1850Theorem every_LAPPEND1:
1851 !P ll1 ll2. every P (LAPPEND ll1 ll2) ==> every P ll1
1852Proof
1853 strip_tac
1854 >> fs[Once (GSYM PULL_EXISTS)]
1855 >> ho_match_mp_tac every_coind
1856 >> rw[PULL_EXISTS]
1857 >> goal_assum drule
1858QED
1859
1860Theorem every_fromList_EVERY:
1861 !l P. every P (fromList l) = EVERY P l
1862Proof
1863 Induct >> rw[]
1864QED
1865
1866Theorem every_LAPPEND2_LFINITE:
1867 !l P ll. LFINITE l /\ every P (LAPPEND l ll) ==> every P ll
1868Proof
1869 Ho_Rewrite.REWRITE_TAC[GSYM PULL_FORALL,GSYM AND_IMP_INTRO]
1870 >> ho_match_mp_tac LFINITE_ind
1871 >> fs[]
1872QED
1873
1874Theorem every_LFILTER_imp:
1875 !Q P ll. every Q ll ==> every Q (LFILTER P ll)
1876Proof
1877 rpt strip_tac >>
1878 rename1`every Q (LFILTER P ll)`
1879 >> `!ll. (?ll'. ll = LFILTER P ll' /\ every Q ll') ==> every Q ll` by (
1880 ho_match_mp_tac every_coind
1881 >> rw[] >> qpat_x_assum `_:::_ = _`(ASSUME_TAC o GSYM)
1882 >> drule_then strip_assume_tac LFILTER_EQ_CONS
1883 >> VAR_EQ_TAC
1884 >> rename1 `LAPPEND (fromList l) (h:::llll)`
1885 >> qspec_then `l` assume_tac LFINITE_fromList
1886 >> VAR_EQ_TAC
1887 >> drule_all every_LAPPEND2_LFINITE
1888 >> rw[every_thm,AC CONJ_ASSOC CONJ_COMM]
1889 >> goal_assum drule
1890 >> REFL_TAC
1891 )
1892 >> metis_tac[]
1893QED
1894
1895val LFLATTEN = new_specification
1896 ("LFLATTEN", ["LFLATTEN"],
1897 prove(
1898 ``?LFLATTEN.
1899 !ll. LFLATTEN (ll:'a llist llist) =
1900 if LL_ALL ($= LNIL) ll then LNIL
1901 else
1902 if THE (LHD ll) = LNIL then
1903 LFLATTEN (THE (LTL ll))
1904 else
1905 LCONS (THE (LHD (THE (LHD ll))))
1906 (LFLATTEN (LCONS (THE (LTL (THE (LHD ll))))
1907 (THE (LTL ll))))``,
1908 ASSUME_TAC (
1909 Q.ISPEC `\ll. if LL_ALL ($= LNIL) ll then NONE
1910 else
1911 let n = LEAST n. ?e. (SOME e = LNTH n ll) /\ ~(e = [||])
1912 in
1913 let nlist = THE (LNTH n ll)
1914 in
1915 SOME(LCONS (THE (LTL nlist))
1916 (THE (LDROP (SUC n) ll)),
1917 THE (LHD nlist))` llist_Axiom) THEN
1918 POP_ASSUM (Q.X_CHOOSE_THEN `g` STRIP_ASSUME_TAC) THEN
1919 Q.EXISTS_TAC `g` THEN GEN_TAC THEN
1920 Cases_on `LL_ALL ($= LNIL) ll` THEN ASM_SIMP_TAC (srw_ss()) [] THENL [
1921 `LTL (g ll) = NONE` by ASM_SIMP_TAC std_ss [] THEN
1922 FULL_SIMP_TAC (srw_ss()) [],
1923 ALL_TAC
1924 ] THEN
1925 `?h t. ll = LCONS h t` by METIS_TAC [llist_CASES,every_thm] THEN
1926 POP_ASSUM SUBST_ALL_TAC THEN
1927 SIMP_TAC (srw_ss()) [] THEN
1928 Cases_on `h = LNIL` THEN ASM_SIMP_TAC (srw_ss()) [] THENL [
1929 FULL_SIMP_TAC (srw_ss()) [LL_ALL_THM] THEN
1930 REPEAT (FIRST_X_ASSUM (fn th =>
1931 MP_TAC (Q.SPEC `LCONS LNIL t` th) THEN
1932 MP_TAC (Q.SPEC `t` th))) THEN
1933 ASM_SIMP_TAC (srw_ss()) [LL_ALL_THM] THEN
1934 `?n e. (SOME e = LNTH n t) /\ ~(e = [||])`
1935 by (FULL_SIMP_TAC (srw_ss()) [every_def, exists_LNTH] THEN
1936 METIS_TAC []) THEN
1937 `(LEAST n. ?e. (SOME e = LNTH n ([||]:::t)) /\ ~(e = [||])) =
1938 SUC (LEAST n. ?e. (SOME e = LNTH n t) /\ ~(e = [||]))`
1939 by (Q.MATCH_ABBREV_TAC `(LEAST) Q1 = SUC ((LEAST) Q2)` THEN
1940 `Q2 = Q1 o SUC` by SRW_TAC [][Abbr`Q1`, Abbr`Q2`, FUN_EQ_THM] THEN
1941 POP_ASSUM SUBST1_TAC THEN Q.UNABBREV_TAC `Q2` THEN
1942 Q.MATCH_ABBREV_TAC `(LEAST)Q1 = RHS` THEN
1943 `RHS = if Q1 0 then 0 else RHS` by SRW_TAC [][Abbr`Q1`] THEN
1944 POP_ASSUM SUBST1_TAC THEN Q.UNABBREV_TAC `RHS` THEN
1945 MATCH_MP_TAC least_lemma THEN
1946 Q.UNABBREV_TAC `Q1` THEN
1947 Q.EXISTS_TAC `SUC n` THEN SRW_TAC [][] THEN METIS_TAC []) THEN
1948 POP_ASSUM SUBST_ALL_TAC THEN SRW_TAC [][LET_THM] THEN
1949 `?h1 t1. g t = h1 ::: t1`
1950 by METIS_TAC [LHD_EQ_NONE, llist_CASES,
1951 NOT_SOME_NONE] THEN
1952 POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN
1953 SRW_TAC [][LHDTL_EQ_SOME],
1954
1955 (* ~(h = LNIL) *)
1956 FULL_SIMP_TAC (srw_ss()) [LL_ALL_THM] THEN
1957 ASM_SIMP_TAC (srw_ss()) [LHDTL_EQ_SOME] THEN
1958 Q.SUBGOAL_THEN
1959 `(LEAST n. ?e. (SOME e = LNTH n (h:::t)) /\ ~(e = [||])) = 0`
1960 SUBST_ALL_TAC THENL [
1961 SRW_TAC [][LEAST_DEF] THEN
1962 ONCE_REWRITE_TAC [WHILE] THEN SRW_TAC [][],
1963 ALL_TAC
1964 ] THEN SRW_TAC [][LET_THM]
1965 ]));
1966
1967Theorem LFLATTEN_THM[simp]:
1968 (LFLATTEN LNIL = LNIL) /\
1969 (!tl. LFLATTEN (LCONS LNIL t) = LFLATTEN t) /\
1970 (!h t tl. LFLATTEN (LCONS (LCONS h t) tl) =
1971 LCONS h (LFLATTEN (LCONS t tl)))
1972Proof
1973 REPEAT STRIP_TAC THEN CONV_TAC (LHS_CONV (REWR_CONV LFLATTEN)) THEN
1974 SIMP_TAC (srw_ss()) [LL_ALL_THM, LHD_THM, LTL_THM] THEN
1975 COND_CASES_TAC THEN SIMP_TAC (srw_ss()) [] THEN
1976 ONCE_REWRITE_TAC [LFLATTEN] THEN ASM_SIMP_TAC (srw_ss()) []
1977QED
1978
1979Theorem LFLATTEN_APPEND[simp]:
1980 !h t. LFLATTEN (LCONS h t) = LAPPEND h (LFLATTEN t)
1981Proof
1982 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC [LLIST_STRONG_BISIMULATION] THEN
1983 Q.EXISTS_TAC `\ll1 ll2. ?h t. (ll1 = LFLATTEN (LCONS h t)) /\
1984 (ll2 = LAPPEND h (LFLATTEN t))` THEN
1985 SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THENL [
1986 PROVE_TAC [],
1987 Cases_on `h = LNIL` THENL [
1988 SRW_TAC [][],
1989
1990 (* ~(h = LNIL) *)
1991 POP_ASSUM (fn th =>
1992 `?h0 t0. h = LCONS h0 t0` by PROVE_TAC [llist_CASES, th]) THEN
1993 SRW_TAC [][] THEN PROVE_TAC []
1994 ]
1995 ]
1996QED
1997
1998
1999Theorem LFLATTEN_EQ_NIL:
2000 !ll. (LFLATTEN ll = LNIL) = LL_ALL ($= LNIL) ll
2001Proof
2002 GEN_TAC THEN EQ_TAC THENL [
2003 Q.ID_SPEC_TAC `ll` THEN
2004 HO_MATCH_MP_TAC every_coind THEN
2005 SRW_TAC [][],
2006 ONCE_REWRITE_TAC [LFLATTEN] THEN SIMP_TAC (srw_ss()) []
2007 ]
2008QED
2009
2010Theorem LFLATTEN_SINGLETON:
2011 !h. LFLATTEN (LCONS h LNIL) = h
2012Proof
2013 GEN_TAC THEN ONCE_REWRITE_TAC [LLIST_BISIMULATION] THEN
2014 Q.EXISTS_TAC `\ll1 ll2. ll1 = LFLATTEN (LCONS ll2 LNIL)` THEN
2015 SIMP_TAC (srw_ss()) [] THEN GEN_TAC THEN
2016 STRUCT_CASES_TAC (Q.SPEC `ll4` llist_CASES) THEN
2017 SIMP_TAC (srw_ss()) [LFLATTEN_THM, LHD_THM, LTL_THM]
2018QED
2019
2020Theorem LFINITE_LFLATTEN_EQN:
2021 !lll:'a llist llist.
2022 every (\ll. LFINITE ll /\ ll <> LNIL) lll ==>
2023 LFINITE (LFLATTEN lll) = LFINITE lll
2024Proof
2025 ‘!lll.
2026 LFINITE lll ==> llist$every (\ll. LFINITE ll /\ ll <> LNIL) lll ==>
2027 LFINITE (LFLATTEN lll)’
2028 by (ho_match_mp_tac LFINITE_ind \\ fs [])
2029 \\ qsuff_tac ‘!x.
2030 LFINITE x ==>
2031 !lll.
2032 x = LFLATTEN lll /\ llist$every (\ll. LFINITE ll /\ ll <> LNIL) lll ==>
2033 LFINITE lll’ THEN1 (metis_tac [])
2034 \\ ho_match_mp_tac LFINITE_ind
2035 \\ fs [PULL_FORALL] \\ rw []
2036 THEN1 (qspec_then‘lll’FULL_STRUCT_CASES_TAC llist_CASES \\ fs [])
2037 \\ rename [‘_ = LFLATTEN lll2’]
2038 \\ qspec_then‘lll2’FULL_STRUCT_CASES_TAC llist_CASES \\ fs []
2039 \\ rename [‘h2 <> _’]
2040 \\ qspec_then‘h2’FULL_STRUCT_CASES_TAC llist_CASES \\ fs [] \\ rw []
2041 \\ rename [‘LAPPEND t2’]
2042 \\ qspec_then‘t2’FULL_STRUCT_CASES_TAC llist_CASES \\ fs []
2043 \\ rename [‘LAPPEND t1’]
2044 \\ first_x_assum (qspec_then ‘(h:::t1) ::: t’ mp_tac) \\ fs []
2045QED
2046
2047(*---------------------------------------------------------------------------*)
2048(* ZIP two streams together, returning LNIL as soon as possible. *)
2049(* *)
2050(* LZIP_THM *)
2051(* |- (!l2. LZIP LNIL l2 = LNIL) /\ *)
2052(* (!l1. LZIP l1 LNIL = LNIL) /\ *)
2053(* (!h1 h2 t1 t2. *)
2054(* LZIP (LCONS h1 t1) (LCONS h2 t2) = LCONS (h1,h2) (LZIP t1 t2)) *)
2055(* *)
2056(*---------------------------------------------------------------------------*)
2057
2058val LZIP_THM = new_specification
2059 ("LZIP_THM", ["LZIP"],
2060 Q.prove
2061 (`?LZIP:'a llist # 'b llist -> ('a#'b) llist.
2062 (!l1. LZIP (l1,[||]) = [||]) /\
2063 (!l2. LZIP ([||],l2) = [||]) /\
2064 (!h1 h2 t1 t2. LZIP (h1:::t1, h2:::t2) = (h1,h2) ::: LZIP (t1,t2))`,
2065 let val ax =
2066 ISPEC
2067 ``λ(l1,l2).
2068 if (l1:'a llist = LNIL) \/ (l2:'b llist = LNIL)
2069 then NONE
2070 else SOME ((THE(LTL l1),THE(LTL l2)),
2071 (THE(LHD l1),THE(LHD l2)))``
2072 llist_Axiom_1
2073 in
2074 STRIP_ASSUME_TAC (SIMP_RULE (srw_ss()) [FORALL_PROD] ax)
2075 THEN Q.EXISTS_TAC `g`
2076 THEN REPEAT CONJ_TAC THENL
2077 [ONCE_ASM_REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC)
2078 THEN RW_TAC (srw_ss()) [],
2079 ONCE_ASM_REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC)
2080 THEN RW_TAC (srw_ss()) [],
2081 REPEAT GEN_TAC THEN
2082 POP_ASSUM (fn th => GEN_REWRITE_TAC LHS_CONV bool_rewrites [th])
2083 THEN RW_TAC (srw_ss()) [LTL_THM,LHD_THM]]
2084 end));
2085val _ = export_rewrites ["LZIP_THM"]
2086
2087
2088(*---------------------------------------------------------------------------*)
2089(* LUNZIP_THM *)
2090(* |- (LUNZIP [||] = ([||],[||])) /\ *)
2091(* !x y t. LUNZIP ((x,y):::t) = *)
2092(* let (ll1,ll2) = LUNZIP t in (x:::ll1,y:::ll2) *)
2093(*---------------------------------------------------------------------------*)
2094
2095Theorem LUNZIP_exists[local]:
2096 ?LUNZIP. (LUNZIP [||] = ([||]:'a llist, [||]:'b llist)) /\
2097 (!x y t. LUNZIP ((x:'a, y:'b):::t) =
2098 let (ll1, ll2) = LUNZIP t in (x:::ll1, y:::ll2))
2099Proof
2100 qspec_then ‘λll. if (LHD ll = NONE) then NONE
2101 else SOME (THE (LTL ll), SND (THE (LHD ll)))’
2102 strip_assume_tac llist_Axiom_1 >>
2103 qspec_then ‘λll. if (LHD ll = NONE) then NONE
2104 else SOME (THE (LTL ll), FST (THE (LHD ll)))’
2105 strip_assume_tac llist_Axiom_1 >>
2106 Q.EXISTS_TAC ‘λll. (g' ll, g ll)’ THEN SIMP_TAC list_ss [] THEN
2107 REPEAT STRIP_TAC THENL [
2108 POP_ASSUM (ASSUME_TAC o Q.SPEC `[||]`) THEN
2109 FULL_SIMP_TAC list_ss [LHD_THM],
2110 POP_ASSUM (K ALL_TAC) THEN POP_ASSUM (ASSUME_TAC o Q.SPEC `[||]`) THEN
2111 FULL_SIMP_TAC list_ss [LHD_THM],
2112 NTAC 2 (POP_ASSUM (MP_TAC o Q.SPEC ‘(x,y):::t’)) THEN
2113 RW_TAC list_ss [LHD_THM, LTL_THM, LET_THM]
2114 ]
2115QED
2116val LUNZIP_THM = new_specification ("LUNZIP_THM", ["LUNZIP"], LUNZIP_exists);
2117val _ = export_rewrites ["LUNZIP_THM"]
2118
2119Theorem LZIP_LUNZIP[simp]:
2120 !ll: ('a # 'b) llist. LZIP(LUNZIP ll) = ll
2121Proof
2122 REWRITE_TAC [Once LLIST_STRONG_BISIMULATION] THEN
2123 GEN_TAC THEN
2124 Q.EXISTS_TAC `λl1 l2. l1 = LZIP (LUNZIP l2)` THEN
2125 SRW_TAC [][] THEN
2126 Q.ISPEC_THEN `ll4` STRUCT_CASES_TAC llist_CASES THEN
2127 SRW_TAC [][] THEN
2128 Cases_on `h` THEN SRW_TAC [][] THEN SRW_TAC [][]
2129QED
2130
2131Theorem LUNFOLD_THM:
2132 !f x v1 v2.
2133 ((f x = NONE) ==> (LUNFOLD f x = [||])) /\
2134 ((f x = SOME (v1,v2)) ==> (LUNFOLD f x = v2:::LUNFOLD f v1))
2135Proof
2136 SRW_TAC [] [] THEN1
2137 SRW_TAC [] [Once LUNFOLD] THEN
2138 SRW_TAC [] [Once LUNFOLD]
2139QED
2140
2141Theorem LLIST_EQ:
2142 !f g.
2143 (!x. ((f x = [||]) /\ (g x = [||])) \/
2144 (?h y. (f x = h:::f y) /\ (g x = h:::g y)))
2145 ==>
2146 (!x. f x = g x)
2147Proof
2148 SRW_TAC [] [] THEN
2149 SRW_TAC [] [Once LLIST_BISIMULATION0] THEN
2150 Q.EXISTS_TAC `λll1 ll2. ?x. (ll1 = f x) /\ (ll2 = g x)` THEN
2151 SRW_TAC [] [] THEN
2152 METIS_TAC []
2153QED
2154
2155Theorem LUNFOLD_EQ:
2156 !R f s ll.
2157 R s ll /\
2158 (!s ll.
2159 R s ll
2160 ==>
2161 ((f s = NONE) /\ (ll = [||])) \/
2162 ?s' x ll'.
2163 (f s = SOME (s',x)) /\ (LHD ll = SOME x) /\ (LTL ll = SOME ll') /\
2164 R s' ll')
2165 ==>
2166 (LUNFOLD f s = ll)
2167Proof
2168 SRW_TAC [] [] THEN
2169 SRW_TAC [] [Once LLIST_BISIMULATION] THEN
2170 Q.EXISTS_TAC `λll1 ll2. ?s. (ll1 = LUNFOLD f s) /\ R s ll2` THEN
2171 SRW_TAC [] [] THEN1
2172 METIS_TAC [] THEN
2173 RES_TAC THEN
2174 SRW_TAC [] [LUNFOLD_THM] THEN
2175 IMP_RES_TAC LUNFOLD_THM THEN
2176 SRW_TAC [] [] THEN
2177 METIS_TAC []
2178QED
2179
2180Theorem LMAP_LUNFOLD:
2181 !f g s.
2182 LMAP f (LUNFOLD g s) = LUNFOLD (λs. OPTION_MAP (λ(x, y). (x, f y)) (g s)) s
2183Proof
2184 SRW_TAC [] [] THEN
2185 MATCH_MP_TAC (GSYM LUNFOLD_EQ) THEN
2186 SRW_TAC [] [] THEN
2187 Q.EXISTS_TAC `\s ll. ll = LMAP f (LUNFOLD g s)` THEN
2188 SRW_TAC [] [] THEN
2189 Cases_on `g s` THEN
2190 SRW_TAC [] [LUNFOLD_THM] THEN
2191 Cases_on `x` THEN
2192 IMP_RES_TAC LUNFOLD_THM THEN
2193 SRW_TAC [] []
2194QED
2195
2196Theorem LNTH_LDROP:
2197 !n l x. (LNTH n l = SOME x) ==> (LHD (THE (LDROP n l)) = SOME x)
2198Proof
2199 Induct THEN
2200 SRW_TAC [] [LNTH, LDROP] THEN
2201 Cases_on `LTL l` THEN
2202 SRW_TAC [] [] THEN
2203 FULL_SIMP_TAC (srw_ss()) []
2204QED
2205
2206Theorem LAPPEND_fromList:
2207 !l1 l2. LAPPEND (fromList l1) (fromList l2) = fromList (l1 ++ l2)
2208Proof
2209 Induct THEN
2210 SRW_TAC [] []
2211QED
2212
2213Theorem LFLATTEN_fromList: !l.
2214 LFLATTEN(fromList(MAP fromList l)) = fromList(FLAT l)
2215Proof
2216 Induct >> rw[LAPPEND_fromList]
2217QED
2218
2219Theorem LTAKE_LENGTH:
2220 !n ll l. (LTAKE n ll = SOME l) ==> (n = LENGTH l)
2221Proof
2222Induct THEN
2223SRW_TAC [] [] THEN
2224SRW_TAC [] [] THEN
2225`(ll = [||]) \/ ?h t. ll = h:::t` by METIS_TAC [llist_CASES] THEN
2226SRW_TAC [] [] THEN
2227FULL_SIMP_TAC (srw_ss()) [] THEN
2228METIS_TAC []
2229QED
2230
2231Theorem LTAKE_TAKE_LESS:
2232 (LTAKE n ll = SOME l) /\ m <= n ==>
2233 (LTAKE m ll = SOME (TAKE m l))
2234Proof
2235 rw[] >> Cases_on`n=m`>>fs[] >>
2236 imp_res_tac LTAKE_LENGTH >> rw[] >>
2237 Cases_on`LTAKE m ll` >- (
2238 imp_res_tac LTAKE_EQ_NONE_LNTH >>
2239 `m < LENGTH l` by fsrw_tac[ARITH_ss][] >>
2240 imp_res_tac LTAKE_LNTH_EL >> fs[] ) >>
2241 imp_res_tac LTAKE_LENGTH >> simp[] >>
2242 simp[LIST_EQ_REWRITE,EL_TAKE] >> rw[] >>
2243 qmatch_assum_rename_tac`n < LENGTH x` >>
2244 `n < LENGTH l` by decide_tac >>
2245 imp_res_tac LTAKE_LNTH_EL >> fs[]
2246QED
2247
2248Theorem LTAKE_LLENGTH_NONE:
2249 (LLENGTH ll = SOME n) /\ n < m ==> (LTAKE m ll = NONE)
2250Proof
2251 rw[] >> `LFINITE ll` by metis_tac[LFINITE_LLENGTH] >>
2252 `!ll. LFINITE ll ==> !m n. (LLENGTH ll = SOME n) /\ n < m
2253 ==> (LTAKE m ll = NONE)` suffices_by metis_tac[] >>
2254 rpt (pop_assum kall_tac) >>
2255 ho_match_mp_tac LFINITE_INDUCTION >> rw[] >>
2256 simp[LTAKE_CONS_EQ_NONE] >>
2257 Cases_on`m`>>fs[]
2258QED
2259
2260Theorem LTAKE_LLENGTH_SOME:
2261 LLENGTH ll = SOME n ==> ?l. LTAKE n ll = SOME l /\ toList ll = SOME l
2262Proof metis_tac[LFINITE_LLENGTH,to_fromList,from_toList,THE_DEF,toList]
2263QED
2264
2265Theorem toList_LAPPEND_APPEND:
2266 (toList (LAPPEND l1 l2) = SOME x) ==>
2267 (x = (THE(toList l1)++THE(toList l2)))
2268Proof
2269 Cases_on`l2=[||]`>>simp[toList_THM,LAPPEND_NIL_2ND] >>
2270 strip_tac >> fs[toList] >>
2271 rfs[LLENGTH_APPEND] >>
2272 qmatch_assum_abbrev_tac`LTAKE n (LAPPEND l1 l2) = SOME x` >>
2273 `LTAKE n l1 = NONE` by (
2274 match_mp_tac (GEN_ALL LTAKE_LLENGTH_NONE) >>
2275 imp_res_tac LTAKE_LENGTH >>
2276 imp_res_tac LFINITE_HAS_LENGTH >>
2277 fs[Abbr`n`] >>
2278 qspec_then`l2`FULL_STRUCT_CASES_TAC llist_CASES >> fs[] >>
2279 decide_tac ) >>
2280 fs[LTAKE_LAPPEND2,Abbr`n`] >>
2281 simp[toList]
2282QED
2283
2284Theorem LNTH_LLENGTH_NONE :
2285 !x n l. (LLENGTH l = SOME x) /\ x <= n ==> (LNTH n l = NONE)
2286Proof
2287 rw[LESS_OR_EQ] >- (
2288 metis_tac[LTAKE_LLENGTH_NONE,LTAKE_EQ_NONE_LNTH] ) >>
2289 `LFINITE l` by metis_tac[NOT_LFINITE_NO_LENGTH,NOT_NONE_SOME] >>
2290 `n < SUC n` by simp[] >>
2291 `LTAKE (SUC n) l = NONE` by metis_tac[LTAKE_LLENGTH_NONE] >>
2292 qspecl_then[`n`,`l`]mp_tac LTAKE_SNOC_LNTH >>
2293 simp[] >>
2294 CASE_TAC >> simp[] >>
2295 CASE_TAC >> simp[] >>
2296 metis_tac[LTAKE_EQ_NONE_LNTH,NOT_NONE_SOME]
2297QED
2298
2299Theorem LNTH_NONE_MONO:
2300 !m n l.
2301 (LNTH m l = NONE) /\ m <= n
2302 ==>
2303 (LNTH n l = NONE)
2304Proof
2305 rw[] >> match_mp_tac(GEN_ALL LNTH_LLENGTH_NONE) >>
2306 `LFINITE l` by metis_tac[LFINITE_LNTH_NONE] >>
2307 `?z. LLENGTH l = SOME z` by metis_tac[LFINITE_HAS_LENGTH] >>
2308 imp_res_tac LTAKE_LLENGTH_SOME >>
2309 imp_res_tac LTAKE_LENGTH >>
2310 `~(m < z)` by metis_tac[LTAKE_LNTH_EL,NOT_SOME_NONE] >>
2311 rw[] >> decide_tac
2312QED
2313
2314(* NOTE: this is just another version of lnth_some_down_closed *)
2315Theorem LNTH_IS_SOME_MONO :
2316 !m n l.
2317 IS_SOME (LNTH n l) /\ m <= n
2318 ==>
2319 IS_SOME (LNTH m l)
2320Proof
2321 rw [IS_SOME_EXISTS]
2322 >> MATCH_MP_TAC lnth_some_down_closed
2323 >> qexistsl_tac [‘x’, ‘n’] >> rw []
2324QED
2325
2326val LFINITE_strongind = DB.fetch "-" "LFINITE_strongind";
2327
2328Theorem LNTH_IS_SOME_lemma[local] :
2329 !ll. LFINITE ll ==> !n. n < THE (LLENGTH ll) ==> IS_SOME (LNTH n ll)
2330Proof
2331 HO_MATCH_MP_TAC LFINITE_strongind >> rw []
2332 >> gs [LFINITE_LLENGTH]
2333 >> Cases_on ‘n’ >> rw [LNTH_THM]
2334QED
2335
2336Theorem LNTH_IS_SOME :
2337 !n ll. IS_SOME (LNTH n ll) <=> (LFINITE ll ==> n < THE (LLENGTH ll))
2338Proof
2339 rpt GEN_TAC
2340 >> reverse EQ_TAC
2341 >- (rpt STRIP_TAC \\
2342 reverse (Cases_on ‘LFINITE ll’)
2343 >- (fs [LFINITE_LNTH_NONE] \\
2344 POP_ASSUM (MP_TAC o Q.SPEC ‘n’) \\
2345 rw [IS_SOME_EQ_NOT_NONE]) \\
2346 irule LNTH_IS_SOME_lemma >> simp [])
2347 >> rw [LFINITE_LLENGTH] >> rw []
2348 >> rename1 ‘i < N’
2349 >> fs [IS_SOME_EXISTS]
2350 >> CCONTR_TAC
2351 >> ‘N <= i’ by rw []
2352 >> ‘LNTH i ll = NONE’ by PROVE_TAC [LNTH_LLENGTH_NONE]
2353 >> fs []
2354QED
2355
2356Theorem LFINITE_LNTH_IS_SOME :
2357 !n ll. LFINITE ll ==> (IS_SOME (LNTH n ll) <=> n < THE (LLENGTH ll))
2358Proof
2359 rw [LNTH_IS_SOME]
2360QED
2361
2362(* ------------------------------------------------------------------------ *)
2363(* Turning a stream-like linear order into a lazy list *)
2364(* ------------------------------------------------------------------------ *)
2365
2366Definition linear_order_to_list_f_def:
2367 linear_order_to_list_f lo =
2368 let min = minimal_elements (domain lo UNION range lo) lo in
2369 if min = {} then
2370 NONE
2371 else
2372 SOME (rrestrict lo ((domain lo UNION range lo) DIFF min), CHOICE min)
2373End
2374
2375Theorem SUC_EX[local]:
2376 (?x. P (SUC x)) ==> $? P
2377Proof
2378 REWRITE_TAC [EXISTS_DEF] THEN BETA_TAC THEN MATCH_ACCEPT_TAC SELECT_AX
2379QED
2380
2381val PRED_SET_ss = pred_setSimps.PRED_SET_ss ;
2382val set_ss = std_ss ++ pred_setSimps.PRED_SET_ss ;
2383
2384Theorem MIN_LO_IN[local]:
2385 (minimal_elements X lo = {y}) ==> x IN X ==> linear_order lo X ==>
2386 (y, x) IN lo
2387Proof
2388 REPEAT STRIP_TAC THEN IMP_RES_TAC IN_MIN_LO THEN
2389 POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC [IN_INSERT]
2390QED
2391
2392val fploum = REWRITE_RULE [SUBSET_REFL, GSYM AND_IMP_INTRO]
2393(Q.SPECL [`r`, `s`, `s`] finite_prefix_linear_order_has_unique_minimal) ;
2394
2395Theorem idlem[local]:
2396 X INTER (X DIFF Y) = X DIFF Y
2397Proof
2398 SIMP_TAC set_ss [INTER_SUBSET_EQN]
2399QED
2400
2401fun vstac th = VALIDATE (CONV_TAC (DEPTH_CONV (REWR_CONV_A
2402 (UNDISCH_ALL (SPEC_ALL th))))) ;
2403
2404Theorem CARD_SUC_DELETE[local]:
2405 x IN s ==> FINITE s ==> (CARD s = SUC (CARD (s DELETE x)))
2406Proof
2407 REPEAT DISCH_TAC THEN IMP_RES_TAC INSERT_DELETE THEN
2408 POP_ASSUM (fn th => REWRITE_TAC [Once (SYM th)]) THEN
2409 ASM_SIMP_TAC set_ss []
2410QED
2411
2412Theorem pssp[local]:
2413 0 < m ==> (PRE (SUC m) = SUC (PRE m))
2414Proof
2415 SIMP_TAC arith_ss [SUC_PRE]
2416QED
2417
2418Theorem csd_gt0[local]:
2419 FINITE s ==> x IN s ==> ~ (y = x) ==> 0 < CARD (s DELETE y)
2420Proof
2421 REPEAT DISCH_TAC THEN
2422 Q.SUBGOAL_THEN `x IN s DELETE y`
2423 (ASSUME_TAC o MATCH_MP CARD_SUC_DELETE) THEN1
2424 ASM_SIMP_TAC set_ss [] THEN
2425 VALIDATE (POP_ASSUM (ASSUME_TAC o UNDISCH)) THEN1
2426 ASM_REWRITE_TAC [FINITE_DELETE] THEN
2427 ASM_REWRITE_TAC [LESS_0]
2428QED
2429
2430Theorem set_o_CONS[local]:
2431 set o CONS h = $INSERT h o set
2432Proof
2433 REWRITE_TAC [FUN_EQ_THM, o_THM, LIST_TO_SET]
2434QED
2435
2436Theorem lo_single_min_prefix[local]:
2437 linear_order lo X ==> (minimal_elements X lo = {x}) ==>
2438 ({y | (y,x) IN lo} = {x})
2439Proof
2440 Ho_Rewrite.REWRITE_TAC [minimal_elements_def,
2441 EXTENSION, IN_GSPEC_IFF, IN_SING] THEN
2442 REPEAT STRIP_TAC THEN EQ_TAC
2443 THENL [
2444 POP_ASSUM (ASSUME_TAC o Q.SPEC `x`) THEN
2445 RULE_L_ASSUM_TAC (CONJUNCTS o REWRITE_RULE []) THEN
2446 POP_ASSUM (ASSUME_TAC o Q.SPEC `x'`) THEN
2447 DISCH_TAC THEN IMP_RES_TAC linear_order_in_set THEN
2448 RES_TAC THEN ASM_REWRITE_TAC [],
2449 DISCH_TAC THEN VAR_EQ_TAC THEN
2450 POP_ASSUM (ASSUME_TAC o Q.SPEC `x`) THEN
2451 RULE_L_ASSUM_TAC (CONJUNCTS o REWRITE_RULE [linear_order_def]) THEN
2452 FIRST_X_ASSUM (ASSUME_TAC o Q.SPECL [`x`, `x`]) THEN RES_TAC]
2453QED
2454
2455(* we don't actually use the second clause of the conclusion of this,
2456 but it didn't take much extra effort to prove *)
2457Theorem linear_order_to_list_lem1a[local]:
2458 !s. FINITE s ==>
2459 !lo X x.
2460 x IN X /\
2461 ({ y | (y,x) IN lo } = s) /\
2462 linear_order lo X /\
2463 finite_prefixes lo X
2464 ==>
2465 (LNTH (PRE (CARD s)) (LUNFOLD linear_order_to_list_f lo) = SOME x) /\
2466 (OPTION_MAP set (LTAKE (CARD s) (LUNFOLD linear_order_to_list_f lo)) =
2467 SOME s)
2468Proof
2469 HO_MATCH_MP_TAC FINITE_COMPLETE_INDUCTION THEN
2470 REPEAT (GEN_TAC ORELSE DISCH_TAC) THEN
2471 RULE_L_ASSUM_TAC CONJUNCTS THEN
2472 `SING (minimal_elements X lo)`
2473 by EVERY [IMP_RES_THEN (IMP_RES_THEN irule) fploum,
2474 Q.EXISTS_TAC `x`,
2475 FIRST_ASSUM ACCEPT_TAC ] THEN
2476 RULE_ASSUM_TAC (REWRITE_RULE [SING_DEF]) THEN POP_ASSUM CHOOSE_TAC THEN
2477 IMP_RES_TAC linear_order_dom_rg THEN Cases_on `x' = x` THEN1
2478 (* where x is minimum of X *)
2479 (IMP_RES_TAC lo_single_min_prefix THEN
2480 REPEAT VAR_EQ_TAC THEN
2481 ASM_SIMP_TAC (arith_ss ++ PRED_SET_ss) [LNTH_LUNFOLD] THEN
2482 SIMP_TAC (bool_ss ++ PRED_SET_ss)
2483 [ONE, LTAKE_LUNFOLD] THEN
2484 ASM_SIMP_TAC (list_ss ++ PRED_SET_ss) [LET_DEF,
2485 pair_CASE_def, linear_order_to_list_f_def, option_CLAUSES]) THEN
2486 (* where x is not minimum of X *)
2487 Ho_Rewrite.ASM_REWRITE_TAC [BETA_THM, LNTH_LUNFOLD, NOT_INSERT_EMPTY,
2488 OPTION_MAP_DEF, SND, option_case_def, pair_CASE_def, FST,
2489 linear_order_to_list_f_def, LET_DEF] THEN
2490 FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `s DELETE x'`) THEN
2491 Q.SUBGOAL_THEN `x IN s` ASSUME_TAC THEN1
2492 (POP_ASSUM (K ALL_TAC) THEN
2493 IMP_RES_TAC linear_order_refl THEN
2494 REPEAT VAR_EQ_TAC THEN
2495 ASM_SIMP_TAC std_ss [IN_GSPEC_IFF]) THEN
2496 Q.SUBGOAL_THEN `x' IN s` ASSUME_TAC THEN1
2497 (REPEAT VAR_EQ_TAC THEN
2498 Ho_Rewrite.REWRITE_TAC [IN_GSPEC_IFF] THEN
2499 IMP_RES_TAC MIN_LO_IN) THEN
2500 VALIDATE (FIRST_X_ASSUM (ASSUME_TAC o UNDISCH)) THEN1
2501 (SIMP_TAC set_ss [PSUBSET_DEF, SUBSET_DEF, EXTENSION] THEN
2502 Q.EXISTS_TAC `x'` THEN ASM_REWRITE_TAC []) THEN
2503 POP_ASSUM (ASSUME_TAC o Q.SPECL [`rrestrict lo (X DELETE x')`,
2504 `X INTER (X DELETE x')`, `x`]) THEN
2505 VALIDATE (POP_ASSUM (ASSUME_TAC o UNDISCH)) THEN1
2506 (POP_ASSUM (K ALL_TAC) THEN REPEAT CONJ_TAC THENL [
2507 ASM_SIMP_TAC set_ss [],
2508 ASM_SIMP_TAC set_ss [rrestrict_def, EXTENSION] THEN
2509 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN
2510 REPEAT VAR_EQ_TAC THEN
2511 FULL_SIMP_TAC set_ss [] THEN
2512 IMP_RES_TAC in_dom_rg THEN ASM_REWRITE_TAC [],
2513 irule linear_order_restrict >> simp[],
2514 IMP_RES_THEN irule finite_prefixes_subset_rs >> simp[] >>
2515 irule rrestrict_SUBSET ]) THEN
2516 Q.SUBGOAL_THEN `CARD s = SUC (CARD (s DELETE x'))` ASSUME_TAC THEN1
2517 (irule CARD_SUC_DELETE THEN ASM_REWRITE_TAC []) THEN
2518 IMP_RES_TAC csd_gt0 THEN IMP_RES_TAC pssp THEN ASM_REWRITE_TAC [] THEN
2519 Ho_Rewrite.REWRITE_TAC [LNTH_LUNFOLD, LTAKE_LUNFOLD,
2520 linear_order_to_list_f_def, LET_DEF, BETA_THM] THEN
2521 COND_CASES_TAC THEN1 REV_FULL_SIMP_TAC set_ss [] THEN
2522 Ho_Rewrite.ASM_REWRITE_TAC
2523 [option_CLAUSES, pair_CASE_def, BETA_THM, SND, FST,
2524 GSYM DELETE_DEF, OPTION_MAP_COMPOSE, set_o_CONS] THEN
2525 ASM_REWRITE_TAC [GSYM OPTION_MAP_COMPOSE, SOME_11,
2526 OPTION_MAP_DEF, CHOICE_SING, INSERT_DELETE] THEN
2527 irule INSERT_DELETE THEN ASM_REWRITE_TAC []
2528QED
2529
2530Theorem linear_order_to_list_lem2a[local]:
2531 !i lo X x.
2532 linear_order lo X /\
2533 (LNTH i (LUNFOLD linear_order_to_list_f lo) = SOME x)
2534 ==>
2535 x IN X /\ !j. j < i ==>
2536 ?y. (LNTH j (LUNFOLD linear_order_to_list_f lo) = SOME y) /\
2537 (y, x) IN lo /\ ~ (y = x)
2538Proof
2539 Induct THEN
2540 Ho_Rewrite.REWRITE_TAC [LNTH_LUNFOLD,
2541 linear_order_to_list_f_def, LET_DEF, BETA_THM] THEN
2542 REPEAT GEN_TAC THEN COND_CASES_TAC THEN
2543 REWRITE_TAC [OPTION_MAP_DEF, option_CLAUSES] THEN1
2544 (IMP_RES_TAC CHOICE_DEF THEN
2545 REPEAT STRIP_TAC THEN
2546 IMP_RES_TAC linear_order_dom_rg THEN
2547 FULL_SIMP_TAC std_ss [] THEN
2548 IMP_RES_TAC (REWRITE_RULE [SUBSET_DEF] minimal_elements_subset)) THEN
2549 Ho_Rewrite.REWRITE_TAC [ BETA_THM, pair_case_def] THEN STRIP_TAC THEN
2550 IMP_RES_THEN (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th]) THEN
2551 ASSUME_TAC th) linear_order_dom_rg THEN
2552 RULE_ASSUM_TAC (REWRITE_RULE [ONCE_REWRITE_RULE [CONJ_COMM]
2553 (GSYM AND_IMP_INTRO)]) THEN
2554 RES_TAC THEN IMP_RES_TAC linear_order_restrict THEN
2555 POP_ASSUM (ASSUME_TAC o Q.SPEC `X DIFF minimal_elements X lo`) THEN
2556 RES_TAC THEN RULE_ASSUM_TAC (REWRITE_RULE [IN_INTER]) THEN
2557 ASM_REWRITE_TAC [] THEN
2558 (* now the second conjunct of the conclusion *)
2559 Cases THEN Ho_Rewrite.ASM_REWRITE_TAC [LNTH_LUNFOLD,
2560 linear_order_to_list_f_def, LET_DEF, BETA_THM,
2561 option_CLAUSES, FST, SND, pair_CASE_def, LESS_MONO_EQ]
2562 THENL [
2563 (* j = 0, y is a minimal element *)
2564 SIMP_TAC arith_ss [] THEN
2565 IMP_RES_TAC CHOICE_DEF THEN
2566 RULE_L_ASSUM_TAC (CONJUNCTS o REWRITE_RULE [IN_DIFF]) THEN
2567 CONJ_TAC THEN1 IMP_RES_TAC IN_MIN_LO THEN
2568 DISCH_THEN (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th])) THEN
2569 IMP_RES_TAC F_IMP,
2570 (* why doesn't DISCH_THEN IMP_RES_TAC ?? work *)
2571 DISCH_TAC THEN RES_TAC THEN Q.EXISTS_TAC `y''` THEN
2572 ASM_REWRITE_TAC [] THEN
2573 IMP_RES_TAC (REWRITE_RULE [SUBSET_DEF] rrestrict_SUBSET) ]
2574QED
2575
2576Theorem linear_order_to_list_lem1d[local]:
2577 linear_order lo X ==> finite_prefixes lo X ==> x IN X ==>
2578 LNTH (PRE (CARD {y | (y,x) IN lo})) (LUNFOLD linear_order_to_list_f lo) =
2579 SOME x
2580Proof
2581 REPEAT DISCH_TAC THEN
2582 irule (cj 1 linear_order_to_list_lem1a) >> rpt conj_tac THENL [
2583 RULE_ASSUM_TAC (REWRITE_RULE [finite_prefixes_def]) THEN RES_TAC,
2584 REFL_TAC,
2585 Q.EXISTS_TAC `X` THEN ASM_REWRITE_TAC []
2586 ]
2587QED
2588
2589Theorem linear_order_to_llist_eq:
2590 !lo X.
2591 linear_order lo X /\
2592 finite_prefixes lo X
2593 ==>
2594 ?ll.
2595 (X = { x | ?i. LNTH i ll = SOME x }) /\
2596 (lo = { (x,y) | ?i j. i <= j /\ (LNTH i ll = SOME x) /\
2597 (LNTH j ll = SOME y) }) /\
2598 (!i j x. (LNTH i ll = SOME x) /\ (LNTH j ll = SOME x) ==> (i = j))
2599Proof
2600 REPEAT STRIP_TAC THEN
2601 Q.EXISTS_TAC `LUNFOLD linear_order_to_list_f lo` THEN
2602 Ho_Rewrite.REWRITE_TAC [EXTENSION, IN_GSPEC_IFF] THEN
2603 REPEAT (STRIP_TAC ORELSE EQ_TAC)
2604 THENL [
2605 IMP_RES_TAC linear_order_to_list_lem1d THEN
2606 Q.EXISTS_TAC `PRE (CARD {y | (y,x) IN lo})` THEN
2607 ASM_REWRITE_TAC [],
2608 IMP_RES_TAC linear_order_to_list_lem2a,
2609 Cases_on `x` THEN Ho_Rewrite.REWRITE_TAC [PAIR_IN_GSPEC_IFF] THEN
2610 Q.EXISTS_TAC `PRE (CARD {y | (y,q) IN lo})` THEN
2611 Q.EXISTS_TAC `PRE (CARD {y | (y,r) IN lo})` THEN
2612 IMP_RES_TAC in_dom_rg THEN IMP_RES_TAC linear_order_dom_rg THEN
2613 IMP_RES_TAC linear_order_to_list_lem1d THEN
2614 Q.SUBGOAL_THEN `q IN X /\ r IN X`
2615 (EVERY o map ASSUME_TAC o CONJUNCTS) THEN1
2616 (VAR_EQ_TAC THEN ASM_REWRITE_TAC [IN_UNION]) THEN
2617 RES_TAC THEN ASM_REWRITE_TAC [] THEN
2618 irule PRE_LESS_EQ THEN irule CARD_SUBSET >> conj_tac THEN1
2619 (RULE_ASSUM_TAC (REWRITE_RULE [finite_prefixes_def]) THEN RES_TAC) THEN
2620 Ho_Rewrite.REWRITE_TAC [SUBSET_DEF, IN_GSPEC_IFF] THEN
2621 REPEAT STRIP_TAC THEN
2622 RULE_ASSUM_TAC (REWRITE_RULE [linear_order_def, transitive_def]) THEN
2623 RES_TAC,
2624 Cases_on `x` THEN
2625 RULE_ASSUM_TAC (Ho_Rewrite.REWRITE_RULE [PAIR_IN_GSPEC_IFF]) THEN
2626 REPEAT (POP_ASSUM CHOOSE_TAC) THEN
2627 RULE_L_ASSUM_TAC CONJUNCTS THEN
2628 IMP_RES_TAC linear_order_to_list_lem2a THEN
2629 RULE_ASSUM_TAC (REWRITE_RULE [LESS_OR_EQ]) THEN
2630 REVERSE (FIRST_X_ASSUM DISJ_CASES_TAC) THEN1
2631 (FULL_SIMP_TAC bool_ss [SOME_11] THEN IMP_RES_TAC linear_order_refl) THEN
2632 RES_TAC THEN REV_FULL_SIMP_TAC bool_ss [SOME_11],
2633 DISJ_CASES_TAC (Q.SPECL [`i`, `j`] LESS_LESS_CASES) THEN1
2634 FIRST_ASSUM ACCEPT_TAC THEN
2635 POP_ASSUM DISJ_CASES_TAC THEN
2636 IMP_RES_TAC linear_order_to_list_lem2a THEN
2637 REV_FULL_SIMP_TAC bool_ss [SOME_11]]
2638QED
2639
2640Theorem linear_order_to_llist:
2641 !lo X.
2642 linear_order lo X /\
2643 finite_prefixes lo X
2644 ==>
2645 ?ll.
2646 (X = { x | ?i. LNTH i ll = SOME x }) /\
2647 lo SUBSET { (x,y) | ?i j. i <= j /\ (LNTH i ll = SOME x) /\
2648 (LNTH j ll = SOME y) } /\
2649 (!i j x. (LNTH i ll = SOME x) /\ (LNTH j ll = SOME x) ==> (i = j))
2650Proof
2651 REPEAT STRIP_TAC THEN IMP_RES_TAC linear_order_to_llist_eq THEN
2652 Q.EXISTS_TAC `ll'` THEN ASM_REWRITE_TAC [SUBSET_REFL]
2653QED
2654
2655Definition LPREFIX_def:
2656 LPREFIX l1 l2 =
2657 case toList l1 of
2658 | NONE => (l1 = l2)
2659 | SOME xs =>
2660 case toList l2 of
2661 | NONE => LTAKE (LENGTH xs) l2 = SOME xs
2662 | SOME ys => isPREFIX xs ys
2663End
2664
2665Theorem LPREFIX_LNIL[simp]:
2666 LPREFIX [||] ll /\
2667 (LPREFIX ll [||] <=> (ll = [||]))
2668Proof
2669 rw[LPREFIX_def,toList_THM] >>
2670 CASE_TAC >>
2671 simp[IS_PREFIX_NIL] >>
2672 rw[EQ_IMP_THM] >> fs[toList_THM] >>
2673 (* "Cases_on `ll`" *)
2674 Q.ISPEC_THEN`ll`FULL_STRUCT_CASES_TAC llist_CASES >>
2675 fs[toList_THM]
2676QED
2677
2678Theorem LPREFIX_LCONS:
2679 (!ll h t.
2680 LPREFIX ll (h:::t) <=>
2681 ((ll = [||]) \/ ?l. (ll = h:::l) /\ LPREFIX l t)) /\
2682 (!h t ll.
2683 LPREFIX (h:::t) ll <=>
2684 ?l. (ll = h:::l) /\ LPREFIX t l)
2685Proof
2686 rw[] >>
2687 Q.ISPEC_THEN`ll`FULL_STRUCT_CASES_TAC llist_CASES >>
2688 simp[LPREFIX_def,toList_THM] >>
2689 every_case_tac >> fs[] >> rw[EQ_IMP_THM]
2690QED
2691
2692Theorem LPREFIX_LUNFOLD:
2693 LPREFIX ll (LUNFOLD f n) <=>
2694 case f n of NONE => (ll = LNIL)
2695 | SOME (n,x) => !h t. (ll = h:::t) ==> (h = x) /\ LPREFIX t (LUNFOLD f n)
2696Proof
2697 CASE_TAC >- (
2698 simp[LUNFOLD_THM,LPREFIX_LNIL] ) >>
2699 CASE_TAC >>
2700 imp_res_tac LUNFOLD_THM >>
2701 simp[LPREFIX_LCONS] >>
2702 (* "Cases_on `ll`" *)
2703 Q.ISPEC_THEN`ll`FULL_STRUCT_CASES_TAC llist_CASES >>
2704 simp[]
2705QED
2706
2707Theorem LPREFIX_REFL[simp]:
2708 LPREFIX ll ll
2709Proof
2710 rw[LPREFIX_def] >> CASE_TAC >> simp[]
2711QED
2712
2713Theorem LPREFIX_ANTISYM:
2714 LPREFIX l1 l2 /\ LPREFIX l2 l1 ==> l1 = l2
2715Proof
2716 rw[LPREFIX_def] >>
2717 every_case_tac >> fs[] >>
2718 imp_res_tac IS_PREFIX_ANTISYM >> rw[] >>
2719 metis_tac[to_fromList,THE_DEF,toList,NOT_SOME_NONE]
2720QED
2721
2722Theorem LPREFIX_TRANS:
2723 LPREFIX l1 l2 /\ LPREFIX l2 l3 ==> LPREFIX l1 l3
2724Proof
2725 rw[LPREFIX_def] >>
2726 every_case_tac >> gvs[] >>
2727 TRY(imp_res_tac IS_PREFIX_TRANS >> NO_TAC) >>
2728 imp_res_tac IS_PREFIX_LENGTH >>
2729 imp_res_tac LTAKE_TAKE_LESS >> simp[] >>
2730 fs[IS_PREFIX_APPEND] >>
2731 simp[TAKE_APPEND1]
2732QED
2733
2734Theorem LPREFIX_fromList:
2735 !l ll.
2736 LPREFIX (fromList l) ll <=>
2737 case toList ll of
2738 | NONE => LTAKE (LENGTH l) ll = SOME l
2739 | SOME ys => isPREFIX l ys
2740Proof
2741 rw [LPREFIX_def, from_toList]
2742QED
2743
2744Theorem prefixes_lprefix_total:
2745 !ll. !l1 l2. LPREFIX l1 ll /\ LPREFIX l2 ll ==>
2746 LPREFIX l1 l2 \/ LPREFIX l2 l1
2747Proof
2748 rw[LPREFIX_def] >> reverse every_case_tac >> fs[]
2749 >- metis_tac[prefixes_is_prefix_total] >>
2750 rpt(pop_assum mp_tac) >>
2751 qho_match_abbrev_tac`P l1 l2 x x'` >>
2752 `P l1 l2 x x' <=> P l2 l1 x' x` by (
2753 simp[Abbr`P`] >> metis_tac[] ) >>
2754 `!ll1 ll2 l1 l2. LENGTH l1 <= LENGTH l2 ==> P ll1 ll2 l1 l2` suffices_by (
2755 rw[] >> metis_tac[LESS_EQ_CASES] ) >>
2756 pop_assum kall_tac >> unabbrev_all_tac >> rw[] >>
2757 `l1 = (TAKE (LENGTH l1) l2)` by (
2758 metis_tac[LTAKE_TAKE_LESS,SOME_11] ) >>
2759 simp[IS_PREFIX_APPEND] >>
2760 metis_tac[TAKE_DROP]
2761QED
2762
2763Theorem LPREFIX_LAPPEND1[local]:
2764 LPREFIX ll (LAPPEND ll l2)
2765Proof
2766 rw[LPREFIX_def] >> every_case_tac >>
2767 metis_tac[LFINITE_toList,NOT_LFINITE_APPEND,NOT_SOME_NONE,
2768 IS_SOME_EXISTS,to_fromList,THE_DEF,LTAKE_LAPPEND1,
2769 LTAKE_fromList,toList_LAPPEND_APPEND,
2770 IS_PREFIX_APPEND]
2771QED
2772
2773Theorem LTAKE_IMP_LDROP:
2774 !n ll l1.
2775 (LTAKE n ll = SOME l1) ==>
2776 ?l2. (LDROP n ll = SOME l2) /\
2777 (LAPPEND (fromList l1) l2 = ll)
2778Proof
2779 Induct >> simp[] >>
2780 gen_tac >> qspec_then`ll`FULL_STRUCT_CASES_TAC llist_CASES >> rw[] >>
2781 first_x_assum(fn th => first_x_assum (strip_assume_tac o MATCH_MP th)) >>
2782 rw[]
2783QED
2784
2785Theorem LDROP_EQ_LNIL'[local]:
2786 !n ll. (LDROP n ll = SOME LNIL) <=> (LLENGTH ll = SOME n)
2787Proof
2788 Induct THEN
2789 FULL_SIMP_TAC std_ss [LDROP_FUNPOW, FUNPOW, LLENGTH_0] THEN GEN_TAC THEN
2790 llist_CASE_TAC ``ll : 'a llist`` THEN
2791 ASM_SIMP_TAC std_ss [LTL_THM, LLENGTH_THM, FUNPOW_BIND_NONE,
2792 SUC_NOT]
2793QED
2794
2795Theorem LDROP_EQ_LNIL = SPEC_ALL LDROP_EQ_LNIL' ;
2796
2797Theorem LPREFIX_APPEND:
2798 LPREFIX l1 l2 <=> ?ll. l2 = LAPPEND l1 ll
2799Proof
2800 reverse EQ_TAC >- metis_tac[LPREFIX_LAPPEND1] >>
2801 simp[LPREFIX_def] >>
2802 Cases_on`toList l1`>>fs[]
2803 >- metis_tac[LAPPEND_NIL_2ND] >>
2804 `LFINITE l1` by fs[toList] >>
2805 imp_res_tac LFINITE_HAS_LENGTH >>
2806 `LTAKE n l1 = SOME x` by fs[toList] >>
2807 imp_res_tac LTAKE_LENGTH >> rw[] >>
2808 qexists_tac`THE(LDROP (LENGTH x) l2)` >>
2809 rw[LNTH_EQ] >>
2810 simp[LNTH_LAPPEND] >>
2811 rw[] >>
2812 every_case_tac >> fs[toList] >>
2813 imp_res_tac LTAKE_LNTH_EL >> simp[] >>
2814 fs[IS_PREFIX_APPEND] >> rw[] >>
2815 imp_res_tac LTAKE_LENGTH >> fs[] >>
2816 TRY (
2817 first_x_assum(qspec_then`n`mp_tac) >>
2818 simp[EL_APPEND1] >> NO_TAC) >>
2819 TRY (
2820 imp_res_tac LTAKE_IMP_LDROP >> rw[] >>
2821 simp[LNTH_LAPPEND] >>
2822 NO_TAC) >>
2823 `LTAKE (LENGTH x) l2 = SOME x` by (
2824 imp_res_tac LTAKE_TAKE_LESS >>
2825 rpt(first_x_assum(qspec_then`LENGTH x`mp_tac)) >>
2826 simp[TAKE_APPEND1] ) >>
2827 pop_assum(strip_assume_tac o MATCH_MP LTAKE_IMP_LDROP) >>
2828 rw[LNTH_LAPPEND]
2829QED
2830
2831Theorem LFINITE_LDROP_APPEND1[local]:
2832 !l. LFINITE l ==>
2833 !n z. (LDROP n l = SOME z) ==>
2834 !l2. LDROP n (LAPPEND l l2) = SOME (LAPPEND z l2)
2835Proof
2836 ho_match_mp_tac LFINITE_INDUCTION >> simp[] >>
2837 conj_tac >- ( Cases >> simp[] ) >>
2838 ntac 3 strip_tac >> Cases >> simp[]
2839QED
2840
2841Theorem NOT_LFINITE_DROP_LFINITE:
2842 !n l t. ~LFINITE l /\ (LDROP n l = SOME t) ==> ~LFINITE t
2843Proof
2844 Induct >> simp[] >> gen_tac >>
2845 qspec_then`l`FULL_STRUCT_CASES_TAC llist_CASES >>
2846 simp[] >> metis_tac[]
2847QED
2848
2849Theorem LDROP_APPEND1:
2850 (LDROP n l1 = SOME l) ==>
2851 (LDROP n (LAPPEND l1 l2) = SOME (LAPPEND l l2))
2852Proof
2853 rw[] >>
2854 Cases_on`LFINITE l1` >- (
2855 metis_tac[LFINITE_LDROP_APPEND1] ) >>
2856 imp_res_tac NOT_LFINITE_DROP_LFINITE >>
2857 simp[NOT_LFINITE_APPEND]
2858QED
2859
2860Theorem LDROP_fromList:
2861 !ls n.
2862 LDROP n (fromList ls) =
2863 if n <= LENGTH ls then SOME (fromList (DROP n ls)) else NONE
2864Proof
2865 Induct >- ( Cases >> simp[] ) >>
2866 gen_tac >> Cases >> simp[]
2867QED
2868
2869Theorem LDROP_SUC:
2870 LDROP (SUC n) ls = OPTION_BIND (LDROP n ls) LTL
2871Proof
2872 SIMP_TAC std_ss [LDROP_FUNPOW, FUNPOW_SUC]
2873QED
2874
2875Theorem LDROP_1[simp]:
2876 LDROP (1: num) (h:::t) = SOME t
2877Proof `LDROP (SUC 0) (h:::t) = SOME t` by fs[LDROP] >>
2878 metis_tac[ONE]
2879QED
2880
2881Theorem LDROP_NONE_LFINITE:
2882 (LDROP k l = NONE) ==> LFINITE l
2883Proof
2884 metis_tac[NOT_LFINITE_DROP,NOT_SOME_NONE]
2885QED
2886
2887Theorem LDROP_LDROP:
2888 !ll k1 k2. ~ LFINITE ll ==>
2889 (THE (LDROP k2 (THE (LDROP k1 ll))) =
2890 THE (LDROP k1 (THE (LDROP k2 ll))))
2891Proof
2892 rw[] >>
2893 `LDROP (k1+k2) ll = LDROP (k2 + k1) ll` by fs[] >>
2894 fs[LDROP_ADD] >>
2895 NTAC 2 (full_case_tac >- imp_res_tac LDROP_NONE_LFINITE) >> fs[]
2896QED
2897
2898(* ----------------------------------------------------------------------
2899 LGENLIST : (num -> 'a) -> num option -> 'a llist
2900 ---------------------------------------------------------------------- *)
2901
2902Definition LGENLIST_def[nocompute]:
2903 (LGENLIST f NONE = LUNFOLD (\n. SOME (n + 1, f n)) 0) /\
2904 (LGENLIST f (SOME lim) = LUNFOLD (\n. if n < lim then SOME (n + 1, f n)
2905 else NONE) 0)
2906End
2907
2908Theorem LHD_LGENLIST[simp,compute]:
2909 LHD (LGENLIST f limopt) =
2910 if limopt = SOME 0 then NONE else SOME (f 0)
2911Proof
2912 Cases_on `limopt` >> simp[LGENLIST_def] >> rw[] >> simp[EXISTS_PROD]
2913QED
2914
2915Theorem LTL_LGENLIST[simp,compute]:
2916 LTL (LGENLIST f limopt) =
2917 if limopt = SOME 0 then NONE
2918 else SOME (LGENLIST (f o SUC) (OPTION_MAP PRE limopt))
2919Proof
2920 Cases_on `limopt` >> simp[LGENLIST_def]
2921 >- (`!m. LUNFOLD (\n. SOME (n + 1, f n)) (m + 1) =
2922 LUNFOLD (\n. SOME (n + 1, f (SUC n))) m`
2923 suffices_by metis_tac[DECIDE ``0 + 1 = 1``] >>
2924 simp[LNTH_EQ] >> Induct_on `n` >> simp[LNTH_LUNFOLD] >>
2925 simp[ADD1]) >>
2926 reverse (rw[]) >- fs[] >>
2927 `!m l. 0 < l ==>
2928 (LUNFOLD (\n. if n < PRE l then SOME (n + 1, f (SUC n)) else NONE) m =
2929 LUNFOLD (\n. if n < l then SOME (n + 1, f n) else NONE) (m + 1))`
2930 suffices_by metis_tac[DECIDE ``0 + 1 = 1``] >>
2931 dsimp[LNTH_EQ] >> Induct_on `n` >>
2932 simp[LNTH_LUNFOLD, DECIDE ``0 < x ==> (y < PRE x <=> y + 1 < x)``,
2933 ADD1] >> rw[]
2934QED
2935
2936(* maybe useful? *)
2937Theorem numopt_BISIMULATION:
2938 !mopt nopt.
2939 (mopt = nopt) <=>
2940 ?R. R mopt nopt /\
2941 !m n. R m n ==>
2942 (m = SOME 0) /\ (n = SOME 0) \/
2943 m <> SOME 0 /\ n <> SOME 0 /\
2944 R (OPTION_MAP PRE m) (OPTION_MAP PRE n)
2945Proof
2946 simp[EQ_IMP_THM, FORALL_AND_THM] >> conj_tac
2947 >- (gen_tac >> qexists_tac `(=)` >> simp[]) >>
2948 rpt strip_tac >>
2949 Cases_on `mopt`
2950 >- (Cases_on `nopt` >> simp[] >> rename1 `R NONE (SOME n)` >>
2951 Induct_on `n` >> strip_tac >> res_tac >> fs[]) >>
2952 Cases_on `nopt` >> simp[]
2953 >- (rename1 `R (SOME m) NONE` >> Induct_on `m` >> strip_tac >>
2954 res_tac >> fs[]) >>
2955 rename1 `R (SOME m) (SOME n)` >>
2956 `!m n. R (SOME m) (SOME n) ==> (m = n)` suffices_by metis_tac[] >>
2957 Induct >> rpt strip_tac >- (res_tac >> fs[]) >>
2958 rename1 `R (SOME (SUC m0)) (SOME n0)` >>
2959 `n0 <> 0 /\ R (SOME m0) (SOME (PRE n0))` by (res_tac >> fs[]) >>
2960 `m0 = PRE n0` by res_tac >> simp[]
2961QED
2962
2963Theorem LGENLIST_EQ_LNIL[simp]:
2964 ((LGENLIST f n = LNIL) <=> (n = SOME 0)) /\
2965 ((LNIL = LGENLIST f n) <=> (n = SOME 0))
2966Proof
2967 Cases_on `n` >> simp[LGENLIST_def] >> rpt conj_tac >>
2968 simp[Once LUNFOLD] >> rename [`0 < limit`] >> Cases_on `limit` >> simp[]
2969QED
2970
2971Theorem LFINITE_LGENLIST[simp]:
2972 LFINITE (LGENLIST f n) <=> n <> NONE
2973Proof
2974 Cases_on `n` >> simp[]
2975 >- (`!l. LFINITE l ==> !f. l <> LGENLIST f NONE` suffices_by metis_tac[] >>
2976 simp[LGENLIST_def] >>
2977 `!l. LFINITE l ==> !f n. l <> LUNFOLD (\n. SOME (n + 1, f n)) n`
2978 suffices_by metis_tac[] >>
2979 ho_match_mp_tac LFINITE_STRONG_INDUCTION >> conj_tac
2980 >- simp[Once LUNFOLD] >>
2981 rpt gen_tac >> strip_tac >> simp[Once LUNFOLD]) >>
2982 rename [`LFINITE (LGENLIST f (SOME n))`] >> simp[LGENLIST_def] >>
2983 `!m. m <= n ==>
2984 LFINITE (LUNFOLD (\x. if x < n then SOME (x + 1, f x) else NONE) m)`
2985 suffices_by metis_tac[DECIDE ``0 <= x``] >>
2986 Induct_on `n - m` >> simp[Once LUNFOLD]
2987QED
2988
2989Theorem LTL_HD_LTL_LHD:
2990 LTL_HD l = OPTION_BIND (LHD l) (\h. OPTION_BIND (LTL l) (λt. SOME (t, h)))
2991Proof
2992 simp[LTL_HD_HD, LTL_HD_TL] >>
2993 Cases_on `LTL_HD l` >> simp[]
2994QED
2995
2996Theorem LGENLIST_SOME[simp]:
2997 (LGENLIST f (SOME 0) = [||]) /\
2998 (!n. LGENLIST f (SOME (SUC n)) = f 0 ::: LGENLIST (f o SUC) (SOME n))
2999Proof
3000 rpt strip_tac >> irule (iffLR LTL_HD_11) >>
3001 simp[LTL_HD_LTL_LHD, Excl "LTL_HD_11"]
3002QED
3003
3004Theorem LGENLIST_SOME_compute[compute] =
3005 CONJ (CONJUNCT1 LGENLIST_SOME)
3006 (CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV (CONJUNCT2 LGENLIST_SOME))
3007
3008Theorem LNTH_LGENLIST:
3009 !n f lim.
3010 LNTH n (LGENLIST f lim) =
3011 case lim of NONE => SOME (f n)
3012 | SOME lim0 => if n < lim0 then SOME (f n) else NONE
3013Proof
3014 Induct_on `n` >> simp[LNTH] >> rpt gen_tac
3015 >- (Cases_on `lim` >> simp[] >> rename [`0 < n`] >> Cases_on `n` >> simp[]) >>
3016 Cases_on `lim` >> simp[] >>
3017 rename [`SUC n < lim`] >> Cases_on `lim` >> simp[]
3018QED
3019
3020Theorem LNTH_LMAP[simp]:
3021 !n f l. LNTH n (LMAP f l) = OPTION_MAP f (LNTH n l)
3022Proof
3023 Induct >> simp[LNTH] >> rpt gen_tac >>
3024 Q.SPEC_THEN `l` STRUCT_CASES_TAC llist_CASES >> simp[]
3025QED
3026
3027Theorem LLENGTH_LGENLIST[simp,compute]:
3028 !f. LLENGTH (LGENLIST f limopt) = limopt
3029Proof
3030 Cases_on `limopt`
3031 >- metis_tac[NOT_LFINITE_NO_LENGTH, LFINITE_LGENLIST] >>
3032 rename [`LGENLIST _ (SOME n)`] >> Induct_on `n` >> simp[]
3033QED
3034
3035Theorem LMAP_LGENLIST[simp]:
3036 LMAP f (LGENLIST g limopt) = LGENLIST (f o g) limopt
3037Proof
3038 simp[LNTH_EQ, LNTH_LGENLIST] >>
3039 Cases_on `limopt` >> simp[] >> rw[]
3040QED
3041
3042Theorem LGENLIST_EQ_CONS:
3043 (LGENLIST f NONE = h:::t) <=>
3044 (h = f 0) /\ (t = LGENLIST (f o (+) 1) NONE)
3045Proof
3046 simp[LGENLIST_def] >> simp[SimpLHS, Once LUNFOLD] >>
3047 `!m. LUNFOLD (\n. SOME (n + 1, f n)) m =
3048 LUNFOLD (\n. SOME (n + 1, f(n + m))) 0` suffices_by metis_tac[] >>
3049 gen_tac >> simp[Once LLIST_STRONG_BISIMULATION] >>
3050 qexists_tac `\l1 l2. ?k m.
3051 (l1 = LUNFOLD (\n. SOME (n + 1, f n)) (m + k)) /\
3052 (l2 = LUNFOLD (\n. SOME (n + 1, f (n + m))) k)` >> simp[] >> conj_tac
3053 >- metis_tac[ADD_CLAUSES] >>
3054 dsimp[] >> rpt gen_tac >> disj2_tac >>
3055 qspec_then `LUNFOLD (\n. SOME (n + 1, f n)) (k + m)` strip_assume_tac
3056 llist_CASES >> simp[]
3057 >- fs[Once LUNFOLD] >>
3058 pop_assum mp_tac >>
3059 simp[SimpL ``$==>``, Once LUNFOLD] >> rw[] >>
3060 map_every qexists_tac [`k+1`, `m`] >> simp[] >>
3061 simp[Once LUNFOLD, SimpLHS]
3062QED
3063
3064(* ----------------------------------------------------------------------
3065 LREPEAT : 'a list -> 'a llist
3066
3067 Infinite repetitions of the argument. If it's [], then the result is
3068 [||]
3069 ---------------------------------------------------------------------- *)
3070
3071Definition LREPEAT_def[nocompute]:
3072 LREPEAT l = if NULL l then [||]
3073 else LGENLIST (\n. EL (n MOD LENGTH l) l) NONE
3074End
3075
3076Theorem LGENLIST_CHUNK_GENLIST:
3077 LGENLIST f NONE =
3078 LAPPEND (fromList (GENLIST f n)) (LGENLIST (f o (+) n) NONE)
3079Proof
3080 simp[Once LLIST_STRONG_BISIMULATION] >>
3081 qexists_tac `\l1 l2. ?m n.
3082 (l1 = LGENLIST (f o (+) m) NONE) /\
3083 (l2 = LAPPEND (fromList (GENLIST (f o (+) m) n))
3084 (LGENLIST (f o $+ (m + n)) NONE))` >>
3085 simp[] >> conj_tac
3086 >- (map_every qexists_tac [`0`, `n`] >>
3087 `$+ 0 = I` by simp[FUN_EQ_THM] >> simp[]) >>
3088 dsimp[] >> qx_genl_tac [`m`, `n`] >>
3089 disj2_tac >>
3090 Q.SPEC_THEN `LGENLIST (f o $+ m) NONE` strip_assume_tac llist_CASES >>
3091 fs[LGENLIST_EQ_CONS] >> rw[] >>
3092 map_every qexists_tac [`m + 1`] >> simp[o_DEF] >>
3093 Cases_on `n` >> simp[]
3094 >- (simp[LGENLIST_EQ_CONS] >> qexists_tac `0` >> simp[o_DEF]) >>
3095 rename [`SUC k`] >> qexists_tac `k` >> simp[GENLIST_CONS] >>
3096 simp[o_DEF, ADD1]
3097QED
3098
3099Theorem LREPEAT_thm:
3100 LREPEAT l = LAPPEND (fromList l) (LREPEAT l)
3101Proof
3102 rw[LREPEAT_def] >- (Cases_on `l` >> fs[]) >>
3103 `0 < LENGTH l /\ l <> []` by (Cases_on `l` >> fs[]) >>
3104 qmatch_abbrev_tac `LGENLIST f NONE = LAPPEND (fromList l) _` >>
3105 `(l = GENLIST f (LENGTH l)) /\ (f = f o (+) (LENGTH l))`
3106 suffices_by metis_tac[LGENLIST_CHUNK_GENLIST] >>
3107 simp[Abbr`f`, o_DEF] >>
3108 simp[LIST_EQ_REWRITE]
3109QED
3110
3111Theorem LREPEAT_NIL[simp,compute]:
3112 LREPEAT [] = LNIL
3113Proof
3114 simp[LREPEAT_def]
3115QED
3116
3117Theorem LREPEAT_EQ_LNIL[simp]:
3118 ((LREPEAT l = LNIL) <=> (l = [])) /\
3119 ((LNIL = LREPEAT l) <=> (l = []))
3120Proof
3121 Cases_on `l` >> simp[] >> conj_tac >> simp[Once LREPEAT_thm]
3122QED
3123
3124Theorem LHD_LREPEAT[simp,compute]:
3125 LHD (LREPEAT l) = LHD (fromList l)
3126Proof
3127 Cases_on `l = []` >> simp[] >> simp[Once LREPEAT_thm, LHD_LAPPEND]
3128QED
3129
3130Theorem LTL_LREPEAT[simp,compute]:
3131 LTL (LREPEAT l) = OPTION_MAP (\t. LAPPEND t (LREPEAT l)) (LTL (fromList l))
3132Proof
3133 Cases_on `l = []` >> simp[] >> simp[Once LREPEAT_thm, LTL_LAPPEND] >>
3134 Cases_on `l` >> fs[]
3135QED
3136
3137Theorem LLENGTH_LREPEAT:
3138 LLENGTH (LREPEAT l) = if NULL l then SOME 0 else NONE
3139Proof
3140 rw[LREPEAT_def]
3141QED
3142
3143(* --------------------------------------------------------------------------
3144 Case constant, distinctness etc. for TypeBase
3145 -------------------------------------------------------------------------- *)
3146
3147Definition llist_CASE_def[nocompute]:
3148 llist_CASE ll b f =
3149 case LTL_HD ll of
3150 NONE => b
3151 | SOME(ltl,lhd) => f lhd ltl
3152End
3153
3154Theorem llist_CASE_compute[simp,compute]:
3155 (llist_CASE [||] b f = b) /\
3156 (llist_CASE (x:::ll) b f = f x ll)
3157Proof
3158 rw[llist_CASE_def]
3159QED
3160
3161Theorem LLIST_BISIMULATION_I =
3162 LLIST_BISIMULATION |> SPEC_ALL |> PURE_ONCE_REWRITE_RULE[EQ_IMP_THM]
3163 |> CONJUNCT2 |> Q.GEN `ll1` |> Q.GEN `ll2`
3164
3165Theorem LLIST_CASE_CONG:
3166 !M M' v f.
3167 M = M' /\ (M' = [||] ==> v = v') /\
3168 (!a0 a1. M' = a0:::a1 ==> f a0 a1 = f' a0 a1) ==>
3169 llist_CASE M v f = llist_CASE M' v' f'
3170Proof
3171 rpt GEN_TAC >>
3172 llist_CASE_TAC ``M':'a llist`` >>
3173 rw[]
3174QED
3175
3176Theorem LLIST_CASE_EQ:
3177 llist_CASE (x:'a llist) v f = v' <=>
3178 x = [||] /\ v = v' \/ ?a l. x = a:::l /\ f a l = v'
3179Proof
3180 llist_CASE_TAC ``x:'a llist`` >> rw[]
3181QED
3182
3183Theorem LLIST_CASE_ELIM:
3184 !f'. f'(llist_CASE (x:'a llist) v f) <=>
3185 x = [||] /\ f' v \/ ?a l. x = a:::l /\ f'(f a l)
3186Proof
3187 llist_CASE_TAC ``x:'a llist`` >> rw[FUN_EQ_THM]
3188QED
3189
3190Theorem LLIST_DISTINCT:
3191 !a1 a0. [||] <> a0:::a1
3192Proof
3193 rw[]
3194QED
3195
3196Definition LSET_def:
3197 LSET l x = ?n. LNTH n l = SOME x
3198End
3199
3200Theorem IN_LSET :
3201 !x l. x IN LSET l <=> ?n. LNTH n l = SOME x
3202Proof
3203 rw [IN_APP, LSET_def]
3204QED
3205
3206Theorem LSET[simp]:
3207 LSET LNIL = {} /\
3208 LSET (x:::xs) = x INSERT LSET xs
3209Proof
3210 fs [EXTENSION] \\ fs [LSET_def,IN_DEF]
3211 \\ rw [] \\ eq_tac \\ rw []
3212 THEN1 (Cases_on `n` \\ fs [] \\ metis_tac [])
3213 THEN1 (qexists_tac `0` \\ fs [])
3214 THEN1 (qexists_tac `SUC n` \\ fs [])
3215QED
3216
3217Theorem LSET_fromList[simp] :
3218 LSET (fromList l) = set l
3219Proof
3220 rw [Once EXTENSION, IN_LSET, LNTH_fromList, MEM_EL]
3221 >> METIS_TAC []
3222QED
3223
3224Definition llist_rel_def:
3225 llist_rel R l1 l2 <=>
3226 LLENGTH l1 = LLENGTH l2 /\
3227 !i x y. LNTH i l1 = SOME x /\ LNTH i l2 = SOME y ==> R x y
3228End
3229
3230(* --------------------------------------------------------------------------
3231 Update TypeBase
3232 -------------------------------------------------------------------------- *)
3233
3234Overload "case" = “llist_CASE”;
3235val _ = TypeBase.export
3236 [TypeBasePure.mk_datatype_info
3237 {
3238 ax = TypeBasePure.ORIG llist_Axiom,
3239 induction = TypeBasePure.ORIG LLIST_BISIMULATION_I,
3240 case_def = llist_CASE_compute,
3241 case_cong = LLIST_CASE_CONG,
3242 case_eq = LLIST_CASE_EQ,
3243 case_elim = LLIST_CASE_ELIM,
3244 nchotomy = llist_CASES,
3245 size = NONE,
3246 encode = NONE,
3247 lift = NONE,
3248 one_one = SOME LCONS_11,
3249 distinct = SOME LLIST_DISTINCT,
3250 fields = [],
3251 accessors = [],
3252 updates = [],
3253 destructors = [],
3254 recognizers = []
3255 }
3256 ]
3257
3258(* ----------------------------------------------------------------------
3259 Temporal logic style operators
3260 ---------------------------------------------------------------------- *)
3261
3262val (eventually_rules,eventually_ind,eventually_cases) = Hol_reln‘
3263 (!ll. P ll ==> eventually P ll) /\
3264 (!h t. eventually P t ==> eventually P (h:::t))
3265’;
3266
3267Theorem eventually_thm[simp]:
3268 (eventually P [||] = P [||]) /\
3269 (eventually P (h:::t) = (P (h:::t) \/ eventually P t))
3270Proof
3271 CONJ_TAC THEN
3272 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [eventually_cases])) THEN
3273 SRW_TAC [][Cong (REWRITE_RULE [GSYM AND_IMP_INTRO] OR_CONG)]
3274QED
3275
3276val (always_rules,always_coind,always_cases) = Hol_coreln‘
3277 (!h t. (P (h ::: t) /\ always P t) ==> always P (h ::: t))
3278’;
3279
3280Theorem always_thm[simp]:
3281 (always P [||] <=> F) /\
3282 !h t. always P (h:::t) <=> P (h:::t) /\ always P t
3283Proof conj_tac >> simp[Once always_cases]
3284QED
3285
3286Theorem always_conj_l:
3287 !ll. always (\x. P x /\ Q x) ll ==> always P ll
3288Proof
3289 ho_match_mp_tac always_coind >> rw[] >> Cases_on`ll` >> fs[]
3290QED
3291
3292Theorem always_eventually_ind:
3293 (!ll. (P ll \/ (~P ll /\ Q (THE(LTL ll)))) ==> Q ll) ==>
3294 !ll. ll <> [||] ==> always(eventually P) ll ==> Q ll
3295Proof
3296 `(!ll. (P ll \/ (~P ll /\ Q (THE(LTL ll)))) ==> Q ll) ==>
3297 (!ll. eventually P ll ==> (Q ll))`
3298 by (strip_tac >> ho_match_mp_tac eventually_ind >>
3299 fs[DISJ_IMP_THM, FORALL_AND_THM] >> rw[] >>
3300 Cases_on ‘P (h:::t)’ >> simp[]) >>
3301 rw[] >> Cases_on`ll` >> fs[] >> res_tac >> first_x_assum irule >> simp[]
3302QED
3303
3304Theorem always_DROP:
3305 !ll. always P ll ==> always P (THE(LDROP k ll))
3306Proof
3307 Induct_on`k` >> Cases_on`ll` >> fs[always_thm,LDROP] >>
3308 rw[] >> imp_res_tac always_thm >> fs[]
3309QED
3310
3311val (until_rules,until_ind,until_cases) = Hol_reln‘
3312 (!ll. Q ll ==> until P Q ll) /\
3313 (!h t. P (h:::t) /\ until P Q t ==> until P Q (h:::t))
3314’;
3315
3316Theorem eventually_until_EQN: eventually P = until (K T) P
3317Proof
3318 simp[FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] >> conj_tac
3319 >- (Induct_on ‘eventually’ >> rpt strip_tac
3320 >- (irule (CONJUNCT1 (SPEC_ALL until_rules)) >> simp[])
3321 >- (irule (CONJUNCT2 (SPEC_ALL until_rules)) >> simp[]))
3322 >- (Induct_on ‘until’ >> simp[eventually_rules])
3323QED
3324
3325(* might be nice if this was also true, but behaviour of eventually at LNIL
3326 as written doesn't allow it; we would have to have
3327 eventually P [||] <=> T
3328*)
3329(*
3330Theorem eventually_NOT_always_EQN: eventually P = $~ o always ($~ o P)
3331Proof
3332 simp[FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] >> conj_tac
3333 >- (Induct_on ‘eventually’ >> simp[] >> Cases >> simp[]) >>
3334 CONV_TAC (STRIP_QUANT_CONV CONTRAPOS_CONV) >> simp[] >>
3335 ho_match_mp_tac always_coind >> Cases >> simp[]
3336QED
3337*)
3338
3339(* ----------------------------------------------------------------------
3340 Discriminating finite and infinite lists
3341 ---------------------------------------------------------------------- *)
3342
3343Definition fromSeq_def:
3344 fromSeq f = LUNFOLD (\x. SOME (SUC x, f x)) 0
3345End
3346
3347Theorem fromSeq_LCONS:
3348 fromSeq f = LCONS (f 0) (fromSeq (f o SUC))
3349Proof
3350 PURE_REWRITE_TAC[fromSeq_def,Once LUNFOLD] >>
3351 simp[] >>
3352 PURE_REWRITE_TAC[Once LUNFOLD_BISIMULATION] >>
3353 qexists_tac ‘\x y. x = SUC y’ >>
3354 rw[Once LUNFOLD]
3355QED
3356
3357Theorem fromList_fromSeq:
3358 !ll. (?l. ll = fromList l) \/ (?f. ll = fromSeq f)
3359Proof
3360 strip_tac >>
3361 Cases_on ‘LFINITE ll’ >-
3362 (drule_then strip_assume_tac LFINITE_toList >>
3363 disj1_tac >>
3364 qexists_tac ‘THE(toList ll)’ >>
3365 drule_then MATCH_ACCEPT_TAC (GSYM to_fromList)) >>
3366 disj2_tac >>
3367 qexists_tac ‘\n. THE(LNTH n ll)’ >>
3368 PURE_REWRITE_TAC[Once LLIST_BISIMULATION] >>
3369 qexists_tac ‘\x y. ~LFINITE x /\ (?n. y = (fromSeq (\n. THE (LNTH n x))))’ >>
3370 rw[] >>
3371 last_x_assum kall_tac >>
3372 rename1 ‘ll = [||]’ >>
3373 disj2_tac >>
3374 simp[Once fromSeq_LCONS] >>
3375 Cases_on ‘ll’ >>
3376 FULL_SIMP_TAC std_ss [LFINITE_THM,LNTH_THM,LHD_THM,LTL_THM] >>
3377 simp[Once fromSeq_LCONS,o_DEF]
3378QED
3379
3380Theorem llist_forall_split:
3381 !P. (!ll. P ll) <=> (!l. P (fromList l)) /\ (!f. P (fromSeq f))
3382Proof
3383 gen_tac \\ eq_tac \\ rpt strip_tac
3384 \\ asm_rewrite_tac []
3385 \\ qspec_then ‘ll’ mp_tac fromList_fromSeq
3386 \\ strip_tac \\ asm_rewrite_tac []
3387QED
3388
3389Theorem LHD_fromSeq[simp]:
3390 !f. LHD (fromSeq f) = SOME (f 0)
3391Proof
3392 rw [Once fromSeq_LCONS]
3393QED
3394
3395Theorem LTL_fromSeq[simp]:
3396 !f. LTL (fromSeq f) = SOME (fromSeq (f o SUC))
3397Proof
3398 rw [Once fromSeq_LCONS]
3399QED
3400
3401Theorem LNTH_fromSeq[simp]:
3402 !n f. LNTH n (fromSeq f) = SOME (f n)
3403Proof
3404 Induct \\ rw [LNTH]
3405QED
3406
3407Theorem LTAKE_fromSeq[simp]:
3408 !n f. LTAKE n (fromSeq f) = SOME (GENLIST f n)
3409Proof
3410 Induct \\ rw []
3411 \\ rw [Once fromSeq_LCONS, GSYM GENLIST_CONS]
3412QED
3413
3414Theorem LDROP_fromSeq[simp]:
3415 !n f. LDROP n (fromSeq f) = SOME (fromSeq (f o ((+) n)))
3416Proof
3417 Induct \\ rw []
3418 THEN1 (AP_TERM_TAC \\ rw [FUN_EQ_THM,ADD1])
3419 \\ rw [Once fromSeq_LCONS]
3420 \\ AP_TERM_TAC \\ rw [FUN_EQ_THM,ADD1]
3421QED
3422
3423Theorem LFINITE_fromSeq[simp]:
3424 !f. ~LFINITE (fromSeq f)
3425Proof
3426 rw [LFINITE]
3427QED
3428
3429Theorem LLENGTH_fromSeq[simp]:
3430 !f. LLENGTH (fromSeq f) = NONE
3431Proof
3432 rw [LLENGTH]
3433QED
3434
3435Theorem LGENLIST_EQ_fromSeq:
3436 !f. LGENLIST f NONE = fromSeq f
3437Proof
3438 rewrite_tac [LGENLIST_def,fromSeq_def,ADD1]
3439QED
3440
3441Theorem LGENLIST_EQ_fromList:
3442 !f k. LGENLIST f (SOME k) = fromList (GENLIST f k)
3443Proof
3444 Induct_on ‘k’ \\ fs [GENLIST_CONS]
3445QED
3446
3447Theorem LAPPEND_fromSeq[simp]:
3448 (!f ll. LAPPEND (fromSeq f) ll = fromSeq f) /\
3449 (!l f. LAPPEND (fromList l) (fromSeq f) =
3450 fromSeq (\n. if n < LENGTH l then EL n l else f (n - LENGTH l)))
3451Proof
3452 conj_tac
3453 THEN1 (gen_tac \\ match_mp_tac NOT_LFINITE_APPEND \\ rw [])
3454 \\ Induct
3455 THEN1 (rw [LAPPEND] \\ AP_TERM_TAC \\ rw [FUN_EQ_THM])
3456 \\ rw [LAPPEND] \\ once_rewrite_tac [EQ_SYM_EQ]
3457 \\ rw [Once fromSeq_LCONS]
3458 \\ AP_TERM_TAC \\ rw [FUN_EQ_THM]
3459QED
3460
3461Theorem LMAP_fromSeq[simp]:
3462 !f g. LMAP f (fromSeq g) = fromSeq (f o g)
3463Proof
3464 rewrite_tac [GSYM LGENLIST_EQ_fromSeq,LMAP_LGENLIST]
3465QED
3466
3467Theorem LMAP_fromList:
3468 LMAP f (fromList l) = fromList(MAP f l)
3469Proof
3470 Induct_on `l` >> fs[]
3471QED
3472
3473Theorem MAP_toList :
3474 !ll f. LFINITE ll ==> MAP f (THE (toList ll)) = THE (toList (LMAP f ll))
3475Proof
3476 rpt STRIP_TAC
3477 >> ‘ll = fromList (THE (toList ll))’ by METIS_TAC [to_fromList]
3478 >> POP_ORW
3479 >> simp [LMAP_fromList, to_fromList, from_toList]
3480QED
3481
3482Theorem exists_fromSeq[simp]:
3483 !p f. exists p (fromSeq f) = ?i. p (f i)
3484Proof
3485 rw [] \\ reverse eq_tac
3486 THEN1
3487 (fs [PULL_EXISTS]
3488 \\ qid_spec_tac ‘f’
3489 \\ Induct_on ‘i’ \\ rw []
3490 \\ rw [Once fromSeq_LCONS])
3491 \\ qsuff_tac ‘!ll. exists p ll ==> !f. ll = fromSeq f ==> ?i. p (f i)’
3492 THEN1 rw []
3493 \\ ho_match_mp_tac exists_ind \\ rw []
3494 \\ pop_assum mp_tac
3495 \\ rw [Once fromSeq_LCONS]
3496 THEN1 (qexists_tac ‘0’ \\ fs [])
3497 \\ first_x_assum (qspec_then ‘f o SUC’ mp_tac)
3498 \\ rw [] \\ qexists_tac ‘SUC i’ \\ fs []
3499QED
3500
3501Theorem every_fromSeq[simp]:
3502 !p f. every p (fromSeq f) = !i. p (f i)
3503Proof
3504 rewrite_tac [every_def] \\ rw []
3505QED
3506
3507Theorem LFILTER_fromSeq:
3508 !p f.
3509 LFILTER p (fromSeq f) =
3510 if !i. ~p (f i) then LNIL else
3511 if p (f 0) then LCONS (f 0) (LFILTER p (fromSeq (f o SUC)))
3512 else LFILTER p (fromSeq (f o SUC))
3513Proof
3514 gen_tac \\ gen_tac \\ IF_CASES_TAC
3515 \\ rw [LFILTER_EQ_NIL,Once fromSeq_LCONS]
3516QED
3517
3518(* more theorems about fromList and fromSeq *)
3519
3520Theorem fromList_11[simp]:
3521 !xs ys. fromList xs = fromList ys <=> xs = ys
3522Proof
3523 Induct \\ Cases_on ‘ys’ \\ fs []
3524QED
3525
3526Theorem fromSeq_11[simp]:
3527 !f g. fromSeq f = fromSeq g <=> f = g
3528Proof
3529 rw [] \\ eq_tac \\ rw [] \\ fs [FUN_EQ_THM]
3530 \\ gen_tac \\ rename [‘f n = g n’]
3531 \\ pop_assum mp_tac
3532 \\ qid_spec_tac ‘f’
3533 \\ qid_spec_tac ‘g’
3534 \\ Induct_on ‘n’ \\ fs []
3535 \\ once_rewrite_tac [fromSeq_LCONS] \\ fs []
3536 \\ rw [] \\ res_tac \\ fs []
3537QED
3538
3539Theorem fromList_NEQ_fromSeq[simp]:
3540 !l f. fromList l <> fromSeq f
3541Proof
3542 CCONTR_TAC \\ fs []
3543 \\ qspec_then ‘l’ mp_tac LFINITE_fromList
3544 \\ qspec_then ‘f’ mp_tac LFINITE_fromSeq
3545 \\ METIS_TAC []
3546QED
3547
3548Theorem LFINITE_IMP_fromList:
3549 !ll. LFINITE ll ==> ?l. ll = fromList l
3550Proof
3551 rw [] \\ qspec_then ‘ll’ mp_tac fromList_fromSeq
3552 \\ rw [] \\ fs []
3553QED
3554
3555Theorem NOT_LFINITE_IMP_fromSeq:
3556 !ll. ~LFINITE ll ==> ?f. ll = fromSeq f
3557Proof
3558 rw [] \\ qspec_then ‘ll’ mp_tac fromList_fromSeq
3559 \\ rw [] \\ fs [LFINITE_fromList]
3560QED
3561
3562(* suffix over lazy lists *)
3563Definition LSUFFIX_def:
3564 LSUFFIX xs zs <=> ?ys. xs = LAPPEND (fromList ys) zs \/ zs = LNIL
3565End
3566
3567Theorem LSUFFIX:
3568 LSUFFIX l LNIL = T /\
3569 LSUFFIX LNIL (LCONS y ys) = F /\
3570 LSUFFIX (LCONS x xs) l = (LCONS x xs = l \/ LSUFFIX xs l)
3571Proof
3572 fs [LSUFFIX_def] \\ rw [] \\ eq_tac \\ rw []
3573 THEN1 (rename [‘fromList zs’] \\ Cases_on ‘zs’ \\ fs []
3574 \\ disj2_tac \\ qexists_tac ‘t’ \\ fs [])
3575 THEN1 (qexists_tac ‘[]’ \\ fs [])
3576 THEN1 (qexists_tac ‘x::ys’ \\ fs [])
3577QED
3578
3579Theorem LSUFFIX_fromList:
3580 !xs ys. LSUFFIX (fromList xs) (fromList ys) <=> IS_SUFFIX xs ys
3581Proof
3582 rpt gen_tac \\ fs [LSUFFIX_def,LAPPEND_fromList]
3583 \\ qid_spec_tac ‘ys’
3584 \\ qid_spec_tac ‘xs’
3585 \\ ho_match_mp_tac SNOC_INDUCT \\ rw []
3586 THEN1
3587 (qspec_then ‘ys’ mp_tac SNOC_CASES \\ rpt strip_tac
3588 \\ asm_rewrite_tac [IS_SUFFIX] \\ fs [SNOC_APPEND])
3589 \\ qspec_then ‘ys’ mp_tac SNOC_CASES \\ rpt strip_tac
3590 \\ asm_rewrite_tac [IS_SUFFIX]
3591 \\ fs [GSYM PULL_EXISTS, SNOC_APPEND]
3592 \\ Cases_on ‘l = []’ \\ fs []
3593 \\ asm_rewrite_tac [IS_SUFFIX]
3594 \\ first_x_assum (qspec_then ‘l’ mp_tac)
3595 \\ asm_simp_tac std_ss []
3596 \\ rw [] \\ eq_tac \\ rw []
3597QED
3598
3599Theorem LSUFFIX_REFL[simp]:
3600 !s. LSUFFIX s s
3601Proof
3602 rw [LSUFFIX_def] \\ qexists_tac ‘[]’ \\ fs []
3603QED
3604
3605Theorem LSUFFIX_TRANS:
3606 !x y z. LSUFFIX x y /\ LSUFFIX y z ==> LSUFFIX x z
3607Proof
3608 rw [LSUFFIX_def]
3609 \\ fs [LAPPEND_EQ_LNIL]
3610 \\ rename [‘LAPPEND (fromList zs1) (LAPPEND (fromList zs2) _)’]
3611 \\ qexists_tac ‘zs1 ++ zs2’
3612 \\ rewrite_tac [GSYM LAPPEND_ASSOC,LAPPEND_fromList]
3613QED
3614
3615Theorem LSUFFIX_ANTISYM:
3616 !x y. LSUFFIX x y /\ LSUFFIX y x /\ LFINITE x ==> x = y
3617Proof
3618 rw [LSUFFIX_def,LAPPEND_EQ_LNIL]
3619 \\ imp_res_tac LFINITE_IMP_fromList \\ rw []
3620 \\ fs [LAPPEND_fromList]
3621QED
3622
3623Theorem LTAKE_LAPPEND_fromList:
3624 !ll l n.
3625 LTAKE (n + LENGTH l) (LAPPEND (fromList l) ll) =
3626 OPTION_MAP (APPEND l) (LTAKE n ll)
3627Proof
3628 rw [] \\ Cases_on `LTAKE n ll` \\ fs []
3629 THEN1 (
3630 `LFINITE ll` by (fs [LFINITE] \\ goal_assum drule)
3631 \\ drule LFINITE_HAS_LENGTH \\ strip_tac \\ rename1 `SOME m`
3632 \\ irule LTAKE_LLENGTH_NONE
3633 \\ qexists_tac `m + LENGTH l` \\ rw []
3634 THEN1 (
3635 drule LTAKE_LLENGTH_SOME \\ strip_tac
3636 \\ Cases_on `n <= m` \\ fs []
3637 \\ drule (GEN_ALL LTAKE_TAKE_LESS)
3638 \\ disch_then drule \\ fs [])
3639 \\ fs [LLENGTH_APPEND, LFINITE_fromList])
3640 \\ Induct_on `l` \\ rw []
3641 \\ fs [LTAKE_CONS_EQ_SOME]
3642 \\ goal_assum(drule o PURE_ONCE_REWRITE_RULE[CONJ_SYM])
3643 \\ simp[]
3644QED
3645
3646Theorem LTAKE_LPREFIX:
3647 !x ll.
3648 ~LFINITE ll ==>
3649 ?l. LTAKE x ll = SOME l /\ LPREFIX (fromList l) ll
3650Proof
3651 rpt strip_tac >>
3652 imp_res_tac NOT_LFINITE_IMP_fromSeq >> VAR_EQ_TAC >>
3653 simp[LPREFIX_fromList,LFINITE_toList_SOME,LPREFIX_fromList,toList]
3654QED
3655
3656Theorem LPREFIX_NTH:
3657 LPREFIX l1 l2 <=>
3658 !i v. LNTH i l1 = SOME v ==> LNTH i l2 = SOME v
3659Proof
3660 qspec_then `l1` strip_assume_tac fromList_fromSeq
3661 \\ qspec_then `l2` strip_assume_tac fromList_fromSeq
3662 \\ rw [LPREFIX_def,from_toList]
3663 \\ fs [toList,FUN_EQ_THM]
3664 \\ fs [LNTH_fromList]
3665 THEN1
3666 (qid_spec_tac `l'` \\ qid_spec_tac `l` \\ Induct \\ fs []
3667 \\ Cases_on `l'` \\ fs [] THEN1 (qexists_tac `0` \\ fs [])
3668 \\ rw [] \\ eq_tac \\ rw []
3669 \\ TRY (Cases_on `i` \\ fs [] \\ NO_TAC)
3670 THEN1 (first_x_assum (qspec_then `0` mp_tac) \\ fs [])
3671 \\ first_x_assum (qspec_then `SUC i` mp_tac) \\ fs [])
3672 THEN1
3673 (qid_spec_tac `l`
3674 \\ ho_match_mp_tac SNOC_INDUCT
3675 \\ fs [GSYM ADD1,GENLIST] \\ rw []
3676 \\ eq_tac \\ rw []
3677 THEN1
3678 (Cases_on `i = LENGTH l` \\ fs []
3679 \\ fs [SNOC_APPEND,
3680 EL_LENGTH_APPEND,EL_APPEND1])
3681 \\ fs [SNOC_APPEND,
3682 EL_LENGTH_APPEND,EL_APPEND1])
3683 THEN1 (qexists_tac `LENGTH l` \\ fs [])
3684 \\ eq_tac \\ rw []
3685QED
3686
3687(* ----------------------------------------------------------------------
3688 Lazy list bisimulation up-to context, = and transitivity
3689 ---------------------------------------------------------------------- *)
3690
3691Inductive llist_upto:
3692 (llist_upto R x x) /\
3693 (R x y ==> llist_upto R x y) /\
3694 (llist_upto R x y /\ llist_upto R y z ==> llist_upto R x z) /\
3695 (llist_upto R x y ==> llist_upto R (LAPPEND z x) (LAPPEND z y))
3696End
3697
3698local val [llist_upto_eq,llist_upto_rel,llist_upto_trans,llist_upto_context] =
3699 llist_upto_rules |> SPEC_ALL |> CONJUNCTS |> map GEN_ALL
3700in
3701Theorem llist_upto_eq = llist_upto_eq
3702Theorem llist_upto_rel = llist_upto_rel
3703Theorem llist_upto_trans = llist_upto_trans
3704Theorem llist_upto_context = llist_upto_context;
3705end
3706
3707Theorem LLIST_BISIM_UPTO:
3708 !ll1 ll2 R.
3709 R ll1 ll2 /\
3710 (!ll3 ll4.
3711 R ll3 ll4 ==>
3712 ll3 = [||] /\ ll4 = [||] \/
3713 LHD ll3 = LHD ll4 /\
3714 llist_upto R (THE (LTL ll3)) (THE (LTL ll4)))
3715 ==> ll1 = ll2
3716Proof
3717 rpt strip_tac
3718 >> PURE_ONCE_REWRITE_TAC[LLIST_BISIMULATION]
3719 >> qexists_tac `llist_upto R`
3720 >> conj_tac >- rw[llist_upto_rules]
3721 >> ho_match_mp_tac llist_upto_ind
3722 >> rpt conj_tac
3723 >- rw[llist_upto_rules]
3724 >- first_x_assum ACCEPT_TAC
3725 >- (rw[]
3726 >> match_mp_tac OR_INTRO_THM2
3727 >> conj_tac >- simp[]
3728 >> metis_tac[llist_upto_rules])
3729 >- (rw[llist_upto_rules]
3730 >> Cases_on `ll3 = [||]`
3731 >- (Cases_on `ll4` >> fs[llist_upto_rules])
3732 >> match_mp_tac OR_INTRO_THM2
3733 >> conj_tac
3734 >- (Cases_on `z` >> simp[])
3735 >> Cases_on `z` >- simp[]
3736 >> simp[]
3737 >> Cases_on `ll3` >> Cases_on `ll4`
3738 >> fs[] >> rpt VAR_EQ_TAC
3739 >> CONV_TAC(RAND_CONV
3740 (RAND_CONV
3741 (RAND_CONV(PURE_ONCE_REWRITE_CONV [GSYM(cj 1 LAPPEND)]))))
3742 >> CONV_TAC(RATOR_CONV
3743 (RAND_CONV
3744 (RAND_CONV(RAND_CONV
3745 (PURE_ONCE_REWRITE_CONV [GSYM(cj 1 LAPPEND)])))))
3746 >> PURE_ONCE_REWRITE_TAC[GSYM(CONJUNCT2 LAPPEND)]
3747 >> simp[GSYM LAPPEND_ASSOC]
3748 >> metis_tac[llist_upto_rules])
3749QED
3750
3751Theorem LDROP_LCONS_LNTH:
3752 !n xs a t. LDROP n xs = SOME (a:::t) ==> LNTH n xs = SOME a
3753Proof
3754 Induct \\ fs [] \\ Cases \\ fs []
3755QED
3756
3757Theorem LDROP_WHILE_LEMMA[local]:
3758 !n k xs ys zs y z.
3759 LTAKE n xs = SOME ys /\
3760 LTAKE k xs = SOME zs /\
3761 LNTH n xs = SOME y /\
3762 LNTH k xs = SOME z /\
3763 ~P y /\ ~P z /\ EVERY P ys /\ EVERY P zs ==>
3764 n = k
3765Proof
3766 Induct \\ Cases_on ‘k’ \\ fs []
3767 \\ Cases_on ‘xs’ \\ fs [] \\ rw []
3768 \\ CCONTR_TAC \\ fs [] \\ fs []
3769 \\ res_tac
3770QED
3771
3772Theorem LDROP_WHILE[local]:
3773 ?f.
3774 (!P. f P LNIL = LNIL) /\
3775 (!P x xs. f P (LCONS x xs) = if P x then f P xs else LCONS x xs) /\
3776 (!P l. every P l ==> f P l = LNIL)
3777Proof
3778 qabbrev_tac ‘foo = λP l n. ?x ls. LNTH n l = SOME x /\ ~P x /\
3779 LTAKE n l = SOME ls /\ EVERY P ls’
3780 \\ qexists_tac ‘λP l. if every P l then LNIL else
3781 THE (LDROP (@n. foo P l n) l)’
3782 \\ rpt strip_tac \\ fs []
3783 \\ reverse (Cases_on ‘P x’) \\ fs []
3784 >-
3785 (qsuff_tac ‘!n. foo P (x:::xs) n <=> n = 0’ >- fs []
3786 \\ unabbrev_all_tac \\ fs []
3787 \\ rw [] \\ eq_tac \\ rw []
3788 \\ Cases_on ‘n’ \\ gvs [])
3789 \\ Cases_on ‘every P xs’ \\ fs []
3790 \\ fs [every_def,exists_thm_strong]
3791 \\ fs [EVERY_MEM] \\ fs [GSYM EVERY_MEM]
3792 \\ drule_then assume_tac LDROP_LCONS_LNTH
3793 \\ qsuff_tac ‘(!k. foo P xs k <=> k = n) /\
3794 (!k. foo P (x:::xs) k <=> k = SUC n)’ >- fs []
3795 \\ rw [Abbr‘foo’]
3796 \\ rw [] \\ eq_tac \\ rw []
3797 >- (imp_res_tac LDROP_WHILE_LEMMA \\ fs [])
3798 \\ Cases_on ‘k’ \\ gvs []
3799 \\ imp_res_tac LDROP_WHILE_LEMMA \\ fs []
3800QED
3801
3802val LDROP_WHILE = new_specification("LDROP_WHILE",["LDROP_WHILE"],LDROP_WHILE);
3803
3804Theorem LTAKE_WHILE[local]:
3805 ?f.
3806 (!P. f P LNIL = LNIL) /\
3807 (!P x xs. f P (LCONS x xs) = if P x then x ::: f P xs else LNIL) /\
3808 (!P l. every P l ==> f P l = l)
3809Proof
3810 qabbrev_tac ‘foo = λP l n. ?x ls. LNTH n l = SOME x /\ ~P x /\
3811 LTAKE n l = SOME ls /\ EVERY P ls’
3812 \\ qexists_tac ‘λP l. if every P l then l else
3813 fromList (THE (LTAKE (@n. foo P l n) l))’
3814 \\ rpt strip_tac \\ fs []
3815 \\ reverse (Cases_on ‘P x’) \\ fs []
3816 >-
3817 (qsuff_tac ‘!n. foo P (x:::xs) n <=> n = 0’ >- fs []
3818 \\ unabbrev_all_tac \\ fs []
3819 \\ rw [] \\ eq_tac \\ rw []
3820 \\ Cases_on ‘n’ \\ gvs [])
3821 \\ Cases_on ‘every P xs’ \\ fs []
3822 \\ fs [every_def,exists_thm_strong]
3823 \\ fs [EVERY_MEM] \\ fs [GSYM EVERY_MEM]
3824 \\ drule_then assume_tac LDROP_LCONS_LNTH
3825 \\ qsuff_tac ‘(!k. foo P xs k <=> k = n) /\
3826 (!k. foo P (x:::xs) k <=> k = SUC n)’ >- fs []
3827 \\ rw [Abbr‘foo’]
3828 \\ rw [] \\ eq_tac \\ rw []
3829 >- (imp_res_tac LDROP_WHILE_LEMMA \\ fs [])
3830 \\ Cases_on ‘k’ \\ gvs []
3831 \\ imp_res_tac LDROP_WHILE_LEMMA \\ fs []
3832QED
3833
3834val LTAKE_WHILE = new_specification("LTAKE_WHILE",["LTAKE_WHILE"],LTAKE_WHILE);
3835
3836Theorem LTAKE_WHILE_LDROP_WHILE:
3837 !P l. LAPPEND (LTAKE_WHILE P l) (LDROP_WHILE P l) = l
3838Proof
3839 rw [] \\ Cases_on ‘every P l’
3840 >- fs [LTAKE_WHILE,LDROP_WHILE,LAPPEND_NIL_2ND]
3841 \\ fs [every_def,exists_thm_strong]
3842 \\ fs [EVERY_MEM] \\ fs [GSYM EVERY_MEM]
3843 \\ rpt $ pop_assum mp_tac
3844 \\ qid_spec_tac ‘l'’
3845 \\ qid_spec_tac ‘l’
3846 \\ qid_spec_tac ‘n’
3847 \\ Induct
3848 >- fs [LTAKE_WHILE,LDROP_WHILE]
3849 \\ Cases
3850 \\ fs [LTAKE_WHILE,LDROP_WHILE,PULL_EXISTS]
3851QED
3852
3853Definition lbind_def:
3854 lbind ll f = LFLATTEN (LMAP f ll)
3855End
3856
3857Theorem lbind_EQ_NIL:
3858 lbind ll f = [||] <=>
3859 !e. e IN LSET ll ==> f e = [||]
3860Proof
3861 REWRITE_TAC [Once $ DECIDE “(p = q:bool) = (~p = ~q)”] >>
3862 simp_tac pure_ss [NOT_FORALL_THM] >>
3863 simp[lbind_def, LFLATTEN_EQ_NIL, every_def,
3864 exists_LNTH, LSET_def, PULL_EXISTS, IN_DEF] >>
3865 metis_tac[]
3866QED
3867
3868Theorem LFLATTEN_APPEND_FINITE1:
3869 !l1 l2.
3870 LFINITE l1 ==>
3871 LFLATTEN (LAPPEND l1 l2) = LAPPEND (LFLATTEN l1) (LFLATTEN l2)
3872Proof
3873 Induct_on ‘LFINITE’ using LFINITE_INDUCTION >> simp[LAPPEND_ASSOC]
3874QED
3875
3876Theorem LFINITE_LFILTER:
3877 !ll. LFINITE ll ==> LFINITE (LFILTER P ll)
3878Proof
3879 Induct_on ‘LFINITE’ >> rw[]
3880QED
3881
3882Theorem not_compose:
3883 $~ o ($~ o f) = f /\ $~ o $~ = I
3884Proof
3885 simp[FUN_EQ_THM]
3886QED
3887
3888Theorem LFLATTEN_fromList_of_NILs:
3889 EVERY ($= LNIL) l ==> LFLATTEN (fromList l) = LNIL
3890Proof
3891 Induct_on ‘l’ >> simp[]
3892QED
3893
3894Theorem LFINITE_LFLATTEN:
3895 LFINITE (LFLATTEN ll) <=>
3896 LFINITE $ LFILTER ($~ o $= LNIL) ll /\ every LFINITE ll
3897Proof
3898 reverse eq_tac >> rw[] >> simp[every_def] >~
3899 [‘~exists _ ll’]
3900 >- (strip_tac >> qpat_x_assum ‘LFINITE _’ mp_tac >>
3901 pop_assum mp_tac >> Induct_on ‘exists’ >> simp[]) >~
3902 [‘every LFINITE ll’]
3903 >- (rpt $ pop_assum mp_tac >> qid_spec_tac ‘ll’ >> Induct_on ‘LFINITE’ >>
3904 rpt strip_tac >> gs[LFILTER_EQ_NIL, not_compose, iffRL LFLATTEN_EQ_NIL]>>
3905 drule_then strip_assume_tac LFILTER_EQ_CONS >>
3906 gvs[LFLATTEN_APPEND_FINITE1, LFINITE_fromList,
3907 not_compose, LFLATTEN_fromList_of_NILs] >>
3908 drule_at (Pos last) every_LAPPEND2_LFINITE >>
3909 simp[LFINITE_fromList]) >>
3910 rpt $ pop_assum mp_tac >> qid_spec_tac ‘ll’ >> Induct_on ‘LFINITE’ >>
3911 rw[]
3912 >- gs[LFLATTEN_EQ_NIL, iffRL LFILTER_EQ_NIL, not_compose] >>
3913 Cases_on ‘LFILTER ($~ o $= LNIL) ll’ >> simp[] >>
3914 drule_then strip_assume_tac LFILTER_EQ_CONS >>
3915 gvs[not_compose, LFLATTEN_APPEND_FINITE1, LFINITE_fromList,
3916 LFILTER_APPEND] >>
3917 rename [‘LNIL <> hl’,
3918 ‘LAPPEND (LFLATTEN $ fromList l) (LAPPEND hl $ LFLATTEN ll2) =
3919 h:::ll1’] >>
3920 ‘FILTER ($~ o $= LNIL) l = []’
3921 by simp[FILTER_EQ_NIL, SF ETA_ss] >>
3922 gs[LFLATTEN_fromList_of_NILs] >>
3923 Cases_on ‘hl’ >> gvs[] >> rename [‘LFLATTEN _ = LAPPEND t _’] >>
3924 first_x_assum $ qspec_then ‘t:::ll2’ mp_tac >> simp[LFLATTEN_APPEND] >>
3925 rw[] >> rw[]
3926QED
3927
3928Theorem LFLATTEN_EQ_CONS:
3929 LFLATTEN ll = h:::t <=>
3930 ?p e t1 t2.
3931 ll = LAPPEND p ((h:::t1) ::: t2) /\
3932 LFINITE p /\ every ($= LNIL) p /\
3933 t = LAPPEND t1 (LFLATTEN t2)
3934Proof
3935 reverse eq_tac >> rpt strip_tac
3936 >- (simp[LFLATTEN_APPEND_FINITE1] >>
3937 ‘LFLATTEN p = LNIL’ suffices_by simp[] >>
3938 simp[LFLATTEN_EQ_NIL]) >>
3939 ‘exists ($~ o $= LNIL) ll’
3940 by (CCONTR_TAC >> gs[GSYM every_def, GSYM LFLATTEN_EQ_NIL]) >>
3941 rpt (pop_assum mp_tac) >> map_every qid_spec_tac [‘h’, ‘t’, ‘ll’] >>
3942 Induct_on ‘exists’ >> rw[] >~
3943 [‘LNIL <> hl’, ‘LAPPEND hl $ LFLATTEN t1 = h:::t2’]
3944 >- (Cases_on ‘hl’ >> gvs[] >> irule_at Any EQ_REFL >> qexists ‘LNIL’ >>
3945 simp[]) >~
3946 [‘LAPPEND hl $ LFLATTEN t1 = h:::t2’] >>
3947 Cases_on ‘hl’ >> gvs[]
3948 >- (qexists ‘LNIL ::: p’ >> simp[] >> metis_tac[]) >>
3949 qexists ‘LNIL’ >> simp[]
3950QED
3951
3952Theorem lbind_APPEND:
3953 LFINITE l1 ==>
3954 lbind (LAPPEND l1 l2) f = LAPPEND (lbind l1 f) (lbind l2 f)
3955Proof
3956 simp[lbind_def, LMAP_APPEND, LFLATTEN_APPEND_FINITE1]
3957QED
3958
3959Theorem lbind_CONS[simp]:
3960 lbind (h:::t) f = LAPPEND (f h) (lbind t f)
3961Proof
3962 simp[lbind_def]
3963QED
3964
3965Theorem LMAP_EQ_NIL[simp]:
3966 (LMAP f l = LNIL <=> l = LNIL) /\
3967 (LNIL = LMAP f l <=> l = LNIL)
3968Proof
3969 Cases_on ‘l’ >> simp[]
3970QED
3971
3972Theorem LMAP_EQ_CONS:
3973 LMAP f l = h:::t <=> ?h0 t0. l = h0:::t0 /\ h = f h0 /\ t = LMAP f t0
3974Proof
3975 Cases_on ‘l’ >> simp[] >> metis_tac[]
3976QED
3977
3978Theorem LMAP_EQ_APPEND_FINITE1:
3979 !ll ll1 ll2.
3980 LFINITE ll1 ==>
3981 (LMAP f ll = LAPPEND ll1 ll2 <=>
3982 ?ll10 ll20. ll = LAPPEND ll10 ll20 /\ LMAP f ll10 = ll1 /\
3983 LMAP f ll20 = ll2)
3984Proof
3985 Induct_on ‘LFINITE’ >> simp[LMAP_EQ_CONS, PULL_EXISTS] >> metis_tac[]
3986QED
3987
3988Theorem lbind_EQ_CONS:
3989 lbind ll f = h:::t <=>
3990 ?p e s t1 t2.
3991 ll = LAPPEND p (e ::: s) /\ LFINITE p /\
3992 (!e0. e0 IN LSET p ==> f e0 = [||]) /\
3993 t = LAPPEND t1 t2 /\
3994 f e = h:::t1 /\
3995 lbind s f = t2
3996Proof
3997 reverse eq_tac >> rpt strip_tac
3998 >- (simp[lbind_APPEND] >> ‘lbind p f = LNIL’ by simp[lbind_EQ_NIL] >>
3999 simp[]) >>
4000 gvs[lbind_def, LFLATTEN_EQ_CONS, LMAP_EQ_APPEND_FINITE1, LMAP_EQ_CONS] >>
4001 rpt $ irule_at Any EQ_REFL >> simp[] >>
4002 gs[every_LNTH, PULL_EXISTS, LSET_def, IN_DEF]
4003QED
4004
4005Theorem LSET_exists:
4006 x IN LSET ll <=> exists ($= x) ll
4007Proof
4008 simp[IN_DEF, LSET_def, exists_LNTH] >> metis_tac[]
4009QED
4010
4011Theorem exists_APPEND:
4012 !l1 l2. exists P (LAPPEND l1 l2) <=> exists P l1 \/ LFINITE l1 /\ exists P l2
4013Proof
4014 simp[EQ_IMP_THM, FORALL_AND_THM, DISJ_IMP_THM] >> rpt conj_tac >~
4015 [‘exists _ (LAPPEND _ _) ==> _’]
4016 >- (Induct_on‘exists’ >> rw[] >> rename [‘LAPPEND l1 l2 = h:::t’] >>
4017 Cases_on ‘l1’ >> gvs[] >> metis_tac[]) >~
4018 [‘exists _ _ ==> _’]
4019 >- (Induct_on ‘exists’ >> simp[]) >>
4020 Induct_on ‘LFINITE’ >> simp[]
4021QED
4022
4023Theorem LAPPEND11_FINITE1:
4024 !l1 l2 l3. LFINITE l1 ==> (LAPPEND l1 l2 = LAPPEND l1 l3 <=> l2 = l3)
4025Proof
4026 Induct_on ‘LFINITE’ >> simp[]
4027QED
4028
4029Theorem every_APPEND_EQN:
4030 every P (LAPPEND l1 l2) <=> every P l1 /\ (LFINITE l1 ==> every P l2)
4031Proof
4032 reverse $ Cases_on ‘LFINITE l1’ >> simp[NOT_LFINITE_APPEND] >>
4033 pop_assum mp_tac >> Induct_on ‘LFINITE’ >> simp[] >> metis_tac[]
4034QED
4035
4036Theorem exists_FLATTEN:
4037 exists P (LFLATTEN ll) <=>
4038 ?p e0 s.
4039 LFINITE p /\ every LFINITE p /\ ll = LAPPEND p (e0:::s) /\ exists P e0
4040Proof
4041 eq_tac
4042 >- (qid_spec_tac ‘ll’ >> Induct_on ‘exists’ >> rw[] >>
4043 gvs[LFLATTEN_EQ_CONS, exists_APPEND] >> dsimp[] >~
4044 [‘exists P (LFLATTEN t2)’, ‘LFLATTEN _ = LAPPEND t1 (LFLATTEN t2)’]
4045 >- (first_x_assum $ qspec_then ‘t1:::t2’ mp_tac >> simp[] >> rw[] >>
4046 rename [‘t1:::t2 = LAPPEND p0 (e0:::s)’,
4047 ‘LAPPEND p ((h:::t1):::t2)’] >>
4048 Cases_on ‘p0’ >> gvs[]
4049 >- (irule_at Any EQ_REFL >> simp[] >> irule MONO_every >>
4050 first_assum $ irule_at Any >> simp[]) >>
4051 rename [‘LAPPEND p ((h:::hl) ::: LAPPEND t (e0:::s))’] >>
4052 qexists ‘LAPPEND p ((h:::hl) ::: t)’ >>
4053 simp[LAPPEND11_FINITE1, LAPPEND_ASSOC,
4054 every_APPEND_EQN] >> irule MONO_every >>
4055 first_assum $ irule_at Any >> simp[]) >>
4056 irule_at Any EQ_REFL >> simp[] >> irule MONO_every >>
4057 first_assum $ irule_at Any >> simp[]) >>
4058 simp[PULL_EXISTS, LFLATTEN_APPEND_FINITE1, exists_APPEND, LFINITE_LFLATTEN,
4059 LFINITE_LFILTER]
4060QED
4061
4062Theorem LSET_FLATTEN:
4063 LSET $ LFLATTEN ll = { e | ?p e0 s. ll = LAPPEND p (e0:::s) /\ e IN LSET e0 /\
4064 LFINITE p /\ every LFINITE p }
4065Proof
4066 simp[LSET_exists, EXTENSION, exists_FLATTEN] >> metis_tac[]
4067QED
4068
4069Theorem every_LMAP:
4070 every P (LMAP f l) <=> every (P o f) l
4071Proof
4072 eq_tac
4073 >- (qid_spec_tac ‘l’ >> ho_match_mp_tac every_coind >> simp[]) >>
4074 ‘!l. (?l0. l = LMAP f l0 /\ every (P o f) l0) ==> every P l’
4075 suffices_by simp[PULL_EXISTS] >>
4076 ho_match_mp_tac every_coind >> simp[LMAP_EQ_CONS, PULL_EXISTS] >>
4077 metis_tac[]
4078QED
4079
4080Theorem LSET_lbind:
4081 LSET (lbind ll f) = { e | ?p e0 s. ll = LAPPEND p (e0:::s) /\
4082 LFINITE p /\ every (LFINITE o f) p /\
4083 e IN LSET $ f e0 }
4084Proof
4085 simp[EXTENSION,lbind_def, LSET_FLATTEN, SF CONJ_ss, LMAP_EQ_APPEND_FINITE1,
4086 PULL_EXISTS, LMAP_EQ_CONS, every_LMAP] >>
4087 metis_tac[]
4088QED
4089
4090Theorem LSET_APPEND:
4091 LSET (LAPPEND l1 l2) = LSET l1 UNION (if LFINITE l1 then LSET l2 else {})
4092Proof
4093 reverse $ Cases_on ‘LFINITE l1’ >> simp[NOT_LFINITE_APPEND] >>
4094 pop_assum mp_tac >> Induct_on ‘LFINITE’ >>
4095 simp[INSERT_UNION_EQ]
4096QED
4097
4098Theorem LSET_FINITE_pfx:
4099 x IN LSET ll <=> ?p s. ll = LAPPEND p (x:::s) /\ LFINITE p
4100Proof
4101 simp[EQ_IMP_THM, PULL_EXISTS, LSET_APPEND] >>
4102 simp[IN_DEF, LSET_def, PULL_EXISTS] >> qid_spec_tac ‘ll’ >> Induct_on ‘n’ >>
4103 Cases_on ‘ll’ >> simp[] >> strip_tac >- (qexists ‘LNIL’ >> simp[]) >>
4104 first_x_assum $ drule_then strip_assume_tac >> gvs[] >>
4105 rename [‘h:::(LAPPEND p _)’] >> qexists ‘h:::p’ >> simp[] >>
4106 metis_tac[]
4107QED
4108
4109Overload rpt_el = “λe. LGENLIST (K e) NONE”
4110
4111Theorem fromList_EQ_CONS:
4112 fromList l = h:::t <=> ?t0. l = h::t0 /\ t = fromList t0
4113Proof
4114 Cases_on ‘l’ >> simp[] >> metis_tac[]
4115QED
4116
4117Theorem GENLIST_EQ_CONS:
4118 GENLIST f n = h::t <=> 0 < n /\ f 0 = h /\ t = GENLIST (f o SUC) (n - 1)
4119Proof
4120 Cases_on ‘n’ >> simp[GENLIST_CONS] >> metis_tac[]
4121QED
4122
4123Theorem LGENLIST_SOME_EQ_CONS:
4124 LGENLIST f (SOME n) = h:::t <=>
4125 0 < n /\ f 0 = h /\ t = LGENLIST (f o SUC) (SOME (n - 1))
4126Proof
4127 simp[LGENLIST_EQ_fromList, fromList_EQ_CONS, GENLIST_EQ_CONS]
4128QED
4129
4130Theorem every_LGENLIST:
4131 (every P (LGENLIST f (SOME n)) <=> (!m. m < n ==> P (f m))) /\
4132 (every P (LGENLIST f NONE) <=> !m. P (f m))
4133Proof
4134 conj_tac >> eq_tac >~
4135 [‘_ ==> every P (LGENLIST f NONE)’]
4136 >- (‘!ll. (?f. ll = LGENLIST f NONE /\ !m. P (f m)) ==> every P ll’
4137 suffices_by metis_tac[]>>
4138 ho_match_mp_tac every_coind >>
4139 simp[LGENLIST_EQ_CONS, PULL_EXISTS] >> rw[] >>
4140 irule_at Any EQ_REFL >> simp[]) >~
4141 [‘_ ==> every _ _ ’]
4142 >- (‘!ll. (?f n. ll = LGENLIST f (SOME n) /\ !m. m < n ==> P (f m)) ==>
4143 every P ll’
4144 suffices_by metis_tac[] >>
4145 ho_match_mp_tac every_coind >> simp[LGENLIST_SOME_EQ_CONS, PULL_EXISTS] >>
4146 rpt strip_tac >> irule_at Any EQ_REFL >> simp[]) >~
4147 [‘every _ (LGENLIST f (SOME n))’]
4148 >- (map_every qid_spec_tac [‘f’, ‘n’] >> Induct >>
4149 simp[LT_SUC, DISJ_IMP_THM, FORALL_AND_THM, PULL_EXISTS] >>
4150 rpt strip_tac >> first_x_assum drule_all >> simp[]) >>
4151 CONV_TAC CONTRAPOS_CONV >> qid_spec_tac ‘f’ >>
4152 simp[GSYM every_def, PULL_EXISTS] >> CONV_TAC SWAP_FORALL_CONV >>
4153 Induct >> rpt strip_tac >>
4154 Cases_on ‘LGENLIST f NONE’ >> gvs[LGENLIST_EQ_CONS] >>
4155 first_x_assum $ drule_at Concl >> gs[ADD1]
4156QED
4157
4158Theorem rpt_el_CONS':
4159 e ::: rpt_el e = rpt_el e
4160Proof
4161 Cases_on ‘rpt_el e’ >> gs[LGENLIST_EQ_CONS]
4162QED
4163
4164Theorem rpt_el_EQ_APPEND:
4165 rpt_el e = LAPPEND l1 l2 <=>
4166 if LFINITE l1 then every ($= e) l1 /\ l2 = rpt_el e
4167 else l1 = rpt_el e
4168Proof
4169 reverse $ rw[NOT_LFINITE_APPEND] >- metis_tac[] >>
4170 pop_assum mp_tac >> Induct_on ‘LFINITE’ >> simp[] >> conj_tac
4171 >- metis_tac[] >>
4172 rpt strip_tac >> simp[Once $ GSYM rpt_el_CONS', SimpLHS] >> metis_tac[]
4173QED
4174
4175(*
4176Theorem LFLATTEN_rpt_el:
4177 LFLATTEN (rpt_el l) = if LFINITE l then LREPEAT (THE (toList l))
4178 else l
4179Proof
4180 Cases_on ‘LFINITE l’ >> simp[]
4181 >- (Cases_on ‘l = LNIL’ >> simp[toList_THM, LFLATTEN_EQ_NIL, every_LGENLIST]>>
4182 ONCE_REWRITE_TAC [LLIST_BISIMULATION] >>
4183 qexists ‘λl1 l2. ?l. LFINITE l /\ l1 = LFLATTEN (rpt_el l) /\
4184 l2 = LREPEAT (THE (toList l))’ >>
4185 rw[] >- (irule_at Any EQ_REFL >> simp[]) >>
4186 rename [‘LFLATTEN (rpt_el ll) = LNIL’] >>
4187 Cases_on ‘LFLATTEN (rpt_el ll)’ >> simp[]
4188 >- gvs[LFLATTEN_EQ_NIL, every_LGENLIST, toList_THM] >>
4189 simp[] >> gvs[LFLATTEN_EQ_CONS] >>
4190 Cases_on ‘ll = LNIL’
4191 >- (gvs[toList_THM, rpt_el_EQ_APPEND] >>
4192 gs[LGENLIST_EQ_CONS]) >>
4193 gvs[rpt_el_EQ_APPEND, LGENLIST_EQ_CONS] >>
4194 rename [‘every _ pfx’] >> Cases_on ‘pfx’ >> gvs[] >>
4195 simp[to_fromList] >> rename [‘LAPPEND ’
4196*)
4197
4198Theorem lbind_thm:
4199 lbind LNIL f = LNIL /\
4200 lbind (h:::t) f = LAPPEND (f h) $ lbind t f
4201Proof
4202 simp[lbind_def]
4203QED
4204
4205Theorem lbind_notASSOC:
4206 let f b = if b then rpt_el T else [|F|] ;
4207 g b = if b then LNIL else [| 1 |] ;
4208 bs = [|T; F|]
4209 in
4210 lbind bs (λb. lbind (f b) g) <> lbind (lbind bs f) g
4211Proof
4212 simp[lbind_def, NOT_LFINITE_APPEND] >>
4213 ‘LFLATTEN (rpt_el LNIL : num llist llist) = LNIL’ suffices_by simp[] >>
4214 simp[LFLATTEN_EQ_NIL, every_LGENLIST]
4215QED
4216
4217Theorem LPREFIX_LAPPEND_fromList:
4218 (LPREFIX (LAPPEND (fromList l) l1) (LAPPEND (fromList l) l2))
4219 <=> (LPREFIX l1 l2)
4220Proof
4221 fs[LPREFIX_APPEND]>>
4222 fs[Once LAPPEND_ASSOC]>>
4223 fs[LFINITE_fromList,LAPPEND11_FINITE1]>>metis_tac[]
4224QED