1(*---------------------------------------------------------------------------*) 2(* Regular expressions and a regexp matcher. *) 3(* Originated from Konrad Slind, tweaked by MJCG for Accellera PSL SEREs *) 4(* An automata-based matcher added by Joe Hurd *) 5(*---------------------------------------------------------------------------*) 6 7(* 8app load ["bossLib", "rich_listTheory", "metisLib"]; 9*) 10 11open HolKernel Parse boolLib; 12open bossLib metisLib pairTheory combinTheory listTheory rich_listTheory 13 arithmeticTheory; 14 15val () = new_theory "regexp"; 16 17(*---------------------------------------------------------------------------*) 18(* Symbolic tacticals. *) 19(*---------------------------------------------------------------------------*) 20 21infixr 0 || THENC ORELSEC ORELSER; 22 23val op || = op ORELSE; 24val Know = Q_TAC KNOW_TAC; 25val Suff = Q_TAC SUFF_TAC; 26val REVERSE = Tactical.REVERSE; 27 28(*---------------------------------------------------------------------------*) 29(* Make list append into an infix recognized by the parser *) 30(*---------------------------------------------------------------------------*) 31 32val _ = set_fixity "<>" (Infixl 500); 33val _ = overload_on ("<>", Term`APPEND`); 34 35(*---------------------------------------------------------------------------*) 36(* Misc. theorems *) 37(*---------------------------------------------------------------------------*) 38 39val IN_THM = prove 40 (``!x. P x = x IN P``, 41 RW_TAC bool_ss [boolTheory.IN_DEF]); 42 43val APPEND_ID_THM = prove 44 (``!l1 l2. ((l1<>l2 = l1) = (l2=[])) /\ 45 ((l1<>l2 = l2) = (l1=[]))``, 46 Induct THEN EVAL_TAC THEN ASM_REWRITE_TAC [] 47 THEN GEN_TAC THEN Cases THEN RW_TAC list_ss [] THEN DISJ2_TAC 48 THEN SPOSE_NOT_THEN (MP_TAC o Q.AP_TERM `LENGTH`) 49 THEN RW_TAC list_ss []); 50 51val APPEND_CONS = prove 52 (``!h t. [h]<>t = h::t``, 53 RW_TAC list_ss []); 54 55val NULL_EQ_NIL = prove 56 (``!l. NULL l = (l = [])``, 57 Cases THEN RW_TAC list_ss []); 58 59val LENGTH_EQ_ONE = store_thm 60 ("LENGTH_EQ_ONE", 61 ``!l. (LENGTH l = 1) = ?x. l = [x]``, 62 Cases THEN RW_TAC list_ss [] THEN 63 Cases_on `t` THEN RW_TAC list_ss []); 64 65val MEM_TL = prove 66 (``!x l. ~NULL l ==> MEM x (TL l) ==> MEM x l``, 67 Induct_on `l` THEN RW_TAC list_ss []); 68 69val FIRST_EXISTS_THM = prove 70 (``!P L. EXISTS P L ==> 71 ?prefix w suffix. 72 (L = prefix <> [w] <> suffix) /\ EVERY ($~ o P) prefix /\ P w``, 73 GEN_TAC THEN Induct THEN RW_TAC list_ss [] 74 THEN FULL_SIMP_TAC list_ss [EXISTS_DEF] THEN RW_TAC list_ss [] 75 THENL [MAP_EVERY Q.EXISTS_TAC [`[]`, `h`, `L`] THEN RW_TAC list_ss [], 76 RES_TAC THEN Cases_on `P h` THENL 77 [MAP_EVERY Q.EXISTS_TAC [`[]`, `h`, `prefix <> [w] <> suffix`] 78 THEN RW_TAC list_ss [], 79 MAP_EVERY Q.EXISTS_TAC [`h::prefix`, `w`, `suffix`] THEN 80 RW_TAC list_ss [combinTheory.o_DEF]]]); 81 82val EXISTS_ELIM_THM = prove 83 (``!P l. EXISTS P l = ?x. MEM x l /\ x IN P``, 84 GEN_TAC THEN Induct 85 THEN RW_TAC list_ss [EXISTS_DEF] 86 THEN PROVE_TAC [IN_THM]); 87 88val EVERY_ELIM_THM = prove 89 (``!P l. EVERY P l = !x. MEM x l ==> x IN P``, 90 GEN_TAC THEN Induct 91 THEN RW_TAC list_ss [EVERY_DEF] 92 THEN PROVE_TAC [IN_THM]); 93 94(*---------------------------------------------------------------------------*) 95(* Concatenate a list of lists *) 96(*---------------------------------------------------------------------------*) 97 98val CONCAT_def = Define 99 `(CONCAT [] = []) /\ 100 (CONCAT(l::ll) = l <> CONCAT ll)`; 101 102val CONCAT_EQ_NIL = prove 103 (``!wlist. (CONCAT wlist = []) = EVERY NULL wlist``, 104 Induct THEN RW_TAC list_ss [CONCAT_def,NULL_EQ_NIL]); 105 106val NULL_CONCAT_THM = prove 107 (``!L. NULL (CONCAT L) = EVERY NULL L``, 108 PROVE_TAC [CONCAT_EQ_NIL, NULL_EQ_NIL]); 109 110val CONCAT_APPEND_DISTRIB = prove 111 (``!l1 l2. CONCAT (l1 <> l2) = CONCAT l1 <> CONCAT l2``, 112 Induct THEN RW_TAC list_ss [CONCAT_def]); 113 114(*---------------------------------------------------------------------------*) 115(* All ways to split a list in 2 pieces *) 116(*---------------------------------------------------------------------------*) 117 118val ALL_SPLITS_def = Define 119 `(ALL_SPLITS (l,[]) = [(l,[])]) /\ 120 (ALL_SPLITS (l,h::t) = (l,h::t)::ALL_SPLITS(l<>[h],t))`; 121 122val SPLITS_def = Define `SPLITS l = ALL_SPLITS ([],l)`; 123 124(*---------------------------------------------------------------------------*) 125(* Testing 126 127 EVAL (Term`SPLITS [1;2;3;4]`); 128 EVAL (Term`SPLITS [1;2;3;4;5;6;7;8;9]`); 129 EVAL (Term`LENGTH (SPLITS [1;2;3;4;5;6;7;8;9; 130 1;2;3;4;5;6;7;8;9; 131 1;2;3;4;5;6;7;8;9])`); 132*) 133(*---------------------------------------------------------------------------*) 134 135val ALL_SPLITS_LEMMA = prove 136 (``!l1 l2 l3 l4. MEM (l3,l4) (ALL_SPLITS (l1,l2)) ==> (l1<>l2 = l3<>l4)``, 137 Induct_on `l2` THEN RW_TAC list_ss [ALL_SPLITS_def] THEN 138 METIS_TAC [APPEND,APPEND_ASSOC]); 139 140val SPLITS_APPEND = prove 141 (``!l l1 l2. MEM (l1,l2) (SPLITS l) ==> (l1<>l2 = l)``, 142 RW_TAC list_ss [SPLITS_def] THEN 143 METIS_TAC [ALL_SPLITS_LEMMA,APPEND]); 144 145val MEM_ALL_SPLITS_ID = prove 146 (``!x. MEM x (ALL_SPLITS x)``, 147 Cases THEN Cases_on `r` THEN RW_TAC list_ss [ALL_SPLITS_def]); 148 149val MEM_ALL_SPLITS_LEM = prove 150 (``!l1 l2 w1 w2. (l2 = w1<>w2) ==> MEM (l1<>w1,w2) (ALL_SPLITS (l1, l2))``, 151 recInduct (fetch "-" "ALL_SPLITS_ind") 152 THEN RW_TAC list_ss [ALL_SPLITS_def,APPEND_ID_THM] 153 THEN Cases_on `w1` THEN FULL_SIMP_TAC list_ss [] 154 THEN PROVE_TAC [APPEND_ASSOC,APPEND_CONS]); 155 156val MEM_ALL_SPLITS = prove 157 (``!w1 w2. MEM (w1,w2) (ALL_SPLITS ([],w1<>w2))``, 158 PROVE_TAC [MEM_ALL_SPLITS_LEM, CONJUNCT1 APPEND]); 159 160val MEM_SPLITS = prove 161 (``!w1 w2. MEM (w1,w2) (SPLITS (w1<>w2))``, 162 PROVE_TAC [MEM_ALL_SPLITS, SPLITS_def]); 163 164val MEM_TL_SPLITS = prove 165 (``!w1 w2. ~NULL w1 ==> MEM(w1,w2) (TL (SPLITS (w1<>w2)))``, 166 RW_TAC list_ss [SPLITS_def, ALL_SPLITS_def] 167 THEN Cases_on `w1` THEN FULL_SIMP_TAC list_ss [ALL_SPLITS_def] 168 THEN ONCE_REWRITE_TAC [GSYM APPEND_CONS] 169 THEN PURE_REWRITE_TAC [APPEND_NIL] 170 THEN RW_TAC list_ss [SIMP_RULE bool_ss [] MEM_ALL_SPLITS_LEM]); 171 172val SPLITS_LENGTH = prove 173 (``!l l1 l2. MEM (l1,l2) (SPLITS l) ==> (LENGTH l1 + LENGTH l2 = LENGTH l)``, 174 METIS_TAC [SPLITS_APPEND,LENGTH_APPEND]); 175 176val SPLITS_NON_EMPTY = prove 177 (``!l. ~NULL (SPLITS l)``, 178 RW_TAC list_ss [SPLITS_def] THEN 179 Induct_on `l` THEN RW_TAC list_ss [ALL_SPLITS_def]); 180 181val lem = prove 182 (``!l1 l2 l3 s1 s2. 183 MEM (s1,s2) (ALL_SPLITS (l1,l2)) 184 ==> 185 ?s3. MEM (s3,s2) (ALL_SPLITS (l3,l2))``, 186 Induct_on `l2` THEN RW_TAC list_ss [ALL_SPLITS_def] THEN PROVE_TAC []); 187 188val MEM_ALL_SPLITS_LENGTH = prove 189 (``!l s1 s2. 190 ~NULL l ==> MEM (s1,s2) (TL (SPLITS l)) ==> LENGTH s2 < LENGTH l``, 191 REWRITE_TAC [SPLITS_def] THEN 192 Induct THEN RW_TAC list_ss [ALL_SPLITS_def] 193 THEN Cases_on `l` 194 THEN FULL_SIMP_TAC list_ss [ALL_SPLITS_def] 195 THEN METIS_TAC [lem, DECIDE (Term `x < y ==> x < SUC y`)]); 196 197(*---------------------------------------------------------------------------*) 198(* Datatype of regular expressions *) 199(* Modified by MJCG from KXS version to match Accellera PSL *) 200(*---------------------------------------------------------------------------*) 201 202val () = Hol_datatype 203 `regexp = 204 Atom of ('s -> bool) (* Boolean expression *) 205 | Cat of regexp => regexp (* Concatenation *) 206 | Fuse of regexp => regexp (* Fusion *) 207 | Or of regexp => regexp (* Disjunction *) 208 | And of regexp => regexp (* Conjunction *) 209 | Repeat of regexp (* Iterated concat, >= 0 *) 210 | Prefix of regexp`; (* Prefix *) 211 212val Dot_def = Define `Dot = Atom (\x : 'a. T)`; 213val Zero_def = Define `Zero = Atom (\x : 'a. F)`; 214val One_def = Define `One = Repeat Zero`; 215 216(*---------------------------------------------------------------------------*) 217(* Following mysterious invocations remove old-style syntax for conditionals *) 218(* from the grammar and thus allow | to be used for "or" patterns. *) 219(*---------------------------------------------------------------------------*) 220 221(* "|" is conflicting with pred_setTheory and many other things, use "||". *) 222val _ = overload_on ("||", Term`$Or`); 223val _ = overload_on ("&", Term`$And`); 224val _ = overload_on ("#", Term`$Cat`); 225val _ = overload_on ("%", Term`$Fuse`); 226 227val _ = set_fixity "||" (Infixr 501); 228val _ = set_fixity "&" (Infixr 511); 229val _ = set_fixity "#" (Infixr 601); 230val _ = set_fixity "%" (Infixr 602); 231 232(*---------------------------------------------------------------------------*) 233(* PSL style semantics of regular expressions *) 234(* *) 235(* sem r w means regular expression r matches word w (represented as a list) *) 236(*---------------------------------------------------------------------------*) 237 238val sem_def = 239 Define 240 `(sem (Atom b) w = 241 (LENGTH w = 1) /\ b(HD w)) /\ 242 (sem (r1#r2) w = 243 ?w1 w2. (w = w1<>w2) /\ sem r1 w1 /\ sem r2 w2) /\ 244 (sem (r1%r2) w = 245 ?w1 w2 l. (w = w1<>[l]<>w2) /\ sem r1 (w1<>[l]) /\ sem r2 ([l]<>w2)) /\ 246 (sem (r1||r2) w = 247 sem r1 w \/ sem r2 w) /\ 248 (sem (r1&r2) w = 249 sem r1 w /\ sem r2 w) /\ 250 (sem (Repeat r) w = 251 ?wlist. (w = CONCAT wlist) /\ EVERY (sem r) wlist) /\ 252 (sem (Prefix r) w = 253 ?w'. sem r (w <> w'))`; 254 255val sem_Dot = store_thm 256 ("sem_Dot", 257 ``!l. sem Dot l = (LENGTH l = 1)``, 258 RW_TAC std_ss [sem_def, Dot_def]); 259 260val sem_Zero = store_thm 261 ("sem_Zero", 262 ``!l. ~(sem Zero l)``, 263 RW_TAC std_ss [sem_def, Zero_def]); 264 265val sem_One = store_thm 266 ("sem_One", 267 ``!l. sem One l = (l = [])``, 268 RW_TAC std_ss [sem_def, One_def] 269 >> REVERSE EQ_TAC 270 >- (RW_TAC std_ss [] 271 >> Q.EXISTS_TAC `[]` 272 >> RW_TAC std_ss [CONCAT_def, ALL_EL]) 273 >> RW_TAC std_ss [] 274 >> POP_ASSUM MP_TAC 275 >> Cases_on `wlist` 276 >> RW_TAC std_ss [CONCAT_def, ALL_EL, sem_Zero]); 277 278(*---------------------------------------------------------------------------*) 279(* Misc. semantics lemmas *) 280(*---------------------------------------------------------------------------*) 281 282val Concat_ID = prove 283(``!r w. (sem (r # One) w = sem r w) /\ (sem (One # r) w = sem r w)``, 284 RW_TAC std_ss [sem_def, sem_One, APPEND_NIL]); 285 286(* Should be true, but the proof is currently broken 287val Then_ASSOC = Count.apply Q.prove 288(`!r1 r2 r3 w. sem (r1 # (r2 # r3)) w = sem ((r1 # r2) # r3) w`, 289 Cases THENL 290 [EVAL_TAC THEN METIS_TAC [APPEND_ASSOC], 291 EVAL_TAC THEN REPEAT GEN_TAC THEN EQ_TAC 292 THEN RW_TAC list_ss [] THEN EVAL_TAC THENL 293 [Q.EXISTS_TAC `x::w1'` THEN Q.EXISTS_TAC `w2'` THEN RW_TAC list_ss [] THEN 294 Q.EXISTS_TAC `[x]` THEN Q.EXISTS_TAC `w1'` THEN RW_TAC list_ss [], 295 Q.EXISTS_TAC `[x]` THEN Q.EXISTS_TAC `w2'<>w2` 296 THEN RW_TAC list_ss [] THEN METIS_TAC []], 297 REPEAT GEN_TAC THEN EVAL_TAC THEN EQ_TAC THEN RW_TAC list_ss [], 298 REPEAT GEN_TAC THEN EVAL_TAC THEN EQ_TAC THEN RW_TAC list_ss [] THENL 299 [Q.EXISTS_TAC `c::w1` THEN Q.EXISTS_TAC `w2'` THEN RW_TAC list_ss [], 300 Q.EXISTS_TAC `w2'<>w2` THEN RW_TAC list_ss [] THEN METIS_TAC []], 301 REPEAT GEN_TAC THEN EVAL_TAC THEN EQ_TAC THEN RW_TAC list_ss [] THENL 302 [Q.EXISTS_TAC`w1<>w1'` THEN Q.EXISTS_TAC`w2'` THEN RW_TAC list_ss [] THEN 303 Q.EXISTS_TAC`w1` THEN Q.EXISTS_TAC`w1'` THEN RW_TAC list_ss [], 304 Q.EXISTS_TAC`w1<>w1'` THEN Q.EXISTS_TAC`w2'` THEN RW_TAC list_ss [] THEN 305 Q.EXISTS_TAC`w1` THEN Q.EXISTS_TAC `w1'` THEN RW_TAC list_ss [], 306 Q.EXISTS_TAC`w1'` THEN Q.EXISTS_TAC`w2'<>w2` THEN RW_TAC list_ss [] THEN 307 Q.EXISTS_TAC `w2'` THEN Q.EXISTS_TAC `w2` THEN RW_TAC list_ss [], 308 Q.EXISTS_TAC`w1'` THEN Q.EXISTS_TAC`w2'<>w2` THEN RW_TAC list_ss [] THEN 309 Q.EXISTS_TAC`w2'` THEN Q.EXISTS_TAC`w2` THEN RW_TAC list_ss []], 310 REPEAT GEN_TAC THEN EVAL_TAC THEN EQ_TAC THEN RW_TAC list_ss [] THENL 311 [Q.EXISTS_TAC `(w1'<>w2')<>w1''` THEN Q.EXISTS_TAC `w2''` 312 THEN RW_TAC list_ss [] 313 THEN Q.EXISTS_TAC `w1'<>w2'` THEN Q.EXISTS_TAC `w1''` 314 THEN RW_TAC list_ss [] THEN METIS_TAC[], 315 Q.EXISTS_TAC `(w1''<>w2'')` THEN Q.EXISTS_TAC `w2'<>w2` 316 THEN RW_TAC list_ss [] THEN METIS_TAC []], 317 REPEAT GEN_TAC THEN EVAL_TAC THEN EQ_TAC THEN RW_TAC list_ss [] THENL 318 [Q.EXISTS_TAC `(CONCAT wlist <> w1')` THEN Q.EXISTS_TAC `w2'` 319 THEN RW_TAC list_ss [] THEN 320 Q.EXISTS_TAC `CONCAT wlist` THEN Q.EXISTS_TAC `w1'` THEN METIS_TAC[], 321 Q.EXISTS_TAC `CONCAT wlist` THEN Q.EXISTS_TAC `w2'<>w2` 322 THEN RW_TAC list_ss [] THEN METIS_TAC[]]]); 323*) 324 325val Or_lemma = prove 326 (``!r1 r2 r3. sem ((r1 || r2) # r3) w = sem (r1 # r3) w \/ sem (r2 # r3) w``, 327 RW_TAC list_ss [sem_def] THEN PROVE_TAC []); 328 329(*---------------------------------------------------------------------------*) 330(* Checker - from a tech. report of Simon Thompson *) 331(*---------------------------------------------------------------------------*) 332 333val match_defn = Hol_defn 334 "match" 335 `(match (Atom b) l = (LENGTH l = 1) /\ b(HD l)) 336/\ (match (r1||r2) l = match r1 l \/ match r2 l) 337/\ (match (r1&r2) l = match r1 l /\ match r2 l) 338/\ (match (r1#r2) l = 339 EXISTS (\(s1,s2). match r1 s1 /\ match r2 s2) (SPLITS l)) 340/\ (match (r1%r2) l = 341 if NULL l then F else 342 EXISTS (\(s1,s2). if NULL s2 343 then match r1 s1 /\ match r2 [LAST s1] 344 else match r1 (s1<>[HD s2]) /\ match r2 s2) 345 (SPLITS l)) 346/\ (match (Repeat r) l = 347 if NULL l then T 348 else EXISTS (\(s1,s2). match r s1 /\ match (Repeat r) s2) 349 (TL(SPLITS l))) 350/\ (match (Prefix r) l = ?l'. match r (l <> l'))`; 351 352val (match_def, match_ind) = Defn.tprove 353(match_defn, 354 WF_REL_TAC `measure (regexp_size (K 0)) LEX (measure LENGTH)` 355 THEN RW_TAC list_ss [fetch "-" "regexp_size_def"] 356 THEN PROVE_TAC [MEM_ALL_SPLITS_LENGTH]); 357 358(*---------------------------------------------------------------------------*) 359(* Correctness of the matcher *) 360(*---------------------------------------------------------------------------*) 361 362val sem_match = store_thm 363 ("sem_match", 364 ``!r w. sem r w = match r w``, 365 recInduct match_ind THEN REPEAT CONJ_TAC THENL 366 [(* Atom c *) RW_TAC list_ss [sem_def,match_def], 367 (* r || r' *) RW_TAC list_ss [sem_def,match_def], 368 (* r & r' *) RW_TAC list_ss [sem_def,match_def], 369 (* r # r' *) RW_TAC list_ss [sem_def,match_def,EXISTS_ELIM_THM] 370 THEN EQ_TAC THEN RW_TAC list_ss [] THENL 371 [Q.EXISTS_TAC `(w1,w2)` 372 THEN SIMP_TAC list_ss [MEM_SPLITS] THEN SIMP_TAC std_ss [IN_DEF] THEN METIS_TAC [MEM_SPLITS], 373 Cases_on`x` THEN FULL_SIMP_TAC list_ss [IN_DEF] THEN PROVE_TAC[SPLITS_APPEND, IN_DEF]], 374 375 (* r1 % r2 *) 376 RW_TAC list_ss [sem_def,match_def,EXISTS_ELIM_THM,GSYM IN_THM] 377 THEN EQ_TAC THEN SIMP_TAC list_ss [pairTheory.EXISTS_PROD] THENL 378 [STRIP_TAC THEN 379 `~NULL (w1 <> [l'] <> w2)` by (Cases_on `w1` THEN RW_TAC list_ss []) THEN 380 `MEM (w1, l' ::w2) (SPLITS (w1 <> [l'] <> w2))` 381 by PROVE_TAC[MEM_SPLITS,GSYM listTheory.APPEND_ASSOC,APPEND_CONS] 382 THEN ASM_SIMP_TAC list_ss [] 383 THEN MAP_EVERY Q.EXISTS_TAC [`w1`, `l' ::w2`] 384 THEN RW_TAC list_ss [] 385 THEN METIS_TAC [listTheory.NULL,APPEND_CONS,listTheory.HD, IN_DEF], 386 Cases_on `l` THEN FULL_SIMP_TAC list_ss [] 387 THEN BasicProvers.NORM_TAC list_ss [] 388 THEN Cases_on `p_2` THEN FULL_SIMP_TAC list_ss [] THENL 389 [METIS_TAC [listTheory.APPEND_FRONT_LAST,listTheory.NULL, 390 SPLITS_APPEND,APPEND_NIL,IN_DEF], 391 METIS_TAC [SPLITS_APPEND,CONS_APPEND,listTheory.NULL, listTheory.HD, 392 listTheory.APPEND_ASSOC,listTheory.APPEND_FRONT_LAST,IN_DEF]]], 393 (* Repeat r *) 394 RW_TAC list_ss [sem_def] 395 THEN ONCE_REWRITE_TAC [match_def] 396 THEN RW_TAC list_ss [EXISTS_ELIM_THM] 397 THEN Cases_on `NULL l` THENL 398 [RW_TAC list_ss [] THEN Q.EXISTS_TAC `[]` THEN 399 RW_TAC list_ss [CONCAT_def] THEN PROVE_TAC [NULL_EQ_NIL], 400 FULL_SIMP_TAC list_ss [GSYM IN_THM] THEN EQ_TAC THEN 401 RW_TAC list_ss [EXISTS_PROD] THENL 402 [`EXISTS ($~ o NULL) wlist` by PROVE_TAC [NULL_CONCAT_THM,NOT_EVERY] THEN 403 IMP_RES_TAC FIRST_EXISTS_THM THEN 404 RULE_ASSUM_TAC (SIMP_RULE list_ss [o_DEF]) THEN 405 `sem r w /\ EVERY (sem r) suffix` by FULL_SIMP_TAC list_ss [EVERY_APPEND] 406 THEN 407 `CONCAT wlist = CONCAT (w::suffix)` 408 by (RW_TAC list_ss [CONCAT_APPEND_DISTRIB,CONCAT_def] THEN 409 RULE_ASSUM_TAC (CONV_RULE (ONCE_DEPTH_CONV ETA_CONV)) THEN 410 METIS_TAC[NULL_CONCAT_THM,APPEND,NULL_EQ_NIL,IN_DEF]) THEN 411 `MEM (w,CONCAT suffix) (TL(SPLITS(CONCAT wlist)))` 412 by RW_TAC list_ss [CONCAT_def, MEM_TL_SPLITS] THEN 413 PROVE_TAC [IN_DEF] 414 , 415 `?wlist. (p_2=CONCAT wlist) /\ EVERY (sem r) wlist` by PROVE_TAC[] THEN 416 Q.EXISTS_TAC `p_1::wlist` THEN RW_TAC list_ss [CONCAT_def] THEN 417 PROVE_TAC [MEM_TL,SPLITS_NON_EMPTY,SPLITS_APPEND,IN_DEF]]], 418 RW_TAC std_ss [sem_def, match_def]]); 419 420val () = export_theory (); 421