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