DecodeScript.sml
1(*==========================================================================*)
2(* Defining Decoders to be inverse Encoders *)
3(*==========================================================================*)
4
5(* Interactive mode
6app load
7["bossLib", "rich_listTheory", "EncodeTheory", "normalForms", "metisLib"];
8*)
9Theory Decode
10Ancestors
11 pair arithmetic list rich_list Encode option combin
12Libs
13 pairTools metisLib normalForms
14
15
16val arith_ss = old_arith_ss
17
18val Suff = Q_TAC SUFF_TAC;
19val Know = Q_TAC KNOW_TAC;
20val std_ss = std_ss -* ["lift_disj_eq", "lift_imp_disj"]
21val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
22
23val REVERSE = Tactical.REVERSE;
24
25val TOP_CASE_TAC = BasicProvers.TOP_CASE_TAC;
26
27(*---------------------------------------------------------------------------
28 Well-formed decoders: the definition is carefully chosen to be the
29 dual of well-formed encoders.
30 ---------------------------------------------------------------------------*)
31
32Definition wf_decoder_def:
33 wf_decoder p (d : bool list -> ('a # bool list) option) =
34 !x.
35 if p x then (?a. !b c. (d b = SOME (x, c)) = (b = APPEND a c))
36 else !a b. ~(d a = SOME (x, b))
37End
38
39(*---------------------------------------------------------------------------
40 Functions to transform well-formed encoders to well-formed decoders,
41 and vice versa.
42 ---------------------------------------------------------------------------*)
43
44Definition enc2dec_def:
45 enc2dec p e (l : bool list) =
46 if ?x t. p (x : 'a) /\ (l = APPEND (e x) t)
47 then SOME (@(x, t). p x /\ (l = APPEND (e x) t))
48 else NONE
49End
50
51Definition dec2enc_def:
52 dec2enc (d : bool list -> ('a # bool list) option) x =
53 @l. d l = SOME (x, [])
54End
55
56(*---------------------------------------------------------------------------
57 Proofs that the transformation functions are mutually inverse.
58 ---------------------------------------------------------------------------*)
59
60Theorem enc2dec_none:
61 !p e l. (enc2dec p e l = NONE) = (!x t. p x ==> ~(l = APPEND (e x) t))
62Proof
63 RW_TAC std_ss [enc2dec_def] >>
64 PROVE_TAC []
65QED
66
67Theorem enc2dec_some:
68 !p e l x t.
69 wf_encoder p e ==>
70 ((enc2dec p e l = SOME (x, t)) <=> p x /\ (l = APPEND (e x) t))
71Proof
72 REPEAT STRIP_TAC THEN SRW_TAC [][enc2dec_def] THEN
73 Cases_on `?y tt. p y /\ (l = e y ++ tt)` THENL [
74 SRW_TAC [][ELIM_UNCURRY] THEN SELECT_ELIM_TAC THEN
75 CONJ_TAC THEN1 (Q.EXISTS_TAC `(y,tt)` THEN SRW_TAC [][]) THEN
76 SIMP_TAC (srw_ss()) [FORALL_PROD] THEN
77 MAP_EVERY Q.X_GEN_TAC [`z`, `uu`] THEN
78 STRIP_TAC THEN EQ_TAC THEN1 (STRIP_TAC THEN SRW_TAC [][]) THEN
79 STRIP_TAC THEN
80 Q_TAC SUFF_TAC `e z <<= e x \/ e x <<= e z`
81 THEN1 METIS_TAC [APPEND_11, wf_encoder_def] THEN
82 METIS_TAC [IS_PREFIX_APPEND1, IS_PREFIX_APPEND2, IS_PREFIX_REFL],
83
84 ASM_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []
85 ]
86QED
87
88Theorem enc2dec_some_alt:
89 !p e l x.
90 wf_encoder p e ==>
91 ((enc2dec p e l = SOME x) <=>
92 p (FST x) /\ (l = APPEND (e (FST x)) (SND x)))
93Proof
94 RW_TAC std_ss []
95 >> Cases_on `x`
96 >> RW_TAC std_ss [FST, SND]
97 >> METIS_TAC [enc2dec_some]
98QED
99
100Theorem wf_enc2dec:
101 !p e. wf_encoder p e ==> wf_decoder p (enc2dec p e)
102Proof
103 RW_TAC std_ss [wf_decoder_def, enc2dec_some] >>
104 PROVE_TAC [APPEND_NIL]
105QED
106
107Theorem dec2enc_some:
108 !p d x l.
109 wf_decoder p d ==>
110 ((dec2enc d x = l) /\ p x <=> (d l = SOME (x, [])))
111Proof
112 RW_TAC std_ss [dec2enc_def] >>
113 SELECT_TAC >>
114 RW_TAC std_ss [] >>
115 EQ_TAC >-
116 (RW_TAC std_ss [] >>
117 Q.PAT_X_ASSUM `X ==> Y` MATCH_MP_TAC >>
118 FULL_SIMP_TAC std_ss [wf_decoder_def] >>
119 PROVE_TAC [APPEND_NIL]) >>
120 POP_ASSUM MP_TAC >>
121 MATCH_MP_TAC
122 (PROVE [] ``(z ==> x) /\ (y ==> z ==> t) ==> (x ==> y) ==> z ==> t``) >>
123 CONJ_TAC >- PROVE_TAC [] >>
124 POP_ASSUM MP_TAC >>
125 SIMP_TAC std_ss [wf_decoder_def] >>
126 DISCH_THEN (MP_TAC o Q.SPEC `x`) >>
127 REVERSE (Cases_on `p x`) >- PROVE_TAC [] >>
128 ASM_REWRITE_TAC [] >>
129 DISCH_THEN (CHOOSE_THEN MP_TAC) >>
130 RW_TAC std_ss []
131QED
132
133Theorem decode_dec2enc:
134 !p d x.
135 wf_decoder p d /\ p x ==> (d (dec2enc d x) = SOME (x, []))
136Proof
137 PROVE_TAC [dec2enc_some]
138QED
139
140Theorem decode_dec2enc_append:
141 !p d x t.
142 wf_decoder p d /\ p x ==>
143 (d (APPEND (dec2enc d x) t) = SOME (x, t))
144Proof
145 RW_TAC std_ss [] >>
146 MP_TAC (Q.SPECL [`p`, `d`, `x`] decode_dec2enc) >>
147 RW_TAC std_ss [] >>
148 FULL_SIMP_TAC std_ss [wf_decoder_def] >>
149 Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`) >>
150 RW_TAC std_ss [] >>
151 RW_TAC std_ss [] >>
152 RES_TAC >>
153 RW_TAC std_ss [APPEND_NIL]
154QED
155
156Theorem wf_dec2enc:
157 !p d. wf_decoder p d ==> wf_encoder p (dec2enc d)
158Proof
159 RW_TAC std_ss [wf_encoder_def] >>
160 MP_TAC (Q.SPECL [`p`, `d`] wf_decoder_def) >>
161 ASM_REWRITE_TAC [] >>
162 DISCH_THEN (fn th => MP_TAC (Q.SPEC `x` th) THEN MP_TAC (Q.SPEC `y` th)) >>
163 RW_TAC std_ss [] >>
164 MP_TAC (Q.SPECL [`p`, `d`, `x`] decode_dec2enc) >>
165 MP_TAC (Q.SPECL [`p`, `d`, `y`] decode_dec2enc) >>
166 RW_TAC std_ss [APPEND_NIL] >>
167 POP_ASSUM MP_TAC >>
168 POP_ASSUM MP_TAC >>
169 POP_ASSUM (CHOOSE_THEN MP_TAC o REWRITE_RULE [IS_PREFIX_APPEND]) >>
170 RW_TAC std_ss [GSYM APPEND_ASSOC] >>
171 POP_ASSUM (MP_TAC o Q.SPECL [`APPEND (dec2enc d y) l`, `[]`]) >>
172 POP_ASSUM (MP_TAC o Q.SPECL [`APPEND (dec2enc d y) l`, `l`]) >>
173 RW_TAC std_ss [APPEND_NIL]
174QED
175
176Theorem dec2enc_enc2dec:
177 !p e x. wf_encoder p e /\ p x ==> (dec2enc (enc2dec p e) x = e x)
178Proof
179 RW_TAC std_ss [] >>
180 MP_TAC (Q.SPECL [`p`, `e`] wf_enc2dec) >>
181 RW_TAC std_ss [dec2enc_some] >>
182 MP_TAC (Q.SPECL [`p`, `enc2dec p e`, `x`, `e x`] dec2enc_some) >>
183 RW_TAC std_ss [enc2dec_some, APPEND_NIL]
184QED
185
186Theorem enc2dec_dec2enc:
187 !p d. wf_decoder p d ==> (enc2dec p (dec2enc d) = d)
188Proof
189 RW_TAC std_ss [] >>
190 MATCH_MP_TAC EQ_EXT >>
191 Q.X_GEN_TAC `l` >>
192 MP_TAC (Q.SPECL [`p`, `d`] wf_dec2enc) >>
193 RW_TAC std_ss [] >>
194 Cases_on `d l` >|
195 [RW_TAC std_ss [enc2dec_none] >>
196 STRIP_TAC >>
197 RW_TAC std_ss [] >>
198 Q.PAT_X_ASSUM `X = Y` MP_TAC >>
199 PROVE_TAC [NOT_SOME_NONE, decode_dec2enc_append],
200 Cases_on `x` >>
201 ASM_SIMP_TAC std_ss [enc2dec_some] >>
202 MATCH_MP_TAC (PROVE [] ``x /\ (x ==> y) ==> x /\ y``) >>
203 RW_TAC std_ss [] >- PROVE_TAC [wf_decoder_def] >>
204 MP_TAC (Q.SPECL [`p`, `d`] wf_decoder_def) >>
205 ASM_REWRITE_TAC [] >>
206 DISCH_THEN (MP_TAC o Q.SPEC `q`) >>
207 RW_TAC std_ss [] >>
208 RES_TAC >>
209 RW_TAC std_ss [APPEND_11] >>
210 Suff `d a = SOME (q, [])` >- PROVE_TAC [dec2enc_some] >>
211 RW_TAC std_ss [APPEND_NIL]]
212QED
213
214(*---------------------------------------------------------------------------
215 Units
216 ---------------------------------------------------------------------------*)
217
218Definition decode_unit_def[nocompute]:
219 decode_unit p = enc2dec p encode_unit
220End
221
222Theorem wf_decode_unit:
223 wf_decoder p (decode_unit p)
224Proof
225 RW_TAC std_ss [decode_unit_def, wf_enc2dec, wf_encode_unit]
226QED
227
228Theorem dec2enc_decode_unit:
229 !p x. p x ==> (dec2enc (decode_unit p) x = encode_unit x)
230Proof
231 RW_TAC std_ss [decode_unit_def, dec2enc_enc2dec, wf_encode_unit]
232QED
233
234Theorem decode_unit:
235 decode_unit p l = if p () then SOME ((), l) else NONE
236Proof
237 RW_TAC std_ss
238 [decode_unit_def, enc2dec_none, enc2dec_some, encode_unit_def,
239 APPEND, wf_encode_unit, oneTheory.one]
240QED
241
242(*---------------------------------------------------------------------------
243 Booleans
244 ---------------------------------------------------------------------------*)
245
246Definition decode_bool_def[nocompute]:
247 decode_bool p = enc2dec p encode_bool
248End
249
250Theorem wf_decode_bool:
251 !p. wf_decoder p (decode_bool p)
252Proof
253 RW_TAC std_ss [decode_bool_def, wf_enc2dec, wf_encode_bool]
254QED
255
256Theorem dec2enc_decode_bool:
257 !p x. p x ==> (dec2enc (decode_bool p) x = encode_bool x)
258Proof
259 RW_TAC std_ss [decode_bool_def, dec2enc_enc2dec, wf_encode_bool]
260QED
261
262Theorem decode_bool:
263 decode_bool p l =
264 case l of [] => NONE | (h :: t) => if p h then SOME (h, t) else NONE
265Proof
266 TOP_CASE_TAC >>
267 RW_TAC std_ss
268 [decode_bool_def, enc2dec_none, enc2dec_some, encode_bool_def,
269 APPEND, wf_encode_bool]
270QED
271
272(*---------------------------------------------------------------------------
273 Pairs
274 ---------------------------------------------------------------------------*)
275
276Definition decode_prod_def[nocompute]:
277 decode_prod p d1 d2 = enc2dec p (encode_prod (dec2enc d1) (dec2enc d2))
278End
279
280Theorem wf_decode_prod:
281 !p1 p2 d1 d2.
282 wf_decoder p1 d1 /\ wf_decoder p2 d2 ==>
283 wf_decoder (lift_prod p1 p2) (decode_prod (lift_prod p1 p2) d1 d2)
284Proof
285 RW_TAC std_ss [decode_prod_def] >>
286 PROVE_TAC [wf_dec2enc, wf_enc2dec, wf_encode_prod]
287QED
288
289Theorem dec2enc_decode_prod:
290 !p1 p2 d1 d2 x.
291 wf_decoder p1 d1 /\ wf_decoder p2 d2 /\ lift_prod p1 p2 x ==>
292 (dec2enc (decode_prod (lift_prod p1 p2) d1 d2) x =
293 encode_prod (dec2enc d1) (dec2enc d2) x)
294Proof
295 RW_TAC std_ss
296 [decode_prod_def, dec2enc_enc2dec, wf_encode_prod, wf_dec2enc]
297QED
298
299Theorem encode_then_decode_prod:
300 !p1 p2 e1 e2 l t.
301 wf_encoder p1 e1 /\ wf_encoder p2 e2 /\ lift_prod p1 p2 l ==>
302 (decode_prod (lift_prod p1 p2) (enc2dec p1 e1) (enc2dec p2 e2)
303 (APPEND (encode_prod e1 e2 l) t) = SOME (l, t))
304Proof
305 RW_TAC std_ss [decode_prod_def] >>
306 MP_TAC
307 (Q.SPECL
308 [`lift_prod p1 p2`,
309 `encode_prod (dec2enc (enc2dec p1 e1)) (dec2enc (enc2dec p2 e2))`,
310 `APPEND (encode_prod e1 e2 l) t`, `l`, `t`]
311 (INST_TYPE [alpha |-> ``:'a # 'b``] enc2dec_some)) >>
312 MATCH_MP_TAC (PROVE [] ``x /\ (y ==> z) ==> (x ==> y) ==> z``) >>
313 CONJ_TAC >- PROVE_TAC [wf_encode_prod, wf_dec2enc, wf_enc2dec] >>
314 RW_TAC std_ss [APPEND_11] >>
315 POP_ASSUM (K ALL_TAC) >>
316 Cases_on `l` >>
317 FULL_SIMP_TAC std_ss [lift_prod_def, encode_prod_def, APPEND_11] >>
318 PROVE_TAC [dec2enc_enc2dec]
319QED
320
321Theorem decode_prod:
322 wf_decoder p1 d1 /\ wf_decoder p2 d2 ==>
323 (decode_prod (lift_prod p1 p2) d1 d2 l =
324 case d1 l of NONE => NONE
325 | SOME (x, t) =>
326 (case d2 t of NONE => NONE
327 | SOME (y, t') => SOME ((x, y), t')))
328Proof
329 (REPEAT TOP_CASE_TAC >>
330 RW_TAC std_ss
331 [decode_prod_def, enc2dec_none, GSYM APPEND_ASSOC, encode_prod_alt]) >|
332 [STRIP_TAC
333 >> RW_TAC std_ss []
334 >> Cases_on `x`
335 >> FULL_SIMP_TAC std_ss [lift_prod_def]
336 >> PROVE_TAC [decode_dec2enc_append, NOT_SOME_NONE],
337 STRIP_TAC
338 >> RW_TAC std_ss []
339 >> Cases_on `x`
340 >> FULL_SIMP_TAC std_ss [lift_prod_def]
341 >> Q.PAT_X_ASSUM `X = SOME Y` MP_TAC
342 >> MP_TAC (Q.SPECL [`p1`, `d1`, `q'`] decode_dec2enc_append)
343 >> ASM_SIMP_TAC std_ss []
344 >> DISCH_THEN (K ALL_TAC)
345 >> PURE_REWRITE_TAC [GSYM DE_MORGAN_THM]
346 >> STRIP_TAC
347 >> RW_TAC std_ss []
348 >> Q.PAT_X_ASSUM `X = Y` MP_TAC
349 >> RW_TAC std_ss [decode_prod_def, enc2dec_none]
350 >> PROVE_TAC [decode_dec2enc_append, NOT_SOME_NONE],
351 Know `wf_decoder (lift_prod p1 p2) (decode_prod (lift_prod p1 p2) d1 d2)`
352 >- PROVE_TAC [wf_decode_prod]
353 >> STRIP_TAC
354 >> Know `wf_encoder p1 (dec2enc d1)` >- PROVE_TAC [wf_dec2enc]
355 >> STRIP_TAC
356 >> Know `wf_encoder p2 (dec2enc d2)` >- PROVE_TAC [wf_dec2enc]
357 >> STRIP_TAC
358 >> Know
359 `wf_encoder (lift_prod p1 p2) (encode_prod (dec2enc d1) (dec2enc d2))`
360 >- PROVE_TAC [wf_encode_prod]
361 >> STRIP_TAC
362 >> ASM_SIMP_TAC std_ss [enc2dec_some, encode_prod_def, APPEND]
363 >> MATCH_MP_TAC (PROVE [] ``x /\ (x ==> y) ==> x /\ y``)
364 >> CONJ_TAC
365 >- (RW_TAC std_ss [lift_prod_def]
366 >> PROVE_TAC [wf_decoder_def, wf_decode_prod])
367 >> RW_TAC std_ss [lift_prod_def]
368 >> MP_TAC (Q.SPECL [`p1`, `d1`] wf_decoder_def)
369 >> ASM_SIMP_TAC std_ss []
370 >> DISCH_THEN (MP_TAC o Q.SPEC `q`)
371 >> RW_TAC std_ss []
372 >> RES_TAC
373 >> RW_TAC std_ss [GSYM APPEND_ASSOC]
374 >> Know `dec2enc d1 q = a` >- PROVE_TAC [APPEND_NIL, dec2enc_some]
375 >> RW_TAC std_ss [APPEND_11]
376 >> Q.PAT_X_ASSUM `!x. P x` (K ALL_TAC)
377 >> MP_TAC (Q.SPECL [`p2`, `d2`] (INST_TYPE [alpha |-> beta] wf_decoder_def))
378 >> ASM_SIMP_TAC std_ss []
379 >> DISCH_THEN (MP_TAC o Q.SPEC `q'`)
380 >> RW_TAC std_ss []
381 >> RES_TAC
382 >> RW_TAC std_ss [GSYM APPEND_ASSOC]
383 >> Know `dec2enc d2 q' = a` >- PROVE_TAC [APPEND_NIL, dec2enc_some]
384 >> RW_TAC std_ss [APPEND_11]]
385QED
386
387(*---------------------------------------------------------------------------
388 Sums
389 ---------------------------------------------------------------------------*)
390
391Definition decode_sum_def[nocompute]:
392 decode_sum p d1 d2 = enc2dec p (encode_sum (dec2enc d1) (dec2enc d2))
393End
394
395Theorem wf_decode_sum:
396 !p1 p2 d1 d2.
397 wf_decoder p1 d1 /\ wf_decoder p2 d2 ==>
398 wf_decoder (lift_sum p1 p2) (decode_sum (lift_sum p1 p2) d1 d2)
399Proof
400 RW_TAC std_ss [decode_sum_def] >>
401 PROVE_TAC [wf_dec2enc, wf_enc2dec, wf_encode_sum]
402QED
403
404Theorem dec2enc_decode_sum:
405 !p1 p2 d1 d2 x.
406 wf_decoder p1 d1 /\ wf_decoder p2 d2 /\ lift_sum p1 p2 x ==>
407 (dec2enc (decode_sum (lift_sum p1 p2) d1 d2) x =
408 encode_sum (dec2enc d1) (dec2enc d2) x)
409Proof
410 RW_TAC std_ss
411 [decode_sum_def, dec2enc_enc2dec, wf_encode_sum, wf_dec2enc]
412QED
413
414Theorem encode_then_decode_sum:
415 !p1 p2 e1 e2 l t.
416 wf_encoder p1 e1 /\ wf_encoder p2 e2 /\ lift_sum p1 p2 l ==>
417 (decode_sum (lift_sum p1 p2) (enc2dec p1 e1) (enc2dec p2 e2)
418 (APPEND (encode_sum e1 e2 l) t) = SOME (l, t))
419Proof
420 RW_TAC std_ss [decode_sum_def] >>
421 MP_TAC
422 (Q.SPECL
423 [`lift_sum p1 p2`,
424 `encode_sum (dec2enc (enc2dec p1 e1)) (dec2enc (enc2dec p2 e2))`,
425 `APPEND (encode_sum e1 e2 l) t`, `l`, `t`]
426 (INST_TYPE [alpha |-> ``:'a + 'b``] enc2dec_some)) >>
427 MATCH_MP_TAC (PROVE [] ``x /\ (y ==> z) ==> (x ==> y) ==> z``) >>
428 CONJ_TAC >- PROVE_TAC [wf_encode_sum, wf_dec2enc, wf_enc2dec] >>
429 RW_TAC std_ss [APPEND_11] >>
430 POP_ASSUM (K ALL_TAC) >>
431 Cases_on `l` >>
432 FULL_SIMP_TAC std_ss [lift_sum_def, encode_sum_def, APPEND_11] >>
433 PROVE_TAC [dec2enc_enc2dec]
434QED
435
436Theorem decode_sum:
437 wf_decoder p1 d1 /\ wf_decoder p2 d2 ==>
438 (decode_sum (lift_sum p1 p2) d1 d2 l =
439 case l of [] => NONE
440 | (T :: t) =>
441 (case d1 t of NONE => NONE
442 | SOME (x, t') => SOME (INL x, t'))
443 | (F :: t) =>
444 (case d2 t of NONE => NONE
445 | SOME (x, t') => SOME (INR x, t')))
446Proof
447 (REPEAT TOP_CASE_TAC >>
448 RW_TAC std_ss [decode_sum_def, enc2dec_none, GSYM APPEND_ASSOC]) >|
449 [Cases_on `x`
450 >> RW_TAC std_ss [encode_sum_def, APPEND],
451 (Cases_on `x` >> RW_TAC std_ss [encode_sum_def, APPEND])
452 >> STRIP_TAC
453 >> RW_TAC std_ss []
454 >> FULL_SIMP_TAC std_ss [lift_sum_def]
455 >> PROVE_TAC [decode_dec2enc_append, NOT_SOME_NONE],
456 Know `wf_decoder (lift_sum p1 p2) (decode_sum (lift_sum p1 p2) d1 d2)`
457 >- PROVE_TAC [wf_decode_sum]
458 >> STRIP_TAC
459 >> Know `wf_encoder p1 (dec2enc d1)` >- PROVE_TAC [wf_dec2enc]
460 >> STRIP_TAC
461 >> Know `wf_encoder p2 (dec2enc d2)` >- PROVE_TAC [wf_dec2enc]
462 >> STRIP_TAC
463 >> Know
464 `wf_encoder (lift_sum p1 p2) (encode_sum (dec2enc d1) (dec2enc d2))`
465 >- PROVE_TAC [wf_encode_sum]
466 >> STRIP_TAC
467 >> ASM_SIMP_TAC std_ss [enc2dec_some, encode_sum_def, APPEND]
468 >> MATCH_MP_TAC (PROVE [] ``x /\ (x ==> y) ==> x /\ y``)
469 >> CONJ_TAC
470 >- (RW_TAC std_ss [lift_sum_def]
471 >> PROVE_TAC [wf_decoder_def, wf_decode_sum])
472 >> RW_TAC std_ss [lift_sum_def]
473 >> MP_TAC (Q.SPECL [`p1`, `d1`] wf_decoder_def)
474 >> ASM_SIMP_TAC std_ss []
475 >> DISCH_THEN (MP_TAC o Q.SPEC `q`)
476 >> RW_TAC std_ss []
477 >> RES_TAC
478 >> RW_TAC std_ss [GSYM APPEND_ASSOC]
479 >> Know `dec2enc d1 q = a` >- PROVE_TAC [APPEND_NIL, dec2enc_some]
480 >> RW_TAC std_ss [APPEND_11],
481 (Cases_on `x` >> RW_TAC std_ss [encode_sum_def, APPEND])
482 >> STRIP_TAC
483 >> RW_TAC std_ss []
484 >> FULL_SIMP_TAC std_ss [lift_sum_def]
485 >> PROVE_TAC [decode_dec2enc_append, NOT_SOME_NONE],
486 Know `wf_decoder (lift_sum p1 p2) (decode_sum (lift_sum p1 p2) d1 d2)`
487 >- PROVE_TAC [wf_decode_sum]
488 >> STRIP_TAC
489 >> Know `wf_encoder p1 (dec2enc d1)` >- PROVE_TAC [wf_dec2enc]
490 >> STRIP_TAC
491 >> Know `wf_encoder p2 (dec2enc d2)` >- PROVE_TAC [wf_dec2enc]
492 >> STRIP_TAC
493 >> Know
494 `wf_encoder (lift_sum p1 p2) (encode_sum (dec2enc d1) (dec2enc d2))`
495 >- PROVE_TAC [wf_encode_sum]
496 >> STRIP_TAC
497 >> ASM_SIMP_TAC std_ss [enc2dec_some, encode_sum_def, APPEND]
498 >> MATCH_MP_TAC (PROVE [] ``x /\ (x ==> y) ==> x /\ y``)
499 >> CONJ_TAC
500 >- (RW_TAC std_ss [lift_sum_def]
501 >> PROVE_TAC [wf_decoder_def, wf_decode_sum])
502 >> RW_TAC std_ss [lift_sum_def]
503 >> Q.ISPECL_THEN [`p2`,`d2`] MP_TAC wf_decoder_def
504 >> ASM_SIMP_TAC std_ss []
505 >> DISCH_THEN (Q.SPEC_THEN `q` MP_TAC)
506 >> RW_TAC std_ss []
507 >> RES_TAC
508 >> RW_TAC std_ss [GSYM APPEND_ASSOC]
509 >> Know `dec2enc d2 q = a` >- PROVE_TAC [APPEND_NIL, dec2enc_some]
510 >> RW_TAC std_ss [APPEND_11]]
511QED
512
513(*---------------------------------------------------------------------------
514 Options
515 ---------------------------------------------------------------------------*)
516
517Definition decode_option_def[nocompute]:
518 decode_option p d = enc2dec p (encode_option (dec2enc d))
519End
520
521Theorem wf_decode_option:
522 !p d.
523 wf_decoder p d ==>
524 wf_decoder (lift_option p) (decode_option (lift_option p) d)
525Proof
526 RW_TAC std_ss [decode_option_def] >>
527 PROVE_TAC [wf_dec2enc, wf_enc2dec, wf_encode_option]
528QED
529
530Theorem dec2enc_decode_option:
531 !p d x.
532 wf_decoder p d /\ lift_option p x ==>
533 (dec2enc (decode_option (lift_option p) d) x =
534 encode_option (dec2enc d) x)
535Proof
536 RW_TAC std_ss
537 [decode_option_def, dec2enc_enc2dec, wf_encode_option, wf_dec2enc]
538QED
539
540Theorem encode_then_decode_option:
541 !p e l t.
542 wf_encoder p e /\ lift_option p l ==>
543 (decode_option (lift_option p) (enc2dec p e)
544 (APPEND (encode_option e l) t) = SOME (l, t))
545Proof
546 RW_TAC std_ss [decode_option_def] >>
547 MP_TAC
548 (Q.SPECL [`lift_option p`, `encode_option (dec2enc (enc2dec p e))`,
549 `APPEND (encode_option e l) t`, `l`, `t`]
550 (INST_TYPE [alpha |-> ``:'a option``] enc2dec_some)) >>
551 MATCH_MP_TAC (PROVE [] ``x /\ (y ==> z) ==> (x ==> y) ==> z``) >>
552 CONJ_TAC >- PROVE_TAC [wf_encode_option, wf_dec2enc, wf_enc2dec] >>
553 RW_TAC std_ss [APPEND_11] >>
554 POP_ASSUM (K ALL_TAC) >>
555 Cases_on `l` >>
556 FULL_SIMP_TAC std_ss [lift_option_def, encode_option_def, APPEND_11] >>
557 RW_TAC std_ss [] >>
558 PROVE_TAC [dec2enc_enc2dec]
559QED
560
561Theorem decode_option:
562 wf_decoder p d ==>
563 (decode_option (lift_option p) d l =
564 case l of [] => NONE
565 | (T :: t) =>
566 (case d t of NONE => NONE
567 | SOME (x, t') => SOME (SOME x, t'))
568 | (F :: t) => SOME (NONE, t))
569Proof
570 (REPEAT TOP_CASE_TAC >>
571 RW_TAC std_ss [decode_option_def, enc2dec_none]) >|
572 [Cases_on `x`
573 >> RW_TAC std_ss [encode_option_def, APPEND],
574 Cases_on `x`
575 >> POP_ASSUM MP_TAC
576 >> RW_TAC std_ss
577 [encode_option_def, APPEND, GSYM APPEND_ASSOC, lift_option_def]
578 >> STRIP_TAC
579 >> RW_TAC std_ss []
580 >> MP_TAC (Q.SPECL [`p`, `d`] wf_decoder_def)
581 >> RW_TAC std_ss []
582 >> Q.EXISTS_TAC `x'`
583 >> RW_TAC std_ss []
584 >> PROVE_TAC [decode_dec2enc_append, NOT_SOME_NONE],
585 Know `wf_decoder (lift_option p) (decode_option (lift_option p) d)`
586 >- PROVE_TAC [wf_decode_option]
587 >> STRIP_TAC
588 >> Know `wf_encoder p (dec2enc d)` >- PROVE_TAC [wf_dec2enc]
589 >> STRIP_TAC
590 >> Know `wf_encoder (lift_option p) (encode_option (dec2enc d))`
591 >- PROVE_TAC [wf_encode_option]
592 >> STRIP_TAC
593 >> ASM_SIMP_TAC std_ss
594 [enc2dec_some, encode_option_def, APPEND, lift_option_def]
595 >> MATCH_MP_TAC (PROVE [] ``x /\ (x ==> y) ==> x /\ y``)
596 >> CONJ_TAC >- PROVE_TAC [wf_decoder_def, wf_decode_option]
597 >> RW_TAC std_ss []
598 >> MP_TAC (Q.SPECL [`p`, `d`] wf_decoder_def)
599 >> ASM_SIMP_TAC std_ss []
600 >> DISCH_THEN (MP_TAC o Q.SPEC `q`)
601 >> RW_TAC std_ss []
602 >> RES_TAC
603 >> RW_TAC std_ss [GSYM APPEND_ASSOC]
604 >> Know `dec2enc d q = a` >- PROVE_TAC [APPEND_NIL, dec2enc_some]
605 >> RW_TAC std_ss [APPEND_11],
606 Know `wf_encoder p (dec2enc d)` >- PROVE_TAC [wf_dec2enc]
607 >> STRIP_TAC
608 >> Know `wf_encoder (lift_option p) (encode_option (dec2enc d))`
609 >- PROVE_TAC [wf_encode_option]
610 >> STRIP_TAC
611 >> ASM_SIMP_TAC std_ss
612 [enc2dec_some, encode_option_def, APPEND, lift_option_def]]
613QED
614
615(*---------------------------------------------------------------------------
616 Lists
617 ---------------------------------------------------------------------------*)
618
619Definition decode_list_def[nocompute]:
620 decode_list p d = enc2dec p (encode_list (dec2enc d))
621End
622
623Theorem wf_decode_list:
624 !p d.
625 wf_decoder p d ==> wf_decoder (EVERY p) (decode_list (EVERY p) d)
626Proof
627 RW_TAC std_ss [decode_list_def] >>
628 PROVE_TAC [wf_dec2enc, wf_enc2dec, wf_encode_list]
629QED
630
631Theorem dec2enc_decode_list:
632 !p d x.
633 wf_decoder p d /\ EVERY p x ==>
634 (dec2enc (decode_list (EVERY p) d) x = encode_list (dec2enc d) x)
635Proof
636 RW_TAC std_ss
637 [decode_list_def, dec2enc_enc2dec, wf_encode_list, wf_dec2enc]
638QED
639
640Theorem encode_then_decode_list:
641 !p e l t.
642 wf_encoder p e /\ EVERY p l ==>
643 (decode_list (EVERY p) (enc2dec p e) (APPEND (encode_list e l) t) =
644 SOME (l, t))
645Proof
646 RW_TAC std_ss [decode_list_def] >>
647 MP_TAC
648 (Q.SPECL [`EVERY p`, `encode_list (dec2enc (enc2dec p e))`,
649 `APPEND (encode_list e l) t`, `l`, `t`]
650 (INST_TYPE [alpha |-> ``:'a list``] enc2dec_some)) >>
651 MATCH_MP_TAC (PROVE [] ``x /\ (y ==> z) ==> (x ==> y) ==> z``) >>
652 CONJ_TAC >- PROVE_TAC [wf_encode_list, wf_dec2enc, wf_enc2dec] >>
653 RW_TAC std_ss [APPEND_11] >>
654 POP_ASSUM (K ALL_TAC) >>
655 Induct_on `l` >>
656 RW_TAC std_ss [EVERY_DEF, encode_list_def, APPEND_11] >>
657 PROVE_TAC [dec2enc_enc2dec]
658QED
659
660Theorem decode_list:
661 wf_decoder p d ==>
662 (decode_list (EVERY p) d l =
663 case l of [] => NONE
664 | (T :: t) =>
665 (case d t of NONE => NONE
666 | SOME (x, t') =>
667 (case decode_list (EVERY p) d t' of NONE => NONE
668 | SOME (xs, t'') => SOME (x :: xs, t'')))
669 | (F :: t) => SOME ([], t))
670Proof
671 (REPEAT TOP_CASE_TAC >>
672 RW_TAC std_ss [decode_list_def, enc2dec_none]) >|
673 [Cases_on `x` >>
674 RW_TAC std_ss [encode_list_def, APPEND],
675 Cases_on `x` >>
676 POP_ASSUM MP_TAC >>
677 RW_TAC std_ss [encode_list_def, APPEND, GSYM APPEND_ASSOC, EVERY_DEF] >>
678 POP_ASSUM (K ALL_TAC) >>
679 Q.SPEC_TAC (`APPEND (encode_list (dec2enc d) t'') t'`, `l`) >>
680 REPEAT STRIP_TAC >>
681 RW_TAC std_ss [] >>
682 MP_TAC (Q.SPECL [`p`, `d`] wf_decoder_def) >>
683 RW_TAC std_ss [] >>
684 Q.EXISTS_TAC `h` >>
685 RW_TAC std_ss [] >>
686 PROVE_TAC [decode_dec2enc_append, NOT_SOME_NONE],
687 Cases_on `x` >>
688 POP_ASSUM MP_TAC >>
689 RW_TAC std_ss [encode_list_def, APPEND, GSYM APPEND_ASSOC, EVERY_DEF] >>
690 STRIP_TAC >>
691 RW_TAC std_ss [] >>
692 Q.PAT_X_ASSUM `X = SOME Y` MP_TAC >>
693 MP_TAC (Q.SPECL [`p`, `d`, `h`] decode_dec2enc_append) >>
694 ASM_SIMP_TAC std_ss [] >>
695 DISCH_THEN (K ALL_TAC) >>
696 PURE_REWRITE_TAC [GSYM DE_MORGAN_THM] >>
697 STRIP_TAC >>
698 RW_TAC std_ss [] >>
699 Q.PAT_X_ASSUM `X = Y` MP_TAC >>
700 RW_TAC std_ss [decode_list_def, enc2dec_none] >>
701 PROVE_TAC [],
702 Know `wf_decoder (EVERY p) (decode_list (EVERY p) d)` >-
703 PROVE_TAC [wf_decode_list] >>
704 STRIP_TAC >>
705 Know `wf_encoder p (dec2enc d)` >- PROVE_TAC [wf_dec2enc] >>
706 STRIP_TAC >>
707 Know `wf_encoder (EVERY p) (encode_list (dec2enc d))` >-
708 PROVE_TAC [wf_encode_list] >>
709 STRIP_TAC >>
710 ASM_SIMP_TAC std_ss [enc2dec_some, encode_list_def, APPEND] >>
711 MATCH_MP_TAC (PROVE [] ``x /\ (x ==> y) ==> x /\ y``) >>
712 CONJ_TAC >- PROVE_TAC [EVERY_DEF, wf_decoder_def, wf_decode_list] >>
713 RW_TAC std_ss [EVERY_DEF] >>
714 MP_TAC (Q.SPECL [`p`, `d`] wf_decoder_def) >>
715 ASM_SIMP_TAC std_ss [] >>
716 DISCH_THEN (MP_TAC o Q.SPEC `q`) >>
717 RW_TAC std_ss [] >>
718 RES_TAC >>
719 RW_TAC std_ss [GSYM APPEND_ASSOC] >>
720 Know `dec2enc d q = a` >- PROVE_TAC [APPEND_NIL, dec2enc_some] >>
721 RW_TAC std_ss [APPEND_11] >>
722 Q.PAT_X_ASSUM `!x. P x` (K ALL_TAC) >>
723 MP_TAC
724 (Q.ISPECL [`EVERY (p : 'a -> bool)`, `decode_list (EVERY p) d`]
725 wf_decoder_def) >>
726 ASM_SIMP_TAC std_ss [] >>
727 DISCH_THEN (MP_TAC o Q.SPEC `q'`) >>
728 RW_TAC std_ss [] >>
729 RES_TAC >>
730 RW_TAC std_ss [] >>
731 Q.PAT_X_ASSUM `!x. P x` (K ALL_TAC) >>
732 Q.PAT_X_ASSUM `X = Y` MP_TAC >>
733 ASM_SIMP_TAC std_ss [decode_list_def, enc2dec_some],
734 Know `wf_decoder (EVERY p) (decode_list (EVERY p) d)` >-
735 PROVE_TAC [wf_decode_list] >>
736 STRIP_TAC >>
737 Know `wf_encoder p (dec2enc d)` >- PROVE_TAC [wf_dec2enc] >>
738 STRIP_TAC >>
739 Know `wf_encoder (EVERY p) (encode_list (dec2enc d))` >-
740 PROVE_TAC [wf_encode_list] >>
741 STRIP_TAC >>
742 ASM_SIMP_TAC std_ss [enc2dec_some, encode_list_def, APPEND, EVERY_DEF]]
743QED
744
745(*---------------------------------------------------------------------------
746 Bounded lists
747 ---------------------------------------------------------------------------*)
748
749Definition decode_blist_def[nocompute]:
750 decode_blist p m d = enc2dec p (encode_blist m (dec2enc d))
751End
752
753Theorem wf_decode_blist:
754 !m p d.
755 wf_decoder p d ==>
756 wf_decoder (lift_blist m p) (decode_blist (lift_blist m p) m d)
757Proof
758 RW_TAC std_ss [decode_blist_def]
759 >> PROVE_TAC [wf_dec2enc, wf_enc2dec, wf_encode_blist]
760QED
761
762Theorem dec2enc_decode_blist:
763 !m p d l.
764 wf_decoder p d /\ lift_blist m p l ==>
765 (dec2enc (decode_blist (lift_blist m p) m d) l =
766 encode_blist m (dec2enc d) l)
767Proof
768 RW_TAC std_ss [decode_blist_def]
769 >> PROVE_TAC [dec2enc_enc2dec, wf_encode_blist, wf_dec2enc]
770QED
771
772Theorem encode_then_decode_blist:
773 !m p e l t.
774 wf_encoder p e /\ lift_blist m p l ==>
775 (decode_blist (lift_blist m p) m (enc2dec p e)
776 (APPEND (encode_blist m e l) t) = SOME (l, t))
777Proof
778 RW_TAC std_ss [decode_blist_def]
779 >> MP_TAC
780 (Q.SPECL [`lift_blist m p`, `encode_blist m (dec2enc (enc2dec p e))`,
781 `APPEND (encode_blist m e l) t`, `l`, `t`]
782 (INST_TYPE [alpha |-> ``:'a list``] enc2dec_some))
783 >> MATCH_MP_TAC (PROVE [] ``x /\ (y ==> z) ==> (x ==> y) ==> z``)
784 >> CONJ_TAC >- PROVE_TAC [wf_encode_blist, wf_dec2enc, wf_enc2dec]
785 >> RW_TAC std_ss [APPEND_11]
786 >> POP_ASSUM (K ALL_TAC)
787 >> POP_ASSUM MP_TAC
788 >> Q.SPEC_TAC (`l`, `l`)
789 >> Induct_on `m`
790 >> RW_TAC std_ss [lift_blist_def, encode_blist_def, APPEND_11]
791 >> Cases_on `l` >- FULL_SIMP_TAC std_ss [LENGTH, SUC_NOT]
792 >> FULL_SIMP_TAC std_ss [HD, TL, EVERY_DEF, LENGTH]
793 >> RW_TAC std_ss [dec2enc_enc2dec, APPEND_11]
794 >> Q.PAT_X_ASSUM `!l. P l` MATCH_MP_TAC
795 >> RW_TAC std_ss [lift_blist_def]
796QED
797
798Theorem decode_blist:
799 wf_decoder (p : 'a -> bool) d ==>
800 (decode_blist (lift_blist m p) m d l =
801 case m of 0 => SOME ([], l)
802 | SUC n =>
803 (case d l of NONE => NONE
804 | SOME (x, t) =>
805 (case decode_blist (lift_blist n p) n d t of NONE => NONE
806 | SOME (xs, t') => SOME (x :: xs, t'))))
807Proof
808 (REPEAT TOP_CASE_TAC >>
809 RW_TAC std_ss [decode_blist_def, enc2dec_none, lift_blist_def, LENGTH_NIL])
810 >| [MP_TAC
811 (Q.SPECL
812 [`lift_blist 0 p`, `encode_blist 0 (dec2enc d)`, `l`, `[]`, `l`]
813 (INST_TYPE [alpha |-> ``:'a list``] enc2dec_some))
814 >> MATCH_MP_TAC (PROVE [] ``x /\ (y ==> z) ==> (x ==> y) ==> z``)
815 >> CONJ_TAC >- PROVE_TAC [wf_dec2enc, wf_encode_blist]
816 >> DISCH_THEN (fn th => REWRITE_TAC [th])
817 >> RW_TAC std_ss
818 [lift_blist_def, EVERY_DEF, LENGTH, encode_blist_def, APPEND],
819 STRIP_TAC
820 >> Cases_on `x`
821 >> FULL_SIMP_TAC std_ss [LENGTH, SUC_NOT, EVERY_DEF]
822 >> RW_TAC std_ss []
823 >> Q.PAT_X_ASSUM `X = Y` MP_TAC
824 >> RW_TAC std_ss [encode_blist_def, GSYM APPEND_ASSOC, HD, TL]
825 >> PROVE_TAC [decode_dec2enc_append, NOT_SOME_NONE],
826 STRIP_TAC
827 >> Cases_on `x`
828 >> FULL_SIMP_TAC std_ss [LENGTH, SUC_NOT, EVERY_DEF]
829 >> RW_TAC std_ss []
830 >> Q.PAT_X_ASSUM `X = SOME Y` MP_TAC
831 >> RW_TAC std_ss [encode_blist_def, GSYM APPEND_ASSOC, HD, TL]
832 >> MP_TAC (Q.SPECL [`p`, `d`, `h`] decode_dec2enc_append)
833 >> ASM_REWRITE_TAC []
834 >> Cases_on `h = q`
835 >> DISCH_THEN (fn th => RW_TAC std_ss [th])
836 >> STRIP_TAC
837 >> RW_TAC std_ss []
838 >> Q.PAT_X_ASSUM `X = Y` MP_TAC
839 >> MP_TAC
840 (Q.SPECL [`LENGTH t'`, `p`, `dec2enc d`, `t'`, `t`]
841 encode_then_decode_blist)
842 >> MATCH_MP_TAC (PROVE [] ``x /\ (y ==> z) ==> (x ==> y) ==> z``)
843 >> CONJ_TAC >- RW_TAC std_ss [wf_dec2enc, lift_blist_def]
844 >> Suff `enc2dec p (dec2enc d) = d` >- RW_TAC std_ss []
845 >> PROVE_TAC [enc2dec_dec2enc],
846 Know `wf_encoder p (dec2enc d)` >- PROVE_TAC [wf_dec2enc]
847 >> STRIP_TAC
848 >> ASM_SIMP_TAC std_ss [enc2dec_some, wf_encode_blist, lift_blist_suc]
849 >> MATCH_MP_TAC (PROVE [] ``x /\ (x ==> y) ==> x /\ y``)
850 >> CONJ_TAC
851 >- (CONJ_TAC >- PROVE_TAC [wf_decoder_def, APPEND_NIL]
852 >> Q.PAT_X_ASSUM `X = Y` MP_TAC
853 >> RW_TAC std_ss [decode_blist_def, enc2dec_some, wf_encode_blist])
854 >> RW_TAC std_ss [encode_blist_def, GSYM APPEND_ASSOC, HD, TL]
855 >> Q.UNDISCH_TAC `d l = SOME (q,r)`
856 >> Know `wf_decoder p d` >- RW_TAC std_ss []
857 >> SIMP_TAC std_ss [wf_decoder_def]
858 >> DISCH_THEN (MP_TAC o Q.SPEC `q`)
859 >> ASM_SIMP_TAC std_ss []
860 >> STRIP_TAC
861 >> RW_TAC std_ss []
862 >> Know `dec2enc d q = a` >- PROVE_TAC [APPEND_NIL, dec2enc_some]
863 >> RW_TAC std_ss [APPEND_11]
864 >> POP_ASSUM (K ALL_TAC)
865 >> Q.PAT_X_ASSUM `X = Y` MP_TAC
866 >> RW_TAC std_ss [decode_blist_def, enc2dec_some, wf_encode_blist]]
867QED
868
869(*---------------------------------------------------------------------------
870 Nums
871 ---------------------------------------------------------------------------*)
872
873Definition decode_num_def[nocompute]:
874 decode_num p = enc2dec p encode_num
875End
876
877Theorem wf_decode_num:
878 !p. wf_decoder p (decode_num p)
879Proof
880 RW_TAC std_ss [decode_num_def, wf_enc2dec, wf_encode_num]
881QED
882
883Theorem dec2enc_decode_num:
884 !p x. p x ==> (dec2enc (decode_num p) x = encode_num x)
885Proof
886 RW_TAC std_ss [decode_num_def, dec2enc_enc2dec, wf_encode_num]
887QED
888
889Theorem decode_num_total:
890 decode_num (K T) l =
891 case l of
892 (T :: T :: t) => SOME (0, t)
893 | (T :: F :: t) =>
894 (case decode_num (K T) t of NONE => NONE
895 | SOME (v, t') => SOME (2 * v + 1, t'))
896 | (F :: t) =>
897 (case decode_num (K T) t of NONE => NONE
898 | SOME (v, t') => SOME (2 * v + 2, t'))
899 | _ => NONE
900Proof
901 (REPEAT TOP_CASE_TAC
902 >> REPEAT (POP_ASSUM MP_TAC)
903 >> RW_TAC std_ss
904 [decode_num_def, enc2dec_none, K_THM, enc2dec_some, wf_encode_num]) >|
905 [ONCE_REWRITE_TAC [encode_num_def]
906 >> RW_TAC std_ss [APPEND],
907 ONCE_REWRITE_TAC [encode_num_def]
908 >> RW_TAC std_ss [APPEND],
909 ONCE_REWRITE_TAC [encode_num_def]
910 >> RW_TAC std_ss [APPEND],
911 ONCE_REWRITE_TAC [encode_num_def]
912 >> RW_TAC std_ss [APPEND],
913 CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [encode_num_def]))
914 >> RW_TAC arith_ss [APPEND, MULT_DIV, Q.SPECL [`2`, `q`] MULT_COMM]
915 >> POP_ASSUM MP_TAC
916 >> RW_TAC std_ss [GSYM ADD1, EVEN]
917 >> PROVE_TAC [EVEN_DOUBLE, MULT_COMM],
918 ONCE_REWRITE_TAC [encode_num_def]
919 >> RW_TAC std_ss [APPEND],
920 CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [encode_num_def]))
921 >> RW_TAC arith_ss [APPEND, MULT_DIV, Q.SPECL [`2`, `q`] MULT_COMM]
922 >> POP_ASSUM MP_TAC
923 >> RW_TAC arith_ss [APPEND, GSYM MULT, Q.SPECL [`q`, `2`] MULT_COMM]
924 >> PROVE_TAC [EVEN_DOUBLE]]
925QED
926
927Theorem decode_num:
928 decode_num p l =
929 case l of
930 (T :: T :: t) => if p 0 then SOME (0, t) else NONE
931 | (T :: F :: t) =>
932 (case decode_num (K T) t of NONE => NONE
933 | SOME (v, t') =>
934 if p (2 * v + 1) then SOME (2 * v + 1, t') else NONE)
935 | (F :: t) =>
936 (case decode_num (K T) t of NONE => NONE
937 | SOME (v, t') =>
938 if p (2 * v + 2) then SOME (2 * v + 2, t') else NONE)
939 | _ => NONE
940Proof
941 (MP_TAC decode_num_total
942 >> STRIP_TAC
943 >> REPEAT TOP_CASE_TAC
944 >> RW_TAC std_ss [decode_num_def, enc2dec_none]
945 >> ASSUM_LIST (UNDISCH_TAC o concl o last)
946 >> RW_TAC std_ss
947 [K_THM, decode_num_def, enc2dec_none, enc2dec_some, wf_encode_num]
948 >> POP_ASSUM (fn th => REWRITE_TAC [SYM th])
949 >> ONCE_REWRITE_TAC [encode_num_def]
950 >> RW_TAC std_ss [APPEND]
951 >> STRIP_TAC
952 >> RW_TAC std_ss []) >|
953 [PROVE_TAC [],
954 Q.PAT_X_ASSUM `X = Y` MP_TAC
955 >> Know `encode_num = dec2enc (decode_num (K T))`
956 >- (RW_TAC std_ss [decode_num_def]
957 >> MATCH_MP_TAC EQ_EXT
958 >> RW_TAC std_ss [dec2enc_enc2dec, K_THM, wf_encode_num])
959 >> RW_TAC std_ss []
960 >> MP_TAC (Q.SPEC `K T` wf_decode_num)
961 >> Q.SPEC_TAC (`decode_num (K T)`, `d`)
962 >> REPEAT STRIP_TAC
963 >> MP_TAC
964 (Q.SPECL [`K T`, `d`, `(x - 1) DIV 2`, `t`]
965 (INST_TYPE [alpha |-> ``:num``] decode_dec2enc_append))
966 >> RW_TAC std_ss [K_THM]
967 >> REWRITE_TAC [GSYM DE_MORGAN_THM]
968 >> STRIP_TAC
969 >> RW_TAC std_ss []
970 >> FULL_SIMP_TAC std_ss [EVEN_ODD, ODD_EXISTS]
971 >> Q.PAT_X_ASSUM `~p X` MP_TAC
972 >> RW_TAC arith_ss []
973 >> RW_TAC arith_ss [MULT_DIV, Q.SPECL [`2`, `m`] MULT_COMM, GSYM ADD1]
974 >> PROVE_TAC [MULT_COMM],
975 Q.PAT_X_ASSUM `X = Y` MP_TAC
976 >> Know `encode_num = dec2enc (decode_num (K T))`
977 >- (RW_TAC std_ss [decode_num_def]
978 >> MATCH_MP_TAC EQ_EXT
979 >> RW_TAC std_ss [dec2enc_enc2dec, K_THM, wf_encode_num])
980 >> RW_TAC std_ss []
981 >> MP_TAC (Q.SPEC `K T` wf_decode_num)
982 >> Q.SPEC_TAC (`decode_num (K T)`, `d`)
983 >> GEN_TAC
984 >> STRIP_TAC
985 >> MP_TAC
986 (Q.SPECL [`K T`, `d`, `(x - 2) DIV 2`, `t'`]
987 (INST_TYPE [alpha |-> ``:num``] decode_dec2enc_append))
988 >> RW_TAC std_ss [K_THM]
989 >> REWRITE_TAC [GSYM DE_MORGAN_THM]
990 >> STRIP_TAC
991 >> RW_TAC std_ss []
992 >> Cases_on `x` >- RW_TAC std_ss []
993 >> FULL_SIMP_TAC std_ss [EVEN, EVEN_ODD, ODD_EXISTS]
994 >> Q.PAT_X_ASSUM `~p X` MP_TAC
995 >> RW_TAC arith_ss [ADD1]
996 >> Q.PAT_X_ASSUM `p X` MP_TAC
997 >> RW_TAC arith_ss [MULT_DIV, Q.SPECL [`2`, `m`] MULT_COMM, ADD1]]
998QED
999
1000(*---------------------------------------------------------------------------
1001 Bounded numbers
1002 ---------------------------------------------------------------------------*)
1003
1004Definition decode_bnum_def[nocompute]:
1005 decode_bnum m p = enc2dec p (encode_bnum m)
1006End
1007
1008Definition dec_bnum_def:
1009 (dec_bnum 0 l = SOME (0, l)) /\
1010 (dec_bnum (SUC m) l =
1011 case l of [] => NONE
1012 | (h :: t) =>
1013 (case dec_bnum m t of NONE => NONE
1014 | SOME (n, t') => SOME (2 * n + (if h then 1 else 0), t')))
1015End
1016
1017Theorem dec_bnum_lt:
1018 !m l n t. (dec_bnum m l = SOME (n, t)) ==> n < 2 ** m
1019Proof
1020 Induct >> rw[dec_bnum_def, AllCaseEqs()] >> first_x_assum drule >>
1021 rw[EXP]
1022QED
1023
1024Theorem dec_bnum_inj:
1025 !m l n t.
1026 (dec_bnum m l = SOME (n, t)) ==> (l = APPEND (encode_bnum m n) t)
1027Proof
1028 Induct
1029 >> RW_TAC std_ss [dec_bnum_def, encode_bnum_def, APPEND]
1030 >> POP_ASSUM MP_TAC
1031 >> REPEAT TOP_CASE_TAC
1032 >> RES_TAC
1033 >> POP_ASSUM SUBST1_TAC
1034 >> POP_ASSUM_LIST (K ALL_TAC)
1035 >> MP_TAC (Q.SPEC `2` DIVISION)
1036 >> SIMP_TAC arith_ss []
1037 >> DISCH_THEN (MP_TAC o ONCE_REWRITE_RULE [MULT_COMM] o Q.SPEC `n`)
1038 >> DISCH_THEN (fn th => CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [th])))
1039 >> RW_TAC arith_ss [MOD_2, GSYM ADD1, APPEND_11]
1040 >> (Know `!m n. (2 * m = 2 * n) = (m = n)`
1041 >- RW_TAC arith_ss [EQ_MULT_LCANCEL])
1042 >> DISCH_THEN (fn th => FULL_SIMP_TAC std_ss [th])
1043 >> RW_TAC std_ss []
1044 >> PROVE_TAC [ODD_DOUBLE, EVEN_DOUBLE, ODD_EVEN]
1045QED
1046
1047Theorem wf_decode_bnum:
1048 !m p. wf_pred_bnum m p ==> wf_decoder p (decode_bnum m p)
1049Proof
1050 RW_TAC std_ss [decode_bnum_def, wf_enc2dec, wf_encode_bnum]
1051QED
1052
1053Theorem dec2enc_decode_bnum:
1054 !m p x.
1055 wf_pred_bnum m p /\ p x ==>
1056 (dec2enc (decode_bnum m p) x = encode_bnum m x)
1057Proof
1058 RW_TAC std_ss [decode_bnum_def, dec2enc_enc2dec, wf_encode_bnum]
1059QED
1060
1061Theorem decode_bnum:
1062 wf_pred_bnum m p ==>
1063 (decode_bnum m p l =
1064 case dec_bnum m l of NONE => NONE
1065 | SOME (n, t) => if p n then SOME (n, t) else NONE)
1066Proof
1067 simp[decode_bnum_def] >>
1068 map_every qid_spec_tac [‘p’, ‘l’] >> Induct_on `m`
1069 >- (rw[dec_bnum_def, enc2dec_none, enc2dec_some,
1070 wf_encode_bnum, encode_bnum_def] >>
1071 gs[wf_pred_bnum_def] >> PROVE_TAC [DECIDE ``x < 1 ==> (x = 0)``]) >>
1072 simp[dec_bnum_def] >> rpt strip_tac >>
1073 Cases_on ‘l’ >> simp[enc2dec_none, encode_bnum_def] >>
1074 Cases_on ‘dec_bnum m t’ >>
1075 simp[enc2dec_none, encode_bnum_def, dec_bnum_def]
1076 >- (rename [‘dec_bnum m t = NONE’] >>
1077 first_x_assum $ qspec_then ‘t’ mp_tac >>
1078 simp[enc2dec_none] >> rpt strip_tac >>
1079 disj2_tac >> first_x_assum irule >>
1080 gs[wf_pred_bnum_def] >> qexists_tac ‘λx. x < 2 ** m’ >>
1081 simp[wf_pred_def] >> irule_at Any (iffRL ZERO_LT_EXP) >> simp[]) >>
1082 rename [‘dec_bnum m t = SOME pair’] >> Cases_on ‘pair’ >> simp[] >>
1083 qmatch_abbrev_tac ‘enc2dec _ _ _ = if p N then _ else NONE’ >> rw[] >>
1084 simp[enc2dec_some, enc2dec_none, wf_encode_bnum]
1085 >- (rename [‘dec_bnum m t = SOME (N0, t0)’] >>
1086 simp[encode_bnum_def] >> conj_tac
1087 >- (simp[Abbr‘N’, EVEN_ADD, EVEN_MULT] >> rw[]) >>
1088 first_x_assum $ qspec_then ‘t’ mp_tac >> simp[] >>
1089 disch_then $ qspec_then ‘λn. n < 2 ** m’ mp_tac >>
1090 ‘N0 < 2 ** m’ by metis_tac[dec_bnum_lt] >>
1091 simp[enc2dec_some, wf_encode_bnum] >> impl_tac
1092 >- (simp[wf_pred_bnum_def, wf_pred_def] >>
1093 irule_at Any (iffRL ZERO_LT_EXP) >> simp[]) >>
1094 simp[Abbr‘N’] >> rw[]) >>
1095 simp[encode_bnum_def] >> rpt strip_tac >>
1096 first_x_assum $ qspec_then ‘t’ mp_tac >> simp[] >> strip_tac >>
1097 gs[SF boolSimps.LIFT_COND_ss] >>
1098 gs[enc2dec_none, wf_encode_bnum, enc2dec_some, COND_EXPAND_IMP,
1099 FORALL_AND_THM] >>
1100 rename [‘encode_bnum m (x DIV 2)’, ‘dec_bnum m t = SOME (N0, t0)’] >>
1101 Cases_on ‘N0 = x DIV 2’
1102 >- (Cases_on ‘h = ~EVEN x’ >> simp[] >> gvs[Abbr‘N’] >>
1103 ‘(~EVEN x ==> 2 * (x DIV 2) + 1 = x) /\
1104 (EVEN x ==> 2 * (x DIV 2) = x)’
1105 by (rpt strip_tac >> mp_tac $ Q.SPEC ‘2’ DIVISION >> simp[] >>
1106 disch_then $ qspec_then ‘x’ (fn th => simp[Once th, SimpRHS]) >>
1107 simp[MOD_2]) >> gs[]) >>
1108 disj2_tac >>
1109 first_x_assum irule >>
1110 qexists_tac ‘λn. n = x DIV 2’ >> simp[] >> gs[wf_pred_bnum_def, wf_pred_def]
1111QED
1112
1113(*---------------------------------------------------------------------------
1114 Trees
1115 ---------------------------------------------------------------------------*)
1116
1117Definition decode_tree_def[nocompute]:
1118 decode_tree p d = enc2dec p (encode_tree (dec2enc d))
1119End
1120
1121Theorem wf_decode_tree:
1122 !p d.
1123 wf_decoder p d ==>
1124 wf_decoder (lift_tree p) (decode_tree (lift_tree p) d)
1125Proof
1126 RW_TAC std_ss [decode_tree_def] >>
1127 PROVE_TAC [wf_dec2enc, wf_enc2dec, wf_encode_tree]
1128QED
1129
1130Theorem decode_tree:
1131 wf_decoder p d ==>
1132 (decode_tree (lift_tree p) d l =
1133 case d l of NONE => NONE
1134 | SOME (a, t) =>
1135 (case decode_list (EVERY (lift_tree p))
1136 (decode_tree (lift_tree p) d) t
1137 of NONE => NONE
1138 | SOME (ts, t') => SOME (Node a ts, t')))
1139Proof
1140 STRIP_TAC >>
1141 Know `wf_decoder (lift_tree p) (decode_tree (lift_tree p) d)` >-
1142 PROVE_TAC [wf_decode_tree] >>
1143 STRIP_TAC >>
1144 Know `wf_decoder (EVERY (lift_tree p))
1145 (decode_list (EVERY (lift_tree p)) (decode_tree (lift_tree p) d))` >-
1146 PROVE_TAC [wf_decode_list] >>
1147 STRIP_TAC >>
1148 REPEAT TOP_CASE_TAC >|
1149 [RW_TAC std_ss [decode_tree_def, enc2dec_none] >>
1150 STRIP_TAC >>
1151 RW_TAC std_ss [] >>
1152 Q.PAT_X_ASSUM `X = Y` MP_TAC >>
1153 Cases_on `x` >>
1154 RW_TAC std_ss [encode_tree_def, GSYM APPEND_ASSOC] >>
1155 POP_ASSUM MP_TAC >>
1156 RW_TAC std_ss [lift_tree_def] >>
1157 MP_TAC (Q.SPECL [`p`, `d`, `a`] decode_dec2enc_append) >>
1158 RW_TAC std_ss [],
1159 RW_TAC std_ss [decode_tree_def, enc2dec_none] >>
1160 STRIP_TAC >>
1161 RW_TAC std_ss [] >>
1162 Q.PAT_X_ASSUM `X = SOME Y` MP_TAC >>
1163 POP_ASSUM MP_TAC >>
1164 Cases_on `x` >>
1165 RW_TAC std_ss [lift_tree_def, encode_tree_def, GSYM APPEND_ASSOC] >>
1166 MP_TAC (Q.SPECL [`p`, `d`, `a`] decode_dec2enc_append) >>
1167 RW_TAC std_ss [] >>
1168 REVERSE (Cases_on `a = q`) >- RW_TAC std_ss [] >>
1169 RW_TAC std_ss [] >>
1170 STRIP_TAC >>
1171 RW_TAC std_ss [] >>
1172 POP_ASSUM (K ALL_TAC) >>
1173 Q.PAT_X_ASSUM `X = Y` MP_TAC >>
1174 POP_ASSUM MP_TAC >>
1175 POP_ASSUM (K ALL_TAC) >>
1176 CONV_TAC (DEPTH_CONV ETA_CONV) >>
1177 STRIP_TAC >>
1178 MP_TAC (Q.SPECL [`lift_tree p`, `encode_tree (dec2enc d)`, `l`, `t`]
1179 (INST_TYPE [alpha |-> ``:'a tree``] encode_then_decode_list)) >>
1180 MATCH_MP_TAC (PROVE [] ``(y ==> z) /\ x ==> (x ==> y) ==> z``) >>
1181 CONJ_TAC >- RW_TAC std_ss [decode_tree_def] >>
1182 PROVE_TAC [wf_encode_tree, wf_dec2enc],
1183 MP_TAC
1184 (Q.SPECL [`lift_tree p`, `encode_tree (dec2enc d)`, `l`, `Node q q'`, `r'`]
1185 (INST_TYPE [alpha |-> ``:'a tree``] enc2dec_some)) >>
1186 MATCH_MP_TAC (PROVE [] ``x /\ (y ==> z) ==> (x ==> y) ==> z``) >>
1187 CONJ_TAC >- PROVE_TAC [wf_encode_tree, wf_dec2enc] >>
1188 DISCH_THEN (fn th => SIMP_TAC std_ss [decode_tree_def, th]) >>
1189 SIMP_TAC std_ss [encode_tree_def, GSYM APPEND_ASSOC, lift_tree_def] >>
1190 CONV_TAC (DEPTH_CONV ETA_CONV) >>
1191 Suff
1192 `(p q /\ (l = APPEND (dec2enc d q) r)) /\
1193 (ALL_EL (lift_tree p) q' /\
1194 (r = APPEND (encode_list (encode_tree (dec2enc d)) q') r'))` >-
1195 RW_TAC std_ss [] >>
1196 CONJ_TAC >|
1197 [Know `enc2dec p (dec2enc d) l = SOME (q, r)` >-
1198 PROVE_TAC [enc2dec_dec2enc] >>
1199 RW_TAC std_ss [enc2dec_some, wf_dec2enc],
1200 POP_ASSUM MP_TAC >>
1201 SIMP_TAC std_ss [decode_list_def] >>
1202 RW_TAC std_ss [enc2dec_some, wf_dec2enc, wf_encode_list, APPEND_11] >>
1203 Q.PAT_X_ASSUM `X = Y` (K ALL_TAC) >>
1204 Induct_on `q'` >>
1205 RW_TAC std_ss [EVERY_DEF, encode_list_def, APPEND_11] >>
1206 RW_TAC std_ss
1207 [decode_tree_def, dec2enc_enc2dec, wf_dec2enc, wf_encode_tree]]]
1208QED
1209
1210val _ = computeLib.add_persistent_funs
1211 ["decode_unit",
1212 "decode_bool",
1213 "decode_num"];
1214
1215(* decode_prod, decode_sum, decode_option, decode_list, decode_blist,
1216 decode_bnum, and decode_tree all have preconditions that need
1217 to be eliminated *)
1218