1open HolKernel Parse boolLib;
2open bossLib pred_setTheory listTheory rich_listTheory pairTheory realLib
3     hurdUtils extra_listTheory;
4
5val _ = new_theory "prob_canon";
6val _ = ParseExtras.temp_loose_equality()
7
8(* ------------------------------------------------------------------------- *)
9(* Definition of the canonicalisation of algebra elements.                   *)
10(* ------------------------------------------------------------------------- *)
11
12val prob_twin_def = Define
13  `prob_twin x y = ?l. (x = SNOC T l) /\ (y = SNOC F l)`;
14
15val prob_order_def = Define
16  `(prob_order [] _ = T) /\
17   (prob_order _ [] = F) /\
18   (prob_order (h :: t) (h' :: t') =
19    ((h = T) /\ (h' = F)) \/ ((h = h') /\ prob_order t t'))`;
20
21val prob_sorted_def = Define `(prob_sorted (x :: y :: z)
22      = prob_order x y /\ prob_sorted (y :: z))
23  /\ (prob_sorted l = T)`;
24
25val prob_prefixfree_def = Define `(prob_prefixfree ((x:bool list)::y::z)
26      = ~IS_PREFIX y x /\ prob_prefixfree (y::z))
27  /\ (prob_prefixfree l = T)`;
28
29val prob_twinfree_def = Define `(prob_twinfree (x::y::z)
30      = ~(prob_twin x y) /\ prob_twinfree (y::z))
31  /\ (prob_twinfree l = T)`;
32
33val prob_longest_def = Define `prob_longest
34  = FOLDR (\h t. if t <= LENGTH (h:bool list) then LENGTH h else t) 0`
35
36val prob_canon_prefs_def = Define `(prob_canon_prefs (l:bool list) [] = [l])
37  /\ (prob_canon_prefs l (h::t) = if IS_PREFIX h l then prob_canon_prefs l t
38                                 else l::h::t)`;
39
40val prob_canon_find_def = Define `(prob_canon_find l [] = [l])
41  /\ (prob_canon_find l (h::t) = if prob_order h l then
42          if IS_PREFIX l h then (h::t) else h::(prob_canon_find l t)
43        else prob_canon_prefs l (h::t))`;
44
45val prob_canon1_def = Define `prob_canon1 = FOLDR prob_canon_find []`;
46
47val prob_canon_merge_def = Define `(prob_canon_merge l [] = [l])
48  /\ (prob_canon_merge l (h::t)
49      = if prob_twin l h then prob_canon_merge (BUTLAST h) t else l::h::t)`;
50
51val prob_canon2_def = Define `prob_canon2 = FOLDR prob_canon_merge []`;
52
53val prob_canon_def = Define `prob_canon l = prob_canon2 (prob_canon1 l)`;
54
55val prob_canonical_def = Define `prob_canonical l = (prob_canon l = l)`;
56
57(* ------------------------------------------------------------------------- *)
58(* Theorems leading to:                                                      *)
59(* 1. Canonical form is the same as sorted, prefixfree and twinfree.         *)
60(* 2. Induction principle on elements in canonical form.                     *)
61(* ------------------------------------------------------------------------- *)
62
63val PROB_TWIN_NIL = store_thm
64  ("PROB_TWIN_NIL",
65   ``!l. ~(prob_twin l []) /\ ~(prob_twin [] l)``,
66   RW_TAC std_ss [prob_twin_def]
67   >> Cases_on `l'`
68   >> RW_TAC std_ss [SNOC]);
69
70val PROB_TWIN_SING = store_thm
71  ("PROB_TWIN_SING",
72   ``!x l. (prob_twin [x] l = (x = T) /\ (l = [F]))
73           /\ (prob_twin l [x] = (l = [T]) /\ (x = F))``,
74   RW_TAC std_ss [prob_twin_def] >|
75   [EQ_TAC >|
76    [Cases_on `l` >- PROVE_TAC [NOT_NIL_SNOC]
77     >> DISCH_THEN (Q.X_CHOOSE_THEN `l` STRIP_ASSUME_TAC)
78     >> NTAC 2 (POP_ASSUM MP_TAC)
79     >> reverse (Cases_on `l`) >- RW_TAC std_ss [SNOC, NOT_NIL_SNOC]
80     >> RW_TAC std_ss [SNOC],
81     RW_TAC std_ss []
82     >> Q.EXISTS_TAC `[]`
83     >> RW_TAC std_ss [SNOC]],
84    EQ_TAC >|
85    [Cases_on `l` >- PROVE_TAC [NOT_NIL_SNOC]
86     >> DISCH_THEN (Q.X_CHOOSE_THEN `l` STRIP_ASSUME_TAC)
87     >> NTAC 2 (POP_ASSUM MP_TAC)
88     >> reverse (Cases_on `l`) >- RW_TAC std_ss [SNOC, NOT_NIL_SNOC]
89     >> RW_TAC std_ss [SNOC],
90     RW_TAC std_ss []
91     >> Q.EXISTS_TAC `[]`
92     >> RW_TAC std_ss [SNOC]]]);
93
94val PROB_TWIN_CONS = store_thm
95  ("PROB_TWIN_CONS",
96   ``!x y z h t. (prob_twin (x::y::z) (h::t) = (x = h) /\ prob_twin (y::z) t)
97              /\ (prob_twin (h::t) (x::y::z) = (x = h) /\ prob_twin t (y::z))``,
98   RW_TAC std_ss [prob_twin_def] >|
99   [EQ_TAC >|
100    [STRIP_TAC
101     >> NTAC 2 (POP_ASSUM MP_TAC)
102     >> Cases_on `l` >- RW_TAC std_ss [SNOC]
103     >> Cases_on `t'`
104     >- (RW_TAC std_ss [SNOC]
105         >> Q.EXISTS_TAC `[]`
106         >> RW_TAC std_ss [SNOC])
107     >> RW_TAC std_ss [SNOC]
108     >> Q.EXISTS_TAC `h''::t''`
109     >> RW_TAC std_ss [SNOC],
110     RW_TAC std_ss []
111     >> Q.EXISTS_TAC `h::l`
112     >> RW_TAC std_ss [SNOC]],
113    EQ_TAC >|
114    [STRIP_TAC
115     >> NTAC 2 (POP_ASSUM MP_TAC)
116     >> Cases_on `l` >- RW_TAC std_ss [SNOC]
117     >> Cases_on `t'`
118     >- (RW_TAC std_ss [SNOC]
119         >> Q.EXISTS_TAC `[]`
120         >> RW_TAC std_ss [SNOC])
121     >> RW_TAC std_ss [SNOC]
122     >> Q.EXISTS_TAC `h''::t''`
123     >> RW_TAC std_ss [SNOC],
124     RW_TAC std_ss []
125     >> Q.EXISTS_TAC `h::l`
126     >> RW_TAC std_ss [SNOC]]]);
127
128val PROB_TWIN_REDUCE = store_thm
129  ("PROB_TWIN_REDUCE",
130   ``!h t t'. prob_twin (h::t) (h::t') = prob_twin t t'``,
131   Cases_on `t`
132   >> RW_TAC std_ss [PROB_TWIN_CONS, PROB_TWIN_SING, PROB_TWIN_NIL]
133   >> PROVE_TAC []);
134
135val PROB_TWINS_PREFIX = store_thm
136  ("PROB_TWINS_PREFIX",
137   ``!x l. IS_PREFIX x l
138           ==> (x = l) \/ IS_PREFIX x (SNOC T l) \/ IS_PREFIX x (SNOC F l)``,
139   Induct_on `x` >- RW_TAC list_ss [IS_PREFIX_NIL]
140   >> Cases_on `l` >- RW_TAC list_ss [SNOC, IS_PREFIX]
141   >> RW_TAC list_ss [IS_PREFIX, SNOC]);
142
143val PROB_ORDER_NIL = store_thm
144  ("PROB_ORDER_NIL",
145   ``!x. prob_order [] x /\ (prob_order x [] = (x = []))``,
146   Induct >- RW_TAC list_ss [prob_order_def]
147   >> RW_TAC list_ss [prob_order_def]);
148
149val PROB_ORDER_REFL = store_thm
150  ("PROB_ORDER_REFL",
151   ``!x. prob_order x x``,
152   Induct >- RW_TAC list_ss [prob_order_def]
153   >> RW_TAC list_ss [prob_order_def]);
154
155val PROB_ORDER_ANTISYM = store_thm
156  ("PROB_ORDER_ANTISYM",
157   ``!x y. prob_order x y /\ prob_order y x ==> (x = y)``,
158   Induct >- (Cases >> RW_TAC list_ss [prob_order_def])
159   >> STRIP_TAC
160   >> Cases >- RW_TAC list_ss [prob_order_def]
161   >> (RW_TAC std_ss [prob_order_def] >> PROVE_TAC []));
162
163val PROB_ORDER_TRANS = store_thm
164  ("PROB_ORDER_TRANS",
165   ``!x y z. prob_order x y /\ prob_order y z ==> prob_order x z``,
166   Induct >- (Cases_on `z` >> RW_TAC list_ss [prob_order_def])
167   >> STRIP_TAC
168   >> Cases >- RW_TAC list_ss [prob_order_def]
169   >> Cases >- RW_TAC list_ss [prob_order_def]
170   >> (RW_TAC list_ss [prob_order_def] >> PROVE_TAC []));
171
172val PROB_ORDER_TOTAL = store_thm
173  ("PROB_ORDER_TOTAL",
174   ``!x y. prob_order x y \/ prob_order y x``,
175   Induct >- PROVE_TAC [PROB_ORDER_NIL]
176   >> Cases_on `y` >- PROVE_TAC [PROB_ORDER_NIL]
177   >> RW_TAC list_ss [prob_order_def]
178   >> PROVE_TAC []);
179
180val PROB_ORDER_PREFIX = store_thm
181  ("PROB_ORDER_PREFIX",
182   ``!x y. IS_PREFIX y x ==> prob_order x y``,
183   Induct >- (Cases >> RW_TAC list_ss [prob_order_def])
184   >> Cases_on `y` >- RW_TAC list_ss [IS_PREFIX_NIL]
185   >> RW_TAC list_ss [IS_PREFIX, prob_order_def]);
186
187val PROB_ORDER_PREFIX_ANTI = store_thm
188  ("PROB_ORDER_PREFIX_ANTI",
189   ``!x y. prob_order x y /\ IS_PREFIX x y ==> (x = y)``,
190   Induct >- RW_TAC list_ss [IS_PREFIX_NIL]
191   >> Cases_on `y` >- RW_TAC list_ss [IS_PREFIX_NIL, prob_order_def]
192   >> (RW_TAC list_ss [IS_PREFIX, prob_order_def]
193         >> PROVE_TAC []))
194
195val PROB_ORDER_PREFIX_MONO = store_thm
196  ("PROB_ORDER_PREFIX_MONO",
197   ``!x y z. prob_order x y /\ prob_order y z /\ IS_PREFIX z x
198             ==> IS_PREFIX y x``,
199   Induct >- RW_TAC list_ss [IS_PREFIX]
200   >> Cases_on `y` >- RW_TAC list_ss [prob_order_def]
201   >> Cases_on `z` >- RW_TAC list_ss [IS_PREFIX_NIL]
202   >> (RW_TAC list_ss [prob_order_def, IS_PREFIX]
203         >> PROVE_TAC []));
204
205val PROB_ORDER_PREFIX_TRANS = store_thm
206  ("PROB_ORDER_PREFIX_TRANS",
207   ``!x y z. prob_order x y /\ IS_PREFIX y z
208             ==> prob_order x z \/ IS_PREFIX x z``,
209   Induct >- (Cases_on `z` >> RW_TAC list_ss [prob_order_def])
210   >> Cases_on `y` >- RW_TAC list_ss [PROB_ORDER_NIL]
211   >> Cases_on `z` >- RW_TAC list_ss [IS_PREFIX]
212   >> (RW_TAC list_ss [prob_order_def, IS_PREFIX] >> PROVE_TAC []));
213
214val PROB_ORDER_SNOC = store_thm
215  ("PROB_ORDER_SNOC",
216   ``!x l. ~prob_order (SNOC x l) l``,
217   Induct_on `l` >- RW_TAC std_ss [prob_order_def, SNOC]
218   >> RW_TAC std_ss [prob_order_def, SNOC]);
219
220val PROB_SORTED_MIN = store_thm
221  ("PROB_SORTED_MIN",
222   ``!h t. prob_sorted (h::t) ==> (!x. MEM x t ==> prob_order h x)``,
223   Induct_on `t` >- RW_TAC list_ss [MEM]
224   >> RW_TAC list_ss [prob_sorted_def, MEM] >- PROVE_TAC []
225   >> Know `prob_order h x` >- PROVE_TAC []
226   >> PROVE_TAC [PROB_ORDER_TRANS]);
227
228val PROB_SORTED_DEF_ALT = store_thm
229  ("PROB_SORTED_DEF_ALT",
230   ``!h t. prob_sorted (h::t)
231           = (!x. MEM x t ==> prob_order h x) /\ prob_sorted t``,
232   REPEAT STRIP_TAC
233   >> EQ_TAC
234     >- (Cases_on `t` >> PROVE_TAC [PROB_SORTED_MIN, prob_sorted_def])
235   >> Cases_on `t` >- RW_TAC list_ss [prob_sorted_def]
236   >> RW_TAC list_ss [prob_sorted_def]
237   >> PROVE_TAC [MEM]);
238
239val PROB_SORTED_TL = store_thm
240  ("PROB_SORTED_TL",
241   ``!h t. prob_sorted (h::t) ==> prob_sorted t``,
242   PROVE_TAC [PROB_SORTED_DEF_ALT]);
243
244val PROB_SORTED_MONO = store_thm
245  ("PROB_SORTED_MONO",
246   ``!x y z. prob_sorted (x::y::z) ==> prob_sorted (x::z)``,
247   RW_TAC list_ss [PROB_SORTED_DEF_ALT, MEM]);
248
249val PROB_SORTED_TLS = store_thm
250  ("PROB_SORTED_TLS",
251   ``!l b. prob_sorted (MAP (CONS b) l) = prob_sorted l``,
252   Induct >- RW_TAC list_ss [MAP]
253   >> Cases_on `l` >- RW_TAC list_ss [MAP, prob_sorted_def]
254   >> RW_TAC list_ss [prob_sorted_def, prob_order_def]
255   >> PROVE_TAC [MAP]);
256
257val PROB_SORTED_STEP = store_thm
258  ("PROB_SORTED_STEP",
259   ``!l1 l2. prob_sorted (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))
260             = prob_sorted l1 /\ prob_sorted l2``,
261   NTAC 2 STRIP_TAC
262   >> Induct_on `l1` >- RW_TAC list_ss [MAP, PROB_SORTED_TLS, prob_sorted_def]
263   >> STRIP_TAC
264   >> POP_ASSUM MP_TAC
265   >> Cases_on `l1` >|
266   [Cases_on `l2` >- RW_TAC list_ss [MAP, prob_sorted_def]
267    >> RW_TAC list_ss [MAP, prob_sorted_def, prob_order_def],
268    RW_TAC list_ss [prob_sorted_def, prob_order_def]
269    >> PROVE_TAC []]);
270
271val PROB_SORTED_APPEND = store_thm
272  ("PROB_SORTED_APPEND",
273   ``!h h' t t'. prob_sorted (APPEND (h::t) (h'::t'))
274                 = prob_sorted (h::t) /\ prob_sorted (h'::t')
275                   /\ prob_order (LAST (h::t)) h'``,
276   Induct_on `t`
277     >- (RW_TAC list_ss [prob_sorted_def, LAST_CONS]
278         >> PROVE_TAC [])
279   >> RW_TAC list_ss [prob_sorted_def]
280   >> RW_TAC std_ss [(GSYM o CONJUNCT2) APPEND, LAST_CONS]
281   >> PROVE_TAC []);
282
283val PROB_SORTED_FILTER = store_thm
284  ("PROB_SORTED_FILTER",
285   ``!P b. prob_sorted b ==> prob_sorted (FILTER P b)``,
286   STRIP_TAC
287   >> Induct >- RW_TAC list_ss [FILTER]
288   >> RW_TAC list_ss [PROB_SORTED_DEF_ALT, FILTER]
289   >> PROVE_TAC [MEM_FILTER]);
290
291val PROB_PREFIXFREE_TL = store_thm
292  ("PROB_PREFIXFREE_TL",
293   ``!h t. prob_prefixfree (h::t) ==> prob_prefixfree t``,
294   STRIP_TAC
295   >> (Cases >> RW_TAC list_ss [prob_prefixfree_def]));
296
297val PROB_PREFIXFREE_MONO = store_thm
298  ("PROB_PREFIXFREE_MONO",
299   ``!x y z. prob_sorted (x::y::z) /\ prob_prefixfree (x::y::z)
300             ==> prob_prefixfree (x::z)``,
301   Cases_on `z` >- RW_TAC list_ss [prob_prefixfree_def]
302   >> RW_TAC list_ss [prob_prefixfree_def, prob_sorted_def]
303   >> PROVE_TAC [PROB_ORDER_PREFIX_MONO]);
304
305val PROB_PREFIXFREE_ELT = store_thm
306  ("PROB_PREFIXFREE_ELT",
307   ``!h t. prob_sorted (h::t) /\ prob_prefixfree (h::t)
308         ==> (!x. MEM x t ==> ~IS_PREFIX x h /\ ~IS_PREFIX h x)``,
309   Induct_on `t` >- RW_TAC list_ss [MEM]
310   >> ONCE_REWRITE_TAC [MEM]
311   >> NTAC 5 STRIP_TAC >|
312   [CONJ_TAC >- PROVE_TAC [prob_prefixfree_def]
313    >> Know `prob_order h' h` >- PROVE_TAC [prob_sorted_def]
314    >> PROVE_TAC [PROB_ORDER_PREFIX_ANTI, IS_PREFIX_REFL, prob_prefixfree_def],
315    Suff `prob_sorted (h'::t) /\ prob_prefixfree (h'::t)`
316      >- PROVE_TAC []
317    >> PROVE_TAC [PROB_SORTED_MONO, PROB_PREFIXFREE_MONO]]);
318
319val PROB_PREFIXFREE_TLS = store_thm
320  ("PROB_PREFIXFREE_TLS",
321   ``!l b. prob_prefixfree (MAP (CONS b) l) = prob_prefixfree l``,
322   Induct >- RW_TAC list_ss [MAP]
323   >> Cases_on `l` >- RW_TAC list_ss [MAP, prob_prefixfree_def]
324   >> RW_TAC list_ss [prob_prefixfree_def, IS_PREFIX]
325   >> PROVE_TAC [MAP]);
326
327val PROB_PREFIXFREE_STEP = store_thm
328  ("PROB_PREFIXFREE_STEP",
329   ``!l1 l2. prob_prefixfree (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))
330             = prob_prefixfree l1 /\ prob_prefixfree l2``,
331   NTAC 2 STRIP_TAC
332   >> Induct_on `l1`
333   >- RW_TAC list_ss [MAP, PROB_PREFIXFREE_TLS, prob_prefixfree_def]
334   >> STRIP_TAC
335   >> POP_ASSUM MP_TAC
336   >> Cases_on `l1` >|
337   [Cases_on `l2` >- RW_TAC list_ss [MAP, prob_prefixfree_def]
338    >> RW_TAC list_ss [MAP, prob_prefixfree_def, IS_PREFIX],
339    RW_TAC list_ss [prob_prefixfree_def, IS_PREFIX]
340    >> PROVE_TAC []]);
341
342val PROB_PREFIXFREE_APPEND = store_thm
343  ("PROB_PREFIXFREE_APPEND",
344   ``!h h' t t'. prob_prefixfree (APPEND (h::t) (h'::t'))
345                 = prob_prefixfree (h::t) /\ prob_prefixfree (h'::t')
346                   /\ ~IS_PREFIX h' (LAST (h::t))``,
347   Induct_on `t`
348     >- (RW_TAC list_ss [prob_prefixfree_def, LAST_CONS]
349         >> PROVE_TAC [])
350   >> RW_TAC list_ss [prob_prefixfree_def]
351   >> RW_TAC std_ss [(GSYM o CONJUNCT2) APPEND, LAST_CONS]
352   >> PROVE_TAC []);
353
354val PROB_PREFIXFREE_FILTER = store_thm
355  ("PROB_PREFIXFREE_FILTER",
356   ``!P b. prob_sorted b /\ prob_prefixfree b ==> prob_prefixfree (FILTER P b)``,
357   STRIP_TAC
358   >> Induct >- RW_TAC list_ss [FILTER]
359   >> NTAC 2 STRIP_TAC
360   >> Know `prob_prefixfree (FILTER P b)`
361     >- PROVE_TAC [PROB_SORTED_TL, PROB_PREFIXFREE_TL]
362   >> RW_TAC list_ss [FILTER]
363   >> Cases_on `FILTER P b` >- RW_TAC list_ss [prob_prefixfree_def]
364   >> RW_TAC list_ss [prob_prefixfree_def]
365   >> Know `MEM (h':bool list) b` >- PROVE_TAC [MEM_FILTER, MEM]
366   >> PROVE_TAC [PROB_PREFIXFREE_ELT]);
367
368val PROB_TWINFREE_TL = store_thm
369  ("PROB_TWINFREE_TL",
370   ``!h t. prob_twinfree (h::t) ==> prob_twinfree t``,
371   Cases_on `t` >> RW_TAC list_ss [prob_twinfree_def]);
372
373val PROB_TWINFREE_TLS = store_thm
374  ("PROB_TWINFREE_TLS",
375   ``!l b. prob_twinfree (MAP (CONS b) l) = prob_twinfree l``,
376   NTAC 2 STRIP_TAC
377   >> Induct_on `l` >- RW_TAC list_ss [MAP]
378   >> STRIP_TAC
379   >> Cases_on `l` >- RW_TAC std_ss [MAP, prob_twinfree_def]
380   >> POP_ASSUM MP_TAC
381   >> RW_TAC std_ss [MAP, prob_twinfree_def, prob_twin_def]
382   >> KILL_TAC
383   >> Suff `(?l. (b::h = SNOC T l) /\ (b::h' = SNOC F l))
384                = (?l. (h = SNOC T l) /\ (h' = SNOC F l))`
385   >- PROVE_TAC []
386   >> EQ_TAC >|
387   [RW_TAC std_ss []
388    >> NTAC 2 (POP_ASSUM MP_TAC)
389    >> Cases_on `l` >- RW_TAC std_ss [SNOC]
390    >> RW_TAC std_ss [SNOC]
391    >> PROVE_TAC [],
392    RW_TAC std_ss []
393    >> Q.EXISTS_TAC `b::l`
394    >> Cases_on `l`
395    >> RW_TAC std_ss [SNOC]]);
396
397val PROB_TWINFREE_STEP1 = store_thm
398  ("PROB_TWINFREE_STEP1",
399   ``!l1 l2. prob_twinfree (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))
400             ==> prob_twinfree l1 /\ prob_twinfree l2``,
401   NTAC 2 STRIP_TAC
402   >> Induct_on `l1`
403   >- RW_TAC list_ss [MAP, PROB_TWINFREE_TLS, prob_twinfree_def]
404   >> STRIP_TAC
405   >> POP_ASSUM MP_TAC
406   >> Cases_on `l1` >|
407   [Cases_on `l2` >- RW_TAC list_ss [MAP, prob_twinfree_def]
408    >> RW_TAC list_ss [MEM, MAP, prob_twinfree_def],
409    RW_TAC list_ss [prob_twinfree_def, PROB_TWIN_REDUCE, MEM]]);
410
411val PROB_TWINFREE_STEP2 = store_thm
412  ("PROB_TWINFREE_STEP2",
413   ``!l1 l2. (~(MEM [] l1) \/ ~(MEM [] l2))
414             /\ prob_twinfree l1 /\ prob_twinfree l2
415             ==> prob_twinfree (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))``,
416   NTAC 2 STRIP_TAC
417   >> Induct_on `l1`
418   >- RW_TAC list_ss [MAP, PROB_TWINFREE_TLS, prob_twinfree_def]
419   >> STRIP_TAC
420   >> POP_ASSUM MP_TAC
421   >> Cases_on `l1` >|
422   [Cases_on `l2` >- RW_TAC list_ss [MAP, prob_twinfree_def]
423    >> RW_TAC list_ss [MEM, MAP, prob_twinfree_def] >|
424    [Cases_on `h` >- RW_TAC std_ss []
425     >> RW_TAC std_ss [PROB_TWIN_CONS],
426     Cases_on `h'` >- RW_TAC std_ss []
427     >> RW_TAC std_ss [PROB_TWIN_CONS]],
428    RW_TAC list_ss [prob_twinfree_def, PROB_TWIN_REDUCE, MEM]
429    >> RES_TAC]);
430
431val PROB_TWINFREE_STEP = store_thm
432  ("PROB_TWINFREE_STEP",
433   ``!l1 l2. ~(MEM [] l1) \/ ~(MEM [] l2)
434             ==> (prob_twinfree (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))
435                  = prob_twinfree l1 /\ prob_twinfree l2)``,
436   PROVE_TAC [PROB_TWINFREE_STEP1, PROB_TWINFREE_STEP2]);
437
438val PROB_LONGEST_HD = store_thm
439  ("PROB_LONGEST_HD",
440   ``!h t. LENGTH h <= prob_longest (h::t)``,
441   Induct_on `t` >- RW_TAC arith_ss [prob_longest_def, FOLDR]
442   >> RW_TAC arith_ss [prob_longest_def, FOLDR]);
443
444val PROB_LONGEST_TL = store_thm
445  ("PROB_LONGEST_TL",
446   ``!h t. prob_longest t <= prob_longest (h::t)``,
447   Induct_on `t` >- RW_TAC arith_ss [prob_longest_def, FOLDR]
448   >> RW_TAC arith_ss [prob_longest_def, FOLDR]);
449
450val PROB_LONGEST_TLS = store_thm
451  ("PROB_LONGEST_TLS",
452   ``!h t b. prob_longest (MAP (CONS b) (h::t)) = SUC (prob_longest (h::t))``,
453   Induct_on `t`
454     >- RW_TAC arith_ss [prob_longest_def, FOLDR_MAP, FOLDR, LENGTH]
455   >> RW_TAC arith_ss [prob_longest_def]
456   >> ONCE_REWRITE_TAC [MAP]
457   >> ONCE_REWRITE_TAC [FOLDR]
458   >> REWRITE_TAC [GSYM prob_longest_def]
459   >> RW_TAC arith_ss [LENGTH]);
460
461val PROB_LONGEST_APPEND = store_thm
462  ("PROB_LONGEST_APPEND",
463   ``!l1 l2. prob_longest l1 <= prob_longest (APPEND l1 l2)
464             /\ prob_longest l2 <= prob_longest (APPEND l1 l2)``,
465   NTAC 2 STRIP_TAC
466   >> Induct_on `l1` >- RW_TAC arith_ss [APPEND, prob_longest_def, FOLDR]
467   >> REWRITE_TAC [APPEND, prob_longest_def, FOLDR]
468   >> REWRITE_TAC [GSYM prob_longest_def]
469   >> RW_TAC arith_ss []);
470
471val PROB_CANON_PREFS_HD = store_thm
472  ("PROB_CANON_PREFS_HD",
473   ``!l b. HD (prob_canon_prefs l b) = l``,
474   STRIP_TAC
475   >> Induct >- RW_TAC list_ss [prob_canon_prefs_def]
476   >> RW_TAC list_ss [prob_canon_prefs_def]);
477
478val PROB_CANON_PREFS_DELETES = store_thm
479  ("PROB_CANON_PREFS_DELETES",
480   ``!l b x. MEM x (prob_canon_prefs l b) ==> MEM x (l::b)``,
481   STRIP_TAC
482   >> Induct >- RW_TAC list_ss [prob_canon_prefs_def]
483   >> RW_TAC list_ss [prob_canon_prefs_def]
484   >> RES_TAC
485   >> POP_ASSUM MP_TAC
486   >> KILL_TAC
487   >> RW_TAC list_ss [MEM]
488   >> PROVE_TAC []);
489
490val PROB_CANON_PREFS_SORTED = store_thm
491  ("PROB_CANON_PREFS_SORTED",
492   ``!l b. prob_sorted (l::b) ==> prob_sorted (prob_canon_prefs l b)``,
493   STRIP_TAC
494   >> Induct >- RW_TAC list_ss [prob_canon_prefs_def]
495   >> RW_TAC list_ss [prob_canon_prefs_def]
496   >> PROVE_TAC [PROB_SORTED_MONO]);
497
498val PROB_CANON_PREFS_PREFIXFREE = store_thm
499  ("PROB_CANON_PREFS_PREFIXFREE",
500   ``!l b. prob_sorted b /\ prob_prefixfree b
501           ==> prob_prefixfree (prob_canon_prefs l b)``,
502   STRIP_TAC
503   >> Induct >- RW_TAC list_ss [prob_canon_prefs_def, prob_prefixfree_def]
504   >> RW_TAC list_ss [prob_canon_prefs_def, prob_prefixfree_def]
505   >> PROVE_TAC [PROB_SORTED_TL, PROB_PREFIXFREE_TL]);
506
507val PROB_CANON_PREFS_CONSTANT = store_thm
508  ("PROB_CANON_PREFS_CONSTANT",
509   ``!l b. prob_prefixfree (l::b)
510           ==> (prob_canon_prefs l b = l::b)``,
511   STRIP_TAC
512   >> Induct >- RW_TAC list_ss [prob_prefixfree_def, prob_canon_prefs_def]
513   >> RW_TAC list_ss [prob_prefixfree_def, prob_canon_prefs_def]);
514
515val PROB_CANON_FIND_HD = store_thm
516  ("PROB_CANON_FIND_HD",
517   ``!l h t. (HD (prob_canon_find l (h::t)) = l)
518             \/ (HD (prob_canon_find l (h::t)) = h)``,
519   Induct_on `t` >- RW_TAC list_ss [prob_canon_find_def, PROB_CANON_PREFS_HD]
520   >> RW_TAC list_ss [prob_canon_find_def, PROB_CANON_PREFS_HD]);
521
522val PROB_CANON_FIND_DELETES = store_thm
523  ("PROB_CANON_FIND_DELETES",
524   ``!l b x. MEM x (prob_canon_find l b) ==> MEM x (l::b)``,
525   STRIP_TAC
526   >> Induct >- RW_TAC list_ss [prob_canon_find_def]
527   >> RW_TAC list_ss [prob_canon_find_def, MEM] >-
528   (PROVE_TAC [MEM]) >-
529   (PROVE_TAC [MEM, PROB_CANON_PREFS_DELETES]));
530
531val PROB_CANON_FIND_SORTED = store_thm
532  ("PROB_CANON_FIND_SORTED",
533   ``!l b. prob_sorted b ==> prob_sorted (prob_canon_find l b)``,
534   STRIP_TAC
535   >> Induct >- RW_TAC list_ss [prob_canon_find_def, prob_sorted_def]
536   >> RW_TAC list_ss [prob_canon_find_def] >-
537   (POP_ASSUM MP_TAC
538    >> RW_TAC list_ss [PROB_SORTED_DEF_ALT]
539    >> PROVE_TAC [PROB_CANON_FIND_DELETES, MEM]) >-
540   (Suff `prob_sorted (l::h::b)` >- PROVE_TAC [PROB_CANON_PREFS_SORTED]
541    >> REWRITE_TAC [prob_sorted_def]
542    >> PROVE_TAC [PROB_ORDER_TOTAL]));
543
544val PROB_CANON_FIND_PREFIXFREE = store_thm
545  ("PROB_CANON_FIND_PREFIXFREE",
546   ``!l b. prob_sorted b /\ prob_prefixfree b
547           ==> prob_prefixfree (prob_canon_find l b)``,
548   STRIP_TAC
549   >> Induct >- RW_TAC list_ss [prob_canon_find_def, prob_prefixfree_def]
550   >> RW_TAC list_ss [prob_canon_find_def] >|
551   [Cases_on `b` >- RW_TAC list_ss [prob_prefixfree_def, prob_canon_find_def]
552    >> Cases_on `prob_canon_find l (h'::t)`
553      >- RW_TAC list_ss [prob_prefixfree_def, prob_canon_find_def]
554    >> reverse (RW_TAC list_ss [prob_prefixfree_def])
555      >- PROVE_TAC [PROB_SORTED_TL, PROB_PREFIXFREE_TL]
556    >> Suff `(h'' = h') \/ (h'' = (l:bool list))`
557      >- PROVE_TAC [prob_prefixfree_def]
558    >> POP_ASSUM MP_TAC
559    >> KILL_TAC
560    >> PROVE_TAC [PROB_CANON_FIND_HD, HD],
561    PROVE_TAC [PROB_CANON_PREFS_PREFIXFREE]]);
562
563val PROB_CANON_FIND_CONSTANT = store_thm
564  ("PROB_CANON_FIND_CONSTANT",
565   ``!l b. prob_sorted (l::b) /\ prob_prefixfree (l::b)
566           ==> (prob_canon_find l b = l::b)``,
567   STRIP_TAC
568   >> Cases >- RW_TAC list_ss [prob_canon_find_def]
569   >> STRIP_TAC
570   >> Know `~((l:bool list) = h)`
571     >- PROVE_TAC [prob_prefixfree_def, IS_PREFIX_REFL]
572   >> (RW_TAC list_ss [prob_canon_find_def, PROB_CANON_PREFS_CONSTANT]
573         >> PROVE_TAC [prob_sorted_def, PROB_ORDER_ANTISYM]));
574
575val PROB_CANON1_SORTED = store_thm
576  ("PROB_CANON1_SORTED",
577   ``!l. prob_sorted (prob_canon1 l)``,
578   REWRITE_TAC [prob_canon1_def]
579   >> Induct >- RW_TAC list_ss [FOLDR, prob_sorted_def]
580   >> RW_TAC list_ss [PROB_CANON_FIND_SORTED, FOLDR]);
581
582val PROB_CANON1_PREFIXFREE = store_thm
583  ("PROB_CANON1_PREFIXFREE",
584   ``!l. prob_prefixfree (prob_canon1 l)``,
585   Induct >- RW_TAC list_ss [prob_prefixfree_def, prob_canon1_def, FOLDR]
586   >> RW_TAC list_ss [prob_canon1_def, FOLDR]
587   >> RW_TAC list_ss [GSYM prob_canon1_def]
588   >> Know `prob_sorted (prob_canon1 l)` >- PROVE_TAC [PROB_CANON1_SORTED]
589   >> PROVE_TAC [PROB_CANON_FIND_PREFIXFREE]);
590
591val PROB_CANON1_CONSTANT = store_thm
592  ("PROB_CANON1_CONSTANT",
593   ``!l. prob_sorted l /\ prob_prefixfree l ==> (prob_canon1 l = l)``,
594   RW_TAC list_ss [prob_canon1_def]
595   >> Induct_on `l` >- RW_TAC list_ss [FOLDR]
596   >> RW_TAC list_ss [FOLDR]
597   >> PROVE_TAC [PROB_CANON_FIND_CONSTANT, PROB_SORTED_TL, PROB_PREFIXFREE_TL]);
598
599val PROB_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE = store_thm
600  ("PROB_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE",
601   ``!l b. prob_sorted (l::b) /\ prob_prefixfree (l::b) /\ prob_twinfree b
602           ==> prob_sorted (prob_canon_merge l b)
603               /\ prob_prefixfree (prob_canon_merge l b)
604               /\ prob_twinfree (prob_canon_merge l b)``,
605    Induct_on `b`
606 >- RW_TAC std_ss [prob_canon_merge_def, prob_twinfree_def]
607 >> NTAC 3 STRIP_TAC
608 >> Know `prob_twinfree b` >- PROVE_TAC [PROB_TWINFREE_TL]
609 >> RW_TAC std_ss [prob_canon_merge_def, prob_twinfree_def, prob_twin_def] (* 3 sub-goals here *)
610 >> (Know `prob_sorted (l'::b)`
611     >- (Know `prob_sorted (SNOC T l'::b)`
612         >- PROVE_TAC [PROB_SORTED_MONO]
613         >> Cases_on `b` >- RW_TAC std_ss [prob_sorted_def]
614         >> POP_ASSUM MP_TAC
615         >> RW_TAC std_ss [prob_sorted_def]
616         >> Suff `prob_order l' (SNOC T l')`
617         >- PROVE_TAC [PROB_ORDER_TRANS]
618         >> MATCH_MP_TAC PROB_ORDER_PREFIX
619         >> RW_TAC std_ss [IS_PREFIX_SNOC, IS_PREFIX_REFL]) \\
620     Know `prob_prefixfree (l'::b)`
621     >- (Know `prob_prefixfree (SNOC T l'::b)`
622         >- PROVE_TAC [PROB_PREFIXFREE_MONO]
623         >> Cases_on `b` >- RW_TAC std_ss [prob_prefixfree_def]
624         >> POP_ASSUM MP_TAC
625         >> Q.PAT_X_ASSUM `prob_prefixfree X` MP_TAC
626         >> Q.PAT_X_ASSUM `prob_sorted (SNOC T X::Y)` MP_TAC
627         >> RW_TAC std_ss [prob_prefixfree_def, prob_sorted_def]
628         >> STRIP_TAC
629         >> MP_TAC (Q.SPECL [`h`, `l'`] PROB_TWINS_PREFIX)
630         >> RW_TAC std_ss []
631         >> STRIP_TAC
632         >> Q.PAT_X_ASSUM `prob_order (SNOC F l') h` MP_TAC
633         >> RW_TAC std_ss [PROB_ORDER_SNOC]) \\
634     RW_TAC std_ss [BUTLAST]) );
635
636val PROB_CANON_MERGE_PREFIXFREE_PRESERVE = store_thm
637  ("PROB_CANON_MERGE_PREFIXFREE_PRESERVE",
638   ``!l b h. (!x. MEM x (l::b) ==> ~IS_PREFIX h x /\ ~IS_PREFIX x h)
639           ==> (!x. MEM x (prob_canon_merge l b)
640                    ==> ~IS_PREFIX h x /\ ~IS_PREFIX x h)``,
641   Induct_on `b` >- RW_TAC std_ss [MEM, prob_canon_merge_def, IS_PREFIX]
642   >> REWRITE_TAC [prob_canon_merge_def]
643   >> NTAC 5 STRIP_TAC
644   >> reverse (Cases_on `prob_twin l h`) >- ASM_REWRITE_TAC []
645   >> ASM_REWRITE_TAC []
646   >> POP_ASSUM MP_TAC
647   >> REWRITE_TAC [prob_twin_def]
648   >> NTAC 2 STRIP_TAC
649   >> Suff `!x. MEM x (BUTLAST h::b)
650                ==> ~IS_PREFIX h' x /\ ~IS_PREFIX x h'`
651     >- PROVE_TAC []
652   >> REWRITE_TAC [MEM]
653   >> reverse (NTAC 2 STRIP_TAC) >- PROVE_TAC [MEM]
654   >> ASM_REWRITE_TAC [BUTLAST]
655   >> reverse (Suff `~IS_PREFIX h' l /\ ~IS_PREFIX l h'
656                            /\ ~IS_PREFIX h' h /\ ~IS_PREFIX h h'`)
657   >- PROVE_TAC [MEM]
658   >> ASM_REWRITE_TAC []
659   >> KILL_TAC
660   >> RW_TAC std_ss [IS_PREFIX_SNOC]
661   >> PROVE_TAC [PROB_TWINS_PREFIX]);
662
663val PROB_CANON_MERGE_SHORTENS = store_thm
664  ("PROB_CANON_MERGE_SHORTENS",
665   ``!l b x. MEM x (prob_canon_merge l b)
666             ==> (?y. MEM y (l::b) /\ IS_PREFIX y x)``,
667   Induct_on `b` >- RW_TAC std_ss [prob_canon_merge_def, MEM, IS_PREFIX_REFL]
668   >> reverse (RW_TAC std_ss [prob_canon_merge_def, prob_twin_def])
669   >- PROVE_TAC [IS_PREFIX_REFL]
670   >> Q.PAT_X_ASSUM `!l. P l` (MP_TAC o Q.SPECL [`l'`, `x`])
671   >> POP_ASSUM MP_TAC
672   >> RW_TAC std_ss [BUTLAST, MEM] >|
673   [Q.EXISTS_TAC `SNOC F l'`
674    >> RW_TAC std_ss [IS_PREFIX_SNOC],
675    PROVE_TAC []]);
676
677val PROB_CANON_MERGE_CONSTANT = store_thm
678  ("PROB_CANON_MERGE_CONSTANT",
679   ``!l b. prob_twinfree (l::b) ==> (prob_canon_merge l b = l::b)``,
680   STRIP_TAC
681   >> Cases >- RW_TAC list_ss [prob_canon_merge_def]
682   >> RW_TAC list_ss [prob_twinfree_def, prob_canon_merge_def, PROB_TWIN_NIL]);
683
684val PROB_CANON2_PREFIXFREE_PRESERVE = store_thm
685  ("PROB_CANON2_PREFIXFREE_PRESERVE",
686   ``!l h. (!x. MEM x l ==> ~IS_PREFIX h x /\ ~IS_PREFIX x h)
687           ==> (!x. MEM x (prob_canon2 l)
688                    ==> ~IS_PREFIX h x /\ ~IS_PREFIX x h)``,
689   REWRITE_TAC [prob_canon2_def]
690   >> NTAC 2 STRIP_TAC
691   >> Induct_on `l` >- RW_TAC list_ss [FOLDR, MEM]
692   >> REWRITE_TAC [FOLDR, MEM]
693   >> NTAC 2 STRIP_TAC
694   >> Suff `!x. MEM x (h'::FOLDR prob_canon_merge [] l)
695                       ==> ~IS_PREFIX h x /\ ~IS_PREFIX x h`
696     >- PROVE_TAC [PROB_CANON_MERGE_PREFIXFREE_PRESERVE]
697   >> REWRITE_TAC [MEM]
698   >> PROVE_TAC []);
699
700val PROB_CANON2_SHORTENS = store_thm
701  ("PROB_CANON2_SHORTENS",
702   ``!l x. MEM x (prob_canon2 l) ==> ?y. MEM y l /\ IS_PREFIX y x``,
703   REWRITE_TAC [prob_canon2_def]
704   >> Induct >- RW_TAC list_ss [MEM, FOLDR]
705   >> RW_TAC list_ss [FOLDR]
706   >> Know
707           `?y. IS_PREFIX y x /\ MEM y (h::(FOLDR prob_canon_merge [] l))`
708     >- PROVE_TAC [PROB_CANON_MERGE_SHORTENS]
709   >> POP_ASSUM MP_TAC
710   >> RW_TAC list_ss [MEM] >- PROVE_TAC []
711   >> Know `?y''. MEM y'' l /\ IS_PREFIX (y'':bool list) y`
712     >- PROVE_TAC []
713   >> PROVE_TAC [IS_PREFIX_TRANS]);
714
715val PROB_CANON2_SORTED_PREFIXFREE_TWINFREE = store_thm
716  ("PROB_CANON2_SORTED_PREFIXFREE_TWINFREE",
717   ``!l. prob_sorted l /\ prob_prefixfree l
718         ==> prob_sorted (prob_canon2 l)
719             /\ prob_prefixfree (prob_canon2 l)
720             /\ prob_twinfree (prob_canon2 l)``,
721   REWRITE_TAC [prob_canon2_def]
722   >> Induct
723   >- RW_TAC list_ss [FOLDR, prob_sorted_def, prob_prefixfree_def,
724                      prob_twinfree_def]
725   >> REWRITE_TAC [FOLDR]
726   >> NTAC 2 STRIP_TAC
727   >> Know `prob_sorted l /\ prob_prefixfree l`
728   >- PROVE_TAC [PROB_SORTED_TL, PROB_PREFIXFREE_TL]
729   >> STRIP_TAC
730   >> RES_TAC
731   >> Suff `prob_sorted (h::FOLDR prob_canon_merge [] l)
732                /\ prob_prefixfree (h::FOLDR prob_canon_merge [] l)`
733   >- PROVE_TAC [PROB_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE]
734   >> POP_ASSUM (K ALL_TAC)
735   >> NTAC 2 (POP_ASSUM MP_TAC) >> NTAC 2 (POP_ASSUM (K ALL_TAC))
736   >> NTAC 2 (POP_ASSUM MP_TAC) >> POP_ASSUM (K ALL_TAC)
737   >> Cases_on `FOLDR prob_canon_merge [] l`
738     >- RW_TAC list_ss [prob_sorted_def, prob_prefixfree_def]
739   >> NTAC 4 STRIP_TAC
740   >> Know `~IS_PREFIX h h' /\ ~IS_PREFIX h' (h:bool list)`
741     >- (Suff `!x. MEM x (prob_canon2 l)
742                        ==> ~IS_PREFIX h x /\ ~IS_PREFIX (x:bool list) h`
743           >- (REWRITE_TAC [prob_canon2_def] >> PROVE_TAC [MEM])
744         >> Suff
745             `!x. MEM x l ==> ~IS_PREFIX h x /\ ~IS_PREFIX (x:bool list) h`
746           >- PROVE_TAC [PROB_CANON2_PREFIXFREE_PRESERVE]
747         >> PROVE_TAC [PROB_PREFIXFREE_ELT])
748   >> RW_TAC list_ss [prob_sorted_def, prob_prefixfree_def]
749   >> Know `?x. MEM x l /\ IS_PREFIX x (h':bool list)`
750     >- (Know `MEM h' (prob_canon2 l)` >- PROVE_TAC [prob_canon2_def, MEM]
751         >> PROVE_TAC [PROB_CANON2_SHORTENS])
752   >> STRIP_TAC
753   >> Know `prob_order h x` >- PROVE_TAC [PROB_SORTED_DEF_ALT]
754   >> PROVE_TAC [PROB_ORDER_PREFIX_TRANS]);
755
756val PROB_CANON2_CONSTANT = store_thm
757  ("PROB_CANON2_CONSTANT",
758   ``!l. prob_twinfree l ==> (prob_canon2 l = l)``,
759   RW_TAC list_ss [prob_canon2_def]
760   >> Induct_on `l` >- RW_TAC list_ss [FOLDR]
761   >> RW_TAC list_ss [FOLDR]
762   >> PROVE_TAC [PROB_CANON_MERGE_CONSTANT, PROB_TWINFREE_TL]);
763
764val PROB_CANON_SORTED_PREFIXFREE_TWINFREE = store_thm
765  ("PROB_CANON_SORTED_PREFIXFREE_TWINFREE",
766   ``!l. prob_sorted (prob_canon l)
767         /\ prob_prefixfree (prob_canon l)
768         /\ prob_twinfree (prob_canon l)``,
769   RW_TAC list_ss [prob_canon_def,
770                   PROB_CANON1_SORTED, PROB_CANON1_PREFIXFREE,
771                   PROB_CANON2_SORTED_PREFIXFREE_TWINFREE]);
772
773val PROB_CANON_CONSTANT = store_thm
774  ("PROB_CANON_CONSTANT",
775   ``!l. prob_sorted l /\ prob_prefixfree l /\ prob_twinfree l
776         ==> (prob_canon l = l)``,
777   RW_TAC std_ss [prob_canon_def, PROB_CANON1_CONSTANT, PROB_CANON2_CONSTANT]);
778
779val PROB_CANON_IDEMPOT = store_thm
780  ("PROB_CANON_IDEMPOT",
781   ``!l. prob_canon (prob_canon l) = prob_canon l``,
782   STRIP_TAC
783   >> MP_TAC (Q.SPEC `l` PROB_CANON_SORTED_PREFIXFREE_TWINFREE)
784   >> RW_TAC std_ss [PROB_CANON_CONSTANT]);
785
786val PROB_CANONICAL_DEF_ALT = store_thm
787  ("PROB_CANONICAL_DEF_ALT",
788   ``!l. prob_canonical l
789         = prob_sorted l /\ prob_prefixfree l /\ prob_twinfree l``,
790   RW_TAC std_ss [prob_canonical_def]
791   >> EQ_TAC >|
792   [PROVE_TAC [PROB_CANON_SORTED_PREFIXFREE_TWINFREE],
793    PROVE_TAC [PROB_CANON_CONSTANT]]);
794
795val PROB_CANONICAL_BASIC = store_thm
796  ("PROB_CANONICAL_BASIC",
797   ``prob_canonical [] /\ prob_canonical [[]] /\ !x. prob_canonical [x]``,
798   RW_TAC list_ss [PROB_CANONICAL_DEF_ALT, prob_sorted_def,
799                   prob_prefixfree_def, prob_twinfree_def]);
800
801val PROB_CANON_BASIC = store_thm
802  ("PROB_CANON_BASIC",
803   ``(prob_canon [] = []) /\ (prob_canon [[]] = [[]])
804     /\ (!x. prob_canon [x] = [x])``,
805   PROVE_TAC [prob_canonical_def, PROB_CANONICAL_BASIC]);
806
807val PROB_CANONICAL_TL = store_thm
808  ("PROB_CANONICAL_TL",
809   ``!h t. prob_canonical (h::t) ==> prob_canonical t``,
810   RW_TAC std_ss [PROB_CANONICAL_DEF_ALT] >|
811   [PROVE_TAC [PROB_SORTED_TL],
812    PROVE_TAC [PROB_PREFIXFREE_TL],
813    PROVE_TAC [PROB_TWINFREE_TL]]);
814
815val PROB_CANONICAL_NIL_MEM = store_thm
816  ("PROB_CANONICAL_NIL_MEM",
817   ``!l. prob_canonical l /\ MEM [] l = (l = [[]])``,
818   RW_TAC std_ss []
819   >> reverse EQ_TAC >- RW_TAC std_ss [PROB_CANONICAL_BASIC, MEM]
820   >> Induct_on `l` >- RW_TAC std_ss [MEM]
821   >> NTAC 2 STRIP_TAC
822   >> Know `prob_canonical l` >- PROVE_TAC [PROB_CANONICAL_TL]
823   >> STRIP_TAC
824   >> Q.PAT_X_ASSUM `prob_canonical (h::l)` MP_TAC
825   >> Q.PAT_X_ASSUM `X ==> Y` MP_TAC
826   >> Q.PAT_X_ASSUM `MEM X Y` MP_TAC
827   >> Cases_on `l` >- RW_TAC std_ss [MEM]
828   >> RW_TAC std_ss [MEM, PROB_CANONICAL_DEF_ALT, prob_sorted_def,
829                     prob_prefixfree_def, PROB_ORDER_NIL, IS_PREFIX_NIL] >|
830   [RW_TAC std_ss [IS_PREFIX_NIL],
831    RW_TAC std_ss [IS_PREFIX_NIL, PROB_ORDER_NIL]
832    >> PROVE_TAC [],
833    RES_TAC
834    >> RW_TAC std_ss []
835    >> PROVE_TAC [MEM]]);
836
837val PROB_CANONICAL_TLS = store_thm
838  ("PROB_CANONICAL_TLS",
839   ``!l b. prob_canonical (MAP (CONS b) l) = prob_canonical l``,
840   RW_TAC list_ss [PROB_CANONICAL_DEF_ALT, PROB_SORTED_TLS, PROB_PREFIXFREE_TLS]
841   >> (EQ_TAC >> PROVE_TAC [PROB_TWINFREE_TLS]));
842
843val PROB_CANONICAL_STEP1 = store_thm
844  ("PROB_CANONICAL_STEP1",
845   ``!l1 l2. prob_canonical (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))
846             ==> prob_canonical l1 /\ prob_canonical l2``,
847   RW_TAC std_ss [PROB_CANONICAL_DEF_ALT, PROB_SORTED_STEP, PROB_PREFIXFREE_STEP]
848   >> PROVE_TAC [PROB_TWINFREE_STEP1]);
849
850val PROB_CANONICAL_STEP2 = store_thm
851  ("PROB_CANONICAL_STEP2",
852   ``!l1 l2. (~(l1 = [[]]) \/ ~(l2 = [[]]))
853             /\ prob_canonical l1 /\ prob_canonical l2
854             ==> prob_canonical (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))``,
855   NTAC 2 STRIP_TAC
856   >> DISCH_TAC
857   >> reverse (Suff `~(MEM [] l1) \/ ~(MEM [] l2)`)
858   >- PROVE_TAC [PROB_CANONICAL_NIL_MEM]
859   >> POP_ASSUM MP_TAC
860   >> RW_TAC std_ss [PROB_CANONICAL_DEF_ALT, PROB_SORTED_STEP,
861                     PROB_PREFIXFREE_STEP]
862   >> PROVE_TAC [PROB_TWINFREE_STEP2]);
863
864val PROB_CANONICAL_STEP = store_thm
865  ("PROB_CANONICAL_STEP",
866   ``!l1 l2. ~(l1 = [[]]) \/ ~(l2 = [[]])
867             ==> (prob_canonical (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))
868                  = prob_canonical l1 /\ prob_canonical l2)``,
869   PROVE_TAC [PROB_CANONICAL_STEP1, PROB_CANONICAL_STEP2]);
870
871val PROB_CANONICAL_CASES_THM = store_thm
872  ("PROB_CANONICAL_CASES_THM",
873   ``!l. prob_canonical l ==> (l = []) \/ (l = [[]])
874            \/ ?l1 l2. prob_canonical l1 /\ prob_canonical l2
875                       /\ (l = APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))``,
876   Induct >- PROVE_TAC []
877   >> Cases
878   >- (MP_TAC (SPEC ``([]:bool list)::l`` PROB_CANONICAL_NIL_MEM)
879       >> RW_TAC list_ss [MEM])
880   >> STRIP_TAC
881   >> Know `prob_canonical l` >- PROVE_TAC [PROB_CANONICAL_TL]
882   >> STRIP_TAC
883   >> RES_TAC >|
884   [RW_TAC std_ss []
885    >> Cases_on `h'` >|
886    [Q.EXISTS_TAC `[t]`
887     >> Q.EXISTS_TAC `[]`
888     >> RW_TAC list_ss [PROB_CANONICAL_BASIC],
889     Q.EXISTS_TAC `[]`
890     >> Q.EXISTS_TAC `[t]`
891     >> RW_TAC list_ss [PROB_CANONICAL_BASIC]],
892    Suff `F` >- PROVE_TAC []
893    >> Q.PAT_X_ASSUM `prob_canonical (X::Y)` MP_TAC
894    >> MP_TAC (Q.SPEC `(h'::t)::l` PROB_CANONICAL_NIL_MEM)
895    >> RW_TAC std_ss [MEM],
896    DISJ2_TAC
897    >> DISJ2_TAC
898    >> Cases_on `h'` >|
899    [Q.EXISTS_TAC `t::l1`
900     >> Q.EXISTS_TAC `l2`
901     >> RW_TAC list_ss []
902     >> Q.PAT_X_ASSUM `prob_canonical (X::APPEND Y Z)` MP_TAC
903     >> KILL_TAC
904     >> MP_TAC (Q.SPECL [`t::l1`, `l2`] PROB_CANONICAL_STEP1)
905     >> RW_TAC list_ss [MAP],
906     Q.EXISTS_TAC `l1`
907     >> Q.EXISTS_TAC `t::l2`
908     >> Cases_on `l1` >|
909     [RW_TAC list_ss []
910      >> Q.PAT_X_ASSUM `prob_canonical (X::APPEND Y Z)` MP_TAC
911      >> KILL_TAC
912      >> MP_TAC (Q.SPECL [`[]`, `t::l2`] PROB_CANONICAL_STEP1)
913      >> RW_TAC list_ss [MAP],
914      Suff `~prob_sorted ((F::t)::l)` >- PROVE_TAC [PROB_CANONICAL_DEF_ALT]
915      >> RW_TAC list_ss [MAP, prob_sorted_def, prob_order_def]]]]);
916
917val PROB_CANONICAL_CASES = store_thm
918  ("PROB_CANONICAL_CASES",
919   ``!P. P [] /\ P [[]]
920         /\ (!l1 l2. prob_canonical l1 /\ prob_canonical l2
921               /\ prob_canonical (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))
922               ==> P (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)))
923         ==> (!l. prob_canonical l ==> P l)``,
924   RW_TAC list_ss []
925   >> MP_TAC (SPEC ``l:bool list list`` PROB_CANONICAL_CASES_THM)
926   >> (RW_TAC list_ss [] >> PROVE_TAC []));
927
928val PROB_CANONICAL_INDUCT = store_thm
929  ("PROB_CANONICAL_INDUCT",
930   ``!P. P [] /\ P [[]]
931         /\ (!l1 l2. prob_canonical l1 /\ prob_canonical l2 /\ P l1 /\ P l2
932               /\ prob_canonical (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))
933               ==> P (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)))
934         ==> (!l. prob_canonical l ==> P l)``,
935   RW_TAC list_ss []
936   >> completeInduct_on `prob_longest l`
937   >> RW_TAC list_ss []
938   >> reverse (Suff `((l = []) \/ (l = [[]])) \/ ?l1 l2.
939            prob_canonical l1 /\ prob_canonical l2 /\
940            (l = APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))`)
941     >- (POP_ASSUM (MP_TAC
942                    o MP (SPEC ``l:bool list list`` PROB_CANONICAL_CASES_THM))
943         >> PROVE_TAC [])
944   >> DISCH_THEN DISJ_CASES_TAC >- PROVE_TAC []
945   >> POP_ASSUM MP_TAC
946   >> STRIP_TAC
947   >> Suff `P (l1:bool list list) /\ P l2` >- PROVE_TAC []
948   >> CONJ_TAC >|
949   [Cases_on `l1` >- PROVE_TAC []
950    >> Suff `prob_longest (h::t) < prob_longest l` >- PROVE_TAC []
951    >> POP_ASSUM MP_TAC
952    >> KILL_TAC
953    >> MP_TAC (SPECL [``MAP (CONS T) (h::t)``, ``MAP (CONS F) l2``]
954                 PROB_LONGEST_APPEND)
955    >> RW_TAC arith_ss [PROB_LONGEST_TLS],
956    Cases_on `l2` >- PROVE_TAC []
957    >> Suff `prob_longest (h::t) < prob_longest l` >- PROVE_TAC []
958    >> POP_ASSUM MP_TAC
959    >> KILL_TAC
960    >> MP_TAC (SPECL [``MAP (CONS T) l1``, ``MAP (CONS F) (h::t)``]
961                 PROB_LONGEST_APPEND)
962    >> RW_TAC arith_ss [PROB_LONGEST_TLS]]);
963
964val MEM_NIL_STEP = store_thm
965  ("MEM_NIL_STEP",
966   ``!l1 l2. ~MEM [] (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))``,
967   RW_TAC list_ss [APPEND_MEM, MEM_NIL_MAP_CONS]);
968
969val PROB_SORTED_PREFIXFREE_MEM_NIL = store_thm
970  ("PROB_SORTED_PREFIXFREE_MEM_NIL",
971   ``!l. prob_sorted l /\ prob_prefixfree l /\ MEM [] l = (l = [[]])``,
972   Induct >- RW_TAC list_ss [MEM]
973   >> STRIP_TAC
974   >> reverse EQ_TAC
975     >- RW_TAC std_ss [prob_prefixfree_def, prob_sorted_def, MEM]
976   >> Cases_on `l` >- RW_TAC list_ss [MEM]
977   >> ONCE_REWRITE_TAC [MEM]
978   >> RW_TAC std_ss [prob_prefixfree_def, prob_sorted_def]
979   >> Cases_on `h` >- RW_TAC list_ss [MEM, prob_order_def, IS_PREFIX]
980   >> Cases_on `h'` >- RW_TAC list_ss [MEM, prob_order_def]
981   >> RW_TAC list_ss [] >|
982   [RW_TAC list_ss [],
983    RW_TAC list_ss [],
984    RW_TAC list_ss []]);
985
986val PROB_SORTED_PREFIXFREE_EQUALITY = store_thm
987  ("PROB_SORTED_PREFIXFREE_EQUALITY",
988   ``!l l'. (!x. MEM x l = MEM x l') /\ prob_sorted l /\ prob_sorted l'
989            /\ prob_prefixfree l /\ prob_prefixfree l'
990            ==> (l = l')``,
991   Induct >- RW_TAC list_ss [MEM, MEM_NIL]
992   >> STRIP_TAC
993   >> Cases >- (RW_TAC std_ss [MEM, MEM_NIL] >> PROVE_TAC [])
994   >> REPEAT STRIP_TAC
995   >> Know `h = h'` >|
996   [Suff `prob_order h h' /\ prob_order h' h` >- PROVE_TAC [PROB_ORDER_ANTISYM]
997    >> CONJ_TAC >|
998    [Know `MEM h' (h::l)` >- PROVE_TAC [MEM]
999     >> REWRITE_TAC [MEM]
1000     >> RW_TAC std_ss [] >- PROVE_TAC [PROB_ORDER_REFL]
1001     >> Q.PAT_X_ASSUM `prob_sorted (h::l)` MP_TAC
1002     >> RW_TAC std_ss [PROB_SORTED_DEF_ALT],
1003     Know `MEM h (h'::t)` >- PROVE_TAC [MEM]
1004     >> REWRITE_TAC [MEM]
1005     >> RW_TAC std_ss [] >- PROVE_TAC [PROB_ORDER_REFL]
1006     >> Q.PAT_X_ASSUM `prob_sorted (h'::t)` MP_TAC
1007     >> RW_TAC std_ss [PROB_SORTED_DEF_ALT]],
1008    RW_TAC std_ss []
1009    >> Q.PAT_X_ASSUM `!l'. P l' ==> Q l'` MATCH_MP_TAC
1010    >> reverse CONJ_TAC >- PROVE_TAC [PROB_SORTED_TL, PROB_PREFIXFREE_TL]
1011    >> RW_TAC std_ss []
1012    >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`)
1013    >> REWRITE_TAC [MEM]
1014    >> reverse (Cases_on `x = h`) >- RW_TAC std_ss []
1015    >> RW_TAC std_ss []
1016    >> ASSUME_TAC PROB_PREFIXFREE_ELT
1017    >> RES_TAC
1018    >> NTAC 2 (POP_ASSUM (MP_TAC o Q.SPEC `h`))
1019    >> NTAC 3 (POP_ASSUM (K ALL_TAC))
1020    >> RW_TAC std_ss [IS_PREFIX_REFL]]);
1021
1022val PROB_CANONICAL_PREFIXFREE = store_thm
1023  ("PROB_CANONICAL_PREFIXFREE",
1024   ``!l a b.
1025       prob_canonical l /\ MEM a l /\ MEM b l /\ IS_PREFIX a b ==> (a = b)``,
1026   Induct >- RW_TAC std_ss [MEM]
1027   >> RW_TAC std_ss [MEM] >|
1028   [Know `prob_sorted (a::l) /\ prob_prefixfree (a::l)`
1029    >- PROVE_TAC [prob_canonical_def, PROB_CANON_SORTED_PREFIXFREE_TWINFREE]
1030    >> RW_TAC std_ss []
1031    >> MP_TAC (Q.SPECL [`a`, `l`] PROB_PREFIXFREE_ELT)
1032    >> RW_TAC std_ss []
1033    >> RES_TAC,
1034    Know `prob_sorted (b::l) /\ prob_prefixfree (b::l)`
1035    >- PROVE_TAC [prob_canonical_def, PROB_CANON_SORTED_PREFIXFREE_TWINFREE]
1036    >> RW_TAC std_ss []
1037    >> MP_TAC (Q.SPECL [`b`, `l`] PROB_PREFIXFREE_ELT)
1038    >> RW_TAC std_ss []
1039    >> RES_TAC,
1040    PROVE_TAC [PROB_CANONICAL_TL]]);
1041
1042val _ = export_theory ();
1043