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