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 9["bossLib", "rich_listTheory", "metisLib", "pred_setTheory", "stringTheory", 10 "regexpTheory"]; 11*) 12 13open HolKernel Parse boolLib; 14open bossLib metisLib 15open pairTheory combinTheory listTheory rich_listTheory 16 stringTheory arithmeticTheory; 17open regexpTheory; 18open pred_setTheory; 19 20val () = new_theory "matcher"; 21 22(*---------------------------------------------------------------------------*) 23(* Symbolic tacticals. *) 24(*---------------------------------------------------------------------------*) 25 26infixr 0 THENC ORELSEC ORELSER; 27 28val Know = Q_TAC KNOW_TAC; 29val Suff = Q_TAC SUFF_TAC; 30val REVERSE = Tactical.REVERSE; 31 32fun FULL_CONV_TAC c = 33 CONV_TAC c THEN POP_ASSUM_LIST (EVERY o map (ASSUME_TAC o CONV_RULE c) o rev); 34 35local 36 val prover = METIS_TAC [ABS_PAIR_THM]; 37 38 fun rewriter th = 39 FULL_SIMP_TAC bool_ss [th] 40 THEN FULL_CONV_TAC (DEPTH_CONV pairLib.let_CONV); 41in 42 fun INTRODUCE_TAC tm = 43 let 44 val (l,r) = dest_eq tm 45 val assumer = if is_var l then K ALL_TAC else ASSUME_TAC 46 val vs = free_vars r 47 in 48 (KNOW_TAC (list_mk_exists (vs,tm)) THEN1 prover) 49 THEN STRIP_TAC 50 THEN POP_ASSUM (fn th => rewriter th THEN assumer th) 51 end; 52end; 53 54val Introduce = Q_TAC INTRODUCE_TAC; 55 56val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define; 57 58fun GCONJUNCTS th = 59 let 60 val tm = concl th 61 val (vs, imps) = strip_forall tm 62 val (xs, conjs) = strip_imp imps 63 val add_imps = fn th => foldr (fn (x,t) => DISCH x t) th xs 64 val add_vars = fn th => foldr (fn (v,t) => GEN v t) th vs 65 in 66 (map (add_vars o add_imps) o CONJUNCTS o UNDISCH_ALL o SPEC_ALL) th 67 end; 68 69(*---------------------------------------------------------------------------*) 70(* Misc. theorems *) 71(*---------------------------------------------------------------------------*) 72 73val MLEX_def = Define `MLEX f r x y = f x < f y \/ (f x = f y) /\ r x y`; 74 75val WF_MLEX = store_thm 76 ("WF_MLEX", 77 ``!f r. WF r ==> WF (MLEX f r)``, 78 RW_TAC std_ss [] 79 >> Suff `MLEX f r = inv_image ((<) LEX r) (\x. (f x, x))` 80 >- METIS_TAC [prim_recTheory.WF_LESS, WF_LEX, relationTheory.WF_inv_image] 81 >> RW_TAC std_ss [FUN_EQ_THM,MLEX_def,relationTheory.inv_image_def,LEX_DEF]); 82 83val NO_MEM = store_thm 84 ("NO_MEM", 85 ``!l. (!x. ~MEM x l) = (l = [])``, 86 Cases >> RW_TAC std_ss [MEM] >> METIS_TAC []); 87 88val set_of_list_def = Define 89 `(set_of_list [] = {}) /\ 90 (set_of_list (h :: t) = h INSERT set_of_list t)`; 91 92val set_of_list = store_thm 93 ("set_of_list", 94 ``!l x. x IN set_of_list l = MEM x l``, 95 Induct >> RW_TAC std_ss [set_of_list_def, MEM, NOT_IN_EMPTY, IN_INSERT]); 96 97val interval_def = Define 98 `(interval x 0 = []) /\ 99 (interval x (SUC n) = x :: interval (SUC x) n)`; 100 101val MEM_interval = store_thm 102 ("MEM_interval", 103 ``!x k n. MEM x (interval k n) = k <= x /\ x < k + n``, 104 Induct_on `n` 105 >> RW_TAC arith_ss [MEM, interval_def]); 106 107val MEM_FILTER = store_thm 108 ("MEM_FILTER", 109 ``!p l x. MEM x (FILTER p l) = MEM x l /\ p x``, 110 Induct_on `l` 111 >> RW_TAC std_ss [FILTER, MEM] 112 >> METIS_TAC []); 113 114val EVERY_MONO = store_thm 115 ("EVERY_MONO", 116 ``!p q l. (!x. p x ==> q x) /\ EVERY p l ==> EVERY q l``, 117 METIS_TAC [EVERY_MONOTONIC]); 118 119val partition_def = Define 120 `(partition p [] = ([],[])) /\ 121 (partition p (h :: t) = 122 let (l,r) = partition p t in if p h then (h::l,r) else (l,h::r))`; 123 124val LENGTH_partition = store_thm 125 ("LENGTH_partition", 126 ``!p l x y. (partition p l = (x,y)) ==> (LENGTH l = LENGTH x + LENGTH y)``, 127 Induct_on `l` 128 >> RW_TAC list_ss [partition_def] 129 >> Introduce `partition p l = (a,b)` 130 >> REPEAT (POP_ASSUM MP_TAC) 131 >> RW_TAC arith_ss [LENGTH] 132 >> RES_TAC 133 >> RW_TAC arith_ss [LENGTH]); 134 135val MEM_partition = store_thm 136 ("MEM_partition", 137 ``!p l x y k. 138 (partition p l = (x,y)) ==> 139 (MEM k x = p k /\ MEM k l) /\ 140 (MEM k y = ~p k /\ MEM k l)``, 141 Induct_on `l` 142 >> RW_TAC list_ss [partition_def] 143 >> Introduce `partition p l = (a,b)` 144 >> REPEAT (POP_ASSUM MP_TAC) 145 >> RW_TAC arith_ss [MEM] 146 >> RES_TAC 147 >> RW_TAC arith_ss [MEM] 148 >> METIS_TAC []); 149 150val BUTFIRSTN_EL = store_thm 151 ("BUTFIRSTN_EL", 152 ``!n l. 153 n < LENGTH l ==> 154 (EL n l :: BUTFIRSTN (SUC n) l = BUTFIRSTN n l)``, 155 Induct 156 >> Cases 157 >> RW_TAC arith_ss [EL, BUTFIRSTN, LENGTH, HD, TL]); 158 159val BUTFIRSTN_HD = store_thm 160 ("BUTFIRSTN_HD", 161 ``!n l. n < LENGTH l ==> (HD (BUTFIRSTN n l) = EL n l)``, 162 Induct 163 >> Cases 164 >> RW_TAC arith_ss [EL, BUTFIRSTN, LENGTH, HD, TL]); 165 166val BUTFIRSTN_TL = store_thm 167 ("BUTFIRSTN_TL", 168 ``!n l. n < LENGTH l ==> (TL (BUTFIRSTN n l) = BUTFIRSTN (SUC n) l)``, 169 Induct 170 >> Cases 171 >> RW_TAC arith_ss [EL, BUTFIRSTN, LENGTH, HD, TL]); 172 173(*---------------------------------------------------------------------------*) 174(* Theorems for reducing character equations. *) 175(*---------------------------------------------------------------------------*) 176 177val chr_11 = store_thm 178 ("chr_11", 179 ``!m n x. (m = ORD x) /\ (n = ORD x) = (m = n) /\ (m = ORD x)``, 180 METIS_TAC []); 181 182val chr_suff = store_thm 183 ("chr_suff", 184 ``!n p. (?x. (n = ORD x) \/ p x) = n < 256 \/ ?x. p x``, 185 METIS_TAC [ORD_ONTO]); 186 187val chr_suff1 = store_thm 188 ("chr_suff1", 189 ``!n. (?x. (n = ORD x)) = n < 256``, 190 METIS_TAC [ORD_ONTO]); 191 192(*---------------------------------------------------------------------------*) 193(* Dijkstra's reachability algorithm. *) 194(*---------------------------------------------------------------------------*) 195 196val accepting_path_def = Define 197 `(accepting_path (t : 'a->'a->bool) a s [] = a s) /\ 198 (accepting_path t a s (s' :: l) = t s s' /\ accepting_path t a s' l)`; 199 200val accepting_path_tail = store_thm 201 ("accepting_path_tail", 202 ``!p t a k ks. 203 ~p k /\ accepting_path t a k ks ==> 204 ?j js n. 205 n <= LENGTH ks /\ (j :: js = BUTFIRSTN n (k :: ks)) /\ 206 ~p j /\ EVERY p js /\ accepting_path t a j js``, 207 completeInduct_on `LENGTH ks` 208 >> RW_TAC std_ss [] 209 >> Cases_on `EVERY p ks` 210 >- (Q.EXISTS_TAC `k` 211 >> Q.EXISTS_TAC `ks` 212 >> Q.EXISTS_TAC `0` 213 >> RW_TAC arith_ss [EVERY_MEM, BUTFIRSTN]) 214 >> POP_ASSUM (MP_TAC o REWRITE_RULE [EVERY_MEM, MEM_EL]) 215 >> RW_TAC std_ss [] 216 >> Suff 217 `?j js n'. 218 n' <= LENGTH (BUTFIRSTN (SUC n) ks) /\ 219 (j::js = BUTFIRSTN n' (EL n ks :: BUTFIRSTN (SUC n) ks)) /\ ~p j /\ 220 ALL_EL p js /\ accepting_path t a j js` 221 >- (Q.PAT_X_ASSUM `!m. P m` (K ALL_TAC) 222 >> RW_TAC arith_ss [BUTFIRSTN_EL, LENGTH_BUTFIRSTN] 223 >> Know `n' + n < LENGTH ks` >- DECIDE_TAC 224 >> STRIP_TAC 225 >> Q.EXISTS_TAC `EL (n + n') ks` 226 >> Q.EXISTS_TAC `BUTFIRSTN (SUC n + n') ks` 227 >> Q.EXISTS_TAC `SUC n + n'` 228 >> FULL_SIMP_TAC arith_ss 229 [BUTFIRSTN, ALL_EL_BUTFIRSTN, BUTFIRSTN_EL, BUTFIRSTN_BUTFIRSTN, ADD] 230 >> Suff `(j = EL (n + n') ks) /\ (js = BUTFIRSTN (SUC (n + n')) ks)` 231 >- METIS_TAC [] 232 >> METIS_TAC [HD, TL, BUTFIRSTN_HD, BUTFIRSTN_TL]) 233 >> Q.PAT_X_ASSUM `!x. P x` MP_TAC 234 >> SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] 235 >> DISCH_THEN MATCH_MP_TAC 236 >> RW_TAC arith_ss [LENGTH_BUTFIRSTN] 237 >> POP_ASSUM (K ALL_TAC) 238 >> POP_ASSUM MP_TAC 239 >> POP_ASSUM MP_TAC 240 >> Q.SPEC_TAC (`k`, `k`) 241 >> Q.SPEC_TAC (`ks`, `ks`) 242 >> Induct_on `n` 243 >> Cases 244 >> RW_TAC arith_ss [BUTFIRSTN, LENGTH, EL, HD, accepting_path_def, TL] 245 >> METIS_TAC []); 246 247val (dijkstra_def, dijkstra_ind) = Defn.tprove 248 (Defn.Hol_defn "dijkstra" 249 `(dijkstra t a [] w = F) /\ 250 (dijkstra t a (s :: l) w = 251 let (x,y) = partition (t s) w 252 in EXISTS a x \/ dijkstra t a (x <> l) y)`, 253 WF_REL_TAC `measure (\ (_,_,l,w). LENGTH l + LENGTH w)` 254 >> RW_TAC list_ss [] 255 >> POP_ASSUM (ASSUME_TAC o SYM) 256 >> MP_TAC (Q.SPECL [`(t : 'a->'a->bool) s`, `w`, `x`, `y`] LENGTH_partition) 257 >> RW_TAC arith_ss []); 258 259val _ = save_thm ("dijkstra_def", dijkstra_def); 260 261val dijkstra = store_thm 262 ("dijkstra", 263 ``!t a u v. 264 EXISTS a u \/ dijkstra t a u v = 265 ?k l. 266 MEM k u /\ EVERY (\x. MEM x (u <> v)) l /\ 267 accepting_path t a k l``, 268 SIMP_TAC std_ss [EXISTS_MEM] 269 >> recInduct dijkstra_ind 270 >> RW_TAC list_ss [dijkstra_def] 271(* >> Introduce `partition (t s) w = (x,y)` *) 272 >> Q.PAT_X_ASSUM `!x y. P x y` (MP_TAC o Q.SPECL [`x`, `y`]) 273 >> RW_TAC std_ss [] 274 >> RW_TAC std_ss [RIGHT_AND_OVER_OR, EXISTS_OR_THM, GSYM DISJ_ASSOC] 275 >> RW_TAC std_ss [DISJ_ASSOC] 276 >> Know 277 `(a s \/ (?k. IS_EL k l /\ a k)) \/ SOME_EL a x = 278 a s \/ ?k. (IS_EL k x \/ IS_EL k l) /\ a k` 279 >- METIS_TAC [EXISTS_MEM] 280 >> DISCH_THEN (fn th => REWRITE_TAC [th]) 281 >> RW_TAC std_ss [GSYM DISJ_ASSOC] 282 >> Q.PAT_X_ASSUM `X = Y` (K ALL_TAC) 283 >> Cases_on 284 `?q. 285 ALL_EL (\k. (k = s) \/ IS_EL k l \/ IS_EL k w) q /\ 286 accepting_path t a s q` 287 >- (ASM_SIMP_TAC std_ss [] 288 >> Know 289 `?q. ALL_EL (\x. IS_EL x l \/ IS_EL x w) q /\ accepting_path t a s q` 290 >- (POP_ASSUM STRIP_ASSUME_TAC 291 >> MP_TAC (Q.SPECL [`\k. ~(k = s)`, `t`, `a`, `s`, `q`] 292 accepting_path_tail) 293 >> RW_TAC std_ss [] 294 >> Q.EXISTS_TAC `js` 295 >> RW_TAC std_ss [] 296 >> Suff `ALL_EL (\k. ~(k = s)) js /\ 297 ALL_EL (\k. (k = s) \/ IS_EL k l \/ IS_EL k w) js` 298 >- (SIMP_TAC std_ss [GSYM EVERY_CONJ] 299 >> Q.SPEC_TAC (`js`, `js`) 300 >> MATCH_MP_TAC EVERY_MONOTONIC 301 >> RW_TAC std_ss [FUN_EQ_THM] 302 >> METIS_TAC []) 303 >> RW_TAC std_ss [] 304 >> Q.PAT_X_ASSUM `X = BUTFIRSTN N L` MP_TAC 305 >> Cases_on `n` 306 >> RW_TAC std_ss [BUTFIRSTN] 307 >> Know `js = TL (BUTFIRSTN n' q)` >- METIS_TAC [TL] 308 >> RW_TAC arith_ss [BUTFIRSTN_TL] 309 >> METIS_TAC [ALL_EL_BUTFIRSTN]) 310 >> POP_ASSUM (K ALL_TAC) 311 >> RW_TAC std_ss [] 312 >> POP_ASSUM MP_TAC 313 >> Cases_on `q` 314 >> RW_TAC std_ss [accepting_path_def] 315 >> DISJ2_TAC 316 >> Q.EXISTS_TAC `h` 317 >> Q.EXISTS_TAC `t'` 318 >> RW_TAC std_ss [] 319 >- (FULL_SIMP_TAC std_ss [EVERY_DEF] >> METIS_TAC [MEM_partition]) 320 >> MATCH_MP_TAC EVERY_MONO 321 >> Q.EXISTS_TAC `\k. MEM k l \/ MEM k w` 322 >> (RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [EVERY_DEF]) 323 >> METIS_TAC [MEM_partition]) 324 >> ASM_SIMP_TAC std_ss [] 325 >> POP_ASSUM MP_TAC 326 >> SIMP_TAC std_ss [] 327 >> DISCH_THEN (MP_TAC o ONCE_REWRITE_RULE [PROVE [] ``a \/ b = ~a ==> b``]) 328 >> SIMP_TAC std_ss [] 329 >> STRIP_TAC 330 >> Cases_on `a s` 331 >- (Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `[]`) 332 >> RW_TAC std_ss [EVERY_DEF, accepting_path_def]) 333 >> RW_TAC std_ss [] 334 >> RW_TAC std_ss [RIGHT_AND_OVER_OR, EXISTS_OR_THM] 335 >> MATCH_MP_TAC (PROVE [] ``~a /\ (b = c) ==> (a \/ b = c)``) 336 >> CONJ_TAC 337 >- (SIMP_TAC std_ss [] 338 >> ONCE_REWRITE_TAC [PROVE [] ``a \/ b = ~a ==> b``] 339 >> ONCE_REWRITE_TAC [PROVE [] ``a \/ b = ~a ==> b``] 340 >> RW_TAC std_ss [] 341 >> STRIP_TAC 342 >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `k :: l'`) 343 >> RW_TAC std_ss [EVERY_DEF, accepting_path_def] 344 >| [METIS_TAC [MEM_partition], 345 MATCH_MP_TAC EVERY_MONO 346 >> Q.EXISTS_TAC `\k. IS_EL k x \/ IS_EL k l \/ IS_EL k y` 347 >> RW_TAC std_ss [] 348 >> METIS_TAC [MEM_partition], 349 METIS_TAC [MEM_partition]]) 350 >> HO_MATCH_MP_TAC 351 (METIS_PROVE [] 352 ``(!x y. A x y /\ C x y ==> (B x y = D x y)) ==> 353 ((?x y. A x y /\ B x y /\ C x y) = (?x y. A x y /\ D x y /\ C x y))``) 354 >> RW_TAC std_ss [] 355 >> EQ_TAC 356 >- (Q.SPEC_TAC (`l'`, `l'`) 357 >> MATCH_MP_TAC EVERY_MONOTONIC 358 >> METIS_TAC [MEM_partition]) 359 >> STRIP_TAC 360 >> Suff `EVERY (\k. ~(k = s)) l'` 361 >- (POP_ASSUM MP_TAC 362 >> SIMP_TAC std_ss [AND_IMP_INTRO, GSYM EVERY_CONJ] 363 >> Q.SPEC_TAC (`l'`, `l'`) 364 >> MATCH_MP_TAC EVERY_MONOTONIC 365 >> METIS_TAC [MEM_partition]) 366 >> RW_TAC std_ss [EVERY_MEM, MEM_EL] 367 >> CCONTR_TAC 368 >> FULL_SIMP_TAC std_ss [] 369 >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `BUTFIRSTN (SUC n) l'`) 370 >> RW_TAC std_ss [] 371 >- (Q.PAT_X_ASSUM `EVERY P L` MP_TAC 372 >> Q.SPEC_TAC (`EL n l'`, `s`) 373 >> RW_TAC std_ss [] 374 >> Know `SUC n <= LENGTH l'` >- DECIDE_TAC 375 >> Q.SPEC_TAC (`n`, `n`) 376 >> MATCH_MP_TAC ALL_EL_BUTFIRSTN 377 >> RW_TAC std_ss []) 378 >> POP_ASSUM MP_TAC 379 >> Q.PAT_X_ASSUM `accepting_path t a k l'` MP_TAC 380 >> POP_ASSUM_LIST (K ALL_TAC) 381 >> SIMP_TAC std_ss [AND_IMP_INTRO] 382 >> Q.SPEC_TAC (`k`, `k`) 383 >> Q.SPEC_TAC (`l'`, `l`) 384 >> Induct_on `n` 385 >> Cases 386 >> RW_TAC arith_ss [LENGTH, BUTFIRSTN, EL, HD, TL, accepting_path_def] 387 >> METIS_TAC []); 388 389val dijkstra_partition = store_thm 390 ("dijkstra_partition", 391 ``!t a p l u v. 392 (partition p l = (u,v)) ==> 393 (EXISTS a u \/ dijkstra t a u v = 394 ?k ks. MEM k u /\ EVERY (\j. MEM j l) ks /\ accepting_path t a k ks)``, 395 RW_TAC std_ss [dijkstra, MEM_APPEND] 396 >> Suff `!j. MEM j l = MEM j u \/ MEM j v` 397 >- RW_TAC std_ss [] 398 >> METIS_TAC [MEM_partition]); 399 400val dijkstra1 = store_thm 401 ("dijkstra1", 402 ``!t a s l. 403 MEM s l ==> 404 (a s \/ dijkstra t a [s] (FILTER (\x. ~(x = s)) l) = 405 ?ks. EVERY (\j. MEM j l) ks /\ accepting_path t a s ks)``, 406 RW_TAC std_ss [] 407 >> Know `a s = EXISTS a [s]` >- RW_TAC std_ss [EXISTS_DEF] 408 >> DISCH_THEN (fn th => REWRITE_TAC [th]) 409 >> RW_TAC std_ss [dijkstra] 410 >> RW_TAC std_ss [MEM, MEM_APPEND] 411 >> Suff `!j. (j = s) \/ IS_EL j (FILTER (\x. ~(x = s)) l) = IS_EL j l` 412 >- RW_TAC std_ss [] 413 >> RW_TAC std_ss [MEM_FILTER] 414 >> METIS_TAC []); 415 416(*---------------------------------------------------------------------------*) 417(* BIGLIST is designed to speed up evaluation of very long lists. *) 418(* (But it doesn't seem to have the desired effect, so we don't use it.) *) 419(*---------------------------------------------------------------------------*) 420 421val drop_def = pureDefine 422 `(drop 0 l = l) /\ 423 (drop (SUC i) l = if NULL l then [] else drop i (TL l))`; 424 425val BIGLIST_def = Define `BIGLIST l = drop 0 l`; 426 427val drop_nil = prove 428 (``!i. drop i [] = []``, 429 Induct >> RW_TAC std_ss [NULL_DEF, drop_def]); 430 431val null_drop = store_thm 432 ("null_drop", 433 ``!i l. NULL (drop i l) = LENGTH l <= i``, 434 Induct 435 >- (RW_TAC arith_ss [drop_def] >> METIS_TAC [LENGTH_NIL, NULL_EQ_NIL]) 436 >> Cases_on `l` 437 >> RW_TAC arith_ss [drop_def, LENGTH, NULL_DEF, TL]); 438 439val tl_drop = store_thm 440 ("tl_drop", 441 ``!i l. 442 TL (drop i l) = if i < LENGTH l then drop (SUC i) l else TL (drop i l)``, 443 Induct 444 >- (RW_TAC arith_ss [drop_def, NULL_EQ_NIL] 445 >> FULL_SIMP_TAC arith_ss [LENGTH]) 446 >> Cases_on `l` 447 >> RW_TAC arith_ss [drop_def, LENGTH, NULL_EQ_NIL, TL] 448 >> Q.PAT_X_ASSUM `!l. P l` (fn th => ONCE_REWRITE_TAC [th]) 449 >> FULL_SIMP_TAC arith_ss [LENGTH, drop_def, NULL_EQ_NIL]); 450 451val head_drop = store_thm 452 ("head_drop", 453 ``!i l h t. (drop i l = h :: t) ==> (HD (drop i l) = h)``, 454 RW_TAC std_ss [HD]); 455 456val tail_drop = store_thm 457 ("tail_drop", 458 ``!l i h t. (drop i l = h :: t) ==> (drop (SUC i) l = t)``, 459 Induct >- RW_TAC bool_ss [drop_def, drop_nil] 460 >> RW_TAC std_ss [drop_def, TL, NULL, drop_nil] 461 >> POP_ASSUM MP_TAC 462 >> Cases_on `i` 463 >> RW_TAC std_ss [drop_def, NULL_EQ_NIL, TL]); 464 465val length_drop = store_thm 466 ("length_drop", 467 ``!i l h. (drop i l = [h]) ==> (LENGTH l = SUC i)``, 468 Induct >- RW_TAC arith_ss [drop_def, LENGTH] 469 >> Cases 470 >> RW_TAC std_ss [drop_def, TL, NULL_EQ_NIL, drop_nil, LENGTH]); 471 472(*---------------------------------------------------------------------------*) 473(* Non-deterministic and deterministic automata. *) 474(*---------------------------------------------------------------------------*) 475 476val () = type_abbrev ("na", Type`:'a # ('a->'b->'a->bool) # ('a->bool)`); 477val () = type_abbrev ("da", Type`:'a # ('a->'b->'a) # ('a->bool)`); 478 479val initial_def = Define `initial ((i,trans,acc) : ('a,'b) na) = i`; 480val transition_def = Define `transition ((i,trans,acc) : ('a,'b) na) = trans`; 481val accept_def = Define `accept ((i,trans,acc) : ('a,'b) na) = acc`; 482 483val na_step_def = Define 484 `(na_step ((i,trans,acc) : ('a,'b) na) s [] = (acc s)) /\ 485 (na_step (i,trans,acc) s (h :: t) = 486 ?s'. trans s h s' /\ na_step (i,trans,acc) s' t)`; 487 488val na_accepts_def = Define 489 `na_accepts (i,trans,acc) l = na_step (i,trans,acc) i l`; 490 491val da_step_def = Define 492 `(da_step ((i,trans,acc) : ('a,'b) da) s [] = acc s) /\ 493 (da_step (i,trans,acc) s (h :: t) = 494 da_step (i,trans,acc) (trans s h) t)`; 495 496val da_accepts_def = Define 497 `da_accepts (i,trans,acc) l = da_step (i,trans,acc) i l`; 498 499val na2da_def = Define 500 `na2da (n : ('a,'b) na) = 501 ({initial n}, 502 (\s c. {y | ?x. x IN s /\ (transition n) x c y}), 503 (\s. ?x. x IN s /\ accept n x))`; 504 505val na2da_lemma = prove 506 (``!n s l. da_step (na2da n) s l = ?x. x IN s /\ na_step n x l``, 507 RW_TAC std_ss [] 508 >> Introduce `n = (i,trans,acc)` 509 >> RW_TAC std_ss [na2da_def, initial_def, transition_def, accept_def] 510 >> Q.SPEC_TAC (`s`, `s`) 511 >> Induct_on `l` 512 >- (RW_TAC std_ss [da_step_def, na_step_def, IN_SING] 513 >> METIS_TAC []) 514 >> RW_TAC std_ss [da_step_def, na_step_def] 515 >> RW_TAC std_ss [GSYM na2da_def, GSPECIFICATION] 516 >> METIS_TAC []); 517 518val na2da = store_thm 519 ("na2da", 520 ``!n l. na_accepts n l = da_accepts (na2da n) l``, 521 RW_TAC std_ss [] 522 >> Introduce `n = (i,trans,acc)` 523 >> RW_TAC std_ss [na_accepts_def, da_accepts_def, na2da_def] 524 >> RW_TAC std_ss [na2da_lemma, GSYM na2da_def, IN_SING] 525 >> RW_TAC std_ss [initial_def]); 526 527(*---------------------------------------------------------------------------*) 528(* A checker that works by constructing a deterministic finite automata. *) 529(*---------------------------------------------------------------------------*) 530 531val regexp2na_def = Define 532 `(regexp2na (Atom b) = (1, (\s x s'. (s=1) /\ b x /\ (s'=0)), \s. s=0)) /\ 533 (regexp2na (r1 # r2) = 534 let (i1,t1,a1) = regexp2na r1 in 535 let (i2,t2,a2) = regexp2na r2 in 536 (i1 + i2 + 1, 537 (\s x s'. 538 if s <= i2 then t2 s x s' 539 else if s' <= i2 then a1 (s - (i2 + 1)) /\ t2 i2 x s' 540 else t1 (s - (i2 + 1)) x (s' - (i2 + 1))), 541 \s. if s <= i2 then a2 s else a2 i2 /\ a1 (s - (i2 + 1)))) /\ 542 (regexp2na (r1 % r2) = 543 let (i1,t1,a1) = regexp2na r1 in 544 let (i2,t2,a2) = regexp2na r2 in 545 (i1 + i2 + 1, 546 (\s x s'. 547 if s <= i2 then t2 s x s' 548 else if s' <= i2 then ?y. t1 (s - (i2 + 1)) x y /\ a1 y /\ t2 i2 x s' 549 else t1 (s - (i2 + 1)) x (s' - (i2 + 1))), 550 a2)) /\ 551 (regexp2na (r1 || r2) = 552 let (i1,t1,a1) = regexp2na r1 in 553 let (i2,t2,a2) = regexp2na r2 in 554 (i1 + i2 + 2, 555 (\s x s'. 556 if s = i1 + i2 + 2 then 557 if s' <= i1 then t1 i1 x s' else t2 i2 x (s' - (i1 + 1)) 558 else if s <= i1 then t1 s x s' 559 else ~(s' <= i1) /\ t2 (s - (i1 + 1)) x (s' - (i1 + 1))), 560 \s. 561 if s = i1 + i2 + 2 then a1 i1 \/ a2 i2 562 else if s <= i1 then a1 s else a2 (s - (i1 + 1)))) /\ 563 (regexp2na (r1 & r2) = 564 let (i1,t1,a1) = regexp2na r1 in 565 let (i2,t2,a2) = regexp2na r2 in 566 (i1 * i2 + i1 + i2, 567 (\s x s'. 568 t1 (s DIV (i2 + 1)) x (s' DIV (i2 + 1)) /\ 569 t2 (s MOD (i2 + 1)) x (s' MOD (i2 + 1))), 570 \s. a1 (s DIV (i2 + 1)) /\ a2 (s MOD (i2 + 1)))) /\ 571 (regexp2na (Repeat r) = 572 let (i,t,a) = regexp2na r in 573 if a i then (i, (\s x s'. t s x s' \/ a s /\ t i x s'), a) 574 else 575 (i + 1, 576 (\s x s'. 577 if s = i + 1 then t i x s' 578 else t s x s' \/ a s /\ t i x s'), 579 \s. (s = i + 1) \/ a s)) /\ 580 (regexp2na (Prefix r) = 581 let (i,t,a) = regexp2na r in 582 (i, t, \s. ?l. accepting_path (\s s'. ?x. t s x s') a s l))`; 583 584val regexp2da_def = Define `regexp2da r = na2da (regexp2na r)`; 585 586val da_match_def = Define `da_match r = da_accepts (regexp2da r)`; 587 588(*---------------------------------------------------------------------------*) 589(* Correctness of the finite automata matcher *) 590(*---------------------------------------------------------------------------*) 591 592val regexp2na_bounds = prove 593 (``!r i trans acc. 594 (regexp2na r = (i,trans,acc)) ==> 595 (!s. acc s ==> s <= i) /\ 596 (!s x s'. trans s x s' ==> s <= i /\ s' <= i)``, 597 Induct (* 7 subgoals *) 598 >| [(* Atom *) 599 FULL_SIMP_TAC std_ss [regexp2na_def], 600 (* # *) 601 Introduce `r = r1` 602 >> Introduce `r' = r2` 603 >> REPEAT GEN_TAC 604 >> SIMP_TAC std_ss [regexp2na_def] 605 >> Introduce `regexp2na r1 = (i1,t1,a1)` 606 >> Introduce `regexp2na r2 = (i2,t2,a2)` 607 >> STRIP_TAC 608 >> REPEAT (POP_ASSUM MP_TAC) 609 >> RW_TAC std_ss [] (* 3 subgoals *) 610 >> POP_ASSUM MP_TAC 611 >> RW_TAC std_ss [] 612 >> RES_TAC >> fs [], 613 (* % *) 614 Introduce `r = r1` 615 >> Introduce `r' = r2` 616 >> REPEAT GEN_TAC 617 >> SIMP_TAC std_ss [regexp2na_def] 618 >> Introduce `regexp2na r1 = (i1,t1,a1)` 619 >> Introduce `regexp2na r2 = (i2,t2,a2)` 620 >> REPEAT (POP_ASSUM MP_TAC) 621 >> RW_TAC std_ss [] 622 >> POP_ASSUM MP_TAC 623 >> RW_TAC std_ss [] 624 >> RES_TAC >> fs [], 625 (* || *) 626 Introduce `r = r1` 627 >> Introduce `r' = r2` 628 >> REPEAT GEN_TAC 629 >> SIMP_TAC std_ss [regexp2na_def] 630 >> Introduce `regexp2na r1 = (i1,t1,a1)` 631 >> Introduce `regexp2na r2 = (i2,t2,a2)` 632 >> REPEAT (POP_ASSUM MP_TAC) 633 >> (RW_TAC std_ss [] >> POP_ASSUM MP_TAC >> RW_TAC std_ss []) 634 >> RES_TAC >> fs [], 635 (* & *) 636 Introduce `r = r1` 637 >> Introduce `r' = r2` 638 >> REPEAT GEN_TAC 639 >> SIMP_TAC std_ss [regexp2na_def] 640 >> Introduce `regexp2na r1 = (i1,t1,a1)` 641 >> Introduce `regexp2na r2 = (i2,t2,a2)` 642 >> Q.PAT_X_ASSUM `!i. P i` (MP_TAC o Q.SPECL [`i2`,`t2`,`a2`]) 643 >> Q.PAT_X_ASSUM `!i. P i` (MP_TAC o Q.SPECL [`i1`,`t1`,`a1`]) 644 >> SIMP_TAC std_ss [] 645 >> REPEAT (DISCH_THEN STRIP_ASSUME_TAC) 646 >> CONJ_TAC 647 >| [REPEAT (POP_ASSUM MP_TAC) 648 >> (RW_TAC std_ss [] >> POP_ASSUM MP_TAC >> RW_TAC std_ss []) 649 >> MP_TAC (Q.SPEC `i2 + 1` DIVISION) 650 >> DISCH_THEN (MP_TAC o Q.SPEC `s` o SIMP_RULE arith_ss []) 651 >> DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 652 >> MATCH_MP_TAC LESS_EQ_TRANS 653 >> Q.EXISTS_TAC `(s DIV (i2 + 1)) * (i2 + 1) + i2` 654 >> SIMP_TAC std_ss [ADD_MONO_LESS_EQ, LESS_EQ_MONO_ADD_EQ] 655 >> CONJ_TAC >- (RES_TAC >> fs []) 656 >> Know `!m n. m * n + m = m * (n + 1)` 657 >- METIS_TAC [MULT_CLAUSES, ADD1, MULT_COMM] 658 >> DISCH_THEN (fn th => REWRITE_TAC [th]) 659 >> MATCH_MP_TAC LESS_MONO_MULT 660 >> METIS_TAC [], 661 REPEAT (POP_ASSUM MP_TAC) 662 >> (RW_TAC std_ss [] >> POP_ASSUM MP_TAC >> RW_TAC std_ss []) 663 >| [MP_TAC (Q.SPEC `i2 + 1` DIVISION) 664 >> DISCH_THEN (MP_TAC o Q.SPEC `s` o SIMP_RULE arith_ss []) 665 >> DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 666 >> MATCH_MP_TAC LESS_EQ_TRANS 667 >> Q.EXISTS_TAC `(s DIV (i2 + 1)) * (i2 + 1) + i2` 668 >> SIMP_TAC std_ss [ADD_MONO_LESS_EQ, LESS_EQ_MONO_ADD_EQ] 669 >> CONJ_TAC >- (RES_TAC >> fs []) 670 >> Know `!m n. m * n + m = m * (n + 1)` 671 >- METIS_TAC [MULT_CLAUSES, ADD1, MULT_COMM] 672 >> DISCH_THEN (fn th => REWRITE_TAC [th]) 673 >> MATCH_MP_TAC LESS_MONO_MULT 674 >> METIS_TAC [], 675 MP_TAC (Q.SPEC `i2 + 1` DIVISION) 676 >> DISCH_THEN (MP_TAC o Q.SPEC `s'` o SIMP_RULE arith_ss []) 677 >> DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 678 >> MATCH_MP_TAC LESS_EQ_TRANS 679 >> Q.EXISTS_TAC `(s' DIV (i2 + 1)) * (i2 + 1) + i2` 680 >> SIMP_TAC std_ss [ADD_MONO_LESS_EQ, LESS_EQ_MONO_ADD_EQ] 681 >> CONJ_TAC >- (RES_TAC >> fs []) 682 >> Know `!m n. m * n + m = m * (n + 1)` 683 >- METIS_TAC [MULT_CLAUSES, ADD1, MULT_COMM] 684 >> DISCH_THEN (fn th => REWRITE_TAC [th]) 685 >> MATCH_MP_TAC LESS_MONO_MULT 686 >> METIS_TAC []]], 687 (* Repeat *) 688 REPEAT GEN_TAC 689 >> SIMP_TAC std_ss [regexp2na_def] 690 >> Introduce `regexp2na r = (i,t,a)` 691 >> REPEAT (POP_ASSUM MP_TAC) 692 >> (RW_TAC std_ss [] >> POP_ASSUM MP_TAC >> RW_TAC std_ss []) 693 >> METIS_TAC [LESS_EQ_TRANS, LESS_EQ_ADD, ADD_COMM, LESS_EQ_REFL], 694 (* Prefix *) 695 REPEAT GEN_TAC 696 >> SIMP_TAC std_ss [regexp2na_def] 697 >> Introduce `regexp2na r = (i,t,a)` 698 >> REPEAT (POP_ASSUM MP_TAC) 699 >> (RW_TAC std_ss [] >> POP_ASSUM MP_TAC >> RW_TAC std_ss []) 700 >| [POP_ASSUM MP_TAC 701 >> Cases_on `l` 702 >> RW_TAC std_ss [accepting_path_def] 703 >> METIS_TAC [], 704 METIS_TAC [], 705 METIS_TAC []]]); 706 707val regexp2na_acc = prove 708 (``!r i trans acc s. (regexp2na r = (i,trans,acc)) /\ acc s ==> s <= i``, 709 METIS_TAC [regexp2na_bounds]); 710 711val regexp2na_trans = prove 712 (``!r i trans acc s x s'. 713 (regexp2na r = (i,trans,acc)) /\ trans s x s' ==> s <= i /\ s' <= i``, 714 METIS_TAC [regexp2na_bounds]); 715 716val na_match_atom = prove 717 (``!b l. na_accepts (regexp2na (Atom b)) l = sem (Atom b) l``, 718 RW_TAC std_ss [regexp2na_def, sem_def, LENGTH_EQ_ONE, na_accepts_def] 719 >> Cases_on `l` 720 >> RW_TAC std_ss [na_step_def, HD] 721 >> Cases_on `t` 722 >> RW_TAC std_ss [na_step_def, HD]); 723 724val na_match_concat = prove 725 (``!r1 r2. 726 (!l. na_accepts (regexp2na r1) l = sem r1 l) /\ 727 (!l. na_accepts (regexp2na r2) l = sem r2 l) ==> 728 !l. na_accepts (regexp2na (r1 # r2)) l = sem (r1 # r2) l``, 729 REPEAT GEN_TAC 730 >> Introduce `regexp2na r1 = (i1, t1, a1)` 731 >> Introduce `regexp2na r2 = (i2, t2, a2)` 732 >> NTAC 2 (RW_TAC std_ss [regexp2na_def, sem_def, na_accepts_def]) 733 >> RW_TAC std_ss [regexp2na_def, sem_def, na_accepts_def] 734 >> REPEAT (Q.PAT_X_ASSUM `!x. P x` (fn th => REWRITE_TAC [GSYM th])) 735 >> Suff 736 `!k. 737 na_step 738 (i1 + i2 + 1, 739 (\s x s'. 740 if s <= i2 then t2 s x s' 741 else if s' <= i2 then a1 (s - (i2 + 1)) /\ t2 i2 x s' 742 else t1 (s - (i2 + 1)) x (s' - (i2 + 1))), 743 (\s. if s <= i2 then a2 s else a2 i2 /\ a1 (s - (i2 + 1)))) 744 (k + i2 + 1) l = 745 ?w1 w2. 746 (l = w1 <> w2) /\ na_step (i1,t1,a1) k w1 /\ 747 na_step (i2,t2,a2) i2 w2` 748 >- METIS_TAC [] 749 >> Induct_on `l` 750 >- (RW_TAC std_ss [na_step_def, APPEND_eq_NIL] 751 >> FULL_SIMP_TAC arith_ss [] 752 >> METIS_TAC []) 753 >> RW_TAC std_ss [] 754 >> Know `!P Q. (Q = P [] \/ ?t h. P (h :: t)) ==> (Q = (?l. P l))` 755 >- (POP_ASSUM_LIST (K ALL_TAC) >> METIS_TAC [list_CASES]) 756 >> DISCH_THEN HO_MATCH_MP_TAC 757 >> RW_TAC arith_ss [APPEND, na_step_def] 758 >> HO_MATCH_MP_TAC 759 (METIS_PROVE [] 760 ``!P Q R X Y Z. 761 ((?x : num. P x /\ Q x /\ Z x) = X) /\ 762 ((?x. ~P x /\ R x /\ Z x) = Y) ==> 763 ((?x. (if P x then Q x else R x) /\ Z x) = X \/ Y)``) 764 >> REVERSE CONJ_TAC 765 >- (Suff 766 `!P Q. 767 ((?x : num. P (x + i2 + 1)) = Q) ==> 768 ((?x. ~(x <= i2) /\ P x) = Q)` 769 >- (DISCH_THEN HO_MATCH_MP_TAC 770 >> POP_ASSUM MP_TAC 771 >> RW_TAC arith_ss [] 772 >> POP_ASSUM (K ALL_TAC) 773 >> METIS_TAC []) 774 >> POP_ASSUM (K ALL_TAC) 775 >> Suff `!x. ~(x <= i2) = (?y. x = y + i2 + 1)` >- METIS_TAC [] 776 >> RW_TAC arith_ss [] 777 >> REVERSE EQ_TAC >- RW_TAC arith_ss [] 778 >> RW_TAC arith_ss [] 779 >> Q.EXISTS_TAC `x - (i2 + 1)` 780 >> DECIDE_TAC) 781 >> POP_ASSUM (K ALL_TAC) 782 >> HO_MATCH_MP_TAC 783 (METIS_PROVE [] 784 ``!A B C D E. 785 (!x. E x ==> A x) /\ (!x. A x ==> (D x = E x)) ==> 786 ((?x. A x /\ (B /\ C x) /\ D x) = B /\ ?x. C x /\ E x)``) 787 >> CONJ_TAC 788 >- (Cases_on `l` 789 >> RW_TAC std_ss [na_step_def] 790 >> METIS_TAC [regexp2na_trans, regexp2na_acc]) 791 >> Induct_on `l` >- RW_TAC std_ss [na_step_def] 792 >> RW_TAC std_ss [na_step_def] 793 >> METIS_TAC [regexp2na_trans]); 794 795val na_match_fuse = prove 796 (``!r1 r2. 797 (!l. na_accepts (regexp2na r1) l = sem r1 l) /\ 798 (!l. na_accepts (regexp2na r2) l = sem r2 l) ==> 799 !l. na_accepts (regexp2na (r1 % r2)) l = sem (r1 % r2) l``, 800 REPEAT GEN_TAC 801 >> Introduce `regexp2na r1 = (i1, t1, a1)` 802 >> Introduce `regexp2na r2 = (i2, t2, a2)` 803 >> NTAC 2 (RW_TAC std_ss [regexp2na_def, sem_def, na_accepts_def]) 804 >> REPEAT (Q.PAT_X_ASSUM `!x. P x` (fn th => REWRITE_TAC [GSYM th])) 805 >> Suff 806 `!k. 807 na_step 808 (i1 + i2 + 1, 809 (\s x s'. 810 if s <= i2 then t2 s x s' 811 else if s' <= i2 then 812 ?y. t1 (s - (i2 + 1)) x y /\ a1 y /\ t2 i2 x s' 813 else t1 (s - (i2 + 1)) x (s' - (i2 + 1))),a2) (k + i2 + 1) l = 814 ?w1 w2 c. 815 (l = w1 <> [c] <> w2) /\ na_step (i1,t1,a1) k (w1 <> [c]) /\ 816 na_step (i2,t2,a2) i2 ([c] <> w2)` 817 >- METIS_TAC [] 818 >> Induct_on `l` 819 >- (RW_TAC std_ss [na_step_def, APPEND_eq_NIL] 820 >> Suff `~(k + i2 + 1 <= i2)` >- METIS_TAC [regexp2na_acc] 821 >> RW_TAC arith_ss []) 822 >> RW_TAC std_ss [] 823 >> HO_MATCH_MP_TAC 824 (METIS_PROVE [list_CASES] 825 ``!P Q. (Q = P [] \/ ?t h. P (h :: t)) ==> (Q = (?l. P l))``) 826 >> RW_TAC arith_ss [na_step_def] 827 >> HO_MATCH_MP_TAC 828 (METIS_PROVE [] 829 ``!P Q R X Y Z. 830 ((?x : num. P x /\ Q x /\ Z x) = X) /\ 831 ((?x. ~P x /\ R x /\ Z x) = Y) ==> 832 ((?x. (if P x then Q x else R x) /\ Z x) = X \/ Y)``) 833 >> REVERSE CONJ_TAC 834 >- (Suff 835 `!P Q. 836 ((?x : num. P (x + i2 + 1)) = Q) ==> 837 ((?x. ~(x <= i2) /\ P x) = Q)` 838 >- (DISCH_THEN HO_MATCH_MP_TAC 839 >> POP_ASSUM MP_TAC 840 >> RW_TAC arith_ss [] 841 >> POP_ASSUM (K ALL_TAC) 842 >> RW_TAC arith_ss [na_step_def, APPEND] 843 >> METIS_TAC []) 844 >> POP_ASSUM (K ALL_TAC) 845 >> Suff `!x. ~(x <= i2) = (?y. x = y + i2 + 1)` >- METIS_TAC [] 846 >> RW_TAC arith_ss [] 847 >> REVERSE EQ_TAC >- RW_TAC arith_ss [] 848 >> RW_TAC arith_ss [] 849 >> Q.EXISTS_TAC `x - (i2 + 1)` 850 >> DECIDE_TAC) 851 >> POP_ASSUM (K ALL_TAC) 852 >> RW_TAC std_ss [APPEND, na_step_def] 853 >> HO_MATCH_MP_TAC 854 (METIS_PROVE [] 855 ``!A B C D E G. 856 (!x. G x ==> A x) /\ (!x. A x ==> (E x = G x)) ==> 857 ((?x. A x /\ (?y. B y /\ C y /\ D x) /\ E x) = 858 (?y. B y /\ C y) /\ (?x. D x /\ G x))``) 859 >> CONJ_TAC 860 >- (Cases_on `l` 861 >> RW_TAC std_ss [na_step_def] 862 >> METIS_TAC [regexp2na_trans, regexp2na_acc]) 863 >> Induct_on `l` >- RW_TAC std_ss [na_step_def] 864 >> RW_TAC std_ss [na_step_def] 865 >> METIS_TAC [regexp2na_trans]); 866 867val na_match_or = prove 868 (``!r1 r2. 869 (!l. na_accepts (regexp2na r1) l = sem r1 l) /\ 870 (!l. na_accepts (regexp2na r2) l = sem r2 l) ==> 871 !l. na_accepts (regexp2na (r1 || r2)) l = sem (r1 || r2) l``, 872 REPEAT GEN_TAC 873 >> Introduce `regexp2na r1 = (i1, t1, a1)` 874 >> Introduce `regexp2na r2 = (i2, t2, a2)` 875 >> NTAC 2 (RW_TAC std_ss [regexp2na_def, sem_def, na_accepts_def]) 876 >> REPEAT (Q.PAT_X_ASSUM `!x. P x` (fn th => REWRITE_TAC [GSYM th])) 877 >> Cases_on `l` >- RW_TAC std_ss [na_step_def] 878 >> RW_TAC std_ss [na_step_def] 879 >> HO_MATCH_MP_TAC 880 (METIS_PROVE [] 881 ``!P Q R X Y Z. 882 ((?x : num. Z x /\ P x /\ R x) = X) /\ 883 ((?x. ~Z x /\ Q x /\ R x) = Y) ==> 884 ((?x. (if Z x then P x else Q x) /\ R x) = X \/ Y)``) 885 >> CONJ_TAC 886 >- (HO_MATCH_MP_TAC 887 (METIS_PROVE [] 888 ``!P Q R X. 889 (!x. P x ==> X x) /\ (!x : num. X x ==> (Q x = R x)) ==> 890 ((?x. X x /\ P x /\ Q x) = (?x. P x /\ R x))``) 891 >> CONJ_TAC >- METIS_TAC [regexp2na_trans] 892 >> Induct_on `t` 893 >- RW_TAC arith_ss [na_step_def] 894 >> RW_TAC arith_ss [na_step_def] 895 >> HO_MATCH_MP_TAC 896 (METIS_PROVE [] 897 ``!P Q R. 898 (!x : num. P x ==> (Q x = R x)) ==> 899 ((?x. P x /\ Q x) = (?x. P x /\ R x))``) 900 >> RW_TAC std_ss [] 901 >> rename1 `na_step _ s''' t = na_step (i1,t1,a1) s''' t` 902 >> Know `s''' <= i1` >- METIS_TAC [regexp2na_trans] (* was: s'' *) 903 >> POP_ASSUM (K ALL_TAC) 904 >> STRIP_TAC 905 >> Q.PAT_X_ASSUM `!k. P k` (MP_TAC o Q.SPEC `s'''`) 906 >> RW_TAC arith_ss []) 907 >> HO_MATCH_MP_TAC 908 (METIS_PROVE [] 909 ``!P Q. 910 (!x. P x ==> ?y. x = y + (i1 + 1)) /\ 911 (!x : num. P (x + (i1 + 1)) = Q x) ==> 912 ((?x. P x) = (?x. Q x))``) 913 >> CONJ_TAC 914 >- (RW_TAC std_ss [] 915 >> Q.EXISTS_TAC `s' - (i1 + 1)` 916 >> POP_ASSUM (K ALL_TAC) 917 >> DECIDE_TAC) 918 >> RW_TAC arith_ss [] 919 >> MATCH_MP_TAC (PROVE [] ``!x y z. (x ==> (y = z)) ==> (x /\ y = x /\ z)``) 920 >> STRIP_TAC 921 >> rename1 `na_step _ (i1 + (s'' + 1)) t = na_step (i2,t2,a2) s'' t` 922 >> Know `s'' <= i2` >- METIS_TAC [regexp2na_trans] (* was: s' *) 923 >> POP_ASSUM (K ALL_TAC) 924 >> Q.SPEC_TAC (`s''`, `k`) 925 >> Induct_on `t` >- RW_TAC arith_ss [na_step_def] 926 >> RW_TAC arith_ss [na_step_def] 927 >> HO_MATCH_MP_TAC 928 (METIS_PROVE [] 929 ``!P Q. 930 (!x. P x ==> ?y. x = y + (i1 + 1)) /\ 931 (!x : num. P (x + (i1 + 1)) = Q x) ==> 932 ((?x. P x) = (?x. Q x))``) 933 >> CONJ_TAC 934 >- (Q.PAT_X_ASSUM `!x. P x` (K ALL_TAC) 935 >> RW_TAC std_ss [] 936 >> Q.EXISTS_TAC `s' - (i1 + 1)` 937 >> POP_ASSUM (K ALL_TAC) 938 >> DECIDE_TAC) 939 >> RW_TAC arith_ss [] 940 >> MATCH_MP_TAC (PROVE [] ``!x y z. (x ==> (y = z)) ==> (x /\ y = x /\ z)``) 941 >> STRIP_TAC 942 >> rename1 `na_step _ (i1 + (s'' + 1)) t = na_step (i2,t2,a2) s'' t` 943 >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `s''`) (* was: s' *) 944 >> Know `s'' <= i2` >- METIS_TAC [regexp2na_trans] 945 >> RW_TAC arith_ss []); 946 947val na_match_and = prove 948 (``!r1 r2. 949 (!l. na_accepts (regexp2na r1) l = sem r1 l) /\ 950 (!l. na_accepts (regexp2na r2) l = sem r2 l) ==> 951 !l. na_accepts (regexp2na (r1 & r2)) l = sem (r1 & r2) l``, 952 REPEAT GEN_TAC 953 >> Introduce `regexp2na r1 = (i1, t1, a1)` 954 >> Introduce `regexp2na r2 = (i2, t2, a2)` 955 >> NTAC 2 (RW_TAC std_ss [regexp2na_def, sem_def, na_accepts_def]) 956 >> REPEAT (Q.PAT_X_ASSUM `!x. P x` (fn th => REWRITE_TAC [GSYM th])) 957 >> Suff 958 `!j k. 959 j <= i1 /\ k <= i2 ==> 960 (na_step 961 (i1 * i2 + i1 + i2, 962 (\s x s'. 963 t1 (s DIV (i2 + 1)) x (s' DIV (i2 + 1)) /\ 964 t2 (s MOD (i2 + 1)) x (s' MOD (i2 + 1))), 965 (\s. a1 (s DIV (i2 + 1)) /\ a2 (s MOD (i2 + 1)))) 966 (j * (i2 + 1) + k) l = 967 na_step (i1,t1,a1) j l /\ na_step (i2,t2,a2) k l)` 968 >- (DISCH_THEN (MP_TAC o Q.SPECL [`i1`, `i2`]) 969 >> RW_TAC arith_ss [LEFT_ADD_DISTRIB]) 970 >> Know `0 < i2 + 1` >- DECIDE_TAC >> STRIP_TAC 971 >> Know `!k. k < i2 + 1 = k <= i2` >- DECIDE_TAC >> STRIP_TAC 972 >> Induct_on `l` >- RW_TAC std_ss [na_step_def, DIV_MULT, MOD_MULT] 973 >> RW_TAC std_ss [na_step_def, DIV_MULT, MOD_MULT] 974 >> CONV_TAC 975 (REDEPTH_CONV (LEFT_AND_EXISTS_CONV ORELSEC RIGHT_AND_EXISTS_CONV)) 976 >> RW_TAC std_ss [] 977 >> MP_TAC (Q.SPEC `i2 + 1` DIVISION) 978 >> ASM_REWRITE_TAC [] 979 >> HO_MATCH_MP_TAC 980 (METIS_PROVE [] 981 ``!P Q A B C. 982 ((?x. A x /\ B (P x)) = C) ==> 983 ((!x. (x = P x) /\ Q x) ==> ((?x. A x /\ B x) = C))``) 984 >> HO_MATCH_MP_TAC 985 (METIS_PROVE [] 986 ``!P A B C. 987 (!x. A x ==> P x) /\ ((?x. A x /\ (P x ==> B x)) = C) ==> 988 ((?x. A x /\ B x) = C)``) 989 >> Q.EXISTS_TAC `\x. x DIV (i2 + 1) <= i1 /\ x MOD (i2 + 1) <= i2` 990 >> BETA_TAC 991 >> CONJ_TAC >- METIS_TAC [regexp2na_trans] 992 >> Q.PAT_X_ASSUM `!x. P x` (fn th => RW_TAC std_ss [th]) 993 >> HO_MATCH_MP_TAC 994 (METIS_PROVE [] 995 ``!P A B C. 996 (!x. A x ==> P x) /\ ((?x. A x /\ B x) = C) ==> 997 ((?x. A x /\ (P x ==> B x)) = C)``) 998 >> CONJ_TAC >- METIS_TAC [regexp2na_trans] 999 >> EQ_TAC >- METIS_TAC [] 1000 >> RW_TAC std_ss [] 1001 >> rename1 `na_step (i2,t2,a2) s''' l` 1002 >> rename1 `na_step (i1,t1,a1) s'' l` 1003 >> Q.EXISTS_TAC `s'' * (i2 + 1) + s'''` (* was: s', s'' *) 1004 >> Know `s''' <= i2` >- METIS_TAC [regexp2na_trans] 1005 >> RW_TAC std_ss [DIV_MULT, MOD_MULT]); 1006 1007val na_match_repeat = prove 1008 (``!r. 1009 (!l. na_accepts (regexp2na r) l = sem r l) ==> 1010 !l. na_accepts (regexp2na (Repeat r)) l = sem (Repeat r) l``, 1011 REPEAT GEN_TAC 1012 >> Introduce `regexp2na r = (i, t, a)` 1013 >> (NTAC 2 (RW_TAC std_ss [regexp2na_def, sem_def, na_accepts_def]) 1014 >> (REPEAT o Q.PAT_X_ASSUM `!x. P x`) 1015 (fn th => REWRITE_TAC [GSYM (MATCH_MP EQ_EXT th)])) 1016 >- (HO_MATCH_MP_TAC 1017 (METIS_PROVE [list_CASES] 1018 ``!P Q. (Q = P [] \/ ?w ws. P (w :: ws)) ==> (Q = (?l. P l))``) 1019 >> RW_TAC std_ss [CONCAT_def, ALL_EL] 1020 >> Cases_on `l = []` >- RW_TAC std_ss [na_step_def] 1021 >> RW_TAC std_ss [] 1022 >> Suff 1023 `!k. 1024 (na_step (i,(\s x s'. t s x s' \/ a s /\ t i x s'),a) k l = 1025 ?w ws. 1026 (l = w <> CONCAT ws) /\ na_step (i,t,a) k w /\ 1027 ALL_EL (na_step (i,t,a) i) ws)` 1028 >- RW_TAC std_ss [] 1029 >> POP_ASSUM (K ALL_TAC) 1030 >> Induct_on `l` 1031 >- (RW_TAC std_ss [na_step_def, APPEND_eq_NIL] 1032 >> REVERSE (Cases_on `a k`) >- RW_TAC std_ss [] 1033 >> RW_TAC std_ss [] 1034 >> Q.EXISTS_TAC `[]` 1035 >> RW_TAC std_ss [CONCAT_def, ALL_EL]) 1036 >> RW_TAC std_ss [] 1037 >> HO_MATCH_MP_TAC 1038 (METIS_PROVE [list_CASES] 1039 ``!P Q. (Q = P [] \/ ?c cs. P (c :: cs)) ==> (Q = (?l. P l))``) 1040 >> RW_TAC std_ss [na_step_def, APPEND] 1041 >> RW_TAC std_ss [RIGHT_AND_OVER_OR, EXISTS_OR_THM] 1042 >> MATCH_MP_TAC (PROVE [] ``(a = d) /\ (b = c) ==> (a \/ b = c \/ d)``) 1043 >> CONJ_TAC >- METIS_TAC [] 1044 >> POP_ASSUM (K ALL_TAC) 1045 >> REVERSE (Cases_on `a k`) >- RW_TAC std_ss [] 1046 >> RW_TAC std_ss [] 1047 >> POP_ASSUM (K ALL_TAC) 1048 >> EQ_TAC 1049 >- (RW_TAC std_ss [] 1050 >> Q.EXISTS_TAC `(h::w) :: ws` 1051 >> RW_TAC std_ss [ALL_EL, CONCAT_def, na_step_def, APPEND] 1052 >> PROVE_TAC []) 1053 >> RW_TAC std_ss [] 1054 >> Induct_on `ws` >- RW_TAC std_ss [CONCAT_def] 1055 >> Cases >- RW_TAC std_ss [CONCAT_def, APPEND, ALL_EL, na_step_def] 1056 >> POP_ASSUM (K ALL_TAC) 1057 >> RW_TAC std_ss [CONCAT_def, APPEND, ALL_EL, na_step_def] 1058 >> PROVE_TAC []) 1059 >> HO_MATCH_MP_TAC 1060 (METIS_PROVE [list_CASES] 1061 ``!P Q. (Q = P [] \/ ?w ws. P (w :: ws)) ==> (Q = (?l. P l))``) 1062 >> RW_TAC std_ss [CONCAT_def, ALL_EL] 1063 >> Cases_on `l` >- RW_TAC std_ss [na_step_def] 1064 >> RW_TAC std_ss [na_step_def] 1065 >> HO_MATCH_MP_TAC 1066 (METIS_PROVE [list_CASES] 1067 ``!P Q. (Q = P [] \/ ?x xs. P (x :: xs)) ==> (Q = (?l. P l))``) 1068 >> RW_TAC std_ss [CONCAT_def, ALL_EL, APPEND, na_step_def] 1069 >> HO_MATCH_MP_TAC 1070 (METIS_PROVE [] 1071 ``!P Q A B C. 1072 (!x. P x ==> x <= i) /\ 1073 (!x. x <= i ==> (Q x = ?y z. A y z /\ B x y z /\ C y z)) ==> 1074 ((?x. P x /\ Q x) = ?y z. A y z /\ (?x. P x /\ B x y z) /\ C y z)``) 1075 >> CONJ_TAC >- METIS_TAC [regexp2na_trans] 1076 >> Induct_on `t'` 1077 >- (RW_TAC arith_ss [na_step_def, APPEND_eq_NIL] 1078 >> rename1 `s'' <= i` 1079 >> REVERSE (Cases_on `a s''`) >- RW_TAC std_ss [] (* was: s' *) 1080 >> RW_TAC std_ss [] 1081 >> Q.EXISTS_TAC `[]` 1082 >> RW_TAC std_ss [CONCAT_def, ALL_EL]) 1083 >> RW_TAC std_ss [] 1084 >> HO_MATCH_MP_TAC 1085 (METIS_PROVE [list_CASES] 1086 ``!P Q. (Q = P [] \/ ?x xs. P (x :: xs)) ==> (Q = (?l. P l))``) 1087 >> RW_TAC arith_ss [CONCAT_def, ALL_EL, APPEND, na_step_def] 1088 >> RW_TAC std_ss [RIGHT_AND_OVER_OR, EXISTS_OR_THM] 1089 >> MATCH_MP_TAC (PROVE [] ``(a = d) /\ (b = c) ==> (a \/ b = c \/ d)``) 1090 >> CONJ_TAC 1091 >- (HO_MATCH_MP_TAC 1092 (METIS_PROVE [] 1093 ``!P A B C. 1094 (!x. A x ==> P x) /\ ((?x. A x /\ (P x ==> B x)) = C) ==> 1095 ((?x. A x /\ B x) = C)``) 1096 >> Q.EXISTS_TAC `\x. x <= i` 1097 >> BETA_TAC 1098 >> CONJ_TAC >- METIS_TAC [regexp2na_trans] 1099 >> Q.PAT_X_ASSUM `!x. P x` (fn th => RW_TAC std_ss [th]) 1100 >> HO_MATCH_MP_TAC 1101 (METIS_PROVE [] 1102 ``!P A B C. 1103 (!x. A x ==> P x) /\ ((?x. A x /\ B x) = C) ==> 1104 ((?x. A x /\ (P x ==> B x)) = C)``) 1105 >> CONJ_TAC >- METIS_TAC [regexp2na_trans] 1106 >> METIS_TAC []) 1107 >> rename1 `s'' <= i` 1108 >> REVERSE (Cases_on `a s''`) >- RW_TAC std_ss [] (* was: s'' *) 1109 >> RW_TAC std_ss [] 1110 >> HO_MATCH_MP_TAC 1111 (METIS_PROVE [] 1112 ``!P Q R. 1113 (!x. P x ==> x <= i) /\ ((?x. P x /\ (x <= i ==> Q x)) = R) ==> 1114 ((?x. P x /\ Q x) = R)``) 1115 >> CONJ_TAC >- METIS_TAC [regexp2na_trans] 1116 >> RW_TAC std_ss [] 1117 >> NTAC 3 (POP_ASSUM (K ALL_TAC)) 1118 >> HO_MATCH_MP_TAC 1119 (METIS_PROVE [] 1120 ``!P Q R. 1121 (!x. P x ==> x <= i) /\ ((?x. P x /\ Q x) = R) ==> 1122 ((?x. P x /\ (x <= i ==> Q x)) = R)``) 1123 >> CONJ_TAC >- METIS_TAC [regexp2na_trans] 1124 >> EQ_TAC 1125 >- (RW_TAC std_ss [] 1126 >> Q.EXISTS_TAC `(h::xs) :: ws` 1127 >> RW_TAC std_ss [ALL_EL, CONCAT_def, na_step_def, APPEND] 1128 >> PROVE_TAC []) 1129 >> RW_TAC std_ss [] 1130 >> REPEAT (POP_ASSUM MP_TAC) 1131 >> Cases_on `ws` >- RW_TAC std_ss [CONCAT_def] 1132 >> Cases_on `h'` >- RW_TAC std_ss [na_step_def, ALL_EL] 1133 >> RW_TAC std_ss [CONCAT_def, APPEND, ALL_EL, na_step_def] 1134 >> METIS_TAC []); 1135 1136val na_match_prefix = prove 1137 (``!r. 1138 (!l. na_accepts (regexp2na r) l = sem r l) ==> 1139 !l. na_accepts (regexp2na (Prefix r)) l = sem (Prefix r) l``, 1140 REPEAT GEN_TAC 1141 >> Introduce `regexp2na r = (i, t, a)` 1142 >> (NTAC 2 (RW_TAC std_ss [regexp2na_def, sem_def, na_accepts_def]) 1143 >> (REPEAT o Q.PAT_X_ASSUM `!x. P x`) 1144 (fn th => REWRITE_TAC [GSYM (MATCH_MP EQ_EXT th)])) 1145 >> Suff 1146 `!k. 1147 na_step 1148 (i,t,(\s. ?l. accepting_path (\s s'. ?x. t s x s') a s l)) k l = 1149 ?w'. na_step (i,t,a) k (l <> w')` 1150 >- RW_TAC std_ss [] 1151 >> REVERSE (Induct_on `l`) 1152 >- (RW_TAC std_ss [na_step_def, APPEND] 1153 >> HO_MATCH_MP_TAC 1154 (METIS_PROVE [] 1155 ``!P Q R. 1156 (!s. P s ==> (Q s = ?w. R w s)) ==> 1157 ((?s. P s /\ Q s) = ?w s. P s /\ R w s)``) 1158 >> POP_ASSUM (fn th => RW_TAC std_ss [GSYM th])) 1159 >> RW_TAC std_ss [APPEND, na_step_def] 1160 >> Suff 1161 `!n k. 1162 (?l. (LENGTH l = n) /\ accepting_path (\s s'. ?x. t s x s') a k l) = 1163 ?w'. (LENGTH w' = n) /\ na_step (i,t,a) k w'` 1164 >- METIS_TAC [] 1165 >> Induct >- RW_TAC std_ss [LENGTH_NIL, accepting_path_def, na_step_def] 1166 >> RW_TAC std_ss [LENGTH_CONS, accepting_path_def, na_step_def, 1167 GSYM LEFT_EXISTS_AND_THM] 1168 >> METIS_TAC []); 1169 1170val na_match = prove 1171 (``!r l. na_accepts (regexp2na r) l = sem r l``, 1172 Induct 1173 >> RW_TAC std_ss 1174 [na_match_atom, na_match_concat, na_match_fuse, 1175 na_match_or, na_match_and, na_match_repeat, na_match_prefix]); 1176 1177val da_accepts_regexp2da = prove 1178 (``!r. sem r = da_accepts (regexp2da r)``, 1179 RW_TAC std_ss [FUN_EQ_THM, regexp2da_def, GSYM na2da, na_match]); 1180 1181val da_match = store_thm 1182 ("da_match", 1183 ``!r l. da_match r l = sem r l``, 1184 RW_TAC std_ss [da_match_def, da_accepts_regexp2da]); 1185 1186val kleene_regexp2dfa = store_thm 1187 ("kleene_regexp2dfa", 1188 ``!exp : 'a regexp. ?dfa : (num->bool,'a) da. sem exp = da_accepts dfa``, 1189 METIS_TAC [da_accepts_regexp2da]); 1190 1191(*---------------------------------------------------------------------------*) 1192(* A version of the automata matcher that is easy to execute. *) 1193(*---------------------------------------------------------------------------*) 1194 1195val initial_regexp2na_def = pureDefine 1196 `initial_regexp2na r = initial (regexp2na r)`; 1197 1198val accept_regexp2na_def = pureDefine 1199 `accept_regexp2na r = accept (regexp2na r)`; 1200 1201val transition_regexp2na_def = pureDefine 1202 `transition_regexp2na r = transition (regexp2na r)`; 1203 1204(* 1205val (accept_regexp2na_prefix_def, accept_regexp2na_prefix_ind) = Defn.tprove 1206 (Defn.Hol_defn "accept_regexp2na_prefix" 1207 `(accept_regexp2na_prefix r [] w = F) /\ 1208 (accept_regexp2na_prefix r (s :: l) w = 1209 accept_regexp2na_prefix' r s l [] w) /\ 1210 (accept_regexp2na_prefix' r s l w [] = accept_regexp2na_prefix r l w) /\ 1211 (accept_regexp2na_prefix' r s l w (h :: t) = 1212 if (?x. transition_regexp2na r s x h) then 1213 accept_regexp2na r h \/ accept_regexp2na_prefix' r s (h :: l) w t 1214 else accept_regexp2na_prefix' r s l (h :: w) t)`, 1215 WF_REL_TAC 1216 `MLEX (sum_case (\ (_,l,w). 2 * (LENGTH l + LENGTH w)) 1217 (\ (_,_,l,w,t). 2 * (LENGTH l + LENGTH w + LENGTH t) + 1)) 1218 (measure (sum_case (\_. 0) (\ (_,_,_,_,t). LENGTH t)))` 1219 >> RW_TAC arith_ss [MLEX_def, LENGTH] 1220 >> RW_TAC std_ss [GSYM prim_recTheory.measure_thm] 1221 >> CONV_TAC (DEPTH_CONV ETA_CONV) 1222 >> METIS_TAC [WF_MLEX, prim_recTheory.WF_measure]); 1223 1224val accept_regexp2na_prefix_ind1 = hd (GCONJUNCTS accept_regexp2na_prefix_ind); 1225*) 1226 1227val exists_transition_regexp2na_def = pureDefine 1228 `exists_transition_regexp2na r s s' = ?x. transition_regexp2na r s x s'`; 1229 1230val transition_regexp2na_fuse_def = Define 1231 `(transition_regexp2na_fuse a t 0 = F) /\ 1232 (transition_regexp2na_fuse a t (SUC s') = 1233 a s' /\ t s' \/ transition_regexp2na_fuse a t s')`; 1234 1235val transition_regexp2na_fuse = prove 1236 (``!k r s x i t a. 1237 (regexp2na r = (i,t,a)) ==> 1238 (transition_regexp2na_fuse a (t s x) k = ?y. a y /\ y < k /\ t s x y)``, 1239 Induct 1240 >> RW_TAC arith_ss [transition_regexp2na_fuse_def] 1241 >> METIS_TAC [prim_recTheory.LESS_THM]); 1242 1243val initial_regexp2na = store_thm 1244 ("initial_regexp2na", 1245 ``(initial_regexp2na (Atom b : 'a regexp) = 1) /\ 1246 (initial_regexp2na (r1 # r2 : 'a regexp) = 1247 initial_regexp2na r1 + initial_regexp2na r2 + 1) /\ 1248 (initial_regexp2na (r1 % r2) = 1249 initial_regexp2na r1 + initial_regexp2na r2 + 1) /\ 1250 (initial_regexp2na (r1 || r2) = 1251 initial_regexp2na r1 + initial_regexp2na r2 + 2) /\ 1252 (initial_regexp2na (r1 & r2) = 1253 let i1 = initial_regexp2na r1 in 1254 let i2 = initial_regexp2na r2 in i1 * i2 + i1 + i2) /\ 1255 (initial_regexp2na (Repeat r : 'a regexp) = 1256 let i = initial_regexp2na r in 1257 if accept_regexp2na r i then i else i + 1) /\ 1258 (initial_regexp2na (Prefix r : 'a regexp) = initial_regexp2na r)``, 1259 Introduce `regexp2na r1 = (i1,t1,a1)` 1260 >> Introduce `regexp2na r2 = (i2,t2,a2)` 1261 >> Introduce `regexp2na r = (i,t,a)` 1262 >> NTAC 2 1263 (RW_TAC std_ss 1264 [regexp2na_def, initial_def, accept_def, 1265 initial_regexp2na_def, accept_regexp2na_def])); 1266 1267val accept_regexp2na = store_thm 1268 ("accept_regexp2na", 1269 ``(accept_regexp2na (Atom b : 'a regexp) s = (s = 0)) /\ 1270 (accept_regexp2na (r1 # r2 : 'a regexp) s = 1271 let i2 = initial_regexp2na r2 in 1272 if s <= i2 then accept_regexp2na r2 s 1273 else accept_regexp2na r2 i2 /\ 1274 accept_regexp2na r1 (s - (i2 + 1))) /\ 1275 (accept_regexp2na (r1 % r2) s = accept_regexp2na r2 s) /\ 1276 (accept_regexp2na (r1 || r2) s = 1277 let i1 = initial_regexp2na r1 in 1278 let i2 = initial_regexp2na r2 in 1279 if s = i1 + i2 + 2 then 1280 accept_regexp2na r1 i1 \/ accept_regexp2na r2 i2 1281 else if s <= i1 then accept_regexp2na r1 s 1282 else accept_regexp2na r2 (s - (i1 + 1))) /\ 1283 (accept_regexp2na (r1 & r2) s = 1284 let i2 = initial_regexp2na r2 in 1285 accept_regexp2na r1 (s DIV (i2 + 1)) /\ 1286 accept_regexp2na r2 (s MOD (i2 + 1))) /\ 1287 (accept_regexp2na (Repeat r : 'a regexp) s = 1288 accept_regexp2na r s \/ 1289 let i = initial_regexp2na r in 1290 (s = i + 1) /\ ~accept_regexp2na r i) /\ 1291 (accept_regexp2na (Prefix r : 'a regexp) s = 1292 accept_regexp2na r s \/ 1293 dijkstra (exists_transition_regexp2na r) (accept_regexp2na r) 1294 [s] (FILTER (\x. ~(x = s)) (interval 0 (SUC (initial_regexp2na r)))))``, 1295 Introduce `regexp2na r1 = (i1,t1,a1)` 1296 >> Introduce `regexp2na r2 = (i2,t2,a2)` 1297 >> Introduce `regexp2na r = (i,t,a)` 1298 >> NTAC 2 1299 (RW_TAC std_ss 1300 [regexp2na_def, initial_def, accept_def, 1301 initial_regexp2na_def, accept_regexp2na_def]) 1302 >- METIS_TAC [] 1303 >> Know `exists_transition_regexp2na r = \s s'. ?x. t s x s'` 1304 >- RW_TAC std_ss 1305 [exists_transition_regexp2na_def, FUN_EQ_THM, 1306 transition_regexp2na_def, transition_def] 1307 >> DISCH_THEN (fn th => RW_TAC std_ss [th]) 1308 >> REVERSE (Cases_on `s <= i`) 1309 >- (MATCH_MP_TAC (PROVE [] ``~a /\ ~b ==> (a = b)``) 1310 >> RW_TAC std_ss [] 1311 >| [Cases_on `l` 1312 >> RW_TAC std_ss [accepting_path_def] 1313 >> METIS_TAC [regexp2na_acc, regexp2na_trans], 1314 METIS_TAC [regexp2na_acc], 1315 RW_TAC std_ss [dijkstra_def] 1316 >> Suff `!l. partition (\s'. ?x. t s x s') l = ([],l)` 1317 >- (DISCH_THEN (fn th => FULL_SIMP_TAC std_ss [th]) 1318 >> RW_TAC std_ss [EXISTS_DEF, APPEND, dijkstra_def]) 1319 >> Induct 1320 >> RW_TAC std_ss [partition_def] 1321 >> METIS_TAC [regexp2na_trans]]) 1322 >> Know `MEM s (interval 0 (SUC i))` 1323 >- RW_TAC arith_ss [MEM_interval] 1324 >> RW_TAC std_ss [dijkstra1] 1325 >> REVERSE EQ_TAC >- METIS_TAC [] 1326 >> RW_TAC arith_ss [MEM_interval] 1327 >> Q.EXISTS_TAC `l` 1328 >> Know `!k. k < SUC i = k <= i` >- DECIDE_TAC 1329 >> DISCH_THEN (fn th => RW_TAC std_ss [th]) 1330 >> POP_ASSUM MP_TAC 1331 >> Q.SPEC_TAC (`s`, `s`) 1332 >> Induct_on `l` 1333 >> RW_TAC std_ss [accepting_path_def, EVERY_DEF] 1334 >> METIS_TAC [regexp2na_trans]); 1335 1336val transition_regexp2na = store_thm 1337 ("transition_regexp2na", 1338 ``(transition_regexp2na (Atom b : 'a regexp) s x s' = 1339 (s = 1) /\ (s' = 0) /\ b x) /\ 1340 (transition_regexp2na (r1 # r2 : 'a regexp) s x s' = 1341 let i2 = initial_regexp2na r2 in 1342 if s <= i2 then transition_regexp2na r2 s x s' 1343 else if s' <= i2 then 1344 accept_regexp2na r1 (s - (i2 + 1)) /\ 1345 transition_regexp2na r2 i2 x s' 1346 else 1347 transition_regexp2na r1 (s - (i2 + 1)) x (s' - (i2 + 1))) /\ 1348 (transition_regexp2na (r1 % r2) s x s' = 1349 let i2 = initial_regexp2na r2 in 1350 if s <= i2 then transition_regexp2na r2 s x s' 1351 else if s' <= i2 then 1352 transition_regexp2na r2 i2 x s' /\ 1353 let i1 = initial_regexp2na r1 in 1354 transition_regexp2na_fuse (accept_regexp2na r1) 1355 (transition_regexp2na r1 (s - (i2 + 1)) x) (SUC i1) 1356 else transition_regexp2na r1 (s - (i2 + 1)) x (s' - (i2 + 1))) /\ 1357 (transition_regexp2na (r1 || r2) s x s' = 1358 let i1 = initial_regexp2na r1 in 1359 let i2 = initial_regexp2na r2 in 1360 if s = i1 + i2 + 2 then 1361 if s' <= i1 then transition_regexp2na r1 i1 x s' 1362 else transition_regexp2na r2 i2 x (s' - (i1 + 1)) 1363 else if s <= i1 then transition_regexp2na r1 s x s' 1364 else ~(s' <= i1) /\ 1365 transition_regexp2na r2 (s - (i1 + 1)) x (s' - (i1 + 1))) /\ 1366 (transition_regexp2na (r1 & r2) s x s' = 1367 let i2 = initial_regexp2na r2 in 1368 transition_regexp2na r1 (s DIV (i2 + 1)) x (s' DIV (i2 + 1)) /\ 1369 transition_regexp2na r2 (s MOD (i2 + 1)) x (s' MOD (i2 + 1))) /\ 1370 (transition_regexp2na (Repeat r : 'a regexp) s x s' = 1371 let i = initial_regexp2na r in 1372 if s = i + 1 then 1373 ~accept_regexp2na r i /\ 1374 transition_regexp2na r i x s' 1375 else 1376 transition_regexp2na r s x s' \/ 1377 accept_regexp2na r s /\ transition_regexp2na r i x s') /\ 1378 (transition_regexp2na (Prefix r : 'a regexp) s x s' = 1379 transition_regexp2na r s x s')``, 1380 Introduce `regexp2na r1 = (i1,t1,a1)` 1381 >> Introduce `regexp2na r2 = (i2,t2,a2)` 1382 >> Introduce `regexp2na r = (i,t,a)` 1383 >> NTAC 2 1384 (RW_TAC std_ss 1385 [regexp2na_def, initial_def, accept_def, transition_def, 1386 initial_regexp2na_def, accept_regexp2na_def, transition_regexp2na_def]) 1387 >| [METIS_TAC [], 1388 MP_TAC (Q.SPECL [`SUC i1`, `r1`, `s - (i2 + 1)`, `x`, `i1`, `t1`, `a1`] 1389 transition_regexp2na_fuse) 1390 >> RW_TAC std_ss [] 1391 >> Know `!p q. p < SUC q = p <= q` >- DECIDE_TAC 1392 >> METIS_TAC [regexp2na_acc], 1393 Know `!n. ~(n + 1 <= n)` >- DECIDE_TAC 1394 >> METIS_TAC [regexp2na_trans, regexp2na_acc], 1395 Know `!n. ~(n + 1 <= n)` >- DECIDE_TAC 1396 >> METIS_TAC [regexp2na_trans, regexp2na_acc]]); 1397 1398val eval_accepts_def = pureDefine 1399 `(eval_accepts (Prefix r) l = 1400 EXISTS (accept_regexp2na r) l \/ 1401 let i = initial_regexp2na r in 1402 dijkstra (exists_transition_regexp2na r) (accept_regexp2na r) 1403 l (FILTER (\x. ~MEM x l) (interval 0 (SUC (initial_regexp2na r))))) /\ 1404 (eval_accepts r l = EXISTS (accept_regexp2na r) l)`; 1405 1406val eval_accepts = prove 1407 (``!r l. eval_accepts r l = EXISTS (accept_regexp2na r) l``, 1408 Cases 1409 >> RW_TAC std_ss [eval_accepts_def] 1410 >> normalForms.REMOVE_ABBR_TAC 1411 >> RW_TAC std_ss [] 1412 >> Introduce `r' = r` 1413 >> Introduce `regexp2na r = (i,t,a)` 1414 >> RW_TAC std_ss [dijkstra] 1415 >> RW_TAC std_ss [MEM_APPEND, EXISTS_MEM, accept_regexp2na_def, 1416 accept_def, regexp2na_def] 1417 >> Know `exists_transition_regexp2na r = \s s'. ?x. t s x s'` 1418 >- RW_TAC std_ss 1419 [exists_transition_regexp2na_def, FUN_EQ_THM, 1420 transition_regexp2na_def, transition_def] 1421 >> DISCH_THEN (fn th => RW_TAC std_ss [th]) 1422 >> RW_TAC arith_ss [MEM_FILTER, MEM_interval] 1423 >> HO_MATCH_MP_TAC 1424 (METIS_PROVE [] 1425 ``(!l k. C k l ==> B k l) ==> 1426 ((?k l'. A k /\ B k l' /\ C k l') = (?e. A e /\ ?l. C e l))``) 1427 >> Know `!x y. x < SUC y = x <= y` >- DECIDE_TAC 1428 >> DISCH_THEN 1429 (fn th => ASM_SIMP_TAC std_ss [th, initial_regexp2na_def, initial_def]) 1430 >> Induct 1431 >> RW_TAC std_ss [EVERY_DEF, accepting_path_def] 1432 >> METIS_TAC [regexp2na_trans]); 1433 1434val calc_transitions_def = Define 1435 `(calc_transitions r l c 0 a = a) /\ 1436 (calc_transitions r l c (SUC s') a = 1437 calc_transitions r l c s' 1438 (if EXISTS (\s. transition_regexp2na r s c s') l then s' :: a else a))`; 1439 1440val eval_transitions_def = pureDefine 1441 `eval_transitions r l c = 1442 calc_transitions r l c (SUC (initial_regexp2na r)) []`; 1443 1444val areport_def = pureDefine `areport h b = b`; 1445 1446val astep_def = Define 1447 `(astep r l [] = eval_accepts r l) /\ 1448 (astep r l (c :: cs) = astep r (eval_transitions r l c) cs)`; 1449 1450val amatch_def = Define 1451 `amatch r l = let i = initial_regexp2na r in astep r [i] l`; 1452 1453val acheckpt_def = Define 1454 `(acheckpt r f h l [] = T) /\ 1455 (acheckpt r f h l (c :: cs) = 1456 let l' = eval_transitions r l c in 1457 let h = c :: h in 1458 (eval_accepts r l' ==> areport h (f (c :: cs))) /\ acheckpt r f h l' cs)`; 1459 1460val acheck_def = Define 1461 `acheck r f l = let i = initial_regexp2na r in acheckpt r f [] [i] l`; 1462 1463(*---------------------------------------------------------------------------*) 1464(* Correctness of this version of the automata matcher. *) 1465(*---------------------------------------------------------------------------*) 1466 1467val da_accepts_na2da = prove 1468 (``!n. da_accepts (na2da n) = da_step (na2da n) (set_of_list [initial n])``, 1469 STRIP_TAC 1470 >> Introduce `n = (i,t,a)` 1471 >> RW_TAC std_ss 1472 [FUN_EQ_THM, na2da_def, da_accepts_def, initial_def, set_of_list_def]); 1473 1474val da_step_regexp2na = prove 1475 (``(da_step (na2da (regexp2na r)) (set_of_list l) [] = 1476 EXISTS (accept (regexp2na r)) l) /\ 1477 (da_step (na2da (regexp2na r)) (set_of_list l) (c :: cs) = 1478 let i = initial (regexp2na r) in 1479 let l' = calc_transitions r l c (SUC i) [] in 1480 da_step (na2da (regexp2na r)) (set_of_list l') cs)``, 1481 Introduce `regexp2na r = (i,t,a)` 1482 >> RW_TAC std_ss [da_step_def, na2da_def, EXISTS_MEM, set_of_list] 1483 >> REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) 1484 >> RW_TAC std_ss [EXTENSION, GSPECIFICATION, set_of_list, initial_def] 1485 >> Suff 1486 `!k. 1487 MEM x (calc_transitions r l c (SUC i) k) = 1488 IS_EL x k \/ (x < SUC i /\ ?y. IS_EL y l /\ transition (i,t,a) y c x)` 1489 >- (DISCH_THEN (MP_TAC o Q.SPEC `[]`) 1490 >> Know `!x. x < SUC i = x <= i` >- DECIDE_TAC 1491 >> RW_TAC std_ss [MEM, transition_def] 1492 >> METIS_TAC [regexp2na_trans]) 1493 >> Q.SPEC_TAC (`SUC i`, `n`) 1494 >> Induct (* 2 subgoals *) 1495 >- RW_TAC arith_ss 1496 [calc_transitions_def, EXISTS_MEM, MEM, transition_regexp2na_def] 1497 >> GEN_TAC >> ONCE_REWRITE_TAC [calc_transitions_def] 1498 >> RW_TAC arith_ss [EXISTS_MEM, MEM, transition_regexp2na_def] (* 2 subgoals *) 1499 >| [ EQ_TAC >> rpt STRIP_TAC >> ASM_REWRITE_TAC [] >| 1500 [ fs [] >> DISJ2_TAC >> Q.EXISTS_TAC `s` >> ASM_REWRITE_TAC [], 1501 fs [] >> DISJ2_TAC >> Q.EXISTS_TAC `y` >> ASM_REWRITE_TAC [], 1502 Cases_on `x = n` >- ASM_REWRITE_TAC [] \\ 1503 DISJ2_TAC \\ 1504 `!a b. ~(a < b) /\ a < SUC b = (a = b)` by DECIDE_TAC \\ 1505 `x < n` by PROVE_TAC [] >> ASM_REWRITE_TAC [] \\ 1506 Q.EXISTS_TAC `y` >> ASM_REWRITE_TAC [] ], 1507 EQ_TAC >> rpt STRIP_TAC >> ASM_REWRITE_TAC [] >| 1508 [ fs [] >> DISJ2_TAC >> Q.EXISTS_TAC `y` >> ASM_REWRITE_TAC [], 1509 Cases_on `x < n` 1510 >- (ASM_REWRITE_TAC [] >> DISJ2_TAC >> Q.EXISTS_TAC `y` >> ASM_REWRITE_TAC []) \\ 1511 `!a b. ~(a < b) /\ a < SUC b = (a = b)` by DECIDE_TAC \\ 1512 `x = n` by PROVE_TAC [] \\ 1513 METIS_TAC [] ] ]); 1514 1515val amatch = store_thm 1516 ("amatch", 1517 ``!r l. amatch r l = sem r l``, 1518 RW_TAC std_ss 1519 [GSYM da_match, da_match_def, regexp2da_def, da_accepts_na2da, amatch_def] 1520 >> normalForms.REMOVE_ABBR_TAC 1521 >> RW_TAC std_ss [initial_regexp2na_def] 1522 >> Suff `!k. astep r k l = da_step (na2da (regexp2na r)) (set_of_list k) l` 1523 >- RW_TAC std_ss [] 1524 >> Induct_on `l` 1525 >- RW_TAC std_ss 1526 [astep_def, da_step_def, na2da_def, eval_accepts, EXISTS_MEM, 1527 set_of_list, accept_regexp2na_def] 1528 >> ONCE_REWRITE_TAC [astep_def] 1529 >> SIMP_TAC std_ss [da_step_regexp2na, eval_transitions_def, NULL_DEF, TL] 1530 >> RW_TAC std_ss [initial_regexp2na_def, HD]); 1531 1532val acheck = store_thm 1533 ("acheck", 1534 ``!r l. 1535 acheck r f l = 1536 !n. n < LENGTH l /\ sem r (FIRSTN (SUC n) l) ==> f (BUTFIRSTN n l)``, 1537 RW_TAC std_ss 1538 [acheck_def, GSYM da_match, da_match_def, regexp2da_def, da_accepts_na2da] 1539 >> normalForms.REMOVE_ABBR_TAC 1540 >> RW_TAC std_ss [initial_regexp2na_def] 1541 >> Q.SPEC_TAC (`[initial (regexp2na r)]`, `k`) 1542 >> Q.SPEC_TAC (`[]`, `h`) 1543 >> Induct_on `l` >- RW_TAC arith_ss [acheckpt_def, LENGTH] 1544 >> ONCE_REWRITE_TAC [acheckpt_def] 1545 >> RW_TAC std_ss [] 1546 >> normalForms.REMOVE_ABBR_TAC 1547 >> RW_TAC std_ss [] 1548 >> HO_MATCH_MP_TAC 1549 (METIS_PROVE [num_CASES] 1550 ``(P = Q 0 /\ !n. Q (SUC n)) ==> (P = !n. Q n)``) 1551 >> RW_TAC arith_ss 1552 [LENGTH, FIRSTN, BUTFIRSTN, da_step_regexp2na, areport_def, eval_accepts, 1553 accept_regexp2na_def, eval_transitions_def, initial_regexp2na_def]); 1554 1555val () = export_theory (); 1556