EncodeScript.sml
1Theory Encode
2Ancestors
3 pair combin arithmetic list rich_list option
4Libs
5 pairTools metisLib
6
7val arith_ss = old_arith_ss
8
9val Suff = Q_TAC SUFF_TAC;
10val Know = Q_TAC KNOW_TAC;
11
12val REVERSE = Tactical.REVERSE;
13
14val TOP_CASE_TAC = BasicProvers.TOP_CASE_TAC;
15
16(*---------------------------------------------------------------------------
17 biprefix is a bi-directional version of IS_PREFIX.
18 ---------------------------------------------------------------------------*)
19
20Definition biprefix_def:
21 biprefix a b <=> IS_PREFIX a b \/ IS_PREFIX b a
22End
23
24Theorem biprefix_refl:
25 !x. biprefix x x
26Proof
27 RW_TAC std_ss [biprefix_def, IS_PREFIX_REFL]
28QED
29
30Theorem biprefix_sym:
31 !x y. biprefix x y ==> biprefix y x
32Proof
33 PROVE_TAC [biprefix_def]
34QED
35
36Theorem biprefix_append:
37 !a b c d. biprefix (APPEND a b) (APPEND c d) ==> biprefix a c
38Proof
39 RW_TAC std_ss [biprefix_def] >>
40 PROVE_TAC [IS_PREFIX_APPEND1, IS_PREFIX_APPEND2]
41QED
42
43Theorem biprefix_cons:
44 !a b c d. biprefix (a :: b) (c :: d) <=> (a = c) /\ biprefix b d
45Proof
46 RW_TAC std_ss [biprefix_def, IS_PREFIX] >>
47 PROVE_TAC []
48QED
49
50Theorem biprefix_appends:
51 !a b c. biprefix (APPEND a b) (APPEND a c) = biprefix b c
52Proof
53 RW_TAC std_ss [biprefix_def, IS_PREFIX_APPENDS]
54QED
55
56(*---------------------------------------------------------------------------
57 An always true predicate for total encodings.
58 ---------------------------------------------------------------------------*)
59
60(*
61local
62 val th =prove (``?p. !x. p x``, Q.EXISTS_TAC `\x. T` >> RW_TAC std_ss []);
63in
64 val total_def = new_specification ("total_def", ["total"], th);
65end;
66
67val every_total = store_thm
68 ("every_total",
69 ``EVERY total = total``,
70 MATCH_MP_TAC EQ_EXT >>
71 Induct >>
72 RW_TAC std_ss [EVERY_DEF, total_def]);
73
74val lift_prod_total = store_thm
75 ("lift_prod_total",
76 ``lift_prod total total = total``,
77 MATCH_MP_TAC EQ_EXT >>
78 RW_TAC std_ss [lift_prod_def, total_def]);
79
80val lift_sum_total = store_thm
81 ("lift_sum_total",
82 ``lift_sum total total = total``,
83 MATCH_MP_TAC EQ_EXT >>
84 RW_TAC std_ss [lift_sum_def, total_def] >>
85 TOP_CASE_TAC);
86
87val lift_option_total = store_thm
88 ("lift_option_total",
89 ``lift_option total = total``,
90 MATCH_MP_TAC EQ_EXT >>
91 RW_TAC std_ss [lift_option_def, total_def] >>
92 TOP_CASE_TAC);
93
94val lift_tree_total = store_thm
95 ("lift_tree_total",
96 ``lift_tree total = total``,
97 MATCH_MP_TAC EQ_EXT >>
98 HO_MATCH_MP_TAC tree_ind >>
99 RW_TAC std_ss [lift_tree_def, total_def] >>
100 CONV_TAC (DEPTH_CONV ETA_CONV) >>
101 RW_TAC std_ss [EVERY_MEM]);
102*)
103
104(*---------------------------------------------------------------------------
105 Well-formed predicates are non-empty.
106 ---------------------------------------------------------------------------*)
107
108Definition wf_pred_def:
109 wf_pred p = ?x. p x
110End
111
112(*---------------------------------------------------------------------------
113 A well-formed encoder is prefix-free and injective.
114 ---------------------------------------------------------------------------*)
115
116Definition wf_encoder_def:
117 wf_encoder p (e : 'a -> bool list) =
118 !x y. p x /\ p y /\ IS_PREFIX (e x) (e y) ==> (x = y)
119End
120
121Theorem wf_encoder_alt:
122 wf_encoder p (e : 'a -> bool list) =
123 !x y. p x /\ p y /\ biprefix (e x) (e y) ==> (x = y)
124Proof
125 PROVE_TAC [wf_encoder_def, biprefix_def]
126QED
127
128Theorem wf_encoder_eq:
129 !p e f. wf_encoder p e /\ (!x. p x ==> (e x = f x)) ==> wf_encoder p f
130Proof
131 RW_TAC std_ss [wf_encoder_def]
132QED
133
134Theorem wf_encoder_total:
135 !p e. wf_encoder (K T) e ==> wf_encoder p e
136Proof
137 RW_TAC std_ss [wf_encoder_def, wf_encoder_def, K_THM]
138QED
139
140(*---------------------------------------------------------------------------
141 The unit type is cool because it consumes no space in the
142 target list: the type has all the information!
143 ---------------------------------------------------------------------------*)
144
145Definition encode_unit_def:
146 encode_unit (_ : one) : bool list = []
147End
148
149Theorem wf_encode_unit:
150 !p. wf_encoder p encode_unit
151Proof
152 RW_TAC std_ss [wf_encoder_def, encode_unit_def, IS_PREFIX, oneTheory.one]
153QED
154
155(*---------------------------------------------------------------------------
156 Booleans
157 ---------------------------------------------------------------------------*)
158
159Definition encode_bool_def:
160 encode_bool (x : bool) = [x]
161End
162
163Theorem wf_encode_bool:
164 !p. wf_encoder p encode_bool
165Proof
166 RW_TAC std_ss [wf_encoder_def, encode_bool_def, IS_PREFIX]
167QED
168
169(*---------------------------------------------------------------------------
170 Pairs
171 ---------------------------------------------------------------------------*)
172
173Definition encode_prod_def:
174 encode_prod xb yb (x : 'a, y : 'b) : bool list = APPEND (xb x) (yb y)
175End
176
177Definition lift_prod_def:
178 lift_prod p1 p2 x <=> p1 (FST x) /\ p2 (SND x)
179End
180
181Theorem encode_prod_alt:
182 !xb yb p. encode_prod xb yb p = APPEND (xb (FST p)) (yb (SND p))
183Proof
184 GEN_TAC >> GEN_TAC >> Cases >>
185 RW_TAC std_ss [encode_prod_def]
186QED
187
188Theorem wf_encode_prod:
189 !p1 p2 e1 e2.
190 wf_encoder p1 e1 /\ wf_encoder p2 e2 ==>
191 wf_encoder (lift_prod p1 p2) (encode_prod e1 e2)
192Proof
193 RW_TAC std_ss [wf_encoder_def, encode_prod_alt, lift_prod_def] >>
194 Cases_on `x` >>
195 Cases_on `y` >>
196 FULL_SIMP_TAC std_ss [] >>
197 Suff `q = q'` >- PROVE_TAC [IS_PREFIX_APPENDS] >>
198 PROVE_TAC [IS_PREFIX_APPEND1, IS_PREFIX_APPEND2]
199QED
200
201(*---------------------------------------------------------------------------
202 Sums
203 ---------------------------------------------------------------------------*)
204
205Definition encode_sum_def:
206 (encode_sum xb yb (INL (x : 'a)) : bool list = T :: xb x) /\
207 (encode_sum xb yb (INR (y : 'b)) = F :: yb y)
208End
209
210Definition lift_sum_def:
211 lift_sum (p1 : 'a->bool) p2 x =
212 case x of INL x1 => p1 x1 | INR x2 => p2 x2
213End
214
215Theorem wf_encode_sum:
216 !p1 p2 e1 e2.
217 wf_encoder p1 e1 /\ wf_encoder p2 e2 ==>
218 wf_encoder (lift_sum p1 p2) (encode_sum e1 e2)
219Proof
220 RW_TAC std_ss [wf_encoder_def, lift_sum_def] >>
221 Cases_on `x` >>
222 Cases_on `y` >>
223 FULL_SIMP_TAC std_ss [encode_sum_def, IS_PREFIX]
224QED
225
226(*---------------------------------------------------------------------------
227 Options
228 ---------------------------------------------------------------------------*)
229
230Definition encode_option_def:
231 encode_option xb NONE = [F] /\
232 encode_option xb (SOME x) = T :: xb x
233End
234
235Definition lift_option_def:
236 lift_option p x = case x of NONE => T | SOME y => p y
237End
238
239Theorem wf_encode_option:
240 !p e. wf_encoder p e ==> wf_encoder (lift_option p) (encode_option e)
241Proof
242 RW_TAC std_ss [wf_encoder_def, lift_option_def] >>
243 Cases_on `x` >>
244 Cases_on `y` >>
245 FULL_SIMP_TAC std_ss [encode_option_def, IS_PREFIX]
246QED
247
248(*---------------------------------------------------------------------------
249 Lists
250 ---------------------------------------------------------------------------*)
251
252Definition encode_list_def:
253 (encode_list xb [] = [F]) /\
254 (encode_list xb (x :: xs) = T :: APPEND (xb x) (encode_list xb xs))
255End
256
257Theorem wf_encode_list:
258 !p e. wf_encoder p e ==> wf_encoder (EVERY p) (encode_list e)
259Proof
260 RW_TAC std_ss [wf_encoder_def] >>
261 POP_ASSUM MP_TAC >>
262 POP_ASSUM MP_TAC >>
263 POP_ASSUM MP_TAC >>
264 Q.SPEC_TAC (`y`, `y`) >>
265 Q.SPEC_TAC (`x`, `x`) >>
266 Induct >-
267 (Cases >>
268 RW_TAC std_ss [IS_PREFIX, encode_list_def]) >>
269 GEN_TAC >>
270 Cases >- RW_TAC std_ss [IS_PREFIX, encode_list_def] >>
271 SIMP_TAC std_ss [encode_list_def, IS_PREFIX, EVERY_DEF] >>
272 STRIP_TAC >>
273 STRIP_TAC >>
274 STRIP_TAC >>
275 Suff `h = h'` >- PROVE_TAC [IS_PREFIX_APPENDS] >>
276 PROVE_TAC [IS_PREFIX_APPEND1, IS_PREFIX_APPEND2]
277QED
278
279(* A congruence rule *)
280
281Theorem encode_list_cong[defncong]:
282 !l1 l2 f1 f2.
283 (l1=l2) /\ (!x. MEM x l2 ==> (f1 x = f2 x))
284 ==>
285 (encode_list f1 l1 = encode_list f2 l2)
286Proof
287 Induct >>
288 SIMP_TAC list_ss [MEM,encode_list_def] >>
289 RW_TAC list_ss []
290QED
291
292(*---------------------------------------------------------------------------
293 Bounded lists
294 ---------------------------------------------------------------------------*)
295
296Definition encode_blist_def:
297 (encode_blist 0 e l = []) /\
298 (encode_blist (SUC m) e l = APPEND (e (HD l)) (encode_blist m e (TL l)))
299End
300
301Definition lift_blist_def:
302 lift_blist m p x <=> EVERY p x /\ (LENGTH x = m)
303End
304
305Theorem lift_blist_suc:
306 !n p h t. lift_blist (SUC n) p (h :: t) <=> p h /\ lift_blist n p t
307Proof
308 RW_TAC std_ss [lift_blist_def, EVERY_DEF, LENGTH, CONJ_ASSOC]
309QED
310
311Theorem wf_encode_blist:
312 !m p e.
313 wf_encoder p e ==> wf_encoder (lift_blist m p) (encode_blist m e)
314Proof
315 RW_TAC std_ss [wf_encoder_alt, lift_blist_def]
316 >> NTAC 4 (POP_ASSUM MP_TAC)
317 >> REWRITE_TAC [AND_IMP_INTRO]
318 >> Q.SPEC_TAC (`y`, `y`)
319 >> Q.SPEC_TAC (`x`, `x`)
320 >> (Induct_on `x` >> Cases_on `y` >> FULL_SIMP_TAC std_ss [LENGTH, SUC_NOT])
321 >> SIMP_TAC std_ss [EVERY_DEF, prim_recTheory.INV_SUC_EQ,
322 encode_blist_def, HD, TL]
323 >> REPEAT STRIP_TAC
324 >> Suff `h = h'`
325 >- (RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [biprefix_appends])
326 >> Q.PAT_X_ASSUM `!y. P y` (K ALL_TAC)
327 >> Q.PAT_X_ASSUM `!x. P x` MATCH_MP_TAC
328 >> RW_TAC std_ss []
329 >> MATCH_MP_TAC biprefix_append
330 >> PROVE_TAC [biprefix_sym]
331QED
332
333(*---------------------------------------------------------------------------
334 Nums (Norrish numeral encoding)
335 ---------------------------------------------------------------------------*)
336
337Definition encode_num_def:
338 encode_num (n:num) =
339 if n = 0 then [T; T]
340 else if EVEN n then F :: encode_num ((n - 2) DIV 2)
341 else T :: F :: encode_num ((n - 1) DIV 2)
342Termination
343 WF_REL_TAC ‘$<’ >> simp[DIV_LT_X]
344End
345
346val encode_num_def = SPEC_ALL encode_num_def
347
348Theorem wf_encode_num:
349 !p. wf_encoder p encode_num
350Proof
351 MATCH_MP_TAC wf_encoder_total >>
352 SIMP_TAC std_ss [wf_encoder_def, K_THM] >>
353 recInduct encode_num_ind >>
354 GEN_TAC >>
355 Cases_on `n = 0` >-
356 (POP_ASSUM SUBST1_TAC >>
357 SIMP_TAC std_ss [REWRITE_RULE [] (Q.INST [`n` |-> `0`] encode_num_def)] >>
358 ONCE_REWRITE_TAC [encode_num_def] >>
359 RW_TAC std_ss [IS_PREFIX]) >>
360 ASM_REWRITE_TAC [] >>
361 MP_TAC encode_num_def >>
362 (DISCH_THEN (fn th => RW_TAC std_ss [th]) >>
363 POP_ASSUM MP_TAC >>
364 Q.SPEC_TAC (`y`, `y`) >>
365 recInduct encode_num_ind >>
366 GEN_TAC >>
367 MP_TAC (Q.INST [`n` |-> `n'`] encode_num_def) >>
368 RW_TAC std_ss [IS_PREFIX] >>
369 RES_TAC) >|
370 [Cases_on `n` >- RW_TAC std_ss [] >>
371 Cases_on `n''` >- FULL_SIMP_TAC std_ss [EVEN] >>
372 FULL_SIMP_TAC arith_ss [EVEN] >>
373 Q.PAT_X_ASSUM `EVEN n` MP_TAC >>
374 RW_TAC std_ss [EVEN_EXISTS] >>
375 Cases_on `n'` >- RW_TAC std_ss [] >>
376 Cases_on `n` >- FULL_SIMP_TAC std_ss [EVEN] >>
377 FULL_SIMP_TAC arith_ss [EVEN] >>
378 Q.PAT_X_ASSUM `EVEN n'` MP_TAC >>
379 RW_TAC std_ss [EVEN_EXISTS] >>
380 POP_ASSUM MP_TAC >>
381 POP_ASSUM_LIST (K ALL_TAC) >>
382 Know `!m : num. SUC (SUC m) - 2 = m` >- DECIDE_TAC >>
383 DISCH_THEN (fn th => REWRITE_TAC [th]) >>
384 ONCE_REWRITE_TAC [MULT_COMM] >>
385 RW_TAC arith_ss [MULT_DIV],
386 Cases_on `n` >- RW_TAC std_ss [] >>
387 FULL_SIMP_TAC arith_ss [EVEN] >>
388 Q.PAT_X_ASSUM `EVEN n''` MP_TAC >>
389 RW_TAC std_ss [EVEN_EXISTS] >>
390 Cases_on `n'` >- RW_TAC std_ss [] >>
391 FULL_SIMP_TAC arith_ss [EVEN] >>
392 Q.PAT_X_ASSUM `EVEN n` MP_TAC >>
393 RW_TAC std_ss [EVEN_EXISTS] >>
394 POP_ASSUM MP_TAC >>
395 POP_ASSUM_LIST (K ALL_TAC) >>
396 ONCE_REWRITE_TAC [MULT_COMM] >>
397 RW_TAC arith_ss [MULT_DIV]]
398QED
399
400(*---------------------------------------------------------------------------
401 Bounded numbers (bit encoding)
402 ---------------------------------------------------------------------------*)
403
404Definition encode_bnum_def:
405 (encode_bnum 0 (n : num) = []) /\
406 (encode_bnum (SUC m) n = ~(EVEN n) :: encode_bnum m (n DIV 2))
407End
408
409Definition collision_free_def:
410 collision_free m p =
411 !x y. p x /\ p y /\ (x MOD (2 EXP m) = y MOD (2 EXP m)) ==> (x = y)
412End
413
414Definition wf_pred_bnum_def:
415 wf_pred_bnum m p <=> wf_pred p /\ !x. p x ==> x < 2 ** m
416End
417
418Theorem wf_pred_bnum_total:
419 !m. wf_pred_bnum m (\x. x < 2 ** m)
420Proof
421 RW_TAC std_ss [wf_pred_bnum_def, wf_pred_def]
422 >> Q.EXISTS_TAC `0`
423 >> REWRITE_TAC [ZERO_LESS_EXP, TWO]
424QED
425
426Theorem wf_pred_bnum:
427 !m p. wf_pred_bnum m p ==> collision_free m p
428Proof
429 RW_TAC std_ss [wf_pred_bnum_def, collision_free_def]
430 >> POP_ASSUM MP_TAC
431 >> RW_TAC arith_ss [LESS_MOD]
432QED
433
434Theorem encode_bnum_length:
435 !m n. LENGTH (encode_bnum m n) = m
436Proof
437 Induct
438 >> RW_TAC std_ss [LENGTH, encode_bnum_def]
439QED
440
441Theorem encode_bnum_inj:
442 !m x y.
443 x < 2 ** m /\ y < 2 ** m /\ encode_bnum m x = encode_bnum m y ==>
444 x = y
445Proof
446 Induct >> rw[encode_bnum_def] >>
447 first_x_assum $ drule_at Any >> simp[] >>
448 Q.PAT_X_ASSUM `EVEN x = Y` MP_TAC
449 >> POP_ASSUM_LIST (K ALL_TAC)
450 >> RW_TAC std_ss []
451 >> MP_TAC (MP (Q.SPEC `2` DIVISION) (DECIDE ``0 < 2``))
452 >> DISCH_THEN (fn th => ONCE_REWRITE_TAC [th])
453 >> RW_TAC std_ss [MOD_2]
454QED
455
456Theorem wf_encode_bnum_collision_free:
457 !m p. wf_encoder p (encode_bnum m) = collision_free m p
458Proof
459 RW_TAC std_ss [collision_free_def, wf_encoder_def]
460 >> HO_MATCH_MP_TAC
461 (PROVE []
462 “(!x y. p x /\ p y ==> (Q x y = R x y)) ==>
463 ((!x y. p x /\ p y /\ Q x y ==> P x y) <=>
464 (!x y. p x /\ p y /\ R x y ==> P x y))”)
465 >> RW_TAC std_ss []
466 >> MP_TAC
467 (Q.SPECL [`encode_bnum m y`, `encode_bnum m x`]
468 (INST_TYPE [alpha |-> bool] IS_PREFIX_LENGTH_ANTI))
469 >> RW_TAC std_ss [encode_bnum_length]
470 >> POP_ASSUM_LIST (K ALL_TAC)
471 >> Q.SPEC_TAC (`y`, `y`)
472 >> Q.SPEC_TAC (`x`, `x`)
473 >> Q.SPEC_TAC (`m`, `m`)
474 >> Induct
475 >> RW_TAC std_ss [encode_bnum_def, EXP, MOD_1]
476 >> POP_ASSUM (K ALL_TAC)
477 >> MP_TAC (Q.SPEC `2` DIVISION)
478 >> SIMP_TAC arith_ss []
479 >> DISCH_THEN (fn th => MP_TAC (CONJ (Q.SPEC `x` th) (Q.SPEC `y` th)))
480 >> DISCH_THEN (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [th])))
481 >> Know `!n. (n MOD 2 = 0) \/ (n MOD 2 = 1)`
482 >- (STRIP_TAC
483 >> Suff `n MOD 2 < 2` >- DECIDE_TAC
484 >> RW_TAC arith_ss [DIVISION])
485 >> STRIP_TAC
486 >> Know `(EVEN y = EVEN x) <=> (x MOD 2 = y MOD 2)`
487 >- (RW_TAC std_ss [EVEN_MOD2]
488 >> POP_ASSUM (fn th => MP_TAC (CONJ (Q.SPEC `x` th) (Q.SPEC `y` th)))
489 >> STRIP_TAC
490 >> ASM_REWRITE_TAC []
491 >> METIS_TAC [])
492 >> DISCH_THEN (fn th => REWRITE_TAC [th])
493 >> MATCH_MP_TAC (PROVE [] ``(R ==> P) /\ (P ==> (Q = R)) ==> (P /\ Q <=> R)``)
494 >> CONJ_TAC
495 >- (RW_TAC std_ss []
496 >> Suff `?m n. (m * 2 + x MOD 2) MOD 2 = (n * 2 + y MOD 2) MOD 2`
497 >- (RW_TAC std_ss []
498 >> POP_ASSUM MP_TAC
499 >> MP_TAC (Q.SPEC `2` MOD_PLUS)
500 >> SIMP_TAC arith_ss []
501 >> DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th])
502 >> RW_TAC arith_ss [MOD_EQ_0, MOD_MOD])
503 >> Suff `0 < 2 /\ 0 < 2 ** m` >- PROVE_TAC [MOD_MULT_MOD, MULT_COMM]
504 >> REWRITE_TAC [ZERO_LESS_EXP, TWO]
505 >> DECIDE_TAC)
506 >> DISCH_THEN (fn th => REWRITE_TAC [th])
507 >> Suff `((x DIV 2) MOD 2 ** m = (y DIV 2) MOD 2 ** m) =
508 ((x DIV 2 * 2) MOD (2 * 2 ** m) =
509 (y DIV 2 * 2) MOD (2 * 2 ** m))`
510 >- (POP_ASSUM (MP_TAC o Q.SPEC `y`)
511 >> STRIP_TAC
512 >> RW_TAC arith_ss [GSYM ADD1]
513 >> POP_ASSUM MP_TAC
514 >> MP_TAC (Q.SPEC `2 * 2 ** m` SUC_MOD)
515 >> Suff `0 < 2 * 2 ** m` >- RW_TAC std_ss []
516 >> REWRITE_TAC [GSYM EXP, ZERO_LESS_EXP, TWO])
517 >> REWRITE_TAC [GSYM EXP]
518 >> ONCE_REWRITE_TAC [MULT_COMM]
519 >> REWRITE_TAC [EXP, TWO]
520 >> RW_TAC arith_ss [GSYM MOD_COMMON_FACTOR, ZERO_LESS_EXP]
521QED
522
523Theorem wf_encode_bnum:
524 !m p. wf_pred_bnum m p ==> wf_encoder p (encode_bnum m)
525Proof
526 PROVE_TAC [wf_encode_bnum_collision_free, wf_pred_bnum]
527QED
528
529(*---------------------------------------------------------------------------
530 Datatype of polymorphic n-ary trees.
531
532 A challenging example for boolification.
533 ---------------------------------------------------------------------------*)
534
535Datatype:
536 tree = Node 'a (tree list)
537End
538
539Definition encode_tree_def:
540 encode_tree e (Node a ts) = (e a) ++ encode_list (encode_tree e) ts
541End
542
543Definition lift_tree_def:
544 lift_tree p (Node a ts) <=> p a /\ EVERY (lift_tree p) ts
545End
546
547Theorem encode_tree_def[allow_rebind] =
548 CONV_RULE (DEPTH_CONV ETA_CONV) encode_tree_def
549
550Theorem lift_tree_def[allow_rebind] =
551 CONV_RULE (DEPTH_CONV ETA_CONV) lift_tree_def;
552
553
554val tree_induction = fetch "-" "tree_induction";
555
556Theorem tree_ind:
557 !p. (!a ts. (!t. MEM t ts ==> p t) ==> p (Node a ts)) ==> (!t. p t)
558Proof
559 GEN_TAC
560 >> REPEAT DISCH_TAC
561 >> Suff `(!t. p t) /\ (!l : 'a tree list. EVERY p l)` >- PROVE_TAC []
562 >> HO_MATCH_MP_TAC tree_induction
563 >> RW_TAC std_ss [EVERY_DEF]
564 >> Q.PAT_X_ASSUM `!x. Q x` MATCH_MP_TAC
565 >> FULL_SIMP_TAC std_ss [EVERY_MEM]
566QED
567
568Theorem wf_encode_tree:
569 !p e. wf_encoder p e ==> wf_encoder (lift_tree p) (encode_tree e)
570Proof
571 RW_TAC std_ss [] >>
572 SIMP_TAC std_ss [wf_encoder_alt] >>
573 HO_MATCH_MP_TAC tree_ind >>
574 REPEAT GEN_TAC >>
575 REPEAT DISCH_TAC >>
576 Cases >>
577 SIMP_TAC std_ss [lift_tree_def, encode_tree_def] >>
578 REPEAT STRIP_TAC >>
579 Know `a = a'` >- PROVE_TAC [biprefix_append, wf_encoder_alt] >>
580 RW_TAC std_ss [] >>
581 FULL_SIMP_TAC std_ss [biprefix_appends] >>
582 POP_ASSUM MP_TAC >>
583 POP_ASSUM MP_TAC >>
584 POP_ASSUM (K ALL_TAC) >>
585 POP_ASSUM MP_TAC >>
586 POP_ASSUM (K ALL_TAC) >>
587 CONV_TAC (DEPTH_CONV ETA_CONV) >>
588 POP_ASSUM MP_TAC >>
589 Q.SPEC_TAC (`ts`, `z`) >>
590 Q.SPEC_TAC (`l`, `y`) >>
591 Induct >-
592 (Cases >> RW_TAC std_ss [IS_PREFIX, encode_list_def, biprefix_def]) >>
593 GEN_TAC >>
594 Cases >- RW_TAC std_ss [IS_PREFIX, encode_list_def, biprefix_def] >>
595 SIMP_TAC std_ss [encode_list_def, EVERY_DEF, biprefix_cons] >>
596 REPEAT STRIP_TAC >>
597 Know `h = h'` >-
598 (Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `h'`) >>
599 Q.PAT_X_ASSUM `!x. P x` (K ALL_TAC) >>
600 RW_TAC std_ss [MEM] >>
601 MATCH_MP_TAC EQ_SYM >>
602 POP_ASSUM MATCH_MP_TAC >>
603 RW_TAC std_ss [] >>
604 PROVE_TAC [biprefix_append]) >>
605 RW_TAC std_ss [] >>
606 Q.PAT_X_ASSUM `!z. (!x. P x z) ==> Q z`
607 (MATCH_MP_TAC o REWRITE_RULE [AND_IMP_INTRO]) >>
608 PROVE_TAC [MEM, biprefix_appends]
609QED
610