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