1open HolKernel Parse boolLib Drule BasicProvers 2open simpLib TotalDefn ConseqConv numLib 3open quantHeuristicsLib 4open optionTheory 5open listTheory 6open metisLib 7 8val _ = new_theory "patternMatches" 9 10val std_ss = numLib.std_ss 11val list_ss = numLib.arith_ss ++ listSimps.LIST_ss 12val zDefine = Lib.with_flag (computeLib.auto_import_definitions,false) Define 13 14val _ = ParseExtras.temp_loose_equality() 15 16 17(***************************************************) 18(* Auxiliary stuff *) 19(***************************************************) 20 21val IS_SOME_OPTION_MAP = prove ( 22 ``!f v. IS_SOME (OPTION_MAP f v) = IS_SOME v``, 23Cases_on `v` THEN 24SIMP_TAC list_ss []) 25 26val some_eq_SOME = prove ( 27 ``!P x. ((some x. P x) = SOME x) ==> (P x)``, 28SIMP_TAC std_ss [some_def] THEN 29REPEAT STRIP_TAC THEN 30SELECT_ELIM_TAC THEN 31PROVE_TAC[]) 32 33val some_var_bool_T = store_thm ("some_var_bool_T", 34 ``(some x. x) = SOME T``, 35 `(some x. x) = (some x. (x = T))` by REWRITE_TAC[] THEN 36 ONCE_ASM_REWRITE_TAC[] THEN 37 PURE_REWRITE_TAC[optionTheory.some_EQ] THEN 38 REWRITE_TAC[] 39) 40 41val some_var_bool_F = store_thm ("some_var_bool_F", 42 ``(some x. ~x) = SOME F``, 43 `(some x. ~x) = (some x. (x = F))` by REWRITE_TAC[] THEN 44 ONCE_ASM_REWRITE_TAC[] THEN 45 PURE_REWRITE_TAC[optionTheory.some_EQ] THEN 46 REWRITE_TAC[] 47) 48 49val some_eq_NONE = prove ( 50 ``!P. ((some x. P x) = NONE) <=> (!x. ~(P x))``, 51SIMP_TAC std_ss [some_def]) 52 53val some_IS_SOME = prove ( 54 ``!P. (IS_SOME (some x. P x)) <=> (?x. P x)``, 55SIMP_TAC (std_ss++boolSimps.LIFT_COND_ss) [some_def]) 56 57val some_IS_SOME_EXISTS = prove ( 58 ``!P. (IS_SOME (some x. P x)) <=> (?x. P x /\ ((some x. P x) = SOME x))``, 59GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ( 60 ASM_SIMP_TAC std_ss [] 61) THEN 62Cases_on `some x. P x` THEN FULL_SIMP_TAC std_ss [] THEN 63MATCH_MP_TAC some_eq_SOME THEN 64ASM_REWRITE_TAC[]) 65 66val OPTION_MAP_EQ_OPTION_MAP = prove ( 67``(OPTION_MAP f x = OPTION_MAP f' x') = 68 (((x = NONE) /\ (x' = NONE)) \/ 69 (?y y'. (x = SOME y) /\ (x' = SOME y') /\ (f y = f' y')))``, 70 71Cases_on `x` THEN Cases_on `x'` THEN ( 72 SIMP_TAC std_ss [] 73)) 74 75 76(***************************************************) 77(* Main Definitions *) 78(***************************************************) 79 80(* rows of a case-expression consist of a 81 - pattern p 82 - guard g 83 - rhs r 84 85 A row matches an input value i with a variable 86 binding v, iff the following 87 predicate holds. *) 88val PMATCH_ROW_COND_def = zDefine `PMATCH_ROW_COND pat guard inp v = 89 (pat v = inp) /\ (guard v)` 90 91(* With this we can easily define the semantics of a row *) 92val PMATCH_ROW_def = zDefine `PMATCH_ROW pat guard rhs i = 93 (OPTION_MAP rhs (some v. PMATCH_ROW_COND pat guard i v))` 94 95 96(* We defined semantics of single rows. Let's extend 97 it to multiple ones, i.e. full pattern matches now. *) 98val PMATCH_INCOMPLETE_def = Define `PMATCH_INCOMPLETE = ARB` 99val PMATCH_def = zDefine ` 100 (PMATCH v [] = PMATCH_INCOMPLETE) /\ 101 (PMATCH v (r::rs) = option_CASE (r v) (PMATCH v rs) I)` 102 103 104(***************************************************) 105(* Constants for parsing magic *) 106(***************************************************) 107 108(* We need some dummy constant without any semnatic meaning 109 for setting up some parser magic. It is HOL 4 specific 110 and boring technical stuff. You can safely ignore the following. *) 111 112val _ = new_constant ("PMATCH_magic_1", type_of ``PMATCH``) 113 114val _ = new_constant ("PMATCH_ROW_magic_1", type_of 115 ``\abc. PMATCH_ROW (\x. FST (abc x)) (\x. FST (SND (abc x))) (\x. SND (SND ((abc x))))``) 116 117val _ = new_constant ("PMATCH_ROW_magic_0", type_of 118 ``\abc. PMATCH_ROW (\x:unit. FST abc) (\x. FST (SND abc)) (\x. SND (SND (abc)))``) 119 120val _ = new_constant ("PMATCH_ROW_magic_4", type_of 121 ``\abc. PMATCH_ROW (\x:unit. FST abc) (\x. FST (SND abc)) (\x. SND (SND (abc)))``) 122 123val _ = new_constant ("PMATCH_ROW_magic_2", type_of 124 ``\(pat:'a) (g:bool) (res:'b). (pat,g,res)``) 125 126val _ = new_constant ("PMATCH_ROW_magic_3", type_of 127 ``\(pat:'a) (res:'b). (pat,T,res)``) 128 129 130 131(***************************************************) 132(* Congruences for termination *) 133(***************************************************) 134 135(* Pattern matches expressed via PMATCH should 136 be usable in recursive function defintions. In order 137 to be able to do this, we need to set up some 138 congruence theorems that guide the automatic 139 wellfoundedness (termination) checker. *) 140 141val PMATCH_ROW_CONG = store_thm ("PMATCH_ROW_CONG", 142``!p p' g g' r r' v v'. 143 (p = p') /\ (v = v') /\ 144 (!x. (v = (p x)) ==> (g x = g' x)) /\ 145 (!x. ((v = (p x)) /\ (g x)) ==> 146 (r x = r' x)) ==> 147 (PMATCH_ROW p g r v = PMATCH_ROW p' g' r' v')``, 148 149REPEAT STRIP_TAC THEN 150ASM_SIMP_TAC (std_ss++boolSimps.CONJ_ss) [PMATCH_ROW_def, 151 PMATCH_ROW_COND_def] THEN 152Cases_on `some x. (p' x = v') /\ (g' x)` THEN ( 153 ASM_SIMP_TAC std_ss [] 154) THEN 155POP_ASSUM (fn thm => MP_TAC (HO_MATCH_MP (SPEC_ALL some_eq_SOME) thm)) THEN 156ASM_SIMP_TAC std_ss []) 157 158 159val PMATCH_CONG = store_thm ("PMATCH_CONG", 160``!v v' rows rows' r r'. ((v = v') /\ (r v' = r' v') /\ 161 (PMATCH v' rows = PMATCH v' rows')) ==> 162 (PMATCH v (r :: rows) = PMATCH v' (r' :: rows'))``, 163SIMP_TAC std_ss [PMATCH_def]) 164 165val _ = DefnBase.export_cong "PMATCH_ROW_CONG"; 166val _ = DefnBase.export_cong "PMATCH_CONG"; 167 168 169(***************************************************) 170(* Rewrites *) 171(***************************************************) 172 173val PMATCH_ROW_EQ_AUX = store_thm ("PMATCH_ROW_EQ_AUX", 174 ``((!i. (?x. PMATCH_ROW_COND p g i x) = 175 (?x'. PMATCH_ROW_COND p' g' i x')) /\ 176 (!x x'. ((p x = p' x') /\ g x /\ g' x') ==> (r x = r' x'))) ==> 177 (PMATCH_ROW p g r = PMATCH_ROW p' g' r')``, 178REPEAT STRIP_TAC THEN 179SIMP_TAC std_ss [FUN_EQ_THM, PMATCH_ROW_def, 180 OPTION_MAP_EQ_OPTION_MAP] THEN 181CONV_TAC (RENAME_VARS_CONV ["i"]) THEN 182GEN_TAC THEN 183Q.PAT_X_ASSUM `!i. (_ = _)` (fn thm => ASSUME_TAC (Q.SPEC `i` thm)) THEN 184Tactical.REVERSE (Cases_on `?x. PMATCH_ROW_COND p g i x`) THEN ( 185 FULL_SIMP_TAC std_ss [] 186) THEN 187DISJ2_TAC THEN 188`IS_SOME (some x. PMATCH_ROW_COND p g i x) /\ 189 IS_SOME (some x. PMATCH_ROW_COND p' g' i x)` by ( 190 ASM_SIMP_TAC std_ss [some_IS_SOME] THEN 191 PROVE_TAC[] 192) THEN 193FULL_SIMP_TAC std_ss [some_IS_SOME_EXISTS] THEN 194FULL_SIMP_TAC std_ss [PMATCH_ROW_COND_def]) 195 196val PMATCH_ROW_EQ_NONE = store_thm ("PMATCH_ROW_EQ_NONE", 197 ``(PMATCH_ROW p g r i = NONE) <=> 198 (!x. ~(PMATCH_ROW_COND p g i x))``, 199SIMP_TAC std_ss [PMATCH_ROW_def, some_eq_NONE]); 200 201val PMATCH_ROW_EQ_SOME = store_thm ("PMATCH_ROW_EQ_SOME", 202 ``(PMATCH_ROW p g r i = SOME y) ==> 203 (?x. (PMATCH_ROW_COND p g i x) /\ (y = r x))``, 204SIMP_TAC std_ss [PMATCH_ROW_def] THEN 205REPEAT STRIP_TAC THEN 206Q.EXISTS_TAC `z` THEN 207IMP_RES_TAC some_eq_SOME THEN 208ASM_SIMP_TAC std_ss []); 209 210 211val PMATCH_COND_SELECT_UNIQUE = store_thm ("PMATCH_COND_SELECT_UNIQUE", 212 ``!p g i. 213 (!x1 x2. (g x1 /\ g x2 /\ (p x1 = p x2)) ==> (x1 = x2)) ==> 214 !x. PMATCH_ROW_COND p g i x ==> 215 ((@y. PMATCH_ROW_COND p g i y) = x)``, 216 217SIMP_TAC std_ss [PMATCH_ROW_COND_def] THEN 218METIS_TAC[]); 219 220val PMATCH_ROW_COND_DEF_GSYM = store_thm ("PMATCH_ROW_COND_DEF_GSYM", 221 ``PMATCH_ROW_COND pat guard inp v = 222 ((inp = pat v) /\ (guard v))``, 223SIMP_TAC std_ss [PMATCH_ROW_COND_def] THEN 224PROVE_TAC[]) 225 226 227val PMATCH_EVAL = store_thm ("PMATCH_EVAL", 228 ``(PMATCH v [] = PMATCH_INCOMPLETE) /\ 229 (PMATCH v ((PMATCH_ROW p g r) :: rs) = 230 if (?x. (PMATCH_ROW_COND p g v x)) then 231 (r (@x. PMATCH_ROW_COND p g v x)) else PMATCH v rs)``, 232 233SIMP_TAC std_ss [PMATCH_def] THEN 234Cases_on `PMATCH_ROW p g r v` THENL [ 235 FULL_SIMP_TAC std_ss [PMATCH_ROW_def, some_eq_NONE], 236 237 FULL_SIMP_TAC std_ss [PMATCH_ROW_def, some_def] THEN 238 METIS_TAC[] 239]) 240 241val PMATCH_EVAL_MATCH = store_thm ("PMATCH_EVAL_MATCH", 242 ``~(PMATCH_ROW p g r v = NONE) ==> 243 (PMATCH v ((PMATCH_ROW p g r) :: rs) = 244 (r (@x. PMATCH_ROW_COND p g v x)))``, 245 246SIMP_TAC std_ss [PMATCH_EVAL, 247 PMATCH_ROW_EQ_NONE]); 248 249 250(***************************************************) 251(* Changing rows and removing redundant ones *) 252(***************************************************) 253 254(* For many of automatic methods, we need to show 255 that two PMATCH expressions which are derived from 256 each other by modifying or dropping rows are equivalent. 257 We want to perform these proofs in an a way that can be 258 automated nicely. In the following, we provide lemmata that 259 given an established equivalence, allow adding 260 a row to both or a single side. 261 By starting with an empty list and iterating, one can 262 use this method to construct the desired correspondance. *) 263val PMATCH_EXTEND_BASE = store_thm ("PMATCH_EXTEND_BASE", 264``!v_old v_new. (PMATCH v_old [] = PMATCH v_new [])``, 265SIMP_TAC std_ss [PMATCH_def]) 266 267val PMATCH_EXTEND_BOTH = store_thm ("PMATCH_EXTEND_BOTH", 268``!v_old v_new rows_old rows_new r_old r_new. 269 (r_old v_old = r_new v_new) ==> 270 (PMATCH v_old rows_old = PMATCH v_new rows_new) ==> 271 (PMATCH v_old (r_old::rows_old) = PMATCH v_new (r_new :: rows_new))``, 272SIMP_TAC std_ss [PMATCH_def]) 273 274val PMATCH_EXTEND_BOTH_ID = store_thm ("PMATCH_EXTEND_BOTH_ID", 275``!v rows_old rows_new r. 276 (PMATCH v rows_old = PMATCH v rows_new) ==> 277 (PMATCH v (r::rows_old) = PMATCH v (r :: rows_new))``, 278SIMP_TAC std_ss [PMATCH_def]) 279 280val PMATCH_EXTEND_OLD = store_thm ("PMATCH_EXTEND_OLD", 281``!v_old v_new rows_old rows_new r_old. 282 (r_old v_old = NONE) ==> 283 (PMATCH v_old rows_old = PMATCH v_new rows_new) ==> 284 (PMATCH v_old (r_old::rows_old) = PMATCH v_new rows_new)``, 285SIMP_TAC std_ss [PMATCH_def]) 286 287 288 289(***************************************************) 290(* Simplifying case expressions *) 291(***************************************************) 292 293(* We can now construct equivalences of case expressions, provided 294 we can reason about the semantics of single rows. So, 295 let's now consider useful theorems for single rows. *) 296 297(* Add an injective function to the pattern and the value. 298 This can be used to eliminate constructors. *) 299val PMATCH_ROW_REMOVE_FUN = store_thm ("PMATCH_ROW_REMOVE_FUN", 300``!ff v p g r. (!x y. (ff x = ff y) ==> (x = y)) ==> 301 302 (PMATCH_ROW (\x. (ff (p x))) g r (ff v) = 303 PMATCH_ROW (\x. (p x)) g r v)``, 304 305REPEAT STRIP_TAC THEN 306`!x y. (ff x = ff y) = (x = y)` by PROVE_TAC[] THEN 307ASM_SIMP_TAC std_ss [PMATCH_ROW_def, PMATCH_ROW_COND_def]) 308 309 310(* The following lemma looks rather complicated. It is 311 intended to work together with PMATCH_ROW_REMOVE_FUN to 312 propagate information in the var cases. 313 314 as an example consider 315 316 val t = ``PMATCH (SOME x, y) [ 317 PMATCH_ROW (\x. (SOME x, 0)) (K T) (\x. (SOME (x + y))); 318 PMATCH_ROW (\(x', y). (x', y)) (K T) (\(x', y). x') 319 ]`` 320 321 We want to simplify this to 322 323 val t = ``PMATCH (x, y) [ 324 PMATCH_ROW (\x. (x, 0)) (K T) (\x. (SOME (x + y))); 325 PMATCH_ROW (\(x'', y). (x'', y)) (K T) (\(x'', y). SOME x'') 326 ]`` 327 328 This is done via PMATCH_ROWS_SIMP and PMATCH_ROWS_SIMP_SOUNDNESS. 329 We need to show that the rows correspond to each other. 330 331 For the first row, PMATCH_ROW_REMOVE_FUN is used with 332 333 v := (x, y) 334 ff (x, y) := (SOME x, y) 335 336 p x := (x, 0) 337 r x := SOME (x + y) 338 339 340 For the second row, PMATCH_ROW_REMOVE_FUN is used with 341 342 v := (SOME x, y) 343 v' := (x, y) 344 p (x', y) := (x', y) 345 r (x', y) := x' 346 p' (x'', y) = (x'', y) 347 f (x'', y) := (SOME x'', y) 348*) 349 350val PMATCH_ROW_EXTEND_INPUT = store_thm ("PMATCH_ROW_EXTEND_INPUT", 351``!v v' f' f p g r p' . 352 ((!x'. (v' = p' x') ==> (p (f x') = v)) /\ 353 (!x. (v = p x) ==> ?x'. (p' x' = v')) /\ 354 (!x y. (p x = p y) ==> (x = y))) ==> 355 (PMATCH_ROW p (g (f' v')) (r (f' v')) v = 356 PMATCH_ROW p' (\x. g (f' (p' x)) (f x)) (\x. r (f' (p' x)) (f x)) v')``, 357 358REPEAT STRIP_TAC THEN 359ASM_SIMP_TAC std_ss [PMATCH_ROW_def] THEN 360`IS_SOME (some x. PMATCH_ROW_COND p' (\x. g (f' (p' x)) (f x)) v' x) = 361 IS_SOME (some x. PMATCH_ROW_COND p (g (f' v')) v x)` by ( 362 ASM_SIMP_TAC std_ss [some_IS_SOME, PMATCH_ROW_COND_def] THEN 363 METIS_TAC[] 364) THEN 365Tactical.REVERSE (Cases_on `IS_SOME (some x. PMATCH_ROW_COND p (g (f' v')) v x)`) THEN ( 366 FULL_SIMP_TAC std_ss [] 367) THEN 368FULL_SIMP_TAC std_ss [some_IS_SOME_EXISTS] THEN 369FULL_SIMP_TAC std_ss [PMATCH_ROW_COND_def] THEN 370METIS_TAC[]); 371 372 373val PMATCH_ROW_REMOVE_FUN_VAR = store_thm ("PMATCH_ROW_REMOVE_FUN_VAR", 374``!v v' f p g r p' . 375 ((!x'. (v' = p' x') = (p (f x') = v)) /\ 376 ((!x. (v = p x) ==> ?x'. f x' = x)) /\ 377 ((!x y. (p x = p y) ==> (x = y)))) ==> 378 (PMATCH_ROW p g r v = 379 PMATCH_ROW p' (\x. g (f x)) (\x. r (f x)) v')``, 380 381REPEAT STRIP_TAC THEN 382ASM_SIMP_TAC std_ss [PMATCH_ROW_def] THEN 383`IS_SOME (some x. PMATCH_ROW_COND p' (\x. g (f x)) v' x) = 384 IS_SOME (some x. PMATCH_ROW_COND p g v x)` by ( 385 ASM_SIMP_TAC std_ss [some_IS_SOME, PMATCH_ROW_COND_def] THEN 386 METIS_TAC[] 387) THEN 388Tactical.REVERSE (Cases_on `IS_SOME (some x. PMATCH_ROW_COND p g v x)`) THEN ( 389 FULL_SIMP_TAC std_ss [] 390) THEN 391FULL_SIMP_TAC std_ss [some_IS_SOME_EXISTS] THEN 392FULL_SIMP_TAC std_ss [PMATCH_ROW_COND_def] THEN 393METIS_TAC[]); 394 395 396(***************************************************) 397(* Equivalent sets of rows *) 398(***************************************************) 399 400val PMATCH_EQUIV_ROWS_def = Define ` 401 PMATCH_EQUIV_ROWS v rows1 rows2 = ( 402 (PMATCH v rows1 = PMATCH v rows2) /\ 403 ((?r. MEM r rows1 /\ IS_SOME (r v)) = 404 (?r. MEM r rows2 /\ IS_SOME (r v))))` 405 406 407val PMATCH_EQUIV_ROWS_EQUIV_EXPAND = store_thm ("PMATCH_EQUIV_ROWS_EQUIV_EXPAND", 408 ``PMATCH_EQUIV_ROWS v rows1 rows2 = ( 409 PMATCH_EQUIV_ROWS v rows1 = PMATCH_EQUIV_ROWS v rows2)``, 410 411SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def, FUN_EQ_THM] THEN 412METIS_TAC[]) 413 414val PMATCH_EQUIV_ROWS_is_equiv_1 = store_thm ("PMATCH_EQUIV_ROWS_is_equiv_1", 415 ``(!v rows. (PMATCH_EQUIV_ROWS v rows rows))``, 416SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def]) 417 418 419val PMATCH_EQUIV_ROWS_is_equiv_2 = store_thm ("PMATCH_EQUIV_ROWS_is_equiv_2", 420 ``(!v rows1 rows2. ((PMATCH_EQUIV_ROWS v rows1 rows2) = 421 (PMATCH_EQUIV_ROWS v rows2 rows1)))``, 422SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def] THEN METIS_TAC[]) 423 424val PMATCH_EQUIV_ROWS_is_equiv_3 = store_thm ("PMATCH_EQUIV_ROWS_is_equiv_3", 425 ``(!v rows1 rows2 rows3. 426 (PMATCH_EQUIV_ROWS v rows1 rows2) ==> 427 (PMATCH_EQUIV_ROWS v rows2 rows3) ==> 428 (PMATCH_EQUIV_ROWS v rows1 rows3))``, 429SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def]); 430 431val PMATCH_EQUIV_ROWS_MATCH = store_thm ("PMATCH_EQUIV_ROWS_MATCH", 432 ``PMATCH_EQUIV_ROWS v rows1 rows2 ==> 433 (PMATCH v rows1 = PMATCH v rows2)``, 434SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def]) 435 436val PMATCH_APPEND_SEM = store_thm ("PMATCH_APPEND_SEM", 437 ``!v rows1 rows2. PMATCH v (rows1 ++ rows2) = ( 438 if (?r. MEM r rows1 /\ IS_SOME (r v)) then PMATCH v rows1 else PMATCH v rows2)``, 439REPEAT GEN_TAC THEN 440Induct_on `rows1` THEN1 ( 441 SIMP_TAC list_ss [] 442) THEN 443ASM_SIMP_TAC list_ss [PMATCH_def, RIGHT_AND_OVER_OR, EXISTS_OR_THM] THEN 444GEN_TAC THEN 445Cases_on `h v` THEN ( 446 ASM_SIMP_TAC std_ss [] 447)) 448 449val PMATCH_EQUIV_APPEND = store_thm ("PMATCH_EQUIV_APPEND", 450``!v rows1a rows1b rows2a rows2b. 451 (PMATCH_EQUIV_ROWS v rows1a rows1b) ==> 452 (PMATCH_EQUIV_ROWS v rows2a rows2b) ==> 453 (PMATCH_EQUIV_ROWS v (rows1a ++ rows2a) (rows1b ++ rows2b))``, 454REPEAT STRIP_TAC THEN 455FULL_SIMP_TAC list_ss [PMATCH_EQUIV_ROWS_def, RIGHT_AND_OVER_OR, 456 EXISTS_OR_THM, PMATCH_APPEND_SEM]); 457 458 459val PMATCH_EQUIV_ROWS_CONS_NONE = store_thm("PMATCH_EQUIV_ROWS_CONS_NONE", 460``(row v = NONE) ==> ( 461 PMATCH_EQUIV_ROWS v (row::rows) = 462 PMATCH_EQUIV_ROWS v rows)``, 463 464SIMP_TAC list_ss [GSYM PMATCH_EQUIV_ROWS_EQUIV_EXPAND, 465 PMATCH_EQUIV_ROWS_def, RIGHT_AND_OVER_OR, 466 EXISTS_OR_THM, PMATCH_def]) 467 468 469 470(***************************************************) 471(* Simple removal of redundant rows *) 472(***************************************************) 473 474(* If we have a row that matches, everything after it can be dropped *) 475val PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS_EQUIV = store_thm ("PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS_EQUIV", 476``!v rows n. ((n < LENGTH rows) /\ (IS_SOME ((EL n rows) v))) ==> 477 (PMATCH_EQUIV_ROWS v rows (TAKE (SUC n) rows))``, 478 479REPEAT STRIP_TAC THEN 480`PMATCH_EQUIV_ROWS v (TAKE (SUC n) rows ++ DROP (SUC n) rows) 481 (TAKE (SUC n) rows)` 482 suffices_by FULL_SIMP_TAC list_ss [] THEN 483 484SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def, PMATCH_APPEND_SEM] THEN 485SIMP_TAC list_ss [] THEN 486 487`?r. MEM r (TAKE (SUC n) rows) /\ IS_SOME (r v)` suffices_by METIS_TAC[] THEN 488Q.EXISTS_TAC `EL n (TAKE (SUC n) rows)` THEN 489ASM_SIMP_TAC list_ss [rich_listTheory.MEM_TAKE, rich_listTheory.EL_MEM, 490 listTheory.LENGTH_TAKE, rich_listTheory.EL_TAKE]); 491 492 493val PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS = store_thm ("PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS", 494``!v rows n. ((n < LENGTH rows) /\ (IS_SOME ((EL n rows) v))) ==> 495 (PMATCH v rows = PMATCH v (TAKE (SUC n) rows))``, 496 497REPEAT STRIP_TAC THEN 498MATCH_MP_TAC PMATCH_EQUIV_ROWS_MATCH THEN 499MATCH_MP_TAC PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS_EQUIV THEN 500ASM_REWRITE_TAC[]) 501 502 503 504(* A row is redundant, if (but not(!) only if) it is made 505 redundant by exactly one 506 row above. This is simple to test and often already very 507 helful. More fancy tests involving multiple rows follow below. *) 508val PMATCH_ROWS_DROP_REDUNDANT = store_thm ( 509 "PMATCH_ROWS_DROP_REDUNDANT", 510``!r1 r2 rows1 rows2 rows3 v. 511 (IS_SOME (r2 v) ==> IS_SOME (r1 v)) ==> 512 (PMATCH v (rows1 ++ (r1 :: rows2) ++ (r2 :: rows3)) = 513 PMATCH v (rows1 ++ (r1 :: rows2) ++ rows3))``, 514 515REPEAT STRIP_TAC THEN 516SIMP_TAC (list_ss++boolSimps.CONJ_ss) [PMATCH_APPEND_SEM, RIGHT_AND_OVER_OR, EXISTS_OR_THM] THEN 517 518Cases_on `?r. MEM r rows1 /\ IS_SOME (r v)` THEN ( 519 ASM_REWRITE_TAC [] 520) THEN 521Cases_on `IS_SOME (r1 v)` THEN ASM_REWRITE_TAC[] THEN 522Cases_on `?r. MEM r rows2 /\ IS_SOME (r v)` THEN ( 523 ASM_REWRITE_TAC [] 524) THEN 525FULL_SIMP_TAC std_ss [PMATCH_def]); 526 527 528val PMATCH_ROWS_DROP_REDUNDANT_PMATCH_ROWS = store_thm ( 529 "PMATCH_ROWS_DROP_REDUNDANT_PMATCH_ROWS", 530``!p g r p' g' r' rows1 rows2 rows3 v. 531 (!x'. (v = p' x') /\ (g' x') ==> (?x. (p' x' = p x) /\ (g x))) ==> 532 (PMATCH v (rows1 ++ (PMATCH_ROW p g r :: rows2) ++ (PMATCH_ROW p' g' r' :: rows3)) = 533 PMATCH v (rows1 ++ (PMATCH_ROW p g r :: rows2) ++ rows3))``, 534 535REPEAT STRIP_TAC THEN 536MATCH_MP_TAC PMATCH_ROWS_DROP_REDUNDANT THEN 537SIMP_TAC std_ss [PMATCH_ROW_def, optionTheory.some_def, 538 PMATCH_ROW_COND_def, IS_SOME_OPTION_MAP] THEN 539Cases_on `?x'. (p' x' = v) /\ g' x'` THEN ( 540 ASM_SIMP_TAC std_ss [] 541) THEN 542METIS_TAC[IS_SOME_DEF]); 543 544 545 546(***************************************************) 547(* Simple removal of subsumed rows *) 548(***************************************************) 549 550(* Some rows are not redundant in the classical sense, but can 551 safely be dropped nevertheless. A redundant row never matches, 552 because it is shaddowed by a previous row. One can also 553 drop rows, if a later row matches if they match and returns the 554 same value. I will call such rows subsumed. *) 555 556val PMATCH_ROWS_DROP_SUBSUMED = store_thm ( 557 "PMATCH_ROWS_DROP_SUBSUMED", 558``!r1 r2 rows1 rows2 rows3 v. 559 ((!x. (r1 v = SOME x) ==> (r2 v = SOME x)) /\ 560 (IS_SOME (r1 v) ==> EVERY (\row. (row v = NONE)) rows2)) ==> 561 (PMATCH v (rows1 ++ (r1 :: (rows2 ++ (r2 :: rows3)))) = 562 PMATCH v (rows1 ++ rows2 ++ (r2 :: rows3)))``, 563 564REPEAT STRIP_TAC THEN 565REWRITE_TAC [GSYM rich_listTheory.APPEND_ASSOC_CONS] THEN 566SIMP_TAC (list_ss++boolSimps.CONJ_ss) [PMATCH_APPEND_SEM, RIGHT_AND_OVER_OR, EXISTS_OR_THM] THEN 567 568Cases_on `?r. MEM r rows1 /\ IS_SOME (r v)` THEN ( 569 ASM_REWRITE_TAC [] 570) THEN 571Cases_on `?r. MEM r rows2 /\ IS_SOME (r v)` THEN ( 572 ASM_REWRITE_TAC [] 573) THENL [ 574 SIMP_TAC std_ss [PMATCH_def] THEN 575 Cases_on `r1 v` THEN ( 576 FULL_SIMP_TAC std_ss [EVERY_MEM] 577 ) THEN 578 RES_TAC THEN 579 FULL_SIMP_TAC std_ss [], 580 581 Cases_on `r1 v` THEN ( 582 ASM_SIMP_TAC std_ss [] 583 ) THEN 584 FULL_SIMP_TAC std_ss [PMATCH_def] 585]); 586 587val PMATCH_ROWS_DROP_SUBSUMED_PMATCH_ROWS = store_thm ( 588 "PMATCH_ROWS_DROP_SUBSUMED_PMATCH_ROWS", 589``!p g r p' g' r' rows1 rows2 rows3 v. 590 ((!x. (v = p x) /\ (g x) ==> (?x'. (p x = p' x') /\ (g' x'))) /\ 591 (!x x'. ((v = p x) /\ (p x = p' x') /\ g x /\ g' x') ==> 592 (r x = r' x')) /\ 593 (!x. ((v = p x) /\ (g x)) ==> EVERY (\row. (row (p x) = NONE)) rows2)) ==> 594 (PMATCH v (rows1 ++ (PMATCH_ROW p g r :: (rows2 ++ (PMATCH_ROW p' g' r' :: rows3)))) = 595 PMATCH v (rows1 ++ rows2 ++ (PMATCH_ROW p' g' r' :: rows3)))``, 596 597REPEAT STRIP_TAC THEN 598MATCH_MP_TAC PMATCH_ROWS_DROP_SUBSUMED THEN 599SIMP_TAC std_ss [PMATCH_ROW_def, optionTheory.some_def, 600 PMATCH_ROW_COND_def, IS_SOME_OPTION_MAP] THEN 601Cases_on `?x. (p x = v) /\ g x` THEN ( 602 ASM_SIMP_TAC std_ss [] 603) THEN 604REPEAT STRIP_TAC THENL [ 605 PROVE_TAC[], 606 607 SELECT_ELIM_TAC THEN 608 CONJ_TAC THEN1 PROVE_TAC[] THEN 609 REPEAT STRIP_TAC THEN 610 SELECT_ELIM_TAC THEN 611 PROVE_TAC[], 612 613 FULL_SIMP_TAC std_ss [] THEN 614 METIS_TAC[] 615]); 616 617 618(* A common case for removing subsumed rows 619 is removing ARB rows that are introduced by 620 translating a classical case-expression naively. *) 621val PMATCH_REMOVE_ARB = store_thm ("PMATCH_REMOVE_ARB", 622``!p g r v rows. 623 (!x. r x = ARB) ==> 624 (PMATCH v (SNOC (PMATCH_ROW p g r) rows) = 625 PMATCH v rows)``, 626 627Induct_on `rows` THENL [ 628 SIMP_TAC list_ss [PMATCH_EVAL, PMATCH_INCOMPLETE_def], 629 ASM_SIMP_TAC list_ss [PMATCH_def] 630]) 631 632(* Introduce explicit catch-all at end *) 633val PMATCH_INTRO_CATCHALL = store_thm ("PMATCH_INTRO_CATCHALL", 634``PMATCH v rows = PMATCH v (SNOC (PMATCH_ROW (\_0. _0) (\_0. T) (\_0. ARB)) rows)``, 635SIMP_TAC std_ss [PMATCH_REMOVE_ARB]); 636 637 638val PMATCH_REMOVE_ARB_NO_OVERLAP = store_thm ("PMATCH_REMOVE_ARB_NO_OVERLAP", 639``!v p g r rows1 rows2. 640 ((!x. (r x = ARB)) /\ 641 (!x. ((v = p x) /\ (g x)) ==> EVERY (\row. (row (p x) = NONE)) rows2)) ==> 642 (PMATCH v (rows1 ++ ((PMATCH_ROW p g r) :: rows2)) = 643 PMATCH v (rows1 ++ rows2))``, 644 645REPEAT STRIP_TAC THEN 646ONCE_REWRITE_TAC [PMATCH_INTRO_CATCHALL] THEN 647SIMP_TAC list_ss [SNOC_APPEND, 648 rich_listTheory.APPEND_ASSOC_CONS] THEN 649MATCH_MP_TAC PMATCH_ROWS_DROP_SUBSUMED_PMATCH_ROWS THEN 650ASM_SIMP_TAC std_ss []) 651 652 653 654(***************************************************) 655(* Fancy redundancy check *) 656(***************************************************) 657 658(* Let's first define when a row is redundant. 659 The predicate PMATCH_ROW_REDUNDANT v rs i holds, 660 iff row number i is redundant for input v in the 661 list of rows rs. *) 662val PMATCH_ROW_REDUNDANT_def = Define ` 663 PMATCH_ROW_REDUNDANT v rs i = ( 664 (i < LENGTH rs /\ (IS_SOME ((EL i rs) v) ==> 665 (?j. ((j < i) /\ IS_SOME ((EL j rs) v))))))`; 666 667val PMATCH_ROW_REDUNDANT_NIL = store_thm ("PMATCH_ROW_REDUNDANT_NIL", 668 ``PMATCH_ROW_REDUNDANT v [] i = F``, 669SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_def]); 670 671val PMATCH_ROW_REDUNDANT_0 = store_thm ("PMATCH_ROW_REDUNDANT_0", 672 ``PMATCH_ROW_REDUNDANT v (r::rs) 0 <=> (r v = NONE)``, 673SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_def]); 674 675val PMATCH_ROW_REDUNDANT_SUC = store_thm ("PMATCH_ROW_REDUNDANT_SUC", 676 ``!v r rs i. 677 PMATCH_ROW_REDUNDANT v (r::rs) (SUC i) <=> 678 (((~(r v = NONE)) /\ i < LENGTH rs) \/ PMATCH_ROW_REDUNDANT v rs i)``, 679 680SIMP_TAC (list_ss++boolSimps.EQUIV_EXTRACT_ss) [PMATCH_ROW_REDUNDANT_def] THEN 681REPEAT STRIP_TAC THEN 682EQ_TAC THENL [ 683 STRIP_TAC THEN 684 Cases_on `j` THENL [ 685 Cases_on `r v` THEN FULL_SIMP_TAC list_ss [], 686 687 Q.RENAME1_TAC `SUC j' < SUC i` THEN 688 DISJ2_TAC THEN 689 Q.EXISTS_TAC `j'` THEN 690 FULL_SIMP_TAC list_ss [] 691 ], 692 693 REPEAT STRIP_TAC THENL [ 694 Q.EXISTS_TAC `0` THEN 695 Cases_on `r v` THEN FULL_SIMP_TAC list_ss [], 696 697 Q.EXISTS_TAC `SUC j` THEN 698 FULL_SIMP_TAC list_ss [] 699 ] 700]); 701 702 703val PMATCH_ROW_REDUNDANT_APPEND_LT = store_thm ("PMATCH_ROW_REDUNDANT_APPEND_LT", 704 ``!v rs1 rs2 i. 705 i < LENGTH rs1 ==> 706 (PMATCH_ROW_REDUNDANT v (rs1 ++ rs2) i = 707 PMATCH_ROW_REDUNDANT v rs1 i)``, 708SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_def] THEN 709REPEAT STRIP_TAC THEN 710FULL_SIMP_TAC (list_ss++boolSimps.CONJ_ss) [rich_listTheory.EL_APPEND1]); 711 712val PMATCH_ROW_REDUNDANT_APPEND_GE = store_thm ("PMATCH_ROW_REDUNDANT_APPEND_GE", 713 ``!v rs1 rs2 i. 714 ~(i < LENGTH rs1) ==> 715 (PMATCH_ROW_REDUNDANT v (rs1 ++ rs2) i <=> ( 716 (~(EVERY (\r. r v = NONE) rs1) /\ 717 (i < LENGTH rs1 + LENGTH rs2)) \/ 718 PMATCH_ROW_REDUNDANT v rs2 (i - LENGTH rs1)))``, 719 720SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_def, MEM_EL, EXISTS_MEM, GSYM LEFT_EXISTS_AND_THM] THEN 721REPEAT STRIP_TAC THEN 722FULL_SIMP_TAC (list_ss++boolSimps.EQUIV_EXTRACT_ss) [arithmeticTheory.NOT_LESS, rich_listTheory.EL_APPEND2, 723 quantHeuristicsTheory.IS_SOME_EQ_NOT_NONE] THEN 724REPEAT STRIP_TAC THEN 725EQ_TAC THEN STRIP_TAC THENL [ 726 Cases_on `j < LENGTH rs1` THENL [ 727 FULL_SIMP_TAC list_ss [rich_listTheory.EL_APPEND1] THEN 728 METIS_TAC[], 729 730 FULL_SIMP_TAC list_ss [arithmeticTheory.NOT_LESS, rich_listTheory.EL_APPEND2] THEN 731 DISJ2_TAC THEN 732 Q.EXISTS_TAC `j - LENGTH rs1` THEN 733 FULL_SIMP_TAC arith_ss [] 734 ], 735 736 Q.RENAME1_TAC `j' < LENGTH rs1` THEN 737 Q.EXISTS_TAC `j'` THEN 738 ASM_SIMP_TAC arith_ss [rich_listTheory.EL_APPEND1], 739 740 741 Q.EXISTS_TAC `j + LENGTH rs1` THEN 742 ASM_SIMP_TAC list_ss [rich_listTheory.EL_APPEND2] 743]); 744 745 746(* We can accumulate redundancy information for all rows. 747 This is done via IS_REDUNDANT_ROWS_INFO v rows c infos. 748 If the n-th entry of list infos is true, then the n-th 749 row of rows is redundant for input v. If it is not true, 750 it may or may not be redundant. 751 752 The parameter c is used for accumulating information 753 of all rows already in the info. If none of the rows 754 in rows matches, c holds. *) 755val IS_REDUNDANT_ROWS_INFO_def = Define ` 756 IS_REDUNDANT_ROWS_INFO v rows c infos <=> ( 757 (LENGTH rows = LENGTH infos) /\ 758 (!i. i < LENGTH rows ==> EL i infos ==> 759 PMATCH_ROW_REDUNDANT v rows i) /\ 760 (EVERY (\r. r v = NONE) rows ==> c))` 761 762 763(* This setup allows to build up such an info 764 row by row. We start with a list of empty rows 765 and add new rows at the end using the information in c. *) 766val IS_REDUNDANT_ROWS_INFO_NIL = store_thm ( 767 "IS_REDUNDANT_ROWS_INFO_NIL", 768``!v. IS_REDUNDANT_ROWS_INFO v [] T []``, 769SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def]); 770 771 772val IS_REDUNDANT_ROWS_INFO_SNOC = store_thm ( 773 "IS_REDUNDANT_ROWS_INFO_SNOC", 774``!v rows c infos r i c'. 775 IS_REDUNDANT_ROWS_INFO v rows c infos ==> 776 ((r v = NONE) ==> c ==> c') ==> 777 (c ==> i ==> (r v = NONE)) ==> 778 IS_REDUNDANT_ROWS_INFO v (SNOC r rows) c' (SNOC i infos) 779``, 780 781REPEAT STRIP_TAC THEN 782FULL_SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def, SNOC_APPEND] THEN 783REPEAT STRIP_TAC THEN 784Cases_on `i' < LENGTH infos` THEN1 ( 785 FULL_SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_APPEND_LT, rich_listTheory.EL_APPEND1] 786) THEN 787 788`i' = LENGTH infos` by DECIDE_TAC THEN 789Cases_on `c` THEN FULL_SIMP_TAC list_ss [rich_listTheory.EL_APPEND2, PMATCH_ROW_REDUNDANT_APPEND_GE, 790 PMATCH_ROW_REDUNDANT_0] 791); 792 793 794(* However, we still need to specialise this for 795 rows of the from PMATCH_ROW. For this case, it is handy 796 to use an auxiliary definition. *) 797val PMATCH_ROW_COND_EX_def = Define `PMATCH_ROW_COND_EX i p g = 798?x. PMATCH_ROW_COND p g i x` 799 800 801val IS_REDUNDANT_ROWS_INFO_SNOC_PMATCH_ROW = store_thm ( 802 "IS_REDUNDANT_ROWS_INFO_SNOC_PMATCH_ROW", 803``!v rows c infos p g r c'. 804 IS_REDUNDANT_ROWS_INFO v rows c infos ==> 805 (~(PMATCH_ROW_COND_EX v p g) ==> (c = c')) ==> 806 IS_REDUNDANT_ROWS_INFO v (SNOC (PMATCH_ROW p g r) rows) c' (SNOC (c ==> ~(PMATCH_ROW_COND_EX v p g)) infos) 807``, 808 809REPEAT STRIP_TAC THEN 810MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] IS_REDUNDANT_ROWS_INFO_SNOC) THEN 811Q.EXISTS_TAC `c` THEN 812FULL_SIMP_TAC std_ss [PMATCH_ROW_EQ_NONE, PMATCH_ROW_COND_EX_def] THEN 813METIS_TAC[]) 814 815(* A rewrite rule useful for proofs. *) 816val IS_REDUNDANT_ROWS_INFO_CONS = store_thm ( 817 "IS_REDUNDANT_ROWS_INFO_CONS", 818`` 819 IS_REDUNDANT_ROWS_INFO v (row::rows) c (i::infos') = ( 820 (LENGTH rows = LENGTH infos') /\ 821 (i ==> ((row v) = NONE)) /\ 822 ((row v = NONE) ==> IS_REDUNDANT_ROWS_INFO v rows c infos') 823)``, 824 825EQ_TAC THEN SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def] THEN 826REPEAT STRIP_TAC THENL [ 827 Q.PAT_X_ASSUM `!i'. _` (MP_TAC o SPEC ``0``) THEN 828 ASM_SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_0], 829 830 Q.PAT_X_ASSUM `!i'. _` (MP_TAC o Q.SPEC `SUC i'`) THEN 831 FULL_SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_SUC], 832 833 sg `(i'=0) \/ (?i''. (i' = SUC i''))` THENL [ 834 Cases_on `i'` THEN SIMP_TAC std_ss [], 835 FULL_SIMP_TAC list_ss [], 836 ALL_TAC 837 ] THEN 838 FULL_SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_0, PMATCH_ROW_REDUNDANT_SUC] THEN 839 Tactical.REVERSE (Cases_on `row v`) THEN ( 840 FULL_SIMP_TAC std_ss [] 841 ) 842]) 843 844 845(* We can use such a REDUNDANT_ROWS_INFO to prune 846 the a pattern match *) 847 848val APPLY_REDUNDANT_ROWS_INFO_def = Define ` 849 (APPLY_REDUNDANT_ROWS_INFO is xs = MAP SND ( 850 FILTER (\x. ~ (FST x)) (ZIP (is, xs))))` 851 852val APPLY_REDUNDANT_ROWS_INFO_THMS = store_thm ( 853 "APPLY_REDUNDANT_ROWS_INFO_THMS", 854``(APPLY_REDUNDANT_ROWS_INFO [] [] = []) /\ 855 (!is x xs. (APPLY_REDUNDANT_ROWS_INFO (T::is) (x::xs) = 856 (APPLY_REDUNDANT_ROWS_INFO is xs))) /\ 857 (!is x xs. (APPLY_REDUNDANT_ROWS_INFO (F::is) (x::xs) = 858 x::(APPLY_REDUNDANT_ROWS_INFO is xs)))``, 859 860SIMP_TAC list_ss [APPLY_REDUNDANT_ROWS_INFO_def]); 861 862 863val PMATCH_ROWS_DROP_REDUNDANT_ROWS_INFO_EQUIV = store_thm ("PMATCH_ROWS_DROP_REDUNDANT_ROWS_INFO_EQUIV", 864``!v c rows infos. IS_REDUNDANT_ROWS_INFO v rows c infos ==> 865 (PMATCH_EQUIV_ROWS v rows (APPLY_REDUNDANT_ROWS_INFO infos rows))``, 866 867GEN_TAC THEN 868Induct_on `rows` THEN1 ( 869 SIMP_TAC (list_ss++QUANT_INST_ss [std_qp]) [ 870 IS_REDUNDANT_ROWS_INFO_def, 871 APPLY_REDUNDANT_ROWS_INFO_def, 872 PMATCH_EQUIV_ROWS_is_equiv_1] 873) THEN 874CONV_TAC (RENAME_VARS_CONV ["row"]) THEN 875REPEAT STRIP_TAC THEN 876`?i infos'. infos = i::infos'` by ( 877 Cases_on `infos` THEN 878 FULL_SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def] 879) THEN 880FULL_SIMP_TAC std_ss [IS_REDUNDANT_ROWS_INFO_CONS] THEN 881Q.PAT_X_ASSUM `!c infos. _` (MP_TAC o Q.SPECL [`c`, `infos'`]) THEN 882Cases_on `i` THENL [ 883 FULL_SIMP_TAC std_ss [APPLY_REDUNDANT_ROWS_INFO_THMS, 884 PMATCH_EQUIV_ROWS_CONS_NONE], 885 886 Cases_on `row v` THEN ( 887 FULL_SIMP_TAC std_ss [APPLY_REDUNDANT_ROWS_INFO_THMS, 888 PMATCH_EQUIV_ROWS_CONS_NONE, PMATCH_EQUIV_ROWS_EQUIV_EXPAND] 889 ) THEN 890 STRIP_TAC THEN 891 ASM_SIMP_TAC list_ss [PMATCH_EQUIV_ROWS_def, 892 GSYM PMATCH_EQUIV_ROWS_EQUIV_EXPAND, RIGHT_AND_OVER_OR, 893 EXISTS_OR_THM, PMATCH_def] 894]) 895 896val REDUNDANT_ROWS_INFO_TO_PMATCH_EQ = store_thm ("REDUNDANT_ROWS_INFO_TO_PMATCH_EQ", 897``!v c rows infos. IS_REDUNDANT_ROWS_INFO v rows c infos ==> 898 (PMATCH v rows = 899 PMATCH v (APPLY_REDUNDANT_ROWS_INFO infos rows))``, 900 901REPEAT STRIP_TAC THEN 902MATCH_MP_TAC PMATCH_EQUIV_ROWS_MATCH THEN 903MATCH_MP_TAC PMATCH_ROWS_DROP_REDUNDANT_ROWS_INFO_EQUIV THEN 904PROVE_TAC[]) 905 906 907(* We get exhautiveness information for free using 908 the accumulated information in c *) 909val PMATCH_IS_EXHAUSTIVE_def = Define ` 910 PMATCH_IS_EXHAUSTIVE v rs = ( 911 EXISTS (\r. IS_SOME (r v)) rs)` 912 913 914val PMATCH_IS_EXHAUSTIVE_REWRITES = store_thm ("PMATCH_IS_EXHAUSTIVE_REWRITES", `` 915 (!v. (PMATCH_IS_EXHAUSTIVE v [] = F)) /\ 916 917 (!v r rs. (PMATCH_IS_EXHAUSTIVE v (r::rs) = 918 ~(r v = NONE) \/ PMATCH_IS_EXHAUSTIVE v rs))``, 919 920SIMP_TAC list_ss [PMATCH_IS_EXHAUSTIVE_def, 921quantHeuristicsTheory.IS_SOME_EQ_NOT_NONE]) 922 923 924val IS_REDUNDANT_ROWS_INFO_EXTRACT_IS_EXHAUSTIVE = 925 store_thm ("IS_REDUNDANT_ROWS_INFO_EXTRACT_IS_EXHAUSTIVE", 926 ``!v rows c infos. 927 IS_REDUNDANT_ROWS_INFO v rows c infos ==> 928 ~c ==> PMATCH_IS_EXHAUSTIVE v rows``, 929 930SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def, 931 PMATCH_IS_EXHAUSTIVE_def, combinTheory.o_DEF, 932 quantHeuristicsTheory.IS_SOME_EQ_NOT_NONE 933]) 934 935 936(* One can easily mark rows as not redundant without proof. 937 This is handy for avoiding complicated procedures to check, 938 whether some element of infos is true or false. If in doub 939 replace it with false. Technically this is done by 940 building a pairwise conjunction with a given list. *) 941val REDUNDANT_ROWS_INFOS_CONJ_def = Define ` 942 REDUNDANT_ROWS_INFOS_CONJ ip1 ip2 = 943 (MAP2 (\i1 i2. i1 /\ i2) ip1 ip2)`; 944 945val REDUNDANT_ROWS_INFOS_CONJ_REWRITE = store_thm ( 946 "REDUNDANT_ROWS_INFOS_CONJ_REWRITE", 947``(REDUNDANT_ROWS_INFOS_CONJ [] [] = []) /\ 948 (REDUNDANT_ROWS_INFOS_CONJ (i1 :: is1) (i2::is2) = 949 (i1 /\ i2) :: (REDUNDANT_ROWS_INFOS_CONJ is1 is2))``, 950SIMP_TAC list_ss [REDUNDANT_ROWS_INFOS_CONJ_def]) 951 952(* So, we can weaken an existing REDUNDANT_ROWS_INFOS *) 953val REDUNDANT_ROWS_INFOS_CONJ_THM = store_thm ("REDUNDANT_ROWS_INFOS_CONJ_THM", 954``!v rows c infos c' infos'. 955 IS_REDUNDANT_ROWS_INFO v rows c infos ==> 956 (LENGTH infos' = LENGTH infos) ==> 957 IS_REDUNDANT_ROWS_INFO v rows (c \/ c') (REDUNDANT_ROWS_INFOS_CONJ infos infos')``, 958 959SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def, 960 REDUNDANT_ROWS_INFOS_CONJ_def, MAP2_MAP, EL_MAP, EL_ZIP]) 961 962 963(* Strengthening requires proof though *) 964val REDUNDANT_ROWS_INFOS_DISJ_def = Define ` 965 REDUNDANT_ROWS_INFOS_DISJ ip1 ip2 = 966 (MAP2 (\i1 i2. i1 \/ i2) ip1 ip2)`; 967 968val REDUNDANT_ROWS_INFOS_DISJ_THM = store_thm ("REDUNDANT_ROWS_INFOS_DISJ_THM", 969``!v rows c infos c' infos'. 970 IS_REDUNDANT_ROWS_INFO v rows c infos ==> 971 IS_REDUNDANT_ROWS_INFO v rows c' infos' ==> 972 IS_REDUNDANT_ROWS_INFO v rows (c /\ c') (REDUNDANT_ROWS_INFOS_DISJ infos infos')``, 973 974SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def, 975 REDUNDANT_ROWS_INFOS_DISJ_def, MAP2_MAP, EL_MAP, EL_ZIP] THEN 976METIS_TAC[]) 977 978 979(* One can use the always correct, but usually much too complicated 980 strongest redundant_rows_info for strengthening *) 981 982val STRONGEST_REDUNDANT_ROWS_INFO_AUX_def = Define ` 983 (STRONGEST_REDUNDANT_ROWS_INFO_AUX v [] p infos = (p, infos)) /\ 984 (STRONGEST_REDUNDANT_ROWS_INFO_AUX v (r::rows) p infos = 985 STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows (p /\ (r v = NONE)) 986 (SNOC (p ==> (r v = NONE)) infos))` 987 988val STRONGEST_REDUNDANT_ROWS_INFO_def = Define ` 989 STRONGEST_REDUNDANT_ROWS_INFO v rows = 990 SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows T [])` 991 992val LENGTH_STRONGEST_REDUNDANT_ROWS_INFO_AUX = store_thm ( 993 "LENGTH_STRONGEST_REDUNDANT_ROWS_INFO_AUX", 994 ``!v rows p infos. 995 LENGTH (SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos)) = 996 (LENGTH rows + LENGTH infos)``, 997 998Induct_on `rows` THEN ( 999 ASM_SIMP_TAC list_ss [STRONGEST_REDUNDANT_ROWS_INFO_AUX_def] 1000)) 1001 1002val FST_STRONGEST_REDUNDANT_ROWS_INFO_AUX = store_thm ( 1003 "FST_STRONGEST_REDUNDANT_ROWS_INFO_AUX", 1004 ``!v rows p infos. 1005 FST (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos) = 1006 (p /\ EVERY (\r. r v = NONE) rows)``, 1007 1008Induct_on `rows` THEN ( 1009 ASM_SIMP_TAC (list_ss++boolSimps.EQUIV_EXTRACT_ss) [STRONGEST_REDUNDANT_ROWS_INFO_AUX_def] 1010)) 1011 1012 1013 1014val EL1_STRONGEST_REDUNDANT_ROWS_INFO_AUX = store_thm ( 1015 "EL1_STRONGEST_REDUNDANT_ROWS_INFO_AUX", 1016 ``!v rows p infos i. 1017 (i < LENGTH infos) ==> 1018 (EL i (SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos)) = 1019 EL i infos)``, 1020 1021Induct_on `rows` THEN ( 1022 ASM_SIMP_TAC (list_ss++boolSimps.EQUIV_EXTRACT_ss) [STRONGEST_REDUNDANT_ROWS_INFO_AUX_def, SNOC_APPEND, rich_listTheory.EL_APPEND1] 1023)) 1024 1025 1026val EL2_STRONGEST_REDUNDANT_ROWS_INFO_AUX = store_thm ( 1027 "EL2_STRONGEST_REDUNDANT_ROWS_INFO_AUX", 1028 ``!v rows p infos i. 1029 (i >= LENGTH infos /\ i < LENGTH rows + LENGTH infos) ==> 1030 (EL i (SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos)) = 1031 ((p /\ EVERY (\r. r v = NONE) (TAKE (i - LENGTH infos) rows)) ==> ((EL (i - LENGTH infos) rows) v = NONE)))``, 1032 1033GEN_TAC THEN 1034Induct_on `rows` THEN1 ( 1035 SIMP_TAC list_ss [] 1036) THEN 1037SIMP_TAC list_ss [STRONGEST_REDUNDANT_ROWS_INFO_AUX_def] THEN 1038REPEAT STRIP_TAC THEN 1039Cases_on `i = LENGTH infos` THEN1 ( 1040 ASM_SIMP_TAC list_ss [SNOC_APPEND, EL1_STRONGEST_REDUNDANT_ROWS_INFO_AUX, rich_listTheory.EL_APPEND2] 1041) THEN 1042Q.PAT_X_ASSUM `!p infos. _` (MP_TAC o Q.SPECL [ 1043 `p /\ (h (v:'a) = NONE)`, `SNOC (p ==> (h (v:'a) = NONE)) infos`, `i`]) THEN 1044ASM_SIMP_TAC list_ss [SNOC_APPEND, GSYM arithmeticTheory.ADD1] THEN 1045REPEAT STRIP_TAC THEN 1046ASM_SIMP_TAC (std_ss++boolSimps.EQUIV_EXTRACT_ss) [] THEN 1047REPEAT STRIP_TAC THEN 1048`(i - LENGTH infos) = SUC (i - SUC (LENGTH infos))` by DECIDE_TAC THEN 1049ASM_SIMP_TAC list_ss []) 1050 1051 1052val LENGTH_STRONGEST_REDUNDANT_ROWS_INFO = store_thm ( 1053 "LENGTH_STRONGEST_REDUNDANT_ROWS_INFO", 1054 ``LENGTH (STRONGEST_REDUNDANT_ROWS_INFO v rows) = LENGTH rows``, 1055 1056SIMP_TAC list_ss [STRONGEST_REDUNDANT_ROWS_INFO_def, 1057 LENGTH_STRONGEST_REDUNDANT_ROWS_INFO_AUX]) 1058 1059val FST_STRONGEST_REDUNDANT_ROWS_INFO_AUX = store_thm ( 1060 "FST_STRONGEST_REDUNDANT_ROWS_INFO_AUX", 1061 ``!v rows p infos. 1062 FST (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos) = 1063 (p /\ EVERY (\r. r v = NONE) rows)``, 1064 1065Induct_on `rows` THEN ( 1066 ASM_SIMP_TAC (list_ss++boolSimps.EQUIV_EXTRACT_ss) [STRONGEST_REDUNDANT_ROWS_INFO_AUX_def] 1067)) 1068 1069val EL_STRONGEST_REDUNDANT_ROWS_INFO = store_thm ( 1070 "EL_STRONGEST_REDUNDANT_ROWS_INFO", 1071 ``!v rows i. 1072 (i < LENGTH rows) ==> 1073 (EL i (STRONGEST_REDUNDANT_ROWS_INFO v rows) = 1074 ((EVERY (\r. r v = NONE) (TAKE i rows)) ==> 1075 ((EL i rows) v = NONE)))``, 1076 1077SIMP_TAC list_ss [STRONGEST_REDUNDANT_ROWS_INFO_def, 1078 EL2_STRONGEST_REDUNDANT_ROWS_INFO_AUX]) 1079 1080 1081val STRONGEST_REDUNDANT_ROWS_INFO_OK = store_thm ("STRONGEST_REDUNDANT_ROWS_INFO_OK", 1082 1083 ``IS_REDUNDANT_ROWS_INFO v rows (EVERY (\r. r v = NONE) rows) 1084 (STRONGEST_REDUNDANT_ROWS_INFO v rows)``, 1085 1086SIMP_TAC std_ss [IS_REDUNDANT_ROWS_INFO_def, 1087 EL_STRONGEST_REDUNDANT_ROWS_INFO, 1088 LENGTH_STRONGEST_REDUNDANT_ROWS_INFO, 1089 PMATCH_ROW_REDUNDANT_def] THEN 1090REPEAT STRIP_TAC THEN 1091Cases_on `EL i rows v` THEN1 ( 1092 FULL_SIMP_TAC list_ss [] 1093) THEN 1094FULL_SIMP_TAC list_ss [EXISTS_MEM] THEN 1095`?j. j < i /\ (EL j rows = e)` suffices_by ( 1096 STRIP_TAC THEN Q.EXISTS_TAC `j` THEN 1097 ASM_SIMP_TAC std_ss [] THEN 1098 Cases_on `e v` THEN FULL_SIMP_TAC std_ss [] 1099) THEN 1100Q.PAT_X_ASSUM `MEM e _` MP_TAC THEN 1101ASM_SIMP_TAC (list_ss++boolSimps.CONJ_ss) [MEM_EL,rich_listTheory.EL_TAKE] THEN 1102PROVE_TAC[]) 1103 1104 1105(* IN order to automate this procedure, we need a few 1106 simple, additional lemmata *) 1107 1108val PMATCH_ROW_COND_EX_FULL_DEF = store_thm ("PMATCH_ROW_COND_EX_FULL_DEF", 1109 ``PMATCH_ROW_COND_EX i p g = 1110 ?x. (i = p x) /\ g x``, 1111SIMP_TAC std_ss [PMATCH_ROW_COND_EX_def, PMATCH_ROW_COND_def] THEN 1112METIS_TAC[]) 1113 1114val PMATCH_ROW_COND_EX_WEAKEN = store_thm ("PMATCH_ROW_COND_EX_WEAKEN", 1115``!f v p g p' g'. 1116 1117 ~(PMATCH_ROW_COND_EX v p g) ==> 1118 (!x. p' x = p (f x)) ==> 1119 (PMATCH_ROW_COND_EX v p' g' = 1120 PMATCH_ROW_COND_EX v p' (\x. g' x /\ ~(g (f x))))``, 1121 1122SIMP_TAC std_ss [PMATCH_ROW_COND_EX_def, PMATCH_ROW_COND_def] THEN 1123REPEAT STRIP_TAC THEN 1124CONSEQ_CONV_TAC (K EXISTS_EQ___CONSEQ_CONV) THEN 1125SIMP_TAC (std_ss++boolSimps.EQUIV_EXTRACT_ss) [] THEN 1126METIS_TAC[]); 1127 1128val PMATCH_ROW_COND_EX_FALSE = store_thm ("PMATCH_ROW_COND_EX_FALSE", 1129``!v p g. 1130 (!x. ~(g x)) ==> 1131 (PMATCH_ROW_COND_EX v p g = F)``, 1132 1133SIMP_TAC std_ss [PMATCH_ROW_COND_EX_def, PMATCH_ROW_COND_def]) 1134 1135val PMATCH_ROW_COND_EX_IMP_REWRITE = store_thm ("PMATCH_ROW_COND_EX_IMP_REWRITE", 1136``!v p g p' g' RES. 1137 PMATCH_ROW_COND_EX v p g ==> 1138 (!x. g x ==> ((?x'. (p' x' = p x) /\ g' x') = RES)) ==> 1139 (PMATCH_ROW_COND_EX v p' g' = RES)``, 1140 1141SIMP_TAC std_ss [PMATCH_ROW_COND_EX_def, PMATCH_ROW_COND_def, 1142 GSYM LEFT_FORALL_IMP_THM]); 1143 1144(* Use this simple contradiction to bring 1145 PMATCH_IS_EXHAUSTIVE in the form we need for 1146 automation *) 1147val PMATCH_IS_EXHAUSTIVE_CONTRADICT = store_thm ( 1148 "PMATCH_IS_EXHAUSTIVE_CONTRADICT", 1149``!v rs. 1150 (EVERY (\r. r v = NONE) rs ==> F) ==> 1151 (PMATCH_IS_EXHAUSTIVE v rs)``, 1152 1153REPEAT STRIP_TAC THEN 1154FULL_SIMP_TAC list_ss [PMATCH_IS_EXHAUSTIVE_def, 1155 combinTheory.o_DEF, quantHeuristicsTheory.IS_SOME_EQ_NOT_NONE]) 1156 1157 1158val PMATCH_ROW_EVAL_COND_EX = store_thm ("PMATCH_ROW_EVAL_COND_EX", 1159 ``PMATCH_ROW_COND_EX i p g ==> 1160 ((PMATCH_ROW p g r i) = SOME (r (@x. PMATCH_ROW_COND p g i x)))``, 1161 1162SIMP_TAC std_ss [PMATCH_ROW_def, some_def, PMATCH_ROW_COND_EX_def]) 1163 1164val PMATCH_ROW_NEQ_NONE = store_thm ("PMATCH_ROW_NEQ_NONE", 1165 ``(PMATCH_ROW p g r i <> NONE) <=> 1166 (PMATCH_ROW_COND_EX i p g)``, 1167 1168SIMP_TAC std_ss [PMATCH_ROW_def, some_eq_NONE, 1169 PMATCH_ROW_COND_EX_def]); 1170 1171 1172(***************************************************) 1173(* ELIMINATE DOUBLE VAR-BINDS *) 1174(***************************************************) 1175 1176(* If a variable is used multiple times in a pattern, 1177 we can via the following theorem introduce a fresh variable 1178 and add the connection between the old and the newly created 1179 var to the guard. *) 1180val PMATCH_ROW_REMOVE_DOUBLE_BINDS_THM = 1181 store_thm ("PMATCH_ROW_REMOVE_DOUBLE_BINDS_THM", 1182``!g p1 g1 r1 p2 g2 r2. 1183 ((!x y. (p1 x = p1 y) ==> (x = y)) /\ 1184 (!x. (p2 (g x) = p1 x)) /\ 1185 (!x'. g2 x' = (?x. (x' = g x) /\ g1 x)) /\ 1186 (!x. r2 (g x) = r1 x)) ==> 1187 1188 (PMATCH_ROW p1 g1 r1 = PMATCH_ROW p2 g2 r2)``, 1189 1190SIMP_TAC (std_ss++boolSimps.CONJ_ss) [PMATCH_ROW_def, FUN_EQ_THM, 1191 optionTheory.some_def, PMATCH_ROW_COND_def, 1192 GSYM RIGHT_EXISTS_AND_THM] THEN 1193REPEAT STRIP_TAC THEN 1194Cases_on `?x'. (p1 x' = x) /\ g1 x'` THEN ( 1195 ASM_REWRITE_TAC[optionTheory.OPTION_MAP_DEF] 1196) THEN 1197SELECT_ELIM_TAC THEN ASM_REWRITE_TAC[] THEN 1198SELECT_ELIM_TAC THEN 1199REPEAT STRIP_TAC THEN ( 1200 METIS_TAC[] 1201)) 1202 1203 1204 1205(***************************************************) 1206(* ELIMINATE GUARDS *) 1207(***************************************************) 1208 1209(* We can eliminate guards by replacing them with true 1210 and add the guard in form of a conditional. 1211 Notice that all the rows after the guard are 1212 duplicated. We heavily rely on simplification 1213 of PMATCH to avoid a huge blowup of term-size, 1214 when applying the following rule. *) 1215val GUARDS_ELIM_THM = store_thm ("GUARDS_ELIM_THM", 1216``!v rs1 rs2 p g r. 1217 (!x1 x2. (p x1 = p x2) ==> (x1 = x2)) ==> ( 1218 PMATCH v (rs1++(PMATCH_ROW p g r)::rs2) = 1219 PMATCH v (rs1++(PMATCH_ROW p (\x. T) (\x. 1220 if g x then r x else 1221 PMATCH (p x) rs2))::rs2))``, 1222 1223REPEAT STRIP_TAC THEN 1224SIMP_TAC std_ss [PMATCH_APPEND_SEM] THEN 1225Cases_on `?r. MEM r rs1 /\ IS_SOME (r v)` THEN ( 1226 ASM_REWRITE_TAC[] 1227) THEN 1228SIMP_TAC std_ss [PMATCH_EVAL, PMATCH_ROW_COND_def] THEN 1229Tactical.REVERSE (Cases_on `?x. p x = v`) THEN ( 1230 FULL_SIMP_TAC std_ss [] 1231) THEN 1232`!x'. (p x' = v) <=> (x' = x)` by METIS_TAC[] THEN 1233ASM_SIMP_TAC (std_ss++boolSimps.CONJ_ss) []); 1234 1235 1236 1237(***************************************************) 1238(* THEOREMS ABOUT FLATTENING *) 1239(***************************************************) 1240 1241(* The content of this section is still experimental. 1242 It is likely to chnage quite a bit still. *) 1243val PMATCH_FLATTEN_FUN_def = Define ` 1244 PMATCH_FLATTEN_FUN p g row v = ( 1245 option_CASE (some x. PMATCH_ROW_COND p g v x) 1246 NONE (\x. row x x))`; 1247 1248 1249val PMATCH_FLATTEN_THM_AUX = prove ( 1250 ``(PMATCH v [PMATCH_ROW p g (\x. (PMATCH x (MAP (\r. r x) rows')))]) = 1251 (PMATCH v (MAP (\r. (PMATCH_FLATTEN_FUN p g r)) rows'))``, 1252 1253REPEAT GEN_TAC THEN 1254Induct_on `rows'` THEN1 ( 1255 Cases_on `some x. PMATCH_ROW_COND p g v x` THEN 1256 ASM_SIMP_TAC list_ss [PMATCH_def, PMATCH_ROW_def] 1257) THEN 1258 1259Q.PAT_X_ASSUM `_ = _` (ASSUME_TAC o GSYM) THEN 1260FULL_SIMP_TAC list_ss [PMATCH_def, PMATCH_ROW_def] THEN 1261Q.PAT_X_ASSUM `_ = _` (K ALL_TAC) THEN 1262 1263Cases_on `some x. PMATCH_ROW_COND p g v x` THEN ( 1264 ASM_SIMP_TAC std_ss [PMATCH_FLATTEN_FUN_def] 1265)); 1266 1267 1268val PMATCH_FLATTEN_THM_SINGLE = store_thm ("PMATCH_FLATTEN_THM_SINGLE", 1269 ``!v p g rows. 1270 (!x. PMATCH_IS_EXHAUSTIVE x (MAP (\r. r x) rows)) ==> 1271PMATCH_EQUIV_ROWS v [PMATCH_ROW p g (\x. (PMATCH x (MAP (\r. r x) rows)))] (MAP (\r. (PMATCH_FLATTEN_FUN p g r)) rows)``, 1272 1273REPEAT STRIP_TAC THEN 1274SIMP_TAC list_ss [PMATCH_EQUIV_ROWS_def, PMATCH_FLATTEN_THM_AUX] THEN 1275SIMP_TAC list_ss [PMATCH_ROW_def, IS_SOME_OPTION_MAP, some_IS_SOME, 1276 listTheory.MEM_MAP, GSYM LEFT_EXISTS_AND_THM] THEN 1277 1278SIMP_TAC std_ss [PMATCH_FLATTEN_FUN_def, some_def] THEN 1279Cases_on `?x. PMATCH_ROW_COND p g v x` THEN ( 1280 ASM_SIMP_TAC std_ss [PMATCH_ROW_COND_def] 1281) THEN 1282FULL_SIMP_TAC std_ss [PMATCH_IS_EXHAUSTIVE_def, 1283 listTheory.EXISTS_MEM, listTheory.MEM_MAP, 1284 GSYM LEFT_EXISTS_AND_THM]) 1285 1286 1287val PMATCH_FLATTEN_THM = store_thm ("PMATCH_FLATTEN_THM", 1288 ``!v p g rows1 rows2 rows. 1289 (!x. PMATCH_IS_EXHAUSTIVE x (MAP (\r. r x) rows)) ==> 1290(PMATCH v (rows1 ++ (PMATCH_ROW p g (\x. (PMATCH x (MAP (\r. r x) rows))))::rows2) = 1291 PMATCH v (rows1 ++ (MAP (\r. (PMATCH_FLATTEN_FUN p g r)) rows) ++ rows2))``, 1292 1293REPEAT STRIP_TAC THEN 1294MATCH_MP_TAC PMATCH_EQUIV_ROWS_MATCH THEN 1295REWRITE_TAC[GSYM APPEND_ASSOC] THEN 1296MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] PMATCH_EQUIV_APPEND) THEN 1297REWRITE_TAC[PMATCH_EQUIV_ROWS_is_equiv_1] THEN 1298ONCE_REWRITE_TAC [prove (``x::xs = [x] ++ xs``, SIMP_TAC list_ss [])] THEN 1299MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] PMATCH_EQUIV_APPEND) THEN 1300REWRITE_TAC[PMATCH_EQUIV_ROWS_is_equiv_1] THEN 1301MATCH_MP_TAC PMATCH_FLATTEN_THM_SINGLE THEN 1302ASM_REWRITE_TAC[]); 1303 1304 1305val PMATCH_FLATTEN_FUN_PMATCH_ROW = store_thm ("PMATCH_FLATTEN_FUN_PMATCH_ROW", 1306``!p. 1307 (!x1 x2. (p x1 = p x2) ==> (x1 = x2)) ==> ( 1308 1309 !g p' g' r'. 1310 PMATCH_FLATTEN_FUN p g (\x. PMATCH_ROW p' (g' x) (r' x)) = 1311 PMATCH_ROW (\x. (p (p' x))) (\x. (g (p' x)) /\ (g' (p' x) x)) (\x. r' (p' x) x))``, 1312 1313REPEAT STRIP_TAC THEN 1314SIMP_TAC std_ss [PMATCH_FLATTEN_FUN_def, FUN_EQ_THM, PMATCH_ROW_def] THEN 1315CONV_TAC (RENAME_VARS_CONV ["v"]) THEN GEN_TAC THEN 1316Cases_on ` some x. PMATCH_ROW_COND p g v x` THEN1 ( 1317 FULL_SIMP_TAC list_ss [some_eq_NONE, PMATCH_ROW_COND_def] THEN 1318 PROVE_TAC[] 1319) THEN 1320 1321ASM_SIMP_TAC std_ss [] THEN 1322FULL_SIMP_TAC std_ss [PMATCH_ROW_COND_def] THEN 1323Q.PAT_X_ASSUM `_ = SOME x` (fn thm => 1324 ASSUME_TAC (HO_MATCH_MP some_eq_SOME thm)) THEN 1325`!x'. (p x' = v) = (x' = x)` by PROVE_TAC[] THEN 1326ASM_SIMP_TAC (std_ss++boolSimps.CONJ_ss) [] THEN 1327Cases_on `(some x'. (p' x' = x) /\ g' x x')` THEN ( 1328 ASM_SIMP_TAC std_ss [] 1329) THEN 1330Q.PAT_X_ASSUM `_ = SOME x'` (fn thm => 1331 ASSUME_TAC (HO_MATCH_MP some_eq_SOME thm)) THEN 1332ASM_SIMP_TAC std_ss []) 1333 1334 1335 1336 1337 1338(***************************************************) 1339(* UNROLLING PREDICATES *) 1340(***************************************************) 1341 1342val PMATCH_ROW_COND_NOT_EX_OR_EQ_def = Define `PMATCH_ROW_COND_NOT_EX_OR_EQ (i:'a) (r : 'a -> 'b option) rows = 1343(~(r i <> NONE) \/ ((EXISTS (\row. row i <> NONE) rows) /\ 1344 (THE (r i) = PMATCH i rows)))` 1345 1346val PMATCH_ROW_COND_NOT_EX_OR_EQ_FIRST_ROW = store_thm ("PMATCH_ROW_COND_NOT_EX_OR_EQ_FIRST_ROW", 1347 ``!i r r' rows. 1348 1349 (r' i <> NONE) ==> 1350 ((PMATCH_ROW_COND_NOT_EX_OR_EQ i r (r'::rows)) = 1351 ((r i <> NONE) ==> 1352 (r i = r' i)))``, 1353 1354SIMP_TAC list_ss [PMATCH_ROW_COND_NOT_EX_OR_EQ_def, PMATCH_def] THEN 1355REPEAT GEN_TAC THEN 1356Cases_on `r' i` THEN Cases_on `r i` THEN ( 1357 SIMP_TAC std_ss [] 1358)) 1359 1360 1361val PMATCH_ROW_COND_NOT_EX_OR_EQ_NIL = store_thm ("PMATCH_ROW_COND_NOT_EX_OR_EQ_NIL", 1362 ``PMATCH_ROW_COND_NOT_EX_OR_EQ i r [] = 1363 ((r i <> NONE) ==> F)``, 1364 1365SIMP_TAC list_ss [PMATCH_ROW_COND_NOT_EX_OR_EQ_def]); 1366 1367 1368val PMATCH_ROW_COND_NOT_EX_OR_EQ_NOT_FIRST_ROW = store_thm ("PMATCH_ROW_COND_NOT_EX_OR_EQ_NOT_FIRST_ROW", 1369 ``PMATCH_ROW_COND_NOT_EX_OR_EQ i r' rows ==> 1370 (PMATCH_ROW_COND_NOT_EX_OR_EQ i r (r'::rows) = 1371 (PMATCH_ROW_COND_NOT_EX_OR_EQ i r rows))``, 1372 1373SIMP_TAC list_ss [PMATCH_ROW_COND_NOT_EX_OR_EQ_def, PMATCH_def] THEN 1374Cases_on `r i` THEN ASM_SIMP_TAC std_ss [] THEN 1375Cases_on `r' i` THEN ASM_SIMP_TAC std_ss [] 1376); 1377 1378val PMATCH_PRED_UNROLL_NIL = store_thm ("PMATCH_PRED_UNROLL_NIL", 1379 ``!P v. P (PMATCH v []) = P ARB``, 1380 SIMP_TAC std_ss [PMATCH_def, PMATCH_INCOMPLETE_def]); 1381 1382 1383val PMATCH_PRED_UNROLL_CONS = store_thm ("PMATCH_PRED_UNROLL_CONS", 1384``!P v r rows. 1385 P (PMATCH v (r::rows)) <=> ( 1386 ((r v <> NONE) ==> P (THE (r v))) /\ 1387 ((PMATCH_ROW_COND_NOT_EX_OR_EQ v r rows) ==> 1388 P (PMATCH v rows)))``, 1389 1390REPEAT STRIP_TAC THEN 1391SIMP_TAC std_ss [PMATCH_def, PMATCH_ROW_def, some_def, 1392 PMATCH_ROW_COND_NOT_EX_OR_EQ_def, 1393 PMATCH_ROW_COND_EX_def] THEN 1394Cases_on `r v` THEN ASM_SIMP_TAC std_ss [] THEN 1395METIS_TAC[]); 1396 1397 1398val PMATCH_EXPAND_PRED_def = Define `(PMATCH_EXPAND_PRED P v rows_before [] = (~(PMATCH_IS_EXHAUSTIVE v (REVERSE rows_before)) ==> P ARB)) /\ 1399 1400 (PMATCH_EXPAND_PRED P v rows_before (r::rows_after) = ( 1401 ((r v <> NONE) ==> (EVERY (\r'. (r' v <> NONE) ==> (r' v = r v)) rows_before) 1402 ==> P (THE (r v))) /\ PMATCH_EXPAND_PRED P v (r::rows_before) rows_after))`; 1403 1404 1405val PMATCH_EXPAND_PRED_THM_GEN = store_thm ("PMATCH_EXPAND_PRED_THM_GEN", 1406``!P v rows_before rows_after. 1407 PMATCH_EXPAND_PRED P v rows_before rows_after <=> ( 1408 EVERY (\r. PMATCH_ROW_COND_NOT_EX_OR_EQ v r rows_after ) rows_before ==> 1409 P (PMATCH v rows_after))``, 1410 1411Induct_on `rows_after` THEN1 ( 1412 SIMP_TAC list_ss [PMATCH_EXPAND_PRED_def, PMATCH_IS_EXHAUSTIVE_def, PMATCH_def, PMATCH_INCOMPLETE_def, PMATCH_ROW_COND_NOT_EX_OR_EQ_NIL, combinTheory.o_DEF, rich_listTheory.EVERY_REVERSE] 1413) THEN 1414 1415ASM_SIMP_TAC list_ss [PMATCH_EXPAND_PRED_def, PMATCH_IS_EXHAUSTIVE_def, PMATCH_PRED_UNROLL_CONS] THEN 1416POP_ASSUM (K ALL_TAC) THEN 1417REPEAT GEN_TAC THEN 1418Q.RENAME1_TAC `P (THE (r v))` THEN 1419Cases_on `r v` THENL [ 1420 ASM_SIMP_TAC (std_ss++boolSimps.EQUIV_EXTRACT_ss) [EVERY_MEM] THEN 1421 REPEAT STRIP_TAC THEN 1422 METIS_TAC[PMATCH_ROW_COND_NOT_EX_OR_EQ_NOT_FIRST_ROW], 1423 1424 1425 Q.RENAME1_TAC `r v = SOME x` THEN 1426 ASM_SIMP_TAC std_ss [PMATCH_ROW_COND_NOT_EX_OR_EQ_FIRST_ROW] THEN 1427 1428 Cases_on `PMATCH_ROW_COND_NOT_EX_OR_EQ v r rows_after` THEN ( 1429 ASM_SIMP_TAC std_ss [] 1430 ) THEN 1431 Cases_on `EVERY (\r'. r' v <> NONE ==> (r' v = SOME x)) rows_before` THENL [ 1432 FULL_SIMP_TAC (std_ss++boolSimps.EQUIV_EXTRACT_ss) [EVERY_MEM, PMATCH_ROW_COND_NOT_EX_OR_EQ_def] THEN 1433 METIS_TAC[], 1434 1435 1436 ASM_SIMP_TAC std_ss [] THEN 1437 FULL_SIMP_TAC std_ss [EVERY_MEM, PMATCH_ROW_COND_NOT_EX_OR_EQ_def] THEN1 (FULL_SIMP_TAC std_ss []) THEN 1438 1439 STRIP_TAC THEN 1440 POP_ASSUM (MP_TAC o Q.SPEC `r'`) THEN 1441 Q.PAT_X_ASSUM `THE (r v) = _` (ASSUME_TAC o GSYM) THEN 1442 ASM_SIMP_TAC std_ss [] THEN 1443 Cases_on `r' v` THEN FULL_SIMP_TAC std_ss [] 1444 ] 1445]); 1446 1447 1448val PMATCH_EXPAND_PRED_THM = store_thm ("PMATCH_EXPAND_PRED_THM", 1449``!P v rows. 1450 P (PMATCH v rows) <=> 1451 PMATCH_EXPAND_PRED P v [] rows``, 1452 1453SIMP_TAC list_ss [PMATCH_EXPAND_PRED_THM_GEN]); 1454 1455 1456val PMATCH_ROW_LIFT_def = Define `PMATCH_ROW_LIFT f r = \x. OPTION_MAP f (r x)` 1457 1458val PMATCH_LIFT_THM = store_thm ("PMATCH_LIFT_THM", 1459``!f v rows. 1460 PMATCH_IS_EXHAUSTIVE v rows ==> 1461 (f (PMATCH v rows) = 1462 PMATCH v (MAP (PMATCH_ROW_LIFT f) rows))``, 1463 1464GEN_TAC THEN GEN_TAC THEN 1465Induct_on `rows` THEN ( 1466 FULL_SIMP_TAC list_ss [PMATCH_def, PMATCH_IS_EXHAUSTIVE_def] 1467) THEN 1468CONV_TAC (RENAME_VARS_CONV ["r"]) THEN 1469GEN_TAC THEN 1470Cases_on `r v` THEN ( 1471 ASM_SIMP_TAC std_ss [PMATCH_ROW_LIFT_def] 1472)); 1473 1474 1475val PMATCH_ROW_LIFT_THM = store_thm ("PMATCH_ROW_LIFT_THM", 1476 ``!f p g r. 1477 PMATCH_ROW_LIFT f (PMATCH_ROW p g r) = 1478 PMATCH_ROW p g (\x. f (r x))``, 1479 1480REPEAT STRIP_TAC THEN 1481SIMP_TAC std_ss [PMATCH_ROW_LIFT_def, PMATCH_ROW_def, FUN_EQ_THM] THEN 1482Cases_on `some v. PMATCH_ROW_COND p g x v` THEN ( 1483 ASM_SIMP_TAC std_ss [] 1484)); 1485 1486 1487val PMATCH_IS_EXHAUSTIVE_LIFT = store_thm ("PMATCH_IS_EXHAUSTIVE_LIFT", 1488 ``!f v rows. 1489 PMATCH_IS_EXHAUSTIVE v rows ==> 1490 PMATCH_IS_EXHAUSTIVE v (MAP (PMATCH_ROW_LIFT f) rows)``, 1491 1492SIMP_TAC list_ss [PMATCH_IS_EXHAUSTIVE_def, EXISTS_MAP, PMATCH_ROW_LIFT_def, 1493 IS_SOME_MAP]); 1494 1495 1496val _ = export_theory(); 1497